mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 04:44:39 +03:00
refactor dynamic environment into ModuleEnv
This just makes for a more consistent API; the "dynamic" environment as extended by REPL commands is now part of the ModuleEnv. It's actually more general than just for the REPL. We can use it in general to add bindings on top of a loaded module context.
This commit is contained in:
Adam C. Foltzer
parent
b2e83f8e27
commit
1dedf6d693
@ -325,22 +325,22 @@ proveCmd :: String -> REPL ()
|
||||
proveCmd str = do
|
||||
parseExpr <- replParseExpr str
|
||||
(expr, schema) <- replCheckExpr parseExpr
|
||||
eenv <- getExtEnv
|
||||
denv <- getDynEnv
|
||||
-- spexpr <- replSpecExpr expr
|
||||
EnvString proverName <- getUser "prover"
|
||||
EnvBool iteSolver <- getUser "iteSolver"
|
||||
EnvBool verbose <- getUser "debug"
|
||||
liftModuleCmd $ Cryptol.Symbolic.prove (proverName, iteSolver, verbose, str) (M.eeDecls eenv) (expr, schema)
|
||||
liftModuleCmd $ Cryptol.Symbolic.prove (proverName, iteSolver, verbose, str) (M.deDecls denv) (expr, schema)
|
||||
|
||||
satCmd :: String -> REPL ()
|
||||
satCmd str = do
|
||||
parseExpr <- replParseExpr str
|
||||
(expr, schema) <- replCheckExpr parseExpr
|
||||
eenv <- getExtEnv
|
||||
denv <- getDynEnv
|
||||
EnvString proverName <- getUser "prover"
|
||||
EnvBool iteSolver <- getUser "iteSolver"
|
||||
EnvBool verbose <- getUser "debug"
|
||||
liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose, str) (M.eeDecls eenv) (expr, schema)
|
||||
liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose, str) (M.deDecls denv) (expr, schema)
|
||||
|
||||
specializeCmd :: String -> REPL ()
|
||||
specializeCmd str = do
|
||||
@ -421,7 +421,7 @@ loadCmd path
|
||||
{ lName = Just (T.mName m)
|
||||
, lPath = path
|
||||
}
|
||||
setExtEnv mempty
|
||||
setDynEnv mempty
|
||||
|
||||
quitCmd :: REPL ()
|
||||
quitCmd = stop
|
||||
@ -591,21 +591,22 @@ moduleCmdResult (res,ws0) = do
|
||||
Left err -> raise (ModuleSystemError err)
|
||||
|
||||
replCheckExpr :: P.Expr -> REPL (T.Expr,T.Schema)
|
||||
replCheckExpr e = do
|
||||
eenv <- getExtEnv
|
||||
liftModuleCmd $ M.checkExprWith eenv e
|
||||
replCheckExpr e = liftModuleCmd $ M.checkExpr e
|
||||
|
||||
replCheckDecls :: [P.Decl] -> REPL [T.DeclGroup]
|
||||
replCheckDecls ds = do
|
||||
npds <- liftModuleCmd $ M.noPat ds
|
||||
eenv <- getExtEnv
|
||||
denv <- getDynEnv
|
||||
let dnames = M.namingEnv npds
|
||||
ne' <- M.travNamingEnv uniqify dnames
|
||||
let eenv' = eenv { M.eeNames = ne' `M.shadowing` M.eeNames eenv }
|
||||
dgs <- liftModuleCmd $ M.checkDeclsWith eenv' npds
|
||||
-- only update the REPL environment after a successful rename + typecheck
|
||||
setExtEnv eenv'
|
||||
return dgs
|
||||
let denv' = denv { M.deNames = ne' `M.shadowing` M.deNames denv }
|
||||
undo exn = do
|
||||
-- if typechecking fails, we want to revert changes to the
|
||||
-- dynamic environment and reraise
|
||||
setDynEnv denv
|
||||
raise exn
|
||||
setDynEnv denv'
|
||||
catch (liftModuleCmd $ M.checkDecls npds) undo
|
||||
|
||||
replSpecExpr :: T.Expr -> REPL T.Expr
|
||||
replSpecExpr e = liftModuleCmd $ S.specialize e
|
||||
@ -625,8 +626,7 @@ replEvalExpr str =
|
||||
let su = T.listSubst [ (T.tpVar a, t) | (a,t) <- tys ]
|
||||
return (def1, T.apSubst su (T.sType sig))
|
||||
|
||||
eenv <- getExtEnv
|
||||
val <- liftModuleCmd (M.evalExprWith eenv def1)
|
||||
val <- liftModuleCmd (M.evalExpr def1)
|
||||
whenDebug (io (putStrLn (dump def1)))
|
||||
return (val,ty)
|
||||
where
|
||||
@ -637,9 +637,7 @@ replEvalDecls :: String -> REPL ()
|
||||
replEvalDecls str = do
|
||||
decls <- replParseDecls str
|
||||
dgs <- replCheckDecls decls
|
||||
eenv <- getExtEnv
|
||||
eenv' <- liftModuleCmd (M.evalDeclsWith eenv dgs)
|
||||
setExtEnv eenv'
|
||||
liftModuleCmd (M.evalDecls dgs)
|
||||
|
||||
replEdit :: String -> REPL Bool
|
||||
replEdit file = do
|
||||
|
||||
@ -23,7 +23,7 @@ module REPL.Monad (
|
||||
|
||||
-- ** Environment
|
||||
, getModuleEnv, setModuleEnv
|
||||
, getExtEnv, setExtEnv
|
||||
, getDynEnv, setDynEnv
|
||||
, uniqify
|
||||
, getTSyns, getNewtypes, getVars
|
||||
, whenDebug
|
||||
@ -52,6 +52,7 @@ import Cryptol.Prims.Syntax(ECon(..),ppPrefix)
|
||||
import Cryptol.Eval (EvalError)
|
||||
import qualified Cryptol.ModuleSystem as M
|
||||
import qualified Cryptol.ModuleSystem.Base as M
|
||||
import qualified Cryptol.ModuleSystem.Env as M
|
||||
import qualified Cryptol.ModuleSystem.NamingEnv as M
|
||||
import Cryptol.Parser (ParseError,ppError)
|
||||
import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
|
||||
@ -86,8 +87,6 @@ data RW = RW
|
||||
, eContinue :: Bool
|
||||
, eIsBatch :: Bool
|
||||
, eModuleEnv :: M.ModuleEnv
|
||||
, eExtEnv :: M.ExtendedEnv
|
||||
-- ^ The dynamic environment for new bindings, eg @:let@
|
||||
, eNameSupply :: Int
|
||||
, eUserEnv :: UserEnv
|
||||
}
|
||||
@ -101,7 +100,6 @@ defaultRW isBatch = do
|
||||
, eContinue = True
|
||||
, eIsBatch = isBatch
|
||||
, eModuleEnv = env
|
||||
, eExtEnv = mempty
|
||||
, eNameSupply = 0
|
||||
, eUserEnv = mkUserEnv userOptions
|
||||
}
|
||||
@ -260,12 +258,12 @@ keepOne src as = case as of
|
||||
getVars :: REPL (Map.Map P.QName M.IfaceDecl)
|
||||
getVars = do
|
||||
me <- getModuleEnv
|
||||
eenv <- getExtEnv
|
||||
denv <- getDynEnv
|
||||
-- the subtle part here is removing the #Uniq prefix from
|
||||
-- interactively-bound variables, and also excluding any that are
|
||||
-- shadowed and thus can no longer be referenced
|
||||
let decls = M.focusedEnv me
|
||||
edecls = M.ifDecls (M.eeIfaceDecls eenv)
|
||||
edecls = M.ifDecls (M.deIfaceDecls denv)
|
||||
-- is this QName something the user might actually type?
|
||||
isShadowed (qn@(P.QName (Just (P.ModName ['#':_])) name), _) =
|
||||
case Map.lookup localName neExprs of
|
||||
@ -273,7 +271,7 @@ getVars = do
|
||||
Just uniqueNames -> isNamed uniqueNames
|
||||
where localName = P.QName Nothing name
|
||||
isNamed us = any (== qn) (map M.qname us)
|
||||
neExprs = M.neExprs (M.eeNames eenv)
|
||||
neExprs = M.neExprs (M.deNames denv)
|
||||
isShadowed _ = False
|
||||
unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds)
|
||||
edecls' = Map.fromList
|
||||
@ -321,11 +319,13 @@ getModuleEnv = eModuleEnv `fmap` getRW
|
||||
setModuleEnv :: M.ModuleEnv -> REPL ()
|
||||
setModuleEnv me = modifyRW_ (\rw -> rw { eModuleEnv = me })
|
||||
|
||||
getExtEnv :: REPL M.ExtendedEnv
|
||||
getExtEnv = eExtEnv `fmap` getRW
|
||||
getDynEnv :: REPL M.DynamicEnv
|
||||
getDynEnv = (M.meDynEnv . eModuleEnv) `fmap` getRW
|
||||
|
||||
setExtEnv :: M.ExtendedEnv -> REPL ()
|
||||
setExtEnv eenv = modifyRW_ (\rw -> rw { eExtEnv = eenv })
|
||||
setDynEnv :: M.DynamicEnv -> REPL ()
|
||||
setDynEnv denv = do
|
||||
me <- getModuleEnv
|
||||
setModuleEnv (me { M.meDynEnv = denv })
|
||||
|
||||
-- | Given an existing qualified name, prefix it with a
|
||||
-- relatively-unique string. We make it unique by prefixing with a
|
||||
|
||||
@ -9,16 +9,16 @@
|
||||
module Cryptol.ModuleSystem (
|
||||
-- * Module System
|
||||
ModuleEnv(..), initialModuleEnv
|
||||
, ExtendedEnv(..)
|
||||
, DynamicEnv(..)
|
||||
, ModuleError(..), ModuleWarning(..)
|
||||
, ModuleCmd, ModuleRes
|
||||
, findModule
|
||||
, loadModuleByPath
|
||||
, loadModule
|
||||
, checkExprWith
|
||||
, evalExprWith
|
||||
, checkDeclsWith
|
||||
, evalDeclsWith
|
||||
, checkExpr
|
||||
, evalExpr
|
||||
, checkDecls
|
||||
, evalDecls
|
||||
, noPat
|
||||
, focusedEnv
|
||||
|
||||
@ -71,20 +71,20 @@ loadModule m env = runModuleM env $ do
|
||||
-- can extend dynamically outside of the context of a module.
|
||||
|
||||
-- | Check the type of an expression.
|
||||
checkExprWith :: ExtendedEnv -> P.Expr -> ModuleCmd (T.Expr,T.Schema)
|
||||
checkExprWith eenv e env = runModuleM env (interactive (Base.checkExprWith eenv e))
|
||||
checkExpr :: P.Expr -> ModuleCmd (T.Expr,T.Schema)
|
||||
checkExpr e env = runModuleM env (interactive (Base.checkExpr e))
|
||||
|
||||
-- | Evaluate an expression.
|
||||
evalExprWith :: ExtendedEnv -> T.Expr -> ModuleCmd E.Value
|
||||
evalExprWith eenv e env = runModuleM env (interactive (Base.evalExprWith eenv e))
|
||||
evalExpr :: T.Expr -> ModuleCmd E.Value
|
||||
evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
|
||||
|
||||
-- | Typecheck declarations.
|
||||
checkDeclsWith :: ExtendedEnv -> [P.Decl] -> ModuleCmd [T.DeclGroup]
|
||||
checkDeclsWith eenv ds env = runModuleM env (interactive (Base.checkDeclsWith eenv ds))
|
||||
checkDecls :: [P.Decl] -> ModuleCmd [T.DeclGroup]
|
||||
checkDecls ds env = runModuleM env (interactive (Base.checkDecls ds))
|
||||
|
||||
-- | Evaluate declarations and add them to the extended environment.
|
||||
evalDeclsWith :: ExtendedEnv -> [T.DeclGroup] -> ModuleCmd ExtendedEnv
|
||||
evalDeclsWith eenv dgs env = runModuleM env (interactive (Base.evalDeclsWith eenv dgs))
|
||||
evalDecls :: [T.DeclGroup] -> ModuleCmd ()
|
||||
evalDecls dgs env = runModuleM env (interactive (Base.evalDecls dgs))
|
||||
|
||||
noPat :: RemovePatterns a => a -> ModuleCmd a
|
||||
noPat a env = runModuleM env (interactive (Base.noPat a))
|
||||
|
||||
@ -8,7 +8,7 @@
|
||||
|
||||
module Cryptol.ModuleSystem.Base where
|
||||
|
||||
import Cryptol.ModuleSystem.Env (ExtendedEnv(..))
|
||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.ModuleSystem.Monad
|
||||
import qualified Cryptol.Eval as E
|
||||
@ -32,7 +32,7 @@ import Data.Foldable (foldMap)
|
||||
import Data.Function (on)
|
||||
import Data.List (nubBy)
|
||||
import Data.Maybe (mapMaybe,fromMaybe)
|
||||
import Data.Monoid ((<>), mconcat)
|
||||
import Data.Monoid ((<>))
|
||||
import System.Directory (doesFileExist)
|
||||
import System.FilePath (addExtension,joinPath,(</>))
|
||||
import qualified Data.Map as Map
|
||||
@ -67,14 +67,8 @@ renameModule m = do
|
||||
renameExpr :: P.Expr -> ModuleM P.Expr
|
||||
renameExpr e = do
|
||||
env <- getFocusedEnv
|
||||
rename (R.namingEnv env) e
|
||||
|
||||
-- | Rename an expression in the context of the focused module and an
|
||||
-- extended environment.
|
||||
renameExprWith :: ExtendedEnv -> P.Expr -> ModuleM P.Expr
|
||||
renameExprWith eenv e = do
|
||||
env <- getFocusedEnv
|
||||
rename (eeNames eenv `R.shadowing` R.namingEnv env) e
|
||||
denv <- getDynEnv
|
||||
rename (deNames denv `R.shadowing` R.namingEnv env) e
|
||||
|
||||
-- NoPat -----------------------------------------------------------------------
|
||||
|
||||
@ -228,36 +222,20 @@ loadDeps m
|
||||
checkExpr :: P.Expr -> ModuleM (T.Expr,T.Schema)
|
||||
checkExpr e = do
|
||||
npe <- noPat e
|
||||
denv <- getDynEnv
|
||||
re <- renameExpr npe
|
||||
typecheck T.tcExpr re =<< getQualifiedEnv
|
||||
|
||||
-- | Typecheck a single expression in an extended environment.
|
||||
checkExprWith :: ExtendedEnv -> P.Expr -> ModuleM (T.Expr,T.Schema)
|
||||
checkExprWith eenv e = do
|
||||
npe <- noPat e
|
||||
re <- renameExprWith eenv npe
|
||||
env <- getQualifiedEnv
|
||||
let env' = env <> eeIfaceDecls eenv
|
||||
let env' = env <> deIfaceDecls denv
|
||||
typecheck T.tcExpr re env'
|
||||
|
||||
eeIfaceDecls :: ExtendedEnv -> IfaceDecls
|
||||
eeIfaceDecls EEnv { eeDecls = dgs } =
|
||||
mconcat [ IfaceDecls
|
||||
{ ifTySyns = Map.empty
|
||||
, ifNewtypes = Map.empty
|
||||
, ifDecls = Map.singleton (ifDeclName ifd) [ifd]
|
||||
}
|
||||
| decl <- concatMap T.groupDecls dgs
|
||||
, let ifd = mkIfaceDecl decl
|
||||
]
|
||||
|
||||
-- | Typecheck a group of declarations in an extended environment.
|
||||
checkDeclsWith :: ExtendedEnv -> [P.Decl] -> ModuleM [T.DeclGroup]
|
||||
checkDeclsWith eenv ds = do
|
||||
-- | Typecheck a group of declarations.
|
||||
checkDecls :: [P.Decl] -> ModuleM [T.DeclGroup]
|
||||
checkDecls ds = do
|
||||
-- nopat must already be run
|
||||
rds <- rename (eeNames eenv) ds
|
||||
denv <- getDynEnv
|
||||
rds <- rename (deNames denv) ds
|
||||
env <- getQualifiedEnv
|
||||
let env' = env <> eeIfaceDecls eenv
|
||||
let env' = env <> deIfaceDecls denv
|
||||
typecheck T.tcDecls rds env'
|
||||
|
||||
-- | Typecheck a module.
|
||||
@ -340,18 +318,15 @@ genInferInput r env = do
|
||||
evalExpr :: T.Expr -> ModuleM E.Value
|
||||
evalExpr e = do
|
||||
env <- getEvalEnv
|
||||
return (E.evalExpr env e)
|
||||
denv <- getDynEnv
|
||||
return (E.evalExpr (env <> deEnv denv) e)
|
||||
|
||||
evalExprWith :: ExtendedEnv -> T.Expr -> ModuleM E.Value
|
||||
evalExprWith eenv e = do
|
||||
evalDecls :: [T.DeclGroup] -> ModuleM ()
|
||||
evalDecls dgs = do
|
||||
env <- getEvalEnv
|
||||
return (E.evalExpr (env <> eeEnv eenv) e)
|
||||
|
||||
-- | Evaluate typechecked declarations in an extended environment. The
|
||||
-- result of this is a new environment whose 'EvalEnv' is extended
|
||||
-- with the new declarations and their values.
|
||||
evalDeclsWith :: ExtendedEnv -> [T.DeclGroup] -> ModuleM ExtendedEnv
|
||||
evalDeclsWith eenv dgs = do
|
||||
env <- getEvalEnv
|
||||
let env' = env <> eeEnv eenv
|
||||
return $ eenv { eeDecls = eeDecls eenv ++ dgs, eeEnv = E.evalDecls dgs env' }
|
||||
denv <- getDynEnv
|
||||
let env' = env <> deEnv denv
|
||||
denv' = denv { deDecls = deDecls denv ++ dgs
|
||||
, deEnv = E.evalDecls dgs env'
|
||||
}
|
||||
setDynEnv denv'
|
||||
|
||||
@ -22,6 +22,7 @@ import qualified Cryptol.TypeCheck.AST as T
|
||||
import Control.Monad (guard)
|
||||
import Data.Foldable (fold)
|
||||
import Data.Function (on)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Monoid ((<>), Monoid(..))
|
||||
import System.Environment.Executable(splitExecutablePath)
|
||||
import System.FilePath ((</>), normalise, joinPath, splitPath)
|
||||
@ -36,6 +37,7 @@ data ModuleEnv = ModuleEnv
|
||||
, meEvalEnv :: EvalEnv
|
||||
, meFocusedModule :: Maybe ModName
|
||||
, meSearchPath :: [FilePath]
|
||||
, meDynEnv :: DynamicEnv
|
||||
}
|
||||
|
||||
initialModuleEnv :: IO ModuleEnv
|
||||
@ -49,6 +51,7 @@ initialModuleEnv = do
|
||||
, meEvalEnv = mempty
|
||||
, meFocusedModule = Nothing
|
||||
, meSearchPath = [dataDir </> "lib", instDir </> "lib", "."]
|
||||
, meDynEnv = mempty
|
||||
}
|
||||
|
||||
-- | Try to focus a loaded module in the module environment.
|
||||
@ -128,27 +131,43 @@ addLoadedModule tm lm
|
||||
, lmModule = tm
|
||||
}
|
||||
|
||||
-- Extended Environments -------------------------------------------------------
|
||||
-- Dynamic Environments --------------------------------------------------------
|
||||
|
||||
-- | Extra information we need to carry around to dynamically extend
|
||||
-- an environment outside the context of a single module. Particularly
|
||||
-- useful when dealing with interactive declarations as in @:let@ or
|
||||
-- @it@.
|
||||
|
||||
data ExtendedEnv = EEnv
|
||||
{ eeNames :: R.NamingEnv
|
||||
, eeDecls :: [T.DeclGroup]
|
||||
, eeEnv :: EvalEnv
|
||||
data DynamicEnv = DEnv
|
||||
{ deNames :: R.NamingEnv
|
||||
, deDecls :: [T.DeclGroup]
|
||||
, deEnv :: EvalEnv
|
||||
}
|
||||
|
||||
instance Monoid ExtendedEnv where
|
||||
mempty = EEnv
|
||||
{ eeNames = mempty
|
||||
, eeDecls = mempty
|
||||
, eeEnv = mempty
|
||||
instance Monoid DynamicEnv where
|
||||
mempty = DEnv
|
||||
{ deNames = mempty
|
||||
, deDecls = mempty
|
||||
, deEnv = mempty
|
||||
}
|
||||
mappend ee1 ee2 = EEnv
|
||||
{ eeNames = eeNames ee1 <> eeNames ee2
|
||||
, eeDecls = eeDecls ee1 <> eeDecls ee2
|
||||
, eeEnv = eeEnv ee1 <> eeEnv ee2
|
||||
mappend de1 de2 = DEnv
|
||||
{ deNames = deNames de1 <> deNames de2
|
||||
, deDecls = deDecls de1 <> deDecls de2
|
||||
, deEnv = deEnv de1 <> deEnv de2
|
||||
}
|
||||
|
||||
-- | Build 'IfaceDecls' that correspond to all of the bindings in the
|
||||
-- dynamic environment.
|
||||
--
|
||||
-- XXX: if we ever add type synonyms or newtypes at the REPL, revisit
|
||||
-- this.
|
||||
deIfaceDecls :: DynamicEnv -> IfaceDecls
|
||||
deIfaceDecls DEnv { deDecls = dgs } =
|
||||
mconcat [ IfaceDecls
|
||||
{ ifTySyns = Map.empty
|
||||
, ifNewtypes = Map.empty
|
||||
, ifDecls = Map.singleton (ifDeclName ifd) [ifd]
|
||||
}
|
||||
| decl <- concatMap T.groupDecls dgs
|
||||
, let ifd = mkIfaceDecl decl
|
||||
]
|
||||
|
||||
@ -328,3 +328,11 @@ getFocusedEnv = ModuleT (focusedEnv `fmap` get)
|
||||
|
||||
getQualifiedEnv :: ModuleM IfaceDecls
|
||||
getQualifiedEnv = ModuleT (qualifiedEnv `fmap` get)
|
||||
|
||||
getDynEnv :: ModuleM DynamicEnv
|
||||
getDynEnv = ModuleT (meDynEnv `fmap` get)
|
||||
|
||||
setDynEnv :: DynamicEnv -> ModuleM ()
|
||||
setDynEnv denv = ModuleT $ do
|
||||
me <- get
|
||||
set $! me { meDynEnv = denv }
|
||||
|
||||
Loading…
Reference in New Issue
Block a user