diff --git a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs index b98038199..2cdbacacb 100644 --- a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs +++ b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs @@ -44,7 +44,7 @@ evalExpression' e = let su = listParamSubst tys let theType = apSubst su (sType schema) tenv <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv - ntEnv <- E.NewtypeEnv . loadedNewtypes <$> getModuleEnv + ntEnv <- loadedNewtypes <$> getModuleEnv let tval = E.evalValType ntEnv tenv theType res <- runModuleCmd (evalExpr checked) val <- observe $ readBack tval res diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index d1d82f2c5..1c1c738a3 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -27,6 +27,7 @@ module Cryptol.Eval ( , emptyEnv , evalExpr , evalDecls + , evalNewtypeDecls , evalSel , evalSetSel , EvalError(..) diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index 941b62a84..eb57975d0 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -40,7 +40,7 @@ > import qualified Cryptol.Backend.FloatHelpers as FP > import Cryptol.Backend.Monad (EvalError(..)) > import Cryptol.Eval.Type -> (TValue(..), isTBit, evalValType, evalNumType, NewtypeEnv(..), TypeEnv, bindTypeVar) +> (TValue(..), isTBit, evalValType, evalNumType, NewtypeEnv, TypeEnv, bindTypeVar) > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2) > import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim) > import Cryptol.Utils.Panic (panic) @@ -1710,7 +1710,7 @@ running the reference evaluator on an expression. > evaluate expr minp = return (Right (val, modEnv), []) > where > modEnv = M.minpModuleEnv minp -> ntEnv = NewtypeEnv (M.loadedNewtypes modEnv) +> ntEnv = M.loadedNewtypes modEnv > extDgs = concatMap mDecls (M.loadedModules modEnv) > env = foldl (evalDeclGroup ntEnv) mempty extDgs > val = evalExpr ntEnv env expr diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs index 766a9d5d3..7da9c0430 100644 --- a/src/Cryptol/Eval/Type.hs +++ b/src/Cryptol/Eval/Type.hs @@ -107,8 +107,7 @@ instance Semigroup TypeEnv where l <> r = TypeEnv { envTypeMap = IntMap.union (envTypeMap l) (envTypeMap r) } -newtype NewtypeEnv = - NewtypeEnv { newtypeEnv :: Map.Map Name Newtype } +type NewtypeEnv = Map.Map Name Newtype lookupTypeVar :: TVar -> TypeEnv -> Maybe (Either Nat' TValue) lookupTypeVar tv env = IntMap.lookup (tvUnique tv) (envTypeMap env) @@ -143,7 +142,7 @@ evalType ntEnv env ty = (TCNum n, []) -> Left $ Nat n (TCInf, []) -> Left $ Inf (TCNewtype u@(UserTC nm _),vs) -> - case Map.lookup nm (newtypeEnv ntEnv) of + case Map.lookup nm ntEnv of Just nt -> let vs' = map (evalType ntEnv env) vs in Right $ TVNewtype u vs' $ evalNewtypeBody ntEnv env nt vs' diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index ea2c9e498..e2ada6508 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -26,7 +26,6 @@ import Cryptol.ModuleSystem.Env (lookupModule , ModContext(..) , ModulePath(..), modulePathLabel) import qualified Cryptol.Eval as E -import qualified Cryptol.Eval.Type as E import qualified Cryptol.Eval.Concrete as Concrete import Cryptol.Eval.Concrete (Concrete(..)) import qualified Cryptol.ModuleSystem.NamingEnv as R @@ -208,7 +207,7 @@ doLoadModule quiet isrc path fp pm0 = callStacks <- getCallStacks let ?callStacks = callStacks nts <- getNewtypes - let ?ntEnv = E.NewtypeEnv nts + let ?ntEnv = nts unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm) loadedModule path fp tcm @@ -574,7 +573,7 @@ evalExpr e = do callStacks <- getCallStacks let ?callStacks = callStacks nts <- getNewtypes - let ?ntEnv = E.NewtypeEnv nts + let ?ntEnv = nts io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e) @@ -589,7 +588,7 @@ evalDecls dgs = do callStacks <- getCallStacks let ?callStacks = callStacks nts <- getNewtypes - let ?ntEnv = E.NewtypeEnv nts + let ?ntEnv = nts deEnv' <- io $ E.runEval mempty (E.evalDecls Concrete dgs env') let denv' = denv { deDecls = deDecls denv ++ dgs diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index bd6becceb..04714f284 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -364,7 +364,7 @@ dumpTestsCmd outFile str pos fnm = testNum <- getKnownUser "tests" :: REPL Int g <- io newTFGen tenv <- E.envTypes . M.deEnv <$> getDynEnv - ntEnv <- E.NewtypeEnv . M.loadedNewtypes <$> getModuleEnv + ntEnv <- M.loadedNewtypes <$> getModuleEnv let tyv = E.evalValType ntEnv tenv ty gens <- case TestR.dumpableType tyv of @@ -428,7 +428,7 @@ qcExpr :: qcExpr qcMode exprDoc texpr schema = do (val,ty) <- replEvalCheckedExpr texpr schema testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests" - ntEnv <- E.NewtypeEnv . M.loadedNewtypes <$> getModuleEnv + ntEnv <- M.loadedNewtypes <$> getModuleEnv tenv <- E.envTypes . M.deEnv <$> getDynEnv let tyv = E.evalValType ntEnv tenv ty percentRef <- io $ newIORef Nothing @@ -1740,7 +1740,7 @@ replEvalCheckedExpr def sig = whenDebug (rPutStrLn (dump def1)) tenv <- E.envTypes . M.deEnv <$> getDynEnv - ntEnv <- E.NewtypeEnv . M.loadedNewtypes <$> getModuleEnv + ntEnv <- M.loadedNewtypes <$> getModuleEnv let tyv = E.evalValType ntEnv tenv ty -- add "it" to the namespace via a new declaration diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs index 96615e62a..c83c46fc6 100644 --- a/src/Cryptol/Symbolic/SBV.hs +++ b/src/Cryptol/Symbolic/SBV.hs @@ -56,7 +56,6 @@ import qualified Cryptol.Backend.FloatHelpers as FH import qualified Cryptol.Eval as Eval import qualified Cryptol.Eval.Concrete as Concrete -import qualified Cryptol.Eval.Type as Eval import qualified Cryptol.Eval.Value as Eval import Cryptol.Eval.SBV import Cryptol.Parser.Position (emptyRange) @@ -314,7 +313,7 @@ prepareQuery evo ProverCommand{..} = getEOpts <- M.getEvalOptsAction nts <- M.getNewtypes - let ?ntEnv = Eval.NewtypeEnv nts + let ?ntEnv = nts -- The `addAsm` function is used to combine assumptions that -- arise from the types of symbolic variables (e.g. Z n values @@ -348,7 +347,8 @@ prepareQuery evo ProverCommand{..} = -- evaluation environment, then we compute the value, finally -- we apply it to the symbolic inputs. (safety,b) <- doSBVEval $ - do env <- Eval.evalDecls sym extDgs mempty + do env <- Eval.evalDecls sym extDgs =<< + Eval.evalNewtypeDecls sym nts mempty v <- Eval.evalExpr sym env pcExpr appliedVal <- foldM (Eval.fromVFun sym) v args case pcQueryType of diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs index d3221b0c5..1b6cb1163 100644 --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -60,7 +60,6 @@ import qualified Cryptol.Backend.What4.SFloat as W4 import qualified Cryptol.Eval as Eval import qualified Cryptol.Eval.Concrete as Concrete -import qualified Cryptol.Eval.Type as Eval import qualified Cryptol.Eval.Value as Eval import Cryptol.Eval.What4 import Cryptol.Parser.Position (emptyRange) @@ -237,8 +236,7 @@ prepareQuery :: ([FinType],[VarShape (What4 sym)],W4.Pred sym, W4.Pred sym) ) prepareQuery sym ProverCommand { .. } = do - nts <- M.getNewtypes - let ntEnv = Eval.NewtypeEnv nts + ntEnv <- M.getNewtypes case predArgTypes ntEnv pcQueryType pcSchema of Left msg -> pure (Left msg) Right ts -> @@ -290,7 +288,9 @@ prepareQuery sym ProverCommand { .. } = do let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls doW4Eval (w4 sym) - do env <- Eval.evalDecls sym extDgs mempty + do env <- Eval.evalDecls sym extDgs =<< + Eval.evalNewtypeDecls sym ntEnv mempty + v <- Eval.evalExpr sym env pcExpr appliedVal <- foldM (Eval.fromVFun sym) v (map (pure . varShapeToValue sym) args)