[m-rev.] for review: unification expressions

[Simon Taylor]

--- doc/reference_manual.texi
+++ doc/reference_manual.texi
@@ -1078,2 +1078,2 @@
-The semantics of a unification expression is that @var{X} and @var{Y}
-are unified, and the expression is equivalent to the unified value.
+The meaning of a unification expression is that the arguments are unified,
+and the expression is equivalent to the unified value.
@@ -1081,8 +1081,4 @@
- at w{@code{Z = X @@ Y}} is equivalent to the conjunction
- at w{@code{Z = X, Z = Y}}.
-
-Unification expressions are most useful when writing switches
-(@pxref{Determinism checking and inference}).  The arguments
-of a unification expression are examined when checking for
-switches.  The arguments of an equivalent user-defined function
-would not be.
+The operational semantics of an expression @w{@code{X @@ Y}}
+is that the expression is replaced by a fresh variable @var{Z}, and
+immediately after @var{Z} is evaluated, the conjunction
+ at w{@code{Z = X, Z = Y}} is evaluated.
@@ -1100,4 +1096,4 @@
-p(Y, Z) :-
-        Y = X,
-        Y = f(_, _),
-        Z = X.
+p(H1, H2) :-
+        H1 = X,
+        H1 = f(_, _),
+        H2 = X.
@@ -1104,0 +1101,6 @@
+
+Unification expressions are most useful when writing switches
+(@pxref{Determinism checking and inference}).  The arguments
+of a unification expression are examined when checking for
+switches.  The arguments of an equivalent user-defined function
+would not be.
--- tests/hard_coded/unify_expression.exp
+++ tests/hard_coded/unify_expression.exp
@@ -2,0 +3 @@
+r failed (as expected)
--- tests/hard_coded/unify_expression.m	12 Nov 2001 11:08:18 -0000	1.1
+++ tests/hard_coded/unify_expression.m	22 Nov 2001 21:03:06 -0000
@@ -8,7 +8,7 @@
 
 :- implementation.
 
-:- import_module require.
+:- import_module require, std_util.
 
 :- type t
 	--->	f(int, int)
@@ -19,11 +19,38 @@
 		io__write(X),
 		io__nl
 	;
-		io__write_string("failed\n")
+		io__write_string("Error: p failed\n")
+	),
+	( { q(1, 2) } ->
+		print("Error: q succeeded"), nl
+	;
+		print("q failed (as expected)"), nl
+	),
+
+	( { r(1, 2) } ->
+		print("Error: r succeeded"), nl
+	;
+		print("r failed (as expected)"), nl
 	).
 
 :- pred p(t::in, t::out) is semidet.
 
 p(X @ f(_, _), X).
 p(g(X @ f(_, _)), X).
-p(g(g(_)), _) :- error("p").
+
+:- pred q(int::in, int::in) is semidet.
+q(X, X @ g(_, _)).
+
+:- pred r(int::in, int::in) is semidet.
+r(X, X @ g(1, 2)).
+
+:- func g(int, int) = int.
+:- mode g(in, in) = out is semidet.
+:- mode g(out, out) = in is semidet.
+g(1, 2) = X :-
+	( semidet_succeed ->
+		error("g called")
+	;
+		X = 3
+	).
+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------