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

[Mark Brown]

On Thu, Oct 16, 2014 at 11:43 PM, Zoltan Somogyi
<zoltan.somogyi at runbox.com> wrote:
>
>
> On Sat, 4 Oct 2014 20:37:04 +1000, Mark Brown <mark at mercurylang.org> wrote:
>> 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.
>
> Sorry for the late review, but my laptop was being repaired for the
> last few days.
>
>>  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.
>
> can AND WILL prune away ...

Ok. I have also made this point in the next section - that the
compiler WILL prune away solutions in the general case, not just MAY.

>
>> -is when you know that all the solutions returned will be equivalent.
>> +you need to allow Mercury to prune the other solutions.
>
> prune AWAY
>
>> +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.
>
> under YOUR equality theory
>
> which will prune away all solutions after the first
>
>> +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}.
>
> s/context/contexts/
> Give brief sketches of those cases before the reference.

Done. I've also changed this just to refer to the concept of "where
solutions will be pruned away", rather than forward reference the term
"single-solution contexts".

Relative diff is below.

>
> The diff is otherwise fine. It would be nice if most of this discussion
> were accompanied by examples, but that would be a separate change.

I'll see what I can come up with.

Cheers,
Mark.


diff -u b/doc/reference_manual.texi b/doc/reference_manual.texi
--- b/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -3591,16 +3591,16 @@
 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.
+so Mercury can and will prune away any potential duplicate solutions.
 Determinism analysis thus considers these goals to be
 @code{semidet} and @code{det} respectively.

 If you just want one solution and don't care which,
-you need to allow Mercury to prune the other solutions.
+you need to allow Mercury to prune away 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,
+solution under your equality theory of the output variables,
 then you can use a @samp{promise_equivalent_solutions} determinism cast,
-which will do the pruning.
+which will prune away all solutions after the first.
 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
@@ -3620,13 +3620,16 @@
 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
+These first two cases, where there are no outputs
+and where there are outputs but you only need one solution,
+are particular instances of a more general notion of pruning away solutions
+that is defined for all goals.
+The complete definition of where solutions will be pruned away
 is given in @ref{Committed choice nondeterminism}.

-If you want to combine output values from many solutions into a single result,
+The final case is that
+you want to combine output values from many solutions into a single result.
+To do this,
 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
@@ -3642,7 +3645,10 @@
 to that mode of the predicate (or function) occur in a context in
 which only one solution is needed.

-Such single-solution contexts are determined as follows.
+Such single-solution contexts determine where pruning occurs:
+for calls (of any determinism) that occur in a single-solution context,
+the compiler will ensure that all solutions after the first are pruned away.
+Single-solution contexts are defined as follows.

 @itemize @bullet
 @item