[m-dev.] for review: update state transformation

[Fergus Henderson]

On 29-Mar-2000, Peter Ross <petdr at cs.mu.OZ.AU> wrote:

> library/int.m:
>     Add associativity declarations for + and *.

Hmm... that might be a bit problematic in future,
if/when we add (optional) range checking for ints.

In particular, the accumulator transformation could then transform a program
which does not overflow into one that does overflow.

Well, I suppose we can deal with that issue if/when we add
range checking.  Just something to bear in mind...

> Index: library/int.m
...
> -	% commutivity of +
> +	% commutivity and associativity of +
>  :- promise all [A,B,C] ( C = B + A <=> C = A + B ).
> +:- promise all [A,B,C,ABC] ( ABC = (A + B) + C <=> ABC = A + (B + C) ).
>  
> -	% commutivity of *
> +	% commutivity and associativity of *
>  :- promise all [A,B,C] ( C = B * A <=> C = A * B ).
> +:- promise all [A,B,C,ABC] ( ABC = (A * B) * C <=> ABC = A * (B * C) ).

Is there some reason why they can't be written as just

	:- promise all [A,B,C] ( A * B = B * A ).
	:- promise all [A,B,C] ( (A * B) * C = A * (B * C) ).
	
?

If so, I think it would be a good idea to document that reason.

> Index: library/list.m
...
> +	% construction equivalence law.
> +	% XXX when we implement rewrite rules change this law to a
> +	% rewrite rule.
> +:- promise all [L,H,T] ( append([H], T, L) <=> L = [H|T] ).

I think it would be a good idea to document why this rule is
worth declaring.

> Index: compiler/accumulator.m
...
> % Attempts to transform a single proc to a tail recursive form by
> % introducing accumlators.  The algorithm can do this if the code after
> % the recursive call has either the state update or associative
> % property.
> %
> % /* State update property */
> % :- promise all [A,B,S0,S]
> % 	(
> % 		(some[SA] (update(A, S0, SA), update(B, SA, S)))
> % 	<=>
> % 		(some[SB] (update(B, S0, SB), update(A, SB, S)))
> % 	).	

Hmm, that name is not a great name for that property.
There are many predicates which I would think of as
"state update predicates", for example `io__set_exit_status',
which do not have that property.

Perhaps "Commutative state update property" would be a better name.
It's not commutativity, but it is a bit like commutativity,
as the following alternative way of expressing it shows:

    :- promise all [A, B]
	((pred) --> update(A), update(B)) = ((pred) --> update(B), update(A)).

Note that currently this is not legal Mercury syntax,
because we require mode and determinism annotations on lambda expressions.
This is necessary in goals, but it is not necessary in
`:- promise' declarations (which do not need to be mode-correct),
so it might be nice to relax that restriction so that
it only applies to goals that need to be mode-correct.
(As a side effect, this change would help the compiler
give better error messages in the case where you forget
these annotations.)

Currently you would have to insert some dummy modes, e.g.

    :- promise all [A, B]
	(pred(in, in) is semidet --> update(A), update(B)) =
	(pred(in, in) is semidet --> update(B), update(A)).

> % The transformation recognises predicates in the form
> %
> % p(In, OutUpdate, OutAssoc) :-
> % 	minimal(In),
> % 	initialise(OutUpdate),
> %	base(OutAssoc).
> % p(In, OutUpdate, OutAssoc) :-
> % 	decompose(In, Current, Rest),
> % 	p(Rest, OutUpdate0, OutAssoc0),
> % 	update(Current, OutUpdate0, OutUpdate),
> % 	assoc(Current, OutAssoc0, OutAssoc).
> %
> % which can be transformed by the algorithm in "State Update
> % Transformation" to
> %
> % p(In, OutUpdate, OutAssoc) :-
> % 	initialise(AccUpdate),
> % 	p_acc(In, OutUpdate, OutAssoc, AccUpdate).
> %
> % p_acc(In, OutUpdate, OutAssoc, AccUpdate) :-
> % 	minimal(In),
> % 	base(OutAssoc),
> % 	OutUpdate = AccUpdate.
> % p_acc(In, OutUpdate, OutAssoc, AccUpdate0) :-
> % 	decompose(In, Current, Rest),
> % 	update(Current, AccUpdate0, AccUpdate),
> % 	p_acc(Rest, OutUpdate, OutAssoc0, AccUpdate),
> % 	compose(Current, OutAssoc0, OutAssoc).

Shouldn't `compose' here be `assoc'?
The first code fragment contains a call to `assoc',
where the second code fragment contains a call to `compose'.

> % Note that if the recursive clause contains multiple calls to p, the
> % transformation is attempts to move each recursive call to the end

s/is attempts/attempts/

> 	% A goal is represented by two integers, the first integer
> 	% stores which conjunction the goal came from (base or
> 	% recursive), and the second stores the location of the goal in
> 	% the conjunction.
> :- type goal_id == pair(int).

How is the first int encoded?  Why use an int rather than
an enumeration type?

How is the second int encoded -- starting at zero or one?

> :- type warning 
> 			% warn that two prog_vars in call to pred_id
> 			% at prog_context were swapped, which may cause
> 			% an efficiency problem.
> 	--->	w(prog_context, pred_id, prog_var, prog_var).

I suggest s/w/warn/

> :- type warnings == list(warning).
> 
> %-----------------------------------------------------------------------------%
> 
> 	%
> 	% process_proc
> 	%
> 	% Attempt to transform one procedure into a accumulator
> 	% recursive form.

s/one/a/
s/a //

> process_proc(PredId, ProcId, ProcInfo0, ProcInfo, 
> 		ModuleInfo0, ModuleInfo) -->
...
> 		globals__io_lookup_bool_option(inhibit_accumulator_warnings,
> 				InhibitWarnings),
> 		(
> 			{ not (InhibitWarnings = no, Warnings \= []) }
> 		->

I think it would be clearer to avoid the double negation and write that
condition as `InhibitWarnings = yes ; Warnings = []'

		(	
			{
		->

> 					words("If a predicate has been"),
> 					words("declared associative via"),
> 					words("a promise declaration,"),

I suggest s/promise/`promise'/

> output_warning(w(Context, PredId, VarA, VarB), VarSet, ModuleInfo,
> 		Context, Formats) :-
> 	error_util__describe_one_pred_name(ModuleInfo, PredId, PredStr),
> 	varset__lookup_name(VarSet, VarA, VarAStr),
> 	varset__lookup_name(VarSet, VarB, VarBStr),
> 	Formats = [words("warning: the call to"), words(PredStr),
> 			words("has had the location of the variables"),
> 			words(VarAStr), words("and"), words(VarBStr),
> 			words("swapped to allow accumulator introduction.")
> 			].

The predicate name and variable names should be inside single quotes, e.g.
"`Foo'" rather than "Foo".

> 	standardise(Goal0, Goal),
> 
> 	identify_goal_type(PredId, ProcId, Goal, TopLevel, Base, Rec),
> 
> 	C = initialise_goal_store(Rec, Base, InitialInstMap),

I suggest s/standardise/standardize/g
and s/initialise/initialize/g,
for consistency with the spelling used in (most of)
the rest of the compiler.

> 	%
> 	% This predicate takes the original goal and identifies the
> 	% `shape' of the goal around the recursive and base cases.
> 	% Note that the base case can contain a recursive call, as the
> 	% transformation doesn't depend on what is in the base case.
> 	%
> :- pred identify_goal_type(pred_id::in, proc_id::in, hlds_goal::in,
> 		top_level::out, hlds_goals::out, hlds_goals::out) is semidet.
> 
> identify_goal_type(PredId, ProcId, Goal, Type, Base, Rec) :-
> 	(
> 		Goal = switch(_Var, _CanFail, Cases, _StoreMap) - _GoalInfo,
> 		Cases = [case(_IdA, GoalA), case(_IdB, GoalB)],
> 		goal_to_conj_list(GoalA, GoalAList),
> 		goal_to_conj_list(GoalB, GoalBList)
> 	->
> 		(
> 			is_recursive_case(GoalAList, proc(PredId, ProcId))
> 		->
> 			Type = switch_rec_base,
> 			Base = GoalBList,
> 			Rec = GoalAList
> 		;
> 			is_recursive_case(GoalBList, proc(PredId, ProcId))
> 		->
> 			Type = switch_base_rec,
> 			Base = GoalAList,
> 			Rec = GoalBList
> 		;
> 			fail
> 		)
> 	;
> 		fail
> 	).

Hmm... what about the other possible values for `Type',
e.g. when the goal is an if-then-else or a (semidet?) disjunction?

> :- type store_info
> 	--->	store_info(
> 			int,
> 			instmap,
> 			goal_store
> 		).

What does this type represent?
In particular, what does the `int' field represent?

[... to be continued ...]

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------