Skip to content

Commit

Permalink
Don't memoize subterms in function position in saw-core simulator.
Browse files Browse the repository at this point in the history
Memoizing such subterms doesn't actually save anything, because
the memoized value is just a monadic thunk that runs the same
simulator code each time it's called. This patch lets us avoid
some of the IntMap insertion operations.
  • Loading branch information
Brian Huffman committed Sep 17, 2021
1 parent 66afe20 commit 5bff905
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions saw-core/src/Verifier/SAW/Simulator.hs
Original file line number Diff line number Diff line change
Expand Up @@ -518,7 +518,7 @@ mkMemoLocal cfg memoClosed t env = go mempty t
goTermF memo tf =
case tf of
FTermF ftf -> foldlM go memo ftf
App t1 t2 -> do memo' <- go memo t1
App t1 t2 -> do memo' <- goTermF memo (unwrapTermF t1)
go memo' t2
Lambda _ t1 _ -> go memo t1
Pi _ t1 _ -> go memo t1
Expand Down Expand Up @@ -549,10 +549,10 @@ evalLocalTermF cfg memoClosed memoLocal tf0 env = evalTermF cfg lam recEval tf0
where
lam = evalOpen cfg memoClosed
recEval (Unshared tf) = evalTermF cfg lam recEval tf env
recEval (STApp{ stAppIndex = i, stAppFreeVars = fv }) =
recEval (STApp{ stAppIndex = i, stAppFreeVars = fv, stAppTermF = tf }) =
case IMap.lookup i memo of
Just x -> force x
Nothing -> panic "evalLocalTermF" ["internal error"]
Nothing -> evalTermF cfg lam recEval tf env
where memo = if fv == emptyBitSet then memoClosed else memoLocal

{-# SPECIALIZE evalOpen ::
Expand Down

0 comments on commit 5bff905

Please sign in to comment.