[m-rev.] for review: unification expressions

[Fergus Henderson]

I'll elaborate further on the point I made earlier about order of evaluation.
According to the language reference manual, these two code fragments
are equivalent:

 |    For example
 | 
 |      p(X @ f(_, _), X).
 | 
 | is equivalent to
 | 
 |      p(X, X) :-
 |              X = f(_, _).

But in our current implementation, this is not the case,
as the following example shows.

In this example, f/2 is a function which loops;
p/2 is defined using @ as above, while q/2 is defined in
the supposedly equivalent way using a separate unification.
In the current implementation, the call to q(1, 2) fails,
whereas the call to p(1, 2) gets an infinite loop.

	:- module unify_expr_test.
	:- interface.
	:- import_module io.

	:- pred main(io::di, io::uo) is det.

	:- implementation.

	main -->
		( { q(1, 2) } ->
			print("q succeeded"), nl
		;
			print("q failed"), nl
		),
		( { p(1, 2) } ->
			print("p succeeded"), nl
		;
			print("p failed"), nl
		).

	:- pred p(int::in, int::in) is semidet.
	p(X @ f(_, _), X).

	:- pred q(int::in, int::in) is semidet.
	q(X, X) :-
		X = f(_, _).

	:- func f(int, int) = int.
	:- mode f(out, out) = in is det.
	f(X, Y) = f(X, Y).	% an infinite loop

-- 
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
--------------------------------------------------------------------------