[mercury-users] Mutual Exclusivity & Exhaustiveness

[Simon Taylor]

On 03-Jan-2002, Lars Yencken <lljy at students.cs.mu.oz.au> wrote:
> I'm digging up the topic of mutual exclusivity and exhaustiveness
> declarations again, in the interest of actually developping them. For
> past posts on this topic, do a search for determinism detection on the
> mailing lists. The declarations I had in mind were quite simple, like
> these below:
> 
> :- exclusive X < A, X = A, X > A.
> 
> :- exhaustive X < A, X = A, X > A.

You need to be able to declare the required instantiatedness of the
non-local variables for the pattern to match. You don't want to use
the rule `:- exclusive X = [], X = [_|_]' when X is not bound.

It should be explicitly stated in the declaration that the programmer
is making a promise that the compiler cannot check, so use
`promise_exclusive' rather than `exclusive'.

I'd suggest something like this:

	% exhaustive match.
:- promise_exclusive(X::ground, Y::ground) is det :-
	( X < Y
	; X = Y
	; X > Y
	).

	% non-exhaustive match.
:- promise_exclusive(X::ground, Y::ground) is semidet :-
	( foo(X, Y)
	; bar(X, Y)
 	).

Restrictions:
1. The insts of the arguments must bound or ground insts (not `free' or `any').
2. All of the variables in the head of the rule must appear in each disjunct.
3. Other variables are local to the disjunct in which they appear and must
   appear only once.
4. Each disjunct must be a call or a var-var or var-functor unification.
5. Arguments of a call or a functor must be variables.

These restrictions avoid the need to match against multiple goals.

Simon.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------