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

[Simon Taylor]

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.

I think the problem with cases like this is that the transformation
has no concept of the scope of a state variable. My suggestion
would be to require that state variables be explicitly quantified,
where the occurrence of a state variable in the head of a clause or
a lambda expression quantifies that state variable over the entire
clause or lambda expresion. I would expect that explicit quantifiers
would be very rare. The syntax for explicit quantification of state
variables would be `some [!X] Goal'.

An occurrence of `!:X' within a lambda expression or an if-then-else
expression for a state variable non-local to that expression would
be an error.

Requiring explicit quantification would also allow good error messages
for singleton state variables caused by typos.

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?

> +	% 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?

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