Return rule-id's in execute response

library/Booster/JsonRpc.hs

@@ -41,7 +41,7 @@ import Numeric.Natural
 import Prettyprinter (pretty)
 import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs)
 
-import Booster.Definition.Attributes.Base (getUniqueId, uniqueId)
+import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
 import Booster.Definition.Base (KoreDefinition (..))
 import Booster.Definition.Base qualified as Definition (RewriteRule (..))
 import Booster.LLVM as LLVM (API)
@@ -543,9 +543,9 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
                     { reason = RpcTypes.Branching
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported
+                    , state = toExecState p originalSubstitution unsupported Nothing
                     , nextStates =
-                        Just $ map (\(_, _, p') -> toExecState p' originalSubstitution unsupported) $ toList nexts
+                        Just $ map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported muid) $ toList nexts
                     , rule = Nothing
                     , unknownPredicate = Nothing
                     }
@@ -556,7 +556,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
                     { reason = RpcTypes.Stuck
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported
+                    , state = toExecState p originalSubstitution unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -568,43 +568,43 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
                     { reason = RpcTypes.Vacuous
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported
+                    , state = toExecState p originalSubstitution unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
                     }
-    RewriteCutPoint lbl _ p next ->
+    RewriteCutPoint lbl muid p next ->
         Right $
             RpcTypes.Execute
                 RpcTypes.ExecuteResult
                     { reason = RpcTypes.CutPointRule
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported
-                    , nextStates = Just [toExecState next originalSubstitution unsupported]
+                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , nextStates = Just [toExecState next originalSubstitution unsupported muid]
                     , rule = Just lbl
                     , unknownPredicate = Nothing
                     }
-    RewriteTerminal lbl _ p ->
+    RewriteTerminal lbl muid p ->
         Right $
             RpcTypes.Execute
                 RpcTypes.ExecuteResult
                     { reason = RpcTypes.TerminalRule
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported
+                    , state = toExecState p originalSubstitution unsupported muid
                     , nextStates = Nothing
                     , rule = Just lbl
                     , unknownPredicate = Nothing
                     }
-    RewriteFinished _ _ p ->
+    RewriteFinished _ muid p ->
         Right $
             RpcTypes.Execute
                 RpcTypes.ExecuteResult
                     { reason = RpcTypes.DepthBound
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported
+                    , state = toExecState p originalSubstitution unsupported muid
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -622,7 +622,7 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
                                     (logSuccessfulSimplifications, logFailedSimplifications)
                                     (RewriteStepFailed failure)
                          in logs <|> abortRewriteLog
-                    , state = toExecState p originalSubstitution unsupported
+                    , state = toExecState p originalSubstitution unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -650,15 +650,16 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
                 (Nothing, xs@(_ : _)) -> Just xs
                 (Just t, xs) -> Just (t : xs)
 
-toExecState :: Pattern -> Map Variable Term -> [Syntax.KorePattern] -> RpcTypes.ExecuteState
-toExecState pat sub unsupported =
+toExecState ::
+    Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
+toExecState pat sub unsupported muid =
     RpcTypes.ExecuteState
         { term = addHeader t
         , predicate = addHeader <$> addUnsupported p
         , substitution = addHeader <$> s
         , ruleSubstitution = Nothing
         , rulePredicate = Nothing
-        , ruleId = Nothing
+        , ruleId = getUniqueId <$> muid
         }
   where
     (t, p, s) = externalisePattern pat sub
@@ -826,7 +827,7 @@ mkLogRewriteTrace
                     let final = singleton $ case failure of
                             ApplyEquations.IndexIsNone trm ->
                                 Simplification
-                                    { originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ trm) mempty mempty
+                                    { originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ trm) mempty mempty Nothing
                                     , originalTermIndex = Nothing
                                     , origin = Booster
                                     , result = Failure{reason = "No index found for term", _ruleId = Nothing}

test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response

@@ -1 +1 @@
-{"jsonrpc":"2.0","id":1,"result":{"reason":"depth-bound","depth":2,"state":{"term":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'-LT-'generatedTop'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'k'-GT-'","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortState","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortState","args":[]},"value":"e"}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]},{"tag":"App","name":"Lbl'-LT-'generatedCounter'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]}}}}}
+{"jsonrpc":"2.0","id":1,"result":{"reason":"depth-bound","depth":2,"state":{"term":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'-LT-'generatedTop'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'T'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'k'-GT-'","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortState","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortState","args":[]},"value":"e"}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]},{"tag":"App","name":"Lbl'-LT-'val'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]},{"tag":"App","name":"Lbl'-LT-'generatedCounter'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]}}}}}

test/jsonrpc-examples/expected/depth-limit.execute.response@terminal.execute.response

@@ -5,4 +5,9 @@ Files test/jsonrpc-examples/depth-limit.execute.response and test/jsonrpc-exampl
 >     "reason": "terminal-rule",
 3a4
 >     "rule": "TEST.DE",
+101c102,103
+<         }
+---
+>         },
+>         "rule-id": "a042e8abc8a92dc1a4c0bf0ca8b14a266a049cca42cb03da291f8a960978f859"
 

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@terminal.execute.response

@@ -5,4 +5,9 @@ Files test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response and
 >     "reason": "terminal-rule",
 3a4
 >     "rule": "TEST.DE",
+101c102,103
+<         }
+---
+>         },
+>         "rule-id": "a042e8abc8a92dc1a4c0bf0ca8b14a266a049cca42cb03da291f8a960978f859"
 

test/jsonrpc-examples/expected/terminal.execute.response@depth-limit.execute.response

@@ -5,4 +5,9 @@ Files test/jsonrpc-examples/terminal.execute.response and test/jsonrpc-examples/
 >     "reason": "depth-bound",
 4d3
 <     "rule": "TEST.DE",
+102,103c101
+<         },
+<         "rule-id": "a042e8abc8a92dc1a4c0bf0ca8b14a266a049cca42cb03da291f8a960978f859"
+---
+>         }
 

test/jsonrpc-examples/expected/terminal.execute.response@depth-limit.spaghetti-formatted.execute.response

@@ -5,4 +5,9 @@ Files test/jsonrpc-examples/terminal.execute.response and test/jsonrpc-examples/
 >     "reason": "depth-bound",
 4d3
 <     "rule": "TEST.DE",
+102,103c101
+<         },
+<         "rule-id": "a042e8abc8a92dc1a4c0bf0ca8b14a266a049cca42cb03da291f8a960978f859"
+---
+>         }
 

test/jsonrpc-examples/state-a.spaghetti-formatted.kore.json

@@ -1 +1 @@
-{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'-LT-'generatedTop'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'k'-GT-'","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortState","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortState","args":[]},"value":"a"}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]},{"tag":"App","name":"Lbl'-LT-'generatedCounter'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]}}
+{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'-LT-'generatedTop'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'T'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'k'-GT-'","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortState","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortState","args":[]},"value":"a"}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]},{"tag":"App","name":"Lbl'-LT-'val'-GT-'","sorts":[],"args":[{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]},{"tag":"App","name":"Lbl'-LT-'generatedCounter'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]}}