Trace rewrites (#2339)

Fixes #2331 

- Adding new `profTransitionRule` rule, analogous to `Kore.Reachability.Prove.profTransitionRule`, which adds profile tracing for rewrites.
- Wrapping two invocations of `transitionRule` in `Kore.Exec` with this new function.

---

###### Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

-   [x] **Summary.** Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
-   [x] **Documentation.** Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
-   [ ] **Tests.** Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
-   [x] **Clean up.** The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

Author: emarzion

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)