[m-rev.] for review: unification expressions

[Simon Taylor]

Fergus, is this change OK?

Simon.


On 23-Nov-2001, Simon Taylor <stayl at cs.mu.OZ.AU> wrote:
> --- 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
--------------------------------------------------------------------------