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

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


+%----------------------------------------------------------------------------%
Index: compiler/term_constr_pass2.m
===================================================================
RCS file: compiler/term_constr_pass2.m
diff -N compiler/term_constr_pass2.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_pass2.m	23 Mar 2005 23:35:19 -0000
@@ -0,0 +1,706 @@
+%-----------------------------------------------------------------------------%
+% 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_pass2.m
+% main author: juliensf
+%
+% This module analyses a SCC of the call-graph and tries to prove that
+% it terminates.
+%
+% XXX This version is just a place-holder.  It attempts a very simple
+% proof method which is essentially what the existing termination analyser
+% does.
+%
+%-----------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_pass2.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module transform_hlds.termination2.
+
+:- import_module io.
+:- import_module list.
+
+%-----------------------------------------------------------------------------%
+
+:- type pass2_options.
+
+:- func pass2_options_init(int) = pass2_options.
+
+:- pred prove_termination_in_scc(pass2_options::in, list(pred_proc_id)::in,
+	module_info::in, constr_termination_info::out, io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module check_hlds.mode_util.
+
+:- import_module hlds.hlds_pred.
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_out.
+
+:- import_module libs.globals.
+:- import_module libs.lp_rational.
+:- import_module libs.options.
+:- import_module libs.polyhedron.
+:- import_module libs.rat.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.prog_data.
+:- import_module parse_tree.mercury_to_mercury.
+
+:- import_module transform_hlds.term_constr_util.
+:- import_module transform_hlds.term_constr_errors.
+:- import_module transform_hlds.term_constr_data.
+
+:- import_module assoc_list.
+:- import_module bimap.
+:- import_module bool.
+:- import_module int.
+:- import_module map.
+:- import_module require.
+:- import_module set.
+:- import_module std_util.
+:- import_module string.
+:- import_module term.
+:- import_module varset.
+
+%-----------------------------------------------------------------------------%
+%
+% Handle pass 2 options.
+%
+
+:- type pass2_options
+	--->	pass2_options(
+			max_matrix_size :: int
+	).
+
+pass2_options_init(MaxSize) = pass2_options(MaxSize).
+
+%-----------------------------------------------------------------------------%
+
+:- type scc == list(abstract_ppid).
+
+	% Each edge in the call-graph represents a single call site.
+	%
+:- type edge
+	---> edge(
+		head :: abstract_ppid,
+			% The procedure that is making the call.
+
+		zeros :: set(size_var),
+			% Variables in the procedure known to have
+			% zero-size.
+
+		head_args :: size_vars,
+			% The size_vars that correspond to the
+			% variables in the head of the procedure.
+
+		label :: polyhedron,
+			% The constraints that occur between the
+			% head of the procedure and the call.
+
+		call :: abstract_ppid,
+			% The callee procedure.
+
+		call_args :: size_vars
+			% The size_vars that correspond to the
+			% variables in the procedure call.
+	).
+
+:- type edges == list(edge).
+
+:- type cycle
+	---> cycle(
+		nodes :: list(abstract_ppid),
+			% A list of every procedure involved in
+			% this cycle.
+
+		edges :: list(edge)
+			% A list of edges involved in this cycle.
+			% Note: It is not ordered.  This allows
+			% us to decide (later) on where we want
+			% the cycle to start.
+	).
+
+:- type cycles == list(cycle).
+
+	% A c_cycle is a collapsed cycle; where equalities have replaced
+	% calls between corresponding edges.
+
+%
+% A little clarification on this:  Each `c_cycles' field is list of
+% elementary cycles that start and end at `start'.
+%
+
+:- type cycle_set
+	---> c_set(
+		start    :: abstract_ppid,
+		c_cycles :: list(edge)
+	).
+
+%-----------------------------------------------------------------------------%
+
+prove_termination_in_scc(_, [], _, cannot_loop(analysis), !IO).
+prove_termination_in_scc(Options, SCC0 @ [_|_], ModuleInfo, Result, !IO) :-
+	AbstractSCC = get_abstract_scc(ModuleInfo, SCC0),
+	% XXX Pass 1 should really set this up.
+	SCC = list.map((func(A) = real(A)), SCC0),
+	( scc_contains_recursion(AbstractSCC) ->
+		Varset = varset_from_abstract_scc(AbstractSCC),
+		Edges  = label_edges_in_scc(AbstractSCC, ModuleInfo,
+			Options ^ max_matrix_size),
+		Cycles    = find_elementary_cycles_in_scc(SCC, Edges),
+		CycleSets = partition_cycles(SCC, Cycles),
+		prove_termination(CycleSets, AbstractSCC, Varset, Result)
+	;
+		Result = cannot_loop(analysis)
+	).
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates for labelling edges.
+%
+
+% Work out what the constraints are between each procedure head and each
+% call for every call in the SCC.  This information is implicit in the
+% AR, so we traverse the AR building up a list of labelled edges as
+% we go - this is similar to the fixpoint calculation we performed in pass 1
+% except that we can stop after we have examined the last call.  This often
+% means that we can avoid performing unnecessary convex hull operations.
+
+:- func label_edges_in_scc(abstract_scc, module_info, int) = edges.
+
+label_edges_in_scc(Procs, ModuleInfo, MaxMatrixSize) = Edges :-
+	FindEdges = (pred(Proc::in, !.Edges::in, !:Edges::out) is det :-
+		find_edges_in_goal(Proc, Procs, ModuleInfo, MaxMatrixSize,
+			Proc ^ body, 1, _, polyhedron.identity, _, [],
+			ProcEdges, yes, _),
+		list.append(ProcEdges, !Edges)
+	),
+	list.foldl(FindEdges, Procs, [], Edges).
+
+	% The four accumulators here are for:
+	% (1) the number of calls seen so far
+	% (2) the constraints so far
+	% (3) the edges found
+	% (4) whether to abort or continue looking
+	%
+:- pred find_edges_in_goal(abstract_proc::in, abstract_scc::in,
+	module_info::in, int::in, abstract_goal::in, int::in, int::out,
+	polyhedron::in, polyhedron::out, edges::in, edges::out, bool::in,
+	bool::out) is det.
+
+find_edges_in_goal(Proc, AbstractSCC, ModuleInfo, MaxMatrixSize,
+		AbstractGoal, !Calls, !Polyhedron, !Edges, !Continue) :-
+	AbstractGoal = disj(Goals, _, Locals, _),
+	(
+		!.Continue = yes,
+		%
+		% XXX We may be able to prove termination in more cases
+		% if we pass in !.Polyhedron instead of
+		% of polyhedron.identity ... although I don't think
+		% it is a major concern at the moment.
+		%
+		find_edges_in_disj(Proc, AbstractSCC, ModuleInfo,
+			MaxMatrixSize, polyhedron.identity, Goals, !Calls,
+			[], DisjConstrs0, [], Edges1, !Continue),
+		Edges2 = list.map(fix_edges(!.Polyhedron), Edges1),
+		list.append(Edges2, !Edges),
+		(
+			!.Continue = yes,
+			Varset = Proc ^ varset,
+			DisjConstrs = polyhedron.project_all(Varset, Locals,
+				DisjConstrs0),
+			Constrs2 = list.foldl(
+				polyhedron.convex_union(Varset,
+					yes(MaxMatrixSize)), DisjConstrs,
+					polyhedron.empty),
+			polyhedron.intersection(Constrs2, !Polyhedron)
+		;
+			!.Continue = no
+		)
+	;
+		!.Continue = no
+	).
+
+find_edges_in_goal(Proc, AbstractSCC, ModuleInfo, MaxMatrixSize,
+		AbstractGoal, !Calls, !Polyhedron, !Edges, !Continue) :-
+	AbstractGoal = conj(Goals, Locals, _),
+	(
+		!.Continue = yes,
+		list.foldl4(find_edges_in_goal(Proc, AbstractSCC, ModuleInfo,
+				MaxMatrixSize),
+			Goals, !Calls, !Polyhedron, !Edges, !Continue),
+		(
+			!.Continue = yes,
+          		polyhedron.project(Locals, Proc ^ varset, !Polyhedron)
+		;
+			!.Continue = no
+		)
+	;
+		!.Continue = no
+    	).
+
+find_edges_in_goal(Proc, _AbstractSCC, ModuleInfo, _,
+		call(CallPPId0, _, CallVars, ZeroVars, _, _, _),
+		!Calls, !Polyhedron, !Edges, !Continue) :-
+	%
+	% Having found a call we now need to construct a label for that
+	% edge and then continue looking for more edges.
+	%
+	Edge = edge(Proc ^ ppid, Proc ^ zeros, Proc ^ head_vars, !.Polyhedron,
+		CallPPId0, CallVars),
+	list.cons(Edge, !Edges),
+	%
+	% Update the call count and maybe stop processing if that was
+	% the last call.
+	%
+	!:Calls = !.Calls + 1,
+	( if 	!.Calls > Proc ^ calls
+	  then 	!:Continue = no
+	  else 	true
+	),
+
+	(
+		!.Continue = no
+	;
+		!.Continue = yes,
+		CallPPId0 = real(CallPPId),
+		module_info_pred_proc_info(ModuleInfo, CallPPId,  _,
+			CallProcInfo),
+		proc_info_get_termination2_info(CallProcInfo, CallTermInfo),
+		MaybeArgSizeInfo = CallTermInfo ^ success_constrs,
+		(
+			MaybeArgSizeInfo = no,
+	  		unexpected(this_file,
+				"Proc with no arg size info in pass 2.")
+		;
+			MaybeArgSizeInfo = yes(ArgSizePolyhedron0),
+			%
+			% If the polyhedron is universe then
+			% there's no point running the substitution.
+			%
+			( polyhedron.is_universe(ArgSizePolyhedron0) ->
+		  		true
+			;
+				MaybeCallProc = CallTermInfo ^ abstract_rep,
+				( if 	MaybeCallProc = yes(CallProc0)
+				  then	CallProc = CallProc0
+				  else	unexpected(this_file,
+					"No abstract representation for proc.")
+				),
+				HeadVars = CallProc ^ head_vars,
+				Subst = map.from_corresponding_lists(HeadVars,
+					CallVars),
+				Eqns0 = non_false_constraints(
+					ArgSizePolyhedron0),
+				Eqns1 = substitute_size_vars(Eqns0, Subst),
+				Eqns  = lp_rational.set_vars_to_zero(ZeroVars, Eqns1),
+				ArgSizePolyhedron = from_constraints(Eqns),
+				polyhedron.intersection(ArgSizePolyhedron,
+					!Polyhedron)
+			)
+		)
+	).
+
+find_edges_in_goal(_, _, _, _, AbstractGoal, !Calls, !Polyhedron, !Edges,
+		!Continue) :-
+	AbstractGoal = primitive(Primitive, _, _),
+	(
+		!.Continue = yes,
+		polyhedron.intersection(Primitive, !Polyhedron)
+	;
+		!.Continue = no
+	).
+
+:- pred find_edges_in_disj(abstract_proc::in, abstract_scc::in, module_info::in,
+	int::in, polyhedron::in, abstract_goals::in, int::in, int::out,
+	polyhedra::in, polyhedra::out, edges::in, edges::out, bool::in,
+	bool::out) is det.
+
+find_edges_in_disj(_, _, _, _, _, [], !Calls, !DisjConstrs, !Edges, !Continue).
+find_edges_in_disj(Proc, AbstractSCC, ModuleInfo, MaxMatrixSize, TopPoly,
+		[Disj | Disjs], !Calls, !DisjConstrs, !Edges, !Continue) :-
+	find_edges_in_goal(Proc, AbstractSCC, ModuleInfo, MaxMatrixSize, Disj,
+		!Calls, TopPoly, Constrs, !Edges, !Continue),
+	list.cons(Constrs, !DisjConstrs),
+	%
+	% This is why it is important that after numbering the
+	% calls in the AR we don't change anything around; otherwise
+	% this short-circuiting will not work correctly.
+	%
+	(
+		!.Continue = yes,
+		find_edges_in_disj(Proc, AbstractSCC, ModuleInfo,
+			MaxMatrixSize, TopPoly, Disjs, !Calls, !DisjConstrs,
+			!Edges, !Continue)
+	;
+		!.Continue = no
+	).
+
+:- func fix_edges(polyhedron, edge) = edge.
+
+fix_edges(Poly, Edge0) = Edge :-
+	Edge = Edge0 ^ label := polyhedron.intersection(Poly, Edge0 ^ label).
+
+%-----------------------------------------------------------------------------%
+%
+% Cycle detection.
+%
+
+% To find the elementary cycles of this SCC we perform a DFS of the call-graph.
+% Since the call-graph is technically a psuedograph (ie. it admits parallel
+% edges and self-loops), we first of all strip out any self-loops to make
+% things easier.
+
+:- func find_elementary_cycles_in_scc(list(abstract_ppid), edges) = cycles.
+
+find_elementary_cycles_in_scc(SCC, Edges0) = Cycles :-
+	%
+	% Get any self-loops for each procedure.
+	%
+	list.filter_map(direct_call, Edges0, Cycles0, Edges),
+	%
+	% Find larger elementary cycles in what is left.
+	%
+	Cycles1 = find_cycles(SCC, Edges),
+	Cycles = Cycles0 ++ Cycles1.
+
+	% Succeeds iff Edge is an edge that represents
+	% a directly recursive call (a self-loop in
+	% the psuedograph)
+	%
+:- pred direct_call(edge::in, cycle::out) is semidet.
+
+direct_call(Edge, Cycle) :-
+	Edge ^ head = Edge ^ call,
+	Cycle = cycle([Edge ^ head], [Edge]).
+
+:- func find_cycles(list(abstract_ppid), edges) = cycles.
+
+find_cycles(SCC, Edges) = Cycles :-
+	EdgeMap = partition_edges(SCC, Edges),
+	Cycles = search_for_cycles(SCC, EdgeMap).
+
+	% Builds a map from `pred_proc_id' to a list of the edges that begin
+	% with the `pred_proc_id.
+	%
+:- func partition_edges(list(abstract_ppid), edges) = map(abstract_ppid, edges).
+
+partition_edges([], _) = map.init.
+partition_edges([ProcId | SCC], Edges0) = Map :-
+	Map0 = partition_edges(SCC, Edges0),
+	Edges = list.filter((pred(Edge::in) is semidet :- ProcId = Edge ^ head), Edges0),
+	Map = map.det_insert(Map0, ProcId, Edges).
+
+:- func search_for_cycles(list(abstract_ppid), map(abstract_ppid, edges))
+	= cycles.
+
+search_for_cycles([], _) = [].
+search_for_cycles([Start | Rest], Map0) = Cycles :-
+	Cycles0 = search_for_cycles_2(Start, Map0),
+	Map = map.delete(Map0, Start),
+	Cycles1 = search_for_cycles(Rest, Map),
+	Cycles = Cycles0 ++ Cycles1.
+
+:- func search_for_cycles_2(abstract_ppid, map(abstract_ppid, edges)) = cycles.
+
+search_for_cycles_2(StartPPId, Map) = Cycles :-
+	InitialEdges = Map ^ det_elem(StartPPId),
+	list.foldl(search_for_cycles_3(StartPPId, [], Map, []), InitialEdges,
+		[], Cycles).
+
+:- pred search_for_cycles_3(abstract_ppid::in, edges::in,
+	map(abstract_ppid, edges)::in, list(abstract_ppid)::in, edge::in,
+	cycles::in, cycles::out) is det.
+
+search_for_cycles_3(Start, SoFar, Map, Visited, Edge, !Cycles) :-
+	( Start = Edge ^ call ->
+		Cycle = cycle([Edge ^ head | Visited], [Edge | SoFar]),
+		list.cons(Cycle, !Cycles)
+	;
+		( MoreEdges0 = Map ^ elem(Edge ^ call) ->
+			NotVisited = (pred(E::in) is semidet :-
+				not list.member(E ^ head, Visited)
+			),
+			MoreEdges = list.filter(NotVisited, MoreEdges0),
+			list.foldl(search_for_cycles_3(Start, [Edge | SoFar],
+				Map, [Edge ^ head | Visited]), MoreEdges,
+				!Cycles)
+		;
+			true
+		)
+	).
+
+%-----------------------------------------------------------------------------%
+%
+% Partitioning sets of cycles.
+%
+
+:- func partition_cycles(scc, cycles) = list(cycle_set).
+
+partition_cycles([], _) = [].
+partition_cycles([Proc | Procs], Cycles0) = CycleSets :-
+	list.filter(cycle_contains_proc(Proc), Cycles0, PCycles, Cycles1),
+	CycleSets0 = partition_cycles(Procs, Cycles1),
+	PEdges = list.map(collapse_cycle(Proc), PCycles),
+	( if	PEdges    = []
+	  then	CycleSets = CycleSets0
+	  else	CycleSets = [c_set(Proc, PEdges) | CycleSets0]
+	).
+
+:- func get_proc_from_abstract_scc(list(abstract_proc), abstract_ppid)
+	= abstract_proc.
+
+get_proc_from_abstract_scc([], _) = _ :-
+	unexpected(this_file, "Cannot find proc.").
+get_proc_from_abstract_scc([ Proc | Procs ], PPId) =
+	( Proc ^ ppid = PPId ->
+		Proc
+	;
+		get_proc_from_abstract_scc(Procs, PPId)
+	).
+
+%-----------------------------------------------------------------------------%
+%
+% Termination checking.
+%
+
+% This approach is very crude.  It just checks that the sum of all
+% the non-zero arguments is decreasing around all the elementary cycles.
+
+:- pred prove_termination(list(cycle_set)::in, abstract_scc::in, size_varset::in,
+	constr_termination_info::out) is det.
+
+prove_termination(Cycles, AbstractSCC, Varset, Result) :-
+	( total_sum_decrease(AbstractSCC, Varset, Cycles) ->
+		Result = cannot_loop(analysis)
+	;
+		% NOTE: the context here will never be used, in any
+		% case it's not clear what it should be.
+		Error = term.context_init - cond_not_satisfied,
+		Result = can_loop([Error])
+	).
+
+:- pred total_sum_decrease(abstract_scc::in, size_varset::in,
+	list(cycle_set)::in) is semidet.
+
+total_sum_decrease(_, _, []).
+total_sum_decrease(AbstractSCC, Varset, [c_set(Start, Loops) | Cycles]):-
+	total_sum_decrease_2(AbstractSCC, Varset, Start, Loops),
+	total_sum_decrease(AbstractSCC, Varset, Cycles).
+
+:- pred total_sum_decrease_2(abstract_scc::in, size_varset::in,
+	abstract_ppid::in, list(edge)::in) is semidet.
+
+total_sum_decrease_2(_, _, _, []).
+total_sum_decrease_2(AbstractSCC, Varset, PPId, Loops @ [_|_]) :-
+	all [Loop] list.member(Loop, Loops) =>
+		strict_decrease_around_loop(AbstractSCC, Varset, PPId, Loop).
+
+	% Succeeds iff there is strict decrease in the sum of *all*
+	% the arguments around the given loop.
+	%
+:- pred strict_decrease_around_loop(abstract_scc::in, size_varset::in,
+	abstract_ppid::in, edge::in) is semidet.
+
+strict_decrease_around_loop(AbstractSCC, Varset, PPId, Loop) :-
+	( if 	(PPId \= Loop ^ head ; PPId \= Loop ^ call)
+	  then	unexpected(this_file, "Badly formed loop.")
+	  else	true
+	),
+	IsActive = (func(Var::in, Input::in) = (Var::out) is semidet :-
+		Input = yes
+	),
+	Proc = get_proc_from_abstract_scc(AbstractSCC, PPId),
+	Inputs = Proc ^ inputs,
+	HeadArgs = list.filter_map_corresponding(IsActive, Loop ^ head_args,
+		Inputs),
+	CallArgs = list.filter_map_corresponding(IsActive, Loop ^ call_args,
+		Inputs),
+	Terms = make_coeffs(HeadArgs, -one) ++ make_coeffs(CallArgs, one),
+	%
+	% NOTE: if you examine the condition it may contain less
+	% variables than you expect.  This is because if the same
+	% argument occurs in the head and the call they will cancel
+	% each other out.
+	%
+	Condition = constraint(Terms, (=<), -one),
+	Label = polyhedron.non_false_constraints(Loop ^ label),
+	entailed(Varset, Label, Condition).
+
+:- pred cycle_contains_proc(abstract_ppid::in, cycle::in) is semidet.
+
+cycle_contains_proc(PPId, cycle(Nodes, _)) :- list.member(PPId, Nodes).
+
+	% XXX Fix this name.
+:- func make_coeffs(size_vars, rat) = lp_terms.
+
+make_coeffs(Vars, Coeff) = list.map((func(Var) = Var - Coeff), Vars).
+
+%-----------------------------------------------------------------------------%
+
+	% Collapse all the cycles so that they all start with the given
+	% procedure and all the edge labels between are conjoined.
+	%
+:- func collapse_cycles(abstract_ppid, cycles) = edges.
+
+collapse_cycles(Start, Cycles) = list.map(collapse_cycle(Start), Cycles).
+
+:- func collapse_cycle(abstract_ppid, cycle) = edge.
+
+collapse_cycle(_, cycle(_, [])) = _ :-
+	unexpected(this_file, "Trying to collapse a cycle with no edges.").
+collapse_cycle(_, cycle(_, [Edge])) = Edge.
+collapse_cycle(StartPPId, cycle(_, Edges0 @ [_,_|_])) = CollapsedCycle :-
+	order_nodes(StartPPId, Edges0, Edges),
+	( if 	Edges = [StartEdge0 | Rest0]
+	  then	StartEdge = StartEdge0, Rest = Rest0
+	  else	unexpected(this_file, "Error while collapsing cycles.")
+	),
+	StartEdge = edge(_, Zeros0, HeadVars, Polyhedron0, _, CallVars0),
+	collapse_cycle_2(Rest, Zeros0, Zeros, CallVars0, CallVars, Polyhedron0,
+		Polyhedron),
+	CollapsedCycle = edge(StartPPId, Zeros, HeadVars, Polyhedron,
+		StartPPId, CallVars).
+
+:- pred collapse_cycle_2(edges::in, zero_vars::in, zero_vars::out,
+	size_vars::in, size_vars::out, polyhedron::in, polyhedron::out) is det.
+
+collapse_cycle_2([], !Zeros, !CallVars, !Polyhedron).
+collapse_cycle_2([Edge | Edges], !Zeros, !CallVars, !Polyhedron) :-
+	set.union(Edge ^ zeros, !Zeros),
+	HeadVars = Edge ^ head_args,
+	Subst0 = assoc_list.from_corresponding_lists(HeadVars, !.CallVars),
+	bimap.set_from_assoc_list(Subst0, bimap.init, Subst),
+	%
+	% We now need to substitute variables from the call to *this*
+	% predicate for head variables in both the constraints from the
+	% body of the predicate and also into the variables in the
+	% calls to the next predicate.
+	%
+	% While it might be easier to put equality constraints
+	% between the caller's arguments and the callee's head
+	% arguments the substitution is in some ways more desirable
+	% as we can detect some neutral arguments more directly.
+	%
+	!:CallVars = list.map(subst_size_var(Subst), Edge ^ call_args),
+	%
+	% These should be non-false, so throw an exception if they
+	% are not.
+	%
+	Constraints0 = polyhedron.non_false_constraints(!.Polyhedron),
+	Constraints1 = polyhedron.non_false_constraints(Edge ^ label),
+	Constraints2 = list.map(subst_size_var_eqn(Subst), Constraints1),
+	Constraints3 = Constraints0 ++ Constraints2,
+	!:Polyhedron = polyhedron.from_constraints(Constraints3),
+	collapse_cycle_2(Edges, !Zeros, !CallVars, !Polyhedron).
+
+:- pred order_nodes(abstract_ppid::in, edges::in, edges::out) is det.
+
+order_nodes(StartPPId, Edges0, [Edge | Edges]) :-
+	EdgeMap = build_edge_map(Edges0),
+	Edge = EdgeMap ^ det_elem(StartPPId),
+	order_nodes_2(StartPPId, Edge ^ call, EdgeMap, Edges).
+
+:- pred order_nodes_2(abstract_ppid::in, abstract_ppid::in,
+	map(abstract_ppid, edge)::in, edges::out) is det.
+
+order_nodes_2(StartPPId, CurrPPId, Map, Edges) :-
+	( if 	StartPPId = CurrPPId
+	  then 	Edges = []
+	  else
+		    Edge = Map ^ det_elem(CurrPPId),
+	    	order_nodes_2(StartPPId, Edge ^ call, Map, Edges0),
+	    	Edges = [Edge | Edges0]
+	).
+
+:- func build_edge_map(edges) = map(abstract_ppid, edge).
+
+build_edge_map([]) = map.init.
+build_edge_map([Edge | Edges]) =
+	map.det_insert(build_edge_map(Edges), Edge ^ head, Edge).
+
+:- func subst_size_var_eqn(bimap(size_var, size_var), constraint) =  constraint.
+
+subst_size_var_eqn(Map, Eqn0) = Eqn :-
+	constraint(Eqn0, Coeffs0, Operator, Constant),
+	Coeffs = list.map(subst_size_var_coeff(Map), Coeffs0),
+	Eqn = constraint(Coeffs, Operator, Constant).
+
+:- func subst_size_var_coeff(bimap(size_var, size_var), lp_term) = lp_term.
+
+subst_size_var_coeff(Map, Var0 - Coeff) = Var - Coeff :-
+	Var = subst_size_var(Map, Var0).
+
+:- func subst_size_var(bimap(size_var, size_var), size_var) = size_var.
+
+subst_size_var(Map, Old) = (if bimap.search(Map, Old, New) then New else Old).
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates for printing out debugging traces.
+%
+
+:- pred write_cycles(cycles::in, module_info::in, size_varset::in,
+	io::di, io::uo) is det.
+
+write_cycles([], _, _, !IO).
+write_cycles([Cycle | Cycles], ModuleInfo, Varset, !IO) :-
+	io.write_string("Cycle in SCC:\n", !IO),
+	write_cycle(Cycle ^ nodes, ModuleInfo, !IO),
+	io.write_list(Cycle ^ edges, "\n", write_edge(ModuleInfo, Varset), !IO),
+	io.nl(!IO),
+	write_cycles(Cycles, ModuleInfo, Varset, !IO).
+
+:- pred write_cycle(list(abstract_ppid)::in, module_info::in, io::di, io::uo)
+	is det.
+
+write_cycle([], _, !IO).
+write_cycle([ Proc | Procs ], ModuleInfo, !IO) :-
+	io.write_string("\t- ", !IO),
+	Proc = real(proc(PredId, ProcId)),
+	hlds_out.write_pred_proc_id(ModuleInfo, PredId, ProcId, !IO),
+	io.nl(!IO),
+	write_cycle(Procs, ModuleInfo, !IO).
+
+:- pred write_edge(module_info::in, size_varset::in, edge::in,
+	io::di, io::uo) is det.
+
+write_edge(ModuleInfo, Varset, Edge, !IO) :-
+	io.write_string("Edge is:\n\tHead: ", !IO),
+	Edge ^ head = real(proc(PredId, ProcId)),
+	hlds_out.write_pred_proc_id(ModuleInfo, PredId, ProcId, !IO),
+	io.write_string(" : ", !IO),
+	write_size_vars(Varset, Edge ^ head_args, !IO),
+	io.write_string(" :- \n", !IO),
+	io.write_string("\tConstraints are:  \n", !IO),
+	write_polyhedron(Edge ^ label, Varset, !IO),
+	io.write_string("\n\tCall is:  ", !IO),
+	Edge ^ call = real(proc(CallPredId, CallProcId)),
+	hlds_out.write_pred_proc_id(ModuleInfo, CallPredId, CallProcId, !IO),
+	io.write_string(" : ", !IO),
+	write_size_vars(Varset, Edge ^ call_args, !IO),
+	io.write_string(" :- \n", !IO),
+	io.nl(!IO).
+
+%-----------------------------------------------------------------------------%
+
+:- func this_file = string.
+this_file = "term_constr_pass2.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module transform_hlds.term_constr_pass2.
+%-----------------------------------------------------------------------------%
Index: compiler/term_constr_util.m
===================================================================
RCS file: compiler/term_constr_util.m
diff -N compiler/term_constr_util.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ compiler/term_constr_util.m	23 Mar 2005 23:37:14 -0000
@@ -0,0 +1,532 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%------------------------------------------------------------------------------%
+% Copyright (C) 1997-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_util.m
+% Main author: juliensf
+%
+% This module defines some utility predicates used by the termination analyser.
+%
+%------------------------------------------------------------------------------%
+
+:- module transform_hlds.term_constr_util.
+
+:- interface.
+
+:- import_module hlds.hlds_pred.
+:- import_module hlds.hlds_module.
+
+:- import_module libs.lp_rational.
+:- import_module libs.polyhedron.
+
+:- import_module parse_tree.prog_data.
+
+:- import_module transform_hlds.termination2.
+:- import_module transform_hlds.term_constr_data.
+
+:- import_module bool.
+:- import_module io.
+:- import_module list.
+:- import_module map.
+:- import_module std_util.
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for storing things in the HLDS.
+%
+
+	% This predicate sets the argument size info (in terms of constraints
+	% on inter-argument size relationships) of a given list of procedures.
+	%
+:- pred set_pred_proc_ids_constr_arg_size_info(list(pred_proc_id)::in,
+	constr_arg_size_info::in, module_info::in, module_info::out) is det.
+
+:- func lookup_proc_constr_arg_size_info(module_info, pred_proc_id) =
+	maybe(constr_arg_size_info).
+
+	% Retrieve the abstraction representation from the module_info.
+	%
+:- func get_abstract_scc(module_info, list(pred_proc_id)) = abstract_scc.
+
+:- func get_abstract_proc(module_info, pred_proc_id) = abstract_proc.
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for size_vars.
+%
+
+	% Given a list of prog_vars, allocate one size_var per prog_var.
+	% Return the varset from which the size_vars were allocated and
+	% a map between prog_vars and size_vars.
+	%
+:- pred make_size_var_map(list(prog_var)::in, size_varset::out,
+	size_var_map::out) is det.
+
+	% Give a list of prog_vars, allocate one size_var per prog_var.
+	% Allocate the size_vars from the provided size_varset.  Return
+	% a map between prog_vars and size_vars.
+	%
+:- pred make_size_var_map(list(prog_var)::in,
+	size_varset::in, size_varset::out, size_var_map::out) is det.
+
+	% Takes a list of prog_vars and outputs the corresponding
+	% list of size_vars, based on the given map.
+	%
+:- func prog_vars_to_size_vars(size_var_map, prog_vars) = size_vars.
+:- func prog_var_to_size_var(size_var_map, prog_var) = size_var.
+
+	% Returns a set containing all the size_vars corresponding to prog_vars
+	% that have a type that is always of zero size. i.e. all those for which
+	% the functor norm returns zero for all values of the type.
+	%
+:- func find_zero_size_vars(module_info, size_var_map, vartypes) = zero_vars.
+
+:- func derive_nonneg_eqns(size_var_map, zero_vars) = constraints.
+
+:- type var_substitution == map(size_var, size_var).
+
+	% compose_bijections:
+	% Takes two lists of vars of equal length, each list
+	% with a corresponding map from the vars in the list to size_vars.
+	% There is an implicit bijection between the two lists
+	% (based on the order of the lists).
+	% This predicate composes all three maps to produce a map
+	% from sizevar to sizevar (keys are the elements of the first list,
+	% values the values in the first map).
+	%
+:- func compose_bijections(size_vars, size_vars) = var_substitution.
+
+	% Create a non-negativity constraint for each size_var in the list,
+	% *except* if it has zero-size type.
+	%
+:- func make_arg_constraints(size_vars, zero_vars) = constraints.
+
+    % Check that a size_var is a member of the set of zero size_vars.
+    % XXX Ideally we would just use set.member directly but the arguments
+    % of that procedure are around the wrong way for use in most higher
+    % order procedures.
+    %
+:- pred is_zero_size_var(zero_vars::in, size_var::in) is semidet.
+
+%-----------------------------------------------------------------------------%
+
+:- pred add_context_to_constr_termination_info(
+	maybe(pragma_termination_info)::in, prog_context::in,
+	maybe(constr_termination_info)::out) is det.
+
+%------------------------------------------------------------------------------%
+
+	% substitute_size_vars: Takes a list of constraints and a
+	% var_substitution.  Returns the constraints with the specified
+	% substitutions made.
+	%
+:- func substitute_size_vars(constraints, map(size_var, size_var))
+	= constraints.
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for printing out debugging traces.
+%
+% In order to use these the option `--debug-term' must be set.
+
+	% Call the specified predicate.
+	%
+:- pred maybe_write_trace(pred(io, io), io, io).
+:- mode maybe_write_trace(pred(di, uo) is det, di, uo) is det.
+
+	% As above but if the boolean argument is `yes', print a newline
+	% to stdout before flushing the output.
+	%
+:- pred maybe_write_trace(pred(io, io), bool, io, io).
+:- mode maybe_write_trace(pred(di, uo) is det, in, di, uo) is det.
+
+	% Write the given string to stdout.
+	%
+:- pred maybe_write_string(string::in, io::di, io::uo) is det.
+
+	% Write a newline to stdout.
+	%
+:- pred maybe_write_nl(io::di, io::uo) is det.
+
+:- pred maybe_write_scc_procs(list(pred_proc_id)::in, module_info::in,
+	int::in, io::di, io::uo) is det.
+
+:- pred maybe_write_proc_name(pred_proc_id::in, string::in, module_info::in,
+	int::in, io::di, io::uo) is det.
+
+:- pred write_size_vars(size_varset::in, size_vars::in, io::di, io::uo) is det.
+
+:- pred dump_size_varset(size_varset::in, io::di, io::uo) is det.
+
+:- pred dump_size_vars(size_vars::in, size_varset::in, io::di, io::uo) is det.
+
+%------------------------------------------------------------------------------%
+
+:- pred update_arg_size_info(pred_proc_id::in, polyhedron::in, module_info::in,
+	module_info::out) is det.
+
+	% If Override is yes, then this predicate overrides any existing
+	% termination information. If Override is no, then it leaves the
+	% proc_info of a procedure unchanged unless the proc_info had no
+	% termination information (i.e. the maybe(termination_info)
+	% field was set to "no").
+	%
+:- pred change_procs_constr_termination_info(list(proc_id)::in, bool::in,
+	constr_termination_info::in, proc_table::in, proc_table::out) is det.
+
+	% This predicate sets the arg_size_info property of the given
+	% list of procedures.  If Override is yes, then this predicate
+	% overrides any existing arg_size information. If Override is
+	% no, then it leaves the proc_info of a procedure unchanged
+	% unless the proc_info had no arg_size information (i.e. the
+	% maybe(arg_size_info) field was set to "no").
+	%
+:- pred change_procs_constr_arg_size_info(list(proc_id)::in, bool::in,
+	constr_arg_size_info::in, proc_table::in, proc_table::out) is det.
+
+:- pred all_args_input_or_zero_size(module_info::in, pred_info::in,
+	proc_info::in) is semidet.
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module check_hlds.type_util.
+:- import_module check_hlds.mode_util.
+
+:- import_module libs.options.
+:- import_module libs.globals.
+:- import_module libs.rat.
+
+:- import_module hlds.hlds_goal.
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_out.
+:- import_module hlds.hlds_pred.
+:- import_module hlds.quantification.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.mercury_to_mercury.
+:- import_module parse_tree.prog_type.
+
+:- import_module transform_hlds.termination2.
+:- import_module transform_hlds.term_constr_errors.
+:- import_module transform_hlds.term_norm.
+
+:- import_module int.
+:- import_module set.
+:- import_module string.
+:- import_module svmap.
+:- import_module svvarset.
+:- import_module term.
+:- import_module varset.
+
+%------------------------------------------------------------------------------%
+
+set_pred_proc_ids_constr_arg_size_info([], _ArgSize, !ModuleInfo).
+set_pred_proc_ids_constr_arg_size_info([PPId | PPIds], ArgSize, !ModuleInfo) :-
+	PPId = proc(PredId, ProcId),
+	module_info_preds(!.ModuleInfo, PredTable0),
+	PredInfo0 = PredTable0 ^ det_elem(PredId),
+	pred_info_procedures(PredInfo0, ProcTable0),
+	ProcInfo0 = ProcTable0 ^ det_elem(ProcId),
+	proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+	TermInfo = TermInfo0 ^ success_constrs := yes(ArgSize),
+	proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+	ProcTable = ProcTable0 ^ det_elem(ProcId) := ProcInfo,
+	pred_info_set_procedures(ProcTable, PredInfo0, PredInfo),
+	PredTable = PredTable0 ^ det_elem(PredId) := PredInfo,
+	module_info_set_preds(PredTable, !ModuleInfo),
+	set_pred_proc_ids_constr_arg_size_info(PPIds, ArgSize, !ModuleInfo).
+
+lookup_proc_constr_arg_size_info(ModuleInfo, PredProcId) = MaybeArgSizeInfo :-
+	PredProcId = proc(PredId, ProcId),
+	module_info_pred_proc_info(ModuleInfo, PredId, ProcId, _, ProcInfo),
+	proc_info_get_termination2_info(ProcInfo, TermInfo),
+	MaybeArgSizeInfo = TermInfo ^ success_constrs.
+
+%------------------------------------------------------------------------------%
+
+make_size_var_map(ProgVars, SizeVarset, SizeVarMap) :-
+	make_size_var_map(ProgVars, varset.init, SizeVarset, SizeVarMap).
+
+make_size_var_map(ProgVars, !SizeVarset, SizeVarMap) :-
+	list.foldl2(make_size_var_map_2, ProgVars,
+		map.init, SizeVarMap, !SizeVarset).
+
+:- pred make_size_var_map_2(prog_var::in, size_var_map::in, size_var_map::out,
+	size_varset::in, size_varset::out) is det.
+
+make_size_var_map_2(ProgVar, !SizeVarMap, !SizeVarset) :-
+	svvarset.new_var(SizeVar, !SizeVarset),
+	svmap.set(ProgVar, SizeVar, !SizeVarMap).
+
+prog_vars_to_size_vars(SizeVarMap, Vars)
+	= list.map(prog_var_to_size_var(SizeVarMap), Vars).
+
+prog_var_to_size_var(SizeVarMap, Var) = SizeVar :-
+	( if 	map.search(SizeVarMap, Var, SizeVar0)
+	  then	SizeVar = SizeVar0
+	  else	unexpected(this_file,
+		    "prog_var_to_size_var/2: prog_var not in size_var_map.")
+	).
+
+find_zero_size_vars(ModuleInfo, SizeVarMap, VarTypes) = Zeros :-
+	ProgVars = map.keys(SizeVarMap),
+	ZeroProgVars = list.filter(is_zero_size_prog_var(ModuleInfo, VarTypes),
+		ProgVars),
+    %
+    % Build zeros from corresponding size_vars.
+    %
+    ZerosList = prog_vars_to_size_vars(SizeVarMap, ZeroProgVars),
+	Zeros = set.from_list(ZerosList).
+
+:- pred is_zero_size_prog_var(module_info::in, vartypes::in,
+	prog_var::in) is semidet.
+
+is_zero_size_prog_var(ModuleInfo, VarTypes, Var) :-
+	Type = VarTypes ^ det_elem(Var),
+	(
+		term_norm.zero_size_type(Type, ModuleInfo)
+	;
+		% We don't include the io.state and store.store
+		% in the constraints - they won't tell us anything
+		% useful.
+		type_util.is_dummy_argument_type(Type)
+	;
+		prog_type.type_is_higher_order(Type, _, _, _, _)
+	).
+
+add_context_to_constr_termination_info(no, _, no).
+add_context_to_constr_termination_info(yes(cannot_loop(_)), _,
+		yes(cannot_loop(import_supplied))).
+add_context_to_constr_termination_info(yes(can_loop(_)), Context,
+		yes(can_loop([Context - imported_pred]))).
+
+%------------------------------------------------------------------------------%
+
+substitute_size_vars(Constraints0, SubstMap) = Constraints :-
+	SubVarInCoeff = (func(OldVar - Rat) = NewVar - Rat :-
+		NewVar = SubstMap ^ det_elem(OldVar)
+	),
+	SubVarInEqn = (func(Constr) = constraint(Coeffs, Op, Rat) :-
+		constraint(Constr, Coeffs0, Op, Rat),
+		Coeffs = list.map(SubVarInCoeff, Coeffs0)
+	),
+	Constraints = list.map(SubVarInEqn, Constraints0).
+
+%------------------------------------------------------------------------------%
+%
+% Utility procedures used by various parts of the IR analysis.
+%
+
+	% derive_nonneg_eqns(SizeVarMap, Zeros).
+	% Returns a list of constraints of the form "x >= 0" for every size_var
+	% x that is is in `SizeVarMap' and is not in the set `Zeros'.
+	%
+derive_nonneg_eqns(SizeVarMap, Zeros) = Eqns :-
+	derive_nonneg_eqns(SizeVarMap, Zeros, Eqns).
+
+:- pred derive_nonneg_eqns(size_var_map::in, zero_vars::in,
+	constraints::out) is det.
+
+derive_nonneg_eqns(SizeVarMap, Zeros, NonNegs) :-
+	SizeVars = map.values(SizeVarMap),
+    list.filter(isnt(is_zero_size_var(Zeros)), SizeVars, NonZeroSizeVars),
+	NonNegs = list.map(make_nonneg_constr, NonZeroSizeVars).
+
+compose_bijections(Args, HeadVars) = SubstMap :-
+	compose_bijections(Args, HeadVars, map.init, SubstMap).
+
+:- pred compose_bijections(size_vars::in, size_vars::in,
+	var_substitution::in, var_substitution::out) is det.
+
+compose_bijections([], [], !Subst).
+compose_bijections([_|_], [], _, _) :-
+	unexpected(this_file, "compose_bijections/5: unmatched lists.").
+compose_bijections([], [_|_], _, _) :-
+	unexpected(this_file, "compose_bijections/5: unmatched lists.").
+compose_bijections([Arg | Args], [HeadVar | HeadVars],  !Subst) :-
+	svmap.det_insert(HeadVar, Arg, !Subst),
+	compose_bijections(Args, HeadVars, !Subst).
+
+make_arg_constraints([], _) = [].
+make_arg_constraints([Var | Vars], Zeros) = Constraints :-
+ 	Constraints0 = make_arg_constraints(Vars, Zeros),
+ 	( if 	set.member(Var, Zeros)
+   	  then	Constraints = Constraints0
+   	  else	Constraints =
+                [ constraint([Var - one], (>=), zero) | Constraints0 ]
+ 	).
+
+is_zero_size_var(Zeros, SizeVar) :- set.member(SizeVar, Zeros).
+
+%------------------------------------------------------------------------------%
+%
+% Predicates for printing out debugging traces ...
+%
+
+maybe_write_trace(TracePred, !IO) :-
+	maybe_write_trace(TracePred, no, !IO).
+
+maybe_write_trace(TracePred, NewLine, !IO) :-
+	globals.io_lookup_bool_option(debug_term, Trace, !IO),
+	(
+		Trace = yes,
+		TracePred(!IO),
+		( if NewLine = yes then	io.nl(!IO) else true ),
+		io.flush_output(!IO)
+	;
+		Trace = no
+	).
+
+maybe_write_nl(!IO) :- maybe_write_string("\n", !IO).
+
+maybe_write_string(String, !IO) :-
+	globals.io_lookup_bool_option(debug_term, Debug, !IO),
+	(
+		Debug = yes,
+		io.write_string(String, !IO),
+		io.flush_output(!IO)
+	;
+		Debug = no
+	).
+
+maybe_write_scc_procs(SCC, ModuleInfo, _, !IO) :-
+	write_scc_procs_2(SCC, ModuleInfo, !IO),
+	io.nl(!IO).
+
+:- pred write_scc_procs_2(list(pred_proc_id)::in, module_info::in,
+    io::di, io::uo) is det.
+
+write_scc_procs_2([], _, !IO).
+write_scc_procs_2([PPId | PPIds], ModuleInfo, !IO) :-
+	io.write_char('\t', !IO),
+	hlds_out.write_pred_proc_id(ModuleInfo, PPId, !IO),
+	io.nl(!IO),
+	write_scc_procs_2(PPIds, ModuleInfo, !IO).
+
+maybe_write_proc_name(PPId, String, ModuleInfo, _, !IO) :-
+	io.write_string(String, !IO),
+	hlds_out.write_pred_proc_id(ModuleInfo, PPId, !IO),
+	io.nl(!IO).
+
+write_size_vars(Varset, Vars, !IO) :-
+	WriteSizeVar = (pred(Var::in, !.IO::di, !:IO::uo) is det :-
+		varset.lookup_name(Varset, Var, Name),
+		io.write_string(Name, !IO)
+	),
+	io.write_char('[', !IO),
+	io.write_list(Vars, ", ", WriteSizeVar, !IO),
+	io.write_char(']', !IO).
+
+%------------------------------------------------------------------------------%
+
+dump_size_vars(Vars, Varset, !IO) :-
+	dump_size_varset_2(Vars, Varset, !IO).
+
+dump_size_varset(Varset, !IO) :-
+	Vars = varset.vars(Varset),
+	dump_size_varset_2(Vars, Varset, !IO).
+
+:- pred dump_size_varset_2(size_vars::in, size_varset::in, io::di, io::uo)
+	is det.
+
+dump_size_varset_2([], _, !IO).
+dump_size_varset_2([Var | Vars], Varset, !IO) :-
+	Name = varset.lookup_name(Varset, Var),
+	io.write(Var, !IO),
+	io.format(" = %s\n", [s(Name)], !IO),
+	dump_size_varset_2(Vars, Varset, !IO).
+
+%------------------------------------------------------------------------------%
+
+update_arg_size_info(PPID, Polyhedron, !ModuleInfo) :-
+	set_pred_proc_ids_constr_arg_size_info([PPID], Polyhedron,
+		!ModuleInfo).
+
+%------------------------------------------------------------------------------%
+
+change_procs_constr_termination_info([], _, _, !ProcTable).
+change_procs_constr_termination_info([ProcId | ProcIds], Override, Termination,
+		!ProcTable) :-
+	ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+	proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+	( (Override = yes ; TermInfo0 ^ term_status = no) ->
+		TermInfo = TermInfo0 ^ term_status := yes(Termination),
+		proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+		svmap.det_update(ProcId, ProcInfo, !ProcTable)
+	;
+		true
+	),
+	change_procs_constr_termination_info(ProcIds, Override, Termination,
+		!ProcTable).
+
+change_procs_constr_arg_size_info([], _, _, !ProcTable).
+change_procs_constr_arg_size_info([ProcId | ProcIds], Override, ArgSize,
+		!ProcTable) :-
+	ProcInfo0 = !.ProcTable ^ det_elem(ProcId),
+	proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+	( (Override = yes ; TermInfo0 ^ success_constrs = no) ->
+		TermInfo = TermInfo0 ^ success_constrs := yes(ArgSize),
+		proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+		svmap.det_update(ProcId, ProcInfo, !ProcTable)
+	;
+		true
+	),
+	change_procs_constr_arg_size_info(ProcIds, Override, ArgSize,
+		!ProcTable).
+
+all_args_input_or_zero_size(ModuleInfo, PredInfo, ProcInfo) :-
+	pred_info_arg_types(PredInfo, TypeList),
+	proc_info_argmodes(ProcInfo, ModeList),
+	all_args_input_or_zero_size_2(TypeList, ModeList, ModuleInfo).
+
+:- pred all_args_input_or_zero_size_2(list(type)::in, list(mode)::in,
+	module_info::in) is semidet.
+
+all_args_input_or_zero_size_2([], [], _).
+all_args_input_or_zero_size_2([], [_|_], _) :-
+	unexpected(this_file,
+		"all_args_input_or_zero_size_2/3: unmatched lists.").
+all_args_input_or_zero_size_2([_|_], [], _) :-
+	unexpected(this_file,
+		"all_args_input_or_zero_size_2/3: unmatched lists.").
+all_args_input_or_zero_size_2([Type | Types], [Mode | Modes], ModuleInfo) :-
+	( mode_util.mode_is_input(ModuleInfo, Mode) ->
+		all_args_input_or_zero_size_2(Types, Modes, ModuleInfo)
+	;
+		term_norm.zero_size_type(Type, ModuleInfo),
+		all_args_input_or_zero_size_2(Types, Modes, ModuleInfo)
+	).
+
+%----------------------------------------------------------------------------%
+
+get_abstract_scc(ModuleInfo, SCC) =
+	list.map(get_abstract_proc(ModuleInfo), SCC).
+
+get_abstract_proc(ModuleInfo, PPId) = AbstractProc :-
+	module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+	proc_info_get_termination2_info(ProcInfo, TermInfo),
+	MaybeAbstractProc = TermInfo ^ abstract_rep,
+	(
+		MaybeAbstractProc = yes(AbstractProc)
+	;
+		MaybeAbstractProc = no,
+		unexpected(this_file,
+			"get_abstract_proc/2: no abstract rep. for proc.")
+	).
+
+%------------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "term_constr_util.m".
+
+%------------------------------------------------------------------------------%
+:- end_module term_constr_util.
+%------------------------------------------------------------------------------%
Index: compiler/term_norm.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_norm.m,v
retrieving revision 1.7
diff -u -r1.7 term_norm.m
--- compiler/term_norm.m	22 Mar 2005 06:40:28 -0000	1.7
+++ compiler/term_norm.m	22 Mar 2005 22:04:36 -0000
@@ -25,27 +25,45 @@

 %-----------------------------------------------------------------------------%

-% The functor_info type contains information about how the weight of a term
-% is calculated.
-
+	% The functor_info type contains information about how the weight
+	% of a term is calculated.
+	%
 :- type functor_info.

-% This predicate sets the functor_info depending on the value of the
-% termination_norm option.
-
-:- pred set_functor_info(globals__termination_norm::in, module_info::in,
-	functor_info::out) is det.
-
-% This predicate computes the weight of a functor and the set of arguments
-% of that functor whose sizes should be counted towards the size of the whole
-% term.
-
+	% This predicate sets the functor_info depending on the value of the
+	% termination_norm or termination2_norm option.
+	%
+:- func set_functor_info(globals.termination_norm, module_info) = functor_info.
+
+	% This predicate computes the weight of a functor and the set of
+	% arguments of that functor whose sizes should be counted towards the
+	% size of the whole term.
+	%
+	% NOTE: the list of arguments and the list of modes must be the
+	% same length.  They must also *not* contain any type-info
+	% related arguments as this may cause an exception to be thrown
+	% when using the `--num-data-elems' norm.  (This is because the
+	% weight table doesn't keep track of type-info related variables
+	% - it used to but intervening compiler passes tend to do things
+	% to the code in the mean time so the whole lot becomes
+	% inconsistent - in the end it's just easier to ignore them).
+	%
 :- pred functor_norm(functor_info::in, type_ctor::in, cons_id::in,
 	module_info::in, int::out, list(prog_var)::in, list(prog_var)::out,
 	list(uni_mode)::in, list(uni_mode)::out) is det.

-% Succeeds if all values of the given type are zero size (for all norms).
-
+	% This function computes a lower bound on the weight of a fuctor.
+	% If the lower bound is zero then the weight of that functor is
+	% also zero.  If the lower bound is non-zero then there may be
+	% no upper bound on the size of the functor.  (And if there was
+	% this function wouldn't tell you about it anyhow).
+	%
+:- func functor_lower_bound(functor_info, type_ctor, cons_id, module_info)
+	= int.
+
+	% Succeeds if all values of the given type are zero size
+	% (for all norms).
+	%
 :- pred zero_size_type((type)::in, module_info::in) is semidet.

 %-----------------------------------------------------------------------------%
@@ -58,6 +76,7 @@
 :- import_module check_hlds__type_util.
 :- import_module hlds__hlds_data.
 :- import_module libs__options.
+:- import_module parse_tree__error_util.
 :- import_module parse_tree__prog_out.
 :- import_module parse_tree__prog_type.

@@ -66,6 +85,7 @@
 :- import_module map.
 :- import_module require.
 :- import_module std_util.
+:- import_module string.

 %-----------------------------------------------------------------------------%

@@ -226,11 +246,11 @@

 %-----------------------------------------------------------------------------%

-set_functor_info(total, _Module, total).
-set_functor_info(simple, _Module, simple).
-set_functor_info(num_data_elems, Module, use_map_and_args(WeightMap)) :-
+set_functor_info(total, _Module) = total.
+set_functor_info(simple, _Module) = simple.
+set_functor_info(num_data_elems, Module) = use_map_and_args(WeightMap) :-
 	find_weights(Module, WeightMap).
-set_functor_info(size_data_elems, Module, use_map(WeightMap)) :-
+set_functor_info(size_data_elems, Module) = use_map(WeightMap) :-
 	find_weights(Module, WeightMap).

 %-----------------------------------------------------------------------------%
@@ -268,14 +288,14 @@
 		->
 			true
 		;
-			error("Unmatched lists in functor_norm_filter_args.")
+			unexpected(this_file, "Unmatched lists in " ++
+				"functor_norm_filter_args.")
 		)
 	;
 		Int = 0
 	).

 % This predicate will fail if the length of the input lists are not matched.
-
 :- pred functor_norm_filter_args(list(bool)::in, list(prog_var)::in,
 	list(prog_var)::out, list(uni_mode)::in, list(uni_mode)::out)
 	is semidet.
@@ -290,8 +310,26 @@

 %-----------------------------------------------------------------------------%

+functor_lower_bound(simple, _, ConsId, _) =
+	( if ConsId = cons(_, Arity), Arity \= 0 then 1 else 0).
+functor_lower_bound(total, _, ConsId, _) =
+	( if ConsId = cons(_, Arity) then Arity else 0 ).
+functor_lower_bound(use_map(WeightMap), TypeCtor, ConsId, _) = Weight :-
+	( if	search_weight_table(WeightMap, TypeCtor, ConsId, WeightInfo)
+	  then	WeightInfo = weight(Weight, _)
+	  else	Weight = 0
+	).
+functor_lower_bound(use_map_and_args(WeightMap), TypeCtor, ConsId, _)
+		= Weight :-
+	( if	search_weight_table(WeightMap, TypeCtor, ConsId, WeightInfo)
+	  then	WeightInfo = weight(Weight, _)
+	  else	Weight = 0
+	).
+
+%-----------------------------------------------------------------------------%
+
 zero_size_type(Type, Module) :-
-	classify_type(Module, Type) = TypeCategory,
+	type_util.classify_type(Module, Type) = TypeCategory,
 	zero_size_type_category(TypeCategory, yes).

 :- pred zero_size_type_category(type_category::in, bool::out) is det.
@@ -312,5 +350,11 @@
 zero_size_type_category(user_ctor_type, no).

 %-----------------------------------------------------------------------------%
-:- end_module transform_hlds__term_norm.
+
+:- func this_file = string.
+
+this_file = "term_norm.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module term_norm.
 %-----------------------------------------------------------------------------%
Index: compiler/term_pass2.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_pass2.m,v
retrieving revision 1.18
diff -u -r1.18 term_pass2.m
--- compiler/term_pass2.m	22 Mar 2005 06:40:28 -0000	1.18
+++ compiler/term_pass2.m	22 Mar 2005 06:49:36 -0000
@@ -103,12 +103,12 @@
 			prove_termination_in_scc_single_arg(SCC,
 				Module, PassInfo)
 		->
-			Termination = cannot_loop
+			Termination = cannot_loop(unit)
 		;
 			Termination = Termination1
 		)
 	;
-		Termination1 = cannot_loop,
+		Termination1 = cannot_loop(unit),
 		Termination = Termination1
 	).

@@ -202,7 +202,7 @@
 		ArgNum0, Module, InitRecSuppliers),
 	prove_termination_in_scc_trial([TrialPPId | RestSCC], InitRecSuppliers,
 		up, Module, PassInfo, Termination),
-	( Termination = cannot_loop ->
+	( Termination = cannot_loop(unit) ->
 		true
 	;
 		ArgNum1 = ArgNum0 + 1,
@@ -306,7 +306,7 @@
 			list__take_upto(MaxErrors, Cycles, ReportedCycles),
 			Termination = can_loop(ReportedCycles)
 		;
-			Termination = cannot_loop
+			Termination = cannot_loop(unit)
 		)
 	;
 		Result = error(Errors),
Index: compiler/term_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_util.m,v
retrieving revision 1.40
diff -u -r1.40 term_util.m
--- compiler/term_util.m	24 Mar 2005 02:00:31 -0000	1.40
+++ compiler/term_util.m	24 Mar 2005 02:26:59 -0000
@@ -56,7 +56,7 @@
 	generic_arg_size_info(list(term_errors__error)).

 :- type termination_info ==
-	generic_termination_info(list(term_errors__error)).
+	generic_termination_info(unit, list(term_errors__error)).

 % The type `used_args' holds a mapping which specifies for each procedure
 % which of its arguments are used.
@@ -345,9 +345,10 @@
 %-----------------------------------------------------------------------------%

 add_context_to_termination_info(no, _, no).
-add_context_to_termination_info(yes(cannot_loop), _, yes(cannot_loop)).
+add_context_to_termination_info(yes(cannot_loop(_)), _,
+	yes(cannot_loop(unit))).
 add_context_to_termination_info(yes(can_loop(_)), Context,
-		yes(can_loop([Context - imported_pred]))).
+	yes(can_loop([Context - imported_pred]))).

 add_context_to_arg_size_info(no, _, no).
 add_context_to_arg_size_info(yes(finite(A, B)), _, yes(finite(A, B))).
Index: compiler/termination.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/termination.m,v
retrieving revision 1.50
diff -u -r1.50 termination.m
--- compiler/termination.m	22 Mar 2005 06:40:28 -0000	1.50
+++ compiler/termination.m	22 Mar 2005 06:49:36 -0000
@@ -114,7 +114,7 @@

 		% Find out what norm we should use, and set up for using it
 	globals__io_get_termination_norm(TermNorm, !IO),
-	set_functor_info(TermNorm, !.Module, FunctorInfo),
+	FunctorInfo = set_functor_info(TermNorm, !.Module),
 	globals__io_lookup_int_option(termination_error_limit, MaxErrors, !IO),
 	globals__io_lookup_int_option(termination_path_limit, MaxPaths, !IO),
 	PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths),
@@ -186,7 +186,8 @@
 			MaybeTermination = no,
 			( attributes_imply_termination(Attributes) ->
 				proc_info_set_maybe_termination_info(
-					yes(cannot_loop), ProcInfo0, ProcInfo)
+					yes(cannot_loop(unit)),
+					ProcInfo0, ProcInfo)
 			;
 				TermErr = Context - does_not_term_foreign(PPId),
 				proc_info_set_maybe_termination_info(
@@ -197,7 +198,7 @@
 			% If there was a `pragma terminates' declaration
 			% for this procedure then check that the foreign
 			% code attributes do not contradict this.
-			MaybeTermination = yes(cannot_loop),
+			MaybeTermination = yes(cannot_loop(_)),
 			( terminates(Attributes) = does_not_terminate ->
 				TermErr = Context - inconsistent_annotations,
 				proc_info_set_maybe_termination_info(
@@ -344,8 +345,8 @@
 		MaybeTerm = yes(PPIdStatus)
 	),
 	(
-		Status = cannot_loop,
-		PPIdStatus = cannot_loop
+		Status = cannot_loop(_),
+		PPIdStatus = cannot_loop(_)
 	;
 		Status = can_loop(_),
 		PPIdStatus = can_loop(_)
@@ -620,7 +621,7 @@
 	->
 		( check_marker(Markers, terminates) ->
 			change_procs_termination_info(ProcIds, yes,
-				cannot_loop, ProcTable0, ProcTable2)
+				cannot_loop(unit), ProcTable0, ProcTable2)
 		;
 			ProcTable2 = ProcTable0
 		)
@@ -644,7 +645,7 @@
 			)
 		->
 			change_procs_termination_info(ProcIds, yes,
-				cannot_loop, ProcTable0, ProcTable1)
+				cannot_loop(unit), ProcTable0, ProcTable1)
 		;
 			TerminationError = Context - imported_pred,
 			TerminationInfo = can_loop([TerminationError]),
@@ -742,15 +743,15 @@
 special_pred_id_to_termination(compare, HeadVars, ArgSize, Termination) :-
 	term_util__make_bool_list(HeadVars, [no, no, no], OutList),
 	ArgSize = finite(0, OutList),
-	Termination = cannot_loop.
+	Termination = cannot_loop(unit).
 special_pred_id_to_termination(unify, HeadVars, ArgSize, Termination) :-
 	term_util__make_bool_list(HeadVars, [yes, yes], OutList),
 	ArgSize = finite(0, OutList),
-	Termination = cannot_loop.
+	Termination = cannot_loop(unit).
 special_pred_id_to_termination(index, HeadVars, ArgSize, Termination) :-
 	term_util__make_bool_list(HeadVars, [no, no], OutList),
 	ArgSize = finite(0, OutList),
-	Termination = cannot_loop.
+	Termination = cannot_loop(unit).
 special_pred_id_to_termination(initialise, _, _, _) :-
 	unexpected(this_file, "special_pred_id_to_termination/4 " ++
 		"initialise predicate").
@@ -778,8 +779,8 @@
 		ArgSizeInfo = yes(infinite([Context - Error]))
 	),
 	proc_info_set_maybe_arg_size_info(ArgSizeInfo, ProcInfo0, ProcInfo1),
-	proc_info_set_maybe_termination_info(yes(cannot_loop), ProcInfo1,
-		ProcInfo),
+	proc_info_set_maybe_termination_info(yes(cannot_loop(unit)),
+		ProcInfo1, ProcInfo),
 	map__det_update(!.ProcTable, ProcId, ProcInfo, !:ProcTable),
 	set_builtin_terminates(ProcIds, PredId, PredInfo, Module, !ProcTable).

Index: compiler/termination2.m
===================================================================
RCS file: compiler/termination2.m
diff -N compiler/termination2.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ compiler/termination2.m	24 Mar 2005 04:17:13 -0000
@@ -0,0 +1,736 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%-----------------------------------------------------------------------------%
+% Copyright (C) 1997,2002-2005 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: termination2.m
+% main author: juliensf
+%
+% This module contains the top level of a termination analyser for Mercury.
+% It is responsible for setting up the relevant data structures and invoking
+% all the other passes.
+%
+% --------
+% Overview
+% --------
+%
+% The main data structures used by this analysis are defined in
+% term_constr_data.m.
+%
+% The analysis is carried out in three passes:
+%
+% * Pass 0 - Setup information for builtin predicates and process any
+%   information from user annotations like termination pragmas and
+%   foreign proc. attributes.  Also, set up information imported from
+%   `.opt' and `.trans_opt' files.  (See term_constr_initial.m.)
+%
+% Each of passes 1 and 2 are run consecutively on each SCC of the
+% program call-graph.  This is done in bottom-up order.
+%
+% * Pass 1 - Interargument size relationship (IR) analysis.
+%
+%   (a) Convert HLDS to the abstract representation (AR) defined
+%       in term_constr_data.m.  (See term_constr_build.m.)
+%
+%   (b) Perform fixpoint calculation to derive IR information.
+%       ( See term_constr_fixpoint.m.)
+%
+% * Pass 2 - Termination.
+%   Use the information from pass 1 to attempt to find a proof that the
+%   procedures in a SCC terminate.
+%   There is an example of such a proof finder in term_constr_pass2.m,
+%   although we will probably end up with several such modules, each
+%   of which tries a different approach.
+%
+% In addition there are some utility procedures in term_constr_util.m
+% and some predicates for handling error messages in term_constr_error.m.
+%
+% The machinery for handling convex constraints (polyhedra) is in:
+%
+%   * polyhedron.m
+%   * lp_rational.m
+%   * rat.m
+%
+% TODO:
+%   * add support for higher-order code and intermodule
+%     mutual recursion.
+%
+%   * add support for user-defined IR constraints for foreign
+%     code, :- pragma arg_size_relation(...) or something.
+%
+%   * experiment with different types of widening.
+%
+%   * experiment with different representation for the polyhedra.
+%
+%----------------------------------------------------------------------------%
+
+:- module transform_hlds.termination2.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
+
+:- import_module parse_tree.prog_data.
+
+:- import_module libs.polyhedron.
+
+:- import_module mdbcomp.prim_data.
+
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_constr_errors.
+
+:- import_module io.
+:- import_module list.
+:- import_module std_util.
+
+%----------------------------------------------------------------------------%
+%
+% Types that define termination information about procedures.
+%
+
+    % This type is the interargument size relationships between
+    % the arguments of a predicate.
+    %
+:- type constr_arg_size_info == polyhedron.
+
+    % Whether or not a procedure is terminating and some idea of why
+    % this is or is not the case.
+    %
+:- type constr_termination_info ==
+    generic_termination_info(term_reason, term2_errors).
+
+    % Why does the termination analyser think that a procedure is
+    % terminating?  This is useful for debugging purposes.
+    %
+:- type term_reason
+    --->    builtin             % procedure was a builtin.
+
+    ;       pragma_supplied     % procedure has pramga terminates decl.
+
+    ;       foreign_supplied    % procedure has foreign code attribute.
+
+    ;       import_supplied     % This procedure was imported and it's
+                                % termination info. was read in from a .opt
+                                % or .trans_opt file.
+
+    ;       analysis.           % Termination info. was derived via analysis.
+
+    % Whether a procedure may be involved in mutual recursion
+    % across module boundaries.
+    %
+    % XXX Termination analysis of mutual recursion across module boundaries
+    %     NYI.
+    %
+:- type intermod_status
+    --->    not_mutually_recursive
+    ;       may_be_mutually_recursive.
+
+%----------------------------------------------------------------------------%
+%
+% The `termination2_info' structure.
+%
+
+% All the information needed by the termination analysis is stored in
+% this structure.  There is one such structure attached to every
+% procedure in the module.
+
+:- type termination2_info.
+
+:- func term2_info_init = termination2_info.
+
+:- func termination2_info ^ size_var_map = size_var_map.
+:- func termination2_info ^ import_headvarids = maybe(list(int)).
+:- func termination2_info ^ import_success =
+    maybe(pragma_constr_arg_size_info).
+:- func termination2_info ^ import_failure =
+    maybe(pragma_constr_arg_size_info).
+:- func termination2_info ^ success_constrs = maybe(constr_arg_size_info).
+:- func termination2_info ^ failure_constrs = maybe(constr_arg_size_info).
+:- func termination2_info ^ term_status = maybe(constr_termination_info).
+:- func termination2_info ^ abstract_rep = maybe(abstract_proc).
+:- func termination2_info ^ intermod_status = maybe(intermod_status).
+:- func termination2_info ^ head_vars = list(size_var).
+
+:- func termination2_info ^ size_var_map := size_var_map = termination2_info.
+:- func termination2_info ^ import_headvarids := maybe(list(int)) =
+    termination2_info.
+:- func termination2_info ^ import_success :=
+    maybe(pragma_constr_arg_size_info) = termination2_info.
+:- func termination2_info ^ import_failure :=
+    maybe(pragma_constr_arg_size_info) = termination2_info.
+:- func termination2_info ^ success_constrs := maybe(constr_arg_size_info)
+    = termination2_info.
+:- func termination2_info ^ failure_constrs := maybe(constr_arg_size_info)
+    = termination2_info.
+:- func termination2_info ^ term_status := maybe(constr_termination_info)
+    = termination2_info.
+:- func termination2_info ^ intermod_status := maybe(intermod_status)
+    = termination2_info.
+:- func termination2_info ^ abstract_rep := maybe(abstract_proc)
+    = termination2_info.
+:- func termination2_info ^ head_vars := list(size_var)
+    = termination2_info.
+
+%----------------------------------------------------------------------------%
+%
+% Termination analysis.
+%
+
+    % Perform termination analysis on a module.
+    %
+:- pred termination2.pass(module_info::in, module_info::out, io::di, io::uo)
+    is det.
+
+:- pred termination2.output_maybe_constr_arg_size_info(
+    maybe(constr_arg_size_info)::in, io::di, io::uo) is det.
+
+:- pred termination2.output_maybe_termination2_info(
+    maybe(constr_termination_info)::in, io::di, io::uo) is det.
+
+    % Write out a termination2_info pragma for the predicate if:
+    %   - it is exported.
+    %   - it is not compiler generated.
+    %
+:- pred termination2.output_pred_termination2_info(module_info::in,
+    pred_id::in, io::di, io::uo) is det.
+
+    % This predicate outputs termination_info pragmas;
+    % such annotations can be part of .opt and .trans_opt files.
+    %
+:- pred termination2.output_pragma_termination2_info(pred_or_func::in,
+    sym_name::in, list(mode)::in, prog_context::in,
+    maybe(constr_arg_size_info)::in, maybe(constr_arg_size_info)::in,
+    maybe(constr_termination_info)::in, size_vars::in, 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.rat.
+
+:- 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.dependency_graph.
+:- import_module transform_hlds.term_constr_build.
+:- import_module transform_hlds.term_constr_data.
+:- import_module transform_hlds.term_constr_errors.
+:- import_module transform_hlds.term_constr_fixpoint.
+:- import_module transform_hlds.term_constr_initial.
+:- import_module transform_hlds.term_constr_pass2.
+:- import_module transform_hlds.term_constr_util.
+:- import_module transform_hlds.term_norm.
+
+:- import_module bool.
+:- import_module char.
+:- import_module int.
+:- import_module map.
+:- import_module set.
+:- import_module string.
+:- import_module term.
+:- import_module varset.
+
+%------------------------------------------------------------------------------%
+%
+% The termination2_info structure.
+%
+
+:- type termination2_info
+    --->    term2_info(
+            size_var_map :: size_var_map,
+                % Map between prog_vars and size_vars.
+                % Each procedure should have one of these.
+
+            head_vars :: list(size_var),
+                % These are the size variables that occur in argument
+                % size constraints.  For procedures that are imported
+                % via a `.opt' or `.trans_opt' file we set these during
+                % the initial pass, for procedures in the module we are
+                % analysing, pass 1 sets it.
+
+            import_headvarids :: maybe(list(int)),
+            import_success   :: maybe(pragma_constr_arg_size_info),
+            import_failure   :: maybe(pragma_constr_arg_size_info),
+                % Arg size info. imported from another module via a
+                % `.opt' or `.trans_opt' file.  The preprocessing pass
+                % needs to convert these to the proper form.  These
+                % particular fields are of no use after that.
+
+            success_constrs :: maybe(constr_arg_size_info),
+                % The interargument size relationships
+                % (expressed as convex constraints)
+                % obtained during pass 1.
+
+            failure_constrs :: maybe(constr_arg_size_info),
+                % Failure constraints for predicates that
+                % can fail (set by pass 1).
+
+            term_status :: maybe(constr_termination_info),
+                % The termination status of the procedure as determined
+                % by pass 2.
+
+            intermod_status :: maybe(intermod_status),
+                % Is this procedure (possibly) involved in mutual
+                % recursion across module boundaries. Set by pass 1.
+
+            abstract_rep :: maybe(abstract_proc)
+                % The abstract representation of this
+                % proc. Set by term_constr_build.m.
+        ).
+
+term2_info_init = term2_info(map.init, [], no, no, no, no, no, no, no, no).
+
+%----------------------------------------------------------------------------%
+%
+% Main pass.
+%
+
+% The analysis proceeds as follows:
+%
+% * Preprocess the module:
+%   - setup information from termination pragmas
+%   - setup information from foreign proc attributes
+%   - setup information about imported procedures
+%   - setup termination information for builtin predicates
+%
+% * Analyse the module - process SCCs bottom-up.
+%
+% * Optionally write out termination information to the `.opt' and
+%   `.trans_opt' files.
+%
+
+termination2.pass(!ModuleInfo, !IO) :-
+    %
+    % Get options required by the build pass.
+    % These are:
+    %   - which norm we are using.
+    %   - whether we are propagating failure constraints.
+    %
+    globals.io_get_termination2_norm(Norm, !IO),
+    FunctorInfo = term_norm.set_functor_info(Norm, !.ModuleInfo),
+    globals.io_lookup_bool_option(propagate_failure_constrs, Fail, !IO),
+    globals.io_lookup_bool_option(arg_size_analysis_only, ArgSizeOnly,
+        !IO),
+    BuildOptions = build_options_init(FunctorInfo, Fail, ArgSizeOnly),
+    %
+    % Get options required by the fixpoint pass.
+    % These are:
+    %   - what cutoff value we are using
+    %   - the maximum allowable matrix size
+    %     (this is also used in pass 2).
+    %
+    globals.io_lookup_int_option(term2_maximum_matrix_size, MaxSize, !IO),
+    globals.io_lookup_int_option(widening_limit, CutOff, !IO),
+    %
+    % NOTE: we may eventually allow other types of widening.
+    %
+    Widening = after_fixed_cutoff(CutOff),
+    FixpointOptions = fixpoint_options_init(Widening, MaxSize),
+    %
+    % Get options required by pass 2.
+    % Currently this is just the maximum matrix size.
+    %
+    Pass2Options = pass2_options_init(MaxSize),
+    %
+    % Setup termination information for builtins and compiler generated
+    % predicates.  Setup information from termination pragmas and
+    % foreign proc attributes.
+    %
+    term_constr_initial.preprocess_module(!ModuleInfo, !IO),
+    %
+    % Analyse the module per SCC in bottom-up fashion.
+    %
+    module_info_ensure_dependency_info(!ModuleInfo),
+    module_info_dependency_info(!.ModuleInfo, DepInfo),
+    hlds_dependency_info_get_dependency_ordering(DepInfo, SCCs),
+    list.foldl2(
+        analyse_scc(SCCs, BuildOptions, FixpointOptions, Pass2Options),
+        SCCs, !ModuleInfo, !IO),
+    %
+    % Write `.opt' and `.trans_opt' files.
+    %
+    maybe_make_optimization_interface(!.ModuleInfo, !IO).
+
+%----------------------------------------------------------------------------%
+%
+% Analyse a single SCC.
+%
+
+    % Analyse a single SCC of the call graph.  This will require results
+    % concerning SCCs lower down the call graph.
+    %
+    % The normal procedure for analysing a SCC is:
+    %
+    % (1) Build the abstract representation (AR) of the procedures in
+    %     the SCC. (term_constr_build.m).
+    %
+    % (2) Use a fixpoint iteration to derive interargument size
+    %     relationships for the procedures in the SCC.
+    %     (term_constr_fixpoint.m).
+    %
+    % (3) Use this information to try and find a proof that the procedures
+    %     in the SCC terminate.  (term_constr_pass2.m).
+    %
+    % Exactly which of the above steps gets carried out depends upon
+    % what (if any) additional information the user has supplied.
+    %
+    % For Mercury procedures:
+    % If the procedure is marked as terminating/non-terminating, we
+    % still carry out steps (1) and (2).  If a procedure has been
+    % supplied with an argument size constraint we carry out steps (1)
+    % and (3).  If both have been supplied we do not carry out any
+    % steps.
+    %
+    % The usual caveats regarding the termination pragmas and mutual
+    % recursion apply (see the reference manual).
+    %
+    % XXX What do we do about pragma arg_size_info and mutual recursion?
+    % (Nothing yet, because it isn't implemented :-( )
+    %
+    % For procedures implemented as foreign code:
+    % The usual defaults (see reference manual) apply.
+    % If no argument size constraint is supplied then non-zero arguments
+    % are assumed to have unbounded size.
+    %
+:- pred analyse_scc(dependency_ordering::in, build_options::in,
+    fixpoint_options::in, pass2_options::in,
+    list(pred_proc_id)::in, module_info::in, module_info::out, io::di,
+    io::uo) is det.
+
+analyse_scc(DepOrder, BuildOpts, FixpointOpts, Pass2Opts, SCC, !ModuleInfo,
+        !IO) :-
+    %
+    % Since all of the passes are potentially optional we need to
+    % initialise the size_var_maps separately.  If they are left
+    % uninitialised intermodule optimization will not work.
+    %
+    NeedsAR = list.filter(proc_needs_ar_built(!.ModuleInfo), SCC),
+    %
+    % Build the abstract representation for those procedures that
+    % require it. (those that do not already have both arg_size_info and
+    % termination info).
+    %
+    term_constr_build.build_abstract_scc(DepOrder, NeedsAR, BuildOpts,
+        BuildErrors, !ModuleInfo, !IO),
+    %
+    % We only perform the fixpoint computation for those procedures
+    % where we can gain meaningful information from it.  We do not
+    % do it when:
+    % - the information is already known.
+    % - the argument size relationships depend upon higher-order calls.
+    %
+    NeedsArgSize = list.filter(isnt(has_arg_size_info(!.ModuleInfo)),
+        NeedsAR),
+    term_constr_fixpoint.do_fixpoint_calculation(FixpointOpts,
+        NeedsArgSize, 1, FixpointErrors, !ModuleInfo, !IO),
+    %
+    % Errors detected during pass 1 always result in the rest of the
+    % analysis being aborted for the SCC under consideration.
+    %
+    Pass1Errors = BuildErrors ++ FixpointErrors,
+    Pass1Result = ( if Pass1Errors = [] then ok else error(Pass1Errors) ),
+    globals.io_lookup_bool_option(arg_size_analysis_only, ArgSizeOnly,
+        !IO),
+    (
+        ArgSizeOnly = no
+    ->
+        NeedsTerm = list.filter(isnt(has_term_info(!.ModuleInfo)),
+            NeedsAR),
+        %
+        % Some procedures may not have arg_size_info, but
+        % may have termination info, i.e. those that have
+        % a pragma terminates or does_not_terminate declaration.
+        %
+        ( Pass1Result = error(Pass1Errors) ->
+            Pass2Result = can_loop(Pass1Errors)
+        ;
+            term_constr_pass2.prove_termination_in_scc(Pass2Opts,
+                NeedsTerm, !.ModuleInfo, Pass2Result, !IO)
+        ),
+        %
+        % Set the termination property for this procedure and
+        % report any errors that we found during pass 2.
+        %
+        set_termination_info_for_procs(NeedsTerm, Pass2Result,
+            !ModuleInfo),
+        ( Pass2Result = can_loop(Errors) ->
+            report_termination2_errors(NeedsTerm, Errors,
+                !ModuleInfo, !IO)
+        ;
+            true
+        )
+    ;
+        true
+    ).
+
+%------------------------------------------------------------------------------%
+%
+% Procedures for storing termination2_info in the HLDS.
+%
+
+:- pred set_termination_info_for_procs(list(pred_proc_id)::in,
+    constr_termination_info::in, module_info::in, module_info::out) is det.
+
+set_termination_info_for_procs(PPIds, TerminationInfo, !ModuleInfo) :-
+    list.foldl(set_termination_info_for_proc(TerminationInfo), PPIds,
+        !ModuleInfo).
+
+:- pred set_termination_info_for_proc(constr_termination_info::in,
+    pred_proc_id::in, module_info::in, module_info::out) is det.
+
+set_termination_info_for_proc(TerminationInfo, PPId, !ModuleInfo) :-
+    module_info_pred_proc_info(!.ModuleInfo, PPId, PredInfo, ProcInfo0),
+    proc_info_get_termination2_info(ProcInfo0, TermInfo0),
+    TermInfo = TermInfo0 ^ term_status := yes(TerminationInfo),
+    proc_info_set_termination2_info(TermInfo, ProcInfo0, ProcInfo),
+    module_info_set_pred_proc_info(PPId, PredInfo, ProcInfo, !ModuleInfo).
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates for writing optimization interfaces.
+%
+
+:- pred maybe_make_optimization_interface(module_info::in, io::di, io::uo)
+    is det.
+
+maybe_make_optimization_interface(ModuleInfo, !IO) :-
+    globals.io_lookup_bool_option(make_optimization_interface, MakeOptInt,
+        !IO),
+    module_info_predids(ModuleInfo, PredIds),
+    ( if    MakeOptInt = yes
+      then  make_opt_int(PredIds, ModuleInfo, !IO)
+      else  true
+    ).
+
+:- pred make_opt_int(list(pred_id)::in, module_info::in, io::di, io::uo) is det.
+
+make_opt_int(_PredIds, _ModuleInfo, !IO).
+
+% XXX The code for writing .opt files is currently disabled.
+
+%   module_info_name(ModuleInfo, ModuleName),
+%   module_name_to_file_name(ModuleName, ".opt.tmp", no, OptFileName, !IO),
+%   globals.io_lookup_bool_option(verbose, Verbose, !IO),
+%   maybe_write_string(Verbose,
+%       "% Appending termination2_info pragmas to `", !IO),
+%   maybe_write_string(Verbose, OptFileName, !IO),
+%   maybe_write_string(Verbose, "'...", !IO),
+%   maybe_flush_output(Verbose, !IO),
+%   io.open_append(OptFileName, OptFileRes, !IO),
+%   (
+%       OptFileRes = ok(OptFile),
+%       io.set_output_stream(OptFile, OldStream, !IO),
+%         list.foldl(output_pred_termination2_info(ModuleInfo), PredIds,
+%           !IO),
+%       io.set_output_stream(OldStream, _, !IO),
+%       io.close_output(OptFile, !IO),
+%       maybe_write_string(Verbose, " done.\n", !IO)
+%   ;
+%       OptFileRes = error(IOError),
+%           % failed to open the .opt file for processing
+%       maybe_write_string(Verbose, " failed!\n", !IO),
+%       io.error_message(IOError, IOErrorMessage),
+%       io.write_strings(["Error opening file `",
+%           OptFileName, "' for output: ", IOErrorMessage], !IO),
+%       io.set_exit_status(1, !IO)
+%   ).
+
+output_pred_termination2_info(ModuleInfo, PredId, !IO) :-
+    %
+    % Don't try to output termination2_info pragmas unless
+    % the analysis was actually run.  Doing otherwise won't
+    % work because the necessary information will not have been set
+    % up.
+    %
+    globals.io_lookup_bool_option(termination2, RunningTerm2, !IO),
+    ( RunningTerm2 = yes ->
+        module_info_pred_info(ModuleInfo, PredId, PredInfo),
+        pred_info_import_status(PredInfo, ImportStatus),
+        module_info_type_spec_info(ModuleInfo, TypeSpecInfo),
+        TypeSpecInfo = type_spec_info(_, TypeSpecForcePreds, _, _),
+        (
+            (ImportStatus = exported
+            ;ImportStatus = opt_exported),
+            not hlds_pred.is_unify_or_compare_pred(PredInfo),
+            not set.member(PredId, TypeSpecForcePreds)
+        ->
+            PredName   = pred_info_name(PredInfo),
+            pred_info_procedures(PredInfo, ProcTable),
+            pred_info_context(PredInfo, Context),
+            PredOrFunc = pred_info_is_pred_or_func(PredInfo),
+            ModuleName = pred_info_module(PredInfo),
+            ProcIds    = pred_info_procids(PredInfo),
+            SymName    = qualified(ModuleName, PredName),
+            make_opt_int_procs(PredId, ProcIds, ProcTable, PredOrFunc,
+                SymName, Context, !IO)
+        ;
+            true
+        )
+    ;
+        true
+    ).
+
+:- pred make_opt_int_procs(pred_id::in, list(proc_id)::in,
+    proc_table::in, pred_or_func::in, sym_name::in, prog_context::in,
+    io::di, io::uo) is det.
+
+make_opt_int_procs(_PredId, [], _, _, _, _, !IO).
+make_opt_int_procs(PredId, [ ProcId | ProcIds ], ProcTable,
+        PredOrFunc, SymName, Context, !IO) :-
+    ProcInfo = ProcTable ^ det_elem(ProcId),
+    proc_info_get_termination2_info(ProcInfo, TermInfo),
+    proc_info_declared_argmodes(ProcInfo, ModeList),
+    proc_info_headvars(ProcInfo, HeadVars),
+    SizeVarMap = TermInfo ^ size_var_map,
+    HeadSizeVars = prog_vars_to_size_vars(SizeVarMap, HeadVars),
+    output_pragma_termination2_info(PredOrFunc, SymName,
+        ModeList, Context, TermInfo ^ success_constrs,
+        TermInfo ^ failure_constrs, TermInfo ^ term_status,
+        HeadSizeVars, !IO),
+    make_opt_int_procs(PredId, ProcIds, ProcTable,
+        PredOrFunc, SymName, Context, !IO).
+
+%----------------------------------------------------------------------------%
+%
+% Predicates for writing termination2_info pragmas.
+%
+
+% NOTE: if these predicates are changed then prog_io_pragma.m must
+%       also be changed so that it can parse the resulting pragma
+%       termination2_info declarations.
+
+output_pragma_termination2_info(PredOrFunc, SymName, ModeList,
+        Context, MaybeSuccess, MaybeFailure, MaybeTermination,
+        HeadVars, !IO) :-
+    io.write_string(":- pragma termination2_info(", !IO),
+    (
+        PredOrFunc = predicate,
+        mercury_output_pred_mode_subdecl(varset.init, SymName,
+            ModeList, no, Context, !IO)
+    ;
+        PredOrFunc = function,
+        pred_args_to_func_args(ModeList, FuncModeList, RetMode),
+        mercury_output_func_mode_subdecl(varset.init, SymName,
+            FuncModeList, RetMode, no, Context, !IO)
+    ),
+    io.write_string(", ", !IO),
+    output_headvars(HeadVars, !IO),
+    io.write_string(", ", !IO),
+    output_maybe_constr_arg_size_info(MaybeSuccess, !IO),
+    io.write_string(", ", !IO),
+    output_maybe_constr_arg_size_info(MaybeFailure, !IO),
+    io.write_string(", ", !IO),
+    output_maybe_termination2_info(MaybeTermination, !IO),
+    io.write_string(").\n", !IO).
+
+:- pred output_headvars(size_vars::in, io::di, io::uo) is det.
+
+output_headvars(Vars, !IO) :-
+    io.write_char('[', !IO),
+    io.write_list(Vars, ", ", output_headvar, !IO),
+    io.write_char(']', !IO).
+
+:- pred output_headvar(size_var::in, io::di, io::uo) is det.
+
+output_headvar(Var, !IO) :-
+    io.write_int(term.var_to_int(Var), !IO).
+
+output_maybe_constr_arg_size_info(MaybeArgSizeConstrs, !IO) :-
+    (
+        MaybeArgSizeConstrs = no,
+        io.write_string("not_set", !IO)
+    ;
+        MaybeArgSizeConstrs = yes(Polyhedron),
+        io.write_string("constraints(", !IO),
+        Constraints = polyhedron.non_false_constraints(Polyhedron),
+        OutputVar = (func(Var) =
+            int_to_string(term.var_to_int(Var))
+        ),
+        lp_rational.output_constraints(OutputVar, Constraints, !IO),
+        io.write_char(')', !IO)
+    ).
+
+output_maybe_termination2_info(MaybeConstrTermInfo, !IO) :-
+    (
+        MaybeConstrTermInfo = no,
+        io.write_string("not_set", !IO)
+    ;
+        MaybeConstrTermInfo = yes(cannot_loop(_)),
+        io.write_string("cannot_loop", !IO)
+    ;
+        MaybeConstrTermInfo = yes(can_loop(_)),
+        io.write_string("can_loop", !IO)
+    ).
+
+%----------------------------------------------------------------------------%
+%
+% Utility predicates.
+%
+
+% These test whether various fields in the termination2_info struct have
+% been set.
+
+    % Succeeds iff the given procedure has argument size constraints
+    % associated with it.
+    %
+:- pred has_arg_size_info(module_info::in, pred_proc_id::in) is semidet.
+
+has_arg_size_info(ModuleInfo, PPId) :-
+    module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+    proc_info_get_termination2_info(ProcInfo, TermInfo),
+    TermInfo ^ success_constrs = yes(_).
+
+    % Succeeds iff the termination status of a the given
+    % procedure has been set.
+    %
+:- pred has_term_info(module_info::in, pred_proc_id::in) is semidet.
+
+has_term_info(ModuleInfo, PPId) :-
+    module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+    proc_info_get_termination2_info(ProcInfo, TermInfo),
+    TermInfo ^ term_status = yes(_).
+
+:- pred proc_needs_ar_built(module_info::in, pred_proc_id::in) is semidet.
+
+proc_needs_ar_built(ModuleInfo, PPId) :-
+    module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
+    proc_info_get_termination2_info(ProcInfo, TermInfo),
+    (
+        TermInfo ^ success_constrs = no
+    ;
+        TermInfo ^ term_status = no
+    ).
+
+%------------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "termination2.m".
+
+%------------------------------------------------------------------------------%
+:- end_module termination2.
+%------------------------------------------------------------------------------%
Index: compiler/trans_opt.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/trans_opt.m,v
retrieving revision 1.27
diff -u -r1.27 trans_opt.m
--- compiler/trans_opt.m	22 Mar 2005 06:40:29 -0000	1.27
+++ compiler/trans_opt.m	22 Mar 2005 06:49:36 -0000
@@ -84,6 +84,7 @@
 :- import_module parse_tree__prog_out.
 :- import_module transform_hlds__intermod.
 :- import_module transform_hlds__termination.
+:- import_module transform_hlds__termination2.
 :- import_module transform_hlds__exception_analysis.

 :- import_module list.
@@ -132,13 +133,17 @@
 		module_info_predids(Module, PredIds),
 		list__foldl(termination__write_pred_termination_info(Module),
 			PredIds, !IO),
+% XXX Writing termination2_info pragma to .trans_opt files is currently
+% disabled.
+% 		list__foldl(termination2__output_pred_termination2_info(Module),
+% 			PredIds, !IO),

 		module_info_exception_info(Module, ExceptionInfo),
 		list__foldl(
 			exception_analysis__write_pragma_exceptions(Module,
 				ExceptionInfo),
 			PredIds, !IO),
-
+
 		io__set_output_stream(OldStream, _, !IO),
 		io__close_output(Stream, !IO),

Index: compiler/transform_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/transform_hlds.m,v
retrieving revision 1.16
diff -u -r1.16 transform_hlds.m
--- compiler/transform_hlds.m	6 Mar 2005 05:17:30 -0000	1.16
+++ compiler/transform_hlds.m	22 Mar 2005 06:44:45 -0000
@@ -40,8 +40,22 @@
    :- include_module term_util.
    :- include_module lp. % this could alternatively go in the `libs' module

-:- include_module post_term_analysis.
+:- include_module termination2.
+    	%
+		% The termination analyser.
+		%
+	:- include_module term_constr_initial.
+		% Pass 1.
+	:- include_module term_constr_build.
+	:- include_module term_constr_fixpoint.
+		% Pass 2.
+	:- include_module term_constr_pass2.
+		% Other bits.
+	:- include_module term_constr_util.
+	:- include_module term_constr_data.
+	:- include_module term_constr_errors.

+:- include_module post_term_analysis.
 :- include_module exception_analysis.

 % Optimizations (HLDS -> HLDS)

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