#3143 rewrite graph traversal + output unexplored leaves (#3168)

* Rewrite of graph traversal used by Kore.Exec and Kore.Reachability.Prove

New traversal models required functionality in data types rather than
using exceptions and monad stack layers to add functionality.

The `graphTraversal` function operates with a list of "steps"
(sequences of "instructions") that take a configuration to a result
containing new configurations.

The traversal is parameterised with a specific transition function
`([Step instr],config) -> m (TransitionResult ([Step instr],config))`
which interprets step results. `TransitionResult` can indicate to
continue with one (`Continuing`) or more (`Branch`) new
configurations, or that the configuration is final, stuck, or should
be stopped.

One reason to stop is when the list of steps runs empty, other reasons
could be to stop execuction on the application of certain rules.

The transition function can be constructed from one that operates on
the primitive instructions, together with an interpretation function
that differs depending on the use case (proving or executing).

* Introduce named type for ([Step instr], config) (TState), document behaviour better

* refactor Kore.Exec.exec for readability

* update ghc923 nix configuration

Command

> nix run .#update-cabal-ghc9

* Overall documentation attached to graphTraversal

* adapt Simplifier imports

Author: jberthold

flake.lock

@@ -313,6 +313,7 @@ library
     Kore.Equation.Validate
     Kore.Error
     Kore.Exec
+    Kore.Exec.GraphTraversal
     Kore.IndexedModule.Error
     Kore.IndexedModule.IndexedModule
     Kore.IndexedModule.MetadataTools

kore/kore.cabal

@@ -40,8 +40,9 @@ import Control.Monad.Trans.Maybe (runMaybeT)
 import Data.Coerce (
     coerce,
  )
-import Data.Limit (
+import Data.Limit as Limit (
     Limit (..),
+    takeWithin,
  )
 import Data.List (
     tails,
@@ -69,6 +70,7 @@ import Kore.Equation qualified as Equation (
     argument,
     requires,
  )
+import Kore.Exec.GraphTraversal qualified as GraphTraversal
 import Kore.IndexedModule.IndexedModule (
     IndexedModule (..),
     VerifiedModule,
@@ -168,7 +170,6 @@ import Kore.Rewrite.Search (
     searchGraph,
  )
 import Kore.Rewrite.Search qualified as Search
-import Kore.Rewrite.Strategy (FinalNodeType (Leaf))
 import Kore.Rewrite.Strategy qualified as Strategy
 import Kore.Rewrite.Transition (
     runTransitionT,
@@ -278,44 +279,30 @@ exec
         , overloadGraph
         , metadataTools
         , verifiedModule
-        , rewrites
+        , rewrites = Initialized{rewriteRules}
         , equations
         }
-    strategy
+    execMode
     (mkRewritingTerm -> initialTerm) =
         evalSimplifier simplifierx verifiedModule' sortGraph overloadGraph metadataTools equations $ do
-            let Initialized{rewriteRules} = rewrites
             finals <-
-                getFinalConfigsOf $ do
-                    initialConfig <-
-                        Pattern.simplify
-                            (Pattern.fromTermLike initialTerm)
-                            >>= Logic.scatter
-                    let updateQueue = \as ->
-                            Strategy.unfoldDepthFirst as
-                                >=> lift
-                                    . Strategy.applyBreadthLimit
-                                        breadthLimit
-                                        dropStrategy
-                        rewriteGroups = groupRewritesByPriority rewriteRules
-                        transit instr config =
-                            Strategy.transitionRule
-                                ( transitionRule rewriteGroups strategy
-                                    & profTransitionRule
-                                    & trackExecDepth
-                                )
-                                instr
-                                config
-                                & runTransitionT
-                                & fmap (map fst)
-                                & lift
-                    Strategy.leavesM
-                        Leaf
-                        updateQueue
-                        (unfoldTransition transit)
-                        ( limitedExecutionStrategy depthLimit
-                        , (ExecDepth 0, Start initialConfig)
-                        )
+                GraphTraversal.graphTraversal
+                    Strategy.Leaf
+                    Strategy.DepthFirst
+                    breadthLimit
+                    transit
+                    Limit.Unlimited
+                    execStrategy
+                    (ExecDepth 0, Start $ Pattern.fromTermLike initialTerm)
+                    >>= \case
+                        GraphTraversal.Ended results -> pure results
+                        GraphTraversal.GotStuck n results -> do
+                            when (n == 0 && any (notStuck . snd) results) $
+                                forM_ depthLimit warnDepthLimitExceeded
+                            pure results
+                        GraphTraversal.Aborted _ results -> do
+                            pure results
+
             let (depths, finalConfigs) = unzip finals
             infoExecDepth (maximum (ExecDepth 0 : depths))
             let finalConfigs' =
@@ -328,17 +315,60 @@ exec
                         & sameTermLikeSort initialSort
             return (exitCode, finalTerm)
       where
-        dropStrategy = snd
-        getFinalConfigsOf act = observeAllT $ fmap snd act
         verifiedModule' =
             IndexedModule.mapAliasPatterns
                 -- TODO (thomas.tuegel): Move this into Kore.Builtin
                 (Builtin.internalize metadataTools)
                 verifiedModule
         initialSort = termLikeSort initialTerm
-        unfoldTransition transit (instrs, config) = do
-            when (null instrs) $ forM_ depthLimit warnDepthLimitExceeded
-            Strategy.unfoldTransition transit (instrs, config)
+
+        execStrategy :: [GraphTraversal.Step Prim]
+        execStrategy =
+            Limit.takeWithin depthLimit $
+                [Begin, Simplify, Rewrite, Simplify] :
+                repeat [Begin, Rewrite, Simplify]
+
+        transit ::
+            GraphTraversal.TState
+                Prim
+                (ExecDepth, ProgramState (Pattern RewritingVariableName)) ->
+            Simplifier.Simplifier
+                ( GraphTraversal.TransitionResult
+                    ( GraphTraversal.TState
+                        Prim
+                        (ExecDepth, ProgramState (Pattern RewritingVariableName))
+                    )
+                )
+        transit =
+            GraphTraversal.simpleTransition
+                ( trackExecDepth . profTransitionRule $
+                    transitionRule (groupRewritesByPriority rewriteRules) execMode
+                )
+                toTransitionResult
+
+        toTransitionResult ::
+            (ExecDepth, ProgramState p) ->
+            [(ExecDepth, ProgramState p)] ->
+            ( GraphTraversal.TransitionResult
+                (ExecDepth, ProgramState p)
+            )
+        toTransitionResult prior [] =
+            case snd prior of
+                Start _ -> GraphTraversal.Stopped [prior]
+                Rewritten _ -> GraphTraversal.Stopped [prior]
+                Remaining _ -> GraphTraversal.Stuck prior
+                Kore.Rewrite.Bottom -> GraphTraversal.Stuck prior
+        toTransitionResult _prior [next] =
+            case snd next of
+                Start _ -> GraphTraversal.Continuing next
+                Rewritten _ -> GraphTraversal.Continuing next
+                Remaining _ -> GraphTraversal.Stuck next
+                Kore.Rewrite.Bottom -> GraphTraversal.Stuck next
+        toTransitionResult prior (s : ss) =
+            GraphTraversal.Branch prior (s :| ss)
+
+        notStuck :: ProgramState a -> Bool
+        notStuck = isJust . extractProgramState
 
 -- | Modify a 'TransitionRule' to track the depth of the execution graph.
 trackExecDepth ::
@@ -494,7 +524,7 @@ prove ::
     Limit Natural ->
     Limit Natural ->
     Natural ->
-    FinalNodeType ->
+    Strategy.FinalNodeType ->
     -- | The main module
     VerifiedModule StepperAttributes ->
     -- | The spec module