[m-rev.] for review: Improvements to reference manual

[Mark Brown]

Hi,

The sections in the reference manual on interfacing nondet code to the
real world and committed choice are a bit out of date, and can also be
clarified. For review by Zoltan.

Cheers,
Mark.

Improve description of interfacing nondet code with the real world.

doc/reference_manual.texi:
    Describe pruning in terms of single-solution contexts, and add a link
    to the full definition.

    Move the point about "don't care" nondeterminism into the next section,
    where the relevant determinism is introduced.

    Refer to all predicates and functions in the solutions module, not
    just solutions/2.

    Include promise_equivalent_solutions as a way of introducing a
    single-solution context.

diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index 8900945..b360185 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -3567,45 +3567,40 @@ a @code{nondet} or @code{multi} mode of a predicate
 from a predicate declared as @code{semidet} or @code{det}
 will cause a determinism error.
 So how can we call nondeterministic code from deterministic code?
-There are several alternative possibilities.
+It depends on how you want to use the outputs from the nondetermistic code.
+There are three possibilities:
+
+ at itemize @bullet
+ at item
+You don't care about the output values;
+you just want to see if the goal is satisfiable or not.
+
+ at item
+You want to use the output values from one of the solutions,
+and it doesn't matter which one.
+
+ at item
+You want to combine the output values from many or all solutions
+into a single result.
+
+ at end itemize

 If you just want to see if a nondeterministic goal is satisfiable or not,
 without needing to know what variable bindings it produces,
 then there is no problem -
-determinism analysis considers @code{nondet} and @code{multi} goals
-with no non-local output variables to be
+solutions to @code{nondet} and @code{multi} goals
+with no non-local output variables
+are declaratively equivalent,
+so Mercury can safely prune away any potential duplicate solutions.
+Determinism analysis thus considers these goals to be
 @code{semidet} and @code{det} respectively.

-If you want to use the values of output variables,
-then you need to ask yourself
-which one of possibly many solutions to a goal do you want?
-If you want all of them, you need to use the predicate
- at samp{solutions/2} in the standard library module @samp{solutions},
-which collects all of the solutions to a goal into a list ---
- at pxref{Higher-order}.
-
 If you just want one solution and don't care which,
-the calling predicate should be declared @code{nondet} or @code{multi}.
-The nondeterminism should then be propagated up the call tree
-to the point at which it can be pruned.
-In Mercury, pruning can be achieved in several ways.
-
-The first way is the one mentioned above:
-if a goal has no non-local output variables
-then the implementation will only attempt to satisfy the goal once.
-Any potential duplicate solutions will be implicitly pruned away.
-
-The second way is to rely on the fact that
-the implementation will only seek a single solution to @samp{main/2},
-so alternative solutions to @samp{main/2}
-(and hence also to @code{nondet} or @code{multi} predicates
-called directly or indirectly from @samp{main/2})
-are implicitly pruned away.
-This is one way to achieve ``don't care'' style nondeterminism in Mercury.
-
-The other situation in which you may want pruning
-and committed choice style nondeterminism
-is when you know that all the solutions returned will be equivalent.
+you need to allow Mercury to prune the other solutions.
+If you know that there will only ever be at most one distinct
+solution under the equality theory of the output variables,
+then you can use a @samp{promise_equivalent_solutions} determinism cast,
+which will do the pruning.
 For example, you might want to find the maximum element in a set
 by iterating over the elements in the set.
 Iterating over the elements in a set in an unspecified order is a
@@ -3613,10 +3608,6 @@ nondeterministic operation,
 but no matter which order you remove them,
 the maximum value in the set should be the same.

-If you know that there will only ever be at most one distinct
-solution under the equality theory of the output variables, then you can use a
- at samp{promise_equivalent_solutions} determinism cast.
-
 Note that specifying a user-defined equivalence relation
 as the equality predicate for user-defined types
 (@pxref{User-defined equality and comparison})
@@ -3629,6 +3620,18 @@ The @samp{promise_equivalent_solutions}
determinism cast could then be used for
 sets even though the lists used to represent the sets might not be in the same
 order in every solution.

+More generally, Mercury prunes alternative solutions for
+goals that are in a ``single-solution context'',
+of which the above are two particular cases.
+The full definition of single-solution context
+is given in @ref{Committed choice nondeterminism}.
+
+If you want to combine output values from many solutions into a single result,
+you need to use one of the predicates or functions
+in the @samp{solutions} standard library module.
+In order to use these you will need to construct a higher-order term
+for the nondeterministic goal (@pxref{Higher-order}).
+
 @node Committed choice nondeterminism
 @section Committed choice nondeterminism

@@ -3645,14 +3648,15 @@ Such single-solution contexts are determined as follows.
 @item
 The body of any procedure declared @code{cc_multi} or
 @code{cc_nondet} is in a single-solution context.
-For example, the program entry point @samp{main/2} may
-be declared @code{cc_multi}, and in that case the clauses
-for @code{main} are in a single-solution context.

 @item
 Any goal with no output variables is in a single-solution context.

 @item
+The goal inside a @samp{promise_equivalent_solutions} determinism cast
+is in a single-solution context.
+
+ at item
 If a conjunction is in a single-solution context, then
 the right-most conjunct is in a single-solution context,
 and if the right-most conjunct cannot fail,
@@ -3686,6 +3690,12 @@ or not.  Calls from single-solution contexts
will call the committed
 choice version, while calls which are not from single-solution contexts
 will call the backtracking version.

+You can declare the program entry point @samp{main/2} to be @samp{cc_multi},
+and in this case the entire program starts in a single-solution context.
+It can therefore produce output nondeterministically,
+without promising that the solutions are equivalent.
+This is one way to achieve ``don't care'' style nondeterminism in Mercury.
+
 There are several reasons to use committed choice determinism annotations.
 One reason is for efficiency: committed choice annotations allow
 the compiler to generate much more efficient code.
@@ -3693,7 +3703,7 @@ Another reason is for doing I/O, which is
allowed only in @samp{det}
 or @samp{cc_multi} predicates, not in @samp{multi} predicates.
 Another is for dealing with types that use non-canonical representations
 (@pxref{User-defined equality and comparison}).
-And there are a variety of other applications.
+There are a variety of other applications.

 @c XXX fix semantics for I/O + committed choice + mode inference