Trace rewrites

kore/src/Kore/Exec.hs

@@ -156,8 +156,7 @@ import Kore.Step.Search
     )
 import qualified Kore.Step.Search as Search
 import Kore.Step.Simplification.Data
-    ( MonadProf
-    , evalSimplifier
+    ( evalSimplifier
     )
 import qualified Kore.Step.Simplification.Data as Simplifier
 import qualified Kore.Step.Simplification.Pattern as Pattern
@@ -168,6 +167,7 @@ import Kore.Step.Simplification.Simplify
 import qualified Kore.Step.Strategy as Strategy
 import Kore.Step.Transition
     ( runTransitionT
+    , scatter
     )
 import Kore.Syntax.Module
     ( ModuleName
@@ -185,6 +185,7 @@ import Logic
     , observeAllT
     )
 import qualified Logic
+import Prof
 import SMT
     ( MonadSMT
     , SMT
@@ -236,7 +237,9 @@ exec depthLimit breadthLimit verifiedModule strategy initialTerm =
                     rewriteGroups = groupRewritesByPriority rewriteRules
                     transit instr config =
                         Strategy.transitionRule
-                            (transitionRule rewriteGroups strategy & trackExecDepth)
+                            (transitionRule rewriteGroups strategy
+                                & profTransitionRule
+                                & trackExecDepth)
                             instr
                             config
                         & runTransitionT
@@ -287,6 +290,24 @@ trackExecDepth transit prim (execDepth, execState) = do
     isRewrite Rewrite = True
     isRewrite _ = False
 
+{- | Add profiling markers to a 'TransitionRule'.
+-}
+profTransitionRule
+    :: forall monad rule state
+    .  MonadProf monad
+    => TransitionRule monad rule state
+    -> TransitionRule monad rule state
+profTransitionRule rule prim proofState =
+    case prim of
+        Rewrite -> Just ":rewrite:"
+        Simplify -> Just ":simplify:"
+        Begin -> Nothing
+    & \case
+        Just marker -> lift (traceProf marker (runTransitionT go)) >>= scatter
+        Nothing -> go
+  where
+    go = rule prim proofState
+
 -- | Project the value of the exit cell, if it is present.
 getExitCode
     :: forall simplifier
@@ -365,7 +386,8 @@ search depthLimit breadthLimit verifiedModule termLike searchPattern searchConfi
                     breadthLimit
                     -- search relies on exploring
                     -- the entire space of states.
-                    (transitionRule rewriteGroups All)
+                    (transitionRule rewriteGroups All
+                        & profTransitionRule)
                     (limitedExecutionStrategy depthLimit)
         executionGraph <-
             runStrategy' (Start $ mkRewritingPattern initialPattern)