[m-dev.] Fw: Replacement syntax for DCGs

[Ralph Becket]

Okay, here's a spec. for the DCG replacement syntax translation that was
discussed last month.

To recap, the idea is to support multiple "state variables" explicitly
and more elegantly than is the case for DCGs and EDCGs.

Syntactically, a "state variable" is identified by a `!' prefix.  At
each call site, every state variable X in scope has a "current" value
denoted !+X and a "next" value denoted !-X.

For convenience, an argument !X is syntactic sugar for two real
arguments !+X, !-X (that is, io__print("Hello", !IO) is shorthand for
io__print("Hello", !+IO, !-IO)).

As with (E)DCGs, lexical order matters: the value !-X in one call is the
same as !+X in the immediately following call.

It is an error for a state variable to share a name with a normal
variable (that is, a clause cannot simultaneously refer to both X and
any of !+X, !-X or !X).

Some preliminaries:

We define a function sv computing the set of state variables in a
formula in superhomogenous normal form:

	sv((H :- B))      = sv(H) u sv(B)
	sv((P, Q))        = sv(P) u sv(Q)
	sv((P ; Q))       = sv(P) u sv(Q)
	sv((not P))       = sv(P)
	sv((some Xs P))   = sv(P) \ (state variables in Xs)
	sv(p(X1, .., Xn)) = {X | Xi = !+X or Xi = !-X}

We define a current/next substitution s over a set of variables Xs to be

	cns(Xs) = {X -> <X', X''> | X in Xs, X' and X'' fresh variables}

If S is a current/next substitution then we define
- S maps X to mean there is a mapping for X in S,
- the substitution !+X.S = X'  where X -> <X', X''> in S
- the substitution !-X.S = X'' where X -> <X', X''> in S
- the substitution   X.S = X   for non-state variables X.

We lift substitution to cover calls as p(X1, .., Xn).S = p(X1.S, .., Xn.S)

We define a split function over current/next substitutions:

	split(S) = <Sa, Sb>
		s.t. all [X]
			X -> <X', X''> in S
		<=>
			X -> <X', X'''>  in Sa and
			X -> <X''', X''> in Sb
			for some fresh variable X'''.

Now we can define the translation t from SHNF with state variables to
vanilla SHNF:

	t((H :- B)) = (H.S :- t(B, S))
		where S = cns(sv((H :- B)))
		
and...

	t((P, Q), S)  = (t(P, Sa), t(Q, Sb))
		where <Sa, Sb> = split(S)

	t((P ; Q), S) = (t(P, S) ; t(Q, S))

	t((not P), S) = (not t(P, S), unifiers(emptyset, S))

	t((some Xs P), S) = (some Xs.S' t(P, S'))
		where S' = S u cns(state variables in Xs)

	t(p(X1, .., Xn), S) = (p(X1, .., Xn).S, unifiers({X1, .., Xn}, S))

where

	unifiers(Xs, S) = t((!+X1 = !-X1, .., !+Xn = !-Xn), S)
		where {X1, .., Xn} = {X | S maps X and !-X not in Xs}

(I need to extend this to cover lamdas.)

I'd be interested in any comments people have.

Cheers,

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