diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 623053d9a..3d0cc789e 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -14,7 +14,7 @@ module Cryptol.ModuleSystem.Base where -import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls) +import Cryptol.ModuleSystem.Env (DynamicEnv(..)) import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Monad @@ -22,6 +22,7 @@ import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap) import Cryptol.ModuleSystem.Env (lookupModule , LoadedModule(..) , meCoreLint, CoreLint(..) + , ModContext(..) , ModulePath(..), modulePathLabel) import qualified Cryptol.Eval as E import qualified Cryptol.Eval.Value as E @@ -313,21 +314,15 @@ loadDeps m = -- Type Checking --------------------------------------------------------------- --- | Load the local environment, which consists of the environment for the --- currently opened module, shadowed by the dynamic environment. -getLocalEnv :: ModuleM (IfaceParams,IfaceDecls,R.NamingEnv) -getLocalEnv = - do (params,decls,fNames,_) <- getFocusedEnv - denv <- getDynEnv - let dynDecls = deIfaceDecls denv - return (params,dynDecls `mappend` decls, deNames denv `R.shadowing` fNames) - -- | Typecheck a single expression, yielding a renamed parsed expression, -- typechecked core expression, and a type schema. checkExpr :: P.Expr PName -> ModuleM (P.Expr Name,T.Expr,T.Schema) checkExpr e = do - (params,decls,names) <- getLocalEnv + fe <- getFocusedEnv + let params = mctxParams fe + decls = mctxDecls fe + names = mctxNames fe -- run NoPat npe <- noPat e @@ -348,7 +343,10 @@ checkExpr e = do -- INVARIANT: This assumes that NoPat has already been run on the declarations. checkDecls :: [P.TopDecl PName] -> ModuleM (R.NamingEnv,[T.DeclGroup]) checkDecls ds = do - (params,decls,names) <- getLocalEnv + fe <- getFocusedEnv + let params = mctxParams fe + decls = mctxDecls fe + names = mctxNames fe -- introduce names for the declarations before renaming them declsEnv <- liftSupply (R.namingEnv' (map (R.InModule interactiveName) ds)) diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index 49e2b6d0e..4b200a3d6 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -20,7 +20,7 @@ import Paths_cryptol (getDataDir) import Cryptol.Eval (EvalEnv) import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface -import Cryptol.ModuleSystem.Name (Supply,emptySupply) +import Cryptol.ModuleSystem.Name (Name,Supply,emptySupply) import qualified Cryptol.ModuleSystem.NamingEnv as R import Cryptol.Parser.AST import qualified Cryptol.TypeCheck as T @@ -31,8 +31,8 @@ import Data.ByteString(ByteString) import Control.Monad (guard,mplus) import qualified Control.Exception as X import Data.Function (on) +import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe(fromMaybe) import Data.Semigroup import System.Directory (getAppUserDataDirectory, getCurrentDirectory) import System.Environment(getExecutablePath) @@ -45,6 +45,9 @@ import Control.DeepSeq import Prelude () import Prelude.Compat +import Cryptol.Utils.Panic(panic) +import Cryptol.Utils.PP(pp) + -- Module Environment ---------------------------------------------------------- -- | This is the current state of the interpreter. @@ -178,47 +181,95 @@ hasParamModules :: ModuleEnv -> Bool hasParamModules = not . null . lmLoadedParamModules . meLoadedModules --- | Produce an ifaceDecls that represents the focused environment of the module --- system, as well as a 'NameDisp' for pretty-printing names according to the --- imports. --- --- XXX This could really do with some better error handling, just returning --- mempty when one of the imports fails isn't really desirable. --- --- XXX: This is not quite right. For example, it does not take into --- account *how* things were imported in a module (e.g., qualified). --- It would be simpler to simply store the naming environment that was --- actually used when we renamed the module. -focusedEnv :: ModuleEnv -> (IfaceParams,IfaceDecls,R.NamingEnv,NameDisp) + +-- | Contains enough information to browse what's in scope, +-- or type check new expressions. +data ModContext = ModContext + { mctxParams :: IfaceParams + , mctxDecls :: IfaceDecls + , mctxNames :: R.NamingEnv + , mctxNameDisp :: NameDisp + , mctxTypeProvenace :: Map Name DeclProvenance + , mctxValueProvenance :: Map Name DeclProvenance + } + +-- | Specifies how a declared name came to be in scope. +data DeclProvenance = + NameIsImportedFrom ModName + | NameIsLocalPublic + | NameIsLocalPrivate + | NameIsParameter + | NameIsDynamicDecl + deriving (Eq,Ord) + + +-- | Given the state of the environment, compute information about what's +-- in scope on the REPL. This includes what's in the focused module, plus any +-- additional definitions from the REPL (e.g., let bound names, and @it@). +focusedEnv :: ModuleEnv -> ModContext focusedEnv me = - fromMaybe (noIfaceParams, mempty, mempty, mempty) $ - do fm <- meFocusedModule me - lm <- lookupModule fm me - deps <- mapM loadImport (T.mImports (lmModule lm)) - let (ifaces,names) = unzip deps - Iface { .. } = lmInterface lm - localDecls = ifPublic `mappend` ifPrivate - localNames = R.unqualifiedEnv localDecls `mappend` - R.modParamsNamingEnv ifParams - namingEnv = localNames `R.shadowing` mconcat names - - return ( ifParams - , mconcat (localDecls:ifaces) - , namingEnv - , R.toNameDisp namingEnv) + ModContext + { mctxParams = parameters + , mctxDecls = mconcat (dynDecls : localDecls : importedDecls) + , mctxNames = namingEnv + , mctxNameDisp = R.toNameDisp namingEnv + , mctxTypeProvenace = fst provenance + , mctxValueProvenance = snd provenance + } + where + (importedNames,importedDecls,importedProvs) = unzip3 (map loadImport imports) + localDecls = publicDecls `mappend` privateDecls + localNames = R.unqualifiedEnv localDecls `mappend` + R.modParamsNamingEnv parameters + dynDecls = deIfaceDecls (meDynEnv me) + dynNames = deNames (meDynEnv me) + + namingEnv = dynNames `R.shadowing` + localNames `R.shadowing` + mconcat importedNames + + provenance = shadowProvs + $ declsProv NameIsDynamicDecl dynDecls + : declsProv NameIsLocalPublic publicDecls + : declsProv NameIsLocalPrivate privateDecls + : paramProv parameters + : importedProvs + + (imports, parameters, publicDecls, privateDecls) = + case meFocusedModule me of + Nothing -> (mempty, noIfaceParams, mempty, mempty) + Just fm -> + case lookupModule fm me of + Just lm -> + let Iface { .. } = lmInterface lm + in (T.mImports (lmModule lm), ifParams, ifPublic, ifPrivate) + Nothing -> panic "focusedEnv" ["Focused module is not loaded."] + loadImport imp = - do lm <- lookupModule (iModule imp) me - let decls = ifPublic (lmInterface lm) - return (decls,R.interpImport imp decls) - --- | The unqualified declarations and name environment for the dynamic --- environment. -dynamicEnv :: ModuleEnv -> (IfaceDecls,R.NamingEnv,NameDisp) -dynamicEnv me = (decls,names,R.toNameDisp names) - where - decls = deIfaceDecls (meDynEnv me) - names = R.unqualifiedEnv decls + case lookupModule (iModule imp) me of + Just lm -> + let decls = ifPublic (lmInterface lm) + in ( R.interpImport imp decls + , decls + , declsProv (NameIsImportedFrom (iModule imp)) decls + ) + Nothing -> panic "focusedEnv" + [ "Missing imported module: " ++ show (pp (iModule imp)) ] + + + -- earlier ones shadow + shadowProvs ps = let (tss,vss) = unzip ps + in (Map.unions tss, Map.unions vss) + + paramProv IfaceParams { .. } = (doMap ifParamTypes, doMap ifParamFuns) + where doMap mp = const NameIsParameter <$> mp + + declsProv prov IfaceDecls { .. } = + ( Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ] + , doMap ifDecls + ) + where doMap mp = const prov <$> mp -- Loaded Modules -------------------------------------------------------------- @@ -281,14 +332,23 @@ instance Monoid LoadedModules where data LoadedModule = LoadedModule { lmName :: ModName + -- ^ The name of this module. Should match what's in 'lmModule' + , lmFilePath :: ModulePath -- ^ The file path used to load this module (may not be canonical) + , lmModuleId :: String -- ^ An identifier used to identify the source of the bytes for the module. -- For files we just use the cononical path, for in memory things we -- use their label. + , lmInterface :: Iface + -- ^ The module's interface. This is for convenient. At the moment + -- we have the whole module in 'lmModule', so this could be computer. + , lmModule :: T.Module + -- ^ The actual type-checked module + , lmFingerprint :: Fingerprint } deriving (Show, Generic, NFData) @@ -328,6 +388,8 @@ addLoadedModule path ident fp tm lm } -- | Remove a previously loaded module. +-- Note that this removes exactly the modules specified by the predicate. +-- One should be carfule to preserve the invariant on 'LoadedModules'. removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules removeLoadedModule rm lm = LoadedModules @@ -340,9 +402,8 @@ removeLoadedModule rm lm = -- | Extra information we need to carry around to dynamically extend -- an environment outside the context of a single module. Particularly --- useful when dealing with interactive declarations as in @:let@ or +-- useful when dealing with interactive declarations as in @let@ or -- @it@. - data DynamicEnv = DEnv { deNames :: R.NamingEnv , deDecls :: [T.DeclGroup] diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index a6037dfee..4218f1940 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -19,8 +19,7 @@ import Cryptol.ModuleSystem.Env import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Name (FreshM(..),Supply) -import Cryptol.ModuleSystem.Renamer - (RenamerError(),RenamerWarning(),NamingEnv) +import Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning()) import qualified Cryptol.Parser as Parser import qualified Cryptol.Parser.AST as P import Cryptol.Parser.Position (Located) @@ -508,8 +507,7 @@ withPrependedSearchPath fps m = ModuleT $ do set $! env { meSearchPath = fps0 } return x --- XXX improve error handling here -getFocusedEnv :: ModuleM (IfaceParams,IfaceDecls,NamingEnv,NameDisp) +getFocusedEnv :: ModuleM ModContext getFocusedEnv = ModuleT (focusedEnv `fmap` get) getDynEnv :: ModuleM DynamicEnv diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 7f9a84cf2..b5d07ecd9 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -72,7 +72,7 @@ import qualified Cryptol.TypeCheck.Parseable as T import qualified Cryptol.TypeCheck.Subst as T import Cryptol.TypeCheck.Solve(defaultReplExpr) import qualified Cryptol.TypeCheck.Solver.SMT as SMT -import Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap,backticks) +import Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap) import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic) import qualified Cryptol.Parser.AST as P @@ -89,7 +89,8 @@ import qualified Data.ByteString.Char8 as BS8 import Data.Bits (shiftL, (.&.), (.|.)) import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii) import Data.Function (on) -import Data.List (intercalate, nub, sortBy, partition, isPrefixOf,intersperse) +import Data.List (intercalate, nub, sortBy, groupBy, + partition, isPrefixOf,intersperse) import Data.Maybe (fromMaybe,mapMaybe,isNothing) import System.Environment (lookupEnv) import System.Exit (ExitCode(ExitSuccess)) @@ -99,6 +100,7 @@ import System.FilePath((), isPathSeparator) import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist ,getTemporaryDirectory,setPermissions,removeFile ,emptyPermissions,setOwnerReadable) +import Data.Map (Map) import qualified Data.Map as Map import qualified Data.Set as Set import System.IO(hFlush,stdout,openTempFile,hClose) @@ -732,9 +734,9 @@ typeOfCmd str = do -- XXX need more warnings from the module system whenDebug (rPutStrLn (dump def)) - (_,_,_,names) <- getFocusedEnv + fDisp <- M.mctxNameDisp <$> getFocusedEnv -- type annotation ':' has precedence 2 - rPrint $ runDoc names $ ppPrec 2 expr <+> text ":" <+> pp sig + rPrint $ runDoc fDisp $ ppPrec 2 expr <+> text ":" <+> pp sig readFileCmd :: FilePath -> REPL () readFileCmd fp = do @@ -905,10 +907,6 @@ quitCmd = stop browseCmd :: String -> REPL () browseCmd input = do - (params, iface, fNames, disp) <- getFocusedEnv - denv <- getDynEnv - let names = M.deNames denv `M.shadowing` fNames - let mnames = map (M.textToModName . T.pack) (words input) validModNames <- (:) M.interactiveName <$> getModNames let checkModName m = @@ -916,6 +914,16 @@ browseCmd input = do rPutStrLn ("error: " ++ show m ++ " is not a loaded module.") mapM_ checkModName mnames + fe <- getFocusedEnv + + let params = M.mctxParams fe + iface = M.mctxDecls fe + names = M.mctxNames fe + disp = M.mctxNameDisp fe + provV = M.mctxValueProvenance fe + provT = M.mctxTypeProvenace fe + + let f &&& g = \x -> f x && g x isUser x = case M.nameInfo x of M.Declared _ M.SystemName -> False @@ -929,16 +937,15 @@ browseCmd input = do visibleType = isUser &&& restricted &&& inSet visibleTypes visibleDecl = isUser &&& restricted &&& inSet visibleDecls - browseMParams visibleType visibleDecl params disp - browseTSyns visibleType iface disp - browsePrimTys visibleType iface disp - browseNewtypes visibleType iface disp - browseVars visibleDecl iface disp + browseTSyns visibleType provT iface disp + browsePrimTys visibleType provT iface disp + browseNewtypes visibleType provT iface disp + browseVars visibleDecl provV iface disp browseMParams :: (M.Name -> Bool) -> (M.Name -> Bool) -> - M.IfaceParams-> NameDisp -> REPL () + M.IfaceParams -> NameDisp -> REPL () browseMParams visT visD M.IfaceParams { .. } names = do ppBlock names ppParamTy "Type Parameters" (sorted visT T.mtpName ifParamTypes) @@ -953,53 +960,150 @@ browseMParams visT visD M.IfaceParams { .. } names = sorted vis nm mp = sortBy (M.cmpNameDisplay names `on` nm) $ filter (vis . nm) $ Map.elems mp - -browsePrimTys :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL () -browsePrimTys isVisible M.IfaceDecls { .. } names = - do let pts = sortBy (M.cmpNameDisplay names `on` T.atName) - [ ts | ts <- Map.elems ifAbstractTypes, isVisible (T.atName ts) ] - ppBlock names ppA "Primitive Types" pts +type Prov = Map M.Name M.DeclProvenance + +browsePrimTys :: (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL () +browsePrimTys isVisible prov M.IfaceDecls { .. } names = + ppSection (Map.elems ifAbstractTypes) + Section { secName = "Primitive Types" + , secEntryName = T.atName + , secProvenance = prov + , secDisp = names + , secPP = ppA + , secVisible = isVisible + } where ppA a = pp (T.atName a) <+> ":" <+> pp (T.atKind a) -browseTSyns :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL () -browseTSyns isVisible M.IfaceDecls { .. } names = do - let tsyns = sortBy (M.cmpNameDisplay names `on` T.tsName) - [ ts | ts <- Map.elems ifTySyns, isVisible (T.tsName ts) ] - (cts,tss) = partition isCtrait tsyns +browseTSyns :: (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL () +browseTSyns isVisible prov M.IfaceDecls { .. } names = + do ppSection tss + Section { secName = "Type Synonyms" + , secEntryName = T.tsName + , secProvenance = prov + , secDisp = names + , secVisible = isVisible + , secPP = pp + } + ppSection cts + Section { secName = "Constraint Synonyms" + , secEntryName = T.tsName + , secProvenance = prov + , secDisp = names + , secVisible = isVisible + , secPP = pp + } + where + (cts,tss) = partition isCtrait (Map.elems ifTySyns) + isCtrait t = T.kindResult (T.kindOf (T.tsDef t)) == T.KProp - ppBlock names pp "Type Synonyms" tss - ppBlock names pp "Constraint Synonyms" cts +browseNewtypes :: + (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL () +browseNewtypes isVisible prov M.IfaceDecls { .. } names = + ppSection (Map.elems ifNewtypes) + Section { secName = "Newtypes" + , secEntryName = T.ntName + , secVisible = isVisible + , secProvenance = prov + , secDisp = names + , secPP = T.ppNewtypeShort + } + +browseVars :: (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL () +browseVars isVisible prov M.IfaceDecls { .. } names = + do ppSection props Section { secName = "Properties" + , secEntryName = M.ifDeclName + , secVisible = isVisible + , secProvenance = prov + , secDisp = names + , secPP = ppVar + } + ppSection syms Section { secName = "Symbols" + , secEntryName = M.ifDeclName + , secVisible = isVisible + , secProvenance = prov + , secDisp = names + , secPP = ppVar + } where - isCtrait t = T.kindResult (T.kindOf (T.tsDef t)) == T.KProp + isProp p = T.PragmaProperty `elem` (M.ifDeclPragmas p) + (props,syms) = partition isProp (Map.elems ifDecls) -browseNewtypes :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL () -browseNewtypes isVisible M.IfaceDecls { .. } names = do - let nts = sortBy (M.cmpNameDisplay names `on` T.ntName) - [ nt | nt <- Map.elems ifNewtypes, isVisible (T.ntName nt) ] - unless (null nts) $ do - rPutStrLn "Newtypes" - rPutStrLn "========" - rPrint (runDoc names (nest 4 (vcat (map T.ppNewtypeShort nts)))) - rPutStrLn "" + ppVar M.IfaceDecl { .. } = hang (pp ifDeclName <+> char ':') 2 (pp ifDeclSig) -browseVars :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL () -browseVars isVisible M.IfaceDecls { .. } names = do - let vars = sortBy (M.cmpNameDisplay names `on` M.ifDeclName) - [ d | d <- Map.elems ifDecls, isVisible (M.ifDeclName d) ] - let isProp p = T.PragmaProperty `elem` (M.ifDeclPragmas p) - (props,syms) = partition isProp vars +data Section a = Section + { secName :: String + , secEntryName :: a -> M.Name + , secVisible :: M.Name -> Bool + , secProvenance :: Map M.Name M.DeclProvenance + , secDisp :: NameDisp + , secPP :: a -> Doc + } +ppSection :: [a] -> Section a -> REPL () +ppSection things s + | null grouped = pure () + | otherwise = + do let heading = secName s + rPutStrLn heading + rPutStrLn (map (const '=') heading) + rPutStrLn "" + mapM_ ppSub grouped - let ppVar M.IfaceDecl { .. } = hang (pp ifDeclName <+> char ':') - 2 (pp ifDeclSig) + where + ppSub (p,ts) = + do let heading = provHeading p + rPutStrLn (" " ++ heading) + rPutStrLn (" " ++ map (const '-') heading) + rPutStrLn "" + rPutStrLn $ show $ runDoc (secDisp s) $ nest 4 $ vcat $ map (secPP s) ts + rPutStrLn "" + + grouped = map rearrange $ + groupBy sameProv $ + sortBy cmpThings + [ (n,p,t) | t <- things, + let n = secEntryName s t, + secVisible s n, + let p = case Map.lookup n (secProvenance s) of + Just i -> i + Nothing -> panic "ppSection" + [ "Name with no provenance" + , show n ] + ] + + rearrange xs = (p, [ a | (_,_,a) <- xs ]) + where (_,p,_) : _ = xs + + cmpThings (n1, p1, _) (n2, p2, _) = + case cmpProv p1 p2 of + EQ -> M.cmpNameDisplay (secDisp s) n1 n2 + r -> r + + sameProv (_,p1,_) (_,p2,_) = provOrd p1 == provOrd p2 + + provOrd p = + case p of + M.NameIsParameter -> Left 1 :: Either Int P.ModName + M.NameIsDynamicDecl -> Left 2 + M.NameIsLocalPublic -> Left 3 + M.NameIsLocalPrivate -> Left 4 + M.NameIsImportedFrom x -> Right x + + cmpProv p1 p2 = compare (provOrd p1) (provOrd p2) + + provHeading p = + case p of + M.NameIsParameter -> "Parameters" + M.NameIsDynamicDecl -> "REPL" + M.NameIsLocalPublic -> "Public" + M.NameIsLocalPrivate -> "Private" + M.NameIsImportedFrom m -> "From " ++ show (pp m) - ppBlock names ppVar "Properties" props - ppBlock names ppVar "Symbols" syms ppBlock :: NameDisp -> (a -> Doc) -> String -> [a] -> REPL () @@ -1010,7 +1114,6 @@ ppBlock names ppFun name xs = unless (null xs) $ rPutStrLn "" - setOptionCmd :: String -> REPL () setOptionCmd str | Just value <- mbValue = setUser key value @@ -1053,12 +1156,17 @@ helpCmd cmd | otherwise = case parseHelpName cmd of Just qname -> - do (params,env,rnEnv,nameEnv) <- getFocusedEnv - let vNames = M.lookupValNames qname rnEnv + do fe <- getFocusedEnv + let params = M.mctxParams fe + env = M.mctxDecls fe + rnEnv = M.mctxNames fe + disp = M.mctxNameDisp fe + + vNames = M.lookupValNames qname rnEnv tNames = M.lookupTypeNames qname rnEnv - let helps = map (showTypeHelp params env nameEnv) tNames ++ - map (showValHelp params env nameEnv qname) vNames + let helps = map (showTypeHelp params env disp) tNames ++ + map (showValHelp params env disp qname) vNames separ = rPutStrLn " ---------" sequence_ (intersperse separ helps) @@ -1298,7 +1406,7 @@ moduleCmdResult (res,ws0) = do filterShadowing w = Just w let ws = mapMaybe filterDefaults . mapMaybe filterShadowing $ ws0 - (_,_,_,names) <- getFocusedEnv + names <- M.mctxNameDisp <$> getFocusedEnv mapM_ (rPrint . runDoc names . pp) ws case res of Right (a,me') -> setModuleEnv me' >> return a diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index ec6df681a..e38905d46 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -36,7 +36,6 @@ module Cryptol.REPL.Monad ( , getModuleEnv, setModuleEnv , getDynEnv, setDynEnv , uniqify, freshName - , getTSyns, getNewtypes, getVars , whenDebug , getExprNames , getTypeNames @@ -474,75 +473,33 @@ rPutStrLn str = rPutStr $ str ++ "\n" rPrint :: Show a => a -> REPL () rPrint x = rPutStrLn (show x) -getFocusedEnv :: REPL (M.IfaceParams,M.IfaceDecls,M.NamingEnv,NameDisp) -getFocusedEnv = do - me <- getModuleEnv - -- dyNames is a NameEnv that removes the #Uniq prefix from interactively-bound - -- variables. - let (dyDecls,dyNames,dyDisp) = M.dynamicEnv me - let (fParams,fDecls,fNames,fDisp) = M.focusedEnv me - return ( fParams - , dyDecls `mappend` fDecls - , dyNames `M.shadowing` fNames - , dyDisp `mappend` fDisp) - - -- -- the subtle part here is removing the #Uniq prefix from - -- -- interactively-bound variables, and also excluding any that are - -- -- shadowed and thus can no longer be referenced - -- let (fDecls,fNames,fDisp) = M.focusedEnv me - -- edecls = M.ifDecls dyDecls - -- -- is this QName something the user might actually type? - -- isShadowed (qn@(P.QName (Just (P.unModName -> ['#':_])) name), _) = - -- case Map.lookup localName neExprs of - -- Nothing -> False - -- Just uniqueNames -> isNamed uniqueNames - -- where localName = P.QName Nothing name - -- isNamed us = any (== qn) (map M.qname us) - -- neExprs = M.neExprs (M.deNames (M.meDynEnv me)) - -- isShadowed _ = False - -- unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds) - -- edecls' = Map.fromList - -- . map unqual - -- . filter isShadowed - -- $ Map.toList edecls - -- return (decls `mappend` mempty { M.ifDecls = edecls' }, names `mappend` dyNames) - -getVars :: REPL (Map.Map M.Name M.IfaceDecl) -getVars = do - (_,decls,_,_) <- getFocusedEnv - return (M.ifDecls decls) - -getTSyns :: REPL (Map.Map M.Name T.TySyn) -getTSyns = do - (_,decls,_,_) <- getFocusedEnv - return (M.ifTySyns decls) - -getNewtypes :: REPL (Map.Map M.Name T.Newtype) -getNewtypes = do - (_,decls,_,_) <- getFocusedEnv - return (M.ifNewtypes decls) +getFocusedEnv :: REPL M.ModContext +getFocusedEnv = M.focusedEnv <$> getModuleEnv -- | Get visible variable names. +-- This is used for command line completition. getExprNames :: REPL [String] getExprNames = - do (_,_, fNames, _) <- getFocusedEnv + do fNames <- M.mctxNames <$> getFocusedEnv return (map (show . pp) (Map.keys (M.neExprs fNames))) -- | Get visible type signature names. +-- This is used for command line completition. getTypeNames :: REPL [String] getTypeNames = - do (_,_, fNames, _) <- getFocusedEnv + do fNames <- M.mctxNames <$> getFocusedEnv return (map (show . pp) (Map.keys (M.neTypes fNames))) -- | Return a list of property names, sorted by position in the file. getPropertyNames :: REPL ([M.Name],NameDisp) getPropertyNames = - do (_,decls,_,names) <- getFocusedEnv - let xs = M.ifDecls decls + do fe <- getFocusedEnv + let xs = M.ifDecls (M.mctxDecls fe) ps = sortBy (comparing (from . M.nameLoc)) - $ [ x | (x,d) <- Map.toList xs, T.PragmaProperty `elem` M.ifDeclPragmas d ] + [ x | (x,d) <- Map.toList xs, + T.PragmaProperty `elem` M.ifDeclPragmas d ] - return (ps, names) + return (ps, M.mctxNameDisp fe) getModNames :: REPL [I.ModName] getModNames = diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index d8d8880d7..5154a3e23 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -4,6 +4,10 @@ Loading module issue226r2 Loading module issue226 Type Synonyms ============= + + From Cryptol + ------------ + type Bool = Bit type Char = [8] type lg2 n = width (max 1 n - 1) @@ -12,12 +16,20 @@ Type Synonyms Constraint Synonyms =================== + + From Cryptol + ------------ + type constraint i < j = j >= 1 + i type constraint i <= j = j >= i type constraint i > j = i >= 1 + j Primitive Types =============== + + From Cryptol + ------------ + (!=) : # -> # -> Prop (==) : # -> # -> Prop (>=) : # -> # -> Prop @@ -47,6 +59,15 @@ Primitive Types Symbols ======= + + Public + ------ + + foo : {a} a -> a + + From Cryptol + ------------ + (==>) : Bit -> Bit -> Bit (\/) : Bit -> Bit -> Bit (/\) : Bit -> Bit -> Bit @@ -98,7 +119,6 @@ Symbols False : Bit foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b - foo : {a} a -> a fromInteger : {a} (Arith a) => Integer -> a fromThenTo : {first, next, last, a, len} (fin first, fin next, fin last, diff --git a/tests/modsys/T10.icry.stdout b/tests/modsys/T10.icry.stdout index 0d7fbdb39..f4e0c8127 100644 --- a/tests/modsys/T10.icry.stdout +++ b/tests/modsys/T10.icry.stdout @@ -2,5 +2,9 @@ Loading module Cryptol Loading module T10::Main Symbols ======= + + Public + ------ + f : {T} {x : T} -> T