diff --git a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs index 2cdbacacb..f605a4a17 100644 --- a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs +++ b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs @@ -44,8 +44,7 @@ evalExpression' e = let su = listParamSubst tys let theType = apSubst su (sType schema) tenv <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv - ntEnv <- loadedNewtypes <$> getModuleEnv - let tval = E.evalValType ntEnv tenv theType + let tval = E.evalValType tenv theType res <- runModuleCmd (evalExpr checked) val <- observe $ readBack tval res return (JSON.object [ "value" .= val diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index 3803421e8..5a2da0351 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -68,10 +68,10 @@ import Prelude.Compat type EvalEnv = GenEvalEnv Concrete type EvalPrims sym = - ( Backend sym, ?ntEnv :: NewtypeEnv, ?callStacks :: Bool, ?evalPrim :: PrimIdent -> Maybe (Either Expr (Prim sym)) ) + ( Backend sym, ?callStacks :: Bool, ?evalPrim :: PrimIdent -> Maybe (Either Expr (Prim sym)) ) type ConcPrims = - (?callStacks :: Bool, ?ntEnv :: NewtypeEnv, ?evalPrim :: PrimIdent -> Maybe (Either Expr (Prim Concrete))) + (?callStacks :: Bool, ?evalPrim :: PrimIdent -> Maybe (Either Expr (Prim Concrete))) -- Expression Evaluation ------------------------------------------------------- @@ -131,7 +131,7 @@ evalExpr sym env expr = case expr of xs <- mapM (sDelay sym) vs return $ VSeq len $ finiteSeqMap xs where - tyv = evalValType ?ntEnv (envTypes env) ty + tyv = evalValType (envTypes env) ty vs = map eval es len = genericLength es @@ -149,7 +149,7 @@ evalExpr sym env expr = case expr of ESet ty e sel v -> {-# SCC "evalExpr->ESet" #-} do e' <- eval e - let tyv = evalValType ?ntEnv (envTypes env) ty + let tyv = evalValType (envTypes env) ty evalSetSel sym tyv e' sel (eval v) EIf c t f -> {-# SCC "evalExpr->EIf" #-} do @@ -157,8 +157,8 @@ evalExpr sym env expr = case expr of iteValue sym b (eval t) (eval f) EComp n t h gs -> {-# SCC "evalExpr->EComp" #-} do - let len = evalNumType ?ntEnv (envTypes env) n - let elty = evalValType ?ntEnv (envTypes env) t + let len = evalNumType (envTypes env) n + let elty = evalValType (envTypes env) t evalComp sym env len elty h gs EVar n -> {-# SCC "evalExpr->EVar" #-} do @@ -187,8 +187,8 @@ evalExpr sym env expr = case expr of ETApp e ty -> {-# SCC "evalExpr->ETApp" #-} do eval e >>= \case - f@VPoly{} -> fromVPoly sym f $! (evalValType ?ntEnv (envTypes env) ty) - f@VNumPoly{} -> fromVNumPoly sym f $! (evalNumType ?ntEnv (envTypes env) ty) + f@VPoly{} -> fromVPoly sym f $! (evalValType (envTypes env) ty) + f@VNumPoly{} -> fromVNumPoly sym f $! (evalNumType (envTypes env) ty) val -> do vdoc <- ppV val panic "[Eval] evalExpr" ["expected a polymorphic value" @@ -339,7 +339,6 @@ evalDeclGroup sym env dg = do {-# SPECIALIZE fillHole :: - (?ntEnv :: NewtypeEnv) => Concrete -> GenEvalEnv Concrete -> (Name, Schema, SEval Concrete (GenValue Concrete), SEval Concrete (GenValue Concrete) -> SEval Concrete ()) -> @@ -358,7 +357,7 @@ evalDeclGroup sym env dg = do -- operation and only fall back on full eta expansion if the thunk is double-forced. fillHole :: - (?ntEnv :: NewtypeEnv, Backend sym) => + Backend sym => sym -> GenEvalEnv sym -> (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ()) -> @@ -366,7 +365,7 @@ fillHole :: fillHole sym env (nm, sch, _, fill) = do case lookupVar nm env of Just (Right v) - | isValueType ?ntEnv env sch -> + | isValueType env sch -> fill =<< sDelayFill sym v (Just (etaDelay sym env sch v)) (show (ppLocName nm)) @@ -380,9 +379,9 @@ fillHole sym env (nm, sch, _, fill) = do -- be implemented rather more efficiently than general types because we can -- rely on the 'delayFill' operation to build a thunk that falls back on performing -- eta-expansion rather than doing it eagerly. -isValueType :: NewtypeEnv -> GenEvalEnv sym -> Schema -> Bool -isValueType ntEnv env Forall{ sVars = [], sProps = [], sType = t0 } - = go (evalValType ntEnv (envTypes env) t0) +isValueType :: GenEvalEnv sym -> Schema -> Bool +isValueType env Forall{ sVars = [], sProps = [], sType = t0 } + = go (evalValType (envTypes env) t0) where go TVBit = True go (TVSeq _ x) = go x @@ -391,7 +390,7 @@ isValueType ntEnv env Forall{ sVars = [], sProps = [], sType = t0 } go (TVNewtype _ _ xs) = and (fmap go xs) go _ = False -isValueType _ _ _ = False +isValueType _ _ = False {-# SPECIALIZE etaWord :: @@ -415,7 +414,6 @@ etaWord sym n val = do pure $ LargeBitsVal n xs {-# SPECIALIZE etaDelay :: - (?ntEnv :: NewtypeEnv) => Concrete -> GenEvalEnv Concrete -> Schema -> @@ -430,7 +428,7 @@ etaWord sym n val = do -- expressions that should be expected to produce well-defined values in the -- denotational semantics will fail to terminate instead. etaDelay :: - (?ntEnv :: NewtypeEnv, Backend sym) => + Backend sym => sym -> GenEvalEnv sym -> Schema -> @@ -440,7 +438,7 @@ etaDelay sym env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0 where goTpVars env [] val = do stk <- sGetCallStack sym - go stk (evalValType ?ntEnv (envTypes env) tp0) val + go stk (evalValType (envTypes env) tp0) val goTpVars env (v:vs) val = case tpKind v of KType -> tlam sym $ \t -> @@ -851,7 +849,7 @@ evalMatch sym lenv m = case m of return $ bindVarList n vs lenv' where - len = evalNumType ?ntEnv (leTypes lenv) l + len = evalNumType (leTypes lenv) l -- XXX we don't currently evaluate these as though they could be recursive, as -- they are typechecked that way; the read environment to evalExpr is the same diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index eb57975d0..898f54e73 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, TypeEnv, bindTypeVar) > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2) > import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim) > import Cryptol.Utils.Panic (panic) @@ -278,35 +278,34 @@ recursion over its structure. For an expression that contains free variables, the meaning also depends on the environment `env`, which assigns values to those variables. -> evalExpr :: NewtypeEnv -> -> Env -- ^ Evaluation environment +> evalExpr :: Env -- ^ Evaluation environment > -> Expr -- ^ Expression to evaluate > -> E Value -> evalExpr ntEnv env expr = +> evalExpr env expr = > case expr of > -> ELocated _ e -> evalExpr ntEnv env e +> ELocated _ e -> evalExpr env e > > EList es _ty -> -> pure $ VList (Nat (genericLength es)) [ evalExpr ntEnv env e | e <- es ] +> pure $ VList (Nat (genericLength es)) [ evalExpr env e | e <- es ] > > ETuple es -> -> pure $ VTuple [ evalExpr ntEnv env e | e <- es ] +> pure $ VTuple [ evalExpr env e | e <- es ] > > ERec fields -> -> pure $ VRecord [ (f, evalExpr ntEnv env e) | (f, e) <- canonicalFields fields ] +> pure $ VRecord [ (f, evalExpr env e) | (f, e) <- canonicalFields fields ] > > ESel e sel -> -> evalSel sel =<< evalExpr ntEnv env e +> evalSel sel =<< evalExpr env e > > ESet ty e sel v -> -> evalSet (evalValType ntEnv (envTypes env) ty) -> (evalExpr ntEnv env e) sel (evalExpr ntEnv env v) +> evalSet (evalValType (envTypes env) ty) +> (evalExpr env e) sel (evalExpr env v) > > EIf c t f -> -> condValue (fromVBit <$> evalExpr ntEnv env c) (evalExpr ntEnv env t) (evalExpr ntEnv env f) +> condValue (fromVBit <$> evalExpr env c) (evalExpr env t) (evalExpr env f) > -> EComp _n _ty e branches -> evalComp ntEnv env e branches +> EComp _n _ty e branches -> evalComp env e branches > > EVar n -> > case Map.lookup n (envVars env) of @@ -317,22 +316,22 @@ assigns values to those variables. > ETAbs tv b -> > case tpKind tv of > KType -> pure $ VPoly $ \ty -> -> evalExpr ntEnv (bindType (tpVar tv) (Right ty) env) b +> evalExpr (bindType (tpVar tv) (Right ty) env) b > KNum -> pure $ VNumPoly $ \n -> -> evalExpr ntEnv (bindType (tpVar tv) (Left n) env) b +> evalExpr (bindType (tpVar tv) (Left n) env) b > k -> evalPanic "evalExpr" ["Invalid kind on type abstraction", show k] > > ETApp e ty -> -> evalExpr ntEnv env e >>= \case -> VPoly f -> f $! (evalValType ntEnv (envTypes env) ty) -> VNumPoly f -> f $! (evalNumType ntEnv (envTypes env) ty) +> evalExpr env e >>= \case +> VPoly f -> f $! (evalValType (envTypes env) ty) +> VNumPoly f -> f $! (evalNumType (envTypes env) ty) > _ -> evalPanic "evalExpr" ["Expected a polymorphic value"] > -> EApp e1 e2 -> appFun (evalExpr ntEnv env e1) (evalExpr ntEnv env e2) -> EAbs n _ty b -> pure $ VFun (\v -> evalExpr ntEnv (bindVar (n, v) env) b) -> EProofAbs _ e -> evalExpr ntEnv env e -> EProofApp e -> evalExpr ntEnv env e -> EWhere e dgs -> evalExpr ntEnv (foldl (evalDeclGroup ntEnv) env dgs) e +> EApp e1 e2 -> appFun (evalExpr env e1) (evalExpr env e2) +> EAbs n _ty b -> pure $ VFun (\v -> evalExpr (bindVar (n, v) env) b) +> EProofAbs _ e -> evalExpr env e +> EProofApp e -> evalExpr env e +> EWhere e dgs -> evalExpr (foldl evalDeclGroup env dgs) e > appFun :: E Value -> E Value -> E Value @@ -375,6 +374,7 @@ Update the given value using the given selector and new value. > case (tyv, sel) of > (TVTuple ts, TupleSel n _) -> updTupleAt ts n > (TVRec fs, RecordSel n _) -> updRecAt fs n +> (TVNewtype _ _ fs, RecordSel n _) -> updRecAt fs n > (TVSeq len _, ListSel n _) -> updSeqAt len n > (_, _) -> evalPanic "evalSet" ["type/selector mismatch", show tyv, show sel] > where @@ -417,43 +417,43 @@ The result of evaluating a match in an initial environment is a list of extended environments. Each new environment binds the same single variable to a different element of the match's list. -> evalMatch :: NewtypeEnv -> Env -> Match -> [Env] -> evalMatch ntEnv env m = +> evalMatch :: Env -> Match -> [Env] +> evalMatch env m = > case m of -> Let d -> [ bindVar (evalDecl ntEnv env d) env ] +> Let d -> [ bindVar (evalDecl env d) env ] > From nm len _ty expr -> [ bindVar (nm, get i) env | i <- idxs ] > where > get i = -> do v <- evalExpr ntEnv env expr +> do v <- evalExpr env expr > genericIndex (fromVList v) i > > idxs :: [Integer] > idxs = -> case evalNumType ntEnv (envTypes env) len of +> case evalNumType (envTypes env) len of > Inf -> [0 ..] > Nat n -> [0 .. n-1] -> lenMatch :: NewtypeEnv -> Env -> Match -> Nat' -> lenMatch ntEnv env m = +> lenMatch :: Env -> Match -> Nat' +> lenMatch env m = > case m of > Let _ -> Nat 1 -> From _ len _ _ -> evalNumType ntEnv (envTypes env) len +> From _ len _ _ -> evalNumType (envTypes env) len The result of of evaluating a branch in an initial environment is a list of extended environments, each of which extends the initial environment with the same set of new variables. The length of the list is equal to the product of the lengths of the lists in the matches. -> evalBranch :: NewtypeEnv -> Env -> [Match] -> [Env] -> evalBranch _ env [] = [env] -> evalBranch ntEnv env (match : matches) = -> [ env'' | env' <- evalMatch ntEnv env match -> , env'' <- evalBranch ntEnv env' matches ] +> evalBranch :: Env -> [Match] -> [Env] +> evalBranch env [] = [env] +> evalBranch env (match : matches) = +> [ env'' | env' <- evalMatch env match +> , env'' <- evalBranch env' matches ] -> lenBranch :: NewtypeEnv -> Env -> [Match] -> Nat' -> lenBranch _ntEnv _env [] = Nat 1 -> lenBranch ntEnv env (match : matches) = -> nMul (lenMatch ntEnv env match) (lenBranch ntEnv env matches) +> lenBranch :: Env -> [Match] -> Nat' +> lenBranch _env [] = Nat 1 +> lenBranch env (match : matches) = +> nMul (lenMatch env match) (lenBranch env matches) The head expression of the comprehension can refer to any variable bound in any of the parallel branches. So to evaluate the @@ -462,18 +462,17 @@ environments from each branch. The head expression is then evaluated separately in each merged environment. The length of the resulting list is equal to the minimum length over all parallel branches. -> evalComp :: NewtypeEnv -> -> Env -- ^ Starting evaluation environment +> evalComp :: Env -- ^ Starting evaluation environment > -> Expr -- ^ Head expression of the comprehension > -> [[Match]] -- ^ List of parallel comprehension branches > -> E Value -> evalComp ntEnv env expr branches = -> pure $ VList len [ evalExpr ntEnv e expr | e <- envs ] +> evalComp env expr branches = +> pure $ VList len [ evalExpr e expr | e <- envs ] > where > -- Generate a new environment for each iteration of each > -- parallel branch. > benvs :: [[Env]] -> benvs = map (evalBranch ntEnv env) branches +> benvs = map (evalBranch env) branches > > -- Zip together the lists of environments from each branch, > -- producing a list of merged environments. Longer branches get @@ -482,7 +481,7 @@ list is equal to the minimum length over all parallel branches. > envs = foldr1 (zipWith mappend) benvs > > len :: Nat' -> len = foldr1 nMin (map (lenBranch ntEnv env) branches) +> len = foldr1 nMin (map (lenBranch env) branches) Declarations @@ -494,22 +493,41 @@ recursive declaration group, we tie the recursive knot by evaluating each declaration in the extended environment `env'` that includes all the new bindings. -> evalDeclGroup :: NewtypeEnv -> Env -> DeclGroup -> Env -> evalDeclGroup ntEnv env dg = do +> evalDeclGroup :: Env -> DeclGroup -> Env +> evalDeclGroup env dg = do > case dg of > NonRecursive d -> -> bindVar (evalDecl ntEnv env d) env +> bindVar (evalDecl env d) env > Recursive ds -> > let env' = foldr bindVar env bindings -> bindings = map (evalDecl ntEnv env') ds +> bindings = map (evalDecl env') ds > in env' > -> evalDecl :: NewtypeEnv -> Env -> Decl -> (Name, E Value) -> evalDecl ntEnv env d = +> evalDecl :: Env -> Decl -> (Name, E Value) +> evalDecl env d = > case dDefinition d of > DPrim -> (dName d, pure (evalPrim (dName d))) -> DExpr e -> (dName d, evalExpr ntEnv env e) +> DExpr e -> (dName d, evalExpr env e) +> + +Newtypes +-------- +At runtime, newtypes values are represented in exactly +the same was as records. The constructor function for +newtypes is thus basically just the identity function, +that consumes and ignores its type arguments. + +> evalNewtypeDecl :: Env -> Newtype -> Env +> evalNewtypeDecl env nt = bindVar (ntName nt, pure val) env +> where +> val = foldr tabs con (ntParams nt) +> con = VFun (\x -> x) +> tabs tp body = +> case tpKind tp of +> KType -> VPoly (\_ -> pure body) +> KNum -> VNumPoly (\_ -> pure body) +> k -> evalPanic "evalNewtypeDecl" ["illegal newtype parameter kind", show k] Primitives ========== @@ -1710,7 +1728,7 @@ running the reference evaluator on an expression. > evaluate expr minp = return (Right (val, modEnv), []) > where > modEnv = M.minpModuleEnv minp -> ntEnv = M.loadedNewtypes modEnv > extDgs = concatMap mDecls (M.loadedModules modEnv) -> env = foldl (evalDeclGroup ntEnv) mempty extDgs -> val = evalExpr ntEnv env expr +> nts = Map.elems (M.loadedNewtypes modEnv) +> env = foldl evalDeclGroup (foldl evalNewtypeDecl mempty nts) extDgs +> val = evalExpr env expr diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs index 5e10993f3..ced6e1c9d 100644 --- a/src/Cryptol/Eval/Type.hs +++ b/src/Cryptol/Eval/Type.hs @@ -20,7 +20,6 @@ import Cryptol.Utils.Ident (Ident) import Cryptol.Utils.RecordMap import Data.Maybe(fromMaybe) -import qualified Data.Map.Strict as Map import qualified Data.IntMap.Strict as IntMap import GHC.Generics (Generic) import Control.DeepSeq @@ -109,8 +108,6 @@ instance Semigroup TypeEnv where l <> r = TypeEnv { envTypeMap = IntMap.union (envTypeMap l) (envTypeMap r) } -type NewtypeEnv = Map.Map Name Newtype - lookupTypeVar :: TVar -> TypeEnv -> Maybe (Either Nat' TValue) lookupTypeVar tv env = IntMap.lookup (tvUnique tv) (envTypeMap env) @@ -118,19 +115,19 @@ bindTypeVar :: TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv bindTypeVar tv ty env = env{ envTypeMap = IntMap.insert (tvUnique tv) ty (envTypeMap env) } -- | Evaluation for types (kind * or #). -evalType :: NewtypeEnv -> TypeEnv -> Type -> Either Nat' TValue -evalType ntEnv env ty = +evalType :: TypeEnv -> Type -> Either Nat' TValue +evalType env ty = case ty of TVar tv -> case lookupTypeVar tv env of Just v -> v Nothing -> evalPanic "evalType" ["type variable not bound", show tv] - TUser _ _ ty' -> evalType ntEnv env ty' + TUser _ _ ty' -> evalType env ty' TRec fields -> Right $ TVRec (fmap val fields) - TNewtype nt ts -> Right $ TVNewtype nt tvs $ evalNewtypeBody ntEnv env nt tvs - where tvs = map (evalType ntEnv env) ts + TNewtype nt ts -> Right $ TVNewtype nt tvs $ evalNewtypeBody env nt tvs + where tvs = map (evalType env) ts TCon (TC c) ts -> case (c, ts) of @@ -149,7 +146,7 @@ evalType ntEnv env ty = (TCInf, []) -> Left $ Inf (TCAbstract u,vs) -> case kindOf ty of - KType -> Right $ TVAbstract u (map (evalType ntEnv env) vs) + KType -> Right $ TVAbstract u (map (evalType env) vs) k -> evalPanic "evalType" [ "Unsupported" , "*** Abstract type of kind: " ++ show (pp k) @@ -162,16 +159,16 @@ evalType ntEnv env ty = TCon (TError _) ts -> evalPanic "evalType" $ "Lingering invalid type" : map (show . pp) ts where - val = evalValType ntEnv env - num = evalNumType ntEnv env + val = evalValType env + num = evalNumType env inum x = case num x of Nat i -> i Inf -> evalPanic "evalType" ["Expecting a finite size, but got `inf`"] -- | Evaluate the body of a newtype, given evaluated arguments -evalNewtypeBody :: NewtypeEnv -> TypeEnv -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue -evalNewtypeBody ntEnv env0 nt args = fmap (evalValType ntEnv env') (ntFields nt) +evalNewtypeBody :: TypeEnv -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue +evalNewtypeBody env0 nt args = fmap (evalValType env') (ntFields nt) where env' = loop env0 (ntParams nt) args @@ -180,16 +177,16 @@ evalNewtypeBody ntEnv env0 nt args = fmap (evalValType ntEnv env') (ntFields nt) loop _ _ _ = evalPanic "evalNewtype" ["type parameter/argument mismatch"] -- | Evaluation for value types (kind *). -evalValType :: NewtypeEnv -> TypeEnv -> Type -> TValue -evalValType ntEnv env ty = - case evalType ntEnv env ty of +evalValType :: TypeEnv -> Type -> TValue +evalValType env ty = + case evalType env ty of Left _ -> evalPanic "evalValType" ["expected value type, found numeric type"] Right t -> t -- | Evaluation for number types (kind #). -evalNumType :: NewtypeEnv -> TypeEnv -> Type -> Nat' -evalNumType ntEnv env ty = - case evalType ntEnv env ty of +evalNumType :: TypeEnv -> Type -> Nat' +evalNumType env ty = + case evalType env ty of Left n -> n Right _ -> evalPanic "evalValType" ["expected numeric type, found value type"] diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index e2ada6508..603719bb3 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -206,8 +206,6 @@ doLoadModule quiet isrc path fp pm0 = let ?evalPrim = \i -> Right <$> Map.lookup i tbl callStacks <- getCallStacks let ?callStacks = callStacks - nts <- getNewtypes - let ?ntEnv = nts unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm) loadedModule path fp tcm @@ -572,8 +570,6 @@ evalExpr e = do let ?range = emptyRange callStacks <- getCallStacks let ?callStacks = callStacks - nts <- getNewtypes - let ?ntEnv = nts io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e) @@ -587,8 +583,6 @@ evalDecls dgs = do let ?evalPrim = \i -> Right <$> Map.lookup i tbl callStacks <- getCallStacks let ?callStacks = callStacks - nts <- getNewtypes - 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 04714f284..cd5707daa 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -364,8 +364,7 @@ dumpTestsCmd outFile str pos fnm = testNum <- getKnownUser "tests" :: REPL Int g <- io newTFGen tenv <- E.envTypes . M.deEnv <$> getDynEnv - ntEnv <- M.loadedNewtypes <$> getModuleEnv - let tyv = E.evalValType ntEnv tenv ty + let tyv = E.evalValType tenv ty gens <- case TestR.dumpableType tyv of Nothing -> raise (TypeNotTestable ty) @@ -428,9 +427,8 @@ qcExpr :: qcExpr qcMode exprDoc texpr schema = do (val,ty) <- replEvalCheckedExpr texpr schema testNum <- (toInteger :: Int -> Integer) <$> getKnownUser "tests" - ntEnv <- M.loadedNewtypes <$> getModuleEnv tenv <- E.envTypes . M.deEnv <$> getDynEnv - let tyv = E.evalValType ntEnv tenv ty + let tyv = E.evalValType tenv ty percentRef <- io $ newIORef Nothing testsRef <- io $ newIORef 0 case testableType tyv of @@ -1740,8 +1738,7 @@ replEvalCheckedExpr def sig = whenDebug (rPutStrLn (dump def1)) tenv <- E.envTypes . M.deEnv <$> getDynEnv - ntEnv <- M.loadedNewtypes <$> getModuleEnv - let tyv = E.evalValType ntEnv tenv ty + let tyv = E.evalValType tenv ty -- add "it" to the namespace via a new declaration itVar <- bindItVariable tyv def1 diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index 2020b8e51..da93c77bc 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -55,7 +55,7 @@ import qualified Cryptol.Eval.Concrete as Concrete import Cryptol.Eval.Value import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat -import Cryptol.Eval.Type (TValue(..), evalType,NewtypeEnv,tValTy,tNumValTy) +import Cryptol.Eval.Type (TValue(..), evalType,tValTy,tNumValTy) import Cryptol.Utils.Ident (Ident,prelPrim,floatPrim) import Cryptol.Utils.RecordMap import Cryptol.Utils.Panic @@ -116,10 +116,10 @@ data ProverResult = AllSatResult [SatResult] -- LAZY -predArgTypes :: NewtypeEnv -> QueryType -> Schema -> Either String [FinType] -predArgTypes ntEnv qtype schema@(Forall ts ps ty) +predArgTypes :: QueryType -> Schema -> Either String [FinType] +predArgTypes qtype schema@(Forall ts ps ty) | null ts && null ps = - case go <$> (evalType ntEnv mempty ty) of + case go <$> (evalType mempty ty) of Right (Just fts) -> Right fts _ | SafetyQuery <- qtype -> Left $ "Expected finite result type:\n" ++ show (pp schema) | otherwise -> Left $ "Not a valid predicate type:\n" ++ show (pp schema) diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs index c83c46fc6..901cc7ac9 100644 --- a/src/Cryptol/Symbolic/SBV.hs +++ b/src/Cryptol/Symbolic/SBV.hs @@ -312,8 +312,7 @@ prepareQuery evo ProverCommand{..} = getEOpts <- M.getEvalOptsAction - nts <- M.getNewtypes - let ?ntEnv = nts + ntEnv <- M.getNewtypes -- The `addAsm` function is used to combine assumptions that -- arise from the types of symbolic variables (e.g. Z n values @@ -325,7 +324,7 @@ prepareQuery evo ProverCommand{..} = SafetyQuery -> \x y -> SBV.svOr (SBV.svNot x) y SatQuery _ -> \x y -> SBV.svAnd x y - case predArgTypes ?ntEnv pcQueryType pcSchema of + case predArgTypes pcQueryType pcSchema of Left msg -> return (Left msg) Right ts -> M.io $ do when pcVerbose $ logPutStrLn (Eval.evalLogger evo) "Simulating..." @@ -348,7 +347,7 @@ prepareQuery evo ProverCommand{..} = -- we apply it to the symbolic inputs. (safety,b) <- doSBVEval $ do env <- Eval.evalDecls sym extDgs =<< - Eval.evalNewtypeDecls sym nts mempty + Eval.evalNewtypeDecls sym ntEnv 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 1b6cb1163..fa9d66b12 100644 --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -237,7 +237,7 @@ prepareQuery :: ) prepareQuery sym ProverCommand { .. } = do ntEnv <- M.getNewtypes - case predArgTypes ntEnv pcQueryType pcSchema of + case predArgTypes pcQueryType pcSchema of Left msg -> pure (Left msg) Right ts -> do args <- liftIO (mapM (freshVar (what4FreshFns (w4 sym))) ts) @@ -282,7 +282,6 @@ prepareQuery sym ProverCommand { .. } = do let ?range = emptyRange callStacks <- M.getCallStacks let ?callStacks = callStacks - let ?ntEnv = ntEnv modEnv <- M.getModuleEnv let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls