Add support for working with in-memory sources.

Currently we only use this for the Prelude, which is baked into Cryptol.
Previously we used to save it in a temporary file, which would show
up in error messages, leading to bad user experience and unreliable
test outputs.

Also improves the shadowing errors.

Fixes #569

cryptol/Main.hs

@@ -17,6 +17,7 @@ import Cryptol.REPL.Command (loadCmd,loadPrelude,CommandExitCode(..))
 import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,
                    io,prependSearchPath,setSearchPath)
 import qualified Cryptol.REPL.Monad as REPL
+import Cryptol.ModuleSystem.Env(ModulePath(..))
 
 import REPL.Haskeline
 import REPL.Logo
@@ -276,6 +277,6 @@ setupREPL opts = do
              REPL.setEditPath l
              REPL.setLoadedMod REPL.LoadedModule
                { REPL.lName = Nothing
-               , REPL.lPath = l
+               , REPL.lPath = InFile l
                }
     _   -> io $ putStrLn "Only one file may be loaded at the command line."

src/Cryptol/ModuleSystem.hs

@@ -57,19 +57,19 @@ getPrimMap :: ModuleCmd PrimMap
 getPrimMap me = runModuleM me Base.getPrimMap
 
 -- | Find the file associated with a module name in the module search path.
-findModule :: P.ModName -> ModuleCmd FilePath
+findModule :: P.ModName -> ModuleCmd ModulePath
 findModule n env = runModuleM env (Base.findModule n)
 
 -- | Load the module contained in the given file.
-loadModuleByPath :: FilePath -> ModuleCmd (FilePath,T.Module)
+loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.Module)
 loadModuleByPath path (evo,env) = runModuleM (evo,resetModuleEnv env) $ do
-  unloadModule ((path ==) . lmFilePath)
+  unloadModule ((InFile path ==) . lmFilePath)
   m <- Base.loadModuleByPath path
   setFocusedModule (T.mName m)
-  return (path,m)
+  return (InFile path,m)
 
 -- | Load the given parsed module.
-loadModuleByName :: P.ModName -> ModuleCmd (FilePath,T.Module)
+loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module)
 loadModuleByName n env = runModuleM env $ do
   unloadModule ((n ==) . lmName)
   (path,m') <- Base.loadModuleFrom (FromModule n)

src/Cryptol/ModuleSystem/Base.hs

@@ -21,7 +21,8 @@ import Cryptol.ModuleSystem.Monad
 import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap)
 import Cryptol.ModuleSystem.Env (lookupModule
                                 , LoadedModule(..)
-                                , meCoreLint, CoreLint(..))
+                                , meCoreLint, CoreLint(..)
+                                , ModulePath(..), modulePathLabel)
 import qualified Cryptol.Eval                 as E
 import qualified Cryptol.Eval.Value           as E
 import           Cryptol.Prims.Eval ()
@@ -45,7 +46,7 @@ import Cryptol.Utils.PP (pretty)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.Logger(logPutStrLn, logPrint)
 
-import Cryptol.Prelude (writePreludeContents)
+import Cryptol.Prelude (preludeContents)
 
 import Cryptol.Transform.MonoValues (rewModule)
 
@@ -105,23 +106,34 @@ noPat a = do
 
 -- Parsing ---------------------------------------------------------------------
 
-parseModule :: FilePath -> ModuleM (Fingerprint, P.Module PName)
+parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName)
 parseModule path = do
 
-  bytesRes <- io (X.try (B.readFile path))
+  bytesRes <- case path of
+                InFile p -> io (X.try (B.readFile p))
+                InMem _ bs -> pure (Right bs)
 
   bytes <- case bytesRes of
     Right bytes -> return bytes
-    Left exn | IOE.isDoesNotExistError exn -> cantFindFile path
-             | otherwise                   -> otherIOError path exn
+    Left exn ->
+      case path of
+        InFile p
+          | IOE.isDoesNotExistError exn -> cantFindFile p
+          | otherwise                   -> otherIOError p exn
+        InMem p _ -> panic "parseModule"
+                       [ "IOError for in-memory contetns???"
+                       , "Label: " ++ show p
+                       , "Exception: " ++ show exn ]
 
   txt <- case decodeUtf8' bytes of
     Right txt -> return txt
     Left e    -> badUtf8 path e
 
   let cfg = P.defaultConfig
-              { P.cfgSource  = path
-              , P.cfgPreProc = P.guessPreProc path
+              { P.cfgSource  = case path of
+                                 InFile p -> p
+                                 InMem l _ -> l
+              , P.cfgPreProc = P.guessPreProc (modulePathLabel path)
               }
 
   case P.parseModule cfg txt of
@@ -137,25 +149,26 @@ loadModuleByPath :: FilePath -> ModuleM T.Module
 loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
   let fileName = takeFileName path
   foundPath <- findFile fileName
-  (fp, pm) <- parseModule foundPath
+  (fp, pm) <- parseModule (InFile foundPath)
   let n = thing (P.mName pm)
 
   -- Check whether this module name has already been loaded from a different file
   env <- getModuleEnv
   -- path' is the resolved, absolute path, used only for checking
   -- whether it's already been loaded
-  path' <- io $ canonicalizePath foundPath
+  path' <- io (canonicalizePath foundPath)
+
   case lookupModule n env of
     -- loadModule will calculate the canonical path again
-    Nothing -> doLoadModule (FromModule n) foundPath fp pm
+    Nothing -> doLoadModule (FromModule n) (InFile foundPath) fp pm
     Just lm
      | path' == loaded -> return (lmModule lm)
      | otherwise       -> duplicateModuleName n path' loaded
-     where loaded = lmCanonicalPath lm
+     where loaded = lmModuleId lm
 
 
 -- | Load a module, unless it was previously loaded.
-loadModuleFrom :: ImportSource -> ModuleM (FilePath,T.Module)
+loadModuleFrom :: ImportSource -> ModuleM (ModulePath,T.Module)
 loadModuleFrom isrc =
   do let n = importedModule isrc
      mb <- getLoadedMaybe n
@@ -171,7 +184,7 @@ loadModuleFrom isrc =
 -- | Load dependencies, typecheck, and add to the eval environment.
 doLoadModule ::
   ImportSource ->
-  FilePath ->
+  ModulePath ->
   Fingerprint ->
   P.Module PName ->
   ModuleM T.Module
@@ -186,8 +199,7 @@ doLoadModule isrc path fp pm0 =
 
      -- extend the eval env, unless a functor.
      unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv tcm)
-     canonicalPath <- io (canonicalizePath path)
-     loadedModule path canonicalPath fp tcm
+     loadedModule path fp tcm
 
      return tcm
   where
@@ -224,8 +236,9 @@ importIfaces is = mconcat `fmap` mapM importIface is
 moduleFile :: ModName -> String -> FilePath
 moduleFile n = addExtension (joinPath (modNameChunks n))
 
+
 -- | Discover a module.
-findModule :: ModName -> ModuleM FilePath
+findModule :: ModName -> ModuleM ModulePath
 findModule n = do
   paths <- getSearchPath
   loop (possibleFiles paths)
@@ -234,13 +247,13 @@ findModule n = do
 
     path:rest -> do
       b <- io (doesFileExist path)
-      if b then return path else loop rest
+      if b then return (InFile path) else loop rest
 
     [] -> handleNotFound
 
   handleNotFound =
     case n of
-      m | m == preludeName -> io writePreludeContents
+      m | m == preludeName -> pure (InMem "Cryptol" preludeContents)
       _ -> moduleNotFound n =<< getSearchPath
 
   -- generate all possible search paths
@@ -359,7 +372,7 @@ getPrimMap  =
                   [ "Unable to find the prelude" ]
 
 -- | Load a module, be it a normal module or a functor instantiation.
-checkModule :: ImportSource -> FilePath -> P.Module PName -> ModuleM T.Module
+checkModule :: ImportSource -> ModulePath -> P.Module PName -> ModuleM T.Module
 checkModule isrc path m =
   case P.mInstance m of
     Nothing -> checkSingleModule T.tcModule isrc path m
@@ -373,7 +386,7 @@ checkModule isrc path m =
 checkSingleModule ::
   Act (P.Module Name) T.Module {- ^ how to check -} ->
   ImportSource                 {- ^ why are we loading this -} ->
-  FilePath                     {- path -} ->
+  ModulePath                   {- path -} ->
   P.Module PName               {- ^ module to check -} ->
   ModuleM T.Module
 checkSingleModule how isrc path m = do
@@ -383,8 +396,14 @@ checkSingleModule how isrc path m = do
   unless (notParamInstModName nm == thing (P.mName m))
          (moduleNameMismatch nm (mName m))
 
-  -- remove includes first
-  e   <- io (removeIncludesModule path m)
+  -- remove includes first; we only do this for actual files.
+  -- it is less clear what should happen for in-memory things, and since
+  -- this is a more-or-less obsolete feature, we are just not doing
+  -- ot for now.
+  e   <- case path of
+           InFile p -> io (removeIncludesModule p m)
+           InMem {} -> pure (Right m)
+
   nim <- case e of
            Right nim  -> return nim
            Left ierrs -> noIncludeErrors ierrs

src/Cryptol/ModuleSystem/Env.hs

@@ -25,8 +25,9 @@ import qualified Cryptol.ModuleSystem.NamingEnv as R
 import Cryptol.Parser.AST
 import qualified Cryptol.TypeCheck as T
 import qualified Cryptol.TypeCheck.AST as T
-import Cryptol.Utils.PP (NameDisp)
+import Cryptol.Utils.PP (PP(..),text,parens,NameDisp)
 
+import Data.ByteString(ByteString)
 import Control.Monad (guard,mplus)
 import qualified Control.Exception as X
 import Data.Function (on)
@@ -222,6 +223,36 @@ dynamicEnv me = (decls,names,R.toNameDisp names)
 
 -- Loaded Modules --------------------------------------------------------------
 
+-- | The location of a module
+data ModulePath = InFile FilePath
+                | InMem String ByteString -- ^ Label, content
+    deriving (Show, Generic, NFData)
+
+-- | In-memory things are compared by label.
+instance Eq ModulePath where
+  p1 == p2 =
+    case (p1,p2) of
+      (InFile x, InFile y) -> x == y
+      (InMem a _, InMem b _) -> a == b
+      _ -> False
+
+instance PP ModulePath where
+  ppPrec _ e =
+    case e of
+      InFile p  -> text p
+      InMem l _ -> parens (text l)
+
+
+
+-- | The name of the content---either the file path, or the provided label.
+modulePathLabel :: ModulePath -> String
+modulePathLabel p =
+  case p of
+    InFile path -> path
+    InMem lab _ -> lab
+
+
+
 data LoadedModules = LoadedModules
   { lmLoadedModules      :: [LoadedModule]
     -- ^ Invariants:
@@ -250,10 +281,12 @@ instance Monoid LoadedModules where
 
 data LoadedModule = LoadedModule
   { lmName              :: ModName
-  , lmFilePath          :: FilePath
+  , lmFilePath          :: ModulePath
     -- ^ The file path used to load this module (may not be canonical)
-  , lmCanonicalPath     :: FilePath
-    -- ^ The canonical version of the path of this module
+  , 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
   , lmModule            :: T.Module
   , lmFingerprint       :: Fingerprint
@@ -277,8 +310,8 @@ lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules
 -- | Add a freshly loaded module.  If it was previously loaded, then
 -- the new version is ignored.
 addLoadedModule ::
-  FilePath -> FilePath -> Fingerprint -> T.Module -> LoadedModules -> LoadedModules
-addLoadedModule path canonicalPath fp tm lm
+  ModulePath -> String -> Fingerprint -> T.Module -> LoadedModules -> LoadedModules
+addLoadedModule path ident fp tm lm
   | isLoaded (T.mName tm) lm  = lm
   | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :
                                                 lmLoadedParamModules lm }
@@ -288,7 +321,7 @@ addLoadedModule path canonicalPath fp tm lm
   loaded = LoadedModule
     { lmName            = T.mName tm
     , lmFilePath        = path
-    , lmCanonicalPath   = canonicalPath
+    , lmModuleId        = ident
     , lmInterface       = genIface tm
     , lmModule          = tm
     , lmFingerprint     = fp

src/Cryptol/ModuleSystem/Monad.hs

@@ -40,13 +40,15 @@ import Data.Function (on)
 import Data.Maybe (isJust)
 import Data.Text.Encoding.Error (UnicodeException)
 import MonadLib
+import System.Directory (canonicalizePath)
 
 import GHC.Generics (Generic)
 import Control.DeepSeq
 
 import Prelude ()
 import Prelude.Compat
 
+
 -- Errors ----------------------------------------------------------------------
 
 data ImportSource
@@ -78,11 +80,11 @@ data ModuleError
     -- ^ Unable to find the module given, tried looking in these paths
   | CantFindFile FilePath
     -- ^ Unable to open a file
-  | BadUtf8 FilePath UnicodeException
+  | BadUtf8 ModulePath UnicodeException
     -- ^ Bad UTF-8 encoding in while decoding this file
   | OtherIOError FilePath IOException
     -- ^ Some other IO error occurred while reading this file
-  | ModuleParseError FilePath Parser.ParseError
+  | ModuleParseError ModulePath Parser.ParseError
     -- ^ Generated this parse error when parsing the file for module m
   | RecursiveModules [ImportSource]
     -- ^ Recursive module group discovered
@@ -106,7 +108,7 @@ data ModuleError
     -- ^ Failed to add the module parameters to all definitions in a module.
   | NotAParameterizedModule P.ModName
 
-  | ErrorInFile FilePath ModuleError
+  | ErrorInFile ModulePath ModuleError
     -- ^ This is just a tag on the error, indicating the file containing it.
     -- It is convenient when we had to look for the module, and we'd like
     -- to communicate the location of pthe problematic module to the handler.
@@ -153,7 +155,7 @@ instance PP ModuleError where
 
     BadUtf8 path _ue ->
       text "[error]" <+>
-      text "bad utf-8 encoding:" <+> text path
+      text "bad utf-8 encoding:" <+> pp path
 
     OtherIOError path exn ->
       hang (text "[error]" <+>
@@ -207,13 +209,13 @@ moduleNotFound name paths = ModuleT (raise (ModuleNotFound name paths))
 cantFindFile :: FilePath -> ModuleM a
 cantFindFile path = ModuleT (raise (CantFindFile path))
 
-badUtf8 :: FilePath -> UnicodeException -> ModuleM a
+badUtf8 :: ModulePath -> UnicodeException -> ModuleM a
 badUtf8 path ue = ModuleT (raise (BadUtf8 path ue))
 
 otherIOError :: FilePath -> IOException -> ModuleM a
 otherIOError path exn = ModuleT (raise (OtherIOError path exn))
 
-moduleParseError :: FilePath -> Parser.ParseError -> ModuleM a
+moduleParseError :: ModulePath -> Parser.ParseError -> ModuleM a
 moduleParseError path err =
   ModuleT (raise (ModuleParseError path err))
 
@@ -260,7 +262,7 @@ notAParameterizedModule x = ModuleT (raise (NotAParameterizedModule x))
 
 -- | Run the computation, and if it caused and error, tag the error
 -- with the given file.
-errorInFile :: FilePath -> ModuleM a -> ModuleM a
+errorInFile :: ModulePath -> ModuleM a -> ModuleM a
 errorInFile file (ModuleT m) = ModuleT (m `handle` h)
   where h e = raise $ case e of
                         ErrorInFile {} -> e
@@ -456,10 +458,14 @@ unloadModule rm = ModuleT $ do
   env <- get
   set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) }
 
-loadedModule :: FilePath -> FilePath -> Fingerprint -> T.Module -> ModuleM ()
-loadedModule path canonicalPath fp m = ModuleT $ do
+loadedModule :: ModulePath -> Fingerprint -> T.Module -> ModuleM ()
+loadedModule path fp m = ModuleT $ do
   env <- get
-  set $! env { meLoadedModules = addLoadedModule path canonicalPath fp m (meLoadedModules env) }
+  ident <- case path of
+             InFile p  -> unModuleT $ io (canonicalizePath p)
+             InMem l _ -> pure l
+
+  set $! env { meLoadedModules = addLoadedModule path ident fp m (meLoadedModules env) }
 
 modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()
 modifyEvalEnv f = ModuleT $ do