[m-rev.] For review: State Variable Transformation

[Ralph Becket]

Simon Taylor, Sunday, 21 April 2002:
> On 08-Apr-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> 
> > Index: compiler/make_hlds.m:
> > ============================
> > @@ -7218,10 +7462,14 @@
> >  		{ Det = Det1 },
> >  		{ term__coerce(GoalTerm1, GoalTerm) },
> >  		{ parse_goal(GoalTerm, VarSet0, ParsedGoal, VarSet1) },
> > +		% Note that all state variables appearing in a lambda
> > +		% are considered local to the lambda - this is a stricter
> > +		% rule than that applied to ordinary logical variables.
> 
> This is awfully counter-intuitive, and disallows sensible code such as
> 
> find_pred_names(PredIds, PredNames, !Info) :-
> 	PredNames = list__map(
> 		(func(PredId) = PredName :-
> 			module_info_name(!.Info ^ module_info,
> 				PredId, PredName)
> 		), PredIds).
> 
> > +	%	When we are processing an atomic formula (such as a call), we
> > +	%	have to ensure that for all state variables X therein, !.X and
> > +	%	!:X have the same respective substitution throughout the atom
> > +	%	and that no intermediate values for X are introduced (for
> > +	%	instance, we don't want this to happen for conjunctions in
> > +	%	the conditions of if-then-else expressions.)
> > +	%
> > +	%	Example:
> > +	%		p((if q(!.X, !:X), r(!.X, !:X) then a else b))
> > +	%
> > +	%		should be transformed into
> > +	%
> > +	%		p((if q(X0, X1), r(X0, X1) then a else b))
> > +	%
> > +	%		rather than
> > +	%
> > +	%		p((if q(X0, X1), r(X1, X2) then a else b))
> > +	%
> > +	%		since the conditional expression occurs inside an
> > +	%		atomic formula and hence cannot introduce
> > +	%		intermediary values for state variables.
> 
> This is unintuitive too. The original code may not be sensible, but
> that's no excuse for the compiler to do something totally bizarre
> with it.

These decisions were arrived at after some consideration.  There are two
options: one is to have a simple rule for the transformation that can
arguably lead to counter-intuitive situations as you point out, the
other is to have a complicated rule which makes it less obvious what the
transformation will turn out.

The simple rule is that within an atomic goal at the level of the source
as provided by the programmer, all state variable references to !.X will
map to the same logical variable, X0 for some X0, and all state variable
references to !:X will map to the same logical variable X1 for some X1.
The only exception to the rule is that all state variables in a lambda
term are local to that lambda term.

The alternative rule is much more complicated.  It would have to include
exceptions like

*1* the simple rule applies to expressions, except for the condition goals
of if-then-else expressions that reference some state variable X as
both !.X and !:X where X does not appear in the enclosing scope;

*2* the simple rule applies to lambda expressions, except where the body
of the lambda expression refers to !.X (but not !:X) where neither !.X
or !:X are referred to in the head of the lambda, in which case !.X
should be defined in the scope enclosing the lambda expression.

Exception *1* would lead to situations where

	!:X = A, p((if q(!.X, !:X), r(!.X, !:X) then U else V)), ...

would be transformed into

	X0 = A, p((if q(X0, X1), r(X0, X1) then U else V)), ...

but

	!:X = A, p((if q(!.Y, !:Y), r(!.Y, !:Y) then U else V)), ...

where state variable Y appears only in this context would be
transformed into

	X0 = A, p((if q(Y0, Y1), r(Y1, Y2) then U else V)), ...

Exception *2* would lead to situations where

	!:X = A,
	F   = ( pred(A) :- !:Y = P, ... )

would have state variable Y considered local (since it doesn't make
much sense for the body of a lambda to "update" the value of a state
variable in the surrounding context), but

	!:X = A,
	F   = ( pred(A) :- !.X = P, ... )

where the body of the lambda does not refer to !:X would have !.X
taken from the enclosing scope, yet

	!:X = A,
	F   = ( pred(A) :- !:X = P0, ..., !.X = P, ... )

would again have state variable X local in the context of the lambda
for the same reason as the example featuring !:Y.

I opted for the simple rule since, all other things being equal, it
seems to me both options can lead to potential confusion where the
notation is abused.

> Somewhere in make_hlds.m you should explain why you can't just copy
> the method used by prog_io_dcg.m for the DCG transformation --
> a forward pass over the goal inserting matching-up unifications
> at the end of if-then-elses and disjunctions. If it wasn't possible
> before, would it be possible with the requirement that state variables
> be explicitly quantified, and the assumption state variables are live
> throughout their scope?

The problem arises because state variables are more flexible than
DCGs.  DCGs have the following properties that do not apply to state
variables:
* the DCG state thread always appears in the head of the clause;
you cannot introduce a DCG thread in the middle of a clause (except
using the rather ugly DCG-lambda trick);
* there is exactly one DCG state thread;
* either a goal is in an "escaped" { } context or it isn't; if it is
then both in and out parts of the DCG thread are appended as
arguments;
* the DCG state thread cannot be referred to in expressions.

One way of tackling the problem more cleanly, perhaps, would be to
traverse the pre-HLDS structure marking each (programmer-level) atomic
goal with state variable use-def labels and then do a separate mark-up
phase.  This is similar to what my original transformation did, but
you indicated strongly that things would be better if the
transformation was done as part of the make_hlds pass!

At first glance this transformation looks simple; the trouble I've had
implementing it and the amount of discussion that has generated
indicate that the transformation is not entirely simple.

> > +	% Example (assumingPostLiveSVarSubst is [X -> X1]):
> > +	%	After transforming
> > +	%
> > +	%		p(!.X)
> > +	%	to
> > +	%		p(X0)
> > +	%
> > +	%	will be [!.X -> X0], necessitating adding a unification to
> > +	%	give
> > +	%
> > +	%		p(X0), X0 = X1
> 
> I'm missing something. Why isn't that transformed into p(X1),
> with no extra unification?

If it were possible to know at the point when the argument !.X is
encountered that !:X does not appear elsewhere in any argument to p
(or in the enclosing scope, if p itself is part of an expression) then
we could just map !.X to X1.

However, we cannot do this in a single pass, hence we map !.X to a
fresh variable X0, !:X (if it appears) to X1, and then insert the
unification X0 = X1 after p (or the atomic goal it appears in) in the
case where p (or the atomic goal it appears in) does not contain !:X.

It's cases like these that make this transformation non-trivial.

- Ralph
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------