Pass initial simplifier cache to performRewrite

runtimeverification · Aug 5, 2024 · 10f6b18 · 10f6b18
1 parent 24b8126
commit 10f6b18
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 12 deletions.
diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs
@@ -177,8 +177,7 @@ respond stateVar request =
                                         unsupported
                             (Left other, _) ->
                                 pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
-                            (Right newPattern, _simplifierCache) -> do
-                                -- FIXME do not throw away @simplifierCache@, pass it to performRewrite somehow
+                            (Right newPattern, simplifierCache) -> do
                                 logger <- getLogger
                                 prettyModifiers <- getPrettyModifiers
                                 let rewriteConfig =
@@ -197,7 +196,7 @@ respond stateVar request =
                                             }
 
                                 result <-
-                                    performRewrite rewriteConfig newPattern
+                                    performRewrite rewriteConfig simplifierCache newPattern
                                 SMT.finaliseSolver solver
                                 stop <- liftIO $ getTime Monotonic
                                 pure $ execResponse (duration req.logTiming start stop) req result substitution unsupported

diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs
@@ -704,9 +704,10 @@ performRewrite ::
     forall io.
     LoggerMIO io =>
     RewriteConfig ->
+    SimplifierCache ->
     Pattern ->
     io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern)
-performRewrite rewriteConfig pat = do
+performRewrite rewriteConfig initialCache pat = do
     (rr, RewriteStepsState{counter, traces}) <-
         flip runStateT rewriteStart $ doSteps False pat
     pure (counter, traces, rr)
@@ -722,6 +723,14 @@ performRewrite rewriteConfig pat = do
         , terminalLabels
         } = rewriteConfig
 
+    rewriteStart :: RewriteStepsState
+    rewriteStart =
+        RewriteStepsState
+            { counter = 0
+            , traces = mempty
+            , simplifierCache = initialCache
+            }
+
     logDepth = withContext CtxDepth . logMessage
 
     depthReached n = maybe False (n >=) mbMaxDepth
@@ -919,11 +928,3 @@ data RewriteStepsState = RewriteStepsState
     , traces :: !(Seq (RewriteTrace ()))
     , simplifierCache :: SimplifierCache
     }
-
-rewriteStart :: RewriteStepsState
-rewriteStart =
-    RewriteStepsState
-        { counter = 0
-        , traces = mempty
-        , simplifierCache = mempty
-        }