kore-repl: do not remove direct children of branchings when using clear command (#1952)

* kore-repl: do not remove direct children of branchings when using clear command

* Clean-up

* Address review comments

* Fix

Author: ana-pantilie

kore/src/Kore/Repl/Data.hs

@@ -358,8 +358,8 @@ helpText =
     \tryf (<a|c><num>)|<name>                 attempts <a>xiom or <c>laim at\
                                               \ index <num> or rule with <name>,\
                                               \ and if successful, it will apply it.\n\
-    \clear [n]                                removes all node children from the\
-                                              \ proof graph\n\
+    \clear [n]                                removes all the node's children from the\
+                                              \ proof graph (****)\n\
     \                                         (defaults to current node)\n\
     \save-session file                        saves the current session to file\n\
     \save-partial-proof [n] file              creates a file, <file>.kore, containing a kore module\
@@ -414,6 +414,9 @@ helpText =
     \ the current node is advanced to the (only) non-bottom leaf. If no such\n\
     \ leaf exists (i.e the proof is complete), the current node remains the same\n\
     \ and a message is emitted.\n\
+    \ (****) The clear command doesn't allow the removal of nodes which are direct\n\
+    \ descendants of branchings. The steps which create branchings cannot be\n\
+    \ partially redone. Therefore, if this were allowed it would result in invalid proofs.\n\
     \\n\n\
     \Rule names can be added in two ways:\n\
     \    a) rule <k> ... </k> [label(myName)]\n\

kore/src/Kore/Repl/Interpreter.hs

@@ -32,6 +32,7 @@ import Control.Lens
 import qualified Control.Lens as Lens
 import Control.Monad
     ( void
+    , (<=<)
     )
 import Control.Monad.Extra
     ( ifM
@@ -935,16 +936,19 @@ clear
     => Maybe ReplNode
     -- ^ 'Nothing' for current node, or @Just n@ for a specific node identifier
     -> m ()
-clear =
-    \case
+clear maybeNode = do
+    graph <- getInnerGraph
+    case maybeNode of
         Nothing -> Lens.use (field @"node") >>= clear . Just
         Just node
-          | unReplNode node == 0 -> putStrLn' "Cannot clear initial node (0)."
-          | otherwise -> clear0 node
+          | unReplNode node == 0 ->
+              putStrLn' "Cannot clear initial node (0)."
+          | isDirectDescendentOfBranching node graph ->
+              putStrLn' "Cannot clear a direct descendant of a branching node."
+          | otherwise -> clear0 node graph
   where
-    clear0 :: ReplNode -> m ()
-    clear0 rnode = do
-        graph <- getInnerGraph
+    clear0 :: ReplNode -> InnerGraph Axiom -> m ()
+    clear0 rnode graph = do
         let node = unReplNode rnode
         let
             nodesToBeRemoved = collect (next graph) node
@@ -962,6 +966,11 @@ clear =
     prevNode :: InnerGraph axiom -> Graph.Node -> Graph.Node
     prevNode graph = fromMaybe 0 . headMay . fmap fst . Graph.lpre graph
 
+    isDirectDescendentOfBranching :: ReplNode -> InnerGraph axiom -> Bool
+    isDirectDescendentOfBranching (ReplNode node) graph =
+        let childrenOfParent = (Graph.suc graph <=< Graph.pre graph) node
+         in length childrenOfParent /= 1
+
 -- | Save this sessions' commands to the specified file.
 saveSession
     :: forall m