[m-dev.] EDCGs

[Peter Nicholas MALKIN]

Hi,

On Mon, 27 Dec 1999, Ralph Becket wrote:

> * Conjunctive Case ((L,R) is a conjunctive goal)
> 
> for all free vars X or X` occurring in (L,R),
> 	in((L,R), X) =  { in(L, X)	if X occurs in L
> 			    { in(R, X)	otherwise
> 	out((L,R), X) = { out(R, X)	if X occurs in R
> 			    { out(L, X)	otherwise
> 	(L,R)* = (L*, U, R*)				
> 		where U is a conjunction of unifications
> 		such that Y = Z in U iff out(L, X) = Z
> 		and in(R, X) = Y
> 
> * Disjunctive Case ((L;R) is a disjunctive goal)
> 
> Here we ensure that the input versions of each variable in each disjunct
> are the same and similarly for the output versions.  That is, for all
> free vars X occurring in the disjunction, in(L, X) = in(R, X) and
> out(L, X) = out(R, X).  This is achieved by extending L* and R* with
> appropriate unifications to get (L,R)*.
> 
> * Conditional Case ((if C then Y else N) is a conditional goal)
> 
> Similar to the disjunctive case, except that we have in((C,Y)*, X) = in(N,
> X)
> and out((C,Y)*, X) = out(N, X) for all X occurring in the compound goal.

Actually for if-then-elses I do not think that it is that simple. The problem
arises because any variables introduced in the conditional part of an
if-then-else that do not occur in the then part are implicitly existentially
quantified inside the conditional part. For example consider the following code:

( p(IO, IO`) ->
	Goals1
;
	Goals2
)

where IO or IO` does not occur in Goals1 or Goals2.

The correct transformation is:

( p(IO0, IO1) ->
	Goals1,
	IO2 = IO1
;
	Goals2,
	IO2 = IO0
)

NOT

( p(IO0, IO1) ->
	Goals1
;
	Goals2,
	IO0 = IO1
)

This code will produce a mode error.

The solution involves handling if-then-elses as a special case.

for all free vars X or X` occurring in (if C then Y else N),
	out((if C then Y else N), X) = newvar

	(if C then Y else N)* = (if C* then Y*,U1 else N*,U2)
		where U1 is a conjunction of unifications such that 
		M = out((if C then Y else N), X) in U1
		iff M = out(Y, X),

		where U2 is a conjunction of unifications such that
		M = out((if C then Y else N), X) in U2
		iff M = out(N, X)

NB: disjunctions can also be handled in a similar way, and then if-then-elses
will not longer be a special case (this is how I handle it, I actually have
implemented this syntax in my latest version of EDCGs).

Peter

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