Diff of /doc/source/logic_tricks.txt [9cf235] .. [f66b44] Maximize Restore

  Switch to side-by-side view

--- a/doc/source/logic_tricks.txt
+++ b/doc/source/logic_tricks.txt
@@ -27,6 +27,7 @@
     /description
     format: rest
     encoding: utf8
+    initialheaderlevel: 2
     output-encoding: utf8
     include: yes
 /restindex
@@ -35,7 +36,7 @@
 Logic Tricks
 ===================================
 
-This describes how to accomplish different logic operations with rules.
+This describes how to accomplish different logic operations with rules_.
 
 X OR Y
 ===========
@@ -43,21 +44,21 @@
 For example: check for text_x($arg) OR test_y($arg).
 
 Create a separate subgoal for the OR case, let's call it ``or_goal``.  Then use
-a separate rule for each OR clause::
-
-    or_goal_test_x:
+a separate rule_ for each OR clause::
+
+    or_goal_test_x
         use or_goal($arg)
         when
             test_x($arg)
 
-    or_goal_test_y:
+    or_goal_test_y
         use or_goal($arg)
         when
             test_y($arg)
 
 Then you'd use ``or_goal($arg)`` where you wanted the *OR* clause.
 
-This can go on for any number of OR-ed clauses by just adding more rules for
+This can go on for any number of OR-ed clauses by just adding more rules_ for
 ``or_goal``.
 
 IF X THEN Y
@@ -66,19 +67,19 @@
 For example: if test_x($arg) then test_y($arg).
 
 What this means is that test_y($arg) must be true if test_x($arg) is true.
-But if test_x($arg) is not true, then test_y($arg) doesn't matter and ``if
+But if test_x($arg) is not true, then test_y($arg) doesn't matter so ``if
 test_x($arg) then test_y($arg)`` is true.
 
-Create a new subgoal, let's call it ``if_x_then_y``.  Use two rules::
-
-    if_x_then_y_if:
+Create a new subgoal, let's call it ``if_x_then_y``.  Use two rules_::
+
+    if_x_then_y_if
         use if_x_then_y($arg)
         when
             test_x($arg)            # if this fails, the next rule will be used
             special.claim_goal()    # don't use any other rules for if_x_then_y
             test_y($arg)            # if this fails, the next rule will not be used, so if_x_then_y will fail.
 
-    if_x_then_y_else:
+    if_x_then_y_else
         use if_x_then_y($_)         # this rule is only used if test_x($arg) fails
 
 NOT X
@@ -89,25 +90,28 @@
 You have to be careful about *not* logic because it can mean different things.
 In this example, if we try ``not test_x($arg)`` and ``$arg`` is unbound what
 should happen?  Should it generate all of the different values for ``$arg``
-for which ``test_x($arg)`` fails?  This generally isn't very practical!
+for which ``test_x($arg)`` fails?  This generally isn't very practical
+computationally!
 
 The other interpretation is that there is **no** possible binding for ``$arg``
 that makes ``test_x($arg)`` true.  In this example, ``not test_x($arg)`` would
 then be false, because there is some ``$arg`` value that makes ``test_x($arg)``
 true.
 
-This second interpretation can be implemented by creating a new subgoal, let's
-say ``not_test_x`` and using a pair of rules::
-
-    not_test_x_fail:
-        use not_test_x($arg)
-        when
-            test_x($arg)            # if there is any way for test_x($arg) to be true
-            special.claim_goal()    # don't use any other rules for not_test_x
-            check False             # and cause this rule to fail, which causes the not_test_x goal to fail
-
-    not_test_x_success:
-        use not_test_x($_)          # this rule only runs if test_x($arg) fails, above
+This second interpretation can be done using the notany_ clause.  This can
+be used in both `forward chaining`_ and `backward chaining`_ rules_::
+
+    your_rule
+        use your_goal($arg)
+        when
+            ..
+            notany
+                test_x($arg)
+            ..
+
+Note that notany_ will only temporarily bind `pattern variables`_ while it
+runs, but not leave any of these bindings in place (for the following premise)
+after it's finished.  Notany_ always fails on backtracking_.
 
 EXISTS X SUCH THAT Y
 ===============================================================
@@ -124,16 +128,84 @@
 FOR ALL X, Y
 ===============================================================
 
-For example: for all $x from generate_x($x), test_y($x) is true
-
-Use the forall clause::
+FOR ALL X, Y succeeds
+-----------------------
+
+For example: for all $x from generate_x($x); test_y($x) succeeds
+
+Use the forall_ clause::
 
     forall
         generate_x($x)
     require
         test_y($x)
 
-Note that all pattern variable bindings done in the forall clause are undone
-before the next clause is run.
-
-This always fails on backtracking.
+Note that all `pattern variables`_ bound in the forall_ clause are unbound
+before the premise following the forall_ is run.  In this example, this
+means that ``$x`` would not be bound to a value following the forall_ clause.
+You can use `python premises`_ to capture the bindings of `pattern variables`_
+in the forall_ clause and make them available to the premises following the
+forall_::
+
+    python x_list = []
+    forall
+        generate_x($x)
+    require
+        test_y($x)
+        python x_list.append($x)
+    $xs = tuple(x_list)
+
+Note that ``x_list`` is a python variable -- not a `pattern variable`_!  It is
+moved back to `pattern variable`_ ``$xs`` in the final line so that the
+following premises can access it.
+
+Forall_ always fails on backtracking_.  Consider these two techniques::
+
+    forall_technique
+        use solve_list($x_list, $x_answers)
+        when
+            python x_answers = []
+            forall
+                $x in $x_list
+            require
+                solve($x, $x_ans)
+                python x_answers.append($x_ans)
+            $x_answers = tuple(x_answers)
+
+and::
+
+    recursive_technique_done
+        use solve_list((), ())
+
+    recursive_technique_more
+        use solve_list(($x1, *$x_rest), ($ans1, *$ans_rest))
+        when
+            solve($x1, $ans1)
+            solve_list($x_rest, $ans_rest)
+
+The first technique will only find the first solution and then fail on
+backtracking_ (if the invoking goal doesn't like the first solution).
+But the second technique will find other solutions on backtracking_.
+
+
+FOR ALL X, Y fails
+-----------------------
+
+For example: for all $x from generate_x($x), not test_y($x)
+
+In this case, just use the notany_ clause::
+
+    notany
+        generate_x($x)
+        test_y($x)
+
+.. _backtracking: overview/rules/backward_chaining.html#backtracking
+.. _backward chaining: overview/rules/backward_chaining.html
+.. _forall: krb_syntax/bc_rule.html#forall
+.. _forward chaining: overview/rules/forward_chaining.html
+.. _notany: krb_syntax/bc_rule.html#notany
+.. _pattern variable: krb_syntax/pattern.html#pattern-variable
+.. _pattern variables: `pattern variable`_
+.. _python premises: krb_syntax/python_premise.html
+.. _rule: overview/rules/index.html
+.. _rules: rule_