Use entire goal in proof strategy

kore/src/Kore/Repl/Data.hs

@@ -229,6 +229,8 @@ data ReplCommand
     -- ^ Select a different node in the graph.
     | ShowConfig !(Maybe ReplNode)
     -- ^ Show the configuration from the current node.
+    | ShowDest !(Maybe ReplNode)
+    -- ^ Show the destination from the current node.
     | OmitCell !(Maybe String)
     -- ^ Adds or removes cell to omit list, or shows current omit list.
     | ShowLeafs
@@ -334,6 +336,8 @@ helpText =
     \select <n>                               select node id 'n' from the graph\n\
     \config [n]                               shows the config for node 'n'\
                                               \ (defaults to current node)\n\
+    \dest [n]                                 shows the destination for node 'n'\
+                                              \ (defaults to current node)\n\
     \omit [cell]                              adds or removes cell to omit list\
                                               \ (defaults to showing the omit\
                                               \ list)\n\

kore/src/Kore/Repl/Interpreter.hs

@@ -178,6 +178,7 @@ import Kore.Step.RulePattern
     ( ReachabilityRule (..)
     , RulePattern (..)
     , ToRulePattern (..)
+    , rhsToPattern
     )
 import Kore.Step.Simplification.Data
     ( MonadSimplify
@@ -186,12 +187,12 @@ import qualified Kore.Step.Strategy as Strategy
 import Kore.Strategies.Goal
 import Kore.Strategies.ProofState
     ( ProofStateTransformer (ProofStateTransformer)
+    , extractUnproven
     , proofState
     )
 import qualified Kore.Strategies.ProofState as ProofState.DoNotUse
 import Kore.Strategies.Verification
     ( CommonProofState
-    , commonProofStateTransformer
     )
 import Kore.Syntax.Application
 import qualified Kore.Syntax.Id as Id
@@ -248,6 +249,7 @@ replInterpreter0 printAux printKore replCmd = do
                 ProveStepsF n         -> proveStepsF n           $> Continue
                 SelectNode i          -> selectNode i            $> Continue
                 ShowConfig mc         -> showConfig mc           $> Continue
+                ShowDest mc           -> showDest mc             $> Continue
                 OmitCell c            -> omitCell c              $> Continue
                 ShowLeafs             -> showLeafs               $> Continue
                 ShowRule   mc         -> showRule mc             $> Continue
@@ -521,14 +523,37 @@ showConfig
     => Maybe ReplNode
     -- ^ 'Nothing' for current node, or @Just n@ for a specific node identifier
     -> ReplM m ()
-showConfig configNode = do
-    maybeConfig <- getConfigAt configNode
-    case maybeConfig of
+showConfig =
+    showProofStateComponent "Config" getConfiguration
+
+-- | Shows destination at node 'n', or current node if 'Nothing' is passed.
+showDest
+    :: Monad m
+    => Maybe ReplNode
+    -- ^ 'Nothing' for current node, or @Just n@ for a specific node identifier
+    -> ReplM m ()
+showDest =
+    showProofStateComponent "Destination" (rhsToPattern . getDestination)
+
+showProofStateComponent
+    :: Monad m
+    => String
+    -- ^ component name
+    -> (ReachabilityRule -> Pattern VariableName)
+    -> Maybe ReplNode
+    -> ReplM m ()
+showProofStateComponent name transformer maybeNode = do
+    maybeProofState <- getProofStateAt maybeNode
+    case maybeProofState of
         Nothing -> putStrLn' "Invalid node!"
         Just (ReplNode node, config) -> do
             omit <- Lens.use (field @"omit")
-            putStrLn' $ "Config at node " <> show node <> " is:"
-            tell $ unparseStrategy omit config
+            putStrLn' $ name <> " at node " <> show node <> " is:"
+            unparseProofStateComponent
+                transformer
+                omit
+                config
+                & tell
 
 -- | Shows current omit list if passed 'Nothing'. Adds/removes from the list
 -- depending on whether the string already exists in the list or not.
@@ -846,7 +871,7 @@ tryAxiomClaimWorker mode ref = do
         -> ReplM m ()
     showUnificationFailure axiomOrClaim' node = do
         let first = extractLeftPattern axiomOrClaim'
-        maybeSecond <- getConfigAt (Just node)
+        maybeSecond <- getProofStateAt (Just node)
         case maybeSecond of
             Nothing -> putStrLn' "Unexpected error getting current config."
             Just (_, second) ->
@@ -858,7 +883,7 @@ tryAxiomClaimWorker mode ref = do
                         , goalRewrittenTransformer = patternUnifier
                         , goalStuckTransformer = patternUnifier
                         }
-                    second
+                    (getConfiguration <$> second)
               where
                 patternUnifier :: Pattern VariableName -> ReplM m ()
                 patternUnifier
@@ -964,30 +989,25 @@ savePartialProof
     -> FilePath
     -> ReplM m ()
 savePartialProof maybeNatural file = do
-    currentClaim <- Lens.use (field @"claim")
     currentIndex <- Lens.use (field @"claimIndex")
     claims <- Lens.use (field @"claims")
     Config { mainModuleName } <- ask
-    maybeConfig <- getConfigAt maybeNode
-    case maybeConfig of
+    maybeConfig <- getProofStateAt maybeNode
+    case (fmap . fmap) extractUnproven maybeConfig of
         Nothing -> putStrLn' "Invalid node!"
-        Just (currentNode, currentProofState) -> do
-            let config = unwrapConfig currentProofState
-                newClaim = createClaim currentClaim config
-                newTrustedClaims =
+        Just (_, Nothing) -> putStrLn' "Goal is proven."
+        Just (currentNode, Just currentGoal) -> do
+            let newTrustedClaims =
                     makeTrusted
                     <$> removeIfRoot currentNode currentIndex claims
                 newDefinition =
                     createNewDefinition
                         mainModuleName
                         (makeModuleName file)
-                        $ newClaim : newTrustedClaims
+                        $ currentGoal : newTrustedClaims
             saveUnparsedDefinitionToFile (unparse newDefinition)
             putStrLn' "Done."
   where
-    unwrapConfig :: CommonProofState -> Pattern VariableName
-    unwrapConfig = proofState commonProofStateTransformer
-
     saveUnparsedDefinitionToFile
         :: Pretty.Doc ann
         -> ReplM m ()
@@ -1203,26 +1223,30 @@ showRewriteRule rule =
     <> makeAuxReplOutput (show . Pretty.pretty . from @_ @SourceLocation $ rule)
 
 -- | Unparses a strategy node, using an omit list to hide specified children.
-unparseStrategy
-    :: Set String
+unparseProofStateComponent
+    :: (ReachabilityRule -> Pattern VariableName)
+    -> Set String
     -- ^ omit list
     -> CommonProofState
     -- ^ pattern
     -> ReplOutput
-unparseStrategy omitList =
+unparseProofStateComponent transformation omitList =
     proofState ProofStateTransformer
-        { goalTransformer = makeKoreReplOutput . unparseToString . fmap hide
-        , goalRemainderTransformer = \pat ->
+        { goalTransformer =
+            makeKoreReplOutput . unparseComponent
+        , goalRemainderTransformer = \goal ->
             makeAuxReplOutput "Stuck: \n"
-            <> makeKoreReplOutput (unparseToString $ fmap hide pat)
+            <> makeKoreReplOutput (unparseComponent goal)
         , goalRewrittenTransformer =
-            makeKoreReplOutput . unparseToString . fmap hide
-        , goalStuckTransformer = \pat ->
+            makeKoreReplOutput . unparseComponent
+        , goalStuckTransformer = \goal ->
             makeAuxReplOutput "Stuck: \n"
-            <> makeKoreReplOutput (unparseToString $ fmap hide pat)
+            <> makeKoreReplOutput (unparseComponent goal)
         , provenValue = makeAuxReplOutput "Reached bottom"
         }
   where
+    unparseComponent =
+        unparseToString . fmap hide . transformation
     hide :: TermLike VariableName -> TermLike VariableName
     hide =
         Recursive.unfold $ \termLike ->

kore/src/Kore/Repl/Parser.hs

@@ -105,6 +105,7 @@ nonRecursiveCommand =
         , proveSteps
         , selectNode
         , showConfig
+        , showDest
         , omitCell
         , showLeafs
         , showRule
@@ -188,6 +189,11 @@ showConfig = do
     dec <- literal "config" *> maybeDecimal
     return $ ShowConfig (fmap ReplNode dec)
 
+showDest :: Parser ReplCommand
+showDest = do
+    dec <- literal "dest" *> maybeDecimal
+    return $ ShowDest (fmap ReplNode dec)
+
 omitCell :: Parser ReplCommand
 omitCell = OmitCell <$$> literal "omit" *> maybeWord
 

kore/src/Kore/Repl/State.hs

@@ -17,7 +17,7 @@ module Kore.Repl.State
     , getTargetNode, getInnerGraph, getExecutionGraph
     , smoothOutGraph
     , getInterestingBranchingNode
-    , getConfigAt, getRuleFor, getLabels, setLabels
+    , getProofStateAt, getRuleFor, getLabels, setLabels
     , runStepper, runStepper'
     , runUnifier
     , updateInnerGraph, updateExecutionGraph
@@ -46,7 +46,6 @@ import Control.Monad.State.Strict
     , modify
     )
 import qualified Control.Monad.Trans.Class as Monad.Trans
-import qualified Data.Bifunctor as Bifunctor
 import Data.Bitraversable
     ( bisequence
     , bitraverse
@@ -110,9 +109,6 @@ import Kore.Internal.Condition
     ( Condition
     )
 import qualified Kore.Internal.Condition as Condition
-import Kore.Internal.Conditional
-    ( Conditional (..)
-    )
 import Kore.Internal.Pattern
     ( Pattern
     )
@@ -128,8 +124,7 @@ import qualified Kore.Internal.TermLike as TermLike
 import qualified Kore.Log as Log
 import Kore.Repl.Data
 import Kore.Step.RulePattern
-    ( RewriteRule (..)
-    , RulePattern (..)
+    ( RulePattern (..)
     )
 import Kore.Step.RulePattern as Rule
 import Kore.Step.Simplification.Data
@@ -140,6 +135,7 @@ import qualified Kore.Strategies.Goal as Goal
 import Kore.Strategies.ProofState
     ( ProofState (Goal)
     , ProofStateTransformer (ProofStateTransformer)
+    , extractUnproven
     , proofState
     )
 import qualified Kore.Strategies.ProofState as ProofState.DoNotUse
@@ -158,11 +154,7 @@ import Kore.Syntax.Variable
 -- | Creates a fresh execution graph for the given claim.
 emptyExecutionGraph :: ReachabilityRule -> ExecutionGraph Axiom
 emptyExecutionGraph =
-    Strategy.emptyExecutionGraph . extractConfig . RewriteRule . toRulePattern
-  where
-    extractConfig :: RewriteRule VariableName -> CommonProofState
-    extractConfig (RewriteRule RulePattern { left, requires }) =
-        Goal $ Conditional left requires mempty
+    Strategy.emptyExecutionGraph . Goal
 
 ruleReference
     :: (Either AxiomIndex ClaimIndex -> a)
@@ -426,12 +418,12 @@ getTargetNode maybeNode = do
        then pure . Just . ReplNode $ node'
        else pure Nothing
 
--- | Get the configuration at selected node (or current node for 'Nothing').
-getConfigAt
+-- | Get the proof state at selected node (or current node for 'Nothing').
+getProofStateAt
     :: MonadState ReplState m
     => Maybe ReplNode
     -> m (Maybe (ReplNode, CommonProofState))
-getConfigAt maybeNode = do
+getProofStateAt maybeNode = do
     node' <- getTargetNode maybeNode
     case node' of
         Nothing -> pure Nothing
@@ -576,18 +568,12 @@ getNodeState graph node =
         . Graph.context graph
         $ node
 
-nodeToPattern
+nodeToGoal
     :: InnerGraph axiom
     -> Graph.Node
-    -> Maybe (Pattern VariableName)
-nodeToPattern graph node =
-    proofState ProofStateTransformer
-        { goalTransformer = Just
-        , goalRemainderTransformer = Just
-        , goalRewrittenTransformer = Just
-        , goalStuckTransformer = Just
-        , provenValue = Nothing
-        }
+    -> Maybe ReachabilityRule
+nodeToGoal graph node =
+    extractUnproven
     . Graph.lab'
     . Graph.context graph
     $ node
@@ -697,18 +683,10 @@ generateInProgressClaims
 generateInProgressClaims = do
     graphs <- Lens.use (field @"graphs")
     claims <- Lens.use (field @"claims")
-    let started = startedClaims graphs claims
+    let started = unprovenGoals graphs
         notStarted = notStartedClaims graphs claims
     return $ started <> notStarted
   where
-    startedClaims
-        :: Map.Map ClaimIndex (ExecutionGraph Axiom)
-        -> [ReachabilityRule]
-        -> [ReachabilityRule]
-    startedClaims graphs claims =
-        fmap (uncurry createClaim)
-        $ claimsWithPatterns graphs claims
-        >>= sequence
     notStartedClaims
         :: Map.Map ClaimIndex (ExecutionGraph Axiom)
         -> [ReachabilityRule]
@@ -728,21 +706,17 @@ generateInProgressClaims = do
                     )
                 )
 
-claimsWithPatterns
+unprovenGoals
     :: Map ClaimIndex (ExecutionGraph axiom)
-    -> [claim]
-    -> [(claim, [Pattern VariableName])]
-claimsWithPatterns graphs claims =
-    Bifunctor.bimap
-        ((claims !!) . unClaimIndex)
-        (findTerminalPatterns . Strategy.graph)
-    <$> Map.toList graphs
-
-findTerminalPatterns
-    :: InnerGraph axiom
-    -> [Pattern VariableName]
-findTerminalPatterns graph =
-    mapMaybe (nodeToPattern graph)
+    -> [ReachabilityRule]
+unprovenGoals graphs =
+    findUnprovenGoals =<< Map.elems graphs
+
+findUnprovenGoals
+    :: ExecutionGraph axiom
+    -> [ReachabilityRule]
+findUnprovenGoals (Strategy.graph -> graph) =
+    mapMaybe (nodeToGoal graph)
     . findLeafNodes
     $ graph
 

kore/src/Kore/Step/RulePattern.hs

@@ -31,6 +31,7 @@ module Kore.Step.RulePattern
     , rhsForgetSimplified
     , rhsToTerm
     , lhsToTerm
+    , rhsToPattern
     , termToRHS
     , injectTermIntoRHS
     , rewriteRuleToTerm
@@ -321,6 +322,23 @@ rhsToTerm RHS { existentials, right, ensures } =
         _ -> TermLike.mkAnd (Predicate.fromPredicate sort ensures) right
     sort = TermLike.termLikeSort right
 
+-- | Converts the 'RHS' back to the term form.
+rhsToPattern
+    :: InternalVariable variable
+    => RHS variable
+    -> Pattern variable
+rhsToPattern RHS { existentials, right, ensures } =
+    TermLike.mkExistsN existentials rhs
+    & Pattern.fromTermLike
+  where
+    rhs =
+        Pattern.toTermLike
+            Conditional
+                { term = right
+                , predicate = ensures
+                , substitution = mempty
+                }
+
 -- | Converts the left-hand side to the term form
 lhsToTerm
     :: InternalVariable variable