[m-rev.] for review: new termination analyser (part 4 of 6)
Julien Fischer
juliensf at cs.mu.OZ.AU
Thu Mar 24 15:48:37 AEDT 2005
===================================================================
RCS file: compiler/term_constr_build.m
diff -N compiler/term_constr_build.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_build.m 24 Mar 2005 04:22:07 -0000
@@ -0,0 +1,1171 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%------------------------------------------------------------------------------%
+% Copyright (C) 2003 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.
+%------------------------------------------------------------------------------%
+%
+% file: term_constr_build.m
+% main author: juliensf
+% (partially based on code written by vjteag)
+%
+% This module is responsible for building the abstract representation (AR)
+% used by the constraint termination analyser.
+% (The AR is defined in term_constr_data.m).
+%
+% TODO: make the resulting abstract representations more independent of the
+% HLDS.
+%
+%------------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_build.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module transform_hlds.term_norm.
+:- import_module transform_hlds.term_constr_errors.
+
+:- import_module bool.
+:- import_module io.
+:- import_module list.
+
+%------------------------------------------------------------------------------%
+
+:- type build_options.
+
+:- func build_options_init(functor_info, bool, bool) = build_options.
+
+ % Builds the abstract representation of an SCC.
+ %
+:- pred term_constr_build.build_abstract_scc(dependency_ordering::in,
+ list(pred_proc_id)::in, build_options::in, term2_errors::out,
+ module_info::in, module_info::out, io::di, io::uo) is det.
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module check_hlds.mode_util.
+:- import_module check_hlds.type_util.
+
+:- import_module libs.globals.
+:- import_module libs.lp_rational.
+:- import_module libs.options.
+:- import_module libs.polyhedron.
+:- import_module libs.rat.
+
+:- import_module transform_hlds.dependency_graph.
+:- import_module transform_hlds.term_constr_util.
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_constr_errors.
+:- import_module transform_hlds.termination2.
+
+:- import_module hlds.hlds_data.
+:- import_module hlds.hlds_goal.
+:- import_module hlds.quantification.
+:- import_module hlds.hlds_out.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.mercury_to_mercury.
+:- import_module parse_tree.modules.
+:- import_module parse_tree.prog_data.
+:- import_module parse_tree.prog_type.
+
+:- import_module assoc_list.
+:- import_module counter.
+:- import_module int.
+:- import_module map.
+:- import_module require.
+:- import_module set.
+:- import_module std_util.
+:- import_module string.
+:- import_module svmap.
+:- import_module svvarset.
+:- import_module term.
+:- import_module varset.
+
+%-----------------------------------------------------------------------------%
+%
+% Build pass options.
+%
+
+:- type build_options
+ ---> build_options(
+ functor_info :: functor_info,
+ failure_constrs :: bool,
+ arg_size_only :: bool
+ ).
+
+build_options_init(Norm, Failure, ArgSizeOnly) =
+ build_options(Norm, Failure, ArgSizeOnly).
+
+%-----------------------------------------------------------------------------%
+
+% This information is accumulated while building the abstract representation
+% of a SCC. After we have finished we write it to the module_info.
+% We cannot do this while we are building each individual procedure because we
+% will not have all the information we need until we have finished the
+% processing the entire SCC.
+
+:- type scc_info
+ ---> scc_info(
+ scc_ppid :: pred_proc_id,
+ proc :: abstract_proc,
+ size_var_map :: size_var_map,
+ intermod :: intermod_status,
+ accum_errors :: term2_errors,
+ non_zero_heads :: list(size_var)
+ ).
+
+%-----------------------------------------------------------------------------%
+
+build_abstract_scc(DepOrder, SCC, Options, Errors, !Module, !IO) :-
+ dependency_graph.get_scc_entry_points(SCC, DepOrder, !.Module,
+ EntryProcs),
+ list.foldl3(build_abstract_proc(EntryProcs, Options, SCC, !.Module),
+ SCC, varset.init, Varset, [], AbstractSCC, !IO),
+ module_info_preds(!.Module, PredTable0),
+ RecordInfo = (pred(Info::in, !.Errors::in, !:Errors::out,
+ !.PredTable::in, !:PredTable::out) is det :-
+ Info = scc_info(proc(PredId, ProcId), AR0, VarMap, Status,
+ ProcErrors, HeadSizeVars),
+ %
+ % Record the proper size_varset. Each procedure has a copy.
+ % XXX It would be nicer to store one copy per SCC.
+ %
+ % NOTE: although each procedure in the a SCC shares the same
+ % size_varset, they should all have separate size_var_maps.
+ %
+ AR = AR0 ^ varset := Varset,
+ PredInfo0 = !.PredTable ^ det_elem(PredId),
+ pred_info_procedures(PredInfo0, ProcTable0),
+ ProcInfo0 = ProcTable0 ^ det_elem(ProcId),
+ some [!TermInfo] (
+ proc_info_get_termination2_info(ProcInfo0, !:TermInfo),
+ !:TermInfo = !.TermInfo ^ intermod_status := yes(Status),
+ !:TermInfo = !.TermInfo ^ abstract_rep := yes(AR),
+ !:TermInfo = !.TermInfo ^ size_var_map := VarMap,
+ !:TermInfo = !.TermInfo ^ head_vars := HeadSizeVars,
+ %
+ % If the remainder of the analysis is going to depend upon
+ % higher order constructs then set up the information accordingly.
+ %
+ ( analysis_depends_on_ho(AR) ->
+ !:TermInfo = !.TermInfo ^ success_constrs :=
+ yes(polyhedron.identity),
+ HorderErrors = list.map((func(ho_call(Context))
+ = Context - horder_call), AR ^ ho),
+ list.append(HorderErrors, !Errors)
+ ;
+ true
+ ),
+ proc_info_set_termination2_info(!.TermInfo, ProcInfo0, ProcInfo)
+ ),
+ svmap.det_update(ProcId, ProcInfo, ProcTable0, ProcTable),
+ pred_info_set_procedures(ProcTable, PredInfo0, PredInfo),
+ svmap.det_update(PredId, PredInfo, !PredTable),
+ list.append(ProcErrors, !Errors)
+ ),
+ list.foldl2(RecordInfo, AbstractSCC, [], Errors, PredTable0, PredTable),
+ module_info_set_preds(PredTable, !Module).
+
+:- pred build_abstract_proc(list(pred_proc_id)::in, build_options::in,
+ list(pred_proc_id)::in, module_info::in, pred_proc_id::in,
+ size_varset::in, size_varset::out,
+ list(scc_info)::in, list(scc_info)::out,
+ io::di, io::uo) is det.
+
+build_abstract_proc(EntryProcs, Options, SCC, Module, PPId, !SizeVarset,
+ !AbstractInfo, !IO) :-
+% XXX For debugging ...
+% io.write_string("Building procedure: ", !IO),
+% hlds_out.write_pred_proc_id(Module, PPId, !IO),
+% io.nl(!IO),
+% io.flush_output(!IO),
+ module_info_pred_proc_info(Module, PPId, PredInfo, ProcInfo),
+ pred_info_context(PredInfo, Context),
+ proc_info_vartypes(ProcInfo, VarTypes),
+ proc_info_headvars(ProcInfo, HeadProgVars),
+ proc_info_goal(ProcInfo, Goal),
+ proc_info_argmodes(ProcInfo, ArgModes0),
+ %
+ % Allocate one size_var for each real var. in the procedure.
+ % Work out which variables have zero-size.
+ %
+ allocate_sizevars(HeadProgVars, Goal, SizeVarMap, !SizeVarset),
+ Zeros = find_zero_size_vars(Module, SizeVarMap, VarTypes),
+ Info0 = init_traversal_info(Module, Options ^ functor_info, PPId,
+ Context, VarTypes, Zeros, SizeVarMap, SCC,
+ Options ^ failure_constrs, Options ^ arg_size_only ),
+ %
+ % Traverse the HLDS and construct the abstract version of
+ % this procedure.
+ %
+ build_abstract_goal(Goal, AbstractBody0, Info0, Info),
+ IntermodStatus = Info ^ intermod_status,
+ HeadSizeVars = prog_vars_to_size_vars(SizeVarMap, HeadProgVars),
+ AbstractBody = simplify_abstract_rep(AbstractBody0),
+ %
+ % Work out which arguments can be used in termination proofs.
+ % An argument may be used if (a) it is input and (b) it has
+ % non-zero size.
+ %
+ ChooseArg = (func(Var, Mode) = UseArg :-
+ Type = VarTypes ^ det_elem(Var),
+ (
+ not zero_size_type(Type, Module),
+ mode_util.mode_is_input(Module, Mode)
+ ->
+ UseArg = yes
+ ;
+ UseArg = no
+ )
+ ),
+ Inputs = list.map_corresponding(ChooseArg, HeadProgVars,
+ ArgModes0),
+ %
+ % The size_varset for this procedure is set to rubbish here.
+ % When we complete building this SCC we will set it to
+ % the correct value.
+ %
+ IsEntryPoint = (list.member(PPId, EntryProcs) -> yes ; no),
+ AbstractProc = abstract_proc(real(PPId), Context, Info ^ recursion,
+ SizeVarMap, HeadSizeVars, Inputs, Zeros, AbstractBody,
+ Info ^ maxcalls, !.SizeVarset, Info ^ ho_info, IsEntryPoint),
+
+ ThisProcInfo = scc_info(PPId, AbstractProc, SizeVarMap, IntermodStatus,
+ Info ^ errors, HeadSizeVars),
+
+ list.cons(ThisProcInfo, !AbstractInfo).
+% XXX For debugging ...
+% io.write_string("Abstract proc is:\n", !IO),
+% dump_abstract_proc(AbstractProc, 0, Module, !IO),
+% io.nl(!IO).
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for traversing HLDS goals and collecting constraints from them.
+%
+
+% While traversing the HLDS we accumulate the following information:
+%
+% * The type of recursion present in each procedure.
+%
+% * If the procedure may be involved in intermodule mutual recursion.
+%
+% * The number of calls in each procedure (We can use this information
+% to short-circuit edge labelling in pass 2).
+%
+% * Any calls that are made from the SCC being processed to lower SCCs
+% that do not terminate.
+
+:- type traversal_info
+ ---> traversal_info(
+ recursion :: recursion_type,
+ % What type of recursion is present
+ % in the procedure. ie. `none', `direct', `mutual'.
+
+ intermod_status :: intermod_status,
+ % Record whether this procedure is potentially
+ % involved in mutual recursion across module boundaries.
+
+ errors :: term2_errors,
+ % Errors encountered while building the AR.
+
+ module_info :: module_info,
+ % The HLDS.
+
+ norm :: functor_info,
+ % The norm we are using.
+
+ ppid :: pred_proc_id,
+ % The procedure we are currently processing.
+
+ context :: term.context,
+ % The context of the current procedure.
+
+ types :: vartypes,
+ % Types for all prog_vars in the current procedure.
+
+ zeros :: set(size_var),
+ % size_vars in the current procedure that
+ % are known to have zero-size.
+
+ var_map :: size_var_map,
+ % Map from prog_vars to size_vars.
+
+ scc :: list(pred_proc_id),
+ % The procedures in the same SCC of the call
+ % graph as the one we are current traversing.
+
+ maxcalls :: int,
+ % The number of calls in the procedure.
+
+ find_fail_constrs :: bool,
+ % If no then do not bother looking for failure constraints.
+ % The `--no-term2-propagate-failure-constraints' options.
+
+ ho_info :: list(abstract_ho_call),
+ % Information about any higher-order calls a procedure makes.
+ % XXX Currently unused.
+
+ arg_analysis_only :: bool
+ % Do we only want to run IR analysis?
+ % The `--term2-arg-size-analysis-only' option.
+ ).
+
+:- func init_traversal_info(module_info, functor_info, pred_proc_id,
+ term.context, vartypes, zero_vars, size_var_map, list(pred_proc_id),
+ bool, bool) = traversal_info.
+
+init_traversal_info(ModuleInfo, Norm, PPId, Context, Types, Zeros,
+ VarMap, SCC, FailConstrs, ArgSizeOnly)
+ = traversal_info(none, not_mutually_recursive, [], ModuleInfo, Norm,
+ PPId, Context, Types, Zeros, VarMap, SCC, 0, FailConstrs, [],
+ ArgSizeOnly).
+
+:- pred info_increment_maxcalls(traversal_info::in, traversal_info::out) is det.
+
+info_increment_maxcalls(!Info) :-
+ !:Info = !.Info ^ maxcalls := !.Info ^ maxcalls + 1.
+
+:- pred info_update_errors(term_constr_errors.error::in, traversal_info::in,
+ traversal_info::out) is det.
+
+info_update_errors(Error, !Info) :-
+ !:Info = !.Info ^ errors := [Error | !.Info ^ errors].
+
+:- pred info_update_recursion(recursion_type::in, traversal_info::in,
+ traversal_info::out) is det.
+
+info_update_recursion(RecType, !Info) :-
+ UpdatedRecType = combine_recursion_types(!.Info ^ recursion, RecType),
+ !:Info = !.Info ^ recursion := UpdatedRecType.
+
+:- pred info_update_ho_info(context::in, traversal_info::in,
+ traversal_info::out) is det.
+
+info_update_ho_info(Context, !Info) :-
+ !:Info = !.Info ^ ho_info := [ho_call(Context) | !.Info ^ ho_info].
+
+:- pred set_intermod_status(intermod_status::in, traversal_info::in,
+ traversal_info::out) is det.
+
+set_intermod_status(Status, !TraversalInfo) :-
+ !:TraversalInfo = !.TraversalInfo ^ intermod_status := Status.
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for abstracting goals.
+%
+
+% When constructing the abstract representation of the program
+% this attaches the local variables to the abstract goal.
+% (See comments about local variables in term_constr_data.m for more details.)
+
+:- pred build_abstract_goal(hlds_goal::in, abstract_goal::out,
+ traversal_info::in, traversal_info::out) is det.
+
+build_abstract_goal(Goal, AbstractGoal, !Info) :-
+ build_abstract_goal_2(Goal, AbstractGoal0, !Info),
+ partition_vars(Goal, Locals0, NonLocals0),
+ VarMap = !.Info ^ var_map,
+ Locals = prog_vars_to_size_vars(VarMap, Locals0),
+ NonLocals = prog_vars_to_size_vars(VarMap, NonLocals0),
+ AbstractGoal = update_local_and_nonlocal_vars(AbstractGoal0,
+ Locals, NonLocals).
+
+:- pred build_abstract_goal_2(hlds_goal::in, abstract_goal::out,
+ traversal_info::in, traversal_info::out) is det.
+
+build_abstract_goal_2(conj(Goals)-_, AbstractGoal, !Info) :-
+ list.map_foldl(build_abstract_goal, Goals, AbstractGoals0, !Info),
+ AbstractGoals = simplify_conjuncts(AbstractGoals0),
+ AbstractGoal = conj(AbstractGoals, [], []).
+
+% NOTE: for switches and disjunctions we add the variables that
+% are local to the entire switch/disjunction to the list of variables
+% that are local to each case/disjunct. The reason for this is that
+% the projection operation distributes over the convex hull operation
+% and it is more efficient to eliminate the variables from each branch
+% *before* taking the convex hull. This is because the transformation
+% matrix used by the convex hull operation (see polyhedron.m) will
+% usually be much larger for the entire disjunction than the matrix used
+% for each case/disjunct.
+
+build_abstract_goal_2(disj(Goals) - _, AbstractGoal, !Info) :-
+ build_abstract_disj(non_switch(Goals), AbstractGoal, !Info).
+
+build_abstract_goal_2(Goal - _, AbstractGoal, !Info) :-
+ Goal = switch(SwitchVar, _, Cases),
+ build_abstract_disj(switch(SwitchVar, Cases), AbstractGoal, !Info).
+
+build_abstract_goal_2(Goal - _, AbstractGoal, !Info) :-
+ Goal = if_then_else(_, Cond, Then, Else),
+ %
+ % Reduce the if-then goals to an abstract conjunction.
+ %
+ list.map_foldl(build_abstract_goal, [Cond, Then], AbstractConjuncts,
+ !Info),
+ AbstractSuccessGoal = conj(AbstractConjuncts, [], []),
+ %
+ % Work out a failure constraint for the Cond and then abstract the else
+ % branch. We won't bother do any other simplifications here as the AR
+ % simplification pass will sort all of this out.
+ %
+ CondFail = find_failure_constraint_for_goal(Cond, !.Info),
+ %
+ % XXX FIXME - the local/non-local variable sets end up
+ % being incorrect here.
+ %
+ build_abstract_goal(Else, AbstractElse, !Info),
+ AbstractFailureGoal = conj([CondFail, AbstractElse], [], []),
+ AbstractDisjuncts = [AbstractSuccessGoal, AbstractFailureGoal],
+ AbstractGoal = disj(AbstractDisjuncts, 2, [], []).
+
+build_abstract_goal_2(some(_, _, Goal)-_, AbstractGoal, !Info) :-
+ build_abstract_goal(Goal, AbstractGoal, !Info).
+
+build_abstract_goal_2(Goal - GoalInfo, AbstractGoal, !Info) :-
+ Goal = call(CallPredId, CallProcId, CallArgs, _, _, _),
+ CallSizeArgs = prog_vars_to_size_vars(!.Info ^ var_map, CallArgs),
+ build_abstract_call(proc(CallPredId, CallProcId), CallSizeArgs,
+ GoalInfo, AbstractGoal, !Info).
+
+build_abstract_goal_2(Goal - _, AbstractGoal, !Info) :-
+ Goal = unify(_, _, _, Unification, _),
+ build_abstract_unification(Unification, AbstractGoal, !Info).
+
+build_abstract_goal_2(not(Goal) - _GoalInfo, AbstractGoal, !Info) :-
+ %
+ % Event though a negated goal cannot have any output we still
+ % need to check it for calls to non-terminating procedures.
+ %
+ build_abstract_goal(Goal, _, !Info),
+ %
+ % Find a failure constraint for the goal if
+ % `--term2-propagate-failure-constraints' is enabled,
+ % otherwise just use the constraint that all non-zero input vars
+ % should be non-negative.
+ %
+ AbstractGoal = find_failure_constraint_for_goal(Goal, !.Info).
+
+ % XXX Eventually we should provide some facility for specifying the
+ % arg_size constraints for foreign_procs.
+ %
+build_abstract_goal_2(Goal - GoalInfo, AbstractGoal, !Info) :-
+ Goal = foreign_proc(Attrs, PredId, ProcId, Args, ExtraArgs, _),
+ %
+ % Create non-negativity constraints for each non-zero argument
+ % in the foreign proc.
+ %
+ ForeignArgToVar = (func(ForeignArg) = ForeignArg ^ arg_var),
+ ProgVars = list.map(ForeignArgToVar, Args ++ ExtraArgs),
+ SizeVars = prog_vars_to_size_vars(!.Info ^ var_map, ProgVars),
+ Constraints = make_arg_constraints(SizeVars, !.Info ^ zeros),
+ (
+ (
+ terminates(Attrs) = terminates
+ ;
+ terminates(Attrs) = depends_on_mercury_calls,
+ may_call_mercury(Attrs) = will_not_call_mercury
+ )
+ ->
+ true
+ ;
+ goal_info_get_context(GoalInfo, Context),
+ Error = Context - foreign_proc_called(proc(PredId, ProcId)),
+ info_update_errors(Error, !Info)
+ ),
+ Polyhedron = polyhedron.from_constraints(Constraints),
+ AbstractGoal = primitive(Polyhedron, [], []).
+
+ % XXX At the moment all higher-order calls are eventually treated
+ % as an error. We do not record them as a normal type of error
+ % because this is going to change. To approximate their effect
+ % here just assume that any non-zero output variables from the HO call
+ % are unbounded in size.
+ %
+build_abstract_goal_2(Goal - GoalInfo, AbstractGoal, !Info) :-
+ Goal = generic_call(_, _, _, _),
+ goal_info_get_context(GoalInfo, Context),
+ AbstractGoal = primitive(polyhedron.identity, [], []),
+ info_update_ho_info(Context, !Info).
+
+ % shorthand/1 goals ought to have been transformed away by
+ % the time we get round to termination analysis.
+ %
+build_abstract_goal_2(shorthand(_) - _, _, _, _) :-
+ unexpected(this_file, "shorthand/1 goal during termination analysis.").
+
+ % For the purposes of termination analysis there is no
+ % distinction between parallel conjunctions and normal ones.
+ %
+build_abstract_goal_2(par_conj(Goals) - GoalInfo, AbstractGoal, !Info) :-
+ build_abstract_goal_2(conj(Goals) - GoalInfo, AbstractGoal, !Info).
+
+%------------------------------------------------------------------------------%
+%
+% Additional predicates for abstracting calls.
+%
+
+:- pred build_abstract_call(pred_proc_id::in, size_vars::in,
+ hlds_goal_info::in, abstract_goal::out, traversal_info::in,
+ traversal_info::out) is det.
+
+build_abstract_call(CalleePPId, CallerArgs, GoalInfo, AbstractGoal, !Info) :-
+ goal_info_get_context(GoalInfo, Context),
+ ( if list.member(CalleePPId, !.Info ^ scc)
+ then build_recursive_call(CalleePPId, CallerArgs, Context,
+ AbstractGoal, !Info)
+ else build_non_recursive_call(CalleePPId, CallerArgs, Context,
+ AbstractGoal, !Info)
+ ).
+
+ % If the call is potentially recursive, we construct an abstract call
+ % to represent it - see term_constr_data.m for details.
+ %
+:- pred build_recursive_call(pred_proc_id::in, size_vars::in, prog_context::in,
+ abstract_goal::out, traversal_info::in, traversal_info::out) is det.
+
+build_recursive_call(CalleePPId, CallerArgs, Context, AbstractGoal, !Info) :-
+ CallerPPId = !.Info ^ ppid,
+ CallerZeros = !.Info ^ zeros,
+ ( if CallerPPId = CalleePPId
+ then info_update_recursion(direct_only, !Info)
+ else info_update_recursion(mutual_only, !Info)
+ ),
+ CallerArgConstrs = make_arg_constraints(CallerArgs, CallerZeros),
+ CallerArgPoly = polyhedron.from_constraints(CallerArgConstrs),
+ info_increment_maxcalls(!Info),
+ AbstractGoal = call(real(CalleePPId), Context, CallerArgs,
+ CallerZeros, [], [], CallerArgPoly).
+
+ % For non-recursive calls look up the argument size constraints for the
+ % callee procedure and build an abstract primitive goal to store them.
+ %
+ % If we are running termination analysis, as opposed to just the IR
+ % analysis then we also need to check that the termination status of the
+ % callee procedure.
+ %
+:- pred build_non_recursive_call(pred_proc_id::in, size_vars::in,
+ prog_context::in, abstract_goal::out, traversal_info::in,
+ traversal_info::out) is det.
+
+build_non_recursive_call(CalleePPId, CallerArgs, Context, AbstractGoal,
+ !Info) :-
+ ModuleInfo = !.Info ^ module_info,
+ CallerPPId = !.Info ^ ppid,
+ ZeroVars = !.Info ^ zeros,
+ module_info_pred_proc_info(ModuleInfo, CalleePPId, _, CalleeProcInfo),
+ %
+ % Check the termination status of the callee procedure if we are running a
+ % full analysis - ignore it if we are only running the IR analysis.
+ %
+ proc_info_get_termination2_info(CalleeProcInfo, CalleeTerm2Info),
+ ( !.Info ^ arg_analysis_only = no ->
+ TermStatus = CalleeTerm2Info ^ term_status,
+ (
+ TermStatus = yes(can_loop(_))
+ ->
+ Error = Context - can_loop_proc_called(CallerPPId,
+ CalleePPId),
+ info_update_errors(Error, !Info)
+ ;
+ TermStatus = yes(cannot_loop(_))
+ ->
+ true
+ ;
+ unexpected(this_file, "Callee procedure has no " ++
+ "termination status.")
+ )
+ ;
+ true
+ ),
+ %
+ % Check the arg_size_info for the procedure being called.
+ %
+ ArgSizeInfo = CalleeTerm2Info ^ success_constrs,
+ (
+ ArgSizeInfo = no,
+ unexpected(this_file, "No argument size info for callee proc.")
+ ;
+ ArgSizeInfo = yes(SizeInfo),
+ ArgSizeConstrs0 = polyhedron.non_false_constraints(SizeInfo),
+ (
+ ArgSizeConstrs0 = [],
+ Constraints = []
+ ;
+ ArgSizeConstrs0 = [_ | _],
+ CalleeHeadVars = CalleeTerm2Info ^ head_vars,
+ SubstMap = compose_bijections(CallerArgs, CalleeHeadVars),
+ Constraints0 = lp_rational.substitute_vars(SubstMap,
+ ArgSizeConstrs0),
+ Constraints = lp_rational.set_vars_to_zero(ZeroVars, Constraints0)
+ )
+ ),
+ Polyhedron = polyhedron.from_constraints(Constraints),
+ AbstractGoal = primitive(Polyhedron, [], []).
+
+%------------------------------------------------------------------------------%
+%
+% Additional predicates for abstracting switches and disjunctions.
+%
+
+:- type disj_info
+ ---> switch(prog_var, list(case))
+ ; non_switch(hlds_goals).
+
+:- pred build_abstract_disj(disj_info::in, abstract_goal::out,
+ traversal_info::in, traversal_info::out) is det.
+
+build_abstract_disj(Type, AbstractGoal, !Info) :-
+ (
+ Type = non_switch(Goals),
+ build_abstract_disj_acc(Goals, [], AbstractGoals, !Info)
+ ;
+ Type = switch(SwitchVar, Cases),
+ build_abstract_switch_acc(SwitchVar, Cases, [], AbstractGoals,
+ !Info)
+ ),
+ ( AbstractGoals = [] ->
+ AbstractGoal = primitive(polyhedron.identity, [], [])
+ ; AbstractGoals = [Goal] ->
+ AbstractGoal = Goal
+ ;
+ DisjSize = list.length(AbstractGoals),
+ AbstractGoal = disj(AbstractGoals, DisjSize, [], [])
+ ).
+
+:- pred build_abstract_disj_acc(hlds_goals::in, abstract_goals::in,
+ abstract_goals::out, traversal_info::in, traversal_info::out) is det.
+
+build_abstract_disj_acc([], !AbstractGoals, !Info).
+build_abstract_disj_acc([Goal | Goals], !AbstractGoals, !Info) :-
+ build_abstract_goal(Goal, AbstractGoal, !Info),
+ list.cons(AbstractGoal, !AbstractGoals),
+ build_abstract_disj_acc(Goals, !AbstractGoals, !Info).
+
+ % With switches we need to consider the constraints on the variable
+ % being switched on as well as those from the body of each case.
+ %
+ % For each case we check if the there is a deconstruction
+ % unification involving the switch variable. If there is no such
+ % unification then the constraint for the case will not include a
+ % constraint on the size of the switch-var. In that case we add an
+ % appropriate constraint.
+ %
+ % We add the extra constraint by creating a new primitive abstract
+ % goal and conjoining that to the rest.
+ %
+:- pred build_abstract_switch_acc(prog_var::in, list(case)::in,
+ abstract_goals::in, abstract_goals::out, traversal_info::in,
+ traversal_info::out) is det.
+
+build_abstract_switch_acc(_, [], !AbstractGoals, !Info).
+build_abstract_switch_acc(SwitchProgVar, [case(ConsId, Goal) | Cases],
+ !AbstractGoals, !Info) :-
+ build_abstract_goal(Goal, AbstractGoal0, !Info),
+ %
+ % We now need to check that constraints on the switch var are
+ % included. They will *not* have been included if the case did not
+ % contain a unification deconstructing that variable. They are of
+ % course in the HLDS, just not stored in a way we can derive them
+ % from the goal in the normal fashion unless there is actually a
+ % deconstruction unification present.
+ %
+ ( detect_switch_var(Goal, SwitchProgVar, ConsId) ->
+ AbstractGoal = AbstractGoal0
+ ;
+ TypeMap = !.Info ^ types,
+ SizeVarMap = !.Info ^ var_map,
+ SwitchVarType = TypeMap ^ det_elem(SwitchProgVar),
+ SwitchSizeVar = prog_var_to_size_var(SizeVarMap, SwitchProgVar),
+ ( type_to_ctor_and_args(SwitchVarType, TypeCtor, _) ->
+ Size = functor_lower_bound(!.Info ^ norm, TypeCtor, ConsId,
+ !.Info ^ module_info)
+ ;
+ unexpected(this_file, "variable type in detect_switch_var.")
+ ),
+ ( not set.member(SwitchSizeVar, !.Info ^ zeros) ->
+ SwitchVarConst = rat(Size),
+ SwitchVarConstr =
+ ( Size = 0 ->
+ make_var_const_eq_constraint(SwitchSizeVar,
+ SwitchVarConst)
+ ;
+ make_var_const_gte_constraint(SwitchSizeVar,
+ SwitchVarConst)
+ ),
+ ExtraConstr = [SwitchVarConstr]
+ ;
+ ExtraConstr = []
+ ),
+ ExtraPoly = polyhedron.from_constraints(ExtraConstr),
+ ExtraGoal = primitive(ExtraPoly, [], []),
+ AbstractGoal = conj([ExtraGoal, AbstractGoal0], [], [])
+ ),
+ list.cons(AbstractGoal, !AbstractGoals),
+ build_abstract_switch_acc(SwitchProgVar, Cases, !AbstractGoals, !Info).
+
+:- pred detect_switch_var(hlds_goal::in, prog_var::in, cons_id::in) is semidet.
+
+detect_switch_var(unify(_, _, _, Kind, _)-_, SwitchVar, ConsId) :-
+ ( Kind = deconstruct(SwitchVar, ConsId, _, _, _, _) ->
+ true
+ ; Kind = complicated_unify(_, _, _) ->
+ unexpected(this_file,
+ "complicated_unify/3 goal during termination analysis.")
+ ;
+ fail
+ ).
+detect_switch_var(shorthand(_)-_, _, _) :-
+ unexpected(this_file, "shorthand/1 goal during termination analysis").
+
+%------------------------------------------------------------------------------%
+%
+% Additional predicates for abstracting unifications.
+%
+
+:- pred build_abstract_unification(unification::in, abstract_goal::out,
+ traversal_info::in, traversal_info::out) is det.
+
+build_abstract_unification(Unification, AbstractGoal, !Info) :-
+ Unification = construct(Var, ConsId, ArgVars, Modes, _, _, _),
+ build_abstract_decon_or_con_unify(Var, ConsId, ArgVars, Modes,
+ Constraints, !Info),
+ AbstractGoal = build_goal_from_unify(Constraints).
+
+build_abstract_unification(Unification, AbstractGoal, !Info) :-
+ Unification = deconstruct(Var, ConsId, ArgVars, Modes, _, _),
+ build_abstract_decon_or_con_unify(Var, ConsId, ArgVars, Modes,
+ Constraints, !Info),
+ AbstractGoal = build_goal_from_unify(Constraints).
+
+build_abstract_unification(assign(LVar, RVar), AbstractGoal, !Info) :-
+ build_abstract_simple_or_assign_unify(LVar, RVar, Constraints, !Info),
+ AbstractGoal = build_goal_from_unify(Constraints).
+
+build_abstract_unification(simple_test(LVar, RVar), AbstractGoal, !Info) :-
+ build_abstract_simple_or_assign_unify(LVar, RVar, Constraints, !Info),
+ AbstractGoal = build_goal_from_unify(Constraints).
+
+build_abstract_unification(complicated_unify(_, _, _), _, _, _) :-
+ unexpected(this_file, "complicated_unify/3 in termination analysis.").
+
+:- func build_goal_from_unify(constraints) = abstract_goal.
+
+build_goal_from_unify(Constraints) = primitive(Polyhedron, [], []) :-
+ Polyhedron = polyhedron.from_constraints(Constraints),
+ ( if polyhedron.is_empty(Polyhedron)
+ then unexpected(this_file, "empty polyhedron from unification.")
+ else true
+ ).
+
+%-----------------------------------------------------------------------------
+%
+% Procedures for abstracting unifications.
+%
+
+ % Used for deconstruction and construction unifications. e.g. for a
+ % unification of the form: X = f(U, V, W), if the norm counts the
+ % first and second arguments then the constraint returned is |X| -
+ % |U| - |V| = |f|. (|X| is the size_var corresponding to X).
+ %
+:- pred build_abstract_decon_or_con_unify(prog_var::in, cons_id::in,
+ prog_vars::in, list(uni_mode)::in, constraints::out,
+ traversal_info::in, traversal_info::out) is det.
+
+build_abstract_decon_or_con_unify(Var, ConsId, ArgVars, Modes, Constraints,
+ !Info) :-
+ VarTypes = !.Info ^ types,
+ Type = VarTypes ^ det_elem(Var),
+ (
+ not type_is_higher_order(Type, _, _, _, _),
+ type_to_ctor_and_args(Type, TypeCtor, _)
+ ->
+ Norm = !.Info ^ norm,
+ ModuleInfo = !.Info ^ module_info,
+ Zeros = !.Info ^ zeros,
+ %
+ % We need to strip out any typeinfo related variables before
+ % measuring the size of the term; otherwise functor_norm will
+ % raise a software error if we are using the `num-data-elems'
+ % norm and the term has existential typeclass constraints.
+ %
+ filter_args_and_modes(VarTypes, ArgVars, FixedArgs,
+ Modes, FixedModes),
+
+ functor_norm(Norm, TypeCtor, ConsId, ModuleInfo, Constant,
+ FixedArgs, CountedVars, FixedModes, _),
+ %
+ % The constraint from this unification is:
+ %
+ % |Var| = Constant + sum(CountedVars)
+ %
+ % |Var| is just the size_var corresponding to Var. The
+ % value of `Constant' will depend upon the norm being used.
+ %
+ SizeVar = prog_var_to_size_var(!.Info ^ var_map, Var),
+ ( if set.member(SizeVar, Zeros)
+ then FirstTerm = []
+ else FirstTerm = [SizeVar - one]
+ ),
+ AddTerms = (func(Var1, Terms0) = Terms1 :-
+ SizeVar1 = prog_var_to_size_var(
+ !.Info ^ var_map, Var1),
+ ( if set.member(SizeVar1, Zeros)
+ then Terms1 = Terms0
+ else Terms1 = [SizeVar1 - (-one) | Terms0]
+ )
+ ),
+ Terms = list.foldl(AddTerms, CountedVars, FirstTerm),
+ Constraint = constraint(Terms, (=), rat(Constant)),
+ ( is_false(Constraint) ->
+ unexpected(this_file, "false constraint from unification.")
+ ;
+ SizeVars0 = prog_vars_to_size_vars(!.Info ^ var_map,
+ ArgVars),
+ SizeVars1 = [SizeVar | SizeVars0],
+ SizeVars = list.filter(isnt(is_zero_size_var(!.Info ^ zeros)),
+ SizeVars1)
+ ),
+ NonNegConstraints = list.map(make_nonneg_constr, SizeVars),
+ Constraints = [ Constraint | NonNegConstraints ]
+ ;
+ % The only valid higher-order unifications are assignments
+ % For the purposes of the IR analysis we can ignore them.
+ Constraints = []
+ ).
+
+:- pred filter_args_and_modes(map(prog_var, (type))::in, list(prog_var)::in,
+ list(prog_var)::out, list(uni_mode)::in, list(uni_mode)::out) is det.
+
+filter_args_and_modes(VarTypes, Args0, Args, Modes0, Modes) :-
+ ArgsAndModes0 = assoc_list.from_corresponding_lists(Args0, Modes0),
+ IsNotTypeInfo = (pred(ArgMode::in) is semidet :-
+ map.lookup(VarTypes, fst(ArgMode), Type),
+ not is_introduced_type_info_type(Type)
+ ),
+ list.filter(IsNotTypeInfo, ArgsAndModes0, ArgsAndModes),
+ assoc_list.keys_and_values(ArgsAndModes, Args, Modes).
+
+ % Assignment and simple_test unifications of the form X = Y
+ % are abstracted as |X| - |Y| = 0.
+ %
+:- pred build_abstract_simple_or_assign_unify(prog_var::in, prog_var::in,
+ constraints::out, traversal_info::in, traversal_info::out) is det.
+
+build_abstract_simple_or_assign_unify(LeftProgVar, RightProgVar,
+ Constraints, !Info) :-
+ SizeVarMap = !.Info ^ var_map,
+ Zeros = !.Info ^ zeros,
+ LeftSizeVar = prog_var_to_size_var(SizeVarMap, LeftProgVar),
+ RightSizeVar = prog_var_to_size_var(SizeVarMap, RightProgVar),
+ (
+ set.member(LeftSizeVar, Zeros),
+ set.member(RightSizeVar, Zeros)
+ ->
+ Constraints = [] % `true' constraint.
+ ;
+ (
+ (set.member(LeftSizeVar, Zeros)
+ ; set.member(RightSizeVar, Zeros))
+ ->
+ unexpected(this_file, "zero unified with non-zero.")
+ ;
+ % Create non-negativity constraints.
+ %
+ NonNegConstrs = list.map(make_nonneg_constr,
+ [LeftSizeVar, RightSizeVar]),
+ Terms = [LeftSizeVar - one, RightSizeVar - (-one)],
+ AssignConstr = constraint(Terms, (=), zero),
+ % XXX I don't think this call to simplify helps anymore.
+ Constraints = simplify_constraints([AssignConstr | NonNegConstrs])
+ )
+ ).
+
+%------------------------------------------------------------------------------%
+
+ % Because quantification returns a conservative estimate of nonlocal
+ % vars, this returns a list of local vars that may omit some of the
+ % real local vars. This shouldn't be a problem as everything but
+ % the head_vars will be projected out at the end of each iteration
+ % anyway.
+ %
+:- func local_vars(hlds_goal) = prog_vars.
+
+local_vars(GoalExpr - GoalInfo) = Locals :-
+ goal_info_get_nonlocals(GoalInfo, NonLocals),
+ quantification.goal_vars(GoalExpr - GoalInfo, QuantVars),
+ LocalsSet = set.difference(QuantVars, NonLocals),
+ Locals = set.to_sorted_list(LocalsSet).
+
+ % Partition the variables of a goal into a set of local variables
+ % and a set of non-local variables.
+ %
+:- pred partition_vars(hlds_goal::in, prog_vars::out, prog_vars::out) is det.
+
+partition_vars(GoalExpr - GoalInfo, Locals, NonLocals) :-
+ goal_info_get_nonlocals(GoalInfo, NonLocals0),
+ quantification.goal_vars(GoalExpr - GoalInfo, QuantVars),
+ Locals = set.to_sorted_list(set.difference(QuantVars, NonLocals0)),
+ NonLocals = set.to_sorted_list(NonLocals0).
+
+%-----------------------------------------------------------------------------%
+%
+% Procedures for manipulating sets of size_vars.
+%
+
+ % Create the size_vars corresponding to the given prog_vars. Also
+ % create map from the prog_vars to the size_vars.
+ %
+ % As termination analysis is (currently) carried out before unused
+ % argument analysis it is possible that some variables in the head
+ % of a procedure may not occur in the body (this typically occurs
+ % with typeinfos).
+ %
+:- pred allocate_sizevars(prog_vars::in, hlds_goal::in, size_var_map::out,
+ size_varset::in, size_varset::out) is det.
+
+allocate_sizevars(HeadProgVars, Goal, SizeVarMap, !SizeVarset) :-
+ fill_var_to_sizevar_map(Goal, !SizeVarset, SizeVarMap0),
+ possibly_fix_sizevar_map(HeadProgVars, !SizeVarset, SizeVarMap0,
+ SizeVarMap).
+
+:- pred fill_var_to_sizevar_map(hlds_goal::in,
+ size_varset::in, size_varset::out, size_var_map::out) is det.
+
+fill_var_to_sizevar_map(Goal, !SizeVarset, SizeVarMap) :-
+ quantification.goal_vars(Goal, ProgVarsInGoal),
+ ProgVars = set.to_sorted_list(ProgVarsInGoal),
+ make_size_var_map(ProgVars, !SizeVarset, SizeVarMap).
+
+ % Fix the map in case some variables that are present only
+ % in the head of a procedure were missed.
+ %
+:- pred possibly_fix_sizevar_map(prog_vars::in, size_varset::in,
+ size_varset::out, size_var_map::in, size_var_map::out) is det.
+
+possibly_fix_sizevar_map([], !SizeVarset, !SizeVarMap).
+possibly_fix_sizevar_map([ProgVar | ProgVars], !SizeVarset, !SizeVarMap) :-
+ ( if map.search(!.SizeVarMap, ProgVar, _)
+ then possibly_fix_sizevar_map(ProgVars, !SizeVarset, !SizeVarMap)
+ else
+ svvarset.new_var(SizeVar, !SizeVarset),
+ svmap.set(ProgVar, SizeVar, !SizeVarMap),
+ possibly_fix_sizevar_map(ProgVars, !SizeVarset, !SizeVarMap)
+ ).
+
+%-----------------------------------------------------------------------------%
+%
+% Failure constraints.
+%
+
+% The idea here is that if a goal can fail, the the fact that it fails
+% may tell us information about the size of any input arguments.
+%
+% For unifications, both deconstructions and simple tests can fail but
+% since the latter involves only zero size types it does not tell us
+% anything useful. For a deconstruction unification that can fail we
+% know that the variable must be bound to one of the other type
+% constructors so we can use this to try and place a lower bound on the
+% size of the variable.
+%
+% For calls we can associate a failure constraint with each procedure in
+% the program. In contexts where the call fails we can just look up the
+% failure constraint.
+%
+% In the worst case we just assume that the size of the (non-zero)
+% inputs is unbounded.
+%
+% TODO Better failure constraints for goals other than unifications.
+
+:- func find_failure_constraint_for_goal(hlds_goal, traversal_info)
+ = abstract_goal.
+
+find_failure_constraint_for_goal(Goal, Info) = AbstractGoal :-
+ (
+ Info ^ find_fail_constrs = yes,
+ find_failure_constraint_for_goal_2(Goal, Info, AbstractGoal0)
+ ->
+ AbstractGoal = AbstractGoal0
+ ;
+ goal_info_get_nonlocals(snd(Goal), NonLocalProgVars0),
+ NonLocalProgVars = set.to_sorted_list(NonLocalProgVars0),
+ NonLocalSizeVars = prog_vars_to_size_vars(Info ^ var_map,
+ NonLocalProgVars),
+ Constraints = make_arg_constraints(NonLocalSizeVars,
+ Info ^ zeros),
+ FailPoly = polyhedron.from_constraints(Constraints),
+ AbstractGoal = primitive(FailPoly, [], [])
+ ).
+
+:- pred find_failure_constraint_for_goal_2(hlds_goal::in,
+ traversal_info::in, abstract_goal::out) is semidet.
+
+ % XXX We could factor out a lot of the code used for
+ % substitutions below as the same code is used elsewhere.
+ %
+find_failure_constraint_for_goal_2(Goal - _, Info, AbstractGoal) :-
+ Goal = call(PredId, ProcId, CallArgs, _, _, _),
+ CallSizeArgs0 = prog_vars_to_size_vars(Info ^ var_map, CallArgs),
+ CallSizeArgs = list.filter(isnt(is_zero_size_var(Info ^ zeros)),
+ CallSizeArgs0),
+ ModuleInfo = Info ^ module_info,
+ module_info_pred_proc_info(ModuleInfo, PredId, ProcId, _, ProcInfo),
+ proc_info_get_termination2_info(ProcInfo, TermInfo),
+ MaybeFailureConstrs = TermInfo ^ failure_constrs,
+ (
+ MaybeFailureConstrs = no,
+ FailureConstraints = []
+ ;
+ MaybeFailureConstrs = yes(CalleeFailurePolyhedron),
+ CalleeFailureConstraints =
+ polyhedron.non_false_constraints(CalleeFailurePolyhedron),
+ (
+ CalleeFailureConstraints = [],
+ FailureConstraints = []
+ ;
+ CalleeFailureConstraints = [_ | _],
+ CalleeHeadVars = TermInfo ^ head_vars,
+ SubstMap = compose_bijections(CallSizeArgs, CalleeHeadVars),
+ FailureConstraints = substitute_size_vars(CalleeFailureConstraints,
+ SubstMap)
+ )
+ ),
+ FailurePolyhedron = polyhedron.from_constraints(FailureConstraints),
+ AbstractGoal = primitive(FailurePolyhedron, [], []).
+
+find_failure_constraint_for_goal_2(Goal @ unify(_, _, _, _, _) - _, Info,
+ AbstractGoal) :-
+ find_deconstruct_fail_bound(Goal, Info, Polyhedron),
+ AbstractGoal = primitive(Polyhedron, [], []).
+
+ % Given a deconstruction unification and assuming that it has
+ % failed, find a bound on the size of the variable being
+ % deconstructed.
+ %
+:- pred find_deconstruct_fail_bound(hlds_goal_expr::in, traversal_info::in,
+ polyhedron::out) is semidet.
+
+find_deconstruct_fail_bound(unify(_, _, _, Kind, _), Info, Polyhedron) :-
+ Kind = deconstruct(Var, ConsId, _, _, can_fail, _),
+ Type = Info ^ types ^ det_elem(Var),
+ prog_type.type_to_ctor_and_args(Type, TypeCtor, _),
+ ModuleInfo = Info ^ module_info,
+ type_util.type_constructors(Type, ModuleInfo, Constructors0),
+ ( if ConsId = cons(ConsName0, ConsArity0)
+ then ConsName = ConsName0, ConsArity = ConsArity0
+ else unexpected(this_file,
+ "find_deconstruct_fail_bound/3: non cons cons_id.")
+ ),
+ FindComplement = (pred(Ctor::in) is semidet :-
+ Ctor = ctor(_, _, SymName, Args),
+ list.length(Args, Arity),
+ not (
+ SymName = ConsName,
+ Arity = ConsArity
+ )
+ ),
+ list.filter(FindComplement, Constructors0, Constructors),
+ SizeVar = prog_var_to_size_var(Info ^ var_map, Var),
+ bounds_on_var(Info ^ norm, ModuleInfo, TypeCtor, SizeVar,
+ Constructors, Polyhedron).
+
+ % Given a variable, its type and a list of constructors to which
+ % it could be bound, return a polyhedron representing the bounds
+ % on the size of that variable.
+ %
+:- pred bounds_on_var(functor_info::in, module_info::in, type_ctor::in,
+ size_var::in, list(constructor)::in, polyhedron::out) is det.
+
+bounds_on_var(Norm, ModuleInfo, TypeCtor, Var, Constructors, Polyhedron) :-
+ CtorSizes = list.map(lower_bound(Norm, ModuleInfo, TypeCtor),
+ Constructors),
+ %
+ % Split constructors into those that have zero size and
+ % those that have non-zero size.
+ %
+ list.filter((pred(V::in) is semidet :- V = 0), CtorSizes,
+ ZeroSizeCtors, NonZeroSizeCtors),
+ (
+ ZeroSizeCtors = [], NonZeroSizeCtors = []
+ ->
+ unexpected(this_file, "bounds_on_var/6: " ++
+ "no other constructors for type.")
+ ;
+ ZeroSizeCtors = [_|_], NonZeroSizeCtors = []
+ ->
+ Constraints = [constraint([Var - one], (=), zero)]
+ ;
+ upper_bound_constraints(Norm, ModuleInfo, Var, TypeCtor,
+ Constructors, UpperBoundConstr),
+
+ ( ZeroSizeCtors = [], NonZeroSizeCtors = [C | Cs] ->
+ LowerBound = list.foldl(int.min, Cs, C),
+ LowerBoundConstr = [constraint([Var - one], (>=), rat(LowerBound))]
+ ;
+ LowerBoundConstr = [constraint([Var - one], (>=), zero)]
+ ),
+ Constraints = LowerBoundConstr ++ UpperBoundConstr
+ ),
+ Polyhedron = polyhedron.from_constraints(Constraints).
+
+:- func lower_bound(functor_info, module_info, type_ctor, constructor) = int.
+
+lower_bound(Norm, Module, TypeCtor, Constructor) = LowerBound :-
+ Constructor = ctor(_, _, SymName, Args),
+ Arity = list.length(Args),
+ ConsId = cons(SymName, Arity),
+ LowerBound = functor_lower_bound(Norm, TypeCtor, ConsId, Module).
+
+ % Given a variable, its type and a set of constructors to which it
+ % could be bound, return a constraint that specifies an upper bound
+ % on the size of the variable. An empty list means that there is no
+ % upper bound.
+ %
+:- pred upper_bound_constraints(functor_info::in, module_info::in, size_var::in,
+ type_ctor::in, list(constructor)::in, constraints::out) is det.
+
+upper_bound_constraints(Norm, Module, Var, TypeCtor, Ctors, Constraints) :-
+ %
+ % If all the arguments of a functor are zero sized then we can give
+ % an upper bound on its size. If we have a set of such functors
+ % then the upper bound is the maximum of the individual upper
+ % bounds.
+ %
+ % XXX We could extend this to include functors can only have a
+ % finite size but I'm not sure that it's worth it.
+ %
+ FindUpperBound = (pred(Ctor::in, !.B::in, !:B::out) is semidet :-
+ Ctor = ctor(_, _, SymName, Args),
+ all [Arg] (list.member(Arg, Args) => zero_size_type(snd(Arg), Module)),
+ Arity = list.length(Args),
+ ConsId = cons(SymName, Arity),
+ Bound = functor_lower_bound(Norm, TypeCtor, ConsId, Module),
+ ( if Bound > !.B then !:B = Bound else true )
+ ),
+ ( list.foldl(FindUpperBound, Ctors, 0, Bound0) ->
+ ( if Bound0 = 0
+ then unexpected(this_file, "zero upper bound.")
+ else Constraints = [constraint([Var - one], (=<), rat(Bound0))]
+ )
+ ;
+ Constraints = []
+ ).
+
+%-----------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "term_constr_build.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module transform_hlds.term_constr_build.
+%-----------------------------------------------------------------------------%
Index: compiler/term_constr_data.m
===================================================================
RCS file: compiler/term_constr_data.m
diff -N compiler/term_constr_data.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_data.m 23 Mar 2005 22:58:56 -0000
@@ -0,0 +1,780 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%-----------------------------------------------------------------------------%
+% Copyright (C) 2002 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.
+%-----------------------------------------------------------------------------%
+%
+% file: term_constr_data.m
+% main author: juliensf
+
+% This module defines data structures that are common to all modules in the
+% termination analyser.
+%
+% The main data structure defined here is the abstract representation (AR),
+% which is an abstraction of a Mercury program in terms of linear arithmetic
+% constraints on term sizes.
+
+%------------------------------------------------------------------------------%
+%
+% AR Goals.
+%
+
+% The AR has four kinds of goal:
+%
+% * primitives - a set of primitive constraints representing the
+% abstraction variable size relationships in some
+% HLDS goal.
+%
+% * conjunction - a conjunction of AR goals.
+%
+% * disjunction - a disjunction of AR goals.
+%
+% * calls - an abstraction of intra-SCC calls. Calls to
+% procedures lower down the call-graph are abstracted
+% as primitive AR goals.
+
+% XXX In order to handle higher-order we need to either modify the
+% exiting AR call goal or add a new AR goal type.
+
+%------------------------------------------------------------------------------%
+%
+% Mapping the HLDS to the AR
+%
+
+% 1. unification
+%
+% A HLDS unification of the form:
+%
+% X = f(A, B, C)
+%
+% is converted to a AR primitive goal of the form:
+%
+% { |X| = |A| + |B| + |C| + |f| }
+%
+% where |X| represents the size of the variable X (according to whatever
+% measure we are using). There will also additional non-negativity
+% constraints on any variables that have non-zero size type. Variables
+% of that have zero-size type are not included at all. Variables that
+% represent polymorphic types are included. The code in
+% (term_constr_fixpoint.m and term_constr_pass2.m that processes calls
+% is responsible for dealing with the situation where a polymorphic
+% procedure is called with zero sized arguments).
+%
+% 2. conjunction and parallel conjunction
+%
+% A HLDS conjunction (A, B) is converted to an AR conjunction. Parallel
+% conjunction is treated the same way.
+%
+% 3. disjunction and switches.
+%
+% A HLDS disjunction (A ; B) is converted to an AR disjunction. Switches
+% are similar although we also have to add any constraints on the variable
+% being switched on.
+%
+% 4. calls
+%
+% A HLDS call to a procedure lower down the call graph is abstracted as
+% an AR primitive. A call to something in the same SCC becomes an AR call.
+%
+% 5. negation.
+%
+% A HLDS negation is abstracted as an AR primitive.
+% XXX Mention failure constraints here.
+%
+% 6. existential quantification.
+%
+% Existential quantifications do not affect term sizes are ignored.
+%
+% 8. if-then-else.
+%
+% ( Cond -> Then ; Else ) is abstracted as
+%
+% disj(conj(|Cond|, |Then|), conj(neg(|Cond|), |Else|))
+%
+% (using |Cond| to represent the abstraction of Cond).
+%
+% 9. foreign_procs
+%
+% Currently these map onto a primitive whose variables are unconstrained.
+% XXX Could do better with user supplied information.
+%
+% 10. generic call.
+%
+% XXX As above, need HO analysis to make these work.
+%
+%-----------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_data.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module libs.lp_rational.
+:- import_module libs.polyhedron.
+
+:- import_module parse_tree.prog_data.
+
+:- import_module transform_hlds.term_constr_errors.
+
+:- import_module bool.
+:- import_module io.
+:- import_module list.
+:- import_module map.
+:- import_module set. % XXX We should experiment with different set
+ % implementations.
+
+%-----------------------------------------------------------------------------%
+%
+% Types that are common to all parts of the termination analyser.
+%
+
+ % A size_var is a variable that represents the size (according
+ % to some measure) of a program variable.
+ %
+:- type size_var == lp_var.
+:- type size_vars == list(size_var).
+:- type size_varset == lp_varset.
+
+:- type size_term == lp_term.
+:- type size_terms == lp_terms.
+
+ % A map between prog_vars and their corresponding size_vars.
+ %
+:- type size_var_map == map(prog_var, size_var).
+
+ % The widening strategy used in the fixpoint calculation.
+ % (At present there is only one but we may add others in the future).
+ %
+:- type widening ---> after_fixed_cutoff(int).
+
+ % The result of the argument size analysis.
+ %
+ % NOTE: this is just an indication that everything worked, any
+ % argument size constraint derived will be stored in the
+ % termination2_info structure.
+ %
+:- type arg_size_result
+ ---> ok
+ ; error(term2_errors).
+
+%-----------------------------------------------------------------------------%
+%
+% The abstract representation.
+%
+
+% XXX There should really be a representation for abstract SCCs as
+% some of the data in the abstract_proc structure is actually information
+% about the SCC; currently the relevant information is just duplicated
+% amongst the abstract procs.
+
+:- type abstract_scc == list(abstract_proc).
+
+ % XXX This will need to be extended in order to handle HO calls and
+ % intermodule mutual recursion.
+ %
+ % The idea here is that information about procedures from other
+ % modules/HO information will be turned into `fake' abstract procs.
+ % Using these fake procs we will then fill in the missing bits of
+ % the SCCs that involve intermodule mutual recursion/HO calls, and
+ % then run the analysis on them.
+ %
+ % This is the main reason that we try a eliminate, as much as
+ % possible, dependencies between the AR and the HLDS.
+ %
+:- type abstract_ppid ---> real(pred_proc_id).
+
+:- type abstract_proc
+ ---> abstract_proc(
+ ppid :: abstract_ppid,
+ % The procedure that this is an abstraction of.
+
+ context :: prog_context,
+ % The context of the procedure.
+
+ recursion :: recursion_type,
+ % The type of recursion present in the procedure.
+
+ size_var_map :: size_var_map,
+ % Map from prog_vars to size_vars for the procedure.
+
+ head_vars :: head_vars,
+ % The procedure's arguments (as size_vars).
+
+ inputs :: list(bool),
+ % `yes' if the corresponding argument can be used
+ % as part of a termination proof, `no' otherwise.
+
+ zeros :: zero_vars,
+ % The size_vars that have zero-size.
+
+ body :: abstract_goal,
+ % An abstraction of the body of the procedure.
+
+ calls :: int,
+ % The number of calls made in the body of the
+ % procedure. This is useful for short-circuiting
+ % pass 2.
+
+ varset :: size_varset,
+ % The varset from which the size_vars were
+ % allocated. The linear solver needs this.
+
+ ho :: list(abstract_ho_call),
+ % A list of higher-order calls made by the
+ % procedure. XXX Currently not used.
+
+ is_entry :: bool
+ % Is this procedure called from outside the SCC?
+ ).
+
+ % This is like an error message (and is treated as such
+ % at the moment). It's here because we want to treat information
+ % regarding higher-order constructs differently from other errors.
+ % In particular higher-order constructs will not always be errors
+ % (ie. when we can analyse them properly).
+ %
+:- type abstract_ho_call ---> ho_call(prog_context).
+
+ % NOTE: the AR's notion of local/non-local variables may not
+ % correspond directly to that in the HLDS because of various
+ % transformations performed on the the AR.
+ %
+:- type local_vars == size_vars.
+:- type nonlocal_vars == size_vars.
+
+:- type call_vars == size_vars.
+:- type head_vars == size_vars.
+
+ % `zero_vars' are those variables in a procedure that have
+ % zero size type (as defined in term_norm.m).
+ %
+:- type zero_vars == set(size_var).
+
+ % This is the representation of goals that the termination analyser
+ % works with.
+ %
+:- type abstract_goal
+ ---> disj(
+ disj_goals :: abstract_goals,
+ disj_size :: int,
+ % We keep track of the number of disjuncts for use
+ % in heuristics that may speed up the convex hull
+ % calculation.
+
+ disj_locals :: local_vars,
+ disj_nonlocals :: nonlocal_vars
+ )
+
+ ; conj(
+ conj_goals :: abstract_goals,
+ conj_locals :: local_vars,
+ conj_nonlocals :: nonlocal_vars
+ )
+
+ ; call(
+ call_ppid :: abstract_ppid,
+ call_context :: prog_context,
+ call_vars :: call_vars,
+ call_zeros :: zero_vars,
+ call_locals :: local_vars,
+ call_nonlocals :: nonlocal_vars,
+ call_constrs :: polyhedron
+ )
+
+ ; primitive(
+ prim_constrs :: polyhedron,
+ prim_locals :: local_vars,
+ prim_nonlocals :: nonlocal_vars
+ ).
+
+:- type abstract_goals == list(abstract_goal).
+
+ % This type is used to keep track of intramodule recursion during
+ % the build pass.
+ %
+ % NOTE: if a procedure is (possibly) involved in intermodule recursion
+ % we handle things differently.
+ %
+:- type recursion_type
+ ---> none % Procedure is not recursive.
+
+ ; direct_only % Only recursion is self-calls.
+
+ ; mutual_only % Only recursion is calls to other procs
+ % in the same SCC.
+
+ ; both. % Both types of recursion.
+
+%-----------------------------------------------------------------------------%
+%
+% Functions that operate on the AR.
+%
+
+ % Update the local and nonlocal variable sets associated with an
+ % abstract goal.
+ %
+:- func update_local_and_nonlocal_vars(abstract_goal, local_vars,
+ nonlocal_vars) = abstract_goal.
+
+ % For any two goals whose recursion types are known return the
+ % recursion type of the conjunction of the two goals.
+ %
+:- func combine_recursion_types(recursion_type, recursion_type)
+ = recursion_type.
+
+ % Combines the constraints contained in two primitive goals
+ % into a single primitive goal. It is an error to pass
+ % any other kind of abstract goal as an argument to this
+ % function.
+ %
+:- func combine_primitive_goals(abstract_goal, abstract_goal) = abstract_goal.
+
+ % Take a list of conjoined primitive goals and simplify them
+ % so there is one large block of constraints.
+ %
+:- func simplify_abstract_rep(abstract_goal) = abstract_goal.
+:- func simplify_conjuncts(abstract_goals) = abstract_goals.
+
+ % Succeeds iff the given SCC contains recursion.
+ %
+:- pred scc_contains_recursion(abstract_scc::in) is semidet.
+
+ % Succeeds iff the given procedure is recursive (either directly
+ % or otherwise).
+ %
+:- pred proc_is_recursive(abstract_proc::in) is semidet.
+
+ % Returns the size_varset for this given SCC.
+ %
+:- func varset_from_abstract_scc(abstract_scc) = size_varset.
+
+ % Succeeds iff the results of the analysis depend upon the
+ % values of some higher-order variables.
+ %
+:- pred analysis_depends_on_ho(abstract_proc::in) is semidet.
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates for printing out debugging traces, etc.
+%
+
+ % Dump a representation of the AR to stdout.
+ %
+:- pred dump_abstract_scc(abstract_scc::in, module_info::in, io::di,
+ io::uo) is det.
+
+ % As above. The extra argument specifies the indentation level.
+ %
+:- pred dump_abstract_scc(abstract_scc::in, int::in, module_info::in, io::di,
+ io::uo) is det.
+
+ % Write an abstract_proc to stdout.
+ %
+:- pred dump_abstract_proc(abstract_proc::in, int::in, module_info::in,
+ io::di, io::uo) is det.
+
+ % Write an abstract_goal to stdout.
+ %
+:- pred dump_abstract_goal(module_info::in, size_varset::in, int::in,
+ abstract_goal::in, io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module hlds.hlds_pred.
+:- import_module hlds.hlds_out.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.prog_data.
+
+:- import_module transform_hlds.term_constr_util.
+
+:- import_module counter.
+:- import_module int.
+:- import_module std_util.
+:- import_module string.
+:- import_module varset.
+:- import_module term.
+
+%-----------------------------------------------------------------------------%
+%
+% Functions that operate on the AR.
+%
+
+update_local_and_nonlocal_vars(Goal0, Locals0, NonLocals0) = Goal :-
+ (
+ Goal0 = disj(Goals, Size, Locals1, NonLocals1),
+ Locals = Locals0 ++ Locals1,
+ NonLocals = NonLocals0 ++ NonLocals1,
+ Goal = disj(Goals, Size, Locals, NonLocals)
+ ;
+ Goal0 = conj(Goals, Locals1, NonLocals1),
+ Locals = Locals0 ++ Locals1,
+ NonLocals = NonLocals0 ++ NonLocals1,
+ Goal = conj(Goals, Locals, NonLocals)
+ ;
+ Goal0 = call(PPId, Context, CallVars, Zeros, Locals1, NonLocals1,
+ Polyhedron),
+ Locals = Locals0 ++ Locals1,
+ NonLocals = NonLocals0 ++ NonLocals1,
+ Goal = call(PPId, Context, CallVars, Zeros, Locals, NonLocals,
+ Polyhedron)
+ ;
+ Goal0 = primitive(Polyhedron, Locals1, NonLocals1),
+ Locals = Locals0 ++ Locals1,
+ NonLocals = NonLocals0 ++ NonLocals1,
+ Goal = primitive(Polyhedron, Locals, NonLocals)
+ ).
+
+scc_contains_recursion([]) :- unexpected(this_file, "empty SCC.").
+scc_contains_recursion([Proc | _]) :- Proc ^ recursion \= none.
+
+proc_is_recursive(Proc) :- not Proc ^ recursion = none.
+
+varset_from_abstract_scc([]) = _ :- unexpected(this_file, "empty SCC.").
+varset_from_abstract_scc([Proc | _]) = Proc ^ varset.
+
+analysis_depends_on_ho(Proc) :- list.is_not_empty(Proc ^ ho).
+
+%-----------------------------------------------------------------------------%
+%
+% Code for simplifying the abstract representation.
+%
+
+% XXX We should keep running the simplifications until we arrive at a
+% fixpoint.
+
+simplify_abstract_rep(Goal0) = Goal :- simplify_abstract_rep(Goal0, Goal).
+
+:- pred simplify_abstract_rep(abstract_goal::in, abstract_goal::out) is det.
+
+simplify_abstract_rep(disj(!.Disjuncts, _Size0, Locals, NonLocals), Goal) :-
+ %
+ % Begin by simplifying each disjunct.
+ %
+ list.map(simplify_abstract_rep, !Disjuncts),
+ (
+ !.Disjuncts = [Disjunct]
+ ->
+ % We need to merge the set of locals with the locals from the
+ % disjunct otherwise we will end up throwing away the locals
+ % from the enclosing goal.
+ %
+ Goal = update_local_and_nonlocal_vars(Disjunct, Locals, NonLocals)
+ ;
+ !.Disjuncts = []
+ ->
+ Goal = primitive(polyhedron.identity, [], [])
+ ;
+ Size = list.length(!.Disjuncts),
+ Goal = disj(!.Disjuncts, Size, Locals, NonLocals)
+ ).
+
+simplify_abstract_rep(conj(!.Conjuncts, Locals, NonLocals), Goal) :-
+ list.map(simplify_abstract_rep, !Conjuncts),
+ list.filter(isnt(is_empty_primitive), !Conjuncts),
+ flatten_conjuncts(!Conjuncts),
+ list.filter(isnt(is_empty_conj), !Conjuncts),
+ ( !.Conjuncts = [Conjunct] ->
+ Goal = update_local_and_nonlocal_vars(Conjunct, Locals,
+ NonLocals)
+ ;
+ Goal = conj(!.Conjuncts, Locals, NonLocals)
+ ).
+
+simplify_abstract_rep(Goal @ primitive(_,_,_), Goal).
+simplify_abstract_rep(Goal @ call(_,_,_,_,_,_,_), Goal).
+
+ % Given a conjunction of the abstract goals of the form:
+ % conj(A, B, C, Goals), where A, B and C are primitive goals
+ % transform this to conj(A /\ B /\ C, Goals) where `/\' is
+ % the intersection operator for convex polyhedra. This tries
+ % to simplify the conjunction as much as possible so that
+ % we don't end up doing as much work during the fixpoint calculation.
+ %
+ % Note: because intersection is commutative we could go further
+ % and take the intersection of all the primitive goals in a
+ % conjunction but that unnecessarily increases the size of the edge
+ % labels in pass 2.
+ %
+:- pred flatten_conjuncts(abstract_goals::in, abstract_goals::out) is det.
+
+flatten_conjuncts([], []).
+flatten_conjuncts([Goal], [Goal]).
+flatten_conjuncts([GoalA, GoalB | Others0], NewGoals) :-
+ flatten_conjuncts([GoalB | Others0], Others1),
+ (
+ Others1 = [GoalC | Others],
+ GoalC = primitive(PolyC, LocalsC, NonLocalsC),
+ GoalA = primitive(PolyA, LocalsA, NonLocalsA)
+ ->
+ Poly = polyhedron.intersection(PolyC, PolyA),
+ Locals = LocalsC ++ LocalsA,
+ NonLocals = NonLocalsC ++ NonLocalsA,
+ Goal = primitive(Poly, Locals, NonLocals),
+ NewGoals = [Goal | Others]
+ ;
+ NewGoals = [GoalA | Others1]
+ ).
+
+ % We end up with `empty' primitives by abstracting unifications
+ % that involve variables that have zero size.
+ %
+:- pred is_empty_primitive(abstract_goal::in) is semidet.
+
+is_empty_primitive(primitive(Poly, _, _)) :- polyhedron.is_universe(Poly).
+
+ % We end up with `empty' conjunctions by abstracting conjunctions
+ % that involve variables that have zero size.
+ %
+:- pred is_empty_conj(abstract_goal::in) is semidet.
+
+is_empty_conj(conj([], _, _)).
+
+ % We end up with `empty' disjunctions by abstracting disjunctions
+ % that involve variables that have zero size.
+ %
+:- pred is_empty_disj(abstract_goal::in) is semidet.
+
+is_empty_disj(disj([], _, _, _)).
+
+%-----------------------------------------------------------------------------%
+%
+% Code for dealing with different types of recursion.
+%
+
+combine_recursion_types(none, none) = none.
+combine_recursion_types(none, direct_only) = direct_only.
+combine_recursion_types(none, mutual_only) = mutual_only.
+combine_recursion_types(none, both) = both.
+combine_recursion_types(direct_only, none) = direct_only.
+combine_recursion_types(direct_only, direct_only) = direct_only.
+combine_recursion_types(direct_only, mutual_only) = both.
+combine_recursion_types(direct_only, both) = both.
+combine_recursion_types(mutual_only, none) = mutual_only.
+combine_recursion_types(mutual_only, direct_only) = both.
+combine_recursion_types(mutual_only, mutual_only) = mutual_only.
+combine_recursion_types(mutual_only, both) = both.
+combine_recursion_types(both, none) = both.
+combine_recursion_types(both, direct_only) = both.
+combine_recursion_types(both, mutual_only) = both.
+combine_recursion_types(both, both) = both.
+
+combine_primitive_goals(GoalA, GoalB) = Goal :-
+ (
+ GoalA = primitive(PolyA, LocalsA, NonLocalsA),
+ GoalB = primitive(PolyB, LocalsB, NonLocalsB)
+ ->
+ Poly = polyhedron.intersection(PolyA, PolyB),
+ Locals = LocalsA ++ LocalsB,
+ NonLocals = NonLocalsA ++ NonLocalsB,
+ Goal = primitive(Poly, Locals, NonLocals)
+ ;
+ unexpected(this_file,
+ "non-primitive goals passed to combine_primitive_goals")
+ ).
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates for printing out the abstract data structure.
+% (These are for debugging only)
+%
+
+dump_abstract_scc(SCC, Module, !IO) :- dump_abstract_scc(SCC, 0, Module, !IO).
+
+dump_abstract_scc(SCC, Indent, Module, !IO) :-
+ list.foldl((pred(Proc::in, !.IO::di, !:IO::uo) is det :-
+ indent_line(Indent, !IO),
+ dump_abstract_proc(Proc, Indent, Module, !IO)
+ ), SCC, !IO).
+
+dump_abstract_proc(Proc, Indent, Module, !IO) :-
+ Proc = abstract_proc(AbstractPPId, _, _, _, HeadVars, _ ,_,
+ Body, _, Varset, _, _),
+ indent_line(Indent, !IO),
+ AbstractPPId = real(PPId),
+ hlds_out.write_pred_proc_id(Module, PPId, !IO),
+ io.write_string(" : [", !IO),
+ WriteHeadVars = (pred(Var::in, !.IO::di, !:IO::uo) is det :-
+ varset.lookup_name(Varset, Var, VarName),
+ io.format(VarName ++ "[%d]", [i(term.var_id(Var))], !IO)
+ ),
+ io.write_list(HeadVars, ", ", WriteHeadVars, !IO),
+ io.write_string(" ] :- \n", !IO),
+ dump_abstract_goal(Module, Varset, Indent + 1, Body, !IO).
+
+:- func recursion_type_to_string(recursion_type) = string.
+
+recursion_type_to_string(none) = "none".
+recursion_type_to_string(direct_only) = "direct recursion only".
+recursion_type_to_string(mutual_only) = "mutual recursion only".
+recursion_type_to_string(both) = "mutual and direct recursion".
+
+:- pred dump_abstract_disjuncts(abstract_goals::in, size_varset::in, int::in,
+ module_info::in, io::di, io::uo) is det.
+
+dump_abstract_disjuncts([], _, _, _, !IO).
+dump_abstract_disjuncts([Goal | Goals], Varset, Indent, Module, !IO) :-
+ dump_abstract_goal(Module, Varset, Indent + 1, Goal, !IO),
+ ( Goals \= [] ->
+ indent_line(Indent, !IO),
+ io.write_string(";\n", !IO)
+ ;
+ true
+ ),
+ dump_abstract_disjuncts(Goals, Varset, Indent, Module, !IO).
+
+dump_abstract_goal(Module, Varset, Indent,
+ disj(Goals, Size, Locals, NonLocals), !IO) :-
+ indent_line(Indent, !IO),
+ io.format("disj[%d](\n", [i(Size)], !IO),
+ dump_abstract_disjuncts(Goals, Varset, Indent, Module, !IO),
+ WriteVars = (pred(Var::in, !.IO::di, !:IO::uo) is det :-
+ varset.lookup_name(Varset, Var, VarName),
+ io.write_string(VarName, !IO)
+ ),
+ indent_line(Indent, !IO),
+ io.write_string(" Locals: ", !IO),
+ io.write_list(Locals, ", ", WriteVars, !IO),
+ io.nl(!IO),
+ indent_line(Indent, !IO),
+ io.write_string(" Non-Locals: ", !IO),
+ io.write_list(NonLocals, ", ", WriteVars, !IO),
+ io.nl(!IO),
+ indent_line(Indent, !IO),
+ io.write_string(")\n", !IO).
+
+dump_abstract_goal(Module, Varset, Indent, conj(Goals, Locals, NonLocals),
+ !IO) :-
+ indent_line(Indent, !IO),
+ io.write_string("conj(\n", !IO),
+ list.foldl(dump_abstract_goal(Module, Varset, Indent + 1), Goals, !IO),
+ WriteVars = (pred(Var::in, !.IO::di, !:IO::uo) is det :-
+ varset.lookup_name(Varset, Var, VarName),
+ io.write_string(VarName, !IO)
+ ),
+ indent_line(Indent, !IO),
+ io.write_string(" Locals: ", !IO),
+ io.write_list(Locals, ", ", WriteVars, !IO),
+ io.nl(!IO),
+ indent_line(Indent, !IO),
+ io.write_string(" Non-Locals: ", !IO),
+ io.write_list(NonLocals, ", ", WriteVars, !IO),
+ io.nl(!IO),
+ indent_line(Indent, !IO),
+ io.write_string(")\n", !IO).
+
+dump_abstract_goal(Module, Varset, Indent, call(PPId0, _, CallVars, _, _, _,
+ CallPoly), !IO) :-
+ indent_line(Indent, !IO),
+ io.write_string("call: ", !IO),
+ PPId0 = real(PPId),
+ hlds_out.write_pred_proc_id(Module, PPId, !IO),
+ io.write_string(" : [", !IO),
+ WriteVars = (pred(Var::in, !.IO::di, !:IO::uo) is det :-
+ varset.lookup_name(Varset, Var, VarName),
+ io.write_string(VarName, !IO)
+ ),
+ io.write_list(CallVars, ", ", WriteVars, !IO),
+ io.write_string("]\n", !IO),
+ indent_line(Indent, !IO),
+ io.write_string("Other call constraints:[\n", !IO),
+ polyhedron.write_polyhedron(CallPoly, Varset, !IO),
+ indent_line(Indent, !IO),
+ io.write_string("]\n", !IO).
+
+dump_abstract_goal(_, Varset, Indent, primitive(Poly, _, _), !IO) :-
+ indent_line(Indent, !IO),
+ io.write_string("[\n", !IO),
+ polyhedron.write_polyhedron(Poly, Varset, !IO),
+ indent_line(Indent, !IO),
+ io.write_string("]\n", !IO).
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates for simplifying conjuncts.
+%
+
+% XXX Make this part of the other AR simplification predicates.
+
+simplify_conjuncts(Goals0) = Goals :-
+ simplify_conjuncts(Goals0, Goals).
+
+:- pred simplify_conjuncts(abstract_goals::in, abstract_goals::out) is det.
+
+simplify_conjuncts(Goals0, Goals) :-
+ (
+ Goals0 = []
+ ->
+ Goals = []
+ ;
+ Goals0 = [Goal]
+ ->
+ Goals = [Goal]
+ ;
+ % If the list of conjuncts starts with two primitives
+ % join them together into a single primitive.
+ Goals0 = [GoalA, GoalB | OtherGoals],
+ GoalA = primitive(PolyA, LocalsA, NonLocalsA),
+ GoalB = primitive(PolyB, LocalsB, NonLocalsB)
+ ->
+ Poly = polyhedron.intersection(PolyA, PolyB),
+ Locals = LocalsA ++ LocalsB,
+ NonLocals = NonLocalsA ++ NonLocalsB,
+ Goal = primitive(Poly, Locals, NonLocals),
+ Goals1 = [Goal | OtherGoals],
+ simplify_conjuncts(Goals1, Goals)
+ ;
+ % A /\ (B \/ C) <= (A /\ B) \/ (A \/ C).
+ % Applying this identity improves the accuracy of
+ % the analysis. At the moment we only apply it
+ % in the situation where there is a primitive, followed
+ % by a disjunction.
+ %
+ % XXX This is really the wrong place to do this -
+ % during the fixpoint calculation would be better.
+ %
+ % Goals0 = [GoalA, GoalB | OtherGoals],
+ % GoalA = primitive(_PolyA, LocalsA, NonLocalsA),
+ % GoalB = disj(Disjuncts0, DisjLocals, DisjNonLocals)
+ %->
+ % ExpandConj = (func(Disj0) = Disj :-
+ % Conjs = simplify_conjuncts([GoalA, Disj0]),
+ % Disj = conj(Conjs, LocalsA, NonLocalsA)
+ % ),
+ % Disjuncts = list.map(ExpandConj, Disjuncts0),
+ % Disjunct = disj(Disjuncts, DisjLocals, DisjNonLocals),
+ % Goals1 = [Disjunct | OtherGoals],
+ % simplify_conjuncts(Goals1, Goals)
+ %;
+ Goals = Goals0
+ ).
+
+%-----------------------------------------------------------------------------%
+%
+% Utility predicates.
+%
+
+:- pred indent_line(int::in, io::di, io::uo) is det.
+
+indent_line(N, !IO) :-
+ ( if N > 0
+ then io.write_string(" ", !IO), indent_line(N - 1, !IO)
+ else true
+ ).
+
+%-----------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "term_constr_data.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module transform_hlds.term_constr_data.
+%-----------------------------------------------------------------------------%
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the reviews
mailing list