mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-19 18:08:37 +03:00
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
This commit is contained in:
parent
cc5c10b4c4
commit
8fe9f5efa9
@ -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."
|
||||
|
@ -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)
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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'
|
||||
|
@ -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|]
|
||||
|
@ -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.
|
||||
|
@ -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
|
||||
@ -123,7 +124,7 @@ 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.
|
||||
, 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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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:
|
||||
|
@ -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:
|
||||
|
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user