Allow focusing of parameterized modules; disable evaluation in such contexts.

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 $
+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
-         return ()
+            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 ()
 
 
 

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

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

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)

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