[mercury-users] Mutual Exclusivity & Exhaustiveness

[Simon Taylor]

On 03-Jan-2002, Lars Yencken <lljy at students.cs.mu.oz.au> wrote:
> > We definitely want to disallow examples like:
> > 
> > :- promise_exclusive(X::ground, Y::ground) is det :-
> > 		( foo(X)
> > 		; bar(X, Y)
> > 		; baz(Y)
> > 		).
> 
> If there was a case where this was useful, why would we definitely want to 
> disallow it, aside from simplicity's sake?

There are two cases where it would make sense for foo(X) and baz(Y)
to be mutually exclusive.

1. One of them can never succeed (it has determinism `failure' or `erroneous').
   This case does not need a `promise_exclusive' declaration.

2. They are impure, and the mutual exclusivity is as a result
   of some hidden state.

For example: 

:- pragma c_code("int state = 1;").

:- semipure pred state is semidet.
:- pragma c_code(state, "SUCCESS_INDICATOR = state;").

:- semipure pred not_state is semidet.
:- pragma c_code(not_state), "SUCCESS_INDICATOR = !state;").

:- promise_exclusive is det where ( state ; not_state ).

This case should be rare enough that it can be ignored.
Even when it does occur, I think it is so non-obvious
that an explicit if-then-else should be required.

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