[m-dev.] Determinism Declarations

[Lars Yencken]

Hi everyone,

Here's the agreed upon syntax for mutual exclusivity and exhaustiveness
declarations to be developed. Here are examples of each which reflect some of
the different ways existentially quantified variables can be handled.

Mutual exclusivity:

	:- all [X, Y] promise_exclusive
		some [Z] (
			p(X, Y, Z)
		;
			q(X, Y, Z)
		).

Exhaustiveness:

	:- all [X] promise_exhaustive
		(
			p(X, _)
		;
			q(X, _)
		).

Both together:

	:- all [X] promise_exclusive_exhaustive
		some [Y] (
			p(X, Y)
		;
			q(X, Y, Z)
		).

All three declarations are restricted in the following ways:

1. Every variable that occurs in more than one disjunct must be explicitly
   quantified.
2. Any variable occuring in only one disjunct is existentially quantified. This
   is similarly applicable when an underscore is used in place of a variable.
3. Each disjunct must be a call or a var-var or var-functor unification.
4. Arguments of a call or a functor must be variables.

If this deviates at all from what was agreed on at today's Mercury meeting, 
please correct me. Otherwise, consider these declarations under development.

Lars
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------