--- a
+++ b/doc/source/krb_syntax/compound_premise.txt
@@ -0,0 +1,286 @@
+.. $Id$
+.. 
+.. Copyright Š 2008 Bruce Frederiksen
+.. 
+.. Permission is hereby granted, free of charge, to any person obtaining a copy
+.. of this software and associated documentation files (the "Software"), to deal
+.. in the Software without restriction, including without limitation the rights
+.. to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+.. copies of the Software, and to permit persons to whom the Software is
+.. furnished to do so, subject to the following conditions:
+.. 
+.. The above copyright notice and this permission notice shall be included in
+.. all copies or substantial portions of the Software.
+.. 
+.. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+.. IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+.. FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+.. AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+.. LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+.. OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+.. THE SOFTWARE.
+
+restindex
+    crumb: Compound Premise
+    page-description:
+        The syntax of compound premises.
+    /description
+    format: rest
+    encoding: utf8
+    output-encoding: utf8
+    include: yes
+    initialheaderlevel: 2
+/restindex
+
+=============================================
+Compound Premise Syntax
+=============================================
+
+There are three kinds of compound premises.  These can be used in both
+`forward-chaining rules`_ and `backward-chaining rules`_, but the nested
+premises are restricted to the kind of premises legal for that kind of rule:
+fc_premise_ for `forward-chaining rules`_, and bc_premise_ for
+`backward-chaining rules`_.
+
+::
+
+    compound_premise ::= first_premise
+                       | forall_premise
+                       | notany_premise
+
+First Premise
+=====================
+
+The ``first`` premise is used to prevent backtracking_ from finding subsequent
+solutions to a set of premises.  The ``first`` premise always fails on
+backtracking_, but does do backtracking_ within the nested premises.
+
+::
+
+    first_premise ::= ['!'] 'first' premise
+                    | ['!'] 'first' NL
+                              INDENT
+                                 {premise NL}
+                              DEINDENT
+
+The ``!`` option can only be used in `backward-chaining rules`_.
+
+The nested premises may include any type of plan_spec_ in `backward-chaining
+rules`_.
+
+Forall Premise
+=====================
+
+The ``forall`` premise forces backtracking within the nested premises to
+process all of the possible solutions found.
+
+::
+
+    forall_premise ::= 'forall' NL
+                         INDENT
+                            {premise NL}
+                         DEINDENT
+                     [ 'require' NL
+                         INDENT
+                            {premise NL}
+                         DEINDENT ]
+
+The premises within the ``require`` clause are tried for each solution found.
+If these fail for any solution, then the entire ``forall`` premise fails.
+Thus, the ``forall`` only succeeds if the ``require`` premises are true for
+all solutions generated within the ``forall`` clause.
+
+The ``forall`` always succeeds if the ``require`` clause is omitted.  This can
+be used in conjunction with python_statements_ to gather a list of results.
+
+The ``forall`` premise always fails on backtracking.
+
+See `Notes on Forall and Notany Premises`_ and Examples_, below.
+
+Notany Premise
+=====================
+
+The ``notany`` premise only succeeds if no solution can be found to the nested
+premises.
+
+::
+
+    notany_premise ::= 'notany' NL
+                         INDENT
+                            {premise NL}
+                         DEINDENT
+
+See `Notes on Forall and Notany Premises`_ and Examples_, below.
+
+Notes on Forall and Notany Premises
+======================================
+
+#. All `pattern variable`_ bindings made during the execution of a ``forall``
+   or ``notany`` premise are undone before the premises following the
+   ``forall`` or ``notany`` are run.
+   Thus, ``forall`` and ``notany`` can be used to test
+   values produced by prior premises; but to generate values for subsequent
+   premises the values must be captured in python variables within the
+   ``forall`` or ``notany`` clause before the `pattern variables` are unbound
+   (see `Computing Sets of Values`_, below).
+
+#. When used in `backward-chaining rules`_, the only plan_spec_ allowed in
+   nested premises is the ``as`` clause.
+
+Examples
+=============
+
+These examples use the following subgoals:
+
+* ``generate_x($x)`` generates multiple solutions (as ``$x``) that will looped
+  over
+* ``test_x($x)`` does some test on ``$x``
+* ``compute_y($x, $y)`` takes ``$x`` as input and computes a ``$y`` value
+
+Finding the First Solution From a Set of Values
+-------------------------------------------------
+
+If you want the first ``$x`` that passes the ``test_x($x)`` test, you have two
+options::
+
+    generate_x($x)
+    test_x($x)
+    ...
+
+And::
+
+    first
+        generate_x($x)
+        test_x($x)
+    ...
+
+The difference is that the first example will find other ``$x`` values that
+pass ``test_x($x)`` on backtracking_, while the second example will stop after
+the first value is found and fail on backtracking_.
+
+Testing Sets of Values
+-------------------------
+
+There are two general cases.  You might want to verify that ``test_x($x)``
+*succeeds* for all generated ``$x`` values::
+
+    forall
+        generate_x($x)
+    require
+        test_x($x)
+
+.. Note::
+   While ``$x`` is set and used within the ``forall`` premise to transfer
+   values from the ``generate_x($x)`` goal to the ``test_x($x)`` goal, it is
+   no longer set afterwards and can not be referenced in the premises
+   following the ``forall`` premise.
+
+The second case that you might want to verify is that ``test_x($x)`` *fails*
+for all generated ``$x`` values::
+
+    forall
+        generate_x($x)
+    require
+        notany
+            test_x($x)
+
+Or, more simply::
+
+    notany
+        generate_x($x)
+        test_x($x)
+
+Computing Sets of Values
+------------------------------
+
+If you want a tuple of computed ``$y`` values for all of the ``$x`` values::
+
+    python y_list = []
+    forall
+        generate_x($x)
+    require
+        compute_x($x, $y)
+        python y_list.append($y)
+    $y_list = tuple(y_list)
+
+This will only succeed if ``compute_y`` succeeds for every ``$x`` value.  If
+you want to skip over ``$x`` values that ``compute_y`` fails on, you might
+try::
+
+    python y_list = []
+    forall
+        generate_x($x)
+        compute_x($x, $y)
+        python y_list.append($y)
+    $y_list = tuple(y_list)
+
+But note that if ``compute_y`` might compute multiple solutions on
+backtracking_, you would end up including all of these solutions for each
+``$x`` in your ``$y_list``.  To only get the first computed value for each
+``$x``::
+
+    python y_list = []
+    forall
+        generate_x($x)
+        first
+            compute_x($x, $y)
+            python y_list.append($y)
+    $y_list = tuple(y_list)
+
+A simple common case of ``generate_x`` is when you are computing values for
+each element of a tuple::
+
+    python y_list = []
+    forall
+        $x in $x_list
+        first
+            compute_x($x, $y)
+            python y_list.append($y)
+    $y_list = tuple(y_list)
+
+This can also be done by creating a new subgoal that recurses on ``$x_list``::
+
+    compute_list_done
+        use compute_list((), ())
+
+    compute_list_step
+        use compute_list(($x, *$x_rest), ($y, *$y_rest))
+        when
+            compute_y($x, $y)
+            compute_list($x_rest, $y_rest)
+
+Note that there is an important difference between these two examples if
+``compute_y`` may find alternate ``$y`` values for any given ``$x`` value on
+backtracking_.
+
+The first example will only generate one ``$y_list``.  If that ``$y_list``
+doesn't work in subsequent premises, the ``forall`` fails on backtracking_,
+so no solution will be found.
+
+The second example will not fail in this situation, but will produce all
+possible combinations of solutions to ``computer_y`` for each ``$x`` on
+backtracking_ until a resulting ``$y_list`` satisfies the subsequent premises.
+
+Finally, if you want to gather only the computed ``$y`` values for ``$x``
+values that pass ``test_x($x)``::
+
+    python y_list = []
+    forall
+        generate_x($x)
+        test_x($x)
+    require
+        compute_x($x, $y)
+        python y_list.append($y)
+    $y_list = tuple(y_list)
+
+.. _backtracking: ../overview/rules/backward_chaining.html#backtracking
+.. _backward-chaining rules: bc_rule.html
+.. _bc_premise: bc_rule.html#when-clause
+.. _Examples: #examples
+.. _fc_premise: fc_rule.html#foreach-clause
+.. _forward-chaining rules: fc_rule.html
+.. _Notes on Forall and Notany Premises: #notes-on-forall-and-notany-premises
+.. _pattern variable: pattern.html#pattern-variable
+.. _plan_spec: bc_rule.html#plan-spec
+.. _python_statements: python_premise.html#python-statements
+.. _Computing Sets of Values: #computing-sets-of-values