Refactor reachability proof strategies

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/Log/InfoReachability.hs

@@ -6,7 +6,7 @@ License     : NCSA
 module Kore.Log.InfoReachability
     ( InfoReachability (..)
     , whileSimplify
-    , whileRemoveDestination
+    , whileCheckImplication
     , whileDeriveSeq
     , whileDerivePar
     ) where
@@ -19,7 +19,7 @@ import qualified Pretty
 
 data InfoReachability
     = InfoSimplify !ReachabilityRule
-    | InfoRemoveDestination !ReachabilityRule
+    | InfoCheckImplication !ReachabilityRule
     | InfoDeriveSeq ![Rule ReachabilityRule] !ReachabilityRule
     | InfoDerivePar ![Rule ReachabilityRule] !ReachabilityRule
     deriving (Show)
@@ -55,8 +55,8 @@ prettyInfoReachabilityGoalAndRules transition goal rules fromRule =
 instance Pretty.Pretty InfoReachability where
     pretty (InfoSimplify goal) =
         prettyInfoReachabilityGoal "Simplify" goal
-    pretty (InfoRemoveDestination goal) =
-        prettyInfoReachabilityGoal "RemoveDestination" goal
+    pretty (InfoCheckImplication goal) =
+        prettyInfoReachabilityGoal "CheckImplication" goal
     pretty (InfoDeriveSeq rules goal) =
         prettyInfoReachabilityGoalAndRules
             "DeriveSeq"
@@ -74,7 +74,7 @@ instance Entry InfoReachability where
     entrySeverity _ = Info
     shortDoc (InfoSimplify _) =
         Just "While simplifying the configuration"
-    shortDoc (InfoRemoveDestination _) =
+    shortDoc (InfoCheckImplication _) =
         Just "While checking implication of the proof goal"
     shortDoc (InfoDeriveSeq _ _) =
         Just "While applying axioms in sequence"
@@ -89,12 +89,12 @@ whileSimplify
     -> log a
 whileSimplify goal = logWhile (InfoSimplify goal)
 
-whileRemoveDestination
+whileCheckImplication
     :: MonadLog log
     => ReachabilityRule
     -> log a
     -> log a
-whileRemoveDestination goal = logWhile (InfoRemoveDestination goal)
+whileCheckImplication goal = logWhile (InfoCheckImplication goal)
 
 whileDeriveSeq
     :: MonadLog log