From 1dedf6d693252b7380c10382895b31af050d4620 Mon Sep 17 00:00:00 2001 From: "Adam C. Foltzer" Date: Mon, 18 Aug 2014 13:28:21 -0700 Subject: [PATCH] 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. --- cryptol/REPL/Command.hs | 36 ++++++++-------- cryptol/REPL/Monad.hs | 22 +++++----- src/Cryptol/ModuleSystem.hs | 26 ++++++------ src/Cryptol/ModuleSystem/Base.hs | 69 ++++++++++--------------------- src/Cryptol/ModuleSystem/Env.hs | 47 ++++++++++++++------- src/Cryptol/ModuleSystem/Monad.hs | 8 ++++ 6 files changed, 104 insertions(+), 104 deletions(-) diff --git a/cryptol/REPL/Command.hs b/cryptol/REPL/Command.hs index 4e5de69f..e5fa5600 100644 --- a/cryptol/REPL/Command.hs +++ b/cryptol/REPL/Command.hs @@ -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 diff --git a/cryptol/REPL/Monad.hs b/cryptol/REPL/Monad.hs index e5d24d01..682cab3e 100644 --- a/cryptol/REPL/Monad.hs +++ b/cryptol/REPL/Monad.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index a687e280..2c99f532 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -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)) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index fb436f9f..e8090298 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -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' diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index 3c2e15f8..fe22290e 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -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 + ] diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index 07ad3acb..592ff0c6 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -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 }