[m-rev.] for review: unification expressions

[Fergus Henderson]

On 02-Nov-2001, Simon Taylor <stayl at cs.mu.OZ.AU> wrote:
> 
> Add unification expressions, written `X @ Y', to the language. 
> `X @ Y' unifies X and Y and returns the result. Unification
> expressions can make switches more compact.
...
> + at node Unification expressions
> + at subsection Unification expressions
> +
> +A unification expression is an expression of the form
> + at example
> +X @@ Y
> + at end example
> +where @var{X} and @var{Y} are data-terms.

There should be an `@noindent' after the `@end example'.

Also, from the texinfo documentation:

 | 	To make the output look good, you should put a blank line before
 | 	the `@example' and another blank line after the `@end example'.

I'm not sure that we consistently follow this advice in the Mercury
reference manual, but you should at least consider it.

> +The semantics of a unification expression is that @var{X} and @var{Y}
> +are unified, and the expression is equivalent to the unified value.

Hmm... this is at about the same level of formality as the
documentation for other data-terms, such as if-then-else expression.
However, the documentation here doesn't really explain how this
construct differs from an ordinary user-defined function, e.g.

	:- func T `at` T = T is semidet.
	X `at` X = X.

Also, somewhere in the language reference manual, we ought
to explain the order of evaluation for unification expressions.
This has effects for both determinism analysis and program termination.

For example, a goal such as

	X = Y @ Z

will be equivalent to a conjunction of two of the
three possible unifications X = Y, X = Z, and Y = Z.
If X, Y, or Z are function calls, then the choice
of which two and the ordering of the conjunction
can affect determinism correctness (since switch
detection does not look past the first function call)
and/or whether the program terminates.

Of course the conjunction will be reordered to ensure
mode correctness, and in the commutative semantics,
the final execution order will be unspecified anyway.
But nevertheless the order should be specified,
so that it is clear what ordering mode analysis
starts with, which determines what ordering is used for
determinism analysis and for the strict sequential semantics.

There should also be some test cases in the test suite
to ensure that the correct order is used.

> Unification expressions are most useful when writing switches
> @pxref{Determinism checking and inference}.

That is not correctly punctuated.
Either put a semi-colon after "switches",
or put a full stop and change @pxref to @xref,
or put the @pxref{...} inside parentheses.

> +++ library/ops.m	2 Nov 2001 09:13:02 -0000
> @@ -164,6 +164,7 @@
>  ops__op_table(">=", after, xfx, 700).		% standard ISO Prolog
>  ops__op_table(">>", after, yfx, 400).		% standard ISO Prolog
>  ops__op_table("?-", before, fx, 1200).		% standard ISO Prolog (*)
> +ops__op_table("@", after, xfx, 90).		% standard ISO Prolog

The comment here is wrong.  It should say "Mercury extension".

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------