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.TypeCheck.AST
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
import Cryptol.Prims.Eval
import Data.List (transpose)
import qualified Data.Map as Map
#if __GLASGOW_HASKELL__ < 710
import Data.Monoid (Monoid(..),mconcat)
#endif
moduleEnv :: Module -> EvalEnv -> EvalEnv
moduleEnv m env = evalDecls (mDecls m) (evalNewtypes (mNewtypes m) env)
evalExpr :: EvalEnv -> Expr -> Value
evalExpr env expr = case expr of
ECon con -> evalECon con
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 QName 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) (evalExpr renv (dDefinition d))
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) ]
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 = map (branchEnvs env) ms
allBranches es = length es == length ms
slices = takeWhile allBranches (transpose benvs)
envs = map mconcat slices
branchEnvs :: ReadEnv -> [Match] -> [EvalEnv]
branchEnvs env matches = case matches of
m:ms -> do
env' <- evalMatch env m
branchEnvs env' ms
[] -> return env
evalMatch :: EvalEnv -> Match -> [EvalEnv]
evalMatch env m = case m of
From n _ty expr -> do
e <- fromSeq (evalExpr env expr)
return (bindVar n e env)
Let d -> [evalDecl env d env]