Kore.Reachability: decouple result type of applyClaims and applyAxioms (#2200)

* Kore.Reachability: use ApplyResult

* ApplyResult: add ReachedBottom case; clean-up

* Clean-up

* rewrite rule application strategy: remove case handling for when result is bottom

* ApplyResult: documentation

* AppliedRule: short documentation

* applyResultToClaimState: factor out case handling in transitionRule

* deriveResults: handle bottom case

Author: ana-pantilie

kore/src/Kore/Reachability/AllPathClaim.hs

@@ -39,10 +39,6 @@ import Kore.Internal.TermLike
     )
 import qualified Kore.Internal.TermLike as TermLike
 import Kore.Reachability.Claim
-import Kore.Reachability.ClaimState
-    ( ClaimState (..)
-    , retractRewritable
-    )
 import Kore.Rewriting.RewritingVariable
     ( RewritingVariableName
     , mkRuleVariable
@@ -141,19 +137,19 @@ instance Claim AllPathClaim where
     applyClaims claims = deriveSeqClaim _Unwrapped AllPathClaim claims
 
     applyAxioms axiomss = \claim ->
-        foldM applyAxioms1 (Remaining claim) axiomss
+        foldM applyAxioms1 (ApplyRemainder claim) axiomss
       where
-        applyAxioms1 claimState axioms
-          | Just claim <- retractRewritable claimState =
+        applyAxioms1 applied axioms
+          | Just claim <- retractApplyRemainder applied =
             deriveParAxiomAllPath axioms claim
             >>= simplifyRemainder
           | otherwise =
-            pure claimState
+            pure applied
 
-        simplifyRemainder claimState =
-            case claimState of
-                Remaining claim -> Remaining <$> simplify claim
-                _ -> return claimState
+        simplifyRemainder applied =
+            case applied of
+                ApplyRemainder claim -> ApplyRemainder <$> simplify claim
+                _ -> return applied
 
 instance From (Rule AllPathClaim) Attribute.PriorityAttributes where
     from = from @(RewriteRule _) . unRuleAllPath
@@ -195,7 +191,7 @@ deriveParAxiomAllPath
     =>  [Rule AllPathClaim]
     ->  AllPathClaim
     ->  TransitionT (AppliedRule AllPathClaim) simplifier
-            (ClaimState AllPathClaim)
+            (ApplyResult AllPathClaim)
 deriveParAxiomAllPath rules =
     derivePar' _Unwrapped AllPathRewriteRule rewrites
   where

kore/src/Kore/Reachability/Claim.hs

@@ -4,7 +4,9 @@ License     : NCSA
 -}
 module Kore.Reachability.Claim
     ( Claim (..)
+    , ApplyResult (..)
     , AppliedRule (..)
+    , retractApplyRemainder
     , strategy
     , TransitionRule
     , Prim
@@ -110,7 +112,6 @@ import Kore.Log.WarnStuckClaimState
 import Kore.Reachability.ClaimState hiding
     ( claimState
     )
-import qualified Kore.Reachability.ClaimState as ClaimState
 import Kore.Reachability.Prim
 import Kore.Rewriting.RewritingVariable
 import Kore.Step.AxiomPattern
@@ -182,30 +183,32 @@ class Claim claim where
         => claim
         -> Strategy.TransitionT (AppliedRule claim) m claim
 
-    {- TODO (thomas.tuegel): applyClaims and applyAxioms should return:
-
-    > data ApplyResult claim
-    >     = ApplyRewritten !claim
-    >     | ApplyRemainder !claim
-
-    Rationale: ClaimState is part of the implementation of transitionRule, that
-    is: these functions have hidden knowledge of how transitionRule works
-    because they tell it what to do next. Instead, they should report their
-    result and leave the decision up to transitionRule.
-
-    -}
     applyClaims
         :: MonadSimplify m
         => [claim]
         -> claim
-        -> Strategy.TransitionT (AppliedRule claim) m (ClaimState claim)
+        -> Strategy.TransitionT (AppliedRule claim) m (ApplyResult claim)
 
     applyAxioms
         :: MonadSimplify m
         => [[Rule claim]]
         -> claim
-        -> Strategy.TransitionT (AppliedRule claim) m (ClaimState claim)
+        -> Strategy.TransitionT (AppliedRule claim) m (ApplyResult claim)
+
+{- | 'ApplyResult' is the result of a rewriting step, like 'applyClaims' or 'applyAxioms'.
 
+    Both 'ApplyRewritten' and 'ApplyRemainder' wrap a newly formed claim.
+    Its left hand side is constructed from either the application of rewrite rules,
+    or, respectively, from the remainder resulting after this procedure.
+-}
+data ApplyResult claim
+    = ApplyRewritten !claim
+    | ApplyRemainder !claim
+    deriving (Show, Eq)
+    deriving (Functor)
+
+{- | 'AppliedRule' represents the rule applied during a rewriting step.
+-}
 data AppliedRule claim
     = AppliedAxiom (Rule claim)
     | AppliedClaim claim
@@ -271,7 +274,7 @@ deriveSeqClaim
     -> (ClaimPattern -> claim)
     -> [claim]
     -> claim
-    -> Strategy.TransitionT (AppliedRule claim) m (ClaimState claim)
+    -> Strategy.TransitionT (AppliedRule claim) m (ApplyResult claim)
 deriveSeqClaim lensClaimPattern mkClaim claims claim =
     getCompose
     $ Lens.forOf lensClaimPattern claim
@@ -336,32 +339,30 @@ transitionRule claims axiomGroups = transitionRuleWorker
               | otherwise -> pure (Claimed a)
       | otherwise = pure claimState
 
-    -- TODO (virgil): Wrap the results in GoalRemainder/GoalRewritten here.
-    --
-    -- thomas.tuegel: "Here" is in ApplyClaims and ApplyAxioms.
-    --
-    -- Note that in most transitions it is obvious what is being transformed
-    -- into what, e.g. that a `ResetGoal` transition transforms
-    -- `GoalRewritten` into `Goal`. However, here we're taking a `Goal`
-    -- and transforming it into `GoalRewritten` and `GoalRemainder` in an
-    -- opaque way. I think that there's no good reason for wrapping the
-    -- results in `derivePar` as opposed to here.
-
     transitionRuleWorker ApplyClaims (Claimed claim) =
         applyClaims claims claim
+        >>= return . applyResultToClaimState
     transitionRuleWorker ApplyClaims claimState = pure claimState
 
     transitionRuleWorker ApplyAxioms claimState
       | Just claim <- retractRewritable claimState =
         applyAxioms axiomGroups claim
+        >>= return . applyResultToClaimState
       | otherwise = pure claimState
 
+    applyResultToClaimState (ApplyRewritten a) = Rewritten a
+    applyResultToClaimState (ApplyRemainder a) = Remaining a
+
 retractSimplifiable :: ClaimState a -> Maybe a
 retractSimplifiable (Claimed a) = Just a
 retractSimplifiable (Rewritten a) = Just a
 retractSimplifiable (Remaining a) = Just a
 retractSimplifiable _ = Nothing
 
+retractApplyRemainder :: ApplyResult a -> Maybe a
+retractApplyRemainder (ApplyRemainder a) = Just a
+retractApplyRemainder _ = Nothing
+
 isRemainder :: ClaimState a -> Bool
 isRemainder (Remaining _) = True
 isRemainder _ = False
@@ -650,7 +651,7 @@ derivePar'
     -> (RewriteRule RewritingVariableName -> Rule claim)
     -> [RewriteRule RewritingVariableName]
     -> claim
-    -> Strategy.TransitionT (AppliedRule claim) m (ClaimState claim)
+    -> Strategy.TransitionT (AppliedRule claim) m (ApplyResult claim)
 derivePar' lensRulePattern mkRule =
     deriveWith lensRulePattern mkRule
     $ Step.applyRewriteRulesParallel Unification.unificationProcedure
@@ -669,7 +670,7 @@ deriveWith
     -> Deriver m
     -> [RewriteRule RewritingVariableName]
     -> claim
-    -> Strategy.TransitionT (AppliedRule claim) m (ClaimState claim)
+    -> Strategy.TransitionT (AppliedRule claim) m (ApplyResult claim)
 deriveWith lensClaimPattern mkRule takeStep rewrites claim =
     getCompose
     $ Lens.forOf lensClaimPattern claim
@@ -694,7 +695,7 @@ deriveSeq'
     -> (RewriteRule RewritingVariableName -> Rule claim)
     -> [RewriteRule RewritingVariableName]
     -> claim
-    -> Strategy.TransitionT (AppliedRule claim) m (ClaimState claim)
+    -> Strategy.TransitionT (AppliedRule claim) m (ApplyResult claim)
 deriveSeq' lensRulePattern mkRule =
     deriveWith lensRulePattern mkRule . flip
     $ Step.applyRewriteRulesSequence Unification.unificationProcedure
@@ -704,7 +705,7 @@ deriveResults
     => (Step.UnifiedRule representation -> AppliedRule claim)
     -> Step.Results representation
     -> Strategy.TransitionT (AppliedRule claim) simplifier
-        (ClaimState.ClaimState (Pattern RewritingVariableName))
+        (ApplyResult (Pattern RewritingVariableName))
 -- TODO (thomas.tuegel): Remove claim argument.
 deriveResults fromAppliedRule Results { results, remainders } =
     addResults <|> addRemainders
@@ -715,13 +716,10 @@ deriveResults fromAppliedRule Results { results, remainders } =
     addResult Result { appliedRule, result } = do
         addRule appliedRule
         case Foldable.toList result of
-            []      ->
-                -- If the rule returns \bottom, the claim is proven on the
-                -- current branch.
-                pure Proven
+            [] -> addRewritten Pattern.bottom
             configs -> Foldable.asum (addRewritten <$> configs)
 
-    addRewritten = pure . Rewritten
-    addRemainder = pure . Remaining
+    addRewritten = pure . ApplyRewritten
+    addRemainder = pure . ApplyRemainder
 
     addRule = Transition.addRule . fromAppliedRule

kore/src/Kore/Reachability/OnePathClaim.hs

@@ -36,9 +36,6 @@ import Kore.Internal.TermLike
     )
 import qualified Kore.Internal.TermLike as TermLike
 import Kore.Reachability.Claim
-import Kore.Reachability.ClaimState
-    ( ClaimState
-    )
 import Kore.Rewriting.RewritingVariable
     ( RewritingVariableName
     , mkRuleVariable
@@ -214,7 +211,7 @@ deriveSeqAxiomOnePath
     =>  [Rule OnePathClaim]
     ->  OnePathClaim
     ->  TransitionT (AppliedRule OnePathClaim) simplifier
-            (ClaimState OnePathClaim)
+            (ApplyResult OnePathClaim)
 deriveSeqAxiomOnePath rules =
     deriveSeq' _Unwrapped OnePathRewriteRule rewrites
   where

kore/test/Test/Kore/Reachability/MockAllPath.hs

@@ -32,6 +32,7 @@ import Kore.Debug
 import qualified Kore.Internal.MultiOr as MultiOr
 import Kore.Reachability.Claim
     ( AppliedRule (..)
+    , ApplyResult (..)
     , Claim (..)
     )
 import qualified Kore.Reachability.Claim as Claim
@@ -381,16 +382,16 @@ derivePar
     :: (MockClaim -> MockAppliedRule)
     -> [MockRule]
     -> MockClaim
-    -> Transition.TransitionT MockAppliedRule m MockClaimState
+    -> Transition.TransitionT MockAppliedRule m (ApplyResult MockClaim)
 derivePar mkAppliedRule rules (MockClaim (src, dst)) =
     goals <|> goalRemainder
   where
     goal (Rule rule@(_, to)) = do
         Transition.addRule (mkAppliedRule (MockClaim rule))
-        (pure . ClaimState.Rewritten . MockClaim) (to, dst)
+        (pure . ApplyRewritten . MockClaim) (to, dst)
     goalRemainder = do
         let r = Foldable.foldl' difference src (fst . unRule <$> applied)
-        (pure . ClaimState.Remaining . MockClaim) (r, dst)
+        (pure . ApplyRemainder . MockClaim) (r, dst)
     applyRule rule@(Rule (fromMockClaim, _))
         | fromMockClaim `matches` src = Just rule
         | otherwise = Nothing