Reap failed goals and children (TODO: This uses [owise]

kframework · Feb 11, 2020 · 537952b · 537952b
1 parent fed7bf9
commit 537952b
Showing 1 changed file with 29 additions and 7 deletions.
diff --git 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: