Remove DerivePar and DeriveSeq

Author: ttuegel

kore/src/Kore/Log/DebugProofState.hs

@@ -9,10 +9,8 @@ module Kore.Log.DebugProofState
 
 import Prelude.Kore
 
-import Kore.Rewriting.RewritingVariable
 import Kore.Step.RulePattern
     ( ReachabilityRule (..)
-    , RewriteRule (..)
     )
 import Kore.Strategies.ProofState
     ( Prim (..)
@@ -27,7 +25,7 @@ import qualified Pretty
 data DebugProofState =
     DebugProofState
         { proofState :: ProofState ReachabilityRule
-        , transition :: Prim (RewriteRule RewritingVariableName)
+        , transition :: Prim
         , result :: Maybe (ProofState ReachabilityRule)
         }
     deriving (Show)
@@ -44,14 +42,10 @@ instance Pretty DebugProofState where
             [ "Reached proof state with the following configuration:"
             , Pretty.indent 4 (pretty proofState)
             , "On which the following transition applies:"
-            , Pretty.indent 4 (prettyTransition transition)
+            , Pretty.indent 4 (pretty transition)
             , "Resulting in:"
             , Pretty.indent 4 (maybe "Terminal state." pretty result)
             ]
-      where
-        prettyTransition (DeriveSeq _) = "Transition DeriveSeq."
-        prettyTransition (DerivePar _) = "Transition DerivePar."
-        prettyTransition prim          = Pretty.pretty prim
 
 instance Entry DebugProofState where
     entrySeverity _ = Debug

kore/src/Kore/Strategies/Goal.hs

@@ -150,8 +150,7 @@ import Kore.Step.Transition
     )
 import qualified Kore.Step.Transition as Transition
 import Kore.Strategies.ProofState hiding
-    ( Prim
-    , proofState
+    ( proofState
     )
 import qualified Kore.Strategies.ProofState as ProofState
 import Kore.Strategies.Rule
@@ -190,8 +189,6 @@ proven
     -> Bool
 proven = Foldable.null . unprovenNodes
 
-type Prim goal = ProofState.Prim (Rule goal)
-
 class Goal goal where
     goalToRule :: goal -> Rule goal
     default goalToRule
@@ -203,7 +200,7 @@ class Goal goal where
         :: goal
         -> [goal]
         -> [Rule goal]
-        -> Stream (Strategy (Prim goal))
+        -> Stream (Strategy Prim)
 
     isTriviallyValid :: goal -> Bool
 
@@ -468,18 +465,16 @@ instance Goal ReachabilityRule where
         :: ReachabilityRule
         -> [ReachabilityRule]
         -> [Rule ReachabilityRule]
-        -> Stream (Strategy (Prim ReachabilityRule))
+        -> Stream (Strategy Prim)
     strategy goal claims axioms =
         case goal of
             OnePath rule ->
-                reachabilityOnePathStrategy
-                $ strategy
+                strategy
                     rule
                     (mapMaybe maybeOnePath claims)
                     (fmap ruleReachabilityToRuleOnePath axioms)
             AllPath rule ->
-                reachabilityAllPathStrategy
-                $ strategy
+                strategy
                     rule
                     (mapMaybe maybeAllPath claims)
                     (fmap ruleReachabilityToRuleAllPath axioms)
@@ -511,24 +506,6 @@ maybeAllPath :: ReachabilityRule -> Maybe AllPathRule
 maybeAllPath (AllPath rule) = Just rule
 maybeAllPath _ = Nothing
 
-reachabilityOnePathStrategy
-    :: Functor t
-    => t (Strategy (Prim OnePathRule))
-    -> t (Strategy (Prim ReachabilityRule))
-reachabilityOnePathStrategy strategy' =
-    (fmap . fmap . fmap)
-        ruleOnePathToRuleReachability
-        strategy'
-
-reachabilityAllPathStrategy
-    :: Functor t
-    => t (Strategy (Prim AllPathRule))
-    -> t (Strategy (Prim ReachabilityRule))
-reachabilityAllPathStrategy strategy' =
-    (fmap . fmap . fmap)
-        ruleAllPathToRuleReachability
-        strategy'
-
 -- The functions below are easier to read coercions between
 -- the newtypes over 'RewriteRule VariableName' defined in the
 -- instances of 'Goal' as 'Rule's.
@@ -553,7 +530,7 @@ ruleOnePathToRuleReachability
 ruleOnePathToRuleReachability = coerce
 
 type TransitionRule m goal =
-    Prim goal
+    Prim
     -> ProofState goal
     -> Strategy.TransitionT (Rule goal) m (ProofState goal)
 
@@ -567,7 +544,7 @@ transitionRule
 transitionRule claims axiomGroups = transitionRuleWorker
   where
     transitionRuleWorker
-        :: Prim goal
+        :: Prim
         -> ProofState goal
         -> Strategy.TransitionT (Rule goal) m (ProofState goal)
     transitionRuleWorker CheckProven Proven = empty
@@ -614,6 +591,17 @@ transitionRule claims axiomGroups = transitionRuleWorker
       | isTriviallyValid goal =
           return Proven
 
+    -- 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 (Goal goal) =
         Profile.timeStrategy "applyClaims"
         $ applyClaims claims goal
@@ -630,37 +618,9 @@ transitionRule claims axiomGroups = transitionRuleWorker
         Profile.timeStrategy "applyAxioms"
         $ applyAxioms axiomGroups goal
 
-    transitionRuleWorker (DerivePar rules) (Goal goal) =
-        -- TODO (virgil): Wrap the results in GoalRemainder/GoalRewritten here.
-        --
-        -- 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.
-        Profile.timeStrategy "Goal.DerivePar"
-        $ derivePar rules goal
-    transitionRuleWorker (DerivePar rules) (GoalRemainder goal) =
-        -- TODO (virgil): Wrap the results in GoalRemainder/GoalRewritten here.
-        -- See above for an explanation.
-        Profile.timeStrategy "Goal.DeriveParRemainder"
-        $ derivePar rules goal
-
-    transitionRuleWorker (DeriveSeq rules) (Goal goal) =
-        -- TODO (virgil): Wrap the results in GoalRemainder/GoalRewritten here.
-        -- See above for an explanation.
-        Profile.timeStrategy "Goal.DeriveSeq"
-        $ deriveSeq rules goal
-    transitionRuleWorker (DeriveSeq rules) (GoalRemainder goal) =
-        -- TODO (virgil): Wrap the results in GoalRemainder/GoalRewritten here.
-        -- See above for an explanation.
-        Profile.timeStrategy "Goal.DeriveSeqRemainder"
-        $ deriveSeq rules goal
-
     transitionRuleWorker _ state = return state
 
-onePathFirstStep :: Strategy (Prim goal)
+onePathFirstStep :: Strategy Prim
 onePathFirstStep =
     (Strategy.sequence . map Strategy.apply)
         [ CheckProven
@@ -675,7 +635,7 @@ onePathFirstStep =
         , TriviallyValid
         ]
 
-onePathFollowupStep :: Strategy (Prim goal)
+onePathFollowupStep :: Strategy Prim
 onePathFollowupStep =
     (Strategy.sequence . map Strategy.apply)
         [ CheckProven
@@ -691,7 +651,7 @@ onePathFollowupStep =
         , TriviallyValid
         ]
 
-allPathFirstStep :: Strategy (Prim AllPathRule)
+allPathFirstStep :: Strategy Prim
 allPathFirstStep =
     (Strategy.sequence . map Strategy.apply)
         [ CheckProven
@@ -706,7 +666,7 @@ allPathFirstStep =
         , TriviallyValid
         ]
 
-allPathFollowupStep :: Strategy (Prim AllPathRule)
+allPathFollowupStep :: Strategy Prim
 allPathFollowupStep =
     (Strategy.sequence . map Strategy.apply)
         [ CheckProven

kore/src/Kore/Strategies/ProofState.hs

@@ -27,7 +27,7 @@ import qualified Pretty
 
 {- | The primitive transitions of the reachability proof strategy.
  -}
-data Prim rule
+data Prim
     = CheckProven
     -- ^ End execution on this branch if the state is 'Proven'.
     | CheckGoalRemainder
@@ -39,26 +39,11 @@ data Prim rule
     | Simplify
     | CheckImplication
     | TriviallyValid
-    | DerivePar [rule]
-    | DeriveSeq [rule]
     | ApplyClaims
     | ApplyAxioms
-    deriving (Show, Functor)
-
-instance Filterable Prim where
-    mapMaybe _ CheckProven        = CheckProven
-    mapMaybe _ CheckGoalRemainder = CheckGoalRemainder
-    mapMaybe _ CheckGoalStuck     = CheckGoalStuck
-    mapMaybe _ ResetGoal          = ResetGoal
-    mapMaybe _ Simplify           = Simplify
-    mapMaybe _ CheckImplication   = CheckImplication
-    mapMaybe _ TriviallyValid     = TriviallyValid
-    mapMaybe _ ApplyClaims        = ApplyClaims
-    mapMaybe _ ApplyAxioms        = ApplyAxioms
-    mapMaybe f (DerivePar rules)  = DerivePar (mapMaybe f rules)
-    mapMaybe f (DeriveSeq rules)  = DeriveSeq (mapMaybe f rules)
-
-instance Unparse goal => Pretty (Prim goal) where
+    deriving (Show)
+
+instance Pretty Prim where
     pretty CheckProven = "Transition CheckProven."
     pretty CheckGoalRemainder = "Transition CheckGoalRemainder."
     pretty CheckGoalStuck = "Transition CheckGoalStuck."
@@ -68,14 +53,6 @@ instance Unparse goal => Pretty (Prim goal) where
     pretty TriviallyValid = "Transition TriviallyValid."
     pretty ApplyClaims = "apply claims"
     pretty ApplyAxioms = "apply axioms"
-    pretty (DerivePar rules) =
-        Pretty.vsep
-            $ ["Transition DerivePar with rules:"]
-            <> fmap (Pretty.indent 4 . unparse) rules
-    pretty (DeriveSeq rules) =
-        Pretty.vsep
-            $ ["Transition DeriveSeq with rules:"]
-            <> fmap (Pretty.indent 4 . unparse) rules
 
 {- | The state of the reachability proof strategy for @goal@.
  -}

kore/src/Kore/Strategies/Verification.hs

@@ -295,7 +295,7 @@ verifyClaim
         & lift
 
     modifiedTransitionRule
-        ::  Prim ReachabilityRule
+        ::  Prim
         ->  CommonProofState
         ->  TransitionT (Rule ReachabilityRule) (Verifier simplifier)
                 CommonProofState
@@ -338,15 +338,15 @@ verifyClaimStep target claims axioms executionGraph node =
     destination = getDestination target
     axiomGroups = groupSortOn Attribute.Axiom.getPriorityOfAxiom axioms
 
-    strategy' :: Strategy (Prim ReachabilityRule)
+    strategy' :: Strategy Prim
     strategy'
         | isRoot = firstStep
         | otherwise = followupStep
 
-    firstStep :: Strategy (Prim ReachabilityRule)
+    firstStep :: Strategy Prim
     firstStep = strategy target claims axioms Stream.!! 0
 
-    followupStep :: Strategy (Prim ReachabilityRule)
+    followupStep :: Strategy Prim
     followupStep = strategy target claims axioms Stream.!! 1
 
     ExecutionGraph { root } = executionGraph
@@ -361,7 +361,7 @@ transitionRule'
     -> [[Rule ReachabilityRule]]
     -> ReachabilityRule
     -> RHS VariableName
-    -> Prim ReachabilityRule
+    -> Prim
     -> CommonProofState
     -> TransitionT (Rule ReachabilityRule) simplifier CommonProofState
 transitionRule' claims axiomGroups goal _ prim state = do
@@ -405,10 +405,6 @@ logTransitionRule rule prim proofState =
             whileSimplify goal $ rule prim proofState
         Prim.CheckImplication ->
             whileCheckImplication goal $ rule prim proofState
-        (Prim.DeriveSeq rules) ->
-            whileDeriveSeq rules goal $ rule prim proofState
-        (Prim.DerivePar rules) ->
-            whileDerivePar rules goal $ rule prim proofState
         _ ->
             rule prim proofState
 
@@ -417,7 +413,7 @@ debugProofStateBracket
     .  MonadLog monad
     => ProofState ReachabilityRule
     -- ^ current proof state
-    -> Prim ReachabilityRule
+    -> Prim
     -- ^ transition
     -> monad (ProofState ReachabilityRule)
     -- ^ action to be computed
@@ -441,7 +437,7 @@ debugProofStateFinal
     => MonadLog monad
     => ProofState ReachabilityRule
     -- ^ current proof state
-    -> Prim ReachabilityRule
+    -> Prim
     -- ^ transition
     -> monad (ProofState ReachabilityRule)
 debugProofStateFinal proofState (coerce -> transition) = do

kore/test/Test/Kore/Strategies/AllPath/AllPath.hs

@@ -4,7 +4,6 @@ module Test.Kore.Strategies.AllPath.AllPath
     , test_transitionRule_CheckGoalRem
     , test_transitionRule_CheckImplication
     , test_transitionRule_TriviallyValid
-    , test_transitionRule_DerivePar
     , test_transitionRule_ApplyClaims
     , test_transitionRule_ApplyAxioms
     , test_runStrategy
@@ -175,34 +174,6 @@ test_transitionRule_TriviallyValid =
     becomesProven :: HasCallStack => ProofState -> TestTree
     becomesProven state = run state `equals_` [(ProofState.Proven, mempty)]
 
-test_transitionRule_DerivePar :: [TestTree]
-test_transitionRule_DerivePar =
-    [ unmodified ProofState.Proven
-    , unmodified (ProofState.GoalRewritten    (A, B))
-    , [Rule (A, C)]
-        `derives`
-        [ (ProofState.Goal    (C,   C), Seq.singleton $ Rule (A, C))
-        , (ProofState.GoalRemainder (Bot, C), mempty)
-        ]
-    , fmap Rule [(A, B), (B, C)]
-        `derives`
-        [ (ProofState.Goal    (B  , C), Seq.singleton $ Rule (A, B))
-        , (ProofState.GoalRemainder (Bot, C), mempty)
-        ]
-    ]
-  where
-    run rules = runTransitionRule [] [] (ProofState.DerivePar rules)
-    unmodified :: HasCallStack => ProofState -> TestTree
-    unmodified state = run [Rule (A, B)] state `equals_` [(state, mempty)]
-    derives
-        :: HasCallStack
-        => [Goal.Rule Goal]
-        -- ^ rules to apply in parallel
-        -> [(ProofState, Seq (Goal.Rule Goal))]
-        -- ^ transitions
-        -> TestTree
-    derives rules = equals_ (run rules $ ProofState.GoalRemainder (A, C))
-
 test_transitionRule_ApplyClaims :: [TestTree]
 test_transitionRule_ApplyClaims =
     [ unmodified ProofState.Proven
@@ -369,7 +340,7 @@ type Goal = (K, K)
 
 type ProofState = ProofState.ProofState Goal
 
-type Prim = Goal.Prim Goal
+type Prim = Goal.Prim
 
 newtype instance Goal.Rule Goal =
     Rule { unRule :: (K, K) }