Bundle performRewrite options into RewriteConfig

Author: jberthold

booster/library/Booster/JsonRpc.hs

@@ -54,6 +54,7 @@ import Booster.Pattern.Bool (pattern TrueBool)
 import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms)
 import Booster.Pattern.Pretty
 import Booster.Pattern.Rewrite (
+    RewriteConfig (..),
     RewriteFailed (..),
     RewriteResult (..),
     RewriteTrace (..),
@@ -153,17 +154,26 @@ respond stateVar request =
                                     ]
 
                         solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
+
+                        logger <- getLogger
+                        prettyModifiers <- getPrettyModifiers
+                        let rewriteConfig =
+                                RewriteConfig
+                                    { definition = def
+                                    , llvmApi = mLlvmLibrary
+                                    , smtSolver = solver
+                                    , varsToAvoid = substVars
+                                    , doTracing
+                                    , logger
+                                    , prettyModifiers
+                                    , mbMaxDepth = mbDepth
+                                    , mbSimplify = rewriteOpts.interimSimplification
+                                    , cutLabels = cutPoints
+                                    , terminalLabels = terminals
+                                    }
                         result <-
                             performRewrite
-                                doTracing
-                                def
-                                mLlvmLibrary
-                                solver
-                                substVars
-                                mbDepth
-                                cutPoints
-                                terminals
-                                rewriteOpts.interimSimplification
+                                rewriteConfig
                                 substPat
                         SMT.finaliseSolver solver
                         stop <- liftIO $ getTime Monotonic

booster/library/Booster/Pattern/Rewrite.hs

@@ -10,6 +10,7 @@ License     : BSD-3-Clause
 module Booster.Pattern.Rewrite (
     performRewrite,
     rewriteStep,
+    RewriteConfig (..),
     RewriteFailed (..),
     RewriteResult (..),
     RewriteTrace (..),
@@ -84,6 +85,9 @@ data RewriteConfig = RewriteConfig
     , doTracing :: Flag "CollectRewriteTraces"
     , logger :: Logger LogMessage
     , prettyModifiers :: ModifiersRep
+    , -- below: parameters used only in performRewrite
+      mbMaxDepth, mbSimplify :: Maybe Natural
+    , cutLabels, terminalLabels :: [Text]
     }
 
 instance MonadIO io => LoggerMIO (RewriteT io) where
@@ -99,25 +103,12 @@ pattern NoCollectRewriteTraces :: Flag "CollectRewriteTraces"
 pattern NoCollectRewriteTraces = Flag False
 
 runRewriteT ::
-    LoggerMIO io =>
-    Flag "CollectRewriteTraces" ->
-    KoreDefinition ->
-    Maybe LLVM.API ->
-    SMT.SMTContext ->
-    Set.Set Variable ->
+    RewriteConfig ->
     SimplifierCache ->
     RewriteT io a ->
     io (Either (RewriteFailed "Rewrite") (a, SimplifierCache))
-runRewriteT doTracing definition llvmApi smtSolver varsToAvoid cache m = do
-    logger <- getLogger
-    prettyModifiers <- getPrettyModifiers
-    runExceptT
-        . flip runStateT cache
-        . flip
-            runReaderT
-            RewriteConfig{definition, llvmApi, smtSolver, varsToAvoid, doTracing, logger, prettyModifiers}
-        . unRewriteT
-        $ m
+runRewriteT rewriteConfig cache =
+    runExceptT . flip runStateT cache . flip runReaderT rewriteConfig . unRewriteT
 
 throw :: LoggerMIO io => RewriteFailed "Rewrite" -> RewriteT io a
 throw = RewriteT . lift . lift . throwE
@@ -704,27 +695,25 @@ mkDiffTerms = \case
 performRewrite ::
     forall io.
     LoggerMIO io =>
-    Flag "CollectRewriteTraces" ->
-    KoreDefinition ->
-    Maybe LLVM.API ->
-    SMT.SMTContext ->
-    -- | Variable names to avoid (for new existentials)
-    Set.Set Variable ->
-    -- | maximum depth
-    Maybe Natural ->
-    -- | cut point rule labels
-    [Text] ->
-    -- | terminal rule labels
-    [Text] ->
-    -- | interim-simplification frequency
-    (Maybe Natural) ->
+    RewriteConfig ->
     Pattern ->
     io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern)
-performRewrite doTracing def mLlvmLibrary smtSolver varsToAvoid mbMaxDepth cutLabels terminalLabels mbSimplify pat = do
+performRewrite rewriteConfig pat = do
     (rr, RewriteStepsState{counter, traces}) <-
         flip runStateT rewriteStart $ doSteps False pat
     pure (counter, traces, rr)
   where
+    RewriteConfig
+        { definition
+        , llvmApi
+        , smtSolver
+        , doTracing
+        , mbMaxDepth
+        , mbSimplify
+        , cutLabels
+        , terminalLabels
+        } = rewriteConfig
+
     logDepth = withContext CtxDepth . logMessage
 
     depthReached n = maybe False (n >=) mbMaxDepth
@@ -745,7 +734,7 @@ performRewrite doTracing def mLlvmLibrary smtSolver varsToAvoid mbMaxDepth cutLa
     simplifyP p = withContext CtxSimplify $ do
         st <- get
         let cache = st.simplifierCache
-        evaluatePattern def mLlvmLibrary smtSolver cache p >>= \(res, newCache) -> do
+        evaluatePattern definition llvmApi smtSolver cache p >>= \(res, newCache) -> do
             updateCache newCache
             case res of
                 Right newPattern -> do
@@ -818,11 +807,7 @@ performRewrite doTracing def mLlvmLibrary smtSolver varsToAvoid mbMaxDepth cutLa
                         Just newPat -> doSteps True newPat
                 | otherwise ->
                     runRewriteT
-                        doTracing
-                        def
-                        mLlvmLibrary
-                        smtSolver
-                        varsToAvoid
+                        rewriteConfig
                         simplifierCache
                         (withPatternContext pat' $ rewriteStep cutLabels terminalLabels pat')
                         >>= \case

booster/unit-tests/Test/Booster/Pattern/Rewrite.hs

@@ -14,15 +14,18 @@ import Data.Bifunctor (second)
 import Data.List.NonEmpty qualified as NE
 import Data.Map (Map)
 import Data.Map qualified as Map
+import Data.Proxy (Proxy (..))
 import Data.Text (Text)
 import Numeric.Natural
 import Test.Tasty
 import Test.Tasty.HUnit
 
 import Booster.Definition.Attributes.Base
 import Booster.Definition.Base
+import Booster.Log (Logger (..))
 import Booster.Pattern.Base
 import Booster.Pattern.Index (CellIndex (..), TermIndex (..))
+import Booster.Pattern.Pretty (ModifiersRep (..))
 import Booster.Pattern.Rewrite
 import Booster.SMT.Interface (noSolver)
 import Booster.Syntax.Json.Internalise (trm)
@@ -171,6 +174,24 @@ mkTheory = Map.map mkPriorityGroups . Map.fromList
 d :: Term
 d = dv someSort "thing"
 
+testConf :: IO RewriteConfig
+testConf = do
+    smtSolver <- noSolver
+    pure
+        RewriteConfig
+            { definition = def
+            , llvmApi = Nothing
+            , smtSolver
+            , varsToAvoid = mempty
+            , doTracing = NoCollectRewriteTraces
+            , logger = Logger $ const $ pure ()
+            , prettyModifiers = ModifiersRep @'[] Proxy
+            , mbMaxDepth = Nothing
+            , mbSimplify = Nothing
+            , cutLabels = []
+            , terminalLabels = []
+            }
+
 ----------------------------------------
 errorCases
     , rewriteSuccess
@@ -244,9 +265,8 @@ rulePriority =
 runWith :: Term -> IO (Either (RewriteFailed "Rewrite") (RewriteResult Pattern))
 runWith t =
     second fst <$> do
-        ns <- noSolver
-        runNoLoggingT $
-            runRewriteT NoCollectRewriteTraces def Nothing ns mempty mempty (rewriteStep [] [] $ Pattern_ t)
+        conf <- testConf
+        runNoLoggingT $ runRewriteT conf mempty (rewriteStep [] [] $ Pattern_ t)
 
 rewritesTo :: Term -> (Text, Term) -> IO ()
 t1 `rewritesTo` (lbl, t2) =
@@ -271,10 +291,10 @@ failsWith t err =
 
 runRewrite :: Term -> IO (Natural, RewriteResult Term)
 runRewrite t = do
-    ns <- noSolver
+    conf <- testConf
     (counter, _, res) <-
         runNoLoggingT $
-            performRewrite NoCollectRewriteTraces def Nothing ns mempty Nothing [] [] Nothing $
+            performRewrite conf $
                 Pattern_ t
     pure (counter, fmap (.term) res)
 
@@ -416,11 +436,9 @@ supportsDepthControl =
   where
     rewritesToDepth :: MaxDepth -> Steps -> Term -> t -> (t -> RewriteResult Term) -> IO ()
     rewritesToDepth (MaxDepth depth) (Steps n) t t' f = do
-        ns <- noSolver
+        conf <- testConf
         (counter, _, res) <-
-            runNoLoggingT $
-                performRewrite NoCollectRewriteTraces def Nothing ns mempty (Just depth) [] [] Nothing $
-                    Pattern_ t
+            runNoLoggingT $ performRewrite conf{mbMaxDepth = Just depth} $ Pattern_ t
         (counter, fmap (.term) res) @?= (n, f t')
 
 supportsCutPoints :: TestTree
@@ -471,10 +489,10 @@ supportsCutPoints =
   where
     rewritesToCutPoint :: Text -> Steps -> Term -> t -> (t -> RewriteResult Term) -> IO ()
     rewritesToCutPoint lbl (Steps n) t t' f = do
-        ns <- noSolver
+        conf <- testConf
         (counter, _, res) <-
             runNoLoggingT $
-                performRewrite NoCollectRewriteTraces def Nothing ns mempty Nothing [lbl] [] Nothing $
+                performRewrite conf{cutLabels = [lbl]} $
                     Pattern_ t
         (counter, fmap (.term) res) @?= (n, f t')
 
@@ -504,8 +522,7 @@ supportsTerminalRules =
   where
     rewritesToTerminal :: Text -> Steps -> Term -> t -> (t -> RewriteResult Term) -> IO ()
     rewritesToTerminal lbl (Steps n) t t' f = do
+        conf <- testConf
         (counter, _, res) <-
-            runNoLoggingT $ do
-                ns <- noSolver
-                performRewrite NoCollectRewriteTraces def Nothing ns mempty Nothing [] [lbl] Nothing $ Pattern_ t
+            runNoLoggingT $ performRewrite conf{terminalLabels = [lbl]} $ Pattern_ t
         (counter, fmap (.term) res) @?= (n, f t')