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 · 5d58fc0 · 5d58fc0
1 parent 98e9b26
commit 5d58fc0
Show file tree

Hide file tree

Showing 6 changed files with 38 additions and 39 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": {

diff --git a/unit-tests/Test/Booster/Pattern/Rewrite.hs b/unit-tests/Test/Booster/Pattern/Rewrite.hs
@@ -182,22 +182,6 @@ errorCases =
             [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con2{}( \dv{SomeSort{}}("thing") ) ), Thing:SortK{}) ) |]
                 `failsWith` NoRulesForTerm
                     [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con2{}( \dv{SomeSort{}}("thing") ) ), Thing:SortK{}) ) |]
-        , testCase "Index is None" $ do
-            let t =
-                    [trm|
-                        kCell{}(
-                            kseq{}(
-                                inj{SomeSort{}, SortKItem{}}(
-                                    \and{SomeSort{}}(
-                                        con1{}( \dv{SomeSort{}}("thing") ),
-                                        con2{}( \dv{SomeSort{}}("thing") )
-                                    )
-                                ),
-                                Thing:SortK{}
-                            )
-                        )
-                    |]
-            t `failsWith` TermIndexIsNone t
         ]
 rewriteSuccess =
     testCase "con1 app rewrites to f1 app" $
@@ -222,10 +206,28 @@ definednessUnclear =
                 [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
         pcon4 `failsWith` DefinednessUnclear rule4 (Pattern_ pcon4) [UndefinedSymbol "f2"]
 rewriteStuck =
-    testCase "con3 app is stuck (no rules apply)" $ do
-        let con3App =
-                [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
-        getsStuck con3App
+    testGroup
+        "Stuck terms"
+        [ testCase "con3 app is stuck (no rules apply)" $ do
+            let con3App =
+                    [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
+            getsStuck con3App
+        , testCase "Index is None" $ do
+            getsStuck
+                [trm|
+                        kCell{}(
+                            kseq{}(
+                                inj{SomeSort{}, SortKItem{}}(
+                                    \and{SomeSort{}}(
+                                        con1{}( \dv{SomeSort{}}("thing") ),
+                                        con2{}( \dv{SomeSort{}}("thing") )
+                                    )
+                                ),
+                                Thing:SortK{}
+                            )
+                        )
+                    |]
+        ]
 rulePriority =
     testCase "con1 rewrites to a branch when higher priority does not apply" $
         [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("otherThing") ) ), ConfigVar:SortK{}) ) |]
@@ -318,6 +320,8 @@ canRewrite =
                 [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |]
                 [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing") ) ), C:SortK{}) ) |]
                 RewriteStuck
+        , testCase "Returns stuck when term index is None" $
+            getsStuck [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( \and{SomeSort{}}( con1{}( \dv{SomeSort{}}("thing") ), con2{}( \dv{SomeSort{}}("thing") ) ) ), C:SortK{} ) ) |]
         ]
 
 abortsOnErrors :: TestTree
@@ -326,12 +330,6 @@ abortsOnErrors =
         "Aborts rewrite when there is an error"
         [ testCase "when there are no rules at all" $
             let term = app con2 [d] in aborts (NoRulesForTerm term) term
-        , testCase "when the term index is None" $
-            let term =
-                    [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( \and{SomeSort{}}( con1{}( \dv{SomeSort{}}("thing") ), con2{}( \dv{SomeSort{}}("thing") ) ) ), C:SortK{} ) ) |]
-             in aborts
-                    (TermIndexIsNone term)
-                    term
         ]
 
 callsError :: TestTree