[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