[m-dev.] for review: document promise_only_solution/1 in lang ref man

[Fergus Henderson]

Estimated hours taken: 0.75

doc/reference_manual.texi:
	Replace some old documentation about a planned
	`unique [X]' quantifier with a description of
	the `promise_only_solution' function in the
	standard library.

Workspace: /d-drive/home/hg/fjh/mercury
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.174
diff -u -d -r1.174 reference_manual.texi
--- doc/reference_manual.texi	2000/02/16 08:36:08	1.174
+++ doc/reference_manual.texi	2000/02/17 13:27:27
@@ -2370,34 +2370,43 @@
 but no matter which order you remove them,
 the maximum value in the set should be the same.
 
-We may eventually extend Mercury to allow users to write
+If you know that there will only ever be at most one distinct
+solution, then you can use the function
+ at samp{promise_only_solution/1}, which is defined
+as a builtin function in the Mercury standard library.
 
 @example
-unique [X] Goal
+:- func promise_only_solution(pred(T)) = T.
+:- mode promise_only_solution(pred(out) is cc_multi) = out is det.
+:- mode promise_only_solution(pred(out) is cc_nondet) = out is semidet.
 @end example
 
 @noindent
-as a special quantifier, meaning
-``there exists a unique @code{X} for which @samp{Goal} is true''.
-This would allow the implementation
-to prune alternative solutions for @samp{Goal}
-if @samp{X} was the only output variable of @samp{Goal}.  
+A call to that function, e.g. @samp{promise_only_solution(Pred)}, constitutes a
+promise on the part of the caller that the argument @samp{Pred} has at most
+one solution, i.e. that
+
+ at example
+not some [X1, X2] (Pred(X1), Pred(X2), X1 \= X2)
+ at end example
 
+ at noindent
+holds.  @samp{promise_only_solution(Pred)} presumes that this
+assumption is satisfied, and returns the value of @samp{X} for which
+ at samp{Pred(X)} is true, if any.  If the assumption is not
+satisfied, then the behaviour is undefined.
+
 Note that specifying a user-defined equivalence relation
 as the equality predicate for user-defined types (@pxref{Equality preds})
-means that the @samp{unique} quantifier
-could be used to express more general forms of equivalence.
+means that the @samp{promise_only_solution/1} function
+can be used to express more general forms of equivalence.
 For example, if you define a set type which represents sets as unsorted lists,
 you would want to define a user-defined equivalence relation for that type,
 which could sort the lists before comparing them.
-The @samp{unique} quantifier could then be used for sets
+The @samp{promise_only_solution/1} function 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.
 
-Currently the language does not support the @samp{unique} quantifier. 
-(However, it is possible to achieve a similar effect by using the C interface
-to type-cast a higher-order predicate term.)
-
 @node Committed choice nondeterminism
 @section Committed choice nondeterminism
 
 

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------