From c3d8b4b3f800e1adf3f68f70a5c5d4517c821186 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 18 Oct 2017 14:33:12 -0700 Subject: [PATCH] Allow focusing of parameterized modules; disable evaluation in such contexts. --- src/Cryptol/ModuleSystem/Base.hs | 37 ++++++++++++++++-------------- src/Cryptol/ModuleSystem/Env.hs | 38 ++++++++++++++++--------------- src/Cryptol/ModuleSystem/Monad.hs | 18 ++++++++++++--- src/Cryptol/REPL/Command.hs | 5 +++- src/Cryptol/REPL/Monad.hs | 24 ++++++++++++++++++- 5 files changed, 82 insertions(+), 40 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 4c13e85f..27e88276 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -48,7 +48,7 @@ import Cryptol.Transform.MonoValues (rewModule) import Control.DeepSeq import qualified Control.Exception as X -import Control.Monad (unless) +import Control.Monad (unless,when) import Data.Maybe (fromMaybe) import Data.Monoid ((<>)) import Data.Text.Lazy (Text) @@ -148,20 +148,21 @@ loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do -- | Load a module that arouse a dependnecy -loadDep :: (ModuleM () -> ModuleM ()) -> P.ModName -> ModuleM () -loadDep what n = do - - alreadyLoaded <- isLoaded n - unless alreadyLoaded $ - do path <- findModule n - pm <- parseModule path - what $ do - - -- make sure that this module is the one we expect - unless (n == thing (P.mName pm)) (moduleNameMismatch n (mName pm)) - - _ <- loadModule path pm - return () +loadDep :: (ModuleM T.Module -> ModuleM T.Module) -> + P.ModName -> + ModuleM T.Module +loadDep what n = + do mb <- getLoadedMaybe n + case mb of + Just m -> return (lmModule m) + Nothing -> + do path <- findModule n + pm <- parseModule path + what $ + do -- make sure that this module is the one we expect + unless (n == thing (P.mName pm)) + (moduleNameMismatch n (mName pm)) + loadModule path pm @@ -270,8 +271,10 @@ loadDeps m = do mapM_ loadI (P.mImports m) mapM_ loadF (P.mInstance m) where - loadI i = loadDep (loadingImport i) (P.iModule (thing i)) - loadF f = loadDep (loadingModInstance f) (thing f) + loadI i = do md <- loadDep (loadingImport i) (P.iModule (thing i)) + when (T.isParametrizedModule md) (importParamModule (T.mName md)) + loadF f = do _ <- loadDep (loadingModInstance f) (thing f) + return () diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index d1843754..46399414 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -211,25 +211,27 @@ dynamicEnv me = (decls,names,R.toNameDisp names) -- Loaded Modules -------------------------------------------------------------- data LoadedModules = LoadedModules - { getLoadedModules :: [LoadedModule] + { lmLoadedModules :: [LoadedModule] -- ^ Invariants: -- 1) All the dependencies of any module `m` must precede `m` in the list. -- 2) Does not contain any parameterized modules. - , getLoadedParamModules :: [LoadedModule] + , lmLoadedParamModules :: [LoadedModule] -- ^ Loaded parameterized modules. } deriving (Show, Generic, NFData) +getLoadedModules :: LoadedModules -> [LoadedModule] +getLoadedModules x = lmLoadedParamModules x ++ lmLoadedModules x + instance Monoid LoadedModules where - mempty = LoadedModules { getLoadedModules = [] - , getLoadedParamModules = [] + mempty = LoadedModules { lmLoadedModules = [] + , lmLoadedParamModules = [] } mappend l r = LoadedModules - { getLoadedModules = List.unionBy ((==) `on` lmName) - (getLoadedModules l) (getLoadedModules r) - , getLoadedParamModules = getLoadedParamModules l ++ - getLoadedParamModules r } + { lmLoadedModules = List.unionBy ((==) `on` lmName) + (lmLoadedModules l) (lmLoadedModules r) + , lmLoadedParamModules = lmLoadedParamModules l ++ lmLoadedParamModules r } data LoadedModule = LoadedModule { lmName :: ModName @@ -247,8 +249,8 @@ isLoaded mn lm = any ((mn ==) . lmName) (getLoadedModules lm) -- | Try to find a previously loaded module lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule -lookupModule mn me = search getLoadedModules `mplus` - search getLoadedParamModules +lookupModule mn me = search lmLoadedModules `mplus` + search lmLoadedParamModules where search how = List.find ((mn ==) . lmName) (how (meLoadedModules me)) @@ -259,10 +261,10 @@ addLoadedModule :: FilePath -> FilePath -> T.Module -> LoadedModules -> LoadedModules addLoadedModule path canonicalPath tm lm | isLoaded (T.mName tm) lm = lm - | T.isParametrizedModule tm = lm { getLoadedParamModules = loaded : - getLoadedParamModules lm } - | otherwise = lm { getLoadedModules = - getLoadedModules lm ++ [loaded] } + | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded : + lmLoadedParamModules lm } + | otherwise = lm { lmLoadedModules = + lmLoadedModules lm ++ [loaded] } where loaded = LoadedModule { lmName = T.mName tm @@ -275,11 +277,11 @@ addLoadedModule path canonicalPath tm lm -- | Remove a previously loaded module. removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules removeLoadedModule path lm = - case rm getLoadedModules of - Just newLms -> lm { getLoadedModules = newLms } + case rm lmLoadedModules of + Just newLms -> lm { lmLoadedModules = newLms } Nothing -> - case rm getLoadedParamModules of - Just newLms -> lm { getLoadedParamModules = newLms } + case rm lmLoadedParamModules of + Just newLms -> lm { lmLoadedParamModules = newLms } Nothing -> lm where rm f = case break ((path ==) . lmFilePath) (f lm) of diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index f8f5b2b2..b1bc0ef5 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -95,6 +95,8 @@ data ModuleError -- ^ Module loaded by 'import' statement has the wrong module name | DuplicateModuleName P.ModName FilePath FilePath -- ^ Two modules loaded from different files have the same module name + | ImportedParamModule P.ModName + -- ^ Attempt to import a parametrized module that was not instantiated. deriving (Show) instance NFData ModuleError where @@ -113,6 +115,7 @@ instance NFData ModuleError where DuplicateModuleName name path1 path2 -> name `deepseq` path1 `deepseq` path2 `deepseq` () OtherFailure x -> x `deepseq` () + ImportedParamModule x -> x `deepseq` () instance PP ModuleError where ppPrec _ e = case e of @@ -163,6 +166,9 @@ instance PP ModuleError where OtherFailure x -> text x + ImportedParamModule p -> + text "Import of a non-instantiated parameterized module:" <+> pp p + @@ -210,6 +216,9 @@ duplicateModuleName :: P.ModName -> FilePath -> FilePath -> ModuleM a duplicateModuleName name path1 path2 = ModuleT (raise (DuplicateModuleName name path1 path2)) +importParamModule :: P.ModName -> ModuleM a +importParamModule x = ModuleT (raise (ImportedParamModule x)) + -- Warnings -------------------------------------------------------------------- @@ -318,10 +327,13 @@ modifyModuleEnv f = ModuleT $ do env <- get set $! f env +getLoadedMaybe :: P.ModName -> ModuleM (Maybe LoadedModule) +getLoadedMaybe mn = ModuleT $ + do env <- get + return (lookupModule mn env) + isLoaded :: P.ModName -> ModuleM Bool -isLoaded mn = ModuleT $ do - env <- get - return (isJust (lookupModule mn env)) +isLoaded mn = isJust <$> getLoadedMaybe mn loadingImport :: Located P.Import -> ModuleM a -> ModuleM a loadingImport = loading . FromImport diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index cff1a7d8..ecc3cd15 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -640,6 +640,7 @@ specializeCmd str = do refEvalCmd :: String -> REPL () refEvalCmd str = do + validEvalContext parseExpr <- replParseExpr str (_, expr, _schema) <- replCheckExpr parseExpr val <- liftModuleCmd (rethrowEvalError . R.evaluate expr) @@ -1065,7 +1066,8 @@ replSpecExpr e = liftModuleCmd $ S.specialize e replEvalExpr :: P.Expr P.PName -> REPL (E.Value, T.Type) replEvalExpr expr = - do (_,def,sig) <- replCheckExpr expr + do validEvalContext + (_,def,sig) <- replCheckExpr expr me <- getModuleEnv let cfg = M.meSolverConfig me @@ -1137,6 +1139,7 @@ bindItVariables ty exprs = bindItVariable seqTy seqExpr replEvalDecl :: P.Decl P.PName -> REPL () replEvalDecl decl = do + validEvalContext dgs <- replCheckDecls [decl] whenDebug (mapM_ (\dg -> (rPutStrLn (dump dg))) dgs) liftModuleCmd (M.evalDecls dgs) diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 4e3b3eab..258df756 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -49,6 +49,7 @@ module Cryptol.REPL.Monad ( , disableLet , enableLet , getLetEnabled + , validEvalContext , updateREPLTitle , setUpdateREPLTitle @@ -230,6 +231,7 @@ data REPLException | ModuleSystemError NameDisp M.ModuleError | EvalPolyError T.Schema | TypeNotTestable T.Type + | EvalInParamModule P.ModName deriving (Show,Typeable) instance X.Exception REPLException @@ -253,6 +255,9 @@ instance PP REPLException where $$ text "Type:" <+> pp s TypeNotTestable t -> text "The expression is not of a testable type." $$ text "Type:" <+> pp t + EvalInParamModule m -> text "The current module," <+> pp m <> comma <+> + text "is parameterized, and does not support" <+> + text "evaluation." -- | Raise an exception. raise :: REPLException -> REPL a @@ -278,6 +283,7 @@ rethrowEvalError m = run `X.catch` rethrow -- Primitives ------------------------------------------------------------------ + io :: IO a -> REPL a io m = REPL (\ _ -> m) @@ -345,6 +351,22 @@ enableLet = modifyRW_ (\ rw -> rw { eLetEnabled = True }) getLetEnabled :: REPL Bool getLetEnabled = fmap eLetEnabled getRW +-- | Is evaluation enabled. If the currently focused module is +-- parameterized, then we cannot evalute. +validEvalContext :: REPL () +validEvalContext = + do me <- eModuleEnv <$> getRW + case M.meFocusedModule me of + Nothing -> return () + Just fm -> + case M.lookupModule fm me of + Just m -> when (T.isParametrizedModule (M.lmModule m)) + $ raise $ EvalInParamModule fm + Nothing -> + panic "getEvalEnabled" ["The focused module is not loaded." + , show fm ] + + -- | Update the title updateREPLTitle :: REPL () updateREPLTitle = unlessBatch $ do @@ -456,7 +478,7 @@ getPropertyNames = getModNames :: REPL [I.ModName] getModNames = do me <- getModuleEnv - return $ map M.lmName $ M.getLoadedModules $ M.meLoadedModules me + return (map T.mName (M.loadedModules me)) getModuleEnv :: REPL M.ModuleEnv getModuleEnv = eModuleEnv `fmap` getRW