From 5d58fc0b1a199460db2338e638f0800f950d6ac9 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 16 Jan 2024 09:36:28 +0100 Subject: [PATCH 1/2] 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 --- library/Booster/Pattern/Rewrite.hs | 19 +++---- .../response-one-ques.booster-dev | 2 +- .../response-two-ques-external.booster-dev | 2 +- ...two-ques-internal-with-counter.booster-dev | 2 +- .../response-two-ques-internal.booster-dev | 2 +- unit-tests/Test/Booster/Pattern/Rewrite.hs | 50 +++++++++---------- 6 files changed, 38 insertions(+), 39 deletions(-) diff --git a/library/Booster/Pattern/Rewrite.hs b/library/Booster/Pattern/Rewrite.hs index 572855f44..472eb2c7c 100644 --- 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 index b1e97aa4a..8852423b9 100644 --- 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 index 88f12b1a7..eb9ba3ab3 100644 --- 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/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev b/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev index ffe77029d..a9f0ed474 100644 --- a/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev +++ b/test/rpc-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 index 9386063fe..a450b120f 100644 --- 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 index 371e4f423..94ade81ca 100644 --- 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 From 964ae5d6ff465499ca8d7fb55ef7283da152ae3c Mon Sep 17 00:00:00 2001 From: github-actions Date: Tue, 16 Jan 2024 09:26:50 +0000 Subject: [PATCH 2/2] Format with fourmolu --- unit-tests/Test/Booster/Pattern/Rewrite.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/unit-tests/Test/Booster/Pattern/Rewrite.hs b/unit-tests/Test/Booster/Pattern/Rewrite.hs index 94ade81ca..2005c5393 100644 --- a/unit-tests/Test/Booster/Pattern/Rewrite.hs +++ b/unit-tests/Test/Booster/Pattern/Rewrite.hs @@ -321,7 +321,8 @@ canRewrite = [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{} ) ) |] + getsStuck + [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( \and{SomeSort{}}( con1{}( \dv{SomeSort{}}("thing") ), con2{}( \dv{SomeSort{}}("thing") ) ) ), C:SortK{} ) ) |] ] abortsOnErrors :: TestTree