diff --git a/cryptol/Main.hs b/cryptol/Main.hs index 56280271b..e375901c0 100644 --- a/cryptol/Main.hs +++ b/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." diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index 4b699bb85..ca10fa326 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/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) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 028b0512e..5f5919272 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/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 diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index 25182042e..49e2b6d0e 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/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 diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index fa886ecee..3c92a8c86 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -40,6 +40,7 @@ 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 @@ -47,6 +48,7 @@ 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 diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 32259d0ba..2f2e775c3 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -163,9 +163,10 @@ data RenamerWarning instance PP RenamerWarning where ppPrec _ (SymbolShadowed new originals disp) = fixNameDisp disp $ hang (text "[warning] at" <+> loc) - 4 $ fsep [ text "This binding for" <+> sym - , (text "shadows the existing binding" <.> plural) <+> text "from" ] - $$ vcat (map ppLocName originals) + 4 $ fsep [ text "This binding for" <+> backticks sym + , text "shadows the existing binding" <.> plural <+> + text "at" ] + $$ vcat (map (pp . nameLoc) originals) where plural | length originals > 1 = char 's' diff --git a/src/Cryptol/Prelude.hs b/src/Cryptol/Prelude.hs index 79b4e74cc..773fe9615 100644 --- a/src/Cryptol/Prelude.hs +++ b/src/Cryptol/Prelude.hs @@ -13,28 +13,15 @@ {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE OverloadedStrings #-} -module Cryptol.Prelude ( - writePreludeContents, - cryptolTcContents - ) where +module Cryptol.Prelude (preludeContents,cryptolTcContents) where -import System.Directory (getTemporaryDirectory) -import System.IO (hClose, hPutStr, openTempFile) +import Data.ByteString(ByteString) +import qualified Data.ByteString.Char8 as B import Text.Heredoc (there) -preludeContents :: String -preludeContents = [there|lib/Cryptol.cry|] - --- | Write the contents of the Prelude to a temporary file so that --- Cryptol can load the module. -writePreludeContents :: IO FilePath -writePreludeContents = do - tmpdir <- getTemporaryDirectory - (path, h) <- openTempFile tmpdir "Cryptol.cry" - hPutStr h preludeContents - hClose h - return path +preludeContents :: ByteString +preludeContents = B.pack [there|lib/Cryptol.cry|] cryptolTcContents :: String cryptolTcContents = [there|lib/CryptolTC.z3|] diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 811b314df..22f269911 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -81,9 +81,12 @@ import qualified Cryptol.Symbolic as Symbolic import qualified Control.Exception as X import Control.Monad hiding (mapM, mapM) +import Control.Monad.IO.Class(liftIO) +import Data.ByteString (ByteString) import qualified Data.ByteString as BS +import qualified Data.ByteString.Char8 as BS8 import Data.Bits ((.&.)) -import Data.Char (isSpace,isPunctuation,isSymbol) +import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii) import Data.Function (on) import Data.List (intercalate, nub, sortBy, partition, isPrefixOf,intersperse) import Data.Maybe (fromMaybe,mapMaybe,isNothing) @@ -92,10 +95,12 @@ import System.Exit (ExitCode(ExitSuccess)) import System.Process (shell,createProcess,waitForProcess) import qualified System.Process as Process(runCommand) import System.FilePath((), isPathSeparator) -import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist) +import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist + ,getTemporaryDirectory,setPermissions,removeFile + ,emptyPermissions,setOwnerReadable) import qualified Data.Map as Map import qualified Data.Set as Set -import System.IO(hFlush,stdout) +import System.IO(hFlush,stdout,openTempFile,hClose) import System.Random.TF(newTFGen) import Numeric (showFFloat) import qualified Data.Text as T @@ -777,7 +782,9 @@ reloadCmd = do Just lm -> case lName lm of Just m | M.isParamInstModName m -> loadHelper (M.loadModuleByName m) - _ -> loadCmd (lPath lm) + _ -> case lPath lm of + M.InFile f -> loadCmd f + _ -> return () Nothing -> return () @@ -787,17 +794,41 @@ editCmd path = mbL <- getLoadedMod if not (null path) then do when (isNothing mbL) - $ setLoadedMod LoadedModule { lName = Nothing, lPath = path } + $ setLoadedMod LoadedModule { lName = Nothing + , lPath = M.InFile path } doEdit path - else case msum [ mbE, lPath <$> mbL ] of + else case msum [ M.InFile <$> mbE, lPath <$> mbL ] of Nothing -> rPutStrLn "No filed to edit." - Just p -> doEdit p + Just p -> + case p of + M.InFile f -> doEdit f + M.InMem l bs -> withROTempFile l bs replEdit >> pure () where doEdit p = do setEditPath p _ <- replEdit p reloadCmd +withROTempFile :: String -> ByteString -> (FilePath -> REPL a) -> REPL a +withROTempFile name cnt k = + do (path,h) <- mkTmp + do mkFile path h + k path + `finally` liftIO (do hClose h + removeFile path) + where + mkTmp = + liftIO $ + do tmp <- getTemporaryDirectory + let esc c = if isAscii c && isAlphaNum c then c else '_' + openTempFile tmp (map esc name ++ ".cry") + + mkFile path h = + liftIO $ + do BS8.hPutStrLn h cnt + setPermissions path (setOwnerReadable True emptyPermissions) + + moduleCmd :: String -> REPL () moduleCmd modString @@ -817,11 +848,11 @@ loadCmd path -- when `:load`, the edit and focused paths become the parameter | otherwise = do setEditPath path setLoadedMod LoadedModule { lName = Nothing - , lPath = path + , lPath = M.InFile path } loadHelper (M.loadModuleByPath path) -loadHelper :: M.ModuleCmd (FilePath,T.Module) -> REPL () +loadHelper :: M.ModuleCmd (M.ModulePath,T.Module) -> REPL () loadHelper how = do clearLoadedMod (path,m) <- liftModuleCmd how @@ -831,7 +862,9 @@ loadHelper how = , lPath = path } -- after a successful load, the current module becomes the edit target - setEditPath path + case path of + M.InFile f -> setEditPath f + M.InMem {} -> clearEditPath setDynEnv mempty quitCmd :: REPL () @@ -1239,7 +1272,7 @@ moduleCmdResult (res,ws0) = do Right (a,me') -> setModuleEnv me' >> return a Left err -> do e <- case err of - M.ErrorInFile file e -> + M.ErrorInFile (M.InFile file) e -> -- on error, the file with the error becomes the edit -- target. Note, however, that the focused module is not -- changed. diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 8d43862fe..e4f4dc14c 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -22,6 +22,7 @@ module Cryptol.REPL.Monad ( , raise , stop , catch + , finally , rPutStrLn , rPutStr , rPrint @@ -42,7 +43,7 @@ module Cryptol.REPL.Monad ( , getPropertyNames , getModNames , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod - , setEditPath, getEditPath + , setEditPath, getEditPath, clearEditPath , setSearchPath, prependSearchPath , getPrompt , shouldContinue @@ -122,8 +123,8 @@ import Prelude.Compat -- | This indicates what the user would like to work on. data LoadedModule = LoadedModule - { lName :: Maybe P.ModName -- ^ Working on this module. - , lPath :: FilePath -- ^ Working on this file. + { lName :: Maybe P.ModName -- ^ Working on this module. + , lPath :: M.ModulePath -- ^ Working on this file. } -- | REPL RW Environment. @@ -185,7 +186,7 @@ mkPrompt rw modLn = case lName =<< eLoadedMod rw of - Nothing -> "cryptol" + Nothing -> show (pp I.preludeName) Just m | M.isLoadedParamMod m (M.meLoadedModules (eModuleEnv rw)) -> modName ++ "(parameterized)" @@ -196,15 +197,15 @@ mkPrompt rw case eLoadedMod rw of Nothing -> modLn Just m -> - case lName m of - Nothing -> ":r to reload " ++ lPath m ++ "\n" ++ modLn - Just _ -> modLn + case (lName m, lPath m) of + (Nothing, M.InFile f) -> ":r to reload " ++ show f ++ "\n" ++ modLn + _ -> modLn withEdit = case eEditFile rw of Nothing -> withFocus Just e - | Just f <- lPath <$> eLoadedMod rw + | Just (M.InFile f) <- lPath <$> eLoadedMod rw , f == e -> withFocus | otherwise -> ":e to edit " ++ e ++ "\n" ++ withFocus @@ -308,6 +309,9 @@ raise exn = io (X.throwIO exn) catch :: REPL a -> (REPLException -> REPL a) -> REPL a catch m k = REPL (\ ref -> rethrowEvalError (unREPL m ref) `X.catch` \ e -> unREPL (k e) ref) +finally :: REPL a -> REPL b -> REPL a +finally m1 m2 = REPL (\ref -> unREPL m1 ref `X.finally` unREPL m2 ref) + rethrowEvalError :: IO a -> IO a rethrowEvalError m = run `X.catch` rethrow @@ -365,6 +369,9 @@ setEditPath p = modifyRW_ $ \rw -> rw { eEditFile = Just p } getEditPath :: REPL (Maybe FilePath) getEditPath = eEditFile <$> getRW +clearEditPath :: REPL () +clearEditPath = modifyRW_ $ \rw -> rw { eEditFile = Nothing } + setSearchPath :: [FilePath] -> REPL () setSearchPath path = do me <- getModuleEnv diff --git a/tests/issues/allexamples.icry.stdout b/tests/issues/allexamples.icry.stdout index 3c2d00cc0..112216c2a 100644 --- a/tests/issues/allexamples.icry.stdout +++ b/tests/issues/allexamples.icry.stdout @@ -10,11 +10,11 @@ Loading module ChaCha20 [warning] at ./ChaChaPolyCryptolIETF.md:2117:20--2117:21 Unused name: b [warning] at ./ChaChaPolyCryptolIETF.md:1984:5--1984:15 - This binding for cypherText shadows the existing binding from - (at ./ChaChaPolyCryptolIETF.md:1982:24--1982:34, cypherText) + This binding for `cypherText` shadows the existing binding at + ./ChaChaPolyCryptolIETF.md:1982:24--1982:34 [warning] at ./ChaChaPolyCryptolIETF.md:2062:20--2062:27 - This binding for AeadAAD shadows the existing binding from - (at ./ChaChaPolyCryptolIETF.md:1149:1--1149:8, AeadAAD) + This binding for `AeadAAD` shadows the existing binding at + ./ChaChaPolyCryptolIETF.md:1149:1--1149:8 Loading module Cryptol Loading module Cipher Loading module Cryptol diff --git a/tests/mono-binds/test05.icry.stdout b/tests/mono-binds/test05.icry.stdout index dbc6920fb..ac7a8e3f6 100644 --- a/tests/mono-binds/test05.icry.stdout +++ b/tests/mono-binds/test05.icry.stdout @@ -2,11 +2,11 @@ Loading module Cryptol Loading module Cryptol Loading module test05 [warning] at ./test05.cry:9:3--9:6 - This binding for foo shadows the existing binding from - (at ./test05.cry:4:1--4:4, foo) + This binding for `foo` shadows the existing binding at + ./test05.cry:4:1--4:4 [warning] at ./test05.cry:13:5--13:8 - This binding for foo shadows the existing binding from - (at ./test05.cry:9:3--9:6, foo) + This binding for `foo` shadows the existing binding at + ./test05.cry:9:3--9:6 module test05 import Cryptol /* Not recursive */ @@ -43,11 +43,11 @@ test05::test = \{n, a, b} (Zero b, Literal 10 a) (a : [n]b) -> Loading module Cryptol Loading module test05 [warning] at ./test05.cry:9:3--9:6 - This binding for foo shadows the existing binding from - (at ./test05.cry:4:1--4:4, foo) + This binding for `foo` shadows the existing binding at + ./test05.cry:4:1--4:4 [warning] at ./test05.cry:13:5--13:8 - This binding for foo shadows the existing binding from - (at ./test05.cry:9:3--9:6, foo) + This binding for `foo` shadows the existing binding at + ./test05.cry:9:3--9:6 [warning] at ./test05.cry:14:11--14:21: Defaulting type argument 'front' of '(#)' to 0 module test05 diff --git a/tests/regression/check09.icry.stdout b/tests/regression/check09.icry.stdout index 5ac6c91d1..9b676caf1 100644 --- a/tests/regression/check09.icry.stdout +++ b/tests/regression/check09.icry.stdout @@ -2,17 +2,17 @@ Loading module Cryptol Loading module Cryptol Loading module Main [warning] at ./check09.cry:22:5--22:10 - This binding for initL shadows the existing binding from - (at ./check09.cry:4:1--4:6, initL) + This binding for `initL` shadows the existing binding at + ./check09.cry:4:1--4:6 [warning] at ./check09.cry:21:5--21:10 - This binding for initS shadows the existing binding from - (at ./check09.cry:3:1--3:6, initS) + This binding for `initS` shadows the existing binding at + ./check09.cry:3:1--3:6 [warning] at ./check09.cry:27:5--27:7 - This binding for ls shadows the existing binding from - (at ./check09.cry:8:1--8:3, ls) + This binding for `ls` shadows the existing binding at + ./check09.cry:8:1--8:3 [warning] at ./check09.cry:23:5--23:7 - This binding for ss shadows the existing binding from - (at ./check09.cry:5:1--5:3, ss) + This binding for `ss` shadows the existing binding at + ./check09.cry:5:1--5:3 [warning] at ./check09.cry:17:12--17:28: Defaulting type argument 'ix' of '(@@)' to 3 [warning] at ./check09.cry:13:12--13:80: diff --git a/tests/regression/check25.icry.stdout b/tests/regression/check25.icry.stdout index 88033eead..49fd4f6b6 100644 --- a/tests/regression/check25.icry.stdout +++ b/tests/regression/check25.icry.stdout @@ -2,8 +2,8 @@ Loading module Cryptol Loading module Cryptol Loading module check25 [warning] at ./check25.cry:6:9--6:11 - This binding for tz shadows the existing binding from - (at ./check25.cry:3:1--3:3, tz) + This binding for `tz` shadows the existing binding at + ./check25.cry:3:1--3:3 [warning] at ./check25.cry:8:11--8:19: Defaulting 1st type argument of 'check25::tx' to [4] [warning] at ./check25.cry:5:6--6:16: diff --git a/tests/regression/check30.icry.stdout b/tests/regression/check30.icry.stdout index 18756f967..c7eaa70ff 100644 --- a/tests/regression/check30.icry.stdout +++ b/tests/regression/check30.icry.stdout @@ -2,7 +2,7 @@ Loading module Cryptol Loading module Cryptol Loading module Main [warning] at ./check30.cry:2:13--2:14 - This binding for x shadows the existing binding from - (at ./check30.cry:1:1--1:2, x) + This binding for `x` shadows the existing binding at + ./check30.cry:1:1--1:2 Loading module Cryptol Loading module Main