[m-dev.] for review: new version of accumulator introduction algorithm
Peter Ross
petdr at cs.mu.OZ.AU
Thu Jan 13 00:48:47 AEDT 2000
Hi,
Zoltan can you please review this?
Note that rather then attaching the diff for accumulator.m, I have
attached the actual file as the diff is bigger then the file.
===================================================================
Estimated hours taken: 40
Rewrite the accumulator introduction algorithm so that it syncs up with
the paper "Making Mercury Programs Tail Recursive".
compiler/accumulator.m:
Rewrite the accumulator introduction algorithm so that it syncs up
with the paper "Making Mercury Programs Tail Recursive".
The major enhancement over the old version is that construction
unfications which depend on associative calls are handled correctly
for arbitary associative calls (the 0.9 version only handles
the asssociative call, list__append, so will not have problems).
The other advantage is that my next transformation will be easier to
code up.
compiler/assertion.m:
assertion__is_associativity_assertion now reports the output
variable which is constructed from the two associative input
variables.
compiler/goal_store.m:
A module to associate arbitary Ids with a hlds_goal and the instmap
before the goal.
library/list.m:
Add the law
:- promise all [L,H,T] ( L = [H|T] <=> list__append([H], T, L)).
Index: compiler/accumulator.m
===================================================================
%-----------------------------------------------------------------------------%
% Copyright (C) 1999 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%
%
% Module: accumulator
% Main authors: petdr
%
% Attempts to transform a single proc to a tail recursive form by
% introducing accumlators.
%
% The algorithm implemented is the one from "Making Mercury Programs
% Tail Recursive", which can be found at
% http::/www.cs.mu.oz.au/research/mercury/information/papers.html
%
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- module accumulator.
:- interface.
:- import_module hlds_module, hlds_pred, io.
:- pred accumulator__process_proc(pred_id::in, proc_id::in, proc_info::in,
proc_info::out, module_info::in, module_info::out,
io__state::di, io__state::uo) is det.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module (assertion), error_util, goal_store, goal_util, globals.
:- import_module hlds_data, hlds_goal, hlds_out, (inst).
:- import_module inst_match, instmap, mode_util, options, prog_data, prog_util.
:- import_module assoc_list, bool, int, list, map, multi_map.
:- import_module require, set, std_util, string, term, varset.
%-----------------------------------------------------------------------------%
:- type top_level
---> switch_base_rec
; switch_rec_base
; disj_base_rec
; disj_rec_base
; ite_base_rec
; ite_rec_base.
:- type goal_id == pair(int).
:- type goal_store == goal_store(goal_id).
:- type subst == map(prog_var, prog_var).
:- type warning
% warn that two prog_vars in call to pred_id
% at prog_context were swapped.
---> w(prog_context, pred_id, prog_var, prog_var).
:- type warnings == list(warning).
%-----------------------------------------------------------------------------%
%
% process_proc
%
% Attempt to transform one procedure into a accumulator
% recursive form.
%
process_proc(PredId, ProcId, ProcInfo0, ProcInfo,
ModuleInfo0, ModuleInfo) -->
globals__io_lookup_bool_option(optimize_constructor_last_call, DoLCO),
globals__io_lookup_bool_option(fully_strict, FullyStrict),
(
{ module_info_pred_info(ModuleInfo0, PredId, PredInfo) },
{ attempt_transform(ProcId, ProcInfo0, PredId,
PredInfo, DoLCO, FullyStrict, ModuleInfo0,
ProcInfo1, ModuleInfo1, Warnings) }
->
globals__io_lookup_bool_option(very_verbose, VeryVerbose),
(
{ VeryVerbose = yes }
->
io__write_string("% Accumulators introduced into "),
hlds_out__write_pred_id(ModuleInfo1, PredId),
io__write_string("\n")
;
[]
),
globals__io_lookup_bool_option(inhibit_accumulator_warnings,
InhibitWarnings),
(
( { Warnings = [] } ; { InhibitWarnings = yes } )
->
{ ModuleInfo = ModuleInfo1 }
;
{ error_util__describe_one_pred_name(ModuleInfo1,
PredId, PredName) },
{ pred_info_context(PredInfo, Context) },
error_util__write_error_pieces(Context, 0,
[words("In"), words(PredName)]),
{ proc_info_varset(ProcInfo, VarSet) },
output_warnings(Warnings, VarSet, ModuleInfo1),
error_util__write_error_pieces(Context, 2,
[
words("Please ensure that these"),
words("argument rearrangements"),
words("do not introduce"),
words("performance problems."),
words("These warnings can"),
words("be suppressed by"),
words("`--inhibit-accumulator-warnings'.")
]),
globals__io_lookup_bool_option(verbose_errors,
VerboseErrors),
(
{ VerboseErrors = yes }
->
error_util__write_error_pieces(Context, 2,
[
words("If a predicate has been"),
words("declared associative via"),
words("a promise declaration,"),
words("the compiler will"),
words("rearrange the order"),
words("of the arguments"),
words("in calls to that"),
words("predicate, if by so doing"),
words("it makes the containing"),
words("predicate tail recursive."),
words("In such situations, the"),
words("compiler will issue"),
words("this warning."),
words("If this reordering changes the"),
words("performance characteristics"),
words("of the call to the"),
words("predicate, use"),
words("`--no-accumulator-introduction'"),
words("to turn the optimization"),
words("off, or"),
words("`--inhibit-accumulator-warnings'"),
words("to turn off the warnings.")
])
;
[]
),
globals__io_lookup_bool_option(halt_at_warn,
HaltAtWarn),
(
{ HaltAtWarn = yes }
->
io__set_exit_status(1),
{ module_info_incr_errors(ModuleInfo1,
ModuleInfo) }
;
{ ModuleInfo = ModuleInfo1 }
)
),
{ ProcInfo = ProcInfo1 }
;
{ ProcInfo = ProcInfo0 },
{ ModuleInfo = ModuleInfo0 }
).
%
% attempt_transform is only true if the current
% proc has been transformed to call the newly created
% accumulator proc.
%
:- pred attempt_transform(proc_id::in, proc_info::in,
pred_id::in, pred_info::in, bool::in, bool::in, module_info::in,
proc_info::out, module_info::out, warnings::out) is semidet.
attempt_transform(ProcId, ProcInfo0, PredId, PredInfo, DoLCO,
FullyStrict, ModuleInfo0, ProcInfo, ModuleInfo, Warnings) :-
proc_info_goal(ProcInfo0, Goal0),
proc_info_headvars(ProcInfo0, HeadVars),
proc_info_get_initial_instmap(ProcInfo0, ModuleInfo0, InitialInstMap),
simplify(Goal0, Goal),
identify_goal_type(PredId, ProcId, Goal, TopLevel, Base, Rec),
C = initialise_C(Rec, Base, InitialInstMap),
identify_recursive_call(PredId, ProcId, C, RecCallIds),
M = list__length(Rec),
attempt_transform_2(RecCallIds, C, M, Rec, HeadVars, InitialInstMap,
TopLevel, DoLCO, FullyStrict, PredInfo,
ProcInfo0, ModuleInfo0, Warnings, ProcInfo, ModuleInfo).
%
% If there is more then one recursive call in the recursive
% case, introduce accumulators into the first one for which the
% transformation succeeds
%
:- pred attempt_transform_2(list(goal_id)::in, goal_store::in, int::in,
hlds_goals::in, prog_vars::in, instmap::in, top_level::in,
bool::in, bool::in, pred_info::in, proc_info::in,
module_info::in, warnings::out,
proc_info::out, module_info::out) is semidet.
attempt_transform_2([Id | Ids], C, M, Rec, HeadVars, InitialInstMap, TopLevel,
DoLCO, FullyStrict, PredInfo, ProcInfo0, ModuleInfo0,
Warnings, ProcInfo, ModuleInfo) :-
(
identify_out_and_out_prime(Id, Rec, HeadVars,
InitialInstMap, ModuleInfo0, _Out, OutPrime,
HeadToCallSubst, CallToHeadSubst),
stage1(Id, M, C, DoLCO, FullyStrict, ModuleInfo0, Sets),
stage2(Id, C, Sets, OutPrime, ModuleInfo0, ProcInfo0,
VarSet - VarTypes, InitAccs, Substs, CS,
Warnings0),
stage3(Id, InitAccs, VarSet, VarTypes, C, CS, Substs,
HeadToCallSubst, CallToHeadSubst, Sets,
TopLevel, PredInfo, ProcInfo0, ModuleInfo0,
ProcInfo1, ModuleInfo1)
->
Warnings = Warnings0,
ProcInfo = ProcInfo1,
ModuleInfo = ModuleInfo1
;
attempt_transform_2(Ids, C, M, Rec, HeadVars, InitialInstMap,
TopLevel, DoLCO, FullyStrict,
PredInfo, ProcInfo0, ModuleInfo0,
Warnings, ProcInfo, ModuleInfo)
).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- pred output_warnings(list(warning)::in, prog_varset::in,
module_info::in, io__state::di, io__state::uo) is det.
output_warnings([], _, _) --> [].
output_warnings([W | Ws], VarSet, ModuleInfo) -->
{ output_warning(W, VarSet, ModuleInfo, Context, Format) },
error_util__write_error_pieces(Context, 2, Format),
output_warnings(Ws, VarSet, ModuleInfo).
:- pred output_warning(warning::in, prog_varset::in, module_info::in,
prog_context::out, list(format_component)::out) is det.
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.")
].
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
%
% simplify
%
% Simplify the goal to make it more amenable to introducing
% accumulators.
%
% At the moment all this does is remove any extra disj/conj
% wrappers around the top level goal.
%
% Future work is for this code to rearrange code with multiple
% base and recursive cases into a single base and recursive
% case.
%
:- pred simplify(hlds_goal, hlds_goal).
:- mode simplify(in, out) is det.
simplify(Goal0, Goal) :-
(
(
Goal0 = conj([Goal1]) - _
;
Goal0 = disj([Goal1], _) - _
)
->
simplify(Goal1, Goal)
;
Goal = Goal0
).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
%
% This predicate takes the original goal and identifies the
% `shape' of the goal around the recursive and base cases.
%
:- 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)),
is_base_case(GoalBList, proc(PredId, ProcId))
->
Type = switch_rec_base,
Base = GoalBList,
Rec = GoalAList
;
is_recursive_case(GoalBList, proc(PredId, ProcId)),
is_base_case(GoalAList, proc(PredId, ProcId))
->
Type = switch_base_rec,
Base = GoalAList,
Rec = GoalBList
;
fail
)
;
fail
).
%
% is_recursive_case(Gs, Id) is true iff the list of goals, Gs,
% contains a call to the procedure specified by Id.
%
:- pred is_recursive_case(list(hlds_goal)::in, pred_proc_id::in) is semidet.
is_recursive_case(Goals, proc(PredId, ProcId)) :-
list__append(_Initial, [RecursiveCall | _Final], Goals),
RecursiveCall = call(PredId, ProcId, _, _, _, _) - _.
%
% is_base_case(Gs, Id) is true iff the list of goals, Gs,
% doesn't contain a call to the procedure specified by Id.
%
:- pred is_base_case(list(hlds_goal)::in, pred_proc_id::in) is semidet.
is_base_case(Goals, PredProcId) :-
not is_recursive_case(Goals, PredProcId).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- type store_info
---> store_info(
int,
instmap,
goal_store
).
%
% Initialise the goal_store, which will holds C_{a,b} goals.
%
:- func initialise_C(hlds_goals, hlds_goals, instmap) = goal_store.
initialise_C(Rec, Base, InitialInstMap) = C :-
goal_store__init(C0),
list__foldl(store(rec), Rec, store_info(1, InitialInstMap, C0),
store_info(_, _, C1)),
list__foldl(store(base), Base,
store_info(1, InitialInstMap, C1),
store_info(_, _, C)).
%
% store(Id, G, SI0, SI) is true iff the goal G is stored inside
% the goal_store (which is part of SI) with the correct
% identifier and instmap associatied with the goal.
%
:- pred store(int::in, hlds_goal::in, store_info::in, store_info::out) is det.
store(Identifier, Goal, store_info(N, IM0, GS0), store_info(N+1, IM, GS)) :-
Goal = _ - GoalInfo,
goal_info_get_instmap_delta(GoalInfo, InstMapDelta),
instmap__apply_instmap_delta(IM0, InstMapDelta, IM),
goal_store__det_insert(GS0, Identifier - N, Goal - IM0, GS).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% Determine the k's which are recursive calls
:- pred identify_recursive_call(pred_id::in, proc_id::in,
goal_store::in, list(goal_id)::out) is det.
identify_recursive_call(PredId, ProcId, GoalStore, Ids) :-
P = (pred(Key::out) is nondet :-
goal_store__member(GoalStore, Key, Goal - _InstMap),
Goal = call(PredId, ProcId, _, _, _, _) - _
),
solutions(P, Ids).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
%
% identify_out_and_out_prime
%
% Determine the variables which are members of the sets Out and
% Out', and initialise the substitutions between the two sets.
%
% This is done by identifing those variables whose
% instantiatedness change in the goals after the recursive call
% and are headvars.
%
:- pred identify_out_and_out_prime(goal_id::in, hlds_goals::in, prog_vars::in,
instmap::in, module_info::in, prog_vars::out,
prog_vars::out, subst::out, subst::out) is det.
identify_out_and_out_prime(_N - K, Rec, HeadVars, InitialInstMap, ModuleInfo,
Out, OutPrime, HeadToCallSubst, CallToHeadSubst) :-
(
list__take(K, Rec, InitialGoals),
list__drop(K-1, Rec, FinalGoals),
FinalGoals = [call(_, _, Args, _, _, _) - _ | Rest]
->
goal_list_instmap_delta(InitialGoals, InitInstMapDelta),
instmap__apply_instmap_delta(InitialInstMap,
InitInstMapDelta, InstMapBeforeRest),
goal_list_instmap_delta(Rest, InstMapDelta),
instmap__apply_instmap_delta(InstMapBeforeRest,
InstMapDelta, InstMapAfterRest),
instmap_changed_vars(InstMapBeforeRest,
InstMapAfterRest, ModuleInfo, ChangedVars),
assoc_list__from_corresponding_lists(HeadVars, Args, HeadArg0),
Member = (pred(M::in) is semidet :-
M = HeadVar - _,
set__member(HeadVar, ChangedVars)
),
list__filter(Member, HeadArg0, HeadArg),
list__map(fst, HeadArg, Out),
list__map(snd, HeadArg, OutPrime),
map__from_assoc_list(HeadArg, HeadToCallSubst),
list__map((pred(X-Y::in, Y-X::out) is det), HeadArg, ArgHead),
map__from_assoc_list(ArgHead, CallToHeadSubst)
;
error("accumulator__identify_out_and_out_prime")
).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- type sets
---> sets(
set(goal_id), % before
set(goal_id), % assoc
set(goal_id), % construct_assoc
set(goal_id), % construct
set(goal_id) % reject
).
%
% Stage 1 is responsible for identifying, which goals are
% associative, which can be moved before the recursive call and
% so on.
%
:- pred stage1(goal_id::in, int::in, goal_store::in, bool::in, bool::in,
module_info::in, sets::out) is semidet.
stage1(N - K, M, GoalStore, DoLCO, FullyStrict, ModuleInfo, Sets) :-
sets_init(Sets0),
stage1_2(N - (K+1), K, M, GoalStore, FullyStrict, ModuleInfo,
Sets0, Sets1),
Sets1 = sets(Before, Assoc, ConstructAssoc, Construct, Reject),
Sets = sets(Before `union` set_upto(N, (K-1)), Assoc,
ConstructAssoc, Construct, Reject),
% Continue the transformation only if the set reject is
% empty and the set assoc contains something that needs
% to be moved before the recursive call.
set__empty(Reject),
not set__empty(Assoc),
(
DoLCO = no
->
% If LCMC is not turned on then there must be no
% construction unifications after the recursive
% call.
set__empty(Construct `union` ConstructAssoc)
;
true
).
%
% For each goal after the recursive call decide which set the
% goal belongs to.
%
:- pred stage1_2(goal_id::in, int::in, int::in, goal_store::in,
bool::in, module_info::in, sets::in, sets::out) is det.
stage1_2(N - I, K, M, GoalStore, FullyStrict, ModuleInfo, Sets0, Sets) :-
(
I > M
->
Sets0 = Sets
;
(
before(N - I, K, GoalStore, Sets0,
FullyStrict, ModuleInfo)
->
stage1_2(N - (I+1), K, M, GoalStore,
FullyStrict, ModuleInfo,
insert_before(N - I, Sets0), Sets)
;
assoc(N - I, K, GoalStore, Sets0,
FullyStrict, ModuleInfo)
->
stage1_2(N - (I+1), K, M, GoalStore,
FullyStrict, ModuleInfo,
insert_assoc(N - I, Sets0), Sets)
;
construct(N - I, K, GoalStore, Sets0,
FullyStrict, ModuleInfo)
->
stage1_2(N - (I+1), K, M, GoalStore,
FullyStrict, ModuleInfo,
insert_construct(N - I, Sets0), Sets)
;
construct_assoc(N - I, K, GoalStore, Sets0,
FullyStrict, ModuleInfo)
->
stage1_2(N - (I+1), K, M, GoalStore,
FullyStrict, ModuleInfo,
insert_construct_assoc(N - I, Sets0),
Sets)
;
Sets = insert_reject(N - I, Sets0)
)
).
%-----------------------------------------------------------------------------%
:- pred sets_init(sets::out) is det.
sets_init(Sets) :-
set__init(Set),
Before = Set,
Assoc = Set,
ConstructAssoc = Set,
Construct = Set,
Reject = Set,
Sets = sets(Before, Assoc, ConstructAssoc, Construct, Reject).
% This function is called repeatedly with the same arguments so
% is an ideal canditate for tabling.
:- pragma memo(set_upto/2).
%
% set_upto(N, K) returns the set {(N,1)...(N,K)}
%
:- func set_upto(int, int) = set(goal_id).
set_upto(N, K) = Set :-
(
K =< 0
->
set__init(Set)
;
Set0 = set_upto(N, K-1),
set__insert(Set0, N-K, Set)
).
:- func insert_before(goal_id, sets) = sets.
insert_before(GoalId, sets(Before, Assoc, ConstructAssoc, Construct, Reject))
= sets(set__insert(Before, GoalId), Assoc, ConstructAssoc, Construct,
Reject).
:- func insert_assoc(goal_id, sets) = sets.
insert_assoc(GoalId, sets(Before, Assoc, ConstructAssoc, Construct, Reject))
= sets(Before, set__insert(Assoc, GoalId), ConstructAssoc, Construct,
Reject).
:- func insert_construct_assoc(goal_id, sets) = sets.
insert_construct_assoc(GoalId, sets(Before, Assoc, ConstructAssoc, Construct,
Reject))
= sets(Before, Assoc, set__insert(ConstructAssoc, GoalId), Construct,
Reject).
:- func insert_construct(goal_id, sets) = sets.
insert_construct(GoalId, sets(Before, Assoc, ConstructAssoc, Construct, Reject))
= sets(Before, Assoc, ConstructAssoc, set__insert(Construct, GoalId),
Reject).
:- func insert_reject(goal_id, sets) = sets.
insert_reject(GoalId, sets(Before, Assoc, ConstructAssoc, Construct, Reject))
= sets(Before, Assoc, ConstructAssoc, Construct,
set__insert(Reject, GoalId)).
%-----------------------------------------------------------------------------%
%
% A goal is a member of the before set iff the goal only depends on
% goals which are before the recursive call or can be moved
% before the recursive call (member of the before set).
%
:- pred before(goal_id::in, int::in, goal_store::in, sets::in,
bool::in, module_info::in) is semidet.
before(N - I, K, GoalStore, sets(Before, _, _, _, _),
FullyStrict, ModuleInfo) :-
goal_store__lookup(GoalStore, N - I, LaterGoal - LaterInstMap),
(
member_lessthan_goalid(GoalStore, N - I, N - J,
EarlierGoal - EarlierInstMap),
not goal_util__can_reorder_goals(ModuleInfo, FullyStrict,
EarlierInstMap, EarlierGoal,
LaterInstMap, LaterGoal)
)
=>
(
set__member(N - J, set_upto(N, K-1) `union` Before)
).
%
% A goal is a member of the assoc set iff the goal only depends
% on goals upto and including the recursive call and goals which
% can be moved before the recursive call (member of the before
% set) AND the goal is associative.
%
:- pred assoc(goal_id::in, int::in, goal_store::in, sets::in, bool::in,
module_info::in) is semidet.
assoc(N - I, K, GoalStore, sets(Before, _, _, _, _),
FullyStrict, ModuleInfo) :-
goal_store__lookup(GoalStore, N - I, LaterGoal - LaterInstMap),
LaterGoal = call(PredId, ProcId, Args, _, _, _) - _,
is_associative(PredId, ProcId, ModuleInfo, Args, _),
(
member_lessthan_goalid(GoalStore, N - I, _N - J,
EarlierGoal - EarlierInstMap),
not goal_util__can_reorder_goals(ModuleInfo, FullyStrict,
EarlierInstMap, EarlierGoal,
LaterInstMap, LaterGoal)
)
=>
(
set__member(N - J, set_upto(N, K) `union` Before)
).
%
% A goal is a member of the construct set iff the goal only depends
% on goals upto and including the recursive call and goals which
% can be moved before the recursive call (member of the before
% set) AND the goal is construction unification.
%
:- pred construct(goal_id::in, int::in, goal_store::in, sets::in,
bool::in, module_info::in) is semidet.
construct(N - I, K, GoalStore, sets(Before, _, _, Construct, _),
FullyStrict, ModuleInfo) :-
goal_store__lookup(GoalStore, N - I, LaterGoal - LaterInstMap),
LaterGoal = unify(_, _, _, Unify, _) - _GoalInfo,
Unify = construct(_, _, _, _, _, _, _),
(
member_lessthan_goalid(GoalStore, N - I, _N - J,
EarlierGoal - EarlierInstMap),
not goal_util__can_reorder_goals(ModuleInfo, FullyStrict,
EarlierInstMap, EarlierGoal,
LaterInstMap, LaterGoal)
)
=>
(
set__member(N - J, set_upto(N, K) `union` Before `union`
Construct)
).
%
% A goal is a member of the construct_assoc set iff the goal
% only depends on goals upto and including the recursive call
% and goals which can be moved before the recursive call (member
% of the before set) and goals which are associative AND the
% goal is construction unification AND the there is only one
% member of the assoc set which the construction unification
% depends on AND the construction unification can be expressed
% as a call to the member of the assoc set which the
% construction unification depends on.
%
:- pred construct_assoc(goal_id::in, int::in, goal_store::in, sets::in,
bool::in, module_info::in) is semidet.
construct_assoc(N - I, K, GoalStore, sets(Before, Assoc, ConstructAssoc, _, _),
FullyStrict, ModuleInfo) :-
goal_store__lookup(GoalStore, N - I, LaterGoal - LaterInstMap),
LaterGoal = unify(_, _, _, Unify, _) - _GoalInfo,
Unify = construct(_, ConsId, _, _, _, _, _),
goal_store__all_ancestors(GoalStore, N - I, ModuleInfo, FullyStrict,
Ancestors),
set__singleton_set(Assoc `intersect` Ancestors, AssocId),
goal_store__lookup(GoalStore, AssocId, AssocGoal - _AssocInstMap),
AssocGoal = call(PredId, _, _, _, _, _) - _,
is_associative_construction(ConsId, PredId, ModuleInfo),
(
member_lessthan_goalid(GoalStore, N - I, _N - J,
EarlierGoal - EarlierInstMap),
not goal_util__can_reorder_goals(ModuleInfo, FullyStrict,
EarlierInstMap, EarlierGoal,
LaterInstMap, LaterGoal)
)
=>
(
set__member(N - J, set_upto(N, K) `union` Before `union`
Assoc `union` ConstructAssoc)
).
%
% member_lessthan_goalid(GS, IdA, IdB, GB) is true iff the
% goal_id, IdB, and its associated goal, GB, is a member of the
% goal_store, GS, and IdB is less than IdA.
%
:- pred member_lessthan_goalid(goal_store::in, goal_id::in,
goal_id::out, goal_store__goal::out) is nondet.
member_lessthan_goalid(GoalStore, N - I, N - J, Goal) :-
goal_store__member(GoalStore, N - J, Goal),
J < I.
%-----------------------------------------------------------------------------%
:- type assoc
---> assoc(
set(prog_var), % the associative input args
prog_var, % the corresponding output arg
bool % is the predicate commutative?
).
%
% If accumulator_is_associative is true, it returns the two
% arguments which are associative and the variable which depends
% on those two arguments, and an indicator of whether or not
% the predicate is commutative.
%
:- pred is_associative(pred_id::in, proc_id::in, module_info::in,
prog_vars::in, assoc::out) is semidet.
is_associative(PredId, ProcId, ModuleInfo, Args, Result) :-
module_info_pred_proc_info(ModuleInfo, PredId, ProcId,
PredInfo, ProcInfo),
pred_info_get_assertions(PredInfo, Assertions),
(
commutativity_assertion(set__to_sorted_list(Assertions),
ModuleInfo, Args, CommutativeVars)
->
% Currently we can only have one output
% argument, so we know which arg is generated
% directly by the two commutative args.
proc_info_argmodes(ProcInfo, ArgModes),
P = (pred(Pair::in, Var::out) is semidet :-
Pair = Var - Mode,
mode_get_insts(ModuleInfo, Mode,
InitialInst, FinalInst),
not inst_matches_final(InitialInst, FinalInst,
ModuleInfo)
),
assoc_list__from_corresponding_lists(Args, ArgModes, Pairs),
list__filter_map(P, Pairs, [OutputVar]),
IsCommutative = yes,
Result = assoc(CommutativeVars, OutputVar, IsCommutative)
;
associativity_assertion(set__to_sorted_list(Assertions),
ModuleInfo, Args, AssociativeVars, OutputVar),
IsCommutative = no,
Result = assoc(AssociativeVars, OutputVar, IsCommutative)
).
%
% commutativity_assertion
%
% Does there exist one (and only one) commutativity assertion for the
% current predicate.
% The 'and only one condition' is required because we currently
% don't handle the case of predicates which have individual
% parts which are commutative, because then we don't know which
% variable is descended from which.
%
:- pred commutativity_assertion(list(assert_id)::in, module_info::in,
prog_vars::in, set(prog_var)::out) is semidet.
commutativity_assertion([AssertId | AssertIds], ModuleInfo, Args0,
PossibleStaticVars) :-
(
assertion__is_commutativity_assertion(AssertId, ModuleInfo,
Args0, StaticVarA - StaticVarB)
->
\+ commutativity_assertion(AssertIds, ModuleInfo, Args0, _),
PossibleStaticVars = set__list_to_set([StaticVarA, StaticVarB])
;
commutativity_assertion(AssertIds, ModuleInfo, Args0,
PossibleStaticVars)
).
%
% associativity_assertion
%
% Does there exist one (and only one) associativity assertion for the
% current predicate.
% The 'and only one condition' is required because we currently
% don't handle the case of predicates which have individual
% parts which are associative, because then we don't know which
% variable is descended from which.
%
:- pred associativity_assertion(list(assert_id)::in, module_info::in,
prog_vars::in, set(prog_var)::out, prog_var::out) is semidet.
associativity_assertion([AssertId | AssertIds], ModuleInfo, Args0, VarAB,
OutputVar) :-
(
assertion__is_associativity_assertion(AssertId, ModuleInfo,
Args0, VarA - VarB, OutputVar0)
->
\+ associativity_assertion(AssertIds, ModuleInfo, Args0, _, _),
VarAB = set__list_to_set([VarA, VarB]),
OutputVar = OutputVar0
;
associativity_assertion(AssertIds, ModuleInfo, Args0,
VarAB, OutputVar)
).
%-----------------------------------------------------------------------------%
%
% Can the construction unification be expressed as a call to the
% specified predicate.
%
:- pred is_associative_construction(cons_id::in, pred_id::in,
module_info::in) is semidet.
is_associative_construction(ConsId, PredId, ModuleInfo) :-
module_info_pred_info(ModuleInfo, PredId, PredInfo),
pred_info_get_assertions(PredInfo, Assertions),
list__filter((pred(AssertId::in) is semidet :-
assertion__is_construction_equivalence_assertion(
AssertId, ModuleInfo, ConsId, PredId)
),
set__to_sorted_list(Assertions),
Result),
Result \= [].
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- type substs
---> substs(
subst, % acc_var_subst
subst, % rec_call_subst
subst % assoc_call_subst
).
%
% Stage 2 is responsible for identifying the substitutions which
% are needed to mimic the unfold/fold process that was used as
% the justification of the algorithm in the paper.
% It is also responsible for ensuring that the reordering of
% arguments doesn't worsen the big-O complexity of the
% procedure.
%
:- pred stage2(goal_id::in, goal_store::in, sets::in,
prog_vars::in, module_info::in, proc_info::in,
pair(prog_varset, vartypes)::out, prog_vars::out,
substs::out, goal_store::out, warnings::out) is semidet.
stage2(N - K, GoalStore, Sets, OutPrime, ModuleInfo, ProcInfo0,
VarSetVarTypesPair, set__to_sorted_list(InitAccs),
Substs, CS, Warnings) :-
Sets = sets(Before0, Assoc, ConstructAssoc, Construct, _Reject),
Before = Before0 `union` set_upto(N, K-1),
After = Assoc `union` ConstructAssoc `union` Construct,
P = (pred(Id::in, Set0::in, Set::out) is det :-
goal_store__lookup(GoalStore, Id, Goal - _InstMap),
Goal = _GoalExpr - GoalInfo,
goal_info_get_nonlocals(GoalInfo, NonLocals),
Set = NonLocals `union` Set0
),
list__foldl(P, set__to_sorted_list(Before), set__init, BeforeNonLocals),
list__foldl(P, set__to_sorted_list(After), set__init, AfterNonLocals),
InitAccs = BeforeNonLocals `intersect` AfterNonLocals,
proc_info_varset(ProcInfo0, VarSet0),
proc_info_vartypes(ProcInfo0, VarTypes0),
substs_init(set__to_sorted_list(InitAccs), VarSet0, VarTypes0,
VarSet1, VarTypes1, Substs0),
process_assoc_set(set__to_sorted_list(Assoc), GoalStore,
set__list_to_set(OutPrime), ModuleInfo, Substs0,
VarSet1 - VarTypes1, Substs, VarSetVarTypesPair, CS,
Warnings).
%-----------------------------------------------------------------------------%
:- pred substs_init(prog_vars::in, prog_varset::in, vartypes::in,
prog_varset::out, vartypes::out, substs::out) is det.
substs_init(InitAccs, VarSet0, VarTypes0, VarSet, VarTypes, Substs) :-
map__init(Subst),
acc_var_subst_init(InitAccs, VarSet0, VarTypes0,
VarSet, VarTypes, AccVarSubst),
RecCallSubst = Subst,
AssocCallSubst = Subst,
Substs = substs(AccVarSubst, RecCallSubst, AssocCallSubst).
%
% Initialise the acc_var_subst to be from Var to A_Var where
% Var is a member of InitAccs and A_Var is a fresh variable of
% the same type of Var.
%
:- pred acc_var_subst_init(prog_vars::in, prog_varset::in, vartypes::in,
prog_varset::out, vartypes::out, subst::out) is det.
acc_var_subst_init([], VarSet, VarTypes, VarSet, VarTypes, Subst) :-
map__init(Subst).
acc_var_subst_init([Var | Vars], VarSet0, VarTypes0,
VarSet, VarTypes, Subst) :-
create_new_var(Var, "A_", AccVar, VarSet0 - VarTypes0,
VarSet1 - VarTypes1),
acc_var_subst_init(Vars, VarSet1, VarTypes1, VarSet, VarTypes, Subst0),
map__det_insert(Subst0, Var, AccVar, Subst).
%
% Create a fresh variable which is the same type as the old
% variable and has the same name except that it begins with the
% prefix.
%
:- pred create_new_var(prog_var::in, string::in, prog_var::out,
pair(prog_varset, vartypes)::in,
pair(prog_varset, vartypes)::out) is det.
create_new_var(OldVar, Prefix, NewVar, VarSet0 - VarTypes0,
VarSet - VarTypes) :-
varset__lookup_name(VarSet0, OldVar, OldName),
string__append(Prefix, OldName, NewName),
varset__new_named_var(VarSet0, NewName, NewVar, VarSet),
map__lookup(VarTypes0, OldVar, Type),
map__det_insert(VarTypes0, NewVar, Type, VarTypes).
%-----------------------------------------------------------------------------%
%
% For each member of the assoc set determine the substitutions
% needed, and also check the efficiency of the procedure isn't
% worsened by swapping reordering the arguments to a call.
%
:- pred process_assoc_set(list(goal_id)::in, goal_store::in, set(prog_var)::in,
module_info::in, substs::in, pair(prog_varset, vartypes)::in,
substs::out, pair(prog_varset, vartypes)::out,
goal_store::out, warnings::out) is semidet.
process_assoc_set([], _GS, _OutPrime, _ModuleInfo, Substs, Types,
Substs, Types, CS, []) :-
goal_store__init(CS).
process_assoc_set([Id | Ids], GS, OutPrime, ModuleInfo, Substs0, Types0,
Substs, Types, CS, Warnings) :-
Substs0 = substs(AccVarSubst, RecCallSubst0, AssocCallSubst0),
lookup_call(GS, Id, Goal - InstMap),
Goal = call(PredId, ProcId, Args, _, _, _) - GoalInfo,
is_associative(PredId, ProcId, ModuleInfo, Args, AssocInfo),
AssocInfo = assoc(Vars, AssocOutput, IsCommutative),
set__singleton_set(Vars `intersect` OutPrime, DuringAssocVar),
set__singleton_set(Vars `difference` (Vars `intersect` OutPrime),
BeforeAssocVar),
map__lookup(AccVarSubst, BeforeAssocVar, AccVar),
create_new_var(BeforeAssocVar, "NewAcc_", NewAcc, Types0, Types1),
map__det_insert(AssocCallSubst0, DuringAssocVar, AccVar,
AssocCallSubst1),
map__det_insert(AssocCallSubst1, AssocOutput, NewAcc,
AssocCallSubst),
map__det_insert(RecCallSubst0, DuringAssocVar, AssocOutput,
RecCallSubst1),
map__det_insert(RecCallSubst1, BeforeAssocVar, NewAcc, RecCallSubst),
Substs1 = substs(AccVarSubst, RecCallSubst, AssocCallSubst),
% Only swap the order of the variables if the goal is
% ONLY associative.
(
IsCommutative = yes,
CSGoal = Goal - InstMap,
Warning = []
;
IsCommutative = no,
% Ensure that the reordering doesn't cause a
% efficiency problem
module_info_pred_info(ModuleInfo, PredId, PredInfo),
pred_info_module(PredInfo, ModuleName),
pred_info_name(PredInfo, PredName),
pred_info_arity(PredInfo, Arity),
(
has_heuristic(ModuleName, PredName, Arity)
->
heuristic(ModuleName, PredName, Arity, Args,
PossibleDuringAssocVars),
set__member(DuringAssocVar, PossibleDuringAssocVars),
Warning = []
;
goal_info_get_context(GoalInfo, ProgContext),
Warning = [w(ProgContext, PredId,
BeforeAssocVar, DuringAssocVar)]
),
% Swap the arguments.
[A,B] = set__to_sorted_list(Vars),
map__from_assoc_list([A-B, B-A], Subst),
goal_util__rename_vars_in_goal(Goal, Subst, SwappedGoal),
CSGoal = SwappedGoal - InstMap
),
process_assoc_set(Ids, GS, OutPrime, ModuleInfo, Substs1, Types1,
Substs, Types, CS0, Warnings0),
goal_store__det_insert(CS0, Id, CSGoal, CS),
list__append(Warnings0, Warning, Warnings).
:- pred has_heuristic(module_name::in, string::in, arity::in) is semidet.
has_heuristic(unqualified("list"), "append", 3).
:- pred heuristic(module_name::in, string::in, arity::in, prog_vars::in,
set(prog_var)::out) is semidet.
heuristic(unqualified("list"), "append", 3, [_Typeinfo, A, _B, _C], Set) :-
set__list_to_set([A], Set).
%-----------------------------------------------------------------------------%
:- inst call = bound(call(ground, ground, ground, ground, ground, ground)).
:- inst hlds_call = bound('-'(call, ground)).
:- inst call_goal = bound('-'(hlds_call, ground)).
% Do a goal_store__lookup where the result is known to be a
% call.
:- pred lookup_call(goal_store, goal_id, goal_store__goal) is det.
:- mode lookup_call(in, in, out(call_goal)) is det.
lookup_call(GoalStore, Id, Call - InstMap) :-
goal_store__lookup(GoalStore, Id, Goal - InstMap),
(
Goal = call(_, _, _, _, _, _) - _
->
Call = Goal
;
error("accumulator__lookup_call: not a call.")
).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
%
% stage3 creates the accumulator version of the predicate using
% the substitutions determined in stage2, it also redefines the
% original procedure to call the accumulator version of the
% procedure.
%
:- pred stage3(goal_id::in, prog_vars::in, prog_varset::in, vartypes::in,
goal_store::in, goal_store::in, substs::in, subst::in,
subst::in, sets::in, top_level::in, pred_info::in,
proc_info::in, module_info::in,
proc_info::out, module_info::out) is det.
stage3(RecCallId, InitAccs, VarSet, VarTypes, C, CS, Substs,
HeadToCallSubst, CallToHeadSubst, Sets, TopLevel,
OrigPredInfo, OrigProcInfo0, ModuleInfo0,
OrigProcInfo, ModuleInfo) :-
acc_proc_info(InitAccs, VarSet, VarTypes, Substs,
OrigProcInfo0, AccTypes, AccProcInfo),
acc_pred_info(AccTypes, AccProcInfo, OrigPredInfo, AccProcId,
AccPredInfo),
pred_info_name(AccPredInfo, AccPredName),
AccName = unqualified(AccPredName),
module_info_get_predicate_table(ModuleInfo0, PredTable0),
predicate_table_insert(PredTable0, AccPredInfo, AccPredId, PredTable),
module_info_set_predicate_table(ModuleInfo0, PredTable, ModuleInfo1),
create_goal(RecCallId, InitAccs, AccPredId, AccProcId, AccName, Substs,
HeadToCallSubst, CallToHeadSubst, Sets, C, CS,
OrigBaseGoal, OrigRecGoal, AccBaseGoal, AccRecGoal),
proc_info_goal(OrigProcInfo0, OrigGoal0),
top_level(TopLevel, OrigGoal0, OrigBaseGoal, OrigRecGoal,
AccBaseGoal, AccRecGoal, OrigGoal, AccGoal),
proc_info_set_goal(OrigProcInfo0, OrigGoal, OrigProcInfo),
update_accumulator_pred(AccPredId, AccProcId, AccGoal,
ModuleInfo1, ModuleInfo).
%-----------------------------------------------------------------------------%
%
% acc_proc_info
%
% Construct a proc_info for the introduced predicate.
%
:- pred acc_proc_info(prog_vars::in, prog_varset::in, vartypes::in,
substs::in, proc_info::in,
list(type)::out, proc_info::out) is det.
acc_proc_info(InitAccs, VarSet, VarTypes, Substs,
OrigProcInfo, AccTypes, AccProcInfo) :-
% ProcInfo Stuff that must change.
proc_info_headvars(OrigProcInfo, HeadVars0),
proc_info_argmodes(OrigProcInfo, HeadModes0),
proc_info_inferred_determinism(OrigProcInfo, Detism),
proc_info_goal(OrigProcInfo, Goal),
proc_info_context(OrigProcInfo, Context),
proc_info_typeinfo_varmap(OrigProcInfo, TVarMap),
proc_info_typeclass_info_varmap(OrigProcInfo, TCVarsMap),
proc_info_is_address_taken(OrigProcInfo, IsAddressTaken),
Substs = substs(AccVarSubst, _RecCallSubst, _AssocCallSubst),
list__map(map__lookup(AccVarSubst), InitAccs, Accs),
HeadVars = HeadVars0 `append` Accs,
% XXX we don't want to use the inst of the var as it can
% be more specific than it should be. ie int_const(1)
% when it should be any integer.
% However this will no longer handle partially
% instantiated data structures.
Inst = ground(shared, no),
inst_lists_to_mode_list([Inst], [Inst], Mode),
list__duplicate(list__length(Accs), list__det_head(Mode), AccModes),
HeadModes = HeadModes0 `append` AccModes,
list__map(map__lookup(VarTypes), Accs, AccTypes),
proc_info_create(VarSet, VarTypes, HeadVars, HeadModes, Detism, Goal,
Context, TVarMap, TCVarsMap, IsAddressTaken,
AccProcInfo).
%-----------------------------------------------------------------------------%
%
% acc_pred_info
%
% Construct the pred_info for the introduced predicate
%
:- pred acc_pred_info(list(type)::in, proc_info::in, pred_info::in,
proc_id::out, pred_info::out) is det.
acc_pred_info(NewTypes, NewProcInfo, PredInfo, NewProcId, NewPredInfo) :-
% PredInfo stuff that must change.
pred_info_arg_types(PredInfo, TypeVarSet, ExistQVars, Types0),
pred_info_module(PredInfo, ModuleName),
pred_info_name(PredInfo, Name),
Cond = true,
pred_info_context(PredInfo, PredContext),
pred_info_get_markers(PredInfo, Markers),
pred_info_get_is_pred_or_func(PredInfo, PredOrFunc),
pred_info_get_class_context(PredInfo, ClassContext),
pred_info_get_aditi_owner(PredInfo, Owner),
set__init(Assertions),
proc_info_context(NewProcInfo, Context),
term__context_line(Context, Line),
Counter = 0,
list__append(Types0, NewTypes, Types),
make_pred_name_with_context(ModuleName, "AccFrom", PredOrFunc, Name,
Line, Counter, SymName),
pred_info_create(ModuleName, SymName, TypeVarSet, ExistQVars, Types,
Cond, PredContext, local, Markers, PredOrFunc,
ClassContext, Owner, Assertions, NewProcInfo, NewProcId,
NewPredInfo).
%-----------------------------------------------------------------------------%
%
% create_goal creates the new base and recursive case of the
% original procedure (OrigBaseGoal and OrigRecGoal) and the base
% and recursive cases of accumulator version (AccBaseGoal and
% AccRecGoal).
%
:- pred create_goal(goal_id, prog_vars, pred_id, proc_id, sym_name, substs,
subst, subst, sets, goal_store, goal_store,
hlds_goal, hlds_goal, hlds_goal, hlds_goal).
:- mode create_goal(in, in, in, in, in,
in, in, in, in, in, in, out, out, out, out) is det.
create_goal(RecCallId, InitAccs, AccPredId, AccProcId, AccName, Substs,
HeadToCallSubst, CallToHeadSubst, Sets, C, CS,
OrigBaseGoal, OrigRecGoal, AccBaseGoal, AccRecGoal) :-
lookup_call(C, RecCallId, OrigCall - _InstMap),
Substs = substs(AccVarSubst, RecCallSubst, AssocCallSubst),
Sets = sets(Before, Assoc, ConstructAssoc, Construct, _Reject),
Call = create_acc_call(OrigCall, InitAccs, AccPredId,
AccProcId, AccName),
goal_util__rename_vars_in_goal(Call, CallToHeadSubst, BaseCall),
goal_util__rename_vars_in_goal(Call, RecCallSubst, RecCall),
Cbefore = goal_list(set__to_sorted_list(Before), C),
Cbase = goal_list(base_case_ids(C), C),
calculate_goal_info(conj(Cbefore `append` [BaseCall]), OrigRecGoal),
calculate_goal_info(conj(Cbase), OrigBaseGoal),
% Create the R sets
R = create_R(Assoc, Construct `union` ConstructAssoc,
AssocCallSubst, AccVarSubst, C, CS),
Rassoc = goal_list(set__to_sorted_list(Assoc), R),
Rconstruct = goal_list(set__to_sorted_list(Construct `union`
ConstructAssoc), R),
% Create the B Sets
B = create_B(Assoc `union` Construct `union` ConstructAssoc,
C, AccVarSubst, HeadToCallSubst),
Bafter = base_case_ids(B) `append` set__to_sorted_list(Assoc `union`
Construct `union` ConstructAssoc),
BaseCase = goal_list(Bafter, B),
calculate_goal_info(conj(Cbefore `append` Rassoc `append`
[RecCall] `append` Rconstruct), AccRecGoal),
calculate_goal_info(conj(BaseCase), AccBaseGoal).
%
% create_acc_call takes the original call and generates a call
% to the accumulator version of the call, which can have the
% substitutions applied to it easily.
%
:- func create_acc_call(hlds_goal, prog_vars, pred_id, proc_id,
sym_name) = hlds_goal.
:- mode create_acc_call(in(hlds_call), in, in, in, in) = out(hlds_call) is det.
create_acc_call(OrigCall, InitAccs, AccPredId, AccProcId, AccName) = Call :-
OrigCall = call(_PredId, _ProcId, Args, Builtin, Context, _Name) - GI,
Call = call(AccPredId, AccProcId, Args `append` InitAccs,
Builtin, Context, AccName) - GI.
%
% Create the R set of goals by renaming all the members of assoc
% in CS using assoc_call_subst and all the members of
% (construct U construct_assoc) in C with acc_var_subst.
%
:- func create_R(set(goal_id), set(goal_id), subst, subst, goal_store,
goal_store) = goal_store.
create_R(Assoc, Constructs, AssocCallSubst, AccVarSubst, C, CS)
= rename(set__to_sorted_list(Constructs), AccVarSubst, C, RBase) :-
RBase = rename(set__to_sorted_list(Assoc), AssocCallSubst, CS,
goal_store__init).
%
% Create the B set of goals by renaming all the base case goals
% of C with head_to_call and all the members of (assoc U
% construct U construct_assoc) of C with acc_var_subst.
%
:- func create_B(set(goal_id), goal_store, subst, subst) = goal_store.
create_B(Ids, C, AccVarSubst, HeadToCallSubst)
= rename(set__to_sorted_list(Ids), AccVarSubst, C, Bbase) :-
Bbase = rename(base_case_ids(C), HeadToCallSubst, C, goal_store__init).
%-----------------------------------------------------------------------------%
%
% Given the top level structure of the goal create new version
% with new base and recursive cases plugged in.
%
:- pred top_level(top_level::in, hlds_goal::in,
hlds_goal::in, hlds_goal::in, hlds_goal::in,
hlds_goal::in, hlds_goal::out, hlds_goal::out) is det.
top_level(switch_base_rec, Goal, OrigBaseGoal, OrigRecGoal,
NewBaseGoal, NewRecGoal, OrigGoal, NewGoal) :-
(
Goal = switch(Var, CanFail, Cases0, StoreMap) - GoalInfo,
Cases0 = [case(IdA, _), case(IdB, _)]
->
OrigCases = [case(IdA, OrigBaseGoal), case(IdB, OrigRecGoal)],
OrigGoal = switch(Var, CanFail, OrigCases, StoreMap) - GoalInfo,
NewCases = [case(IdA, NewBaseGoal), case(IdB, NewRecGoal)],
NewGoal = switch(Var, CanFail, NewCases, StoreMap) - GoalInfo
;
error("top_level: not the correct top level")
).
top_level(switch_rec_base, Goal, OrigBaseGoal, OrigRecGoal,
NewBaseGoal, NewRecGoal, OrigGoal, NewGoal) :-
(
Goal = switch(Var, CanFail, Cases0, StoreMap) - GoalInfo,
Cases0 = [case(IdA, _), case(IdB, _)]
->
OrigCases = [case(IdA, OrigRecGoal), case(IdB, OrigBaseGoal)],
OrigGoal = switch(Var, CanFail, OrigCases, StoreMap) - GoalInfo,
NewCases = [case(IdA, NewRecGoal), case(IdB, NewBaseGoal)],
NewGoal = switch(Var, CanFail, NewCases, StoreMap) - GoalInfo
;
error("top_level: not the correct top level")
).
top_level(disj_base_rec, Goal, OrigBaseGoal,
OrigRecGoal, NewBaseGoal, NewRecGoal, OrigGoal, NewGoal) :-
(
Goal = disj(Goals, StoreMap) - GoalInfo,
Goals = [_, _]
->
OrigGoals = [OrigBaseGoal, OrigRecGoal],
OrigGoal = disj(OrigGoals, StoreMap) - GoalInfo,
NewGoals = [NewBaseGoal, NewRecGoal],
NewGoal = disj(NewGoals, StoreMap) - GoalInfo
;
error("top_level: not the correct top level")
).
top_level(disj_rec_base, Goal, OrigBaseGoal,
OrigRecGoal, NewBaseGoal, NewRecGoal, OrigGoal, NewGoal) :-
(
Goal = disj(Goals, StoreMap) - GoalInfo,
Goals = [_, _]
->
OrigGoals = [OrigRecGoal, OrigBaseGoal],
OrigGoal = disj(OrigGoals, StoreMap) - GoalInfo,
NewGoals = [NewRecGoal, NewBaseGoal],
NewGoal = disj(NewGoals, StoreMap) - GoalInfo
;
error("top_level: not the correct top level")
).
top_level(ite_base_rec, Goal, OrigBaseGoal,
OrigRecGoal, NewBaseGoal, NewRecGoal, OrigGoal, NewGoal) :-
(
Goal = if_then_else(Vars, If, _, _, StoreMap) - GoalInfo
->
OrigGoal = if_then_else(Vars, If,
OrigBaseGoal, OrigRecGoal, StoreMap) - GoalInfo,
NewGoal = if_then_else(Vars, If,
NewBaseGoal, NewRecGoal, StoreMap) - GoalInfo
;
error("top_level: not the correct top level")
).
top_level(ite_rec_base, Goal, OrigBaseGoal,
OrigRecGoal, NewBaseGoal, NewRecGoal, OrigGoal, NewGoal) :-
(
Goal = if_then_else(Vars, If, _, _, StoreMap) - GoalInfo
->
OrigGoal = if_then_else(Vars, If,
OrigRecGoal, OrigBaseGoal, StoreMap) - GoalInfo,
NewGoal = if_then_else(Vars, If,
NewRecGoal, NewBaseGoal, StoreMap) - GoalInfo
;
error("top_level: not the correct top level")
).
%-----------------------------------------------------------------------------%
%
% update_accumulator_pred
%
% Place the accumulator version of the predicate in the
% module_info structure.
%
:- pred update_accumulator_pred(pred_id::in, proc_id::in,
hlds_goal::in, module_info::in, module_info::out) is det.
update_accumulator_pred(NewPredId, NewProcId, AccGoal,
ModuleInfo0, ModuleInfo) :-
module_info_pred_proc_info(ModuleInfo0, NewPredId, NewProcId,
PredInfo, ProcInfo0),
proc_info_set_goal(ProcInfo0, AccGoal, ProcInfo),
module_info_set_pred_proc_info(ModuleInfo0, NewPredId, NewProcId,
PredInfo, ProcInfo, ModuleInfo).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
%
% rename(Ids, Subst, From, Initial)
%
% return a goal_store, Final, which is the result of looking up each
% member of set of goal_ids, Ids, in the goal_store, From,
% applying the substitution and then storing the goal into
% the goal_store, Initial.
%
:- func rename(list(goal_id), subst, goal_store, goal_store) = goal_store.
rename(Ids, Subst, From, Initial) = Final :-
list__foldl((pred(Id::in, GS0::in, GS::out) is det :-
goal_store__lookup(From, Id, Goal0 - InstMap),
goal_util__rename_vars_in_goal(Goal0, Subst, Goal),
goal_store__det_insert(GS0, Id, Goal - InstMap, GS)
), Ids, Initial, Final).
%
% Return all the goal_ids which belong in the base case.
%
:- func base_case_ids(goal_store) = list(goal_id).
base_case_ids(GS) = Base :-
solutions((pred(Key::out) is nondet :-
goal_store__member(GS, Key, _Goal),
Key = base - _
), Base).
%
% Given a list of goal_ids, return the list of hlds_goals from
% the goal_store.
%
:- func goal_list(list(goal_id), goal_store) = hlds_goals.
goal_list(Ids, GS) = Goals :-
list__map((pred(Key::in, G::out) is det :-
goal_store__lookup(GS, Key, G - _)
), Ids, Goals).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- pred calculate_goal_info(hlds_goal_expr::in, hlds_goal::out) is det.
calculate_goal_info(GoalExpr, GoalExpr - GoalInfo) :-
(
GoalExpr = conj(GoalList)
->
goal_list_nonlocals(GoalList, NonLocals),
goal_list_instmap_delta(GoalList, InstMapDelta),
goal_list_determinism(GoalList, Determinism),
goal_info_init(NonLocals, InstMapDelta, Determinism, GoalInfo)
;
error("calculate_goal_info: not a conj.")
).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% The number which indicates the base case.
:- func base = int.
base = 2.
% The number which indicates the recursive case.
:- func rec = int.
rec = 1.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
Index: compiler/assertion.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/assertion.m,v
retrieving revision 1.6
diff -u -r1.6 assertion.m
--- compiler/assertion.m 2000/01/10 00:43:43 1.6
+++ compiler/assertion.m 2000/01/12 13:33:30
@@ -58,15 +58,19 @@
prog_vars::in, pair(prog_var)::out) is semidet.
%
- % assertion__is_associativity_assertion(Id, MI, Vs, CVs)
%
+ % assertion__is_associativity_assertion(Id, MI, Vs, CVs, OV)
+ %
% Does the assertion represented by the assertion id, Id,
% state the associativity of a pred/func?
% We extend the usual definition of associativity to apply to
% predicates or functions with more than two arguments as
% follows by allowing extra arguments which must be invariant.
% If so, this predicate returns (in CVs) the two variables which
- % can be swapped in order if it was a call to Vs.
+ % can be swapped in order if it was a call to Vs, and the
+ % output variable, OV, related to these two variables (for the
+ % case below it would be the variable in the same position as
+ % AB, BC or ABC).
%
% The assertion must be in a form similar to this
% all [Is,A,B,C,ABC]
@@ -80,7 +84,21 @@
% identical locations on both sides of the equivalence).
%
:- pred assertion__is_associativity_assertion(assert_id::in, module_info::in,
- prog_vars::in, pair(prog_var)::out) is semidet.
+ prog_vars::in, pair(prog_var)::out, prog_var::out) is semidet.
+
+ %
+ % assertion__is_construction_equivalence_assertion(Id, MI, C, P)
+ %
+ % Can a single construction unification whose functor is
+ % determined by the cons_id, C, be expressed as a call
+ % to the predid, P (with possibly some construction unifications
+ % to initialise the arguments).
+ %
+ % The assertion will be in a form similar to
+ % all [L,H,T] ( L = [H|T] <=> append([H], T, L) )
+ %
+:- pred assertion__is_construction_equivalence_assertion(assert_id::in,
+ module_info::in, cons_id::in, pred_id::in) is semidet.
%
% assertion__in_interface_check
@@ -97,7 +115,8 @@
:- implementation.
-:- import_module globals, goal_util, hlds_out, options, prog_out, type_util.
+:- import_module globals, goal_util, hlds_out.
+:- import_module options, prog_out, prog_util, type_util.
:- import_module assoc_list, bool, list, map, require, set, std_util.
:- type subst == map(prog_var, prog_var).
@@ -153,8 +172,60 @@
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
+assertion__is_construction_equivalence_assertion(AssertId, Module,
+ ConsId, PredId) :-
+ assertion__goal(AssertId, Module, Goal),
+ equivalent(Goal, P, Q),
+ (
+ single_construction(P, ConsId)
+ ->
+ predicate_call(Q, PredId)
+ ;
+ single_construction(Q, ConsId),
+ predicate_call(P, PredId)
+ ).
+
+ %
+ % One side of the equivalence must be just the single
+ % unification with the correct cons_id.
+ %
+:- pred single_construction(hlds_goal::in, cons_id::in) is semidet.
+
+single_construction(unify(_, UnifyRhs, _, _, _) - _,
+ cons(QualifiedSymName, Arity)) :-
+ UnifyRhs = functor(cons(UnqualifiedSymName, Arity), _),
+ match_sym_name(UnqualifiedSymName, QualifiedSymName).
+
+ %
+ % The side containing the predicate call must be a single call
+ % to the predicate with 0 or more construction unifications
+ % which setup the arguments to the predicates.
+ %
+:- pred predicate_call(hlds_goal::in, pred_id::in) is semidet.
+
+predicate_call(Goal, PredId) :-
+ (
+ Goal = conj(Goals) - _
+ ->
+ list__member(Call, Goals),
+ Call = call(PredId, _, _, _, _, _) - _,
+ list__delete(Goals, Call, Unifications),
+ P = (pred(G::in) is semidet :-
+ not (
+ G = unify(_, UnifyRhs, _, _, _) - _,
+ UnifyRhs = functor(_, _)
+ )
+ ),
+ list__filter(P, Unifications, [])
+ ;
+ Goal = call(PredId, _, _, _, _, _) - _
+ ).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
assertion__is_associativity_assertion(AssertId, Module, CallVars,
- AssociativeVars) :-
+ AssociativeVars, OutputVar) :-
assertion__goal(AssertId, Module, Goal - GoalInfo),
equivalent(Goal - GoalInfo, P, Q),
@@ -163,7 +234,8 @@
P = some(_, _, conj(PCalls) - _) - _PGoalInfo,
Q = some(_, _, conj(QCalls) - _) - _QGoalInfo,
- AssociativeVars = promise_only_solution(associative(PCalls, QCalls,
+ AssociativeVars - OutputVar =
+ promise_only_solution(associative(PCalls, QCalls,
UniversiallyQuantifiedVars, CallVars)).
@@ -178,10 +250,10 @@
% compose(AB, C, ABC) <=> compose(A, BC, ABC)
:- pred associative(hlds_goals::in, hlds_goals::in, set(prog_var)::in,
- prog_vars::in, pair(prog_var)::out) is cc_nondet.
+ prog_vars::in, pair(pair(prog_var), prog_var)::out) is cc_nondet.
associative(PCalls, QCalls, UniversiallyQuantifiedVars, CallVars,
- CallVarA - CallVarB) :-
+ (CallVarA - CallVarB) - OutputVar) :-
reorder(PCalls, QCalls, LHSCalls, RHSCalls),
process_one_side(LHSCalls, UniversiallyQuantifiedVars, AB, PairsL, Vs),
process_one_side(RHSCalls, UniversiallyQuantifiedVars, BC, PairsR, _),
@@ -197,6 +269,8 @@
(AB - ABC) - (BC - ABC)]),
assoc_list__from_corresponding_lists(Vs, CallVars, AssocList),
+ list__filter((pred(X-_Y::in) is semidet :- X = AB),
+ AssocList, [_AB - OutputVar]),
list__filter((pred(X-_Y::in) is semidet :- X = A),
AssocList, [_A - CallVarA]),
list__filter((pred(X-_Y::in) is semidet :- X = B),
@@ -275,7 +349,15 @@
implies(Goal, P, Q) :-
% Goal = (P => Q)
- Goal = not(conj([P, NotQ]) - _) - _,
+ Goal = not(conj(GoalList) - GI) - _,
+ list__reverse(GoalList) = [NotQ | Ps],
+ (
+ Ps = [P0]
+ ->
+ P = P0
+ ;
+ P = conj(list__reverse(Ps)) - GI
+ ),
NotQ = not(Q) - _.
:- pred equivalent(hlds_goal::in, hlds_goal::out, hlds_goal::out) is semidet.
Index: compiler/goal_store.m
===================================================================
RCS file: goal_store.m
diff -N goal_store.m
--- /dev/null Thu Mar 4 04:20:11 1999
+++ goal_store.m Tue Jan 11 15:44:56 2000
@@ -0,0 +1,114 @@
+%-----------------------------------------------------------------------------%
+% Copyright (C) 2000 The University of Melbourne.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%-----------------------------------------------------------------------------%
+%
+% Module: goal_store
+% Main authors: petdr
+%
+% Given a hlds_goal store it in a goal_structure.
+%
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- module goal_store.
+
+:- interface.
+
+:- import_module hlds_goal, hlds_module, instmap.
+:- import_module bool, set, std_util.
+
+%-----------------------------------------------------------------------------%
+
+:- type goal == pair(hlds_goal, instmap).
+:- type goal_store(T).
+
+:- pred goal_store__init(goal_store(T)::out) is det.
+:- func goal_store__init = goal_store(T).
+
+:- pred goal_store__det_insert(goal_store(T)::in, T::in, goal::in,
+ goal_store(T)::out) is det.
+
+:- pred goal_store__lookup(goal_store(T)::in, T::in, goal::out) is det.
+
+:- pred goal_store__member(goal_store(T)::in, T::out, goal::out) is nondet.
+
+:- pred goal_store__all_ancestors(goal_store(T)::in, T::in, module_info::in,
+ bool::in, set(T)::out) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module goal_util.
+:- import_module int, list, map, require.
+
+:- type goal_store(T) == map__map(T, goal).
+
+%-----------------------------------------------------------------------------%
+
+goal_store__init(GS) :-
+ map__init(GS).
+
+goal_store__init = GS :-
+ goal_store__init(GS).
+
+goal_store__det_insert(GS0, Id, Goal, GS) :-
+ map__det_insert(GS0, Id, Goal, GS).
+
+goal_store__lookup(GS, Id, Goal) :-
+ map__lookup(GS, Id, Goal).
+
+goal_store__member(GoalStore, Key, Goal) :-
+ map__member(GoalStore, Key, Goal).
+
+goal_store__all_ancestors(GoalStore, StartId, ModuleInfo, FullyStrict,
+ AncestorIds) :-
+ AncestorIds = ancestors_2(GoalStore, [StartId], set__init,
+ ModuleInfo, FullyStrict).
+
+:- func ancestors_2(goal_store(T), list(T), set(T), module_info, bool) = set(T).
+
+ancestors_2(_GoalStore, [], _VisitedIds, _ModuleInfo, _FullyStrict) = set__init.
+ancestors_2(GoalStore, [Id|Ids], VisitedIds, ModuleInfo, FullyStrict)
+ = AncestorIds :-
+ (
+ set__member(Id, VisitedIds)
+ ->
+ AncestorIds = ancestors_2(GoalStore, Ids, VisitedIds,
+ ModuleInfo, FullyStrict)
+ ;
+ Ancestors = direct_ancestors(GoalStore, Id, ModuleInfo,
+ FullyStrict),
+ AncestorIds = set__list_to_set(Ancestors) `union`
+ ancestors_2(
+ GoalStore,
+ Ancestors `append` Ids,
+ set__insert(VisitedIds, Id),
+ ModuleInfo, FullyStrict)
+
+ ).
+
+:- func direct_ancestors(goal_store(T), T, module_info, bool) = list(T).
+
+direct_ancestors(GoalStore, StartId, ModuleInfo, FullyStrict)
+ = Ancestors :-
+ solutions(direct_ancestor(GoalStore, StartId, ModuleInfo,
+ FullyStrict), Ancestors).
+
+:- pred direct_ancestor(goal_store(T)::in, T::in, module_info::in,
+ bool::in, T::out) is nondet.
+
+direct_ancestor(GoalStore, StartId, ModuleInfo, FullyStrict, EarlierId) :-
+ goal_store__lookup(GoalStore, StartId, LaterGoal - LaterInstMap),
+ goal_store__member(GoalStore, EarlierId, EarlierGoal - EarlierInstMap),
+ compare((<), EarlierId, StartId),
+ not goal_util__can_reorder_goals(ModuleInfo, FullyStrict,
+ EarlierInstMap, EarlierGoal,
+ LaterInstMap, LaterGoal).
+
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
Index: library/list.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/library/list.m,v
retrieving revision 1.89
diff -u -r1.89 list.m
--- library/list.m 2000/01/10 00:44:02 1.89
+++ library/list.m 2000/01/12 05:08:52
@@ -81,6 +81,9 @@
( some [BC]
(list__append(B, C, BC), list__append(A, BC, ABC)) )
).
+ % construction equivalence law.
+:- promise all [L,H,T] ( L = [H|T] <=> list__append([H], T, L)).
+
% list__remove_suffix(List, Suffix, Prefix):
% The same as list__append(Prefix, Suffix, List) except that
----
Peter Ross
PhD Student University of Melbourne
http://www.cs.mu.oz.au/~petdr/
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the developers
mailing list