GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 11:22:33 +03:00
Code Issues Projects Releases Wiki Activity

Make the symbolic simulator more lazy to avoid non-termination

Browse Source
This commit is contained in:
Brian Huffman 2014-09-15 17:25:17 -07:00
parent b8ed45de39
commit fa76ad7e28
1 changed files with 14 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/Cryptol/Symbolic.hs
View File

@ -334,13 +334,25 @@ evalDeclGroup :: Env -> DeclGroup -> Env
evalDeclGroup env dg =
case dg of
NonRecursive d -> bindVar (evalDecl env d) env
Recursive ds -> let env' = foldr bindVar env bindings
Recursive ds -> let env' = foldr bindVar env lazyBindings
bindings = map (evalDecl env') ds
in env'
lazyBindings = [ (qname, copyBySchema env (dSignature d) v)
| (d, (qname, v)) <- zip ds bindings ]
in env' -- foldr bindVar env bindings
evalDecl :: Env -> Decl -> (QName, Value)
evalDecl env d = (dName d, evalExpr env (dDefinition d))
-- | Make a copy of the given value, building the spine based only on
-- the type without forcing the value argument. This lets us avoid
-- strictness problems when evaluating recursive definitions.
copyBySchema :: Env -> Schema -> Value -> Value
copyBySchema env0 (Forall params _props ty) = go params env0
where
go [] env v = logicUnary id id (evalType env ty) v
go (p : ps) env v =
VPoly (\t -> go ps (bindType (tpVar p) t env) (fromVPoly v t))
-- List Comprehensions ---------------------------------------------------------
-- | Evaluate a comprehension.