for review: changes to termination analysis and stack tracing [1/3]

[Zoltan Somogyi]

Estimated hours taken: 60

A rewrite of termination analysis to make it significantly easier to modify,
and to extend its capabilities.

compiler/error_util.m:
	A new file containing code that makes it easier to generate
	nicely formatted error messages.

compiler/termination.m:
	Updates to reflect the changes to the representation of termination
	information.

	Instead of doing pass 1 on all SCCs and then pass 2 on all SCCs,
	we now do both pass 1 and 2 on an SCC before moving on to the next.

	Do not insist that either all procedures in an SCC are
	compiler-generated or all are user-written, since this need not be
	true in the presence of user-defined equality predicates.

	Clarify the structure of the code that handles builtins and compiler
	generated predicates.

	Concentrate all the code for updating module_infos in this module.
	Previously it was scattered in several places in several files.

	Put all the code for writing out termination information at the
	end of the module in a logical order.

compiler/term_traversal.m:
	A new file containing code used by both pass 1 and pass 2 to
	traverse procedure bodies.

compiler/term_pass1.m:
	Use the new traversal module.

	Clarify the fixpoint computation on the set of output supplier
	arguments.

	Remove duplicates from the list of equations given to the solver.
	This avoids a det stack overflow in lp.m when doing termination
	analysis on options.m.

	If an output argument of a predicate makes sense only in the absence
	of errors, then return it only in the absence of errors.

compiler/term_pass2.m:
	Use the new traversal module. Unlike the previous code, this allows us
	to ignore recursive calls with input arguments bigger than the head
	if those calls occur after goals that cannot succeed (since those
	calls will never be reached).

	Implement a better way of doing single argument analysis, which
	(unlike the previous version) works in the presence of mutual recursion
	and other calls between the recursive call and the start of the clause.

	Implement a more precise way of checking for recursions that don't
	cause termination problems. We now allow calls from p to q in which
	the recursive input supplier arguments can grow, provided that on
	any path on which q can call p, directly or indirectly, the recursive
	input supplier arguments shrink by a greater amount.

	If an output argument of a predicate makes sense only in the absence
	of errors, then return it only in the absence of errors.

compiler/term_util.m:
	Updates to reflect the changes to the representation of termination
	information.

	Reorder to put related code together.

	Change the interface of several predicates to better reflect the
	way they are used.

	Add some more utility predicates.

compiler/term_errors.m:
	Small changes to the set of possible errors, and major changes in
	the way the messages are printed out (we now use error_util).

(The diff has the above files in their entirety, since they are smaller
and more meaningful than the diffs.)

compiler/options.m:
	Change --term-single-arg from being a bool to an int option,
	whose value indicates the maximum size of an SCC in which we try
	single argument analysis. (Large SCCs can cause single-arg analysis
	to require a lot of iterations.)

compiler/hlds_pred.m:
	Use two separate slots in the proc_info to hold argument size data
	and termination info, instead of the single slot used until now.
	The two kinds of information are produced and used separately.

	Make the layout of the get and set procedures for proc_infos more
	regular, to facilitate later updates.

	The procedures proc_info_{,set_}variables did the same work as
	proc_info_{,set_}varset. To eliminate potential confusion, I
	removed the first set.

compiler/*.m:
	Change proc_info_{,set_}variables to proc_info_{,set_}varset.

compiler/hlds_out.m:
compiler/make_hlds.m:
compiler/mercury_to_mercury.m:
	Change the code to handle the arg size data and the termination
	info separately.

compiler/prog_data.m:
	Change the internal representation of termination_info pragmas to
	hold the arg size data and the termination info separately.

compiler/prog_io_pragma.m:
	Change the external representation of termination_info pragmas to
	group the arg size data together with the output supplier data,
	to which it is logically connected.

compiler/module_qual.m:
compiler/modules.m:
	Change the code to accommodate the change to the internal
	representation of termination_info pragmas.

compiler/notes/compiler_design.html:
	Fix some documentation rot, and clarify some points.

doc/user_guide.texi:
	Document --term-single-arg.

library/bag.m:
	Add a new predicate, bag__least_upper_bound.

	Fix code that would execute wrongly in Prolog.

	Remove spaces from the ends of lines.

tests/term/*:
	A bunch of new test cases to test the behaviour of termination
	analysis. They are the small benchmark suite from our paper.

tests/Mmakefile:
	Enable the new test case directory.

Zoltan.

%-----------------------------------------------------------------------------%
% Copyright (C) 1997 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.
%-----------------------------------------------------------------------------%
%
% error_util.m
% Main author: zs.
% 
% This module contains code that can be helpful in the formatting of
% error messages.
%
%-----------------------------------------------------------------------------%

:- module error_util.

:- interface.

:- import_module io, list, term, string, int.

	% Given a context, a starting indentation level and a list of words,
	% print an error message that looks like this:
	%
	% module.m:10: first line of error message blah blah blah
	% module.m:10:   second line of error message blah blah blah
	% module.m:10:   third line of error message blah blah blah
	%
	% The words will be packed into lines as tightly as possible,
	% with spaces between each pair of words, subject to the constraints
	% that every line starts with a context, followed by Indent+1 spaces
	% on the first line and Indent+3 spaces on later lines, and that every
	% line contains at most 79 characters (unless a long single word
	% forces the line over this limit).

:- pred write_error_pieces(term__context::in, int::in, list(string)::in,
	io__state::di, io__state::uo) is det.

:- implementation.

:- import_module prog_out.

write_error_pieces(Context, Indent, Words) -->
	{
			% The fixed characters at the start of the line are:
			% filename
			% :
			% line number (min 3 chars)
			% :
			% space
			% indent
		Context = term__context(FileName, LineNumber),
		string__length(FileName, FileNameLength),
		string__int_to_string(LineNumber, LineNumberStr),
		string__length(LineNumberStr, LineNumberStrLength0),
		( LineNumberStrLength0 < 3 ->
			LineNumberStrLength = 3
		;
			LineNumberStrLength = LineNumberStrLength0
		),
		Remain is 79 - (FileNameLength + 1 +
			LineNumberStrLength + 2 + Indent),
		group_words(Words, Remain, Lines)
	},
	write_lines(Lines, Context, Indent).

:- pred write_lines(list(list(string))::in, term__context::in, int::in,
	io__state::di, io__state::uo) is det.

write_lines([], _, _) --> [].
write_lines([Line | Lines], Context, Indent) -->
	prog_out__write_context(Context),
	{ string__pad_left("", ' ', Indent, IndentStr) },
	io__write_string(IndentStr),
	write_line(Line),
	{ Indent2 is Indent + 2 },
	write_nonfirst_lines(Lines, Context, Indent2).

:- pred write_nonfirst_lines(list(list(string))::in, term__context::in, int::in,
	io__state::di, io__state::uo) is det.

write_nonfirst_lines([], _, _) --> [].
write_nonfirst_lines([Line | Lines], Context, Indent) -->
	prog_out__write_context(Context),
	{ string__pad_left("", ' ', Indent, IndentStr) },
	io__write_string(IndentStr),
	write_line(Line),
	write_nonfirst_lines(Lines, Context, Indent).

:- pred write_line(list(string)::in, io__state::di, io__state::uo) is det.

write_line([]) --> [].
write_line([Word | Words]) -->
	io__write_string(Word),
	write_line_rest(Words),
	io__write_char('\n').

:- pred write_line_rest(list(string)::in, io__state::di, io__state::uo) is det.

write_line_rest([]) --> [].
write_line_rest([Word | Words]) -->
	io__write_char(' '),
	io__write_string(Word),
	write_line_rest(Words).

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

	% Groups the given words into lines. The first line can have up to Max
	% characters on it; the later lines (if any) up to Max-2 characters.
	% The given list of words must be nonempty, since we always return
	% at least one line.

:- pred group_words(list(string)::in, int::in, list(list(string))::out) is det.

group_words(Words, Max, Lines) :-
	get_line_of_words(Words, Max, Line, RestWords),
	Max2 is Max - 2,
	group_nonfirst_line_words(RestWords, Max2, RestLines),
	Lines = [Line | RestLines].

:- pred group_nonfirst_line_words(list(string)::in, int::in,
	list(list(string))::out) is det.

group_nonfirst_line_words(Words, Max, Lines) :-
	( Words = [] ->
		Lines = []
	;
		get_line_of_words(Words, Max, Line, RestWords),
		group_nonfirst_line_words(RestWords, Max, RestLines),
		Lines = [Line | RestLines]
	).

:- pred get_line_of_words(list(string)::in, int::in,
	list(string)::out, list(string)::out) is det.

get_line_of_words([], _, [], []).
get_line_of_words([Word | Words], MaxLen, Line, RestWords) :-
	string__length(Word, WordLen),
	get_later_words(Words, WordLen, MaxLen, [Word], Line, RestWords).

:- pred get_later_words(list(string)::in, int::in, int::in,
	list(string)::in, list(string)::out, list(string)::out) is det.

get_later_words([], _, _, Line, Line, []).
get_later_words([Word | Words], OldLen, MaxLen, Line0, Line, RestWords) :-
	string__length(Word, WordLen),
	NewLen is OldLen + 1 + WordLen,
	( NewLen =< MaxLen ->
		append(Line0, [Word], Line1),
		get_later_words(Words, NewLen, MaxLen,
			Line1, Line, RestWords)
	;
		Line = Line0,
		RestWords = [Word | Words]
	).
%-----------------------------------------------------------------------------%
% Copyright (C) 1997 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_errors.m
% Main author: crs.
% 
% This module prints out the various error messages that are produced by
% the various modules of termination analysis.
%
%-----------------------------------------------------------------------------%

:- module term_errors.

:- interface.

:- import_module hlds_module.

:- import_module io, bag, std_util, list, assoc_list, term.

:- type termination_error
	--->	pragma_c_code

	;	imported_pred

	;	can_loop_proc_called(pred_proc_id, pred_proc_id)
			% can_loop_proc_called(Caller, Callee, Context)  
			% The call from Caller to Callee at the associated
			% context is to a procedure (Callee) whose termination
			% info is set to can_loop.
			% Although this error does not prevent us from
			% producing argument size information, it would
			% prevent us from proving termination.
			% We look for this error in pass 1; if we find it,
			% we do not perform pass 2.

	;	horder_args(pred_proc_id, pred_proc_id)
			% horder_args(Caller, Callee, Context)
			% The call from Caller to Callee at the associated
			% context has some arguments of a higher order type.
			% Valid in both passes.

	;	horder_call
			% horder_call
			% There is a higher order call at the associated
			% context.
			% Valid in both passes.

	;	inf_termination_const(pred_proc_id, pred_proc_id)
			% inf_termination_const(Caller, Callee, Context)
			% The call from Caller to Callee at the associated
			% context is to a procedure (Callee) whose arg size
			% info is set to infinite.
			% Valid in both passes.

	;	not_subset(pred_proc_id, bag(var), bag(var))
			% not_subset(Proc, SupplierVariables, InHeadVariables)
			% This error occurs when the bag of active variables
			% is not a subset of the input head variables.
			% Valid error only in pass 1.

	;	inf_call(pred_proc_id, pred_proc_id)
			% inf_call(Caller, Callee)
			% The call from Caller to Callee at the associated
			% context has infinite weight.
			% Valid error only in pass 2.

	;	cycle(pred_proc_id, assoc_list(pred_proc_id, term__context))
			% cycle(StartPPId, CallSites)
			% In the cycle of calls starting at StartPPId and
			% going through the named call sites may be an
			% infinite loop.

	;	no_eqns

	;	too_many_paths
			% There were too many distinct paths to be analyzed.
			% Valid in both passes (which analyze different sets
			% of paths).

	;	solver_failed
			% The solver could not find finite termination
			% constants for the procedures in the SCC.
			% Valid only in pass 1.

	;	is_builtin(pred_id)
			% The termination constant of the given builtin is
			% set to infinity; this happens when the type of at
			% least one output argument permits a norm greater
			% than zero.

	;	does_not_term_pragma(pred_id).
			% The given procedure has a does_not_terminate pragma.

:- type term_errors__error == pair(term__context, termination_error).

:- pred term_errors__report_term_errors(list(pred_proc_id)::in,
	list(term_errors__error)::in, module_info::in,
	io__state::di, io__state::uo) is det.

% An error is considered a simple error if it is likely that the error is
% caused by the analysis failing, instead of being due to a programming
% error. XXX this is not how it is used
:- pred simple_error(term_errors__termination_error).
:- mode simple_error(in) is semidet.

:- implementation.

:- import_module hlds_out, prog_out, hlds_pred, passes_aux, error_util.
:- import_module mercury_to_mercury, term_util, options, globals.

:- import_module bool, int, string, map, bag, require, varset.

simple_error(horder_call).
simple_error(pragma_c_code).
simple_error(imported_pred).
simple_error(can_loop_proc_called(_, _)).
simple_error(horder_args(_, _)).
simple_error(does_not_term_pragma(_)).

:- pred term_errors__output_same_SCC(pred_id, module_info, term__context,
	bool, io__state, io__state).
:- mode term_errors__output_same_SCC(in, in, in, in, di, uo) is det.

term_errors__output_same_SCC(PredId, Module, Context, ForHLDSDump) -->
	io__write_string("it is in the same SCC as the\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  "),
	hlds_out__write_pred_id(Module, PredId).

term_errors__report_term_errors(SCC, Errors, Module) -->
	{ get_context_from_scc(SCC, Module, Context) },
	( { SCC = [PPId] } ->
		{ Pieces0 = ["Termination", "of"] },
		{ term_errors__describe_one_proc_name(PPId, Module, PredName) },
		{ list__append(Pieces0, [PredName], Pieces1) },
		{ Single = yes(PPId) }
	;
		{ Pieces0 = ["Termination", "of", "the",
			"mutually", "recursive", "procedures"] },
		{ term_errors__describe_several_proc_names(SCC, Module, Context,
			PredNames) },
		{ list__append(Pieces0, PredNames, Pieces1) },
		{ Single = no }
	),
	(
		{ Errors = [] },
		{ error("empty list of errors") }
	;
		{ Errors = [Error] },
		{ Pieces2 = ["not", "proven", "for", "the",
			"following", "reason:"] },
		{ list__append(Pieces1, Pieces2, Pieces) },
		write_error_pieces(Context, 0, Pieces),
		term_errors__output_error(Error, Single, no, 0, Module)
	;
		{ Errors = [_, _ | _] },
		{ Pieces2 = ["not", "proven", "for", "the",
			"following", "reasons:"] },
		{ list__append(Pieces1, Pieces2, Pieces) },
		write_error_pieces(Context, 0, Pieces),
		term_errors__output_errors(Errors, Single, 1, 0, Module)
	).

:- pred term_errors__report_arg_size_errors(list(pred_proc_id)::in,
	list(term_errors__error)::in, module_info::in,
	io__state::di, io__state::uo) is det.

term_errors__report_arg_size_errors(SCC, Errors, Module) -->
	{ get_context_from_scc(SCC, Module, Context) },
	( { SCC = [PPId] } ->
		{ Pieces0 = ["Termination", "constant", "of"] },
		{ term_errors__describe_one_proc_name(PPId, Module, PredName) },
		{ list__append(Pieces0, [PredName], Pieces1) },
		{ Single = yes(PPId) }
	;
		{ Pieces0 = ["Termination", "constants", "of", "the",
			"mutually", "recursive", "procedures"] },
		{ term_errors__describe_several_proc_names(SCC, Module, Context,
			PredNames) },
		{ list__append(Pieces0, PredNames, Pieces1) },
		{ Single = no }
	),
	(
		{ Errors = [] },
		{ error("empty list of errors") }
	;
		{ Errors = [Error] },
		{ Pieces2 = ["set", "to", "infinity", "the",
			"following", "reason:"] },
		{ list__append(Pieces1, Pieces2, Pieces) },
		write_error_pieces(Context, 0, Pieces),
		term_errors__output_error(Error, Single, no, 0, Module)
	;
		{ Errors = [_, _ | _] },
		{ Pieces2 = ["set", "to", "infinity", "the",
			"following", "reasons:"] },
		{ list__append(Pieces1, Pieces2, Pieces) },
		write_error_pieces(Context, 0, Pieces),
		term_errors__output_errors(Errors, Single, 1, 0, Module)
	).

:- pred term_errors__output_errors(list(term_errors__error)::in,
	maybe(pred_proc_id)::in, int::in, int::in, module_info::in,
	io__state::di, io__state::uo) is det.

term_errors__output_errors([], _, _, _, _) --> [].
term_errors__output_errors([Error | Errors], Single, ErrNum0, Indent, Module)
		-->
	term_errors__output_error(Error, Single, yes(ErrNum0), Indent, Module),
	{ ErrNum1 is ErrNum0 + 1 },
	term_errors__output_errors(Errors, Single, ErrNum1, Indent, Module).

:- pred term_errors__output_error(term_errors__error::in,
	maybe(pred_proc_id)::in, maybe(int)::in, int::in, module_info::in,
	io__state::di, io__state::uo) is det.

term_errors__output_error(Context - Error, Single, ErrorNum, Indent, Module) -->
	{ term_errors__description(Error, Single, Module, Pieces0, Reason) },
	{ ErrorNum = yes(N) ->
		string__int_to_string(N, Nstr),
		string__append_list(["Reason ", Nstr, ":"], Preamble),
		Pieces = [Preamble | Pieces0]
	;
		Pieces = Pieces0
	},
	write_error_pieces(Context, Indent, Pieces),
	( { Reason = yes(InfArgSizePPId) } ->
		{ lookup_proc_arg_size_info(Module, InfArgSizePPId, ArgSize) },
		( { ArgSize = yes(infinite(ArgSizeErrors)) } ->
			% XXX the next line is cheating
			{ ArgSizePPIdSCC = [InfArgSizePPId] },
			term_errors__report_arg_size_errors(ArgSizePPIdSCC,
				ArgSizeErrors, Module)
		;
			{ error("inf arg size procedure does not have inf arg size") }
		)
	;
		[]
	).

:- pred term_errors__description(termination_error::in,
	maybe(pred_proc_id)::in, module_info::in, list(string)::out,
	maybe(pred_proc_id)::out) is det.

term_errors__description(horder_call, _, _, Pieces, no) :-
	Pieces = ["It", "contains", "a", "higher", "order", "call."].

term_errors__description(pragma_c_code, _, _, Pieces, no) :-
	Pieces = ["It", "contains", "a", "pragma", "c_code()", "declaration."].

term_errors__description(inf_call(CallerPPId, CalleePPId),
		Single, Module, Pieces, no) :-
	(
		Single = yes(PPId),
		require(unify(PPId, CallerPPId), "caller outside this SCC"),
		Piece1 = "It"
	;
		Single = no,
		term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
	),
	Piece2 = "calls",
	term_errors__describe_one_proc_name(CalleePPId, Module, CalleePiece),
	Pieces3 = ["with", "an", "unbounded", "increase", "in", "the",
		"size", "of", "the", "input", "arguments."],
	Pieces = [Piece1, Piece2, CalleePiece | Pieces3].

term_errors__description(can_loop_proc_called(CallerPPId, CalleePPId),
		Single, Module, Pieces, no) :-
	(
		Single = yes(PPId),
		require(unify(PPId, CallerPPId), "caller outside this SCC"),
		Piece1 = "It"
	;
		Single = no,
		term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
	),
	Piece2 = "calls",
	term_errors__describe_one_proc_name(CalleePPId, Module, CalleePiece),
	Pieces3 = ["which", "could", "not", "be", "proven", "to", "terminate."],
	Pieces = [Piece1, Piece2, CalleePiece | Pieces3].

term_errors__description(imported_pred, _, _, Pieces, no) :-
	Pieces = ["it", "contains", "imported", "code."].

term_errors__description(horder_args(CallerPPId, CalleePPId), Single, Module,
		Pieces, no) :-
	(
		Single = yes(PPId),
		require(unify(PPId, CallerPPId), "caller outside this SCC"),
		Piece1 = "It"
	;
		Single = no,
		term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
	),
	Piece2 = "calls",
	term_errors__describe_one_proc_name(CalleePPId, Module, CalleePiece),
	Pieces3 = ["with", "some", "higher", "order", "arguments."],
	Pieces = [Piece1, Piece2, CalleePiece | Pieces3].

term_errors__description(inf_termination_const(CallerPPId, CalleePPId),
		Single, Module, Pieces, yes(CalleePPId)) :-
	(
		Single = yes(PPId),
		require(unify(PPId, CallerPPId), "caller outside this SCC"),
		Piece1 = "It"
	;
		Single = no,
		term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
	),
	Piece2 = "calls",
	term_errors__describe_one_proc_name(CalleePPId, Module, CalleePiece),
	Pieces3 = ["which", "has", "a", "termination", "constant", "of",
		"infinity."],
	Pieces = [Piece1, Piece2, CalleePiece | Pieces3].

term_errors__description(not_subset(ProcPPId, OutputSuppliers, HeadVars),
		Single, Module, Pieces, no) :-
	(
		Single = yes(PPId),
		require(unify(PPId, ProcPPId), "not_subset outside this SCC"),
		Pieces1 = ["The", "set", "of", "its", "output", "supplier",
			"variables"]
	;
		Single = no,
		term_errors__describe_one_proc_name(ProcPPId, Module,
			PPIdPiece),
		Pieces1 = ["The", "set", "of", "output", "supplier",
			"variables", "of", PPIdPiece]
	),
	ProcPPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	proc_info_varset(ProcInfo, Varset),
	term_errors_var_bag_description(OutputSuppliers, Varset,
		OutputSuppliersPieces),
	Pieces3 = ["was", "not", "a", "subset", "of", "the", "head",
		"variables"],
	term_errors_var_bag_description(HeadVars, Varset, HeadVarsPieces),
	list__condense([Pieces1, OutputSuppliersPieces, Pieces3,
		HeadVarsPieces], Pieces).

term_errors__description(cycle(_StartPPId, CallSites), _, Module, Pieces, no) :-
	( CallSites = [DirectCall] ->
		term_errors__describe_one_call_site(DirectCall, Module, Site),
		Pieces = ["At", "the", "recursive", "call", "at", Site,
			"the", "arguments", "are", "not", "guaranteed",
			"to", "decrease", "in", "size."]
	;
		Pieces1 = ["in", "the", "recursive", "cycle",
			"through", "the", "calls", "at"],
		term_errors__describe_several_call_sites(CallSites, Module,
			Sites),
		Pieces2 = ["the", "arguments", "are", "not", "guaranteed",
			"to", "decrease", "in", "size."],
		list__condense([Pieces1, Sites, Pieces2], Pieces)
	).
	% Pieces = ["there", "was", "a", "cycle", "in", "the", "call", "graph",
	% "of", "this", "SCC", "where", "the", "variables", "did", "not",
	% "decrease", "in", "size."].

% term_errors__description(positive_value(CallerPPId, CalleePPId),
% 		Single, Module, Pieces, no) :-
% 	(
% 		Single = yes(PPId),
% 		PPId = CallerPPId,
% 		Piece1 = "it"
% 	;
% 		Single = no,
% 		term_errors__describe_one_proc_name(CallerPPId, Module, Piece1)
% 	),
% 	( CallerPPId = CalleePPId ->
% 		Pieces2 = ["contains", "a", "directly", "recursive", "call"]
% 	;
% 		term_errors__describe_one_proc_name(CalleePPId, Module,
% 			CalleePiece),
% 		Pieces2 = ["recursive", "call", "to", CalleePiece]
% 	),
% 	Pieces3 = ["with", "the", "size", "of", "the", "inputs", "increased."],
% 	list__append([Piece1 | Pieces2], Pieces3, Pieces).

term_errors__description(too_many_paths, _, _, Pieces, no) :-
	Pieces = ["There", "were", "too", "many", "execution", "paths",
		"for", "the", "analysis", "to", "process."].

term_errors__description(no_eqns, _, _, Pieces, no) :-
	Pieces = ["The", "analysis", "was", "unable", "to", "form", "any",
		"constraints", "between", "the", "arguments", "of", "the",
		"procedures", "in", "this", "SCC."].

term_errors__description(solver_failed, _, _, Pieces, no)  :-
	Pieces = ["The", "solver", "found", "the", "constraints", "produced",
		"by", "the", "analysis", "to", "be", "infeasible."].

term_errors__description(is_builtin(_PredId), _Single, _, Pieces, no) :-
	% XXX require(unify(Single, yes(_)), "builtin not alone in SCC"),
	Pieces = ["It", "is", "a", "builtin", "predicate."].

term_errors__description(does_not_term_pragma(PredId), Single, Module,
		Pieces, no) :-
	Pieces1 = ["There", "was", "a", "`does_not_terminate'", "pragma",
		"defined", "on"],
	(
		Single = yes(PPId),
		PPId = proc(SCCPredId, _),
		require(unify(PredId, SCCPredId), "does not terminate pragma outside this SCC"),
		Piece2 = "it."
	;
		Single = no,
		term_errors__describe_one_pred_name(PredId, Module,
			Piece2Nodot),
		string__append(Piece2Nodot, ".", Piece2)
	),
	list__append(Pieces1, [Piece2], Pieces).

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

:- pred term_errors_var_bag_description(bag(var)::in, varset::in,
	list(string)::out) is det.

term_errors_var_bag_description(HeadVars, Varset, Pieces) :-
	bag__to_assoc_list(HeadVars, HeadVarCountList),
	term_errors_var_bag_description_2(HeadVarCountList, Varset, yes,
		Pieces).

:- pred term_errors_var_bag_description_2(assoc_list(var, int)::in, varset::in,
	bool::in, list(string)::out) is det.

term_errors_var_bag_description_2([], _, _, ["{}"]).
term_errors_var_bag_description_2([Var - Count | VarCounts], Varset, First,
		[Piece | Pieces]) :-
	varset__lookup_name(Varset, Var, VarName),
	( Count > 1 ->
		string__append(VarName, "*", VarCountPiece0),
		string__int_to_string(Count, CountStr),
		string__append(VarCountPiece0, CountStr, VarCountPiece)
	;
		VarCountPiece = VarName
	),
	( First = yes ->
		string__append("{", VarCountPiece, Piece0)
	;
		Piece0 = VarCountPiece
	),
	( VarCounts = [] ->
		string__append(Piece0, "}.", Piece),
		Pieces = []
	;
		Piece = Piece0,
		term_errors_var_bag_description_2(VarCounts, Varset, First,
			Pieces)
	).

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

:- pred term_errors__describe_one_pred_name(pred_id::in, module_info::in,
	string::out) is det.

term_errors__describe_one_pred_name(PredId, Module, Piece) :-
	module_info_pred_info(Module, PredId, PredInfo),
	pred_info_module(PredInfo, ModuleName),
	pred_info_name(PredInfo, PredName),
	pred_info_arity(PredInfo, Arity),
	pred_info_get_is_pred_or_func(PredInfo, PredOrFunc),
	(
		PredOrFunc = predicate,
		PredOrFuncPart = "predicate ",
		OrigArity = Arity
	;
		PredOrFunc = function,
		PredOrFuncPart = "function ",
		OrigArity is Arity - 1
	),
	string__int_to_string(OrigArity, ArityPart),
	string__append_list([
		PredOrFuncPart,
		ModuleName,
		":",
		PredName,
		"/",
		ArityPart
		], Piece).

:- pred term_errors__describe_one_proc_name(pred_proc_id::in, module_info::in,
	string::out) is det.

term_errors__describe_one_proc_name(proc(PredId, ProcId), Module, Piece) :-
	module_info_pred_info(Module, PredId, PredInfo),
	pred_info_module(PredInfo, ModuleName),
	pred_info_name(PredInfo, PredName),
	pred_info_arity(PredInfo, Arity),
	pred_info_get_is_pred_or_func(PredInfo, PredOrFunc),
	(
		PredOrFunc = predicate,
		PredOrFuncPart = "predicate ",
		OrigArity = Arity
	;
		PredOrFunc = function,
		PredOrFuncPart = "function ",
		OrigArity is Arity - 1
	),
	string__int_to_string(OrigArity, ArityPart),
	proc_id_to_int(ProcId, ProcIdInt),
	string__int_to_string(ProcIdInt, ProcIdPart),
	string__append_list([
		PredOrFuncPart,
		ModuleName,
		":",
		PredName,
		"/",
		ArityPart,
		" mode ",
		ProcIdPart
		], Piece).

:- pred term_errors__describe_several_proc_names(list(pred_proc_id)::in,
	module_info::in, term__context::in, list(string)::out) is det.

term_errors__describe_several_proc_names([], _, _, []).
term_errors__describe_several_proc_names([PPId | PPIds], Module,
		Context, Pieces) :-
	term_errors__describe_one_proc_name(PPId, Module, Piece0),
	( PPIds = [] ->
		Pieces = [Piece0]
	; PPIds = [LastPPId] ->
		term_errors__describe_one_proc_name(LastPPId, Module,
			LastPiece),
		Pieces = [Piece0, "and", LastPiece]
	;
		string__append(Piece0, ",", Piece),
		term_errors__describe_several_proc_names(PPIds, Module,
			Context, Pieces1),
		Pieces = [Piece | Pieces1]
	).

:- pred term_errors__describe_one_call_site(pair(pred_proc_id,
	term__context)::in, module_info::in, string::out) is det.

term_errors__describe_one_call_site(PPId - Context, Module, Piece) :-
	term_errors__describe_one_proc_name(PPId, Module, ProcName),
	Context = term__context(FileName, LineNumber),
	string__int_to_string(LineNumber, LineNumberPart),
	string__append_list([
		ProcName,
		" at ",
		FileName,
		":",
		LineNumberPart
		], Piece).

:- pred term_errors__describe_several_call_sites(assoc_list(pred_proc_id,
	term__context)::in, module_info::in, list(string)::out) is det.

term_errors__describe_several_call_sites([], _, []).
term_errors__describe_several_call_sites([Site | Sites], Module, Pieces) :-
	term_errors__describe_one_call_site(Site, Module, Piece0),
	( Sites = [] ->
		Pieces = [Piece0]
	; Sites = [LastSite] ->
		term_errors__describe_one_call_site(LastSite, Module,
			LastPiece),
		Pieces = [Piece0, "and", LastPiece]
	;
		string__append(Piece0, ",", Piece),
		term_errors__describe_several_call_sites(Sites, Module,
			Pieces1),
		Pieces = [Piece | Pieces1]
	).

%----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% Copyright (C) 1997 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_pass1.m
%
% Main author: crs.
% Significant parts rewritten by zs.
%
% This file contains the first pass of the termination analysis,
% whose job is to discover an upper bound on the difference between
% the sizes of the output arguments of a procedure on the one hand and
% the sizes of a selected set of input arguments of the procedure
% on the other hand. We refer to this selected set of input arguments
% as the "output suppliers".
%
% For details, please refer to the papers mentioned in termination.m.
%
%-----------------------------------------------------------------------------%

:- module term_pass1.

:- interface.

:- import_module hlds_module, term_util, term_errors.
:- import_module io.

:- type arg_size_result
	--->	ok(
			list(pair(pred_proc_id, int)),
					% Gives the gamma of each procedure
					% in the SCC.
			used_args
					% Gives the output suppliers of
					% each procedure in the SCC.
		)
	;	error(
			list(term_errors__error)
		).

:- pred find_arg_sizes_in_scc(list(pred_proc_id)::in, module_info::in,
	functor_info::in, arg_size_result::out, list(term_errors__error)::out,
	io__state::di, io__state::uo) is det.

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

:- implementation.

:- import_module term_traversal, hlds_pred, hlds_goal, hlds_data.
:- import_module term_errors, mode_util, type_util, lp.

:- import_module int, float, char, string, bool, std_util, list, set, bag, map.
:- import_module term, varset, require.

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

:- type pass1_result
	--->	ok(
			list(path_info),
					% One entry for each path through the
					% code.
			used_args,
					% The next output_supplier map.
			list(term_errors__error)
					% There is any entry in this list for
					% each procedure in the SCC in which
					% the sey of active vars were not
					% a subset of the input arguments.
		)
	;	error(
			list(term_errors__error)
		).

find_arg_sizes_in_scc(SCC, Module, FunctorInfo, ArgSize, TermErrors, S0, S) :-
	init_output_suppliers(SCC, Module, InitOutputSupplierMap),
	find_arg_sizes_in_scc_fixpoint(SCC, Module, FunctorInfo,
		InitOutputSupplierMap, Result, TermErrors),
	(
		Result = ok(Paths, OutputSupplierMap, SubsetErrors),

		( SubsetErrors = [_ | _] ->
			ArgSize = error(SubsetErrors),
			S = S0
		; Paths = [] ->
			% There are no equations in this SCC
			% This has 2 possible causes.  If the predicate has
			% no output arguments, then the relative size of
			% input and output arguments is undefined.  If
			% there are no output arguments, then there will be
			% no equations created.  The other possibility is
			% that the procedure is a builtin predicate,  which
			% has an empty body.

			get_context_from_scc(SCC, Module, Context),
			ArgSize = error([Context - no_eqns]),
			S = S0
		;
			solve_equations(Paths, SCC, MaybeSolution, S0, S),
			(
				MaybeSolution = yes(Solution),
				ArgSize = ok(Solution, OutputSupplierMap)
			;
				MaybeSolution = no,
				get_context_from_scc(SCC, Module, Context),
				ArgSize = error([Context - solver_failed])
			)
		)
	;
		Result = error(Errors),
		ArgSize = error(Errors),
		S = S0
	).

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

% Initialise the output suppliers map.
% Initially, we consider that no input arguments contribute their size
% to the output arguments.

:- pred init_output_suppliers(list(pred_proc_id)::in, module_info::in,
	used_args::out) is det.

init_output_suppliers([], _Module, InitMap) :-
	map__init(InitMap).
init_output_suppliers([PPId | PPIds], Module, OutputSupplierMap) :-
	init_output_suppliers(PPIds, Module, OutputSupplierMap0),
	PPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	proc_info_headvars(ProcInfo, HeadVars),
	MapToNo = lambda([_HeadVar::in, Bool::out] is det, (Bool = no)),
	list__map(MapToNo, HeadVars, BoolList),
	map__det_insert(OutputSupplierMap0, PPId, BoolList, OutputSupplierMap).

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

:- pred find_arg_sizes_in_scc_fixpoint(list(pred_proc_id)::in,
	module_info::in, functor_info::in, used_args::in, pass1_result::out,
	list(term_errors__error)::out) is det.

find_arg_sizes_in_scc_fixpoint(SCC, Module, FunctorInfo, OutputSupplierMap0,
		Result, TermErrors) :-
	% unsafe_perform_io(io__write_string("find_arg_sizes_in_scc_pass\n")),
	% unsafe_perform_io(io__write(OutputSupplierMap0)),
	% unsafe_perform_io(io__write_string("\n")),
	find_arg_sizes_in_scc_pass(SCC, Module, FunctorInfo,
		OutputSupplierMap0, [], [], Result1, [], TermErrors1),
	(
		Result1 = error(_),
		Result = Result1,
		TermErrors = TermErrors1
	;
		Result1 = ok(_, OutputSupplierMap1, _),
		( OutputSupplierMap1 = OutputSupplierMap0 ->
			Result = Result1,
			TermErrors = TermErrors1
		;
			find_arg_sizes_in_scc_fixpoint(SCC, Module,
				FunctorInfo, OutputSupplierMap1,
				Result, TermErrors)
		)
	).

:- pred find_arg_sizes_in_scc_pass(list(pred_proc_id)::in,
	module_info::in, functor_info::in, used_args::in,
	list(path_info)::in, list(term_errors__error)::in, pass1_result::out,
	list(term_errors__error)::in, list(term_errors__error)::out) is det.

find_arg_sizes_in_scc_pass([], _, _, OutputSupplierMap, Paths, SubsetErrors,
		Result, TermErrors, TermErrors) :-
	Result = ok(Paths, OutputSupplierMap, SubsetErrors).
find_arg_sizes_in_scc_pass([PPId | PPIds], Module, FunctorInfo,
		OutputSupplierMap0, Paths0, SubsetErrors0, Result,
		TermErrors0, TermErrors) :-
	find_arg_sizes_pred(PPId, Module, FunctorInfo, OutputSupplierMap0,
		Result1, TermErrors1),
	list__append(TermErrors0, TermErrors1, TermErrors2),
	list__take_upto(3, TermErrors2, TermErrors3),
	(
		Result1 = error(_),
		Result = Result1,
		TermErrors = TermErrors3
	;
		Result1 = ok(Paths1, OutputSupplierMap1, SubsetErrors1),
		list__append(Paths0, Paths1, Paths),
		list__append(SubsetErrors0, SubsetErrors1, SubsetErrors),
		find_arg_sizes_in_scc_pass(PPIds, Module, FunctorInfo,
			OutputSupplierMap1, Paths, SubsetErrors, Result,
			TermErrors3, TermErrors)
	).

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

:- pred find_arg_sizes_pred(pred_proc_id::in, module_info::in,
	functor_info::in, used_args::in, pass1_result::out,
	list(term_errors__error)::out) is det.

find_arg_sizes_pred(PPId, Module, FunctorInfo, OutputSupplierMap0, Result,
		TermErrors) :-
	PPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, PredInfo, ProcInfo),
	pred_info_context(PredInfo, Context),
	proc_info_headvars(ProcInfo, Args),
	proc_info_argmodes(ProcInfo, ArgModes),
	proc_info_vartypes(ProcInfo, VarTypes),
	proc_info_goal(ProcInfo, Goal),
	map__init(EmptyMap),
	init_traversal_params(Module, FunctorInfo, PPId, Context, VarTypes,
		OutputSupplierMap0, EmptyMap, Params),

	partition_call_args(Module, ArgModes, Args, InVars, OutVars),
	Path0 = path_info(PPId, no, 0, [], OutVars),
	set__singleton_set(PathSet0, Path0),
	Info0 = ok(PathSet0, []),
	traverse_goal(Goal, Params, Info0, Info),

	(
		Info = ok(Paths, TermErrors),
		set__to_sorted_list(Paths, PathList),
		upper_bound_active_vars(PathList, AllActiveVars),
		map__lookup(OutputSupplierMap0, PPId,
			OutputSuppliers0),
		update_output_suppliers(Args, AllActiveVars,
			OutputSuppliers0, OutputSuppliers),
		map__det_update(OutputSupplierMap0, PPId,
			OutputSuppliers, OutputSupplierMap),
		( bag__is_subbag(AllActiveVars, InVars) ->
			SubsetErrors = []
		;
			SubsetErrors = [Context -
				not_subset(PPId, AllActiveVars, InVars)]
		),
		Result = ok(PathList, OutputSupplierMap, SubsetErrors)
	;
		Info = error(Errors, TermErrors),
		Result = error(Errors)
	).

:- pred update_output_suppliers(list(var)::in, bag(var)::in,
	list(bool)::in, list(bool)::out) is det.

update_output_suppliers([], _ActiveVars, [], []).
update_output_suppliers([_ | _], _ActiveVars, [], []) :-
	error("update_output_suppliers: Unmatched variables").
update_output_suppliers([], _ActiveVars, [_ | _], []) :-
	error("update_output_suppliers: Unmatched variables").
update_output_suppliers([Arg | Args], ActiveVars,
		[OutputSupplier0 | OutputSuppliers0],
		[OutputSupplier | OutputSuppliers]) :-
	( bag__contains(ActiveVars, Arg) ->
		OutputSupplier = yes
	;
		% This guarantees that the set of output suppliers can only
		% increase, which in turn guarantees that our fixpoint
		% computation is monotonic and therefore terminates.
		OutputSupplier = OutputSupplier0
	),
	update_output_suppliers(Args, ActiveVars,
		OutputSuppliers0, OutputSuppliers).

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

% Solve the list of constraints

% output is of the form required by lp_solve.
% which is given the input = [eqn(Const, PPid, [PPidList])]
% max: .......
% c1: PPid - (PPidList) > Const;
% c2: PPid - (PPidList) > Const;
% where PPid (proc(PredId, ProcId)) is printed as ' aPredId_ProcId - b '
% The choice of the letter `a' is arbitrary, and is chosen as lp_solve does
% not allow variables to start with digits.
% The variable `b' is used as lp_solve will only solve for positive values
% of variables.  replacing each variable occurance with ` a#_# - b ', this
% avoids the problem of only allowing positive variables as  a#_# - b can
% be negative even when a#_# and b are both positive.

:- pred solve_equations(list(path_info)::in, list(pred_proc_id)::in,
	maybe(list(pair(pred_proc_id, int)))::out,
	io__state::di, io__state::uo) is det.

solve_equations(Paths, PPIds, Result, S0, S) :-
	(
		convert_equations(Paths, Varset, Equations,
			Objective, PPVars)
	->
		map__values(PPVars, AllVars0),
		list__sort_and_remove_dups(AllVars0, AllVars),
		% unsafe_perform_io(io__write_string("before\n")),
		% unsafe_perform_io(io__write(Equations)),
		% unsafe_perform_io(io__write_string("\n")),
		% unsafe_perform_io(io__write(Objective)),
		% unsafe_perform_io(io__write_string("\n")),
		% unsafe_perform_io(io__write(AllVars)),
		% unsafe_perform_io(io__write_string("\n")),
		lp_solve(Equations, min, Objective, Varset, AllVars, Soln,
			S0, S),
		% unsafe_perform_io(io__write_string("after\n")),
		(
			Soln = unsatisfiable,
			Result = no
		;
			Soln = satisfiable(_ObjVal, SolnVal),
			list__map(lookup_coeff(PPVars, SolnVal), PPIds,
				SolutionList),
			Result = yes(SolutionList)
		)
	;
		Result = no,
		S = S0
	).

:- pred convert_equations(list(path_info)::in, varset::out, lp__equations::out,
	objective::out, map(pred_proc_id, var)::out) is semidet.

convert_equations(Paths, Varset, Equations, Objective, PPVars) :-
	varset__init(Varset0),
	map__init(PredProcVars0),
	set__init(EqnSet0),
	convert_equations_2(Paths, PredProcVars0, PPVars, Varset0, Varset,
		EqnSet0, EqnSet),
	set__to_sorted_list(EqnSet, Equations),
	map__values(PPVars, Vars),
	Convert = lambda([Var::in, Coeff::out] is det,
	(
		Coeff = Var - 1.0
	)),
	list__map(Convert, Vars, Objective).

:- pred convert_equations_2(list(path_info)::in,
	map(pred_proc_id, var)::in, map(pred_proc_id, var)::out,
	varset::in, varset::out,
	set(lp__equation)::in, set(lp__equation)::out) is semidet.

convert_equations_2([], PPVars, PPVars, Varset, Varset, Eqns, Eqns).
convert_equations_2([Path | Paths], PPVars0, PPVars, Varset0, Varset,
		Eqns0, Eqns) :-
	Path = path_info(ThisPPId, _, IntGamma, PPIds, _),
	int__to_float(IntGamma, FloatGamma),
	Eqn = eqn(Coeffs, (>=), FloatGamma),
	pred_proc_var(ThisPPId, ThisVar, Varset0, Varset2, PPVars0, PPVars1),
	Coeffs = [ThisVar - 1.0 | RestCoeffs],
	Convert = lambda([PPId::in, Coeff::out, Pair0::in, Pair::out] is det,
	(
		Pair0 = VS0 - PPV0,
		pred_proc_var(PPId, Var, VS0, VS, PPV0, PPV),
		Coeff = Var - (-1.0),
		Pair = VS - PPV
	)),
	list__map_foldl(Convert, PPIds, RestCoeffs, Varset2 - PPVars1,
		Varset3 - PPVars2),
	set__insert(Eqns0, Eqn, Eqns1),
	convert_equations_2(Paths, PPVars2, PPVars, Varset3, Varset,
		Eqns1, Eqns).

:- pred lookup_coeff(map(pred_proc_id, var)::in, map(var, float)::in,
	pred_proc_id::in, pair(pred_proc_id, int)::out) is det.

lookup_coeff(PPIds, Soln, PPId, PPId - ICoeff) :-
	map__lookup(PPIds, PPId, Var),
	map__lookup(Soln, Var, Coeff),
	float__ceiling_to_int(Coeff, ICoeff).

:- pred pred_proc_var(pred_proc_id::in, var::out, varset::in, varset::out,
	map(pred_proc_id, var)::in, map(pred_proc_id, var)::out) is det.

pred_proc_var(PPId, Var, Varset0, Varset, PPVars0, PPVars) :-
	( map__search(PPVars0, PPId, Var0) ->
		Var = Var0,
		Varset = Varset0,
		PPVars = PPVars0
	;
		varset__new_var(Varset0, Var, Varset),
		map__det_insert(PPVars0, PPId, Var, PPVars)
	).

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------
% Copyright (C) 1997 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_pass2.m
%
% Main author of original version: crs.
% Main author of this version: zs.
%
% This file contains the code that tries to prove that procedures terminate.
%
% For details, please refer to the papers mentioned in termination.m.
%-----------------------------------------------------------------------------

:- module term_pass2.
:- interface.

:- import_module hlds_module, term_util.

:- pred prove_termination_in_scc(list(pred_proc_id)::in, module_info::in,
	functor_info::in, int::in, termination_info::out) is det.

:- implementation.

:- import_module term_traversal, term_util, term_errors.
:- import_module hlds_pred, hlds_goal, prog_data, type_util, mode_util.

:- import_module std_util, bool, int, list, assoc_list.
:- import_module set, bag, map, term, require.

:- type fixpoint_dir
	--->	up
	;	down.

:- type call_weight_info
	==	pair(list(term_errors__error), call_weight_graph).

:- type call_weight_graph
	==	map(pred_proc_id,		% The max noninfinite weight
						% call from this proc
			map(pred_proc_id,	% to this proc
				pair(term__context, int))).
						% is at this context and with
						% this weight.

:- type pass2_result
	--->	ok(
			call_weight_info,
			used_args
		)
	;	error(
			list(term_errors__error)
		).

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

prove_termination_in_scc(SCC, Module, FunctorInfo, SingleArgs, Termination) :-
	init_rec_input_suppliers(SCC, Module, InitRecSuppliers),
	prove_termination_in_scc_trial(SCC, InitRecSuppliers, down,
		Module, FunctorInfo, Termination1),
	(
		Termination1 = can_loop(Errors),
		(
			% On large SCCs, single arg analysis can require
			% many iterations, so we allow the user to limit
			% the size of the SCCs we will try it on.
			list__length(SCC, ProcCount),
			ProcCount =< SingleArgs,

			% Don't try single arg analysis if it cannot cure
			% the reason for the failure of the main analysis.
			\+ (
				member(Error, Errors),
				Error = _ - imported_pred
			),
			prove_termination_in_scc_single_arg(SCC,
				Module, FunctorInfo)
		->
			Termination = cannot_loop
		;
			Termination = Termination1
		)
	;
		Termination1 = cannot_loop,
		Termination = Termination1
	).

	% Initialise the set of recursive input suppliers to be the set
	% of all input variables in all procedures of the SCC.

:- pred init_rec_input_suppliers(list(pred_proc_id)::in, module_info::in,
	used_args::out) is det.

init_rec_input_suppliers([], _, InitMap) :-
	map__init(InitMap).
init_rec_input_suppliers([PPId | PPIds], Module, RecSupplierMap) :-
	init_rec_input_suppliers(PPIds, Module, RecSupplierMap0),
	PPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	proc_info_headvars(ProcInfo, HeadVars),
	proc_info_argmodes(ProcInfo, ArgModes),
	partition_call_args(Module, ArgModes, HeadVars, InArgs, _OutVars),
	MapIsInput = lambda([HeadVar::in, Bool::out] is det,
	(
		( bag__contains(InArgs, HeadVar) ->
			Bool = yes
		;
			Bool = no
		)
	)),
	list__map(MapIsInput, HeadVars, BoolList),
	map__det_insert(RecSupplierMap0, PPId, BoolList, RecSupplierMap).

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

	% Perform single arg analysis on the SCC.
	%
	% We pick one procedure in the SCC (one of those with minimal arity).
	% We set the recursive input suppliers of this procedure to contain
	% only the first input argument, and the recursive input suppliers
	% of the other procedures to the empty set, and try a fixpoint
	% iteration. If it works, great, if not, try again with the next
	% input arg of the selected procedure, until we run out of input
	% arguments of that procedure.
	%
	% While the fixpoint iteration in the main algorithm looks for the
	% greatest fixpoint, in which the recursive input supplier sets
	% cannot increase, in single arg analysis we are looking for a
	% smallest fixpoint starting from a given location, so we must
	% make sure that the recursive input supplier sets cannot decrease.

:- pred prove_termination_in_scc_single_arg(list(pred_proc_id)::in,
	module_info::in, functor_info::in) is semidet.

prove_termination_in_scc_single_arg(SCC, Module, FunctorInfo) :-
	( SCC = [FirstPPId | LaterPPIds] ->
		lookup_proc_arity(FirstPPId, Module, FirstArity),
		find_min_arity_proc(LaterPPIds, FirstPPId, FirstArity, Module,
			TrialPPId, RestSCC),
		prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC, 1,
			Module, FunctorInfo)
	;
		error("empty SCC in prove_termination_in_scc_single_arg")
	).

	% Find a procedure of minimum arity among the given list and the
	% tentative guess.

:- pred find_min_arity_proc(list(pred_proc_id)::in, pred_proc_id::in, int::in,
	module_info::in, pred_proc_id::out, list(pred_proc_id)::out) is det.

find_min_arity_proc([], BestSofarPPId, _, _, BestSofarPPId, []).
find_min_arity_proc([PPId | PPIds], BestSofarPPId, BestSofarArity, Module,
		BestPPId, RestSCC) :-
	lookup_proc_arity(PPId, Module, Arity),
	( Arity < BestSofarArity ->
		find_min_arity_proc(PPIds, PPId, Arity,
			Module, BestPPId, RestSCC0),
		RestSCC = [BestSofarPPId | RestSCC0]
	;
		find_min_arity_proc(PPIds, BestSofarPPId, BestSofarArity,
			Module, BestPPId, RestSCC0),
		RestSCC = [PPId | RestSCC0]
	).

	% Perform single arg analysis on the SCC.

:- pred prove_termination_in_scc_single_arg_2(pred_proc_id::in,
	list(pred_proc_id)::in, int::in, module_info::in, functor_info::in)
	is semidet.

prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC, ArgNum0,
		Module, FunctorInfo) :-
	init_rec_input_suppliers_single_arg(TrialPPId, RestSCC,
		ArgNum0, Module, InitRecSuppliers),
	prove_termination_in_scc_trial([TrialPPId | RestSCC], InitRecSuppliers,
		up, Module, FunctorInfo, Termination),
	( Termination = cannot_loop ->
		true
	;
		ArgNum1 is ArgNum0 + 1,
		prove_termination_in_scc_single_arg_2(TrialPPId, RestSCC,
			ArgNum1, Module, FunctorInfo)
	).

:- pred init_rec_input_suppliers_single_arg(pred_proc_id::in,
	list(pred_proc_id)::in, int::in, module_info::in, used_args::out)
	is semidet.

init_rec_input_suppliers_single_arg(TrialPPId, RestSCC, ArgNum, Module,
		RecSupplierMap) :-
	TrialPPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	proc_info_argmodes(ProcInfo, ArgModes),
	init_rec_input_suppliers_add_single_arg(ArgModes, ArgNum,
		Module, TrialPPIdRecSuppliers),
	map__init(RecSupplierMap0),
	map__det_insert(RecSupplierMap0, TrialPPId, TrialPPIdRecSuppliers,
		RecSupplierMap1),
	init_rec_input_suppliers_single_arg_others(RestSCC, Module,
		RecSupplierMap1, RecSupplierMap).

:- pred init_rec_input_suppliers_add_single_arg(list(mode)::in, int::in,
	module_info::in, list(bool)::out) is semidet.

init_rec_input_suppliers_add_single_arg([Mode | Modes], ArgNum, Module,
		BoolList) :-
	(
		mode_is_input(Module, Mode),
		ArgNum = 1
	->
		MapToNo = lambda([_Mode::in, Bool::out] is det,
		(
			Bool = no
		)),
		list__map(MapToNo, Modes, BoolList1),
		BoolList = [yes | BoolList1]
	;
		(
			mode_is_output(Module, Mode)
		->
			NextArgNum = ArgNum
		;
			mode_is_input(Module, Mode),
			ArgNum > 1
		->
			NextArgNum is ArgNum - 1
		;
			fail
		)
	->
		init_rec_input_suppliers_add_single_arg(Modes, NextArgNum,
			Module, BoolList1),
		BoolList = [no | BoolList1]
	;
		fail
	).

:- pred init_rec_input_suppliers_single_arg_others(list(pred_proc_id)::in,
	module_info::in, used_args::in, used_args::out) is det.

init_rec_input_suppliers_single_arg_others([], _,
	RecSupplierMap, RecSupplierMap).
init_rec_input_suppliers_single_arg_others([PPId | PPIds], Module,
		RecSupplierMap0, RecSupplierMap) :-
	PPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	proc_info_headvars(ProcInfo, HeadVars),
	MapToNo = lambda([_HeadVar::in, Bool::out] is det,
	(
		Bool = no
	)),
	list__map(MapToNo, HeadVars, BoolList),
	map__det_insert(RecSupplierMap0, PPId, BoolList, RecSupplierMap1),
	init_rec_input_suppliers_single_arg_others(PPIds, Module,
		RecSupplierMap1, RecSupplierMap).

:- pred lookup_proc_arity(pred_proc_id::in, module_info::in, int::out) is det.

lookup_proc_arity(PPId, Module, Arity) :-
	PPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	proc_info_headvars(ProcInfo, HeadVars),
	list__length(HeadVars, Arity).

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

:- pred prove_termination_in_scc_trial(list(pred_proc_id)::in, used_args::in,
	fixpoint_dir::in, module_info::in, functor_info::in,
	termination_info::out) is det.

prove_termination_in_scc_trial(SCC, InitRecSuppliers, FixDir, Module,
		FunctorInfo, Termination) :-
	prove_termination_in_scc_fixpoint(SCC, FixDir, Module, FunctorInfo,
		InitRecSuppliers, Result),
	(
		Result = ok(CallInfo, _),
		CallInfo = InfCalls - CallWeights,
		(
			InfCalls \= []
		->
			list__take_upto(3, InfCalls, ReportedInfCalls),
			Termination = can_loop(ReportedInfCalls)
		;
			zero_or_positive_weight_cycles(CallWeights, Module,
				Cycles),
			Cycles \= []
		->
			list__take_upto(3, Cycles, ReportedCycles),
			Termination = can_loop(ReportedCycles)
		;
			Termination = cannot_loop
		)
	;
		Result = error(Errors),
		Termination = can_loop(Errors)
	).

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

:- pred prove_termination_in_scc_fixpoint(list(pred_proc_id)::in,
	fixpoint_dir::in, module_info::in, functor_info::in, used_args::in,
	pass2_result::out) is det.

prove_termination_in_scc_fixpoint(SCC, FixDir, Module, FunctorInfo,
		RecSupplierMap0, Result) :-
	% unsafe_perform_io(io__write_string("prove_termination_in_scc\n")),
	% unsafe_perform_io(io__write(RecSupplierMap0)),
	% unsafe_perform_io(io__write_string("\n")),
	map__init(NewRecSupplierMap0),
	map__init(CallWeightGraph0),
	CallInfo0 = [] - CallWeightGraph0,
	prove_termination_in_scc_pass(SCC, FixDir, Module, FunctorInfo,
		RecSupplierMap0, NewRecSupplierMap0, CallInfo0, Result1),
	(
		Result1 = ok(_, RecSupplierMap1),
		( RecSupplierMap1 = RecSupplierMap0 ->
			% We are at a fixed point, so further analysis
			% will not get any better results.
			Result = Result1
		;
			prove_termination_in_scc_fixpoint(SCC, FixDir,
				Module, FunctorInfo, RecSupplierMap1, Result)
		)
	;
		Result1 = error(_),
		Result = Result1
	).

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

	% Process a whole SCC, to determine the termination property of each
	% procedure in that SCC.

:- pred prove_termination_in_scc_pass(list(pred_proc_id)::in, fixpoint_dir::in,
	module_info::in, functor_info::in, used_args::in, used_args::in,
	call_weight_info::in, pass2_result::out) is det.

prove_termination_in_scc_pass([], _, _, _, _, NewRecSupplierMap, CallInfo,
		ok(CallInfo, NewRecSupplierMap)).
prove_termination_in_scc_pass([PPId | PPIds], FixDir, Module, FunctorInfo,
		RecSupplierMap, NewRecSupplierMap0, CallInfo0, Result) :-
	% Get the goal info.
	PPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, PredInfo, ProcInfo),
	pred_info_context(PredInfo, Context),
	proc_info_goal(ProcInfo, Goal),
	proc_info_vartypes(ProcInfo, VarTypes),
	map__init(EmptyMap),
	init_traversal_params(Module, FunctorInfo, PPId, Context, VarTypes,
		EmptyMap, RecSupplierMap, Params),
	set__init(PathSet0),
	Info0 = ok(PathSet0, []),
	traverse_goal(Goal, Params, Info0, Info),
	(
		Info = ok(Paths, CanLoop),
		require(unify(CanLoop, []),
			"can_loop detected in pass2 but not pass1"),
		set__to_sorted_list(Paths, PathList),
		upper_bound_active_vars(PathList, ActiveVars),
		map__lookup(RecSupplierMap, PPId, RecSuppliers0),
		proc_info_headvars(ProcInfo, Args),
		bag__init(EmptyBag),
		update_rec_input_suppliers(Args, ActiveVars, FixDir,
			RecSuppliers0, RecSuppliers,
			EmptyBag, RecSuppliers0Bag),
		map__det_insert(NewRecSupplierMap0, PPId, RecSuppliers,
			NewRecSupplierMap1),
		add_call_arcs(PathList, RecSuppliers0Bag,
			CallInfo0, CallInfo1),
		prove_termination_in_scc_pass(PPIds, FixDir, Module,
			FunctorInfo, RecSupplierMap,
			NewRecSupplierMap1, CallInfo1, Result)
	;
		Info = error(Errors, CanLoop),
		require(unify(CanLoop, []),
			"can_loop detected in pass2 but not pass1"),
		Result = error(Errors)
	).

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

:- pred update_rec_input_suppliers(list(var)::in, bag(var)::in,
	fixpoint_dir::in, list(bool)::in, list(bool)::out,
	bag(var)::in, bag(var)::out) is det.

update_rec_input_suppliers([], _, _, [], [], RecBag, RecBag).
update_rec_input_suppliers([_ | _], _, _, [], [], _, _) :-
	error("update_rec_input_suppliers: Unmatched variables").
update_rec_input_suppliers([], _, _, [_ | _], [], _, _) :-
	error("update_rec_input_suppliers: Unmatched variables").
update_rec_input_suppliers([Arg | Args], ActiveVars, FixDir,
		[RecInputSupplier0 | RecInputSuppliers0],
		[RecInputSupplier | RecInputSuppliers],
		RecBag0, RecBag) :-
	(
		RecInputSupplier0 = yes,
		bag__insert(RecBag0, Arg, RecBag1)
	;
		RecInputSupplier0 = no,
		RecBag1 = RecBag0
	),
	(
		FixDir = down,
		% This guarantees that the set of rec input suppliers
		% can only decrease.
		( bag__contains(ActiveVars, Arg) ->
			RecInputSupplier = RecInputSupplier0
		;
			RecInputSupplier = no
		)
	;
		FixDir = up,
		% This guarantees that the set of rec input suppliers
		% can only increase.
		( bag__contains(ActiveVars, Arg) ->
			RecInputSupplier = yes
		;
			RecInputSupplier = RecInputSupplier0
		)
	),
	update_rec_input_suppliers(Args, ActiveVars, FixDir,
		RecInputSuppliers0, RecInputSuppliers, RecBag1, RecBag).

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

% This adds the information from a stage 2 traversal to the graph.
% The graph's nodes are the procedures in the current SCC.
% The graph's edges represent calls from one procedure in the SCC to another.
% The number attached to the edge from p to q shows the upper bound
% on the difference between the size of the recursive input supplier arguments
% in the call to q and the size of the recursive input supplier arguments
% in the head of p. If there is no finite upper bound, then we insert the
% details of the call into the list of "infinite" calls.

:- pred add_call_arcs(list(path_info)::in,
	bag(var)::in, call_weight_info::in, call_weight_info::out) is det.

add_call_arcs([], _RecInputSuppliers, CallInfo, CallInfo).
add_call_arcs([Path | Paths], RecInputSuppliers, CallInfo0, CallInfo) :-
	Path = path_info(PPId, CallSite, GammaConst, GammaVars, ActiveVars),
	( CallSite = yes(CallPPIdPrime - ContextPrime) ->
		CallPPId = CallPPIdPrime,
		Context = ContextPrime
	;
		error("no call site in path in stage 2")
	),
	( GammaVars = [] ->
		true
	;
		error("gamma variables in path in stage 2")
	),
	CallInfo0 = InfCalls0 - CallWeights0,
	( bag__is_subbag(ActiveVars, RecInputSuppliers) ->
		( map__search(CallWeights0, PPId, NeighbourMap0) ->
			( map__search(NeighbourMap0, CallPPId, OldEdgeInfo) ->
				OldEdgeInfo = _OldContext - OldWeight,
				( OldWeight >= GammaConst ->
					EdgeInfo = OldEdgeInfo
				;
					EdgeInfo = Context - GammaConst
				),
				map__det_update(NeighbourMap0, CallPPId,
					EdgeInfo, NeighbourMap)
			;
				map__det_insert(NeighbourMap0, CallPPId,
					Context - GammaConst, NeighbourMap)
			),
			map__det_update(CallWeights0, PPId, NeighbourMap,
				CallWeights1)
		;
			map__init(NeighbourMap0),
			map__det_insert(NeighbourMap0, CallPPId,
				Context - GammaConst, NeighbourMap),
			map__det_insert(CallWeights0, PPId, NeighbourMap,
				CallWeights1)
		),
		CallInfo1 = InfCalls0 - CallWeights1
	;
		InfCalls1 = [Context - inf_call(PPId, CallPPId) | InfCalls0],
		CallInfo1 = InfCalls1 - CallWeights0
	),
	add_call_arcs(Paths, RecInputSuppliers, CallInfo1, CallInfo).

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

	% We use a simple depth first search to find and return the list
	% of all cycles in the call graph of the SCC where the change in
	% the size of the recursive input supplier arguments of the procedure
	% that serves as the start and end point of the circularity are
	% not guaranteed to decrease.
	%
	% Finding one such cycle is enough for us to conclude that we
	% cannot prove termination of the procedures in the SCC; we collect
	% all cycles because it may be useful to print them out (if not
	% all, then maybe a limited set).

:- pred zero_or_positive_weight_cycles(call_weight_graph::in,
	module_info::in, list(term_errors__error)::out) is det.

zero_or_positive_weight_cycles(CallWeights, Module, Cycles) :-
	map__keys(CallWeights, PPIds),
	zero_or_positive_weight_cycles_2(PPIds, CallWeights, Module, Cycles).

:- pred zero_or_positive_weight_cycles_2(list(pred_proc_id)::in,
	call_weight_graph::in, module_info::in,
	list(term_errors__error)::out) is det.

zero_or_positive_weight_cycles_2([], _, _, []).
zero_or_positive_weight_cycles_2([PPId | PPIds], CallWeights, Module, Cycles) :-
	zero_or_positive_weight_cycles_from(PPId, CallWeights, Module, Cycles1),
	zero_or_positive_weight_cycles_2(PPIds, CallWeights, Module, Cycles2),
	list__append(Cycles1, Cycles2, Cycles).

:- pred zero_or_positive_weight_cycles_from(pred_proc_id::in,
	call_weight_graph::in, module_info::in,
	list(term_errors__error)::out) is det.

zero_or_positive_weight_cycles_from(PPId, CallWeights, Module, Cycles) :-
	map__lookup(CallWeights, PPId, NeighboursMap),
	map__to_assoc_list(NeighboursMap, NeighboursList),
	PPId = proc(PredId, _ProcId),
	module_info_pred_info(Module, PredId, PredInfo),
	pred_info_context(PredInfo, Context),
	zero_or_positive_weight_cycles_from_neighbours(NeighboursList,
		PPId, Context, 0, [], CallWeights, Cycles).

:- pred zero_or_positive_weight_cycles_from_neighbours(assoc_list(pred_proc_id,
	pair(term__context, int))::in, pred_proc_id::in, term__context::in,
	int::in, assoc_list(pred_proc_id, term__context)::in,
	call_weight_graph::in, list(term_errors__error)::out) is det.

zero_or_positive_weight_cycles_from_neighbours([], _, _, _, _, _, []).
zero_or_positive_weight_cycles_from_neighbours([Neighbour | Neighbours],
		LookforPPId, Context, WeightSoFar, VisitedCalls, CallWeights,
		Cycles) :-
	zero_or_positive_weight_cycles_from_neighbour(Neighbour, LookforPPId,
		Context, WeightSoFar, VisitedCalls, CallWeights, Cycles1),
	zero_or_positive_weight_cycles_from_neighbours(Neighbours, LookforPPId,
		Context, WeightSoFar, VisitedCalls, CallWeights, Cycles2),
	list__append(Cycles1, Cycles2, Cycles).

:- pred zero_or_positive_weight_cycles_from_neighbour(pair(pred_proc_id,
	pair(term__context, int))::in, pred_proc_id::in, term__context::in,
	int::in, assoc_list(pred_proc_id, term__context)::in,
	call_weight_graph::in, list(term_errors__error)::out) is det.

zero_or_positive_weight_cycles_from_neighbour(CurPPId - (Context - EdgeWeight),
		LookforPPId, ProcContext, WeightSoFar0, VisitedCalls,
		CallWeights, Cycles) :-
	WeightSoFar1 is WeightSoFar0 + EdgeWeight,
	(
		CurPPId = LookforPPId
	->
		% We have a cycle on the looked for ppid.
		( WeightSoFar1 >= 0 ->
			FinalVisitedCalls = [CurPPId - Context | VisitedCalls],
			list__reverse(FinalVisitedCalls, RevFinalVisitedCalls),
			Cycles = [ProcContext -
				cycle(LookforPPId, RevFinalVisitedCalls)]
		;
			Cycles = []
		)
	;
		assoc_list__keys(VisitedCalls, VisitedPPIds),
		list__member(CurPPId, VisitedPPIds)
	->
		% We have a cycle, but not on the looked for ppid.
		% We ignore it here; it will be picked up when we process
		% that ppid.
		Cycles = []
	;
		% No cycle; try all possible edges from this node.
		NewVisitedCalls = [CurPPId - Context | VisitedCalls],
		map__lookup(CallWeights, CurPPId, NeighboursMap),
		map__to_assoc_list(NeighboursMap, NeighboursList),
		zero_or_positive_weight_cycles_from_neighbours(NeighboursList,
			LookforPPId, ProcContext, WeightSoFar1,
			NewVisitedCalls, CallWeights, Cycles)
	).

%-----------------------------------------------------------------------------
%-----------------------------------------------------------------------------%
% Copyright (C) 1997 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_traversal.m
%
% Main author: crs.
% Significant rewrite by zs.
%
% This module contains the code used to traverse procedure bodies
% for both passes of termination analysis.
%
% For details, please refer to the papers mentioned in termination.m.
%
%-----------------------------------------------------------------------------%

:- module term_traversal.

:- interface.

:- import_module term_util, term_errors.
:- import_module hlds_module, hlds_pred, hlds_goal, prog_data.
:- import_module list, bag, map, std_util, term.

:- type traversal_info
	--->	ok(
			set(path_info),
					% Information about the paths we have
					% followed. With a conjunction of
					% length N, each of whose elements is
					% a branched control structure, the
					% number of paths through the
					% conjunction is 2^N. The reason why
					% we use a set of path_infos instead
					% of a list is that this can postpone
					% the representation getting too big
					% if (as is at least moderately likely)
					% many of the paths have identical
					% properties.
			list(term_errors__error)
					% Have we processed a call to a
					% procedure whose maybe termination
					% info was yes(can_loop(_))?
					% If yes, record the error here.
					% (This is not an error in pass 1,
					% but we want to find this out in
					% pass 1 so we can avoid doing pass 2.)
		)
	;	error(
			list(term_errors__error),
					% Errors which are fatal in both
					% passes.
			list(term_errors__error)
					% Have we processed a call to a
					% procedure whose maybe termination
					% info was yes(can_loop(_))?
					% If yes, record the error here.
					% (This is not an error in pass 1,
					% but we want to find this out in
					% pass 1 so we can avoid doing pass 2.)
		).

:- type path_info
	--->	path_info(
			pred_proc_id,	% The identify of the procedure
					% that this path is within.
			maybe(pair(pred_proc_id, term__context)),
					% If no, path was started at the end
					% of the procedure given by field 1.
					% If yes, the arg names the procedure
					% at the call to which the path started
					% and the context of the call.
					% In pass 1, all starts should be no.
					% In pass 2, all starts should be yes.
			int,			
			list(pred_proc_id),
			bag(var)
					% These three fields describe the
					% right hand side of the inequation
					% we are propagating.
		).

:- type traversal_params.

:- pred init_traversal_params(module_info::in, functor_info::in,
	pred_proc_id::in, term__context::in, map(var, type)::in,
	used_args::in, used_args::in, traversal_params::out) is det.

:- pred traverse_goal(hlds_goal::in, traversal_params::in,
	traversal_info::in, traversal_info::out) is det.

:- pred upper_bound_active_vars(list(path_info)::in, bag(var)::out) is det.

:- implementation.

:- import_module hlds_data, type_util.
:- import_module bool, int, set, require.

traverse_goal(Goal, Params, Info0, Info) :-
	Goal = GoalExpr - GoalInfo,
	(
		goal_info_get_determinism(GoalInfo, Detism),
		determinism_components(Detism, _, at_most_zero)
	->
		cannot_succeed(Info0, Info1)
	;
		Info1 = Info0
	),
	traverse_goal_2(GoalExpr, GoalInfo, Params, Info1, Info).

:- pred traverse_goal_2(hlds_goal_expr::in, hlds_goal_info::in,
	traversal_params::in, traversal_info::in, traversal_info::out) is det.

traverse_goal_2(unify(_Var, _RHS, _UniMode, Unification, _Context),
		_GoalInfo, Params, Info0, Info) :-
	(
		Unification = construct(OutVar, ConsId, Args, Modes),
		(
			unify_change(OutVar, ConsId, Args, Modes, Params,
				Gamma, InVars, OutVars0)
		->
			bag__insert(OutVars0, OutVar, OutVars),
			record_change(InVars, OutVars, Gamma, [], Info0, Info)
		;
			% length(Args) is not necessarily equal to length(Modes)
			% for higher order constructions.
			Info = Info0
		)
	;
		Unification = deconstruct(InVar, ConsId, Args, Modes, _),
		(
			unify_change(InVar, ConsId, Args, Modes, Params,
				Gamma0, InVars0, OutVars)
		->
			bag__insert(InVars0, InVar, InVars),
			Gamma is 0 - Gamma0,
			record_change(InVars, OutVars, Gamma, [], Info0, Info)
		;
			error("higher order deconstruction")
		)
	;
		Unification = assign(OutVar, InVar),
		bag__init(Empty),
		bag__insert(Empty, InVar, InVars),
		bag__insert(Empty, OutVar, OutVars),
		record_change(InVars, OutVars, 0, [], Info0, Info)
	;
		Unification = simple_test(_InVar1, _InVar2),
		Info = Info0
	;
		Unification = complicated_unify(_, _),
		error("Unexpected complicated_unify in termination analysis")
	).

traverse_goal_2(conj(Goals), _, Params, Info0, Info) :-
	list__reverse(Goals, RevGoals),
	traverse_conj(RevGoals, Params, Info0, Info).

traverse_goal_2(switch(_, _, Cases, _), _, Params, Info0, Info) :-
	traverse_switch(Cases, Params, Info0, Info).

traverse_goal_2(disj(Goals, _StoreMap), _, Params, Info0, Info) :-
	traverse_disj(Goals, Params, Info0, Info).

traverse_goal_2(not(Goal), _, Params, Info0, Info) :-
		% Since goal cannot bind any active variables,
		% we don't need to traverse Goal for pass1,
		% but it shouldn't hurt either.
	traverse_goal(Goal, Params, Info0, Info).

traverse_goal_2(some(_Vars, Goal), _GoalInfo, Params, Info0, Info) :-
	traverse_goal(Goal, Params, Info0, Info).

traverse_goal_2(if_then_else(_, Cond, Then, Else, _), _, Params, Info0, Info) :-
	traverse_conj([Then, Cond], Params, Info0, Info1),
	traverse_goal(Else, Params, Info0, Info2),
	combine_paths(Info1, Info2, Params, Info).

traverse_goal_2(pragma_c_code(_, _, CallPredId, CallProcId, Args, _, _, _),
		GoalInfo, Params, Info0, Info) :-
	params_get_module_info(Params, Module),
	module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
		CallProcInfo),
	proc_info_argmodes(CallProcInfo, CallArgModes),
	partition_call_args(Module, CallArgModes, Args, _InVars, OutVars),
	goal_info_get_context(GoalInfo, Context),
	error_if_intersect(OutVars, Context, pragma_c_code, Info0, Info).

traverse_goal_2(higher_order_call(_, _, _, _, _, _),
		GoalInfo, _Params, Info0, Info) :-
	goal_info_get_context(GoalInfo, Context),
	add_error(Context, horder_call, Info0, Info).

traverse_goal_2(call(CallPredId, CallProcId, Args, _, _, _),
		GoalInfo, Params, Info0, Info) :-
	goal_info_get_context(GoalInfo, Context),
	params_get_module_info(Params, Module),
	params_get_ppid(Params, PPId),
	CallPPId = proc(CallPredId, CallProcId),

	module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
		CallProcInfo),
	proc_info_argmodes(CallProcInfo, CallArgModes),
	proc_info_get_maybe_arg_size_info(CallProcInfo, CallArgSizeInfo),
	proc_info_get_maybe_termination_info(CallProcInfo, CallTerminationInfo),

	partition_call_args(Module, CallArgModes, Args, InVars, OutVars),

	% Handle existing paths
	(
		CallArgSizeInfo = yes(finite(CallGamma, OutputSuppliers)),
		remove_unused_args(InVars, Args, OutputSuppliers, UsedInVars),
		record_change(UsedInVars, OutVars, CallGamma, [], Info0, Info1)
	;
		CallArgSizeInfo = yes(infinite(_)),
		error_if_intersect(OutVars, Context,
			inf_termination_const(PPId, CallPPId), Info0, Info1)
	;
		CallArgSizeInfo = no,
		% We should get to this point only in pass 1.
		% In pass 2, OutputSuppliersMap will be empty,
		% which will lead to a runtime abort in map__lookup.
		params_get_output_suppliers(Params, OutputSuppliersMap),
		map__lookup(OutputSuppliersMap, CallPPId, OutputSuppliers),
		remove_unused_args(InVars, Args, OutputSuppliers, UsedInVars),
		record_change(UsedInVars, OutVars, 0, [CallPPId], Info0, Info1)
	),

	% Did we call a non-terminating procedure?
	(
		CallTerminationInfo = yes(can_loop(_))
	->
		called_can_loop(Context, can_loop_proc_called(PPId, CallPPId),
			Info1, Info2)
	;
		Info2 = Info1
	),

	% Did we call a procedure with some procedure-valued arguments?
	(
		% This is an overapproximation, since it includes
		% higher order outputs. XXX
		params_get_var_types(Params, VarTypes),
		horder_vars(Args, VarTypes)
	->
		add_error(Context, horder_args(PPId, CallPPId), Info2, Info3)
	;
		Info3 = Info2
	),

	% Do we start another path?
	(
		params_get_rec_input_suppliers(Params, RecInputSuppliersMap),
		map__search(RecInputSuppliersMap, CallPPId, RecInputSuppliers)
	->
		% We should get to this point only in pass 2, and then
		% only if this call is to a procedure in the current SCC.
		% In pass 1, RecInputSuppliersMap will be empty.

		compute_rec_start_vars(Args, RecInputSuppliers, Bag),
		PathStart = yes(CallPPId - Context),
		NewPath = path_info(PPId, PathStart, 0, [], Bag),
		add_path(NewPath, Info3, Info)
	;
		Info = Info3
	).

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

	% Traverse_conj should be invoked with a reversed list of goals.
	% This is to keep stack consumption down.

:- pred traverse_conj(list(hlds_goal)::in, traversal_params::in,
	traversal_info::in, traversal_info::out) is det.

traverse_conj([], _, Info, Info).
traverse_conj([Goal | Goals], Params, Info0, Info) :-
	traverse_goal(Goal, Params, Info0, Info1),
	traverse_conj(Goals, Params, Info1, Info).

:- pred traverse_disj(list(hlds_goal)::in, traversal_params::in,
	traversal_info::in, traversal_info::out) is det.

traverse_disj([], _, _, ok(Empty, [])) :-
	set__init(Empty).
traverse_disj([Goal | Goals], Params, Info0, Info) :-
	traverse_goal(Goal, Params, Info0, Info1),
	traverse_disj(Goals, Params, Info0, Info2),
	combine_paths(Info1, Info2, Params, Info).

:- pred traverse_switch(list(case)::in, traversal_params::in,
	traversal_info::in, traversal_info::out) is det.

traverse_switch([], _, _, ok(Empty, [])) :-
	set__init(Empty).
traverse_switch([case(_, Goal) | Cases], Params, Info0, Info) :-
	traverse_goal(Goal, Params, Info0, Info1),
	traverse_switch(Cases, Params, Info0, Info2),
	combine_paths(Info1, Info2, Params, Info).

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

:- pred cannot_succeed(traversal_info::in, traversal_info::out) is det.

cannot_succeed(error(Errors, CanLoop), error(Errors, CanLoop)).
cannot_succeed(ok(_, CanLoop), ok(Empty, CanLoop)) :-
	set__init(Empty).

:- pred add_path(path_info::in, traversal_info::in, traversal_info::out) is det.

add_path(_, error(Errors, CanLoop), error(Errors, CanLoop)).
add_path(Path, ok(Paths0, CanLoop), ok(Paths, CanLoop)) :-
	set__insert(Paths0, Path, Paths).

:- pred add_error(term__context::in, termination_error::in,
	traversal_info::in, traversal_info::out) is det.

add_error(Context, Error, error(Errors0, CanLoop),
		error(Errors, CanLoop)) :-
	Errors1 = [Context - Error | Errors0],
	list__take_upto(3, Errors1, Errors).
add_error(Context, Error, ok(_, CanLoop),
		error([Context - Error], CanLoop)).

:- pred called_can_loop(term__context::in, termination_error::in,
	traversal_info::in, traversal_info::out) is det.

called_can_loop(Context, Error, error(Errors, CanLoop0),
		error(Errors, CanLoop)) :-
	CanLoop1 = [Context - Error | CanLoop0],
	list__take_upto(3, CanLoop1, CanLoop).
called_can_loop(Context, Error, ok(Paths, CanLoop0), ok(Paths, CanLoop)) :-
	CanLoop1 = [Context - Error | CanLoop0],
	list__take_upto(3, CanLoop1, CanLoop).

:- pred combine_paths(traversal_info::in, traversal_info::in,
	traversal_params::in, traversal_info::out) is det.

combine_paths(error(Errors1, CanLoop1), error(Errors2, CanLoop2), _,
		error(Errors, CanLoop)) :-
	list__append(Errors1, Errors2, Errors3),
	list__take_upto(3, Errors3, Errors),
	list__append(CanLoop1, CanLoop2, CanLoop3),
	list__take_upto(3, CanLoop3, CanLoop).
combine_paths(error(Errors1, CanLoop1), ok(_, CanLoop2), _,
		error(Errors1, CanLoop)) :-
	list__append(CanLoop1, CanLoop2, CanLoop3),
	list__take_upto(3, CanLoop3, CanLoop).
combine_paths(ok(_, CanLoop1), error(Errors2, CanLoop2), _,
		error(Errors2, CanLoop)) :-
	list__append(CanLoop1, CanLoop2, CanLoop3),
	list__take_upto(3, CanLoop3, CanLoop).
combine_paths(ok(Paths1, CanLoop1), ok(Paths2, CanLoop2), Params,
		Info) :-
	list__append(CanLoop1, CanLoop2, CanLoop3),
	list__take_upto(3, CanLoop3, CanLoop),
	set__union(Paths2, Paths1, Paths),
	(
		% Don't try to track the state of too many paths;
		% doing so can require too much memory.
		set__count(Paths, Count),
		Count =< 256
	->
		Info = ok(Paths, CanLoop)
	;
		params_get_context(Params, Context),
		Info = error([Context - too_many_paths], CanLoop)
	).

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

:- pred compute_rec_start_vars(list(var)::in, list(bool)::in,
	bag(var)::out) is det.

compute_rec_start_vars([], [], Out) :-
	bag__init(Out).
compute_rec_start_vars([_|_], [], _Out) :-
	error("Unmatched vars in compute_rec_start_vars\n").
compute_rec_start_vars([], [_|_], _Out) :-
	error("Unmatched vars in compute_rec_start_vars\n").
compute_rec_start_vars([Var | Vars], [RecInputSupplier | RecInputSuppliers],
		Out) :-
	compute_rec_start_vars(Vars, RecInputSuppliers, Out1),
	( RecInputSupplier = yes ->
		bag__insert(Out1, Var, Out)
	;
		Out = Out1
	).

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

	% unify_change is invoked for unifications of the form X = f(Yi),
	% with the first argument giving the identity of X, the second the
	% identity of f, the third and fourth the identity and modes of the Yi.
	% unify_change returns the norm of f and the bags of input and output
	% variables among the Yi. It is up to the caller to look after the
	% sign of the norm of f and after the membership of X in either the
	% input or output bags. The predicate fails if invoked on a higher
	% order unification.

:- pred unify_change(var::in, cons_id::in, list(var)::in, list(uni_mode)::in,
	traversal_params::in, int::out, bag(var)::out, bag(var)::out)
	is semidet.

unify_change(OutVar, ConsId, Args0, Modes0, Params, Gamma, InVars, OutVars) :-
	params_get_functor_info(Params, FunctorInfo),
	params_get_var_types(Params, VarTypes),
	map__lookup(VarTypes, OutVar, Type),
	\+ type_is_higher_order(Type, _, _),
	( type_to_type_id(Type, TypeId, _) ->
		params_get_module_info(Params, Module),
		functor_norm(FunctorInfo, TypeId, ConsId, Module,
			Gamma, Args0, Args, Modes0, Modes),
		split_unification_vars(Args, Modes, Module, InVars, OutVars)
	;
		error("variable type in traverse_goal_2")
	).

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

:- pred record_change(bag(var)::in, bag(var)::in, int::in,
	list(pred_proc_id)::in, traversal_info::in, traversal_info::out) is det.

record_change(_, _, _, _, error(Errors, CanLoop), error(Errors, CanLoop)).
record_change(InVars, OutVars, Gamma, CalledPPIds, ok(Paths0, CanLoop),
		ok(NewPaths, CanLoop)) :-
	set__to_sorted_list(Paths0, PathsList0),
	set__init(NewPaths0),
	record_change_2(PathsList0, InVars, OutVars, Gamma, CalledPPIds,
		NewPaths0, NewPaths).

:- pred record_change_2(list(path_info)::in, bag(var)::in, bag(var)::in,
	int::in, list(pred_proc_id)::in,
	set(path_info)::in, set(path_info)::out) is det.

record_change_2([], _, _, _, _, PathSet, PathSet).
record_change_2([Path0 | Paths0], InVars, OutVars, CallGamma, CallPPIds,
		PathSet0, PathSet) :-
	Path0 = path_info(ProcData, Start, Gamma0, PPIds0, Vars0),
	( bag__intersect(OutVars, Vars0) ->
		% The change produces some active variables.
		Gamma is CallGamma + Gamma0,
		list__append(CallPPIds, PPIds0, PPIds),
		bag__subtract(Vars0, OutVars, Vars1),
		bag__union(InVars, Vars1, Vars),
		Path = path_info(ProcData, Start, Gamma, PPIds, Vars)
	;
		% The change produces no active variables.
		Path = Path0
	),
	set__insert(PathSet0, Path, PathSet1),
	record_change_2(Paths0, InVars, OutVars, CallGamma, CallPPIds,
		PathSet1, PathSet).

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

:- pred error_if_intersect(bag(var)::in, term__context::in,
	termination_error::in, traversal_info::in, traversal_info::out) is det.

error_if_intersect(_, _, _, error(Errors, CanLoop), error(Errors, CanLoop)).
error_if_intersect(OutVars, Context, ErrorMsg, ok(Paths, CanLoop), Info)
		:-
	(
		set__to_sorted_list(Paths, PathList),
		some_active_vars_in_bag(PathList, OutVars)
	->
		Info = error([Context - ErrorMsg], CanLoop)
	;
		Info = ok(Paths, CanLoop)
	).

:- pred some_active_vars_in_bag(list(path_info)::in, bag(var)::in) is semidet.

some_active_vars_in_bag([Path | Paths], OutVars) :-
	(
		Path = path_info(_, _, _, _, Vars),
		bag__intersect(Vars, OutVars)
	;
		some_active_vars_in_bag(Paths, OutVars)
	).

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

upper_bound_active_vars([], ActiveVars) :-
	bag__init(ActiveVars).
upper_bound_active_vars([Path | Paths], ActiveVars) :-
	upper_bound_active_vars(Paths, ActiveVars1),
	Path = path_info(_, _, _, _, ActiveVars2),
	bag__least_upper_bound(ActiveVars1, ActiveVars2, ActiveVars).

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

:- type traversal_params
	--->	traversal_params(
			module_info,
			functor_info,
			pred_proc_id,	% The procedure we are tracing through.
			term__context,	% The context of the procedure.
			map(var, type),
			map(pred_proc_id, list(bool)),
					% Output suppliers of each procedure.
					% Empty during pass 2.
			map(pred_proc_id, list(bool))
					% Rec input suppliers of each procedure.
					% Empty during pass 1.
		).

init_traversal_params(ModuleInfo, FunctorInfo, PredProcId, Context, VarTypes,
		OutputSuppliers, RecInputSuppliers, Params) :-
	Params = traversal_params(ModuleInfo, FunctorInfo, PredProcId, Context,
		VarTypes, OutputSuppliers, RecInputSuppliers).

:- pred params_get_module_info(traversal_params::in, module_info::out)
	is det.
:- pred params_get_functor_info(traversal_params::in, functor_info::out)
	is det.
:- pred params_get_ppid(traversal_params::in, pred_proc_id::out)
	is det.
:- pred params_get_context(traversal_params::in, term__context::out)
	is det.
:- pred params_get_var_types(traversal_params::in, map(var, type)::out)
	is det.
:- pred params_get_output_suppliers(traversal_params::in,
	map(pred_proc_id, list(bool))::out) is det.
:- pred params_get_rec_input_suppliers(traversal_params::in,
	map(pred_proc_id, list(bool))::out) is det.

params_get_module_info(Params, A) :-
	Params = traversal_params(A, _, _, _, _, _, _).

params_get_functor_info(Params, B) :-
	Params = traversal_params(_, B, _, _, _, _, _).

params_get_ppid(Params, C) :-
	Params = traversal_params(_, _, C, _, _, _, _).

params_get_context(Params, D) :-
	Params = traversal_params(_, _, _, D, _, _, _).

params_get_var_types(Params, E) :-
	Params = traversal_params(_, _, _, _, E, _, _).

params_get_output_suppliers(Params, F) :-
	Params = traversal_params(_, _, _, _, _, F, _).

params_get_rec_input_suppliers(Params, G) :-
	Params = traversal_params(_, _, _, _, _, _, G).


[continued in part 2]