[mercury-users] Mutual Exclusivity & Exhaustiveness

[Ralph Becket]

Simon Taylor, Thursday,  3 January 2002:
> 
> 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'.

Good point.

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

I like this syntax suggestion.

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

Why is that necessary?  I might want to say something like

:- promise_exclusive(X::ground, Y::ground) is semidet :-
	(	X = 0
	;	X `is_positive_divisor_of` Y
	).

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

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