Refactor module system things; better loading of `A modules.

src/Cryptol/ModuleSystem.hs

@@ -16,7 +16,7 @@ module Cryptol.ModuleSystem (
   , ModuleCmd, ModuleRes
   , findModule
   , loadModuleByPath
-  , loadModule
+  , loadModuleByName
   , checkExpr
   , evalExpr
   , checkDecls
@@ -61,25 +61,20 @@ findModule :: P.ModName -> ModuleCmd FilePath
 findModule n env = runModuleM env (Base.findModule n)
 
 -- | Load the module contained in the given file.
-loadModuleByPath :: FilePath -> ModuleCmd T.Module
+loadModuleByPath :: FilePath -> ModuleCmd (FilePath,T.Module)
 loadModuleByPath path (evo,env) = runModuleM (evo,resetModuleEnv env) $ do
-  -- unload the module if it already exists
-  unloadModule path
-
+  unloadModule ((path ==) . lmFilePath)
   m <- Base.loadModuleByPath path
   setFocusedModule (T.mName m)
-  return m
+  return (path,m)
 
 -- | Load the given parsed module.
-loadModule :: FilePath -> P.Module PName -> ModuleCmd T.Module
-loadModule path m env = runModuleM env $ do
-  -- unload the module if it already exists
-  unloadModule path
-
-  let n = P.thing (P.mName m)
-  m' <- loadingModule n (Base.loadModule path n m)
+loadModuleByName :: P.ModName -> ModuleCmd (FilePath,T.Module)
+loadModuleByName n env = runModuleM env $ do
+  unloadModule ((n ==) . lmName)
+  (path,m') <- Base.loadModuleFrom (FromModule n)
   setFocusedModule (T.mName m')
-  return m'
+  return (path,m')
 
 -- Extended Environments -------------------------------------------------------
 

src/Cryptol/ModuleSystem/Base.hs

@@ -143,50 +143,49 @@ loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
   path' <- io $ canonicalizePath foundPath
   case lookupModule n env of
     -- loadModule will calculate the canonical path again
-    Nothing -> loadingModule n (loadModule foundPath n pm)
+    Nothing -> doLoadModule (FromModule n) foundPath pm
     Just lm
      | path' == loaded -> return (lmModule lm)
      | otherwise       -> duplicateModuleName n path' loaded
      where loaded = lmCanonicalPath lm
 
 
--- | Load a module that arouse a dependnecy
-loadDep :: (ModuleM T.Module -> ModuleM T.Module) -> P.ModName ->
-                                                        ModuleM T.Module
-loadDep what n =
-  do mb <- getLoadedMaybe n
+-- | Load a module, unless it was previously loaded.
+loadModuleFrom :: ImportSource -> ModuleM (FilePath,T.Module)
+loadModuleFrom isrc =
+  do let n = importedModule isrc
+     mb <- getLoadedMaybe n
      case mb of
-       Just m -> return (lmModule m)
+       Just m -> return (lmFilePath m, lmModule m)
        Nothing ->
          do path <- findModule n
-            pm   <- parseModule path
-            what $
-              do -- make sure that this module is the one we expect
-                 unless (notParamInstModName n == thing (P.mName pm))
-                        (moduleNameMismatch n (mName pm))
-                 loadModule path n pm
-
+            pm <- parseModule path
+            m  <- doLoadModule isrc path pm
+            return (path,m)
 
 -- | Load dependencies, typecheck, and add to the eval environment.
-loadModule :: FilePath -> P.ModName -> P.Module PName -> ModuleM T.Module
-loadModule path mn pm = do
+doLoadModule :: ImportSource ->
+              FilePath ->
+              P.Module PName ->
+              ModuleM T.Module
+doLoadModule isrc path pm0 =
+  loading isrc $
+  do let pm = addPrelude pm0
+     loadDeps pm
 
+     withLogger logPutStrLn
+       ("Loading module " ++ pretty (P.thing (P.mName pm)))
+     tcm <- optionalInstantiate =<< checkModule isrc path pm
 
-  let pm' = addPrelude pm
-  loadDeps pm'
+     -- extend the eval env, unless a functor.
+     unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv tcm)
+     canonicalPath <- io (canonicalizePath path)
+     loadedModule path canonicalPath tcm
 
-  withLogger logPutStrLn ("Loading module " ++ pretty (P.thing (P.mName pm')))
-  tcm <- optionalInstantiate =<< checkModule path pm'
-
-  -- extend the eval env
-  unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv tcm)
-  canonicalPath <- io (canonicalizePath path)
-  loadedModule path canonicalPath tcm
-
-  return tcm
+     return tcm
   where
   optionalInstantiate tcm
-    | isParamInstModName mn && T.isParametrizedModule tcm =
+    | isParamInstModName (importedModule isrc) && T.isParametrizedModule tcm =
       case addModParams tcm of
         Right tcm1 -> return tcm1
         Left xs    -> failedToParameterizeModDefs (T.mName tcm) xs
@@ -283,9 +282,9 @@ loadDeps m =
   do mapM_ loadI (P.mImports m)
      mapM_ loadF (P.mInstance m)
   where
-  loadI i = do m1 <- loadDep (loadingImport i) (P.iModule (thing i))
+  loadI i = do (_,m1)  <- loadModuleFrom (FromImport i)
                when (T.isParametrizedModule m1) $ importParamModule $ T.mName m1
-  loadF f = do _ <- loadDep (loadingModInstance f) (thing f)
+  loadF f = do _ <- loadModuleFrom (FromModuleInstance f)
                return ()
 
 
@@ -352,12 +351,12 @@ getPrimMap  =
                   [ "Unable to find the prelude" ]
 
 -- | Load a module, be it a normal module or a functor instantiation.
-checkModule :: FilePath -> P.Module PName -> ModuleM T.Module
-checkModule path m =
+checkModule :: ImportSource -> FilePath -> P.Module PName -> ModuleM T.Module
+checkModule isrc path m =
   case P.mInstance m of
-    Nothing -> checkSingleModule T.tcModule path m
+    Nothing -> checkSingleModule T.tcModule isrc path m
     Just fmName -> do tf <- getLoaded (thing fmName)
-                      checkSingleModule (T.tcModuleInst tf) path m
+                      checkSingleModule (T.tcModuleInst tf) isrc path m
 
 
 -- | Typecheck a single module.  If the module is an instantiation
@@ -365,10 +364,17 @@ checkModule path m =
 -- See 'checkModule'
 checkSingleModule ::
   Act (P.Module Name) T.Module {- ^ how to check -} ->
+  ImportSource                 {- ^ why are we loading this -} ->
   FilePath                     {- path -} ->
-  P.Module PName               {- ^ check this -} ->
+  P.Module PName               {- ^ module to check -} ->
   ModuleM T.Module
-checkSingleModule how path m = do
+checkSingleModule how isrc path m = do
+
+  -- check that the name of the module matches expectations
+  let nm = importedModule isrc
+  unless (notParamInstModName nm == thing (P.mName m))
+         (moduleNameMismatch nm (mName m))
+
   -- remove includes first
   e   <- io (removeIncludesModule path m)
   nim <- case e of

src/Cryptol/ModuleSystem/Env.hs

@@ -275,18 +275,12 @@ addLoadedModule path canonicalPath tm lm
     }
 
 -- | Remove a previously loaded module.
-removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules
-removeLoadedModule path lm =
-  case rm lmLoadedModules of
-    Just newLms -> lm { lmLoadedModules = newLms }
-    Nothing ->
-      case rm lmLoadedParamModules of
-        Just newLms -> lm { lmLoadedParamModules = newLms }
-        Nothing     -> lm
-  where
-  rm f = case break ((path ==) . lmFilePath) (f lm) of
-           (as,_:bs) -> Just (as ++ bs)
-           _         -> Nothing
+removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules
+removeLoadedModule rm lm =
+  LoadedModules
+    { lmLoadedModules = filter (not . rm) (lmLoadedModules lm)
+    , lmLoadedParamModules = filter (not . rm) (lmLoadedParamModules lm)
+    }
 
 
 -- Dynamic Environments --------------------------------------------------------

src/Cryptol/ModuleSystem/Monad.hs

@@ -422,11 +422,10 @@ setSupply supply = ModuleT $
   do env <- get
      set $! env { meSupply = supply }
 
--- | Remove a module from the set of loaded module, by its path.
-unloadModule :: FilePath -> ModuleM ()
-unloadModule path = ModuleT $ do
+unloadModule :: (LoadedModule -> Bool) -> ModuleM ()
+unloadModule rm = ModuleT $ do
   env <- get
-  set $! env { meLoadedModules = removeLoadedModule path (meLoadedModules env) }
+  set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) }
 
 loadedModule :: FilePath -> FilePath -> T.Module -> ModuleM ()
 loadedModule path canonicalPath m = ModuleT $ do

src/Cryptol/REPL/Command.hs

@@ -749,7 +749,7 @@ moduleCmd modString
   | null modString = return ()
   | otherwise      = do
       case parseModName modString of
-        Just m -> loadCmd =<< liftModuleCmd (M.findModule m)
+        Just m  -> loadHelper (M.loadModuleByName m)
         Nothing -> rPutStrLn "Invalid module name."
 
 loadPrelude :: REPL ()
@@ -758,19 +758,18 @@ loadPrelude  = moduleCmd $ show $ pp M.preludeName
 loadCmd :: FilePath -> REPL ()
 loadCmd path
   | null path = return ()
-  | otherwise = do
-      setLoadedMod LoadedModule
-        { lName = Nothing
-        , lPath = path
-        }
+  | otherwise = loadHelper (M.loadModuleByPath path)
 
-      m <- liftModuleCmd (M.loadModuleByPath path)
-      whenDebug (rPutStrLn (dump m))
-      setLoadedMod LoadedModule
+loadHelper :: M.ModuleCmd (FilePath,T.Module) -> REPL ()
+loadHelper how =
+  do clearLoadedMod
+     (path,m) <- liftModuleCmd how
+     whenDebug (rPutStrLn (dump m))
+     setLoadedMod LoadedModule
         { lName = Just (T.mName m)
         , lPath = path
         }
-      setDynEnv mempty
+     setDynEnv mempty
 
 quitCmd :: REPL ()
 quitCmd  = stop

src/Cryptol/REPL/Monad.hs

@@ -40,7 +40,7 @@ module Cryptol.REPL.Monad (
   , getTypeNames
   , getPropertyNames
   , getModNames
-  , LoadedModule(..), getLoadedMod, setLoadedMod
+  , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod
   , setSearchPath, prependSearchPath
   , getPrompt
   , shouldContinue
@@ -300,6 +300,12 @@ modifyRW_ f = REPL (\ ref -> modifyIORef ref f)
 getPrompt :: REPL String
 getPrompt  = mkPrompt `fmap` getRW
 
+
+clearLoadedMod :: REPL ()
+clearLoadedMod = do modifyRW_ (\rw -> rw { eLoadedMod = upd <$> eLoadedMod rw })
+                    updateREPLTitle
+  where upd x = x { lName = Nothing }
+
 -- | Set the name of the currently focused file, edited by @:e@ and loaded via
 -- @:r@.
 setLoadedMod :: LoadedModule -> REPL ()

tests/issues/issue290.icry.stdout

@@ -1,5 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
 Loading module issue290
 Loading module issue290bar
 Assuming a = 2

tests/modsys/T1.icry.stdout

@@ -1,4 +1,3 @@
 Loading module Cryptol
-Loading module Cryptol
-Loading module A
+Loading module T1::Main
 0x02

tests/modsys/T1/Main.cry

@@ -1,4 +1,4 @@
-module A where
+module T1::Main where
 
 main = 0x02
 

tests/modsys/T2.icry.stdout

@@ -1,5 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
 Loading module T2::A
 Loading module T2::Main
 0x00

tests/modsys/T3.icry.stdout

@@ -1,5 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
 Loading module T3::A
 
-Import of a non-instantiated parameterized module: T3::A
+[error] Import of a non-instantiated parameterized module: T3::A

tests/modsys/T4.icry.stdout

@@ -1,5 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
 Loading module T4::A
 Loading module T4::Main
 main : T

tests/modsys/T5.icry.stdout

@@ -1,5 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
 Loading module T5::A
 Loading module T5::B
 Loading module T5::Main

tests/modsys/T6.icry.stdout

@@ -1,5 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
 Loading module T5::A
 Loading module T5::B
 Loading module T5::Main

tests/modsys/T7.icry.stdout

@@ -1,5 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
 Loading module T7::Main
 
 The current module, T7::Main, is parameterized, and does not support evaluation.

tests/regression/r03.icry.stdout

@@ -1,5 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
 Loading module r03
 (nQueens : Solution 5) [0x3, 0x1, 0x4, 0x2, 0x0] = True
 (nQueensProve : Solution 4) [0x2, 0x0, 0x3, 0x1] = False