module Cryptol.Eval (
moduleEnv
, EvalEnv()
, emptyEnv
, evalExpr
, evalDecls
, EvalError(..)
, WithBase(..)
) where
import Cryptol.Eval.Error
import Cryptol.Eval.Env
import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
import Cryptol.Prims.Eval
import qualified Data.Map as Map
import Prelude ()
import Prelude.Compat
moduleEnv :: Module -> EvalEnv -> EvalEnv
moduleEnv m env = evalDecls (mDecls m) (evalNewtypes (mNewtypes m) env)
evalExpr :: EvalEnv -> Expr -> Value
evalExpr env expr = case expr of
EList es ty -> VSeq (isTBit (evalType env ty)) (map (evalExpr env) es)
ETuple es -> VTuple (map eval es)
ERec fields -> VRecord [ (f,eval e) | (f,e) <- fields ]
ESel e sel -> evalSel env e sel
EIf c t f | fromVBit (eval c) -> eval t
| otherwise -> eval f
EComp l h gs -> evalComp env (evalType env l) h gs
EVar n -> case lookupVar n env of
Just val -> val
Nothing -> panic "[Eval] evalExpr"
["var `" ++ show (pp n) ++ "` is not defined"
, pretty (WithBase defaultPPOpts env)
]
ETAbs tv b -> VPoly $ \ty -> evalExpr (bindType (tpVar tv) ty env) b
ETApp e ty -> case eval e of
VPoly f -> f (evalType env ty)
val -> panic "[Eval] evalExpr"
["expected a polymorphic value"
, show (ppV val), show e, show ty
]
EApp f x -> case eval f of
VFun f' -> f' (eval x)
it -> panic "[Eval] evalExpr" ["not a function", show (ppV it) ]
EAbs n _ty b -> VFun (\ val -> evalExpr (bindVar n val env) b )
EProofAbs _ e -> evalExpr env e
EProofApp e -> evalExpr env e
ECast e _ty -> evalExpr env e
EWhere e ds -> evalExpr (evalDecls ds env) e
where
eval = evalExpr env
ppV = ppValue defaultPPOpts
evalNewtypes :: Map.Map Name Newtype -> EvalEnv -> EvalEnv
evalNewtypes nts env = Map.foldl (flip evalNewtype) env nts
evalNewtype :: Newtype -> EvalEnv -> EvalEnv
evalNewtype nt = bindVar (ntName nt) (foldr tabs con (ntParams nt))
where
tabs _tp body = tlam (\ _ -> body)
con = VFun id
evalDecls :: [DeclGroup] -> EvalEnv -> EvalEnv
evalDecls dgs env = foldl (flip evalDeclGroup) env dgs
evalDeclGroup :: DeclGroup -> EvalEnv -> EvalEnv
evalDeclGroup dg env = env'
where
env' = case dg of
Recursive ds -> foldr (evalDecl env') env ds
NonRecursive d -> evalDecl env d env
evalDecl :: ReadEnv -> Decl -> EvalEnv -> EvalEnv
evalDecl renv d =
bindVar (dName d) $
case dDefinition d of
DPrim -> evalPrim d
DExpr e -> evalExpr renv e
evalSel :: ReadEnv -> Expr -> Selector -> Value
evalSel env e sel = case sel of
TupleSel n _ -> tupleSel n val
RecordSel n _ -> recordSel n val
ListSel ix _ -> fromSeq val !! ix
where
val = evalExpr env e
tupleSel n v =
case v of
VTuple vs -> vs !! n
VSeq False vs -> VSeq False [ tupleSel n v1 | v1 <- vs ]
VStream vs -> VStream [ tupleSel n v1 | v1 <- vs ]
VFun f -> VFun (\x -> tupleSel n (f x))
_ -> evalPanic "Cryptol.Eval.evalSel"
[ "Unexpected value in tuple selection"
, show (ppValue defaultPPOpts v) ]
recordSel n v =
case v of
VRecord {} -> lookupRecord n v
VSeq False vs -> VSeq False [ recordSel n v1 | v1 <- vs ]
VStream vs -> VStream [recordSel n v1 | v1 <- vs ]
VFun f -> VFun (\x -> recordSel n (f x))
_ -> evalPanic "Cryptol.Eval.evalSel"
[ "Unexpected value in record selection"
, show (ppValue defaultPPOpts v) ]
data ZList a = Pure a | Zip [a]
getZList :: ZList a -> [a]
getZList (Pure x) = repeat x
getZList (Zip xs) = xs
instance Functor ZList where
fmap f (Pure x) = Pure (f x)
fmap f (Zip xs) = Zip (map f xs)
instance Applicative ZList where
pure x = Pure x
Pure f <*> Pure x = Pure (f x)
Pure f <*> Zip xs = Zip (map f xs)
Zip fs <*> Pure x = Zip (map ($ x) fs)
Zip fs <*> Zip xs = Zip (zipWith ($) fs xs)
data ListEnv = ListEnv
{ leVars :: Map.Map Name (ZList Value)
, leTypes :: Map.Map TVar TValue
}
instance Monoid ListEnv where
mempty = ListEnv
{ leVars = Map.empty
, leTypes = Map.empty
}
mappend l r = ListEnv
{ leVars = Map.union (leVars l) (leVars r)
, leTypes = Map.union (leTypes l) (leTypes r)
}
toListEnv :: EvalEnv -> ListEnv
toListEnv e =
ListEnv
{ leVars = fmap Pure (envVars e)
, leTypes = envTypes e
}
zipListEnv :: ListEnv -> [EvalEnv]
zipListEnv (ListEnv vm tm) =
[ EvalEnv { envVars = v, envTypes = tm }
| v <- getZList (sequenceA vm) ]
bindVarList :: Name -> [Value] -> ListEnv -> ListEnv
bindVarList n vs lenv = lenv { leVars = Map.insert n (Zip vs) (leVars lenv) }
evalComp :: ReadEnv -> TValue -> Expr -> [[Match]] -> Value
evalComp env seqty body ms
| Just (len,el) <- isTSeq seqty = toSeq len el [ evalExpr e body | e <- envs ]
| otherwise = evalPanic "Cryptol.Eval" [ "evalComp given a non sequence"
, show seqty
]
where
benvs :: [ListEnv]
benvs = map (branchEnvs (toListEnv env)) ms
envs :: [EvalEnv]
envs = zipListEnv (mconcat benvs)
branchEnvs :: ListEnv -> [Match] -> ListEnv
branchEnvs env matches = foldl evalMatch env matches
evalMatch :: ListEnv -> Match -> ListEnv
evalMatch lenv m = case m of
From n _ty expr -> bindVarList n (concat vss) lenv'
where
vss = [ fromSeq (evalExpr env expr) | env <- zipListEnv lenv ]
stutter (Pure x) = Pure x
stutter (Zip xs) = Zip [ x | (x, vs) <- zip xs vss, _ <- vs ]
lenv' = lenv { leVars = fmap stutter (leVars lenv) }
Let d -> bindVarList (dName d) (map f (zipListEnv lenv)) lenv
where f env =
case dDefinition d of
DPrim -> evalPrim d
DExpr e -> evalExpr env e