[m-dev.] for review: accumulator.m 2

[Fergus Henderson]

On 01-Jul-1998, Peter David ROSS <petdr at students.cs.mu.oz.au> wrote:
> % The code looks for procedures which are in the following form (Y is a 
> % set of variables).

"Y" doesn't occur below.  Did you mean "Ys"?

Shouldn't *all* the variables in the example below stand for sets of
variables?

> % :- pred p(T::in, U::out) is SomeMode.
> % p(X,Ys) :-
> % 	minimal(X),
> % 	identity(Ys).
> % p(X,Ys) :-
> % 	decompose(X, Xh, Xr),
> % 	p(Xr, Y0s),
> % 	compose(Xh, Y0s, Ys).
> %
> % Then as long as the compose section of the predicate is assocative
> % (the difficult bit) then the code can be transformed into
> %
> % p(X,Ys) :-
> % 	identity(As),
> % 	p'(X, As, Ys).
> %
> % p'(X, As, Ys) :-
> % 	minimal(X),
> % 	Ys = As.
> % p'(X, As, Ys) :-
> % 	decompose(X, Xh, Xr),
> % 	compose(Xh, As, A1s),
> %	p'(Xr, A1s, Ys).
...
> 	%
> 	% accumulator__setup
> 	%
> 	% is the preliminary phase of the transform.
> 	%
> 	% Output Vars:
> 	%
> 	% AllInVars 
> 	%   will be the set of variables which will be ground at the
> 	%   start of the call to accumulator version of the proc.
> 	% RecOutVars 
> 	%   will be the set of variables which will need to be
> 	%   accumulated.
> 	% SwitchModeVars 
> 	%   will be the set of variables which will have their mode
> 	%   transformed from output to input.
> 	% AccGoals
> 	%   will be the goals used to initialise the accumulators.
> 	% BaseGoals
> 	%   will be the goals which need to be left in the original base
> 	%   case.

I'm having difficulty identifying the correspondence between the
variable names used here, and the stuff in the original example
at the top.  Could you explain what the value of each of these
is supposed to be for the original example?

> 		% ... dynamic var then it can't have its (XXX Finally you
> 		% are getting through to me Fergus ;) ) accumulator

You should delete that (XXX ... ;) ) comment before committing ;-)

P.S. s/me Fergus/me, Fergus/ ;-)

> 	%
> 	% accumulator__construct_acc_pred
> 	%
> 	% this predicate creates the accumulator version of the proc and
> 	% then fills it out, provided that the list of goals that are in
> 	% the "Compose" goal are assocative.

I suggest adding "If they are not associative, this predicate will fail.".

> 	%
> 	% accumulator__classify_vars
> 	%
> 	% Classify the vars into 3 sets:
> 	% 	InVars: 	are the set of vars which are input in the 
> 	% 			head 
> 	%       RecOutVars:	Those variables which are being
> 	%       		accumulated
> 	%       NonRecOutVars:	Those variables which are output in both
> 	%       		the internal recursive call and in the
> 	%       		head of the goal.

Again, please explain what these would be for the original example
at the top of the module.

Are these 3 sets supposed to be mutually exclusive?
Are all variables supposed to fall into one of these categories?

What should happen for variables which have modes `free -> free',
`any -> any', `free -> bound(f(free))', or `bound(f(free)) -> ground',
for example?

Please document what is supposed to happen in those cases,
and why.

(Then I may have some chance of verifying that the code does what you
think it is supposed to do, and that what you think it is supposed to
do is correct.  Currently I'm still finding it very difficult to verify
either of those.)

> 	%
> 	% accumulator__parse_base_goal(G, D0, D, A, B)
> 	% 
> 	% Divide the goal G into two lists of goals A and B.  A is the
> 	% list of goals which must be used to initialise the
> 	% accumulators.  B is the list of goals which must be left in
> 	% the original base case.
> 	%
> 	% D0 should be initialised to the set of variables which are
> 	% ground at the beginning of G.
> 	%

Again, is `ground' correct here?  Why not `bound'?
What about variables whose inst is unknown (`any')?

Please document the intended behaviour for those cases,
and the rationale for that behaviour.

> 	%
> 	% Ensure that each goal is atomic and determine whether or not
> 	% the goal is used to initialise an accumulator or not.
> 	%
> 	% The goals must be atomic because the base case is used to
> 	% initialise the accumulators.  If, for example, the base case
> 	% contained an if-then-else it cannot be determined whether the
> 	% condition will fail or succeed when we are initialising the
> 	% accumulators so it is impossible to determine what to
> 	% initialise the accumulators to.

I don't understand.

Can't you just copy the `identity(Ys)' goal (see the example at the
top) which initializes the variables, regardless of whether this
goal is atomic or whether it contains an if-then-else?

> 	% XXX In the future this should be extended to check whether or
> 	% not the goals inside the non-atomic goal are actually used to
> 	% initialise any of the accumulators if not we should keep the
> 	% goals.

Hmm, that still doesn't explain it for me.

P.S. You should add some punctuation to that sentence.

> 	%
> 	% accumulator__create_acc_vars 
> 	% 
> 	% creates all the variables which will hold accumulators and
> 	% associates those variables with the correct Y and Y0.
> 	%
> accumulator__create_acc_vars([OutVarInfo | OutVars], VarSet0, VarTypes0, 
...
> 	in_mode(AccMode),

The specification (i.e. the documentation) for that predicate
doesn't say anything about modes.

Here you're assuming that they will have mode `ground -> ground';
is that correct?

> 	%
> 	% accumulator__change_modes_to_input
> 	%
> 	% Swap the modes of all the vars in the list to input.

s/Swap/Set/

> :- pred accumulator__instmap_delta(list(var), instmap_delta, instmap_delta).
> :- mode accumulator__instmap_delta(in, in, out) is det.
> 
> accumulator__instmap_delta([], I, I).
> accumulator__instmap_delta([Var | Vars], InstMapDelta0, InstMapDelta) :-
> 	instmap_delta_insert(InstMapDelta0, Var, ground(shared,no), 
> 		InstMapDelta1),
> 	accumulator__instmap_delta(Vars, InstMapDelta1, InstMapDelta).

A comment explaining this predicate would be helpful.

Here again you're assuming that the variables will have final
inst `ground'; is that correct?

I'd like to see a test case that tests that this module does not
cause the generation of incorrect code for `any' insts.

> accumulator__create_base([AccVar | AccVars], AccGoals) :-
> 	AccVar = acc_var(var_info(Y,_),A,_,_),

s/,/, /g

> 
> 
> :- pred accumulator__acc_unification(var, var, hlds_goal).
> :- mode accumulator__acc_unification(in, in, out) is det.
> 
> accumulator__acc_unification(A, Y, Goal) :-
> 	out_mode(LHSMode),
> 	in_mode(RHSMode),
> 	UniMode = LHSMode - RHSMode,
...
> 	instmap_delta_from_assoc_list([Y - ground(shared, no)], InstMapDelta),

Here again you are assuming `in' and `out' modes;
is that correct?

> accumulator__check_assoc_2(if_then_else(Vars, Cond0, Then0, Else0, SM),
> 		Rename0, Rename, 
> 		if_then_else(Vars, Cond, Then, Else, SM)) :-
> 	accumulator__check_assoc(Cond0, Rename0, Rename1, Cond),
> 	accumulator__check_assoc(Then0, Rename1, RenameIfThen, Then),
> 	accumulator__check_assoc(Else0, Rename0, RenameElse,Else),
> 
> 	Rename0 = rename(Ys, Y0s, ModuleInfo, DynamicSet0, _, OrigDynMap, 
> 			PrevCallMap),
> 	RenameList = [RenameIfThen, RenameElse], 
> 
> 	list__map(rename_dynamic, RenameList, DynamicSets),
> 	list__map(rename_static, RenameList, StaticSets),
> 	set__list_to_set(DynamicSets, PowerDynamicSet),
> 	set__list_to_set(StaticSets, PowerStaticSet),
> 	set__power_union(PowerDynamicSet, DynamicSet),
> 	set__power_intersect(PowerStaticSet, StaticSet),

I think it would be simpler, and more efficient, to write

	rename_dynamic(RenameIfThen, IfThenDynamicSet),
	rename_dynamic(RenameElse, ElseDynamicSet),
	set__union(IfThenDynamicSet, ElseDynamicSet, DynamicSet),

	rename_static(RenameIfThen, IfThenStaticSet),
	rename_static(RenameElse, ElseStaticSet),
	set__intersect(IfThenStaticSet, ElseStaticSet, StaticSet),

instead of the 7 lines of code above.

> :- pred accumulator__check_assoc_goallist(list(hlds_goal), rename,
> 						rename, list(hlds_goal)).
> :- mode accumulator__check_assoc_goallist(in, in, out, out) is semidet.
> 
> accumulator__check_assoc_goallist([], Rename, Rename, []).
> accumulator__check_assoc_goallist([G0 | Gs0], Rename0, Rename, [G | Gs]) :-
> 	accumulator__check_assoc(G0, Rename0, Rename1, G),
> 	accumulator__check_assoc_goallist(Gs0, Rename1, Rename, Gs).

This is a somewhat strange order of arguments.
I suggest you swap the order of the last two arguments.

> 	%
> 	% accumulator__check_assoc_disj
> 	%
> 	% Check each arm of the disjunct and ensure that no matter what
> 	% path taken through the disjuncts it is still assocative.
> 	%
> :- pred accumulator__check_assoc_disj(list(hlds_goal), rename,
> 		rename, list(hlds_goal)).
> :- mode accumulator__check_assoc_disj(in, in, out, out) is semidet.
> 
> accumulator__check_assoc_disj(Gs0, Rename0, Rename, Gs) :-
> 	accumulator__check_assoc_disj_2(Gs0, Rename0, RenameList, Gs),
> 
> 	Rename0 = rename(Ys, Y0s, ModuleInfo, DynamicSet0, _, OrigDynMap, 
> 			PrevCallMap),
> 
> 	list__map(rename_dynamic, RenameList, DynamicSets),
> 	list__map(rename_static, RenameList, StaticSets),
> 	set__list_to_set(DynamicSets, PowerDynamicSet),
> 	set__list_to_set(StaticSets, PowerStaticSet),
> 	set__power_union(PowerDynamicSet, DynamicSet),
> 	set__power_intersect(PowerStaticSet, StaticSet),
> 
> 		%
> 		% We can only have a disjunction if each arm of the
> 		% disjunction only updates static variables.
> 		%
> 	DynamicSet = DynamicSet0,
> 
> 	Rename = rename(Ys, Y0s, ModuleInfo, DynamicSet, StaticSet, 
> 			OrigDynMap, PrevCallMap).

Oh, now I think I understand why the code for if-then-else was
the way it was.  I suggest you make the body of that predicate,
less the call to check_assoc_disj_2, into a subroutine -- you
could call it `accumulator__check_branched_goal' or something
like that.  If you make it into a subroutine, then it would
make perfect sense to call it from the code for if-then-elses
and switches.

> %-----------------------------------------------------------------------------%
> 
> 	%
> 	% accumulator__check_assoc_cases
> 	%
> 	% Ensure that each case of a switch is assocative.
> 	%
> :- pred accumulator__check_assoc_cases(list(case), rename,
> 		rename, list(case)).
> :- mode accumulator__check_assoc_cases(in, in, out, out) is semidet.
> 
> accumulator__check_assoc_cases([], Rename, Rename, []).
> accumulator__check_assoc_cases([case(Cons, G0) | Gs0], Rename0,
> 		Rename, [case(Cons, G) | Gs]) :-
> 	accumulator__check_assoc(G0, Rename0, Rename1, G),
> 	accumulator__check_assoc_cases(Gs0, Rename1, Rename, Gs).

Why is the treatment of switches so different to the treatment
of disjunctions?  Is that a bug?

> :- pred accumulator__check_prevcalls(vars, bool, map(var, commutative), 
> 		map(var, commutative)).
> :- mode accumulator__check_prevcalls(in, in, in, out) is semidet.
> 
> accumulator__check_prevcalls(OrigVars, Rearrange, PrevCallMap0, PrevCallMap) :-
> 	(
> 		accumulator__search_prevcalls(OrigVars, 
> 			PrevCallMap0, no, Commutative)
> 	->
> 		(
> 			Commutative = yes,
> 			(
> 				Rearrange = yes,
> 				fail
> 			;
> 				Rearrange = no
> 			)
> 		;
> 			Commutative = no,
> 			fail
> 		),

I think it would be clearer to just write that as

		Commutative = yes,
		Rearrange = no

perhaps with a comment.

> 		PrevCallMap = PrevCallMap0
> 	;
> 		bool__not(Rearrange, Commutative),
> 
> 		list__length(OrigVars, Length),
> 		list__duplicate(Length, Commutative, Commutatives),
> 		assoc_list__from_corresponding_lists(OrigVars,
> 			Commutatives, AssocList),
> 		map__from_assoc_list(AssocList, PrevCallMap1),
> 		map__merge(PrevCallMap0, PrevCallMap1, PrevCallMap)
> 	).
> 
> 
> %-----------------------------------------------------------------------------%
> 
> 
> 	%
> 	% accumulator__search_prevcalls(Vs, Map, Maybe, R)
> 	%
> 	% Search the prevcall map, Map,  for each var in Vs.  Maybe
> 	% should be initialised to no.
> 	%
> 	% R will be bound to yes if all the previous calls were
> 	% commutative, otherwise no.
> 	%
> :- pred accumulator__search_prevcalls(list(var), map(var, commutative), 
> 		maybe(commutative), commutative).
> :- mode accumulator__search_prevcalls(in, in, in, out) is semidet.

The code for this predicate is a bit confusing. 
What does the third argument represent?
The comment says that it should be initialised to `no', but
the recursive calls don't pass `no', is that a bug? ;-)

Why can't you just use a variable of type `commutative' rather
than `maybe(commutative)' as your accumulator, and initialize
it to `yes' rather than `no'?

What is this predicate supposed to do if there were no previous calls?
The specification seems to imply that R should be bound to `yes',
since all none of them were commutative, but the code binds R to `no'.

OK, that's it for this round.  I think it needs another round, though.

Cheers,	
	Fergus.

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