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

[Peter Ross]

On 29-Mar-2000, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> 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.
> 

There is no good reason apart from the fact that it isn't implemented.
I also believe it would be more difficult to match on the = form as you
no longer have the <=> to divide the LHS and RHS.

I will put it down on the TODO list though.

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

How about

This construction equivalence law is useful for transforming predicates
into a tail recursive form, please see "Making Mercury Programs Tail
Recursive", available from http://www.cs.mu.oz.au/mercury, for more
information.


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

I have changed it to `order independent state update property', which is
the name we use in the paper.

The reason why it is a bit like commutativity is that a predicate which
has the properties of commutativity and associativity implies the order
independent state update property.

However the converse assumption is a seductively dangerous fallacy (to
quote my Physical Electronics lecturer).


> > % 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'.
> 

Yes, a cut and paste error.


> > % 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?
> 
Hysterical raisons.  I will change it to be a enumeration type.


> How is the second int encoded -- starting at zero or one?
> 
It doesn't matter, as long as a goal that appears earlier in the body
has a lower number then one that appears later.


> > :- 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 = []'
> 
Done.


> 		(	
> 			{
> 		->
> 
> > 					words("If a predicate has been"),
> > 					words("declared associative via"),
> > 					words("a promise declaration,"),
> 
> I suggest s/promise/`promise'/
> 
Done.

> > 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".
> 
Done.

> > 	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.
> 
OK, but only under duress. ;)


> > 	%
> > 	% 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?
> 
I just haven't ported those cases from my original code yet.  It is just
a SMOP and will be implemented next.


> > :- type store_info
> > 	--->	store_info(
> > 			int,
> > 			instmap,
> > 			goal_store
> > 		).
> 
> What does this type represent?
> In particular, what does the `int' field represent?
> 

How about.

        % The store info is folded over the list of goals which
        % represent the base and recursive case conjunctions.
:- type store_info
        --->    store_info(
                        int,            % the location of the goal in
                                        % the conjunction.
                        instmap,
                        goal_store
                ).
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------