[m-rev.] for review: new termination analyser (part 5 of 6)

Julien Fischer juliensf at cs.mu.OZ.AU
Thu Mar 24 15:46:45 AEDT 2005


+%-----------------------------------------------------------------------------%
Index: compiler/term_constr_errors.m
===================================================================
RCS file: compiler/term_constr_errors.m
diff -N compiler/term_constr_errors.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_errors.m	9 Mar 2005 03:43:17 -0000
@@ -0,0 +1,282 @@
+%-----------------------------------------------------------------------------%
+% 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.
+%-----------------------------------------------------------------------------%
+%
+% term_constr_errors.m
+% main author: juliensf.
+%
+%-----------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_errors.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module parse_tree.prog_data.
+
+:- import_module io.
+:- import_module list.
+:- import_module std_util.
+
+%-----------------------------------------------------------------------------%
+%
+% Termination 2 Errors
+%
+
+% The termination errors are all in reference to possible non-termination.
+% While it is possible for pass 1 to go amiss the worst that will happen
+% (barring an abnormal abort) is that the size of the arguments will be
+% unconstrained.
+
+:- type termination2_error
+	--->		imported_pred
+				% Termination could not be proved because
+				% it depends upon information from another
+				% module and that information is not
+				% available.
+
+	;		can_loop_proc_called(pred_proc_id, pred_proc_id)
+				% Termination could not be proved because
+				% the procedure called another procedure
+				% that may not terminate.
+
+	;		cond_not_satisfied
+				% Termination could not be proved because
+				% no set of decreasing argument could e found.
+
+	;		horder_call
+				% Termination could not be proved because
+				% the procedure makes higher-order calls.
+
+	;		does_not_term_pragma(pred_id)
+				% Termination could not be proved because
+				% the procedure was marked with a
+				% `does_not_terminate' pragma.
+
+	;		foreign_proc_called(pred_proc_id).
+				% Termination depends upon the properties
+				% of a piece of foreign code that cannot
+				% be established as terminating.
+
+:- type term_constr_errors.error == pair(prog_context, termination2_error).
+
+:- type term2_errors == list(term_constr_errors.error).
+
+%-----------------------------------------------------------------------------%
+
+:- pred report_termination2_errors(list(pred_proc_id)::in, term2_errors::in,
+	module_info::in, module_info::out, io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module libs.globals.
+:- import_module libs.options.
+
+:- import_module parse_tree.error_util.
+:- import_module hlds.hlds_error_util.
+
+:- import_module transform_hlds.term_util.
+
+:- import_module bool.
+:- import_module int.
+:- import_module require.
+:- import_module string.
+
+%-----------------------------------------------------------------------------%
+
+report_termination2_errors(SCC, Errors, !Module, !IO) :-
+	globals.io_lookup_bool_option(check_termination2, NormalErrors, !IO),
+	globals.io_lookup_bool_option(verbose_check_termination2,
+		VerboseErrors, !IO),
+	(
+		IsCheckTerm = (pred(PPId::in) is semidet :-
+			module_info_pred_proc_info(!.Module, PPId, PredInfo, _),
+			not pred_info_is_imported(PredInfo),
+			pred_info_get_markers(PredInfo, Markers),
+			check_marker(Markers, check_termination)
+		),
+		CheckTermPPIds = list.filter(IsCheckTerm, SCC),
+		list.is_not_empty(CheckTermPPIds)
+	->
+		report_term_errors(SCC, Errors, !.Module, !IO),
+		io.set_exit_status(1, !IO),
+		module_info_incr_errors(!Module)
+	;
+		IsNonImported = (pred(PPId::in) is semidet :-
+			module_info_pred_proc_info(!.Module, PPId, PredInfo, _),
+			not pred_info_is_imported(PredInfo)
+		),
+		NonImportedPPIds = list.filter(IsNonImported, SCC),
+		list.is_not_empty(NonImportedPPIds),
+		( VerboseErrors = yes ->
+			PrintErrors = Errors
+		; NormalErrors = yes ->
+			IsNonSimple = (pred(ContextError::in) is semidet :-
+				ContextError = _ - Error,
+				not indirect_error(Error)
+			),
+			PrintErrors0 = list.filter(IsNonSimple, Errors),
+			%
+			% If there are no direct errors report
+			% the indirect ones instead.
+			%
+			( if 	PrintErrors0 = []
+			  then	PrintErrors = Errors
+			  else	PrintErrors = PrintErrors0
+			)
+		;
+			fail
+		)
+	->
+		term_constr_errors.report_term_errors(SCC, PrintErrors,
+			!.Module, !IO)
+	;
+		true
+	).
+
+%-----------------------------------------------------------------------------%
+
+:- pred report_term_errors(list(pred_proc_id)::in, term2_errors::in,
+	module_info::in, io::di, io::uo) is det.
+
+report_term_errors(SCC, Errors, Module, !IO) :-
+	get_context_from_scc(SCC, Module, Context),
+	( SCC = [PPId] ->
+		Pieces0  = [words("Termination of")],
+		ProcName = describe_one_proc_name(Module, should_module_qualify,
+			PPId),
+		Pieces1  = Pieces0 ++ ProcName,
+		Single   = yes(PPId)
+	;
+		Pieces0 = [
+			words("Termination of the mutually"),
+			words("recursive procedures")
+		],
+		ProcNames = describe_several_proc_names(Module,
+			should_module_qualify, SCC),
+		Pieces1 = Pieces0 ++ ProcNames,
+		Single = no
+	),
+	(
+		Errors = [],
+		Pieces2 = [words("not proven, for unknown reason(s).")],
+		write_error_pieces(Context, 0, Pieces1 ++ Pieces2, !IO)
+	;
+		Errors = [Error],
+		Pieces2 = [words("not proven for the following reason:")],
+		write_error_pieces(Context, 0, Pieces1 ++ Pieces2, !IO),
+		output_error(Error, Single, no, 0, Module, !IO)
+	;
+		Errors = [_, _ | _],
+		Pieces2 = [words("not proven for the following reasons:")],
+		write_error_pieces(Context, 0, Pieces1 ++ Pieces2, !IO),
+		output_errors(Errors, Single, 1, 0, Module, !IO)
+	).
+
+:- pred output_errors(term2_errors::in,
+	maybe(pred_proc_id)::in, int::in, int::in, module_info::in,
+	io::di, io::uo) is det.
+
+output_errors([], _, _, _, _, !IO).
+output_errors([Error | Errors], Single, ErrNum0, Indent, Module, !IO) :-
+	output_error(Error, Single, yes(ErrNum0), Indent, Module, !IO),
+	output_errors(Errors, Single, ErrNum0 + 1, Indent, Module, !IO).
+
+:- pred output_error(term_constr_errors.error::in, maybe(pred_proc_id)::in,
+	maybe(int)::in, int::in, module_info::in, io::di, io::uo) is det.
+
+output_error(Context - Error, Single, ErrorNum, Indent, Module, !IO) :-
+	description(Error, Single, Module, Pieces0, _),
+	( ErrorNum = yes(N) ->
+		string.int_to_string(N, Nstr),
+		string.append_list(["Reason ", Nstr, ":"], Preamble),
+		Pieces = [fixed(Preamble) | Pieces0]
+	;
+		Pieces = Pieces0
+	),
+	write_error_pieces(Context, Indent, Pieces, !IO).
+
+:- pred description(termination2_error::in,
+	maybe(pred_proc_id)::in, module_info::in, list(format_component)::out,
+	maybe(pred_proc_id)::out) is det.
+
+description(cond_not_satisfied, _, _, Pieces, no) :-
+	Pieces = [
+		words("The termination condition"),
+		words("is not satisfiable.")
+	].
+
+description(imported_pred, _, _, Pieces, no) :-
+	Pieces = [
+		words("It contains one or more"),
+		words("predicates and/or functions"),
+		words("imported from another module.")
+	].
+
+description(can_loop_proc_called(CallerPPId, CalleePPId),
+		Single, Module, Pieces, no) :-
+	(
+		Single = yes(PPId),
+		require(unify(PPId, CallerPPId), "caller outside this SCC"),
+		Piece1 = [words("It")]
+	;
+		Single = no,
+		ProcName = describe_one_proc_name(Module, should_module_qualify,
+			CallerPPId),
+		Piece1 = ProcName
+	),
+	Piece2 = words("calls"),
+	CalleePiece = describe_one_proc_name(Module, should_module_qualify,
+		CalleePPId),
+	Pieces3 = [words("which could not be proven to terminate.")],
+	Pieces  = Piece1 ++ [Piece2] ++ CalleePiece ++ Pieces3.
+
+description(horder_call, _, _, Pieces, no) :-
+	Pieces = [words("It contains a higher-order call.")].
+
+description(does_not_term_pragma(PredId), Single, Module, Pieces, no) :-
+	Pieces1 = [
+			words("There is a"),
+			fixed("`:- pragma does_not_terminate'"),
+			words("declaration for")
+	],
+	(
+		Single = yes(PPId),
+		PPId = proc(SCCPredId, _),
+		require(unify(PredId, SCCPredId),
+			"does not terminate pragma outside this SCC"),
+		Piece2 = [words("it.")]
+	;
+		Single = no,
+		Piece2Nodot = describe_one_pred_name(Module,
+			should_module_qualify, PredId),
+		Piece2 = Piece2Nodot ++ [words(".")]
+	),
+	Pieces = Pieces1 ++ Piece2.
+
+description(foreign_proc_called(PPId), _Single, Module, Pieces, no) :-
+	Name = describe_one_proc_name(Module, should_module_qualify, PPId),
+	Pieces = [words("There is a call the foreign procedure")] ++
+		Name ++ [words("which is not known to terminate.")].
+
+%-----------------------------------------------------------------------------%
+
+:- pred indirect_error(termination2_error::in) is semidet.
+
+indirect_error(imported_pred).
+indirect_error(horder_call).
+indirect_error(does_not_term_pragma(_)).
+indirect_error(can_loop_proc_called(_, _)).
+
+%-----------------------------------------------------------------------------%
+:- end_module term_constr_errors.
+%-----------------------------------------------------------------------------%
Index: compiler/term_constr_fixpoint.m
===================================================================
RCS file: compiler/term_constr_fixpoint.m
diff -N compiler/term_constr_fixpoint.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_fixpoint.m	24 Mar 2005 04:20:56 -0000
@@ -0,0 +1,484 @@
+%-----------------------------------------------------------------------------%
+% 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_fixpoint.m
+% main author: juliensf
+%
+% TODO:
+% * code for handling calls could do with a cleanup.
+%
+% NOTE: the code in this module should not refer to things in the HLDS
+% (with the exception of the termination2_info slots in the
+%  proc_sub_info structure)
+%
+%-----------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_fixpoint.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_constr_errors.
+
+:- import_module io.
+:- import_module list.
+
+%-----------------------------------------------------------------------------%
+
+    % Calculate the next approximation to the argument size constraints.
+    %
+    % ChangeFlag is `yes' if the constraints for any procedure in the SCC
+    % have changed since the previous iteration.
+    %
+:- pred do_fixpoint_calculation(fixpoint_options::in, list(pred_proc_id)::in,
+    int::in, term2_errors::out, module_info::in, module_info::out,
+    io::di, io::uo) is det.
+
+:- type fixpoint_options.
+
+:- func fixpoint_options_init(widening, int) = fixpoint_options.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- 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 transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_constr_util.
+:- import_module transform_hlds.termination2.
+
+:- import_module hlds.hlds_data.
+:- import_module hlds.hlds_goal.
+:- import_module hlds.hlds_out.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.prog_data.
+
+:- import_module assoc_list.
+:- import_module bool.
+:- import_module int.
+:- import_module map.
+:- import_module set.
+:- import_module std_util.
+:- import_module string.
+:- import_module term.
+:- import_module varset.
+
+%------------------------------------------------------------------------------%
+
+:- type fixpoint_options
+    ---> fixpoint_options(
+        widening :: widening,
+        max_size :: int
+    ).
+
+fixpoint_options_init(Widening, MaxMatrixSize) =
+    fixpoint_options(Widening, MaxMatrixSize).
+
+%------------------------------------------------------------------------------%
+%
+% Perform a fixpoint iteration on the AR.
+%
+
+    % The information for each procedure in the SCC returned by a single
+    % iteration of the fixpoint calculation.
+    %
+:- type iteration_info
+    ---> iteration_info(
+         pred_proc_id,
+         arg_size_poly :: polyhedron,
+         change_flag   :: bool
+    ).
+
+:- type iteration_infos == list(iteration_info).
+
+do_fixpoint_calculation(Options, SCC, Iteration, [], !ModuleInfo, !IO) :-
+    AbstractSCC = get_abstract_scc(!.ModuleInfo, SCC),
+    %
+    % Carry out one iteration of fixpoint computation.  We need to
+    % do this for all SCCs at least once in order to obtain the argument
+    % size constraints for non-recursive procedures.  We could do that
+    % during the build phase for non-recursive procedures (and in fact used
+    % to) but the code ends up being a horrible mess.
+    %
+    list.foldl2(traverse_abstract_proc(Iteration, Options, !.ModuleInfo),
+        AbstractSCC, [], IterationInfos, !IO),
+    ChangeFlag = or_flags(IterationInfos),
+    (
+        ChangeFlag = yes
+    ->
+        list.foldl(update_size_info, IterationInfos, !ModuleInfo),
+        do_fixpoint_calculation(Options, SCC, Iteration + 1,
+            _, !ModuleInfo, !IO)
+    ;
+        % If one of the polyhedra in the SCC has `false' as its
+        % argument size constraint then the analysis failed.  In that
+        % case set the argument size constraints for every procedure
+        % in the SCC to `true'.
+        % XXX Should this be happening?
+        %
+        (
+            list.member(OneInfo, IterationInfos),
+            polyhedron.is_empty(OneInfo ^ arg_size_poly)
+        ->
+            ChangePoly = (func(Info0) = Info :-
+                Identity = polyhedron.identity,
+                Info = Info0 ^ arg_size_poly := Identity
+            ),
+            list.foldl(update_size_info, list.map(ChangePoly, IterationInfos),
+                !ModuleInfo)
+        ;
+            list.foldl(update_size_info, IterationInfos, !ModuleInfo)
+        )
+    ).
+
+:- func or_flags(iteration_infos) = bool.
+
+or_flags([]) = no.
+or_flags([Info | Infos]) = bool.or(Info ^ change_flag, or_flags(Infos)).
+
+:- pred update_size_info(iteration_info::in, module_info::in, module_info::out)
+    is det.
+
+update_size_info(Info, !ModuleInfo) :-
+    Info = iteration_info(PPId, Poly, _),
+    update_arg_size_info(PPId, Poly, !ModuleInfo).
+
+%------------------------------------------------------------------------------%
+
+:- pred traverse_abstract_proc(int::in, fixpoint_options::in,
+    module_info::in, abstract_proc::in, iteration_infos::in,
+    iteration_infos::out, io::di, io::uo) is det.
+
+traverse_abstract_proc(Iteration, Options, ModuleInfo, Proc, !IterationInfo,
+        !IO) :-
+    WideningInfo = Options ^ widening,
+    MaxMatrixSize = Options ^ max_size,
+    AbstractPPId = Proc ^ ppid,
+    AbstractPPId = real(PPId),
+    Varset = Proc ^ varset,
+    Zeros  = Proc ^ zeros,
+    HeadVars = Proc ^ head_vars,
+    %
+    % Print out the debugging traces.
+    %
+    maybe_write_trace(io.write(PPId), !IO),
+    maybe_write_trace(io.write_string(": "), !IO),
+    maybe_write_trace(hlds_out.write_pred_proc_id(ModuleInfo, PPId), !IO),
+    maybe_write_trace(io.write_string(" "), !IO),
+    maybe_write_trace(write_size_vars(Varset, HeadVars), !IO),
+    maybe_write_trace(io.format("\nIteration %d:\n", [i(Iteration)]), !IO),
+    %
+    % Begin by traversing the procedure and calculating the
+    % IR approximation for this iteration.
+    %
+    Info = init_fixpoint_info(ModuleInfo, Varset, PPId, MaxMatrixSize,
+        HeadVars, Zeros),
+
+    some [!Polyhedron] (
+        traverse_abstract_goal(Info, Proc ^ body, polyhedron.identity,
+            !:Polyhedron),
+        polyhedron.optimize(Varset, !Polyhedron),
+        %
+        % XXX Bug workaround - the build pass sometimes stuffs up
+        % the local variable set for if-then-elses.
+        % (See comments in term_constr_build.m).
+        %
+        BugConstrs0 = polyhedron.constraints(!.Polyhedron),
+        ConstrVarsSet = get_vars_from_constraints(BugConstrs0),
+        HeadVarSet = set.from_list(HeadVars),
+        BadVarsSet = set.difference(ConstrVarsSet, HeadVarSet),
+        BadVars = set.to_sorted_list(BadVarsSet),
+        !:Polyhedron = polyhedron.project(BadVars, Varset, !.Polyhedron),
+        polyhedron.optimize(Varset, !Polyhedron),
+        %
+        % XXX End of bug workaround.
+        % Print out the polyhedron obtained during this iteration.
+        %
+        maybe_write_trace(polyhedron.write_polyhedron(!.Polyhedron, Varset),
+            !IO),
+        maybe_write_trace(io.nl, !IO),
+        %
+        % Look up the constraints obtained during the previous
+        % iteration.
+        %
+        ArgSizeInfo = lookup_proc_constr_arg_size_info(ModuleInfo, PPId),
+        %
+        % NOTE: `!.Polyhedron' is the set of constraints obtained by
+        % *this* iteration.  `OldPolyhedron' is the set of constraints
+        % obtained by the *previous* iteration -- which may in fact
+        % be `empty' (false).
+        %
+        (
+            % If there were no constraints for the procedure then
+            % we are at the beginning of the analysis.
+            %
+            ArgSizeInfo = no,
+            OldPolyhedron = polyhedron.empty
+        ;
+            ArgSizeInfo = yes(SizeInfo),
+            SizeInfo = OldPolyhedron
+        ),
+        ( polyhedron.is_empty(!.Polyhedron) ->
+            ( if    polyhedron.is_empty(OldPolyhedron)
+              then  ChangeFlag = no
+              else  unexpected(this_file, "old polyhedron is empty.")
+            )
+        ;
+            % If the procedure is not recursive then we need only perform one
+            % pass over the AR - subsequent iterations will yield the same result.
+            %
+            ( if       Proc ^ recursion = none then ChangeFlag = no
+              else if  polyhedron.is_empty(OldPolyhedron) then ChangeFlag = yes
+              else     test_fixpoint_and_perhaps_widen(WideningInfo, Varset,
+                           Iteration, OldPolyhedron, !Polyhedron, ChangeFlag)
+            )
+        ),
+        ThisIterationInfo = iteration_info(PPId, !.Polyhedron, ChangeFlag)
+    ),
+    list.cons(ThisIterationInfo, !IterationInfo).
+
+%------------------------------------------------------------------------------%
+
+:- type fixpoint_info
+    ---> fixpoint_info(
+        module_info        :: module_info,
+        varset             :: size_varset,
+        ppid               :: pred_proc_id,
+        max_matrix_size    :: int,
+        curr_head_vars     :: head_vars,
+        zeros              :: zero_vars
+    ).
+
+:- func init_fixpoint_info(module_info, size_varset, pred_proc_id, int,
+    head_vars, zero_vars) = fixpoint_info.
+
+init_fixpoint_info(ModuleInfo, Varset, PPId, MaxMatrixSize, HeadVars, Zeros) =
+    fixpoint_info(ModuleInfo, Varset, PPId, MaxMatrixSize, HeadVars, Zeros).
+
+%------------------------------------------------------------------------------%
+
+:- pred traverse_abstract_goal(fixpoint_info::in, abstract_goal::in,
+    polyhedron::in, polyhedron::out) is det.
+
+traverse_abstract_goal(Info, disj(Goals, _Size, Locals, _), !Polyhedron) :-
+    %
+    % There are number of possible improvements that should be made here:
+    %
+    %   - Take the intersection each disjunct with the constraints
+    %     before the disjunction and compute the convex hull of that.
+    %     This is more accurate but slower.  (XXX There is some code for this
+    %     in term_constr_data.m but it needs to be moved here).  To do
+    %     this you need to add the constraints that occur to
+    %     left of the disjunctions to `PriorConstraints'.
+    %
+    %   - Try computing the convex hull of large disjunctions
+    %     pairwise rather than linearly.  There is code to do this
+    %     below but we currently don't use it.
+    %
+    PriorConstraints = polyhedron.identity,
+    traverse_abstract_disj_linearly(Goals, Locals, Info, PriorConstraints,
+        Polyhedron0),
+    post_process_abstract_goal(Locals, Info, Polyhedron0, !Polyhedron).
+
+traverse_abstract_goal(Info, conj(Goals, Locals, _), !Polyhedron) :-
+    list.foldl(traverse_abstract_goal(Info), Goals, polyhedron.identity,
+        Polyhedron0),
+    post_process_abstract_goal(Locals, Info, Polyhedron0, !Polyhedron).
+
+traverse_abstract_goal(Info, AbstractGoal, !Polyhedron) :-
+    AbstractGoal = call(CallPPId0, _, CallVars, CallZeros, Locals, _,
+        CallArgsPoly),
+    CallPPId0 = real(CallPPId),
+    module_info_pred_proc_info(Info ^ module_info, CallPPId, _,
+        CallProcInfo),
+    proc_info_get_termination2_info(CallProcInfo, CallTerm2Info),
+    CallArgSizeInfo = CallTerm2Info ^ success_constrs,
+    (
+        CallArgSizeInfo = no,
+        !:Polyhedron = polyhedron.empty
+    ;
+        CallArgSizeInfo = yes(SizeInfo),
+        ( polyhedron.is_empty(SizeInfo) ->
+            !:Polyhedron = polyhedron.empty
+        ;
+            ( not polyhedron.is_universe(SizeInfo) ->
+                HeadVars = CallTerm2Info ^ head_vars,
+                SubstMap = compose_bijections(CallVars,
+                    HeadVars),
+                Polyhedron0 = polyhedron.substitute_vars(
+                    SubstMap, SizeInfo),
+                Polyhedron1 = intersection(Polyhedron0,
+                    CallArgsPoly),
+                %
+                % Set any zero_vars in the constraints
+                % to zero (ie. delete the terms).  We need
+                % to do this when a polymorphic arguments
+                % are zero sized.
+                %
+                Polyhedron2 = polyhedron.zero_vars(CallZeros,
+                    Polyhedron1),
+                post_process_abstract_goal(Locals, Info,
+                    Polyhedron2, !Polyhedron)
+            ;
+                true    % Constraint store += true
+            )
+        )
+    ).
+
+traverse_abstract_goal(Info, primitive(Poly, Locals, _), !Polyhedron) :-
+    post_process_abstract_goal(Locals, Info, Poly, !Polyhedron).
+
+%------------------------------------------------------------------------------%
+
+:- pred post_process_abstract_goal(size_vars::in, fixpoint_info::in,
+    polyhedron::in, polyhedron::in, polyhedron::out) is det.
+
+post_process_abstract_goal(Locals, Info, GoalPolyhedron0, !Polyhedron) :-
+    ( if    polyhedron.is_empty(GoalPolyhedron0)
+      then  GoalPolyhedron = polyhedron.empty
+      else  GoalPolyhedron = polyhedron.project(Locals, Info ^ varset,
+            GoalPolyhedron0)
+    ),
+    polyhedron.intersection(GoalPolyhedron, !Polyhedron).
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for handling disjunctions.
+%
+
+    % This version computes the convex hull linearly.
+    % That is, ( A ; B ; C ; D) is processed as:
+    %
+    %  ((((identity \/ A ) \/ B ) \/ C ) \/ D)
+    %
+:- pred traverse_abstract_disj_linearly(abstract_goals::in,
+    size_vars::in, fixpoint_info::in, polyhedron::in, polyhedron::out)
+    is det.
+
+traverse_abstract_disj_linearly(Goals, Locals, Info, !Polyhedron) :-
+    list.foldl(traverse_abstract_disjunct_linearly(Info, Locals),
+        Goals, polyhedron.empty, ConvexUnion),
+    polyhedron.intersection(ConvexUnion, !Polyhedron).
+
+:- pred traverse_abstract_disjunct_linearly(fixpoint_info::in,
+    size_vars::in, abstract_goal::in, polyhedron::in, polyhedron::out)
+    is det.
+
+traverse_abstract_disjunct_linearly(Info, Locals, Goal, !Polyhedron) :-
+    Varset = Info ^ varset,
+    traverse_abstract_goal(Info, Goal, polyhedron.identity, Polyhedron0),
+    Polyhedron1 = polyhedron.project(Locals, Varset, Polyhedron0),
+    polyhedron.convex_union(Varset, yes(Info ^ max_matrix_size),
+        Polyhedron1, !Polyhedron).
+
+    % This version computes the convex hull pairwise. That is
+    % ( A ; B ; C ; D) is processed as: (( A \/ B ) \/ ( C \/ D)).
+    %
+    % XXX This code is currently unused.
+    %
+:- pred traverse_abstract_disj_pairwise(abstract_goals::in, size_vars::in,
+    fixpoint_info::in, polyhedron::in, polyhedron::out) is det.
+
+traverse_abstract_disj_pairwise(Goals, Locals, Info, !Polyhedron) :-
+    Varset = Info ^ varset,
+    % XXX at the moment, could be !.Poly...
+    PolyToLeft = polyhedron.identity,
+    %
+    % First convert the list of goals into their corresponding
+    % polyhedra
+    %
+    ToPoly = (func(Goal) = Poly :-
+        traverse_abstract_goal(Info, Goal, PolyToLeft, Poly0),
+        Poly = polyhedron.project(Locals, Varset, Poly0)
+    ),
+    Polyhedra0 = list.map(ToPoly, Goals),
+    %
+    % Now pairwise convex hull them.
+    %
+    HullOp = (func(A, B) = C :-
+        polyhedron.convex_union(Varset, yes(Info ^ max_matrix_size),
+            A, B, C)
+    ),
+    ConvexUnion = pairwise_map(HullOp, [ polyhedron.empty | Polyhedra0]),
+    polyhedron.intersection(ConvexUnion, !Polyhedron).
+
+    % This assumes that the operation in question is associative and
+    % commutative.
+    %
+ :- func pairwise_map(func(T, T) = T, list(T)) = T.
+
+pairwise_map(_, []) = _ :- unexpected(this_file, "pairwise_map: empty list").
+pairwise_map(_,  [X]) = X.
+pairwise_map(Op, List @ [_, _ | _]) = X :-
+    pairwise_map_2(Op, List, [], X0),
+    X = pairwise_map(Op, X0).
+
+:- pred pairwise_map_2(func(T, T) = T, list(T), list(T), list(T)).
+:- mode pairwise_map_2(func(in, in) = out is det, in, in, out) is det.
+
+pairwise_map_2(_,  [], !Acc).
+pairwise_map_2(_,  [X], Acc, [X | Acc]).
+pairwise_map_2(Op, [X, Y | Rest], !Acc) :-
+    list.cons(Op(X, Y), !Acc),
+    pairwise_map_2(Op, Rest, !Acc).
+
+%------------------------------------------------------------------------------%
+%
+% Fixpoint test.
+%
+
+:- pred test_fixpoint_and_perhaps_widen(widening::in, size_varset::in, int::in,
+    polyhedron::in, polyhedron::in, polyhedron::out, bool::out) is det.
+
+test_fixpoint_and_perhaps_widen(after_fixed_cutoff(Threshold), Varset,
+        Iteration, OldPoly, NewPoly, ResultPoly, ChangeFlag) :-
+    ( Iteration > Threshold ->
+        ResultPoly = widen(OldPoly, NewPoly, Varset)
+    ;
+        ResultPoly = NewPoly
+    ),
+    ChangeFlag = test_fixpoint(NewPoly, OldPoly, Varset).
+
+:- func test_fixpoint(polyhedron, polyhedron, size_varset) = bool.
+
+test_fixpoint(NewPoly, OldPoly, Varset) = ChangeFlag :-
+    %
+    % Constraints from this iteration.
+    %
+    NewConstraints = polyhedron.non_false_constraints(NewPoly),
+    %
+    % Constraints from previous iteration.
+    %
+    OldConstraints = polyhedron.non_false_constraints(OldPoly),
+    UnchangedConstraints = list.filter(entailed(Varset, NewConstraints),
+         OldConstraints),
+    ( if    list.same_length(OldConstraints, UnchangedConstraints)
+      then  ChangeFlag = no
+      else  ChangeFlag = yes
+    ).
+
+%-----------------------------------------------------------------------------
+
+:- func this_file = string.
+
+this_file = "term_constr_fixpoint.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module transform_hlds.term_constr_fixpoint.
+%-----------------------------------------------------------------------------%
Index: compiler/term_constr_initial.m
===================================================================
RCS file: compiler/term_constr_initial.m
diff -N compiler/term_constr_initial.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_initial.m	24 Mar 2005 04:19:36 -0000
@@ -0,0 +1,586 @@
+%-----------------------------------------------------------------------------%
+% 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_initial.m
+% main author: juliensf
+%
+% This module fills in the appropriate argument size information and
+% termination property for builtin and compiler generated predicates.
+% It also handles the processing of termination pragmas and sets
+% the termination properties for foreign procedures.
+
+% Handling of pragma terminates/does_not_terminate
+%
+% At the moment we set the termination status as appropriate, set the arg
+% size information to true and fill in the size_var_map with dummy values
+% (because intermodule optimization requires these values to be in place).
+% If we ever support user specified arg size constraints this scheme
+% will need modifying - in particular we will need to make sure that
+% the identity of the variables in the size_var_map matches those
+% in the constraints.
+
+% A lot of this code is based on that in termination.m that does the
+% equivalent jobs for the old termination analyser.
+
+%----------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_initial.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+
+:- import_module io.
+
+    % Prepare a module for running the main termination pass.
+    % This involves setting up argument size and termination information
+    % for builtin and compiler-generated predicates and also setting
+    % the termination status of those predicates that have termination
+    % pragmas attached to them.
+    %
+    % XXX Fix handling of terminates/does_not_terminate foreign proc.
+    % attributes.
+    %
+:- pred term_constr_initial.preprocess_module(module_info::in,
+    module_info::out, io::di, io::uo) is det.
+
+%----------------------------------------------------------------------------%
+%----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module check_hlds.inst_match.
+:- import_module check_hlds.mode_util.
+:- import_module check_hlds.type_util.
+
+:- import_module hlds.hlds_data.
+:- import_module hlds.hlds_goal.
+:- import_module hlds.hlds_pred.
+:- import_module hlds.hlds_out.
+:- import_module hlds.passes_aux.
+:- import_module hlds.special_pred.
+
+:- import_module libs.globals.
+:- import_module libs.lp_rational.
+:- import_module libs.options.
+:- import_module libs.polyhedron.
+:- import_module libs.rat.
+
+:- import_module mdbcomp.prim_data.
+
+:- 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_out.
+:- import_module parse_tree.prog_util.
+
+:- import_module transform_hlds.termination2.
+:- import_module transform_hlds.dependency_graph.
+:- import_module transform_hlds.term_constr_util.
+:- import_module transform_hlds.term_constr_errors.
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_norm.
+
+:- import_module bool.
+:- import_module bag.
+:- import_module char.
+:- import_module int.
+:- import_module list.
+:- import_module map.
+:- import_module relation.
+:- 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.
+
+%----------------------------------------------------------------------------%
+%
+% Process each predicate and set the termination property
+%
+
+% Sets termination to `cannot_loop' if:
+%   - there is a `terminates' pragma defined for the predicate.
+%   - there is a `check_termination' pragma defined for the predicate
+%     *and* the compiler is not currently generating the intermodule
+%     optimization file.
+%   - the predicate is builtin or compiler generated.  (These are assumed
+%     to terminate.
+%
+%  Set the termination to `can_loop' if:
+%   - there is a `does_not_terminate' pragma defined for this predicate.
+%   - the predicate is imported and there is no other source of information
+%   - about it (termination_info pragmas, terminates pragmas, builtin).
+%
+% XXX This does the wrong thing for copy/2 & typed_unify/2.  In both
+% cases the constraints should that |HeadVar__1| = |HeadVar__2|.
+
+preprocess_module(!ModuleInfo, !IO) :-
+    module_info_predids(!.ModuleInfo, PredIds),
+    process_builtin_preds(PredIds, !ModuleInfo, !IO),
+    process_imported_preds(PredIds, !ModuleInfo).
+
+%----------------------------------------------------------------------------%
+%
+% Set the argument size constraints for imported procedures.
+%
+
+% When interargument size constraints are imported from other modules there
+% are two parts.  The first of the these is a list of ints.  Each int
+% represents one of a procedures arguments (including typeinfo related ones).
+%
+% XXX Since typeinfos all became zero-sized we don't actually need this list.
+% (I forget the reason we did need it, I think it was something to do with
+% the fact that the compiler cannot (presently) distinguish between typeinfos
+% it has introduced and ones that were there anyway - in some of the library
+% modules).
+%
+% The second piece of information here is the constraints themselves which
+% have been using the integer variable ids to represent actual variables.
+%
+% We now know the actual head_vars so we create size_vars and substitute
+% these into the actual constraints.
+%
+
+:- pred process_imported_preds(list(pred_id)::in,
+    module_info::in, module_info::out) is det.
+
+process_imported_preds(PredIds, !ModuleInfo) :-
+    list.foldl(process_imported_pred, PredIds, !ModuleInfo).
+
+:- pred process_imported_pred(pred_id::in, module_info::in, module_info::out)
+    is det.
+
+process_imported_pred(PredId, !ModuleInfo) :-
+    some [!PredTable] (
+        module_info_preds(!.ModuleInfo, !:PredTable),
+        module_info_type_spec_info(!.ModuleInfo, TypeSpecInfo),
+        TypeSpecInfo = type_spec_info(_, TypeSpecPredIds, _, _),
+        ( not set.member(PredId, TypeSpecPredIds) ->
+            PredInfo0 = !.PredTable  ^ det_elem(PredId),
+            process_imported_procs(PredInfo0, PredInfo),
+            svmap.det_update(PredId, PredInfo, !PredTable),
+            module_info_set_preds(!.PredTable, !ModuleInfo)
+        ;
+            true
+        )
+    ).
+
+:- pred process_imported_procs(pred_info::in, pred_info::out) is det.
+
+process_imported_procs(!PredInfo) :-
+    some [!ProcTable] (
+        pred_info_procedures(!.PredInfo, !:ProcTable),
+        ProcIds = pred_info_procids(!.PredInfo),
+        list.foldl(process_imported_proc, ProcIds, !ProcTable),
+        pred_info_set_procedures(!.ProcTable, !PredInfo)
+    ).
+
+:- pred process_imported_proc(proc_id::in, proc_table::in, proc_table::out)
+    is det.
+
+process_imported_proc(ProcId, !ProcTable) :-
+    some [!ProcInfo] (
+        !:ProcInfo = !.ProcTable ^ det_elem(ProcId),
+        proc_info_get_termination2_info(!.ProcInfo, TermInfo0),
+        process_imported_term_info(!.ProcInfo, TermInfo0, TermInfo),
+        proc_info_set_termination2_info(TermInfo, !ProcInfo),
+        svmap.det_update(ProcId, !.ProcInfo, !ProcTable)
+    ).
+
+:- pred process_imported_term_info(proc_info::in,
+    termination2_info::in, termination2_info::out) is det.
+
+process_imported_term_info(ProcInfo, !TermInfo) :-
+    ( !.TermInfo ^ import_headvarids = yes(HeadVarIds) ->
+        proc_info_headvars(ProcInfo, HeadVars),
+        make_size_var_map(HeadVars, _SizeVarset, SizeVarMap),
+        map.from_corresponding_lists(HeadVarIds, HeadVars, IdsToProgVars),
+        create_substitution_map(HeadVarIds, IdsToProgVars, SizeVarMap,
+            SubstMap),
+        create_arg_size_polyhedron(SubstMap, !.TermInfo ^ import_success,
+            MaybeSuccessPoly),
+        create_arg_size_polyhedron(SubstMap, !.TermInfo ^ import_failure,
+            MaybeFailurePoly),
+        SizeVars = prog_vars_to_size_vars(SizeVarMap, HeadVars),
+        !:TermInfo = !.TermInfo ^ size_var_map := SizeVarMap,
+        !:TermInfo = !.TermInfo ^ head_vars := SizeVars,
+        !:TermInfo = !.TermInfo ^ success_constrs := MaybeSuccessPoly,
+        !:TermInfo = !.TermInfo ^ failure_constrs := MaybeFailurePoly,
+        !:TermInfo = !.TermInfo ^ import_headvarids := no,
+        !:TermInfo = !.TermInfo ^ import_success := no,
+        !:TermInfo = !.TermInfo ^ import_failure := no
+    ;
+        true
+    ).
+
+:- pred create_substitution_map(list(int)::in, map(int, prog_var)::in,
+    size_var_map::in, map(int, size_var)::out) is det.
+
+create_substitution_map(Ids, IdToProgVar, SizeVarMap, IdToSizeVar) :-
+    list.foldl((pred(Id::in, !.Map::in, !:Map::out) is det :-
+            ProgVar = IdToProgVar ^ det_elem(Id),
+            SizeVar = map.lookup(SizeVarMap, ProgVar),
+            svmap.set(Id, SizeVar, !Map)
+        ), Ids, map.init, IdToSizeVar).
+
+:- pred create_arg_size_polyhedron(map(int, var)::in,
+    maybe(pragma_constr_arg_size_info)::in, maybe(polyhedron)::out) is det.
+
+create_arg_size_polyhedron(_, no, no).
+create_arg_size_polyhedron(SubstMap, yes(PragmaArgSizeInfo),
+        yes(Polyhedron)) :-
+    list.map(create_arg_size_constraint(SubstMap), PragmaArgSizeInfo,
+        Constraints),
+    Polyhedron = polyhedron.from_constraints(Constraints).
+
+:- pred create_arg_size_constraint(map(int, var)::in, arg_size_constr::in,
+    constraint::out) is det.
+
+create_arg_size_constraint(SubstMap, le(Terms0, Constant), Constraint) :-
+    list.map(create_lp_term(SubstMap), Terms0, Terms),
+    Constraint = constraint(Terms, (=<), Constant).
+create_arg_size_constraint(SubstMap, eq(Terms0, Constant), Constraint) :-
+    list.map(create_lp_term(SubstMap), Terms0, Terms),
+    Constraint = constraint(Terms, (=), Constant).
+
+:- pred create_lp_term(map(int, var)::in, pair(int, rat)::in, lp_term::out)
+    is det.
+
+create_lp_term(SubstMap, VarId - Coefficient, Var - Coefficient) :-
+    Var = SubstMap ^ det_elem(VarId).
+
+%----------------------------------------------------------------------------%
+%
+% Set up information for builtins.
+%
+
+:- pred process_builtin_preds(list(pred_id)::in,
+    module_info::in, module_info::out, io::di, io::uo) is det.
+
+process_builtin_preds([], !ModuleInfo, !IO).
+process_builtin_preds([PredId | PredIds], !ModuleInfo, !IO) :-
+    write_pred_progress_message("% Termination checking ", PredId,
+        !.ModuleInfo, !IO),
+    globals.io_lookup_bool_option(make_optimization_interface, MakeOptInt,
+        !IO),
+    some [!PredTable] (
+        module_info_preds(!.ModuleInfo, !:PredTable),
+        PredInfo0 = !.PredTable ^ det_elem(PredId),
+        process_builtin_procs(MakeOptInt, PredId, !.ModuleInfo,
+            PredInfo0, PredInfo),
+        svmap.det_update(PredId, PredInfo, !PredTable),
+        module_info_set_preds(!.PredTable, !ModuleInfo)
+    ),
+    process_builtin_preds(PredIds, !ModuleInfo, !IO).
+
+    % It is possible for compiler generated/mercury builtin
+    % predicates to be imported or locally defined, so they
+    % must be covered here separately.
+    %
+:- pred process_builtin_procs(bool::in, pred_id::in, module_info::in,
+    pred_info::in, pred_info::out) is det.
+
+process_builtin_procs(MakeOptInt, PredId, ModuleInfo, !PredInfo) :-
+    pred_info_import_status(!.PredInfo, ImportStatus),
+    pred_info_get_markers(!.PredInfo, Markers),
+    pred_info_context(!.PredInfo, Context),
+    some [!ProcTable] (
+        pred_info_procedures(!.PredInfo, !:ProcTable),
+        ProcIds = pred_info_procids(!.PredInfo),
+        (
+            set_compiler_gen_terminates(!.PredInfo, ProcIds, PredId,
+                ModuleInfo, !ProcTable)
+        ->
+            true
+        ;
+            status_defined_in_this_module(ImportStatus, yes)
+        ->
+            % XXX At the moment if a procedure has a pragma terminates
+            % declaration its argument size information is set to true.
+            % If we allow the user to specify the arg size info this
+            % will need to change.  This also means that the
+            % size_var_map for the procedure is never created.  This
+            % causes problems with intermodule optimization.  The
+            % current workaround  is to set up a dummy size_var_map for
+            % each procedure.
+            %
+            ( check_marker(Markers, terminates) ->
+                TermStatus = cannot_loop(pragma_supplied),
+                change_procs_constr_termination_info(ProcIds,
+                    yes, TermStatus, !ProcTable),
+                ArgSizeInfo = polyhedron.identity,
+                change_procs_constr_arg_size_info(ProcIds, yes,
+                    ArgSizeInfo, !ProcTable),
+                initialise_size_var_maps(ProcIds, !ProcTable)
+            ;
+                true
+            )
+        ;
+            % Not defined in this module.
+
+            % All of the predicates that are processed in this section
+            % are imported in some way.  With imported predicates, any
+            % 'check_termination' pragmas will be checked by the
+            % compiler when it compiles the relevant source file (that
+            % the predicate was imported from).  When making the
+            % intermodule optimization interfaces, the check_termination
+            % will not be checked when the relevant source file is compiled,
+            % so it cannot be depended upon.
+            (
+                (
+                    check_marker(Markers, terminates)
+                ;
+                    MakeOptInt = no,
+                    check_marker(Markers, check_termination)
+                )
+            ->
+                change_procs_constr_termination_info(ProcIds, yes,
+                    cannot_loop(pragma_supplied), !ProcTable)
+            ;
+                change_procs_constr_termination_info(ProcIds, no,
+                    can_loop([]), !ProcTable)
+            ),
+            ArgSizeInfo = polyhedron.identity,
+            change_procs_constr_arg_size_info(ProcIds, yes, ArgSizeInfo,
+                !ProcTable)
+        ),
+        ( check_marker(Markers, does_not_terminate) ->
+            TerminationInfo =
+                can_loop([Context - does_not_term_pragma(PredId)]),
+                NonTermArgSizeInfo = polyhedron.identity,
+                change_procs_constr_termination_info(ProcIds, yes,
+                    TerminationInfo, !ProcTable),
+                change_procs_constr_arg_size_info(ProcIds, yes,
+                    NonTermArgSizeInfo, !ProcTable),
+                initialise_size_var_maps(ProcIds, !ProcTable)
+        ;
+            true
+        ),
+        pred_info_set_procedures(!.ProcTable, !PredInfo)
+    ).
+:- pred set_compiler_gen_terminates(pred_info::in, list(proc_id)::in,
+    pred_id::in, module_info::in, proc_table::in, proc_table::out)
+    is semidet.
+
+set_compiler_gen_terminates(PredInfo, ProcIds, PredId, ModuleInfo,
+        !ProcTable) :-
+    ( hlds_pred.pred_info_is_builtin(PredInfo) ->
+        set_builtin_terminates(ProcIds, PredId, PredInfo, ModuleInfo,
+            !ProcTable)
+    ;
+        (
+            Name  = pred_info_name(PredInfo),
+            Arity = pred_info_orig_arity(PredInfo),
+            special_pred_name_arity(SpecPredId0, Name, Arity),
+            ModuleName = pred_info_module(PredInfo),
+            any_mercury_builtin_module(ModuleName)
+        ->
+            SpecialPredId = SpecPredId0
+            ;
+            pred_info_get_origin(PredInfo, PredOrigin),
+            PredOrigin = special_pred(SpecialPredId - _)
+        )
+    ->
+        set_generated_terminates(ProcIds, SpecialPredId, ModuleInfo,
+            !ProcTable)
+    ;
+        fail
+    ).
+
+:- pred set_generated_terminates(list(proc_id)::in, special_pred_id::in,
+    module_info::in, proc_table::in, proc_table::out) is det.
+
+set_generated_terminates([], _, _, !ProcTable).
+set_generated_terminates([ProcId | ProcIds], SpecialPredId, ModuleInfo,
+        !ProcTable) :-
+    %
+    % We don't need to do anything special for solver type initialisation
+    % predicates.  Leaving it up to the analyser may result in better
+    % argument size information anyway.
+    %
+    ( SpecialPredId \= initialise ->
+        ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+        proc_info_headvars(ProcInfo0, HeadVars),
+        proc_info_vartypes(ProcInfo0, VarTypes),
+        special_pred_id_to_termination(SpecialPredId, HeadVars, ModuleInfo,
+            VarTypes, ArgSize, Termination, VarMap, HeadSizeVars),
+        some [!TermInfo] (
+            proc_info_get_termination2_info(ProcInfo0, !:TermInfo),
+            !:TermInfo = !.TermInfo ^ success_constrs := yes(ArgSize),
+            !:TermInfo = !.TermInfo ^ term_status := yes(Termination),
+            IntermodStatus = yes(not_mutually_recursive),
+            !:TermInfo = !.TermInfo ^ intermod_status := IntermodStatus,
+            !:TermInfo = !.TermInfo ^ size_var_map := VarMap,
+            !:TermInfo = !.TermInfo ^ head_vars := HeadSizeVars,
+            proc_info_set_termination2_info(!.TermInfo, ProcInfo0,
+                ProcInfo)
+        ),
+        svmap.det_update(ProcId, ProcInfo, !ProcTable)
+    ;
+        true
+    ),
+    set_generated_terminates(ProcIds, SpecialPredId, ModuleInfo,
+        !ProcTable).
+
+    % Handle the generation of constraints for special predicates.
+    % XXX argument size constraints for unify predicates for types
+    % with user-defined equality may not be correct.
+    %
+:- pred special_pred_id_to_termination(special_pred_id::in, prog_vars::in,
+    module_info::in, vartypes::in, constr_arg_size_info::out,
+    constr_termination_info::out, size_var_map::out, size_vars::out) is det.
+
+special_pred_id_to_termination(compare, HeadProgVars, ModuleInfo, VarTypes,
+        ArgSizeInfo, Termination, SizeVarMap, HeadSizeVars) :-
+    make_info(HeadProgVars, ModuleInfo, VarTypes, ArgSizeInfo, Termination,
+        SizeVarMap, HeadSizeVars).
+special_pred_id_to_termination(unify, HeadProgVars, ModuleInfo, VarTypes,
+        ArgSizeInfo, Termination, SizeVarMap, HeadSizeVars) :-
+    make_size_var_map(HeadProgVars, _SizeVarset, SizeVarMap),
+    HeadSizeVars = prog_vars_to_size_vars(SizeVarMap, HeadProgVars),
+    Zeros = find_zero_size_vars(ModuleInfo, SizeVarMap, VarTypes),
+    NonZeroHeadSizeVars = list.filter(isnt(is_zero_size_var(Zeros)),
+        HeadSizeVars),
+    %
+    % unify may have more than two input arguments if one of them is a
+    % type-info related arg, or some such thing.  Since all these have
+    % zero-size type, after removing them there are two possibilities.
+    % The list of non-zero size type head_vars is empty (if the
+    % arguments are zero-sized) or it contains two elements.
+    %
+    ( NonZeroHeadSizeVars = [] ->
+        Constrs  = []
+    ; NonZeroHeadSizeVars = [VarA, VarB] ->
+        Constrs  = [make_vars_eq_constraint(VarA, VarB)]
+    ;
+        unexpected(this_file, "special_pred_id_to_termination/7: " ++
+             "wrong number of args for unify.")
+    ),
+    Polyhedron  = polyhedron.from_constraints(Constrs),
+    ArgSizeInfo = Polyhedron,
+    Termination = cannot_loop(builtin).
+special_pred_id_to_termination(index, HeadProgVars, ModuleInfo, VarTypes,
+        ArgSize, Termination, SizeVarMap, HeadSizeVars) :-
+    NumToDrop = list.length(HeadProgVars) - 2,
+    ( list.drop(NumToDrop, HeadProgVars, _ZeroSizeHeadVars) ->
+        make_info(HeadProgVars, ModuleInfo, VarTypes, ArgSize,
+            Termination, SizeVarMap, HeadSizeVars)
+    ;
+        unexpected(this_file,
+            "Less than two arguments to builtin index.")
+    ).
+special_pred_id_to_termination(initialise, _, _, _, _, _, _, _) :-
+    unexpected(this_file, "special_pred_id_to_termination/8 " ++
+                "initialise predicate").
+
+    % Sets up the arg_size an termination info for those special preds
+    % (compare and index) where we don't know any arg-size constraints.
+    %
+:- pred make_info(list(prog_var)::in, module_info::in, vartypes::in,
+    constr_arg_size_info::out, constr_termination_info::out,
+    size_var_map::out, size_vars::out) is det.
+
+make_info(HeadProgVars, ModuleInfo, VarTypes, ArgSize, Termination, SizeVarMap,
+        HeadSizeVars) :-
+    make_size_var_map(HeadProgVars, _SizeVarset, SizeVarMap),
+    Zeros = find_zero_size_vars(ModuleInfo, SizeVarMap, VarTypes),
+    Constraints = derive_nonneg_eqns(SizeVarMap, Zeros),
+    Polyhedron = polyhedron.from_constraints(Constraints),
+    ArgSize = Polyhedron,
+    Termination = cannot_loop(builtin),
+    HeadSizeVars = prog_vars_to_size_vars(SizeVarMap, HeadProgVars).
+
+    % Set the termination information for builtin
+    % predicates.  The list of proc_ids must refer to builtin predicates.
+    %
+:- pred set_builtin_terminates(list(proc_id)::in, pred_id::in, pred_info::in,
+    module_info::in, proc_table::in, proc_table::out) is det.
+
+set_builtin_terminates([], _, _, _, !ProcTable).
+set_builtin_terminates([ProcId | ProcIds], PredId, PredInfo, ModuleInfo,
+        !ProcTable) :-
+    ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+    proc_info_headvars(ProcInfo0, HeadVars),
+    PredModule = pred_info_module(PredInfo),
+    PredName   = pred_info_name(PredInfo),
+    PredArity  = pred_info_orig_arity(PredInfo),
+    make_size_var_map(HeadVars, _SizeVarset, SizeVarMap),
+    (
+        hlds_pred.no_type_info_builtin(PredModule, PredName, PredArity)
+    ->
+        Constrs = process_no_type_info_builtin(PredName, HeadVars,
+            SizeVarMap)
+    ;
+        all_args_input_or_zero_size(ModuleInfo, PredInfo, ProcInfo0)
+    ->
+            Constrs = []
+    ;
+        unexpected(this_file, "builtin with non-zero-size args.")
+    ),
+    Polyhedron = polyhedron.from_constraints(Constrs),
+    ArgSizeInfo = yes(Polyhedron),
+    HeadSizeVars = prog_vars_to_size_vars(SizeVarMap, HeadVars),
+    some [!TermInfo] (
+        proc_info_get_termination2_info(ProcInfo0, !:TermInfo),
+        !:TermInfo = !.TermInfo ^ success_constrs := ArgSizeInfo,
+        !:TermInfo = !.TermInfo ^ term_status := yes(cannot_loop(builtin)),
+        !:TermInfo = !.TermInfo ^ intermod_status := yes(not_mutually_recursive),
+        !:TermInfo = !.TermInfo ^ size_var_map := SizeVarMap,
+        !:TermInfo = !.TermInfo ^ head_vars := HeadSizeVars,
+        proc_info_set_termination2_info(!.TermInfo, ProcInfo0, ProcInfo)
+    ),
+    svmap.det_update(ProcId, ProcInfo, !ProcTable),
+    set_builtin_terminates(ProcIds, PredId, PredInfo, ModuleInfo,
+        !ProcTable).
+
+:- func process_no_type_info_builtin(string, prog_vars, size_var_map)
+    = constraints.
+
+process_no_type_info_builtin(PredName, HeadVars, SizeVarMap) = Constraints :-
+    (
+        HeadVars = [HVar1, HVar2],
+        (PredName  = "unsafe_type_cast" ; PredName = "unsafe_promise_unique")
+    ->
+        SizeVar1 = prog_var_to_size_var(SizeVarMap, HVar1),
+        SizeVar2 = prog_var_to_size_var(SizeVarMap, HVar2),
+        Constraints = [make_vars_eq_constraint(SizeVar1, SizeVar2)]
+    ;
+        unexpected(this_file,
+        "Unrecognised predicate passed to process_special_builtin.")
+    ).
+
+%----------------------------------------------------------------------------%
+
+:- pred initialise_size_var_maps(list(proc_id)::in,
+    proc_table::in, proc_table::out) is det.
+
+initialise_size_var_maps([], !ProcTable).
+initialise_size_var_maps([ProcId | ProcIds], !ProcTable) :-
+    ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+    proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+    proc_info_headvars(ProcInfo0, HeadVars),
+    make_size_var_map(HeadVars, _SizeVarset, SizeVarMap),
+    TermInfo = TermInfo0 ^ size_var_map := SizeVarMap,
+    proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+    svmap.det_update(ProcId, ProcInfo, !ProcTable),
+    initialise_size_var_maps(ProcIds, !ProcTable).
+
+%----------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "term_constr_initial.m".
+
+%----------------------------------------------------------------------------%
+:- end_module term_constr_initial.
+%----------------------------------------------------------------------------%
--------------------------------------------------------------------------
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