From 537952b88cbbe4bab1ccc6ebb84f31cc9c83157b Mon Sep 17 00:00:00 2001
From: Nishant Rodrigues <nishantjr@gmail.com>
Date: Wed, 12 Feb 2020 02:42:53 +0530
Subject: [PATCH] Reap failed goals and children (TODO: This uses `[owise]`

---
 prover/strategies/core.md | 36 +++++++++++++++++++++++++++++-------
 1 file changed, 29 insertions(+), 7 deletions(-)

diff --git a/prover/strategies/core.md b/prover/strategies/core.md
index 07693e8af..3732c7d8b 100644
--- a/prover/strategies/core.md
+++ b/prover/strategies/core.md
@@ -95,15 +95,37 @@ completed, its result is replaced in the parent goal and the subgoal is removed.
                 <strategy> goalStrat(ID) => RStrat ... </strategy>
                 ...
          </goal>
-         ( <goal> <id> ID </id>
-                  <active> true:Bool </active>
-                  <parent> PID </parent>
-                  <strategy> RStrat:TerminalStrategy </strategy>
-                  ...
-           </goal> => .Bag
-         )
+         <goal> <id> ID </id>
+                <active> true:Bool => false </active>
+                <parent> PID </parent>
+                <strategy> (.K => #reap?) ~> RStrat:TerminalStrategy </strategy>
+                ...
+         </goal>
          ...
        </prover>
+
+  syntax KItem ::= "#reap?" // if goal failed prune goal and children
+  rule <strategy> (#reap? => #reap) ~> fail    </strategy>
+  rule <strategy> (#reap? => .K   ) ~> success </strategy>
+
+  syntax KItem ::= "#reap"  // (always) prune goal and children
+  rule <goal>
+         <id> PID </id>
+         <strategy> #reap ~> RStrat:TerminalStrategy </strategy>
+         ...
+       </goal>
+       <goal>
+         <parent> PID </parent>
+         <strategy> (.K => #reap) ~> Strat:Strategy </strategy>
+         ...
+       </goal>
+  rule <prover>
+         <goal>
+           <strategy> #reap ~> Strat:Strategy </strategy>
+           ...
+         </goal> => .Bag
+         ...
+      </prover> [owise]
 ```
 
 Proving a goal may involve proving other subgoals: