Report rewrite as stuck when term index is none

Previously we have thrown an exception here which resulted in an Aborted, rather than a Stuck result
runtimeverification · Jan 16, 2024 · 457177d · 457177d
1 parent 98e9b26
commit 457177d
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 13 deletions.
diff --git a/library/Booster/Pattern/Rewrite.hs b/library/Booster/Pattern/Rewrite.hs
@@ -98,22 +98,23 @@ rewriteStep ::
     Pattern ->
     RewriteT io (RewriteFailed "Rewrite") (RewriteResult Pattern)
 rewriteStep cutLabels terminalLabels pat = do
-    let termIdx = kCellTermIndex pat.term
-    when (termIdx == None) $ throw (TermIndexIsNone pat.term)
     def <- getDefinition
-    let idxRules = fromMaybe Map.empty $ Map.lookup termIdx def.rewriteTheory
+    let termIdx = kCellTermIndex pat.term
+        idxRules = fromMaybe Map.empty $ Map.lookup termIdx def.rewriteTheory
         anyRules = fromMaybe Map.empty $ Map.lookup Anything def.rewriteTheory
         rules =
             map snd . Map.toAscList $
                 if termIdx == Anything
                     then idxRules
                     else Map.unionWith (<>) idxRules anyRules
-
-    when (null rules) $ throw (NoRulesForTerm pat.term)
-
-    -- process one priority group at a time (descending priority),
-    -- until a result is obtained or the entire rewrite fails.
-    processGroups pat rules
+    case termIdx of
+        None -> pure (RewriteStuck pat)
+        _ -> do
+            when (null rules) $ throw (NoRulesForTerm pat.term)
+
+            -- process one priority group at a time (descending priority),
+            -- until a result is obtained or the entire rewrite fails.
+            processGroups pat rules
   where
     processGroups ::
         MonadLoggerIO io =>

diff --git a/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev b/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev
@@ -2,7 +2,7 @@
     "jsonrpc": "2.0",
     "id": 1,
     "result": {
-        "reason": "aborted",
+        "reason": "stuck",
         "depth": 1,
         "state": {
             "term": {

diff --git a/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev b/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev
@@ -2,7 +2,7 @@
     "jsonrpc": "2.0",
     "id": 1,
     "result": {
-        "reason": "aborted",
+        "reason": "stuck",
         "depth": 1,
         "state": {
             "term": {

diff --git a/...pc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev b/...pc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev
@@ -2,7 +2,7 @@
     "jsonrpc": "2.0",
     "id": 1,
     "result": {
-        "reason": "aborted",
+        "reason": "stuck",
         "depth": 2,
         "state": {
             "term": {

diff --git a/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev b/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev
@@ -2,7 +2,7 @@
     "jsonrpc": "2.0",
     "id": 1,
     "result": {
-        "reason": "aborted",
+        "reason": "stuck",
         "depth": 2,
         "state": {
             "term": {