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

Zoltan Somogyi zs at cs.mu.oz.au
Tue Dec 2 15:19:58 AEDT 1997
Previous message: for review: changes to termination analysis and stack tracing [1/3]
Next message: for review: changes to termination analysis and stack tracing [3/3]
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
[continued from part 1]

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% 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_util.m
% Main author: crs.
%
% This module:
%
% -	defines the types used by termination analysis
% -	defines predicates for computing functor norms
% -	defines some utility predicates
%
%-----------------------------------------------------------------------------%

:- module term_util.

:- interface.

:- import_module term_errors, prog_data.
:- import_module hlds_module, hlds_pred, hlds_data, hlds_goal.

:- import_module bool, int, list, map, bag, term.

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

% The arg size info defines an upper bound on the difference
% between the sizes of the output arguments of a procedure and the sizes
% of the input arguments:
%
% | input arguments | + constant >= | output arguments |
%
% where | | represents a semilinear norm.

:- type arg_size_info
	--->	finite(int, list(bool))
				% The termination constant is a finite integer.
				% The list of bool has a 1:1 correspondance
				% with the input arguments of the procedure.
				% It stores whether the argument contributes
				% to the size of the output arguments.

	;	infinite(list(term_errors__error)).
				% There is no finite integer for which the
				% above equation is true. The argument says
				% why the analysis failed to find a finite
				% constant.

:- type termination_info
	---> 	cannot_loop	% This procedure terminates for all
				% possible inputs.

	;	can_loop(list(term_errors__error)).
				% The analysis could not prove that the
				% procedure terminates.

:- type used_args	==	map(pred_proc_id, list(bool)).

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

% We use semilinear norms (denoted by ||) to compute the sizes of terms.
% These have the form
%
% | f(t1, ... tn) | = weight(f) + sum of | ti |
% where i is an element of a set I, and I is a subset of {1, ... n}
%
% We currently support four kinds of semilinear norms.

:- type functor_info
	--->	simple	% All non-constant functors have weight 1,
			% while constants have weight 0.
			% Use the size of all subterms (I = {1, ..., n}.

	;	total	% All functors have weight = arity of the functor.
			% Use the size of all subterms (I = {1, ..., n}.

	;	use_map(weight_table)
			% The weight of each functor is given by the table.
			% Use the size of all subterms (I = {1, ..., n}.

	;	use_map_and_args(weight_table).
			% The weight of each functor is given by the table,
			% and so is the set of arguments of the functor whose
			% size should be counted (I is given by the table
			% entry of the functor).

:- type unify_info	==	pair(map(var, type), functor_info).

:- type weight_info	--->	weight(int, list(bool)).
:- type weight_table	==	map(pair(type_id, cons_id), weight_info).

:- pred find_weights(module_info::in, weight_table::out) is det.

% This predicate is 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.

:- pred functor_norm(functor_info::in, type_id::in, cons_id::in,
	module_info::in, int::out, list(var)::in, list(var)::out,
	list(uni_mode)::in, list(uni_mode)::out) is det.

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

% This predicate partitions the arguments of a call into a list of input
% variables and a list of output variables,

:- pred partition_call_args(module_info::in, list(mode)::in, list(var)::in,
	bag(var)::out, bag(var)::out) is det.

% Given a list of variables from a unification, this predicate divides the
% list into a bag of input variables, and a bag of output variables.

:- pred split_unification_vars(list(var)::in, list(uni_mode)::in,
	module_info::in, bag(var)::out, bag(var)::out) is det.

%  Used to create lists of boolean values, which are used for used_args.
%  make_bool_list(HeadVars, BoolIn, BoolOut) creates a bool list which is
%  (length(HeadVars) - length(BoolIn)) `no' followed by BoolIn.  This is
%  used to set the used args for compiler generated predicates.  The no's
%  at the start are because the Type infos are not used. length(BoolIn)
%  should equal the arity of the predicate, and the difference in length
%  between the arity of the procedure and the arity of the predicate is
%  the number of type infos.

:- pred term_util__make_bool_list(list(_T)::in, list(bool)::in,
	list(bool)::out) is det.

% Removes variables from the InVarBag that are not used in the call.
% remove_unused_args(InVarBag0, VarList, BoolList, InVarBag)
% VarList and BoolList are corresponding lists.  Any variable in VarList
% that has a `no' in the corresponding place in the BoolList is removed
% from InVarBag.

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

% This predicate sets the argument size info of a given a list of procedures.

:- pred set_pred_proc_ids_arg_size_info(list(pred_proc_id)::in,
	arg_size_info::in, module_info::in, module_info::out) is det.

% This predicate sets the termination info of a given a list of procedures.

:- pred set_pred_proc_ids_termination_info(list(pred_proc_id)::in,
	termination_info::in, module_info::in, module_info::out) is det.

:- pred lookup_proc_termination_info(module_info::in, pred_proc_id::in,
	maybe(termination_info)::out) is det.

:- pred lookup_proc_arg_size_info(module_info::in, pred_proc_id::in,
	maybe(arg_size_info)::out) is det.

% Succeeds if one or more variables in the list are higher order.

:- pred horder_vars(list(var), map(var, type)).
:- mode horder_vars(in, in) is semidet.

% Succeeds if all values of the given type are zero size (for all norms).

:- pred zero_size_type(type, module_info).
:- mode zero_size_type(in, in) is semidet.

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

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

:- implementation.

:- import_module inst_match, prog_out, mode_util, type_util.
:- import_module globals, options.

:- import_module io, std_util, assoc_list, require.

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

% Calculate the weight to be assigned to each function symbol for the
% use_map and use_map_and_args semilinear norms.
%
% Given a type definition such as
%
% :- type t(Tk)	--->	f1(a11, ... a1n1)	where n1 is the arity of f1
%		;	...
%		;	fm(am1, ... amnm)	where nm is the arity of fm
%
% we check, for each aij, whether its type is recursive (i.e. it is t with
% type variable arguments that are a permutation of Tk). The weight info
% we compute for each functor will have a boolean list that has a `yes'
% for each recursive argument and a `no' for each nonrecursive argument.
% The weight to be assigned to the functor is the number of nonrecursive
% arguments, except that we assign a weight of at least 1 to all functors
% which are not constants.

find_weights(ModuleInfo, Weights) :-
	module_info_types(ModuleInfo, TypeTable),
	map__to_assoc_list(TypeTable, TypeList),
	map__init(Weights0),
	find_weights_for_type_list(TypeList, Weights0, Weights).

:- pred find_weights_for_type_list(assoc_list(type_id, hlds_type_defn)::in,
	weight_table::in, weight_table::out) is det.

find_weights_for_type_list([], Weights, Weights).
find_weights_for_type_list([TypeId - TypeDefn | TypeList], Weights0, Weights) :-
	find_weights_for_type(TypeId, TypeDefn, Weights0, Weights1),
	find_weights_for_type_list(TypeList, Weights1, Weights).

:- pred find_weights_for_type(type_id::in, hlds_type_defn::in,
	weight_table::in, weight_table::out) is det.

find_weights_for_type(TypeId, TypeDefn, Weights0, Weights) :-
	hlds_data__get_type_defn_body(TypeDefn, TypeBody),
	(
		TypeBody = du_type(Constructors, _, _, _),
		hlds_data__get_type_defn_tparams(TypeDefn, TypeParams),
		find_weights_for_cons_list(Constructors, TypeId, TypeParams,
			Weights0, Weights)
	;
		TypeBody = uu_type(_),
		error("undiscriminated union types not yet implemented")
	;
		% This type does not introduce any functors
		TypeBody = eqv_type(_),
		Weights = Weights0
	;
		% This type may introduce some functors,
		% but we will never see them in this analysis
		TypeBody = abstract_type,
		Weights = Weights0
	).

:- pred find_weights_for_cons_list(list(constructor)::in,
	type_id::in, list(type_param)::in,
	weight_table::in, weight_table::out) is det.

find_weights_for_cons_list([], _, _, Weights, Weights).
find_weights_for_cons_list([Constructor | Constructors], TypeId, Params,
		Weights0, Weights) :-
	find_weights_for_cons(Constructor, TypeId, Params, Weights0, Weights1),
	find_weights_for_cons_list(Constructors, TypeId, Params,
		Weights1, Weights).

:- pred find_weights_for_cons(constructor::in,
	type_id::in, list(type_param)::in,
	weight_table::in, weight_table::out) is det.

find_weights_for_cons(SymName - Args, TypeId, Params, Weights0, Weights) :-
	list__length(Args, Arity),
	( Arity > 0 ->
		find_and_count_nonrec_args(Args, TypeId, Params,
			NumNonRec, ArgInfos0),
		( NumNonRec = 0 ->
			Weight = 1,
			list__duplicate(Arity, yes, ArgInfos)
		;
			Weight = NumNonRec,
			ArgInfos = ArgInfos0
		),
		WeightInfo = weight(Weight, ArgInfos)
	;
		WeightInfo = weight(0, [])
	),
	ConsId = cons(SymName, Arity),
	map__det_insert(Weights0, TypeId - ConsId, WeightInfo, Weights).

:- pred find_and_count_nonrec_args(list(constructor_arg)::in,
	type_id::in, list(type_param)::in,
	int::out, list(bool)::out) is det.

find_and_count_nonrec_args([], _, _, 0, []).
find_and_count_nonrec_args([Arg | Args], Id, Params, NonRecArgs, ArgInfo) :-
	find_and_count_nonrec_args(Args, Id, Params, NonRecArgs0, ArgInfo0),
	( is_arg_recursive(Arg, Id, Params) ->
		NonRecArgs = NonRecArgs0,
		ArgInfo = [yes | ArgInfo0]
	;
		NonRecArgs is NonRecArgs0 + 1,
		ArgInfo = [no | ArgInfo0]
	).

:- pred is_arg_recursive(constructor_arg::in,
	type_id::in, list(type_param)::in) is semidet.

is_arg_recursive(Arg, Id, Params) :-
	Arg = _Name - ArgType,
	type_to_type_id(ArgType, ArgTypeId, ArgTypeParams),
	Id = ArgTypeId,
	list__perm(Params, ArgTypeParams).

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

% Although the module info is not used in either of these norms, it could
% be needed for other norms, so it should not be removed.

functor_norm(simple, _, ConsId, _, Int, Args, Args, Modes, Modes) :-
	(
		ConsId = cons(_, Arity),
		Arity \= 0
	->
		Int = 1
	;
		Int = 0
	).
functor_norm(total, _, ConsId, _Module, Int, Args, Args, Modes, Modes) :-
	( ConsId = cons(_, Arity) ->
		Int = Arity
	;
		Int = 0
	).
functor_norm(use_map(WeightMap), TypeId, ConsId, _Module, Int,
		Args, Args, Modes, Modes) :-
	( map__search(WeightMap, TypeId - ConsId, WeightInfo) ->
		WeightInfo = weight(Int, _)
	;
		Int = 0
	).
functor_norm(use_map_and_args(WeightMap), TypeId, ConsId, _Module, Int,
		Args0, Args, Modes0, Modes) :-
	( map__search(WeightMap, TypeId - ConsId, WeightInfo) ->
		WeightInfo = weight(Int, UseArgList),
		(
			functor_norm_filter_args(UseArgList, Args0, Args1,
				Modes0, Modes1)
		->
			Modes = Modes1,
			Args = Args1
		;
			error("Unmatched lists in functor_norm_filter_args.")
		)
	;
		Int = 0,
		Modes = Modes0,
		Args = Args0
	).

% This predicate will fail if the length of the input lists are not matched.

:- pred functor_norm_filter_args(list(bool), list(var), list(var),
	list(uni_mode), list(uni_mode)).
:- mode functor_norm_filter_args(in, in, out, in, out) is semidet.

functor_norm_filter_args([], [], [], [], []).
functor_norm_filter_args([yes | Bools], [Arg0 | Args0], [Arg0 | Args],
		[Mode0 | Modes0], [Mode0 | Modes]) :-
	functor_norm_filter_args(Bools, Args0, Args, Modes0, Modes).
functor_norm_filter_args([no | Bools], [_Arg0 | Args0], Args,
		[_Mode0 | Modes0], Modes) :-
	functor_norm_filter_args(Bools, Args0, Args, Modes0, Modes).

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

partition_call_args(Module, ArgModes, Args, InVarsBag, OutVarsBag) :-
	partition_call_args_2(Module, ArgModes, Args, InVars, OutVars),
	bag__from_list(InVars, InVarsBag),
	bag__from_list(OutVars, OutVarsBag).

:- pred partition_call_args_2(module_info::in, list(mode)::in, list(var)::in,
	list(var)::out, list(var)::out) is det.

partition_call_args_2(_, [], [], [], []).
partition_call_args_2(_, [], [_ | _], _, _) :-
	error("Unmatched variables in term_util:partition_call_args").
partition_call_args_2(_, [_ | _], [], _, _) :-
	error("Unmatched variables in term_util__partition_call_args").
partition_call_args_2(ModuleInfo, [ArgMode | ArgModes], [Arg | Args],
		InputArgs, OutputArgs) :-
	partition_call_args_2(ModuleInfo, ArgModes, Args,
		InputArgs1, OutputArgs1),
	( mode_is_input(ModuleInfo, ArgMode) ->
		InputArgs = [Arg | InputArgs1],
		OutputArgs = OutputArgs1
	; mode_is_output(ModuleInfo, ArgMode) ->
		InputArgs = InputArgs1,
		OutputArgs = [Arg | OutputArgs1]
	;
		InputArgs = InputArgs1,
		OutputArgs = OutputArgs1
	).

% For these next two predicates (split_unification_vars and
% partition_call_args) there is a problem of what needs to be done for
% partially instantiated data structures.  The correct answer is that the
% system shoud use a norm such that the size of the uninstantiated parts of
% a partially instantiated structure have no effect on the size of the data
% structure according to the norm.  For example when finding the size of a
% list-skeleton, list-length norm should be used.  Therefore, the size of
% any term must be given by
% sizeof(term) = constant + sum of the size of each
% 			(possibly partly) instantiated subterm.
% It is probably easiest to implement this by modifying term_weights.
% The current implementation does not correctly handle partially
% instantiated data structures.

split_unification_vars([], Modes, _ModuleInfo, Vars, Vars) :-
	bag__init(Vars),
	( Modes = [] ->
		true
	;
		error("term_util:split_unification_vars: Unmatched Variables")
	).
split_unification_vars([Arg | Args], Modes, ModuleInfo,
		InVars, OutVars):-
	( Modes = [UniMode | UniModes] ->
		split_unification_vars(Args, UniModes, ModuleInfo,
			InVars0, OutVars0),
		UniMode = ((_VarInit - ArgInit) -> (_VarFinal - ArgFinal)),
		( % if
			inst_is_bound(ModuleInfo, ArgInit)
		->
			% Variable is an input variable
			bag__insert(InVars0, Arg, InVars),
			OutVars = OutVars0
		; % else if
			inst_is_free(ModuleInfo, ArgInit),
			inst_is_bound(ModuleInfo, ArgFinal)
		->
			% Variable is an output variable
			InVars = InVars0,
			bag__insert(OutVars0, Arg, OutVars)
		; % else
			InVars = InVars0,
			OutVars = OutVars0
		)
	;
		error("term_util__split_unification_vars: Unmatched Variables")
	).

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

term_util__make_bool_list(HeadVars0, Bools, Out) :-
	list__length(Bools, Arity),
	( list__drop(Arity, HeadVars0, HeadVars1) ->
		HeadVars = HeadVars1
	;
		error("Unmatched variables in term_util:make_bool_list")
	),
	term_util__make_bool_list_2(HeadVars, Bools, Out).

:- pred term_util__make_bool_list_2(list(_T), list(bool), list(bool)).
:- mode term_util__make_bool_list_2(in, in, out) is det.

term_util__make_bool_list_2([], Bools, Bools).
term_util__make_bool_list_2([ _ | Vars ], Bools, [no | Out]) :-
	term_util__make_bool_list_2(Vars, Bools, Out).

remove_unused_args(Vars, [], [], Vars).
remove_unused_args(Vars, [], [_X | _Xs], Vars) :-
	error("Unmatched variables in term_util:remove_unused_args").
remove_unused_args(Vars, [_X | _Xs], [], Vars) :-
	error("Unmatched variables in term_util__remove_unused_args").
remove_unused_args(Vars0, [ Arg | Args ], [ UsedVar | UsedVars ], Vars) :-
	( UsedVar = yes ->
		% The variable is used, so leave it
		remove_unused_args(Vars0, Args, UsedVars, Vars)
	;
		% The variable is not used in producing output vars, so
		% dont include it as an input variable.
		bag__delete(Vars0, Arg, Vars1),
		remove_unused_args(Vars1, Args, UsedVars, Vars)
	).

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

set_pred_proc_ids_arg_size_info([], _ArgSize, Module, Module).
set_pred_proc_ids_arg_size_info([PPId | PPIds], ArgSize, Module0, Module) :-
	PPId = proc(PredId, ProcId),
	module_info_preds(Module0, PredTable0),
	map__lookup(PredTable0, PredId, PredInfo0),
	pred_info_procedures(PredInfo0, ProcTable0),
	map__lookup(ProcTable0, ProcId, ProcInfo0),

	proc_info_set_maybe_arg_size_info(ProcInfo0, yes(ArgSize), ProcInfo),

	map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
	pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
	map__det_update(PredTable0, PredId, PredInfo, PredTable),
	module_info_set_preds(Module0, PredTable, Module1),
	set_pred_proc_ids_arg_size_info(PPIds, ArgSize, Module1, Module).

set_pred_proc_ids_termination_info([], _Termination, Module, Module).
set_pred_proc_ids_termination_info([PPId | PPIds], Termination,
		Module0, Module) :-
	PPId = proc(PredId, ProcId),
	module_info_preds(Module0, PredTable0),
	map__lookup(PredTable0, PredId, PredInfo0),
	pred_info_procedures(PredInfo0, ProcTable0),
	map__lookup(ProcTable0, ProcId, ProcInfo0),

	proc_info_set_maybe_termination_info(ProcInfo0, yes(Termination),
		ProcInfo),

	map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
	pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
	map__det_update(PredTable0, PredId, PredInfo, PredTable),
	module_info_set_preds(Module0, PredTable, Module1),
	set_pred_proc_ids_termination_info(PPIds, Termination,
		Module1, Module).

lookup_proc_termination_info(Module, PredProcId, MaybeTermination) :-
	PredProcId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	proc_info_get_maybe_termination_info(ProcInfo, MaybeTermination).

lookup_proc_arg_size_info(Module, PredProcId, MaybeArgSize) :-
	PredProcId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	proc_info_get_maybe_arg_size_info(ProcInfo, MaybeArgSize).

horder_vars([Arg | Args], VarType) :-
	(
		map__lookup(VarType, Arg, Type),
		type_is_higher_order(Type, _, _)
	;
		horder_vars(Args, VarType)
	).

zero_size_type(Type, Module) :-
	classify_type(Type, Module, TypeCategory),
	zero_size_type_category(TypeCategory, Type, Module, yes).

	% User_type could be a type_info, which should be called size 0.
	% This is not a big problem, as most type_infos are input.  

:- pred zero_size_type_category(builtin_type, type, module_info, bool).
:- mode zero_size_type_category(in, in, in, out) is det.

zero_size_type_category(int_type, _, _, yes).
zero_size_type_category(char_type, _, _, yes).
zero_size_type_category(str_type, _, _, yes).
zero_size_type_category(float_type, _, _, yes).
zero_size_type_category(pred_type, _, _, no).
zero_size_type_category(enum_type, _, _, yes).
zero_size_type_category(polymorphic_type, _, _, no).
zero_size_type_category(user_type, _, _, no).

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

get_context_from_scc(SCC, Module, Context) :-
	( SCC = [proc(PredId, _) | _] ->
		module_info_pred_info(Module, PredId, PredInfo),
		pred_info_context(PredInfo, Context)
	;
		error("Empty SCC in pass 2 of termination analysis")
	).

%-----------------------------------------------------------------------------%
%----------------------------------------------------------------------------%
% 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.
%----------------------------------------------------------------------------%
%
% termination.m
%
% Main author: crs.
% Significant modifications by zs.
%
% This termination analysis is based on the algorithm given by Gerhard Groeger
% and Lutz Plumer in their paper "Handling of Mutual Recursion in Automatic 
% Termination Proofs for Logic Programs"  which was printed in JICSLP '92
% (the proceedings of the Joint International Conference and Symposium on
% Logic Programming 1992) pages 336 - 350.  
%
% Details about this implementation are covered in:
% Chris Speirs, Zoltan Somogyi, and Harald Sondergaard. Termination
% analysis for Mercury. In P. Van Hentenryck, editor, Static Analysis:
% Proceedings of the 4th International Symposium, Lecture Notes in Computer
% Science. Springer, 1997.  A more detailed version is available for
% download from http://www.cs.mu.oz.au/publications/tr_db/mu_97_09.ps.gz
%
% Currently, this implementation assumes that all c_code terminates.
% It also fails to prove termination for any predicate that involves higher
% order calls.
%
% The termination analysis may use a number of different norms to calculate 
% the size of a term.  These are set by using the --termination-norm string
% option.  To add a new norm, the following files must be modified:
%
% globals.m 		To change the termination_norm type and
% 			convert_termination_norm predicate.
%
% handle_options.m 	To change the error message that is produced when
% 			an incorrect argument is given to --termination-norm.
%
% term_util.m		To change the functor_norm predicate and change the
% 			functor_alg type.
%
% termination.m		To change the set_functor_info predicate.
% 			
%----------------------------------------------------------------------------%

:- module termination.

:- interface.

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

	% Perform termination analysis on the module.

:- pred termination__pass(module_info::in, module_info::out,
	io__state::di, io__state::uo) is det.

	% Write the given arg size info; verbose if the second arg is yes.

:- pred termination__write_maybe_arg_size_info(maybe(arg_size_info)::in,
	bool::in, io__state::di, io__state::uo) is det.

	% Write the given termination info; verbose if the second arg is yes.

:- pred termination__write_maybe_termination_info(maybe(termination_info)::in,
	bool::in, io__state::di, io__state::uo) is det.

	% This predicate outputs termination_info pragmas;
	% such annotations can be part of .opt and .trans_opt files.

:- pred termination__write_pragma_termination_info(pred_or_func::in,
	sym_name::in, list(mode)::in, term__context::in,
	maybe(arg_size_info)::in, maybe(termination_info)::in,
	io__state::di, io__state::uo) is det.

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

:- implementation.

:- import_module term_pass1, term_pass2, term_errors.
:- import_module inst_match, passes_aux, options, globals, prog_data.
:- import_module hlds_data, hlds_pred, hlds_goal, dependency_graph.
:- import_module mode_util, hlds_out, code_util, prog_out.
:- import_module mercury_to_mercury, varset, type_util, special_pred.

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

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

termination__pass(Module0, Module) -->

		% Find out what norm we should use, and set up for using it
	globals__io_get_termination_norm(TermNorm),
	{ set_functor_info(TermNorm, Module0, FunctorInfo) },

		% Process builtin and compiler-generated predicates,
		% and user-supplied pragmas.
	{ module_info_predids(Module0, PredIds) },
	check_preds(PredIds, Module0, Module1),

		% Process all the SCCs of the call graph in a bottom up order.
	{ module_info_ensure_dependency_info(Module1, Module2) },
	{ module_info_dependency_info(Module2, DepInfo) },
	{ hlds_dependency_info_get_dependency_ordering(DepInfo, SCCs) },
	termination__process_all_sccs(SCCs, Module2, FunctorInfo, Module),

	globals__io_lookup_bool_option(make_optimization_interface,
		MakeOptInt),
	( { MakeOptInt = yes } ->
		termination__make_opt_int(PredIds, Module)
	;
		[]
	).

% This predicate sets the functor info depending on the value of the
% termination_norm option. The functor info field stores the weight which
% is associated with each functor, and may contain information about which
% subterms contribute to the size of that functor.

:- pred set_functor_info(globals__termination_norm, module_info, functor_info).
:- mode set_functor_info(in, in, out) is det.

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)) :-
	find_weights(Module, WeightMap).

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

:- pred termination__process_all_sccs(list(list(pred_proc_id)), module_info,
	functor_info, module_info, io__state, io__state).
:- mode termination__process_all_sccs(in, in, in, out, di, uo) is det.

termination__process_all_sccs([], Module, _, Module) --> [].
termination__process_all_sccs([SCC | SCCs], Module0, FunctorInfo, Module) -->
	termination__process_scc(SCC, Module0, FunctorInfo, Module1),
	termination__process_all_sccs(SCCs, Module1, FunctorInfo, Module).

	% For each SCC, we first find out the relationships among
	% the sizes of the arguments of the procedures of the SCC,
	% and then attempt to prove termination of the procedures.

:- pred termination__process_scc(list(pred_proc_id), module_info, functor_info,
	module_info, io__state, io__state).
:- mode termination__process_scc(in, in, in, out, di, uo) is det.

termination__process_scc(SCC, Module0, FunctorInfo, Module) -->
	{ IsArgSizeKnown = lambda([PPId::in] is semidet, (
		PPId = proc(PredId, ProcId),
		module_info_pred_proc_info(Module0, PredId, ProcId,
			_, ProcInfo),
		proc_info_get_maybe_arg_size_info(ProcInfo, yes(_))
	)) },
	{ list__filter(IsArgSizeKnown, SCC,
		_SCCArgSizeKnown, SCCArgSizeUnknown) },
	( { SCCArgSizeUnknown = [] } ->
		{ ArgSizeErrors = [] },
		{ TermErrors = [] },
		{ Module1 = Module0 }
	;
		find_arg_sizes_in_scc(SCCArgSizeUnknown, Module0, FunctorInfo,
			ArgSizeResult, TermErrors),
		{
			ArgSizeResult = ok(Solutions, OutputSupplierMap),
			set_finite_arg_size_infos(Solutions,
				OutputSupplierMap, Module0, Module1),
			ArgSizeErrors = []
		;
			ArgSizeResult = error(Errors),
			set_infinite_arg_size_infos(SCCArgSizeUnknown,
				infinite(Errors), Module0, Module1),
			ArgSizeErrors = Errors
		}
	),
	{ IsTerminationKnown = lambda([PPId::in] is semidet, (
		PPId = proc(PredId, ProcId),
		module_info_pred_proc_info(Module0, PredId, ProcId,
			_, ProcInfo),
		proc_info_get_maybe_arg_size_info(ProcInfo, yes(_))
	)) },
	{ list__filter(IsTerminationKnown, SCC,
		_SCCTerminationKnown, SCCTerminationUnknown) },
	( { SCCTerminationUnknown = [] } ->
		{ Module = Module1 }
	;
		{ IsFatal = lambda([ContextError::in] is semidet, (
			ContextError = _Context - Error,
			( Error = horder_call
			; Error = horder_args(_, _)
			; Error = imported_pred
			)
		)) },
		{ list__filter(IsFatal, ArgSizeErrors, FatalErrors) },
		{ list__append(TermErrors, FatalErrors, BothErrors) },
		( { BothErrors = [_ | _] } ->
			% These errors prevent pass 2 from proving termination
			% in any case, so we may as well not prove it quickly.
			{ list__take_upto(3, BothErrors, ReportedErrors) },
			{ TerminationResult = can_loop(ReportedErrors) }
		;
			globals__io_lookup_int_option(termination_single_args,
				SingleArgs),
			{ prove_termination_in_scc(SCCTerminationUnknown,
				Module1, FunctorInfo, SingleArgs,
				TerminationResult) }
		),
		{ set_termination_infos(SCCTerminationUnknown,
			TerminationResult, Module1, Module2) },
		( { TerminationResult = can_loop(TerminationErrors) } ->
			report_termination_errors(SCC, TerminationErrors,
				Module2, Module)
		;
			{ Module = Module2 }
		)
	).

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

% This predicate takes the results from solve_equations
% and inserts these results into the module info.

:- pred set_finite_arg_size_infos(list(pair(pred_proc_id, int))::in,
	used_args::in, module_info::in, module_info::out) is det.

set_finite_arg_size_infos([], _, Module, Module).
set_finite_arg_size_infos([Soln | Solns], OutputSupplierMap, Module0, Module) :-
	Soln = PPId - Gamma,
	PPId = proc(PredId, ProcId),
	module_info_preds(Module0, PredTable0),
	map__lookup(PredTable0, PredId, PredInfo),
	pred_info_procedures(PredInfo, ProcTable),
	map__lookup(ProcTable, ProcId, ProcInfo),
	map__lookup(OutputSupplierMap, PPId, OutputSuppliers),
	ArgSizeInfo = finite(Gamma, OutputSuppliers),
	proc_info_set_maybe_arg_size_info(ProcInfo, yes(ArgSizeInfo),
		ProcInfo1),
	map__set(ProcTable, ProcId, ProcInfo1, ProcTable1),
	pred_info_set_procedures(PredInfo, ProcTable1, PredInfo1),
	map__set(PredTable0, PredId, PredInfo1, PredTable),
	module_info_set_preds(Module0, PredTable, Module1),
	set_finite_arg_size_infos(Solns, OutputSupplierMap, Module1, Module).

:- pred set_infinite_arg_size_infos(list(pred_proc_id)::in,
	arg_size_info::in, module_info::in, module_info::out) is det.

set_infinite_arg_size_infos([], _, Module, Module).
set_infinite_arg_size_infos([PPId | PPIds], ArgSizeInfo, Module0, Module) :-
	PPId = proc(PredId, ProcId),
	module_info_preds(Module0, PredTable0),
	map__lookup(PredTable0, PredId, PredInfo),
	pred_info_procedures(PredInfo, ProcTable),
	map__lookup(ProcTable, ProcId, ProcInfo),
	proc_info_set_maybe_arg_size_info(ProcInfo, yes(ArgSizeInfo),
		ProcInfo1),
	map__set(ProcTable, ProcId, ProcInfo1, ProcTable1),
	pred_info_set_procedures(PredInfo, ProcTable1, PredInfo1),
	map__set(PredTable0, PredId, PredInfo1, PredTable),
	module_info_set_preds(Module0, PredTable, Module1),
	set_infinite_arg_size_infos(PPIds, ArgSizeInfo, Module1, Module).

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

:- pred set_termination_infos(list(pred_proc_id)::in, termination_info::in,
	module_info::in, module_info::out) is det.

set_termination_infos([], _, Module, Module).
set_termination_infos([PPId | PPIds], TerminationInfo, Module0, Module) :-
	PPId = proc(PredId, ProcId),
	module_info_preds(Module0, PredTable0),
	map__lookup(PredTable0, PredId, PredInfo0),
	pred_info_procedures(PredInfo0, ProcTable0),
	map__lookup(ProcTable0, ProcId, ProcInfo0),
	proc_info_set_maybe_termination_info(ProcInfo0, yes(TerminationInfo),
		ProcInfo),
	map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
	pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
	map__det_update(PredTable0, PredId, PredInfo, PredTable),
	module_info_set_preds(Module0, PredTable, Module1),
	set_termination_infos(PPIds, TerminationInfo, Module1, Module).

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

report_termination_errors(SCC, Errors, Module0, Module) -->
	globals__io_lookup_bool_option(check_termination,
		NormalErrors),
	globals__io_lookup_bool_option(verbose_check_termination,
		VerboseErrors),
	( 
		{ IsCheckTerm = lambda([PPId::in] is semidet, (
			PPId = proc(PredId, ProcId),
			module_info_pred_proc_info(Module0, PredId, ProcId,
				PredInfo, _),
			\+ pred_info_is_imported(PredInfo),
			pred_info_get_markers(PredInfo, Markers),
			check_marker(Markers, check_termination)
		)) },
		{ list__filter(IsCheckTerm, SCC, CheckTermPPIds) },
		{ CheckTermPPIds = [_ | _] }
	->
		% If any procedure in the SCC has a check_terminates pragma,
		% print out one error message for the whole SCC and indicate
		% an error.
		term_errors__report_term_errors(SCC, Errors, Module0),
		io__set_exit_status(1),
		{ module_info_incr_errors(Module0, Module) }
	;
		{ IsNonImported = lambda([PPId::in] is semidet, (
			PPId = proc(PredId, ProcId),
			module_info_pred_proc_info(Module0, PredId, ProcId,
				PredInfo, _),
			\+ pred_info_is_imported(PredInfo)
		)) },
		{ list__filter(IsNonImported, SCC, NonImportedPPIds) },
		{ NonImportedPPIds = [_ | _] },

		% Only output warnings of non-termination for
		% important errors, unless verbose errors are
		% enabled.  Important errors are errors where the
		% compiler analysed the code and was not able to
		% prove termination.  Unimportant warnings are
		% created when code is used/called which the
		% compiler was unable to analyse/prove termination
		% of.  
		{ VerboseErrors = yes ->
			PrintErrors = Errors
		; NormalErrors = yes ->
			IsNonSimple = lambda([ContextError::in] is semidet, (
				ContextError = _Context - Error,
				\+ simple_error(Error)
			)),
			list__filter(IsNonSimple, Errors, PrintErrors)
		;
			fail
		}
	->
		term_errors__report_term_errors(SCC, PrintErrors, Module0),
		{ Module = Module0 }
	;
		{ Module = Module0 }
	).

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

:- pred check_preds(list(pred_id), module_info, module_info, 
	io__state, io__state).
:- mode check_preds(in, in, out, di, uo) is det.

% This predicate processes each predicate and sets the termination property
% if possible.  This is done as follows:  Set the termination to yes if:
% - there is a terminates pragma defined for the predicate
% - there is a `check_termination' pragma defined for the predicate, and it
% 	is imported, and the compiler is not currently generating the
% 	intermodule optimization file.
% - the predicate is a builtin predicate or is compiler generated (This
% 	also sets the termination constant and UsedArgs).
%
% Set the termination to dont_know if:
% - there is a `does_not_terminate' pragma defined for this predicate.
% - the predicate is imported and there is no other source of information
% 	about it (termination_info pragmas, terminates pragmas,
% 	check_termination pragmas, builtin/compiler generated).

check_preds([], Module, Module, State, State).
check_preds([PredId | PredIds] , Module0, Module, State0, State) :-
	globals__io_lookup_bool_option(make_optimization_interface,
		MakeOptInt, State0, State1),
	module_info_preds(Module0, PredTable0),
	map__lookup(PredTable0, PredId, PredInfo0),
	pred_info_import_status(PredInfo0, ImportStatus),
	pred_info_context(PredInfo0, Context),
	pred_info_procedures(PredInfo0, ProcTable0),
	pred_info_get_markers(PredInfo0, Markers),
	map__keys(ProcTable0, ProcIds),
	( 
		% It is possible for compiler generated/mercury builtin
		% predicates to be imported or locally defined, so they
		% must be covered here, separately.
		set_compiler_gen_terminates(PredInfo0, ProcIds, PredId,
			Module0, ProcTable0, ProcTable1)
	->
		ProcTable2 = ProcTable1
	;
		( ImportStatus = exported
		; ImportStatus = local
		; ImportStatus = pseudo_exported
		)
	->
		( check_marker(Markers, terminates) ->
			change_procs_termination_info(ProcIds, yes,
				cannot_loop, ProcTable0, ProcTable2)
		;
			ProcTable2 = ProcTable0
		)
	;
		( ImportStatus = imported
		; ImportStatus = opt_imported
		; ImportStatus = pseudo_imported  % should this be here?
		)
	->
		% All of the predicates that are processed in this section
		% are imported in some way.
		% With imported predicates, any 'check_termination'
		% pragmas will be checked by the compiler when it compiles
		% the relevant source file (that the predicate was imported
		% from).  When making the intermodule optimizations, the 
		% check_termination will not be checked when the relevant
		% source file is compiled, so it cannot be depended upon. 
		(
			(
				check_marker(Markers, terminates)
			; 
				MakeOptInt = no,
				check_marker(Markers, check_termination)
			)
		->
			change_procs_termination_info(ProcIds, yes,
				cannot_loop, ProcTable0, ProcTable1)
		;
			TerminationError = Context - imported_pred,
			TerminationInfo = can_loop([TerminationError]),
			change_procs_termination_info(ProcIds, no,
				TerminationInfo, ProcTable0, ProcTable1)
		),
		ArgSizeError = imported_pred,
		ArgSizeInfo = infinite([Context - ArgSizeError]),
		change_procs_arg_size_info(ProcIds, no, ArgSizeInfo,
			ProcTable1, ProcTable2)
	;
%		( ImportStatus = abstract_imported
%		; ImportStatus = abstract_exported
%		),
		% This should not happen, as procedures are being processed
		% here, and these import_status' refer to abstract types.
		error("termination__check_preds: Unexpected import status")
	),
	( check_marker(Markers, does_not_terminate) ->
		RequestError = Context - does_not_term_pragma(PredId),
		RequestTerminationInfo = can_loop([RequestError]),
		change_procs_termination_info(ProcIds, yes,
			RequestTerminationInfo, ProcTable2, ProcTable)
	;
		ProcTable = ProcTable2
	),
	pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
	map__set(PredTable0, PredId, PredInfo, PredTable),
	module_info_set_preds(Module0, PredTable, Module1),
	check_preds(PredIds, Module1, Module, State1, State).

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

% This predicate checks each ProcId in the list to see if it is a compiler
% generated predicate, or a mercury_builtin predicate.  If it is, then the
% compiler sets the termination property of the ProcIds accordingly.

:- pred set_compiler_gen_terminates(pred_info, list(proc_id), pred_id,
	module_info, proc_table, proc_table).
:- mode set_compiler_gen_terminates(in, in, in, in, in, out) is semidet.

set_compiler_gen_terminates(PredInfo, ProcIds, PredId, Module,
		ProcTable0, ProcTable) :-
	(
		code_util__predinfo_is_builtin(PredInfo)
	->
		set_builtin_terminates(ProcIds, PredId, PredInfo, Module,
			ProcTable0, ProcTable)
	;
		pred_info_name(PredInfo, Name),
		pred_info_arity(PredInfo, Arity),
		(
			special_pred_name_arity(SpecPredId0, Name, _, Arity),
			pred_info_module(PredInfo, ModuleName),
			ModuleName = "mercury_builtin"
		->
			SpecialPredId = SpecPredId0
		;
			special_pred_name_arity(SpecialPredId, _, Name, Arity)
		)
	->
		set_generated_terminates(ProcIds, SpecialPredId,
			ProcTable0, ProcTable)
	;
		fail
	).

:- pred set_generated_terminates(list(proc_id), special_pred_id,
	proc_table, proc_table).
:- mode set_generated_terminates(in, in, in, out) is det.

set_generated_terminates([], _, ProcTable, ProcTable).
set_generated_terminates([ProcId | ProcIds], SpecialPredId,
		ProcTable0, ProcTable) :-
	map__lookup(ProcTable0, ProcId, ProcInfo0),
	proc_info_headvars(ProcInfo0, HeadVars),
	special_pred_id_to_termination(SpecialPredId, HeadVars,
		ArgSize, Termination),
	proc_info_set_maybe_arg_size_info(ProcInfo0, yes(ArgSize), ProcInfo1),
	proc_info_set_maybe_termination_info(ProcInfo1, yes(Termination),
		ProcInfo),
	map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1),
	set_generated_terminates(ProcIds, SpecialPredId,
		ProcTable1, ProcTable).

:- pred special_pred_id_to_termination(special_pred_id::in, 
	list(var)::in, arg_size_info::out, termination_info::out) is det.

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

% The list of proc_ids must refer to builtin predicates.  This predicate
% sets the termination information of builtin predicates.

:- pred set_builtin_terminates(list(proc_id), pred_id, pred_info, module_info, 
	proc_table, proc_table).
:- mode set_builtin_terminates(in, in, in, in, in, out) is det.

set_builtin_terminates([], _, _, _, ProcTable, ProcTable).
set_builtin_terminates([ProcId | ProcIds], PredId, PredInfo, Module,
		ProcTable0, ProcTable) :-
	map__lookup(ProcTable0, ProcId, ProcInfo0), 
	( all_args_input_or_zero_size(Module, PredInfo, ProcInfo0) ->
		% The size of the output arguments will all be 0,
		% independent of the size of the input variables.
		% UsedArgs should be set to yes([no, no, ...]).
		proc_info_headvars(ProcInfo0, HeadVars),
		term_util__make_bool_list(HeadVars, [], UsedArgs),
		ArgSizeInfo = yes(finite(0, UsedArgs))
	;
		pred_info_context(PredInfo, Context),
		Error = is_builtin(PredId),
		ArgSizeInfo = yes(infinite([Context - Error]))
	),
	proc_info_set_maybe_arg_size_info(ProcInfo0, ArgSizeInfo, ProcInfo1),
	proc_info_set_maybe_termination_info(ProcInfo1, yes(cannot_loop),
		ProcInfo),
	map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1),
	set_builtin_terminates(ProcIds, PredId, PredInfo, Module,
		ProcTable1, ProcTable).

:- pred all_args_input_or_zero_size(module_info, pred_info, proc_info).
:- mode all_args_input_or_zero_size(in, in, in) is semidet.

all_args_input_or_zero_size(Module, PredInfo, ProcInfo) :-
	pred_info_arg_types(PredInfo, _, TypeList),
	proc_info_argmodes(ProcInfo, ModeList),
	all_args_input_or_zero_size_2(TypeList, ModeList, Module). 

:- pred all_args_input_or_zero_size_2(list(type), list(mode), module_info).
:- mode all_args_input_or_zero_size_2(in, in, in) is semidet.

all_args_input_or_zero_size_2([], [], _).
all_args_input_or_zero_size_2([], [_|_], _) :- 
	error("all_args_input_or_zero_size_2: Unmatched variables.").
all_args_input_or_zero_size_2([_|_], [], _) :- 
	error("all_args_input_or_zero_size_2: Unmatched variables").
all_args_input_or_zero_size_2([Type | Types], [Mode | Modes], Module) :-
	( mode_is_input(Module, Mode) ->
		% The variable is an input variables, so its size is
		% irrelevant.
		all_args_input_or_zero_size_2(Types, Modes, Module)
	;
		zero_size_type(Type, Module),
		all_args_input_or_zero_size_2(Types, Modes, Module)
	).

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

% This predicate sets the arg_size_info property of the given list
% of procedures.
%
% change_procs_arg_size_info(ProcList, Override, TerminationInfo,
% 		ProcTable, ProcTable)
%
% 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_arg_size_info(list(proc_id)::in, bool::in,
	arg_size_info::in, proc_table::in, proc_table::out) is det.

change_procs_arg_size_info([], _, _, ProcTable, ProcTable).
change_procs_arg_size_info([ProcId | ProcIds], Override, ArgSize,
		ProcTable0, ProcTable) :-
	map__lookup(ProcTable0, ProcId, ProcInfo0),
	( 
		( 
			Override = yes
		;
			proc_info_get_maybe_arg_size_info(ProcInfo0, no)
		)
	->
		proc_info_set_maybe_arg_size_info(ProcInfo0,
			yes(ArgSize), ProcInfo),
		map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1)
	;
		ProcTable1 = ProcTable0
	),
	change_procs_arg_size_info(ProcIds, Override, ArgSize,
		ProcTable1, ProcTable).

% This predicate sets the termination_info property of the given list
% of procedures.
%
% change_procs_termination_info(ProcList, Override, TerminationInfo,
% 		ProcTable, ProcTable)
%
% 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_termination_info(list(proc_id)::in, bool::in,
	termination_info::in, proc_table::in, proc_table::out) is det.

change_procs_termination_info([], _, _, ProcTable, ProcTable).
change_procs_termination_info([ProcId | ProcIds], Override, Termination,
		ProcTable0, ProcTable) :-
	map__lookup(ProcTable0, ProcId, ProcInfo0),
	( 
		( 
			Override = yes
		;
			proc_info_get_maybe_termination_info(ProcInfo0, no)
		)
	->
		proc_info_set_maybe_termination_info(ProcInfo0,
			yes(Termination), ProcInfo),
		map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1)
	;
		ProcTable1 = ProcTable0
	),
	change_procs_termination_info(ProcIds, Override, Termination,
		ProcTable1, ProcTable).

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

% These predicates are used to add the termination_info pragmas to the .opt
% file.  It is oftern better to use the .trans_opt file, as it gives
% much better accuracy.  The two files are not mutually exclusive, and
% termination information may be stored in both.

:- pred termination__make_opt_int(list(pred_id), module_info, io__state, 
		io__state).
:- mode termination__make_opt_int(in, in, di, uo) is det.

termination__make_opt_int(PredIds, Module) -->
	{ module_info_name(Module, ModuleName) },
	{ string__append(ModuleName, ".opt.tmp", OptFileName) },
	io__open_append(OptFileName, OptFileRes),
	( { OptFileRes = ok(OptFile) } ->
		io__set_output_stream(OptFile, OldStream),
		termination__make_opt_int_preds(PredIds, Module),
		io__set_output_stream(OldStream, _),
		io__close_output(OptFile)
	;
		% failed to open the .opt file for processing
		io__write_strings(["Cannot open `",
			OptFileName, "' for output\n"]),
		io__set_exit_status(1)
	).

:- pred termination__make_opt_int_preds(list(pred_id), module_info, 
	io__state, io__state).
:- mode termination__make_opt_int_preds(in, in, di, uo) is det.

termination__make_opt_int_preds([], _Module) --> [].
termination__make_opt_int_preds([ PredId | PredIds ], Module) -->
	{ module_info_preds(Module, PredTable) },
	{ map__lookup(PredTable, PredId, PredInfo) },
	{ pred_info_import_status(PredInfo, ImportStatus) },
	( 
		{ ImportStatus = exported },
		{ \+ code_util__compiler_generated(PredInfo) }
	->
		{ pred_info_name(PredInfo, PredName) },
		{ pred_info_procedures(PredInfo, ProcTable) },
		{ pred_info_procids(PredInfo, ProcIds) },
		{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
		{ pred_info_module(PredInfo, ModuleName) },
		{ pred_info_context(PredInfo, Context) },
		{ SymName = qualified(ModuleName, PredName) },
		termination__make_opt_int_procs(PredId, ProcIds, ProcTable, 
			PredOrFunc, SymName, Context)
	;
		[]
	),
	termination__make_opt_int_preds(PredIds, Module).

:- pred termination__make_opt_int_procs(pred_id, list(proc_id), proc_table,
	pred_or_func, sym_name, term__context, io__state, io__state).
:- mode termination__make_opt_int_procs(in, in, in, in, in, in, di, uo) is det.

termination__make_opt_int_procs(_PredId, [], _, _, _, _) --> [].
termination__make_opt_int_procs(PredId, [ ProcId | ProcIds ], ProcTable, 
		PredOrFunc, SymName, Context) -->
	{ map__lookup(ProcTable, ProcId, ProcInfo) },
	{ proc_info_get_maybe_arg_size_info(ProcInfo, ArgSize) },
	{ proc_info_get_maybe_termination_info(ProcInfo, Termination) },
	{ proc_info_declared_argmodes(ProcInfo, ModeList) },
	termination__write_pragma_termination_info(PredOrFunc, SymName,
		ModeList, Context, ArgSize, Termination),
	termination__make_opt_int_procs(PredId, ProcIds, ProcTable, 
		PredOrFunc, SymName, Context).

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

% These predicates are used to print out the termination_info pragmas.
% If they are changed, then prog_io_pragma.m must also be changed so that
% it can parse the resulting pragma termination_info declarations.

termination__write_pragma_termination_info(PredOrFunc, SymName,
		ModeList, Context, MaybeArgSize, MaybeTermination) -->
	io__write_string(":- pragma termination_info("),
	{ varset__init(InitVarSet) },
	( 
		{ PredOrFunc = predicate },
		mercury_output_pred_mode_subdecl(InitVarSet, SymName, 
			ModeList, no, Context)
	;
		{ PredOrFunc = function },
		{ pred_args_to_func_args(ModeList, FuncModeList, RetMode) },
		mercury_output_func_mode_subdecl(InitVarSet, SymName, 
			FuncModeList, RetMode, no, Context)
	),
	io__write_string(", "),
	termination__write_maybe_arg_size_info(MaybeArgSize, no),
	io__write_string(", "),
	termination__write_maybe_termination_info(MaybeTermination, no),
	io__write_string(").\n").

termination__write_maybe_arg_size_info(MaybeArgSizeInfo, Verbose) -->
	( 	
		{ MaybeArgSizeInfo = no },
		io__write_string("not_set") 
	;
		{ MaybeArgSizeInfo = yes(infinite(Error)) },
		io__write_string("infinite"),
		( { Verbose = yes } ->
			io__write_string("("),
			io__write(Error),
			io__write_string(")")
		;
			[]
		)
	;
		{ MaybeArgSizeInfo = yes(finite(Const, UsedArgs)) },
		io__write_string("finite("),
		io__write_int(Const),
		io__write_string(", "),
		termination__write_used_args(UsedArgs),
		io__write_string(")")
	).

:- pred termination__write_used_args(list(bool)::in,
	io__state::di, io__state::uo) is det.

termination__write_used_args([]) -->
	io__write_string("[]").
termination__write_used_args([UsedArg | UsedArgs]) -->
	io__write_string("["),
	io__write(UsedArg),
	termination__write_used_args_2(UsedArgs),
	io__write_string("]").

:- pred termination__write_used_args_2(list(bool)::in,
	io__state::di, io__state::uo) is det.

termination__write_used_args_2([]) --> [].
termination__write_used_args_2([ UsedArg | UsedArgs ]) -->
	io__write_string(", "),
	io__write(UsedArg),
	termination__write_used_args_2(UsedArgs).

termination__write_maybe_termination_info(MaybeTerminationInfo, Verbose) -->
	( 	
		{ MaybeTerminationInfo = no },
		io__write_string("not_set") 
	;
		{ MaybeTerminationInfo = yes(cannot_loop) },
		io__write_string("cannot_loop")
	;
		{ MaybeTerminationInfo = yes(can_loop(Error)) },
		io__write_string("can_loop"),
		( { Verbose = yes } ->
			io__write_string("("),
			io__write(Error),
			io__write_string(")")
		;
			[]
		)
	).
Index: compiler/bytecode_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/bytecode_gen.m,v
retrieving revision 1.30
diff -u -r1.30 bytecode_gen.m
--- bytecode_gen.m	1997/09/01 14:00:22	1.30
+++ bytecode_gen.m	1997/11/15 02:24:40
@@ -89,7 +89,7 @@
 
 	proc_info_goal(ProcInfo, Goal),
 	proc_info_vartypes(ProcInfo, VarTypes),
-	proc_info_variables(ProcInfo, VarSet),
+	proc_info_varset(ProcInfo, VarSet),
 	proc_info_interface_determinism(ProcInfo, Detism),
 	determinism_to_code_model(Detism, CodeModel),
 
Index: compiler/code_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/code_gen.m,v
retrieving revision 1.39
diff -u -r1.39 code_gen.m
--- code_gen.m	1997/11/08 13:11:09	1.39
+++ code_gen.m	1997/11/15 02:24:53
@@ -180,7 +180,7 @@
 		% get the goal for this procedure
 	proc_info_goal(ProcInfo, Goal),
 		% get the information about this procedure that we need.
-	proc_info_variables(ProcInfo, VarInfo),
+	proc_info_varset(ProcInfo, VarInfo),
 	proc_info_liveness_info(ProcInfo, Liveness),
 	proc_info_stack_slots(ProcInfo, StackSlots),
 	proc_info_get_initial_instmap(ProcInfo, ModuleInfo, InitialInst),
Index: compiler/constraint.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/constraint.m,v
retrieving revision 1.35
diff -u -r1.35 constraint.m
--- constraint.m	1997/09/01 14:00:47	1.35
+++ constraint.m	1997/11/15 02:25:06
@@ -88,7 +88,7 @@
 	map__lookup(ProcTable0, ProcId, ProcInfo0),
 
 	proc_info_goal(ProcInfo0, Goal0),
-	proc_info_variables(ProcInfo0, VarSet0),
+	proc_info_varset(ProcInfo0, VarSet0),
 	varset__vars(VarSet0, VarList),
 	set__list_to_set(VarList, VarSet1),
 
@@ -104,7 +104,7 @@
 	mode_info_get_var_types(ModeInfo, VarTypes),
 	mode_info_get_module_info(ModeInfo, ModuleInfo1),
 
-	proc_info_set_variables(ProcInfo0, VarSet, ProcInfo1),
+	proc_info_set_varset(ProcInfo0, VarSet, ProcInfo1),
 	proc_info_set_vartypes(ProcInfo1, VarTypes, ProcInfo2),
 	proc_info_set_goal(ProcInfo2, Goal, ProcInfo),
 
Index: compiler/cse_detection.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/cse_detection.m,v
retrieving revision 1.48
diff -u -r1.48 cse_detection.m
--- cse_detection.m	1997/09/01 14:00:51	1.48
+++ cse_detection.m	1997/11/15 02:25:16
@@ -135,7 +135,7 @@
 
 	proc_info_goal(ProcInfo0, Goal0),
 	proc_info_get_initial_instmap(ProcInfo0, ModuleInfo0, InstMap0),
-	proc_info_variables(ProcInfo0, Varset0),
+	proc_info_varset(ProcInfo0, Varset0),
 	proc_info_vartypes(ProcInfo0, VarTypes0),
 	CseInfo0 = cse_info(Varset0, VarTypes0, ModuleInfo0),
 	detect_cse_in_goal(Goal0, InstMap0, CseInfo0, CseInfo, Redo, Goal1),
@@ -154,7 +154,7 @@
 			VarTypes1, Goal, Varset, VarTypes, _Warnings),
 
 		proc_info_set_goal(ProcInfo0, Goal, ProcInfo1),
-		proc_info_set_variables(ProcInfo1, Varset, ProcInfo2),
+		proc_info_set_varset(ProcInfo1, Varset, ProcInfo2),
 		proc_info_set_vartypes(ProcInfo2, VarTypes, ProcInfo),
 
 		map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
Index: compiler/det_analysis.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/det_analysis.m,v
retrieving revision 1.124
diff -u -r1.124 det_analysis.m
--- det_analysis.m	1997/11/17 05:47:30	1.124
+++ det_analysis.m	1997/11/19 01:29:36
@@ -747,11 +747,11 @@
 			_TypeContext)
 	->
 		( CanFail = can_fail ->
-			proc_info_variables(ProcInfo, VarSet),
+			proc_info_varset(ProcInfo, VarSet),
 			Msgs = [cc_unify_can_fail(GoalInfo, Var, Type,
 				VarSet, GoalContext) | Msgs0]
 		; SolnContext \= first_soln ->
-			proc_info_variables(ProcInfo, VarSet),
+			proc_info_varset(ProcInfo, VarSet),
 			Msgs = [cc_unify_in_wrong_context(GoalInfo, Var,
 				Type, VarSet, GoalContext) | Msgs0]
 		;
Index: compiler/det_report.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/det_report.m,v
retrieving revision 1.43
diff -u -r1.43 det_report.m
--- det_report.m	1997/11/17 05:47:33	1.43
+++ det_report.m	1997/11/19 01:22:15
@@ -419,7 +419,7 @@
 			DetInfo),
 		prog_out__write_context(Context),
 		{ det_get_proc_info(DetInfo, ProcInfo) },
-		{ proc_info_variables(ProcInfo, Varset) },
+		{ proc_info_varset(ProcInfo, Varset) },
 		{ det_info_get_module_info(DetInfo, ModuleInfo) },
 		(
 			{ det_lookup_var_type(ModuleInfo, ProcInfo, Var,
@@ -700,7 +700,7 @@
 		DetInfo) -->
 	prog_out__write_context(Context),
 	{ det_get_proc_info(DetInfo, ProcInfo) },
-	{ proc_info_variables(ProcInfo, Varset) },
+	{ proc_info_varset(ProcInfo, Varset) },
 	{ SwitchContext = switch_context(Var, ConsId) },
 	io__write_string("  Inside the case "),
 	hlds_out__write_cons_id(ConsId),
@@ -780,7 +780,7 @@
 	hlds_out__write_unify_context(First0, UnifyContext, Context, First),
 	prog_out__write_context(Context),
 	{ det_get_proc_info(DetInfo, ProcInfo) },
-	{ proc_info_variables(ProcInfo, Varset) },
+	{ proc_info_varset(ProcInfo, Varset) },
 	{ det_info_get_module_info(DetInfo, ModuleInfo) },
 	( { First = yes } ->
 		( { Last = yes } ->
Index: compiler/dnf.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dnf.m,v
retrieving revision 1.24
diff -u -r1.24 dnf.m
--- dnf.m	1997/11/24 07:26:38	1.24
+++ dnf.m	1997/11/25 07:32:54
@@ -138,7 +138,7 @@
 	pred_info_typevarset(PredInfo0, TVarSet),
 	pred_info_get_markers(PredInfo0, Markers),
 	proc_info_goal(ProcInfo0, Goal0),
-	proc_info_variables(ProcInfo0, VarSet),
+	proc_info_varset(ProcInfo0, VarSet),
 	proc_info_vartypes(ProcInfo0, VarTypes),
 	DnfInfo = dnf_info(TVarSet, VarTypes, VarSet, Markers),
 
Index: compiler/excess.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/excess.m,v
retrieving revision 1.24
diff -u -r1.24 excess.m
--- excess.m	1997/09/01 14:01:24	1.24
+++ excess.m	1997/11/15 02:26:10
@@ -53,7 +53,7 @@
 	proc_info_set_goal(ProcInfo0, Goal, ProcInfo1),
 
 	% XXX We probably ought to remove these vars from the type map as well.
-	proc_info_variables(ProcInfo1, Varset0),
+	proc_info_varset(ProcInfo1, Varset0),
 	varset__delete_vars(Varset0, ElimVars, Varset),
 	proc_info_set_varset(ProcInfo1, Varset, ProcInfo).
 
Index: compiler/follow_code.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/follow_code.m,v
retrieving revision 1.43
diff -u -r1.43 follow_code.m
--- follow_code.m	1997/09/01 14:01:28	1.43
+++ follow_code.m	1997/11/15 02:26:22
@@ -43,7 +43,7 @@
 	globals__lookup_bool_option(Globals, prev_code, PrevCode),
 	Flags = FollowCode - PrevCode,
 	proc_info_goal(ProcInfo0, Goal0),
-	proc_info_variables(ProcInfo0, Varset0),
+	proc_info_varset(ProcInfo0, Varset0),
 	proc_info_vartypes(ProcInfo0, VarTypes0),
 	(
 		move_follow_code_in_goal(Goal0, Goal1, Flags, no, Res),
Index: compiler/higher_order.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/higher_order.m,v
retrieving revision 1.34
diff -u -r1.34 higher_order.m
--- higher_order.m	1997/11/24 07:26:40	1.34
+++ higher_order.m	1997/11/25 07:32:59
@@ -251,11 +251,11 @@
 	traverse_goal(Goal0, Goal1, proc(PredId, ProcId), _, _,
 					Info0, info(_, Requests1,_,_)),
 	proc_info_headvars(ProcInfo0, HeadVars),
-	proc_info_variables(ProcInfo0, Varset0),
+	proc_info_varset(ProcInfo0, Varset0),
 	implicitly_quantify_clause_body(HeadVars, Goal1, Varset0, VarTypes0,
 						Goal, Varset, VarTypes, _),
 	proc_info_set_goal(ProcInfo0, Goal, ProcInfo1),
-	proc_info_set_variables(ProcInfo1, Varset, ProcInfo2),
+	proc_info_set_varset(ProcInfo1, Varset, ProcInfo2),
 	proc_info_set_vartypes(ProcInfo2, VarTypes, ProcInfo),
 	map__det_update(Procs0, ProcId, ProcInfo, Procs1),
 	traverse_other_procs(PredId, ProcIds, ModuleInfo, Requests1,
@@ -927,13 +927,13 @@
 	set__init(Requests0),
 	traverse_goal(Goal0, Goal1, PredProcId, _, _,
 		info(PredVars0, Requests0, NewPreds, ModuleInfo0), _),
-	proc_info_variables(ProcInfo0, Varset0),
+	proc_info_varset(ProcInfo0, Varset0),
 	proc_info_headvars(ProcInfo0, HeadVars),
 	proc_info_vartypes(ProcInfo0, VarTypes0),
 	implicitly_quantify_clause_body(HeadVars, Goal1, Varset0, VarTypes0,
 					Goal, Varset, VarTypes, _),
 	proc_info_set_goal(ProcInfo0, Goal, ProcInfo1),
-	proc_info_set_variables(ProcInfo1, Varset, ProcInfo2),
+	proc_info_set_varset(ProcInfo1, Varset, ProcInfo2),
 	proc_info_set_vartypes(ProcInfo2, VarTypes, ProcInfo),
 	map__det_update(Procs0, ProcId, ProcInfo, Procs),
 	pred_info_set_procedures(PredInfo0, Procs, PredInfo),
@@ -1016,7 +1016,7 @@
 			info(PredVars0, Requests0, NewPredMap, ModuleInfo0),
 			info(_, Requests1,_,_)),
 	map__set(GoalSizes0, NewPredId, GoalSize, GoalSizes1),
-	proc_info_variables(NewProcInfo1, Varset0),
+	proc_info_varset(NewProcInfo1, Varset0),
 					
 	implicitly_quantify_clause_body(HeadVars, Goal2, Varset0, VarTypes1,
 					Goal3, Varset, VarTypes, _),
@@ -1024,7 +1024,7 @@
 	recompute_instmap_delta(no, Goal3, Goal4, InstMap0,
 		ModuleInfo0, ModuleInfo1),
 	proc_info_set_goal(NewProcInfo1, Goal4, NewProcInfo1a),
-	proc_info_set_variables(NewProcInfo1a, Varset, NewProcInfo2),
+	proc_info_set_varset(NewProcInfo1a, Varset, NewProcInfo2),
 	proc_info_set_vartypes(NewProcInfo2, VarTypes, NewProcInfo3),
 	proc_info_set_argmodes(NewProcInfo3, ArgModes, NewProcInfo4),
 	proc_info_set_headvars(NewProcInfo4, HeadVars, NewProcInfo),
@@ -1083,9 +1083,9 @@
 	;
 		error("list__split_list_failed")
 	),
-	proc_info_variables(ProcInfo0, Varset0),
+	proc_info_varset(ProcInfo0, Varset0),
 	varset__new_vars(Varset0, NumArgs, NewHeadVars0, Varset1),
-	proc_info_set_variables(ProcInfo0, Varset1, ProcInfo1),
+	proc_info_set_varset(ProcInfo0, Varset1, ProcInfo1),
 
 	% Find the type substitution and work out the types
 	% of the new variables.
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.175
diff -u -r1.175 hlds_out.m
--- hlds_out.m	1997/11/24 07:26:42	1.175
+++ hlds_out.m	1997/11/25 07:34:19
@@ -1856,12 +1856,13 @@
 	{ proc_info_vartypes(Proc, VarTypes) },
 	{ proc_info_declared_determinism(Proc, DeclaredDeterminism) },
 	{ proc_info_inferred_determinism(Proc, InferredDeterminism) },
-	{ proc_info_variables(Proc, VarSet) },
+	{ proc_info_varset(Proc, VarSet) },
 	{ proc_info_headvars(Proc, HeadVars) },
 	{ proc_info_argmodes(Proc, HeadModes) },
 	{ proc_info_goal(Proc, Goal) },
 	{ proc_info_context(Proc, ModeContext) },
-	{ proc_info_termination(Proc, Termination) },
+	{ proc_info_get_maybe_arg_size_info(Proc, MaybeArgSize) },
+	{ proc_info_get_maybe_termination_info(Proc, MaybeTermination) },
 	{ proc_info_typeinfo_varmap(Proc, TypeInfoMap) },
 	{ Indent1 is Indent + 1 },
 
@@ -1879,13 +1880,13 @@
 	
 	globals__io_lookup_string_option(verbose_dump_hlds, Verbose),
 	( { string__contains_char(Verbose, 't') } ->
-		io__write_string("% Inferred termination: "),
-		termination__out(Termination),
+		io__write_string("% Arg size properties: "),
+		termination__write_maybe_arg_size_info(MaybeArgSize, yes),
 		io__nl,
-		io__write_string("% Termination - used args: "),
-		termination__out_used_args(Termination),
-		io__nl,
-		term_errors__output_hlds(PredId, ProcId, ModuleInfo)
+		io__write_string("% Termination properties: "),
+		termination__write_maybe_termination_info(MaybeTermination,
+			yes),
+		io__nl
 	;
 		[]
 	),
Index: compiler/hlds_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
retrieving revision 1.38
diff -u -r1.38 hlds_pred.m
--- hlds_pred.m	1997/11/24 07:26:44	1.38
+++ hlds_pred.m	1997/11/25 07:33:01
@@ -458,7 +458,7 @@
 	next_mode_id(Procs0, MaybeDetism, ProcId),
 	map__det_insert(Procs0, ProcId, ProcInfo, Procs),
 	list__length(Types, Arity),
-	proc_info_variables(ProcInfo, VarSet),
+	proc_info_varset(ProcInfo, VarSet),
 	proc_info_vartypes(ProcInfo, VarTypes),
 	proc_info_headvars(ProcInfo, HeadVars),
 	unqualify_name(SymName, PredName),
@@ -667,9 +667,10 @@
 :- pred proc_info_set(maybe(determinism), varset, map(var, type), list(var),
 	list(mode), maybe(list(is_live)), hlds_goal, term__context,
 	stack_slots, determinism, bool, list(arg_info), liveness_info,
-	map(tvar, var), termination, proc_info).
+	map(tvar, var), maybe(arg_size_info), maybe(termination_info),
+	proc_info).
 :- mode proc_info_set(in, in, in, in, in, in, in, in, in, in, in, in, in, in,
-	in, out) is det.
+	in, in, out) is det.
 
 :- pred proc_info_create(varset, map(var, type), list(var), list(mode),
 	determinism, hlds_goal, term__context, map(tvar, var), proc_info).
@@ -697,15 +698,12 @@
 :- pred proc_info_never_succeeds(proc_info, bool).
 :- mode proc_info_never_succeeds(in, out) is det.
 
-:- pred proc_info_variables(proc_info, varset).
-:- mode proc_info_variables(in, out) is det.
+:- pred proc_info_varset(proc_info, varset).
+:- mode proc_info_varset(in, out) is det.
 
 :- pred proc_info_set_varset(proc_info, varset, proc_info).
 :- mode proc_info_set_varset(in, in, out) is det.
 
-:- pred proc_info_set_variables(proc_info, varset, proc_info).
-:- mode proc_info_set_variables(in, in, out) is det.
-
 :- pred proc_info_vartypes(proc_info, map(var, type)).
 :- mode proc_info_vartypes(in, out) is det.
 
@@ -770,11 +768,20 @@
 :- pred proc_info_set_stack_slots(proc_info, stack_slots, proc_info).
 :- mode proc_info_set_stack_slots(in, in, out) is det.
 
-:- pred proc_info_termination(proc_info, termination).
-:- mode proc_info_termination(in, out) is det.
+:- pred proc_info_get_maybe_arg_size_info(proc_info, maybe(arg_size_info)).
+:- mode proc_info_get_maybe_arg_size_info(in, out) is det.
 
-:- pred proc_info_set_termination(proc_info, termination, proc_info).
-:- mode proc_info_set_termination(in, in, out) is det.
+:- pred proc_info_set_maybe_arg_size_info(proc_info, maybe(arg_size_info),
+	proc_info).
+:- mode proc_info_set_maybe_arg_size_info(in, in, out) is det.
+
+:- pred proc_info_get_maybe_termination_info(proc_info,
+	maybe(termination_info)).
+:- mode proc_info_get_maybe_termination_info(in, out) is det.
+
+:- pred proc_info_set_maybe_termination_info(proc_info,
+	maybe(termination_info), proc_info).
+:- mode proc_info_set_maybe_termination_info(in, in, out) is det.
 
 :- pred proc_info_set_can_process(proc_info, bool, proc_info).
 :- mode proc_info_set_can_process(in, in, out) is det.
@@ -849,9 +856,15 @@
 					% for code generation
 			map(tvar, var),	% typeinfo vars for
 					% type parameters
-			termination,	% The termination properties of the
-					% procedure.  Initially 'not_set'.
-					% Final value inferred by termination.m
+			maybe(arg_size_info),
+					% Information about the relative sizes
+					% of the input and output args of the
+					% procedure. Set by termination
+					% analysis.
+			maybe(termination_info),
+					% The termination properties of the
+					% procedure. Set by termination
+					% analysis.
 			maybe(list(mode))
 					% declared modes of arguments.
 		).
@@ -878,37 +891,36 @@
 	ClauseBody = conj([]) - GoalInfo,
 	CanProcess = yes,
 	map__init(TVarsMap),
-	term_util__init(Termination),
 	NewProc = procedure(
 		MaybeDet, BodyVarSet, BodyTypes, HeadVars, Modes, MaybeArgLives,
 		ClauseBody, MContext, StackSlots, InferredDet, CanProcess,
-		ArgInfo, InitialLiveness, TVarsMap, Termination, DeclaredModes
+		ArgInfo, InitialLiveness, TVarsMap, no, no, DeclaredModes
 	).
 
 proc_info_set(DeclaredDetism, BodyVarSet, BodyTypes, HeadVars, HeadModes,
 		HeadLives, Goal,
 		Context, StackSlots, InferredDetism, CanProcess,
-		ArgInfo, Liveness, TVarMap, Termination, ProcInfo) :-
+		ArgInfo, Liveness, TVarMap, ArgSizes, Termination, ProcInfo) :-
 	ProcInfo = procedure(
 		DeclaredDetism, BodyVarSet, BodyTypes, HeadVars, HeadModes,
 		HeadLives, Goal, Context, StackSlots, InferredDetism,
-		CanProcess, ArgInfo, Liveness, TVarMap, Termination, no).
+		CanProcess, ArgInfo, Liveness, TVarMap, ArgSizes, Termination,
+		no).
 
 proc_info_create(VarSet, VarTypes, HeadVars, HeadModes, Detism, Goal,
 		Context, TVarMap, ProcInfo) :-
 	map__init(StackSlots),
 	set__init(Liveness),
-	term_util__init(Termination),
 	MaybeHeadLives = no,
 	ProcInfo = procedure(yes(Detism), VarSet, VarTypes, HeadVars, HeadModes,
 		MaybeHeadLives, Goal, Context, StackSlots, Detism, yes, [],
-		Liveness, TVarMap, Termination, no).
+		Liveness, TVarMap, no, no, no).
 
 proc_info_set_body(ProcInfo0, VarSet, VarTypes, HeadVars, Goal, ProcInfo) :-
 	ProcInfo0 = procedure(A, _, _, _, E, F, _,
-		H, I, J, K, L, M, N, O, P),
+		H, I, J, K, L, M, N, O, P, Q),
 	ProcInfo = procedure(A, VarSet, VarTypes, HeadVars, E, F, Goal,
-		H, I, J, K, L, M, N, O, P).
+		H, I, J, K, L, M, N, O, P, Q).
 
 proc_info_interface_determinism(ProcInfo, Determinism) :-
 	proc_info_declared_determinism(ProcInfo, MaybeDeterminism),
@@ -956,48 +968,6 @@
 	assoc_list__from_corresponding_lists(HeadVars, InitialInsts, InstAL),
 	instmap__from_assoc_list(InstAL, InstMap).
 
-proc_info_declared_determinism(ProcInfo, Detism) :-
-    ProcInfo = procedure(Detism, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _).
-proc_info_variables(ProcInfo, VarSet) :-
-    ProcInfo = procedure(_, VarSet, _, _, _, _, _, _, _, _, _, _, _, _, _, _).
-proc_info_vartypes(ProcInfo, VarTypes) :-
-    ProcInfo = procedure(_, _, VarTypes, _, _, _, _, _, 
-    		_, _, _, _, _, _, _, _).
-proc_info_headvars(ProcInfo, HeadVars) :-
-    ProcInfo = procedure(_, _, _, HeadVars, _, _, _, _, 
-    		_, _, _, _, _, _, _, _).
-proc_info_argmodes(ProcInfo, Modes) :-
-    ProcInfo = procedure(_, _, _, _, Modes, _, _, _, _, _, _, _, _, _, _, _).
-proc_info_maybe_arglives(ProcInfo, ArgLives) :-
-    ProcInfo = procedure(_, _, _, _, _, ArgLives, 
-    		_, _, _, _, _, _, _, _, _, _).
-proc_info_goal(ProcInfo, Goal) :-
-    ProcInfo = procedure(_, _, _, _, _, _, Goal, _, _, _, _, _, _, _, _, _).
-proc_info_context(ProcInfo, Context) :-
-    ProcInfo = procedure(_, _, _, _, _, _, _, Context, _, _, _, _, _, _, _, _).
-proc_info_stack_slots(ProcInfo, StackSlots) :-
-    ProcInfo = procedure(_, _, _, _, _, _, _, _, StackSlots, 
-    		_, _, _, _, _, _, _).
-proc_info_inferred_determinism(ProcInfo, Detism) :-
-    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, Detism, _, _, _, _, _, _).
-proc_info_can_process(ProcInfo, CanProcess) :-
-    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, CanProcess, 
-    		_, _, _, _, _).
-proc_info_arg_info(ProcInfo, ArgInfo) :- 
-    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, ArgInfo, 
-    		_, _, _, _).
-proc_info_liveness_info(ProcInfo, Liveness) :-
-    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, Liveness, 
-    		_, _, _).
-proc_info_typeinfo_varmap(ProcInfo, TVarMap) :-
-    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, _, TVarMap, _, _).
-proc_info_termination(ProcInfo, Termination) :-
-    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, _, _, 
-    		Termination, _).
-proc_info_maybe_declared_argmodes(ProcInfo, MaybeArgModes) :-
-    ProcInfo = procedure(_, _, _, _, _, _, _,
-		_, _, _, _, _, _, _, _, MaybeArgModes).
-
 proc_info_declared_argmodes(ProcInfo, ArgModes) :-
 	proc_info_maybe_declared_argmodes(ProcInfo, MaybeArgModes),
 	( MaybeArgModes = yes(ArgModes1) ->
@@ -1006,6 +976,57 @@
 		proc_info_argmodes(ProcInfo, ArgModes)
 	).
 
+proc_info_declared_determinism(ProcInfo, A) :-
+    ProcInfo = procedure(A, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _).
+
+proc_info_varset(ProcInfo, B) :-
+    ProcInfo = procedure(_, B, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _).
+
+proc_info_vartypes(ProcInfo, C) :-
+    ProcInfo = procedure(_, _, C, _, _, _, _, _, _, _, _, _, _, _, _, _, _).
+
+proc_info_headvars(ProcInfo, D) :-
+    ProcInfo = procedure(_, _, _, D, _, _, _, _, _, _, _, _, _, _, _, _, _).
+
+proc_info_argmodes(ProcInfo, E) :-
+    ProcInfo = procedure(_, _, _, _, E, _, _, _, _, _, _, _, _, _, _, _, _).
+
+proc_info_maybe_arglives(ProcInfo, F) :-
+    ProcInfo = procedure(_, _, _, _, _, F, _, _, _, _, _, _, _, _, _, _, _).
+
+proc_info_goal(ProcInfo, G) :-
+    ProcInfo = procedure(_, _, _, _, _, _, G, _, _, _, _, _, _, _, _, _, _).
+
+proc_info_context(ProcInfo, H) :-
+    ProcInfo = procedure(_, _, _, _, _, _, _, H, _, _, _, _, _, _, _, _, _).
+
+proc_info_stack_slots(ProcInfo, I) :-
+    ProcInfo = procedure(_, _, _, _, _, _, _, _, I, _, _, _, _, _, _, _, _).
+
+proc_info_inferred_determinism(ProcInfo, J) :-
+    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, J, _, _, _, _, _, _, _).
+
+proc_info_can_process(ProcInfo, K) :-
+    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, K, _, _, _, _, _, _).
+
+proc_info_arg_info(ProcInfo, L) :- 
+    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, L, _, _, _, _, _).
+
+proc_info_liveness_info(ProcInfo, M) :-
+    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, M, _, _, _, _).
+
+proc_info_typeinfo_varmap(ProcInfo, N) :-
+    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, _, N, _, _, _).
+
+proc_info_get_maybe_arg_size_info(ProcInfo, O) :-
+    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, _, _, O, _, _).
+
+proc_info_get_maybe_termination_info(ProcInfo, P) :-
+    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, P, _).
+
+proc_info_maybe_declared_argmodes(ProcInfo, R) :-
+    ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, R).
+
 % :- type proc_info	--->	procedure(
 % 				A	maybe(determinism),% _declared_ detism
 % 				B	varset,		% variable names
@@ -1027,72 +1048,69 @@
 % 				M	liveness_info	% the initial liveness
 %				N	map(tvar, var)  % typeinfo vars to
 %							% vars.
-%				O	termination	% Termination analys
-%				P	maybe(list(mode)) % declared modes
+%				O	maybe(arg_size_info)
+%							% Termination analys
+%				P	maybe(termination_info)
+%							% Termination analys
+%				Q	maybe(list(mode)) % declared modes
 %							% of args
 % 				).
 
-proc_info_set_varset(ProcInfo0, VarSet, ProcInfo) :-
-    ProcInfo0 = procedure(A, _, C, D, E, F, G, H, I, J, K, L, M, N, O, P),
-    ProcInfo = procedure(A, VarSet, C, D, E, F, G, H, I, J, K, L, M, N, O, P).
-
-proc_info_set_variables(ProcInfo0, Vars, ProcInfo) :-
-    ProcInfo0 = procedure(A, _, C, D, E, F, G, H, I, J, K, L, M, N, O, P),
-    ProcInfo = procedure(A, Vars, C, D, E, F, G, H, I, J, K, L, M, N, O, P).
-
-proc_info_set_vartypes(ProcInfo0, Vars, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, _, D, E, F, G, H, I, J, K, L, M, N, O, P),
-    ProcInfo = procedure(A, B, Vars, D, E, F, G, H, I, J, K, L, M, N, O, P).
-
-proc_info_set_headvars(ProcInfo0, HdVars, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, _, E, F, G, H, I, J, K, L, M, N, O, P),
-    ProcInfo = procedure(A, B, C, HdVars, E, F, G, H, I, J, K, L, M, N, O, P).
-
-proc_info_set_argmodes(ProcInfo0, ArgModes, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, _, F, G, H, I, J, K, L, M, N, O, P),
-    ProcInfo = procedure(A, B, C, D, ArgModes, F, G, H, I, 
-    		J, K, L, M, N, O, P).
-
-proc_info_set_maybe_arglives(ProcInfo0, ArgLives, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, E, _, G, H, I, J, K, L, M, N, O, P),
-    ProcInfo = procedure(A, B, C, D, E, ArgLives, G, H, I, 
-    		J, K, L, M, N, O, P).
-
-proc_info_set_inferred_determinism(ProcInfo0, Detism, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P),
-    ProcInfo = procedure(A, B, C, D, E, F, G, H, I, Detism, K, L, M, N, O, P).
-
-proc_info_set_can_process(ProcInfo0, CanProcess, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, _, L, M, N, O, P),
-    ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, CanProcess, 
-    		L, M, N, O, P).
-
-proc_info_set_goal(ProcInfo0, Goal, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, E, F, _, H, I, J, K, L, M, N, O, P),
-    ProcInfo = procedure(A, B, C, D, E, F, Goal, H, I, J, K, L, M, N, O, P).
-
-proc_info_set_stack_slots(ProcInfo0, StackSlots, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, _, J, K, L, M, N, O, P),
-    ProcInfo = procedure(A, B, C, D, E, F, G, H, StackSlots, J, K, 
-    		L, M, N, O, P).
-
-proc_info_set_arg_info(ProcInfo0, ArgInfo, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, _, M, N, O, P),
-    ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, ArgInfo, M, N, O, P).
-
-proc_info_set_liveness_info(ProcInfo0, Liveness, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, _, N, O, P),
-    ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L, Liveness, 
-    		N, O, P).
-
-proc_info_set_typeinfo_varmap(ProcInfo0, TVarMap, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, _, O, P),
-    ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, TVarMap, O, P).
-
-proc_info_set_termination(ProcInfo0, Terminat, ProcInfo) :-
-    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, _, P),
-    ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L, 
-    		M, N, Terminat, P).
+proc_info_set_varset(ProcInfo0, B, ProcInfo) :-
+    ProcInfo0 = procedure(A, _, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_vartypes(ProcInfo0, C, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, _, D, E, F, G, H, I, J, K, L, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_headvars(ProcInfo0, D, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, _, E, F, G, H, I, J, K, L, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_argmodes(ProcInfo0, E, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, _, F, G, H, I, J, K, L, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_maybe_arglives(ProcInfo0, F, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, _, G, H, I, J, K, L, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_goal(ProcInfo0, G, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, F, _, H, I, J, K, L, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_stack_slots(ProcInfo0, I, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, _, J, K, L, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_inferred_determinism(ProcInfo0, J, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_can_process(ProcInfo0, K, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, _, L, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_arg_info(ProcInfo0, L, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, _, M, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_liveness_info(ProcInfo0, M, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, _, N, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_typeinfo_varmap(ProcInfo0, N, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, _, O, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_maybe_arg_size_info(ProcInfo0, O, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, _, P, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
+
+proc_info_set_maybe_termination_info(ProcInfo0, P, ProcInfo) :-
+    ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, _, Q),
+    ProcInfo  = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q).
 
 proc_info_get_typeinfo_vars_setwise(ProcInfo, Vars, TypeInfoVars) :-
 	set__to_sorted_list(Vars, VarList),
@@ -1133,26 +1151,26 @@
 proc_info_ensure_unique_names(ProcInfo0, ProcInfo) :-
 	proc_info_vartypes(ProcInfo0, VarTypes),
 	map__keys(VarTypes, AllVars),
-	proc_info_variables(ProcInfo0, VarSet0),
+	proc_info_varset(ProcInfo0, VarSet0),
 	varset__ensure_unique_names(AllVars, "p", VarSet0, VarSet),
-	proc_info_set_variables(ProcInfo0, VarSet, ProcInfo).
+	proc_info_set_varset(ProcInfo0, VarSet, ProcInfo).
 
 proc_info_create_var_from_type(ProcInfo0, Type, NewVar, ProcInfo) :-
-	proc_info_variables(ProcInfo0, VarSet0),
+	proc_info_varset(ProcInfo0, VarSet0),
 	proc_info_vartypes(ProcInfo0, VarTypes0),
 	varset__new_var(VarSet0, NewVar, VarSet),
 	map__det_insert(VarTypes0, NewVar, Type, VarTypes),
-	proc_info_set_variables(ProcInfo0, VarSet, ProcInfo1),
+	proc_info_set_varset(ProcInfo0, VarSet, ProcInfo1),
 	proc_info_set_vartypes(ProcInfo1, VarTypes, ProcInfo).
 
 proc_info_create_vars_from_types(ProcInfo0, Types, NewVars, ProcInfo) :-
 	list__length(Types, NumVars),
-	proc_info_variables(ProcInfo0, VarSet0),
+	proc_info_varset(ProcInfo0, VarSet0),
 	proc_info_vartypes(ProcInfo0, VarTypes0),
 	varset__new_vars(VarSet0, NumVars, NewVars, VarSet),
 	map__det_insert_from_corresponding_lists(VarTypes0, 
 		NewVars, Types, VarTypes),
-	proc_info_set_variables(ProcInfo0, VarSet, ProcInfo1),
+	proc_info_set_varset(ProcInfo0, VarSet, ProcInfo1),
 	proc_info_set_vartypes(ProcInfo1, VarTypes, ProcInfo).
 
 %-----------------------------------------------------------------------------%
Index: compiler/inlining.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inlining.m,v
retrieving revision 1.69
diff -u -r1.69 inlining.m
--- inlining.m	1997/09/01 14:02:31	1.69
+++ inlining.m	1997/11/15 02:27:22
@@ -338,7 +338,7 @@
 	pred_info_typevarset(PredInfo0, TypeVarSet0),
 
 	proc_info_goal(ProcInfo0, Goal0),
-	proc_info_variables(ProcInfo0, VarSet0),
+	proc_info_varset(ProcInfo0, VarSet0),
 	proc_info_vartypes(ProcInfo0, VarTypes0),
 	proc_info_typeinfo_varmap(ProcInfo0, TypeInfoVarMap0),
 
@@ -354,7 +354,7 @@
 
 	pred_info_set_typevarset(PredInfo0, TypeVarSet, PredInfo1),
 
-	proc_info_set_variables(ProcInfo0, VarSet, ProcInfo1),
+	proc_info_set_varset(ProcInfo0, VarSet, ProcInfo1),
 	proc_info_set_vartypes(ProcInfo1, VarTypes, ProcInfo2),
 	proc_info_set_typeinfo_varmap(ProcInfo2, TypeInfoVarMap, ProcInfo3),
 	proc_info_set_goal(ProcInfo3, Goal, ProcInfo),
@@ -427,7 +427,7 @@
 			% Callee has
 		module_info_pred_proc_info(ModuleInfo, PredId, ProcId,
 			PredInfo, ProcInfo),
-        	proc_info_variables(ProcInfo, CalleeVarset),
+        	proc_info_varset(ProcInfo, CalleeVarset),
 		varset__vars(CalleeVarset, CalleeListOfVars),
 		list__length(CalleeListOfVars, CalleeThisMany),
 		TotalVars is ThisMany + CalleeThisMany,
Index: compiler/lambda.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/lambda.m,v
retrieving revision 1.33
diff -u -r1.33 lambda.m
--- lambda.m	1997/11/24 07:26:46	1.33
+++ lambda.m	1997/11/25 07:33:03
@@ -120,7 +120,7 @@
 	pred_info_name(PredInfo0, PredName),
 	pred_info_get_is_pred_or_func(PredInfo0, PredOrFunc),
 	pred_info_typevarset(PredInfo0, TypeVarSet0),
-	proc_info_variables(ProcInfo0, VarSet0),
+	proc_info_varset(ProcInfo0, VarSet0),
 	proc_info_vartypes(ProcInfo0, VarTypes0),
 	proc_info_goal(ProcInfo0, Goal0),
 	proc_info_typeinfo_varmap(ProcInfo0, TVarMap0),
@@ -136,7 +136,7 @@
 
 	% set the new values of the fields in proc_info and pred_info
 	proc_info_set_goal(ProcInfo0, Goal, ProcInfo1),
-	proc_info_set_variables(ProcInfo1, VarSet, ProcInfo2),
+	proc_info_set_varset(ProcInfo1, VarSet, ProcInfo2),
 	proc_info_set_vartypes(ProcInfo2, VarTypes, ProcInfo3),
 	proc_info_set_typeinfo_varmap(ProcInfo3, TVarMap, ProcInfo),
 	pred_info_set_typevarset(PredInfo0, TypeVarSet, PredInfo).
Index: compiler/liveness.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/liveness.m,v
retrieving revision 1.84
diff -u -r1.84 liveness.m
--- liveness.m	1997/10/20 07:35:22	1.84
+++ liveness.m	1997/11/15 02:27:36
@@ -153,7 +153,7 @@
 detect_liveness_proc(ProcInfo0, ModuleInfo, ProcInfo) :-
 	requantify_proc(ProcInfo0, ProcInfo1),
 	proc_info_goal(ProcInfo1, Goal0),
-	proc_info_variables(ProcInfo1, Varset),
+	proc_info_varset(ProcInfo1, Varset),
 	proc_info_vartypes(ProcInfo1, VarTypes),
 	live_info_init(ModuleInfo, ProcInfo1, VarTypes, Varset, LiveInfo),
 
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.245
diff -u -r1.245 make_hlds.m
--- make_hlds.m	1997/11/24 07:26:48	1.245
+++ make_hlds.m	1997/11/25 07:33:05
@@ -383,7 +383,7 @@
 		{ Module = Module0 }
 	;
 		{ Pragma = termination_info(PredOrFunc, SymName, ModeList, 
-			Termination) },
+			MaybeArgSizeInfo, MaybeTerminationInfo) },
 		{ module_info_get_predicate_table(Module0, Preds) },
 		{ list__length(ModeList, Arity) },
 		(
@@ -405,8 +405,11 @@
 					ModeList, Module0, ProcId) }
 			->
 				{ map__lookup(ProcTable0, ProcId, ProcInfo0) },
-				{ proc_info_set_termination(ProcInfo0, 
-					Termination, ProcInfo) },
+				{ proc_info_set_maybe_arg_size_info(ProcInfo0, 
+					MaybeArgSizeInfo, ProcInfo1) },
+				{ proc_info_set_maybe_termination_info(
+					ProcInfo1, 
+					MaybeTerminationInfo, ProcInfo) },
 				{ map__det_update(ProcTable0, ProcId, ProcInfo,
 					ProcTable) },
 				{ pred_info_set_procedures(PredInfo0, 
Index: compiler/mercury_to_c.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_c.m,v
retrieving revision 1.28
diff -u -r1.28 mercury_to_c.m
--- mercury_to_c.m	1997/11/24 23:08:21	1.28
+++ mercury_to_c.m	1997/11/25 07:33:07
@@ -231,7 +231,7 @@
 
 c_gen_proc(Indent, ModuleInfo, PredId, ProcId, Pred, Proc) -->
 	{ proc_info_interface_determinism(Proc, InterfaceDeterminism) },
-	{ proc_info_variables(Proc, VarSet) },
+	{ proc_info_varset(Proc, VarSet) },
 	{ proc_info_headvars(Proc, HeadVars) },
 	{ pred_info_name(Pred, PredName) },
 	{ proc_info_vartypes(Proc, VarTypes) },
@@ -348,7 +348,7 @@
 		PredInfo, ProcInfo) },
 
 	{ proc_info_interface_code_model(ProcInfo, CodeModel) },
-	{ proc_info_variables(ProcInfo, VarSet) },
+	{ proc_info_varset(ProcInfo, VarSet) },
 	{ proc_info_headvars(ProcInfo, HeadVars) },
 	{ pred_info_arg_types(PredInfo, _HeadTypeVarSet, HeadTypes) },
 	{ proc_info_argmodes(ProcInfo, HeadModes) },
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.121
diff -u -r1.121 mercury_to_mercury.m
--- mercury_to_mercury.m	1997/11/23 05:18:23	1.121
+++ mercury_to_mercury.m	1997/11/25 07:33:08
@@ -311,9 +311,10 @@
 		mercury_output_pragma_fact_table(Pred, Arity, FileName)
 	;
 		{ Pragma = termination_info(PredOrFunc, PredName, 
-			ModeList, Termination) },
-		termination__output_pragma_termination_info(PredOrFunc,
-			PredName, ModeList, Termination, Context)
+			ModeList, MaybeArgSizeInfo, MaybeTerminationInfo) },
+		termination__write_pragma_termination_info(PredOrFunc,
+			PredName, ModeList, Context,
+			MaybeArgSizeInfo, MaybeTerminationInfo)
 	;
 		{ Pragma = terminates(Pred, Arity) },
 		mercury_output_pragma_decl(Pred, Arity, predicate, "terminates")
Index: compiler/mode_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_info.m,v
retrieving revision 1.40
diff -u -r1.40 mode_info.m
--- mode_info.m	1997/10/14 09:18:44	1.40
+++ mode_info.m	1997/11/15 02:28:00
@@ -336,7 +336,7 @@
 	map__lookup(Preds, PredId, PredInfo),
 	pred_info_procedures(PredInfo, Procs),
 	map__lookup(Procs, ProcId, ProcInfo),
-	proc_info_variables(ProcInfo, VarSet),
+	proc_info_varset(ProcInfo, VarSet),
 	proc_info_vartypes(ProcInfo, VarTypes),
 
 	LiveVarsList = [LiveVars],
Index: compiler/modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modes.m,v
retrieving revision 1.209
diff -u -r1.209 modes.m
--- modes.m	1997/11/24 23:10:25	1.209
+++ modes.m	1997/11/25 07:33:10
@@ -684,7 +684,7 @@
 	mode_info_get_varset(ModeInfo, VarSet),
 	mode_info_get_var_types(ModeInfo, VarTypes),
 	proc_info_set_goal(ProcInfo0, Body, ProcInfo1),
-	proc_info_set_variables(ProcInfo1, VarSet, ProcInfo2),
+	proc_info_set_varset(ProcInfo1, VarSet, ProcInfo2),
 	proc_info_set_vartypes(ProcInfo2, VarTypes, ProcInfo3),
 	proc_info_set_argmodes(ProcInfo3, ArgModes, ProcInfo).
 
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.24
diff -u -r1.24 module_qual.m
--- module_qual.m	1997/10/09 09:38:57	1.24
+++ module_qual.m	1997/11/05 03:34:02
@@ -608,8 +608,8 @@
 				Info, Info) --> [].
 qualify_pragma(fact_table(SymName, Arity, FileName),
 	fact_table(SymName, Arity, FileName), Info, Info) --> [].
-qualify_pragma(termination_info(PredOrFunc, SymName, ModeList0, Termination), 
-		termination_info(PredOrFunc, SymName, ModeList, Termination), 
+qualify_pragma(termination_info(PredOrFunc, SymName, ModeList0, Args, Term), 
+		termination_info(PredOrFunc, SymName, ModeList, Args, Term), 
 		Info0, Info) --> 
 	qualify_mode_list(ModeList0, ModeList, Info0, Info).
 qualify_pragma(terminates(A, B), terminates(A, B), Info, Info) --> [].
Index: compiler/modules.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modules.m,v
retrieving revision 1.43
diff -u -r1.43 modules.m
--- modules.m	1997/11/21 08:08:23	1.43
+++ modules.m	1997/11/25 07:33:11
@@ -257,7 +257,7 @@
 		{ Pragma \= terminates(_, _) },
 		{ Pragma \= does_not_terminate(_, _) },
 		{ Pragma \= check_termination(_, _) },
-		{ Pragma \= termination_info(_, _, _, _) }
+		{ Pragma \= termination_info(_, _, _, _, _) }
 	->
 		prog_out__write_context(Context),
 		report_warning("Warning: pragma in module interface.\n"),
Index: compiler/options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/options.m,v
retrieving revision 1.211
diff -u -r1.211 options.m
--- options.m	1997/11/13 06:27:17	1.211
+++ options.m	1997/11/24 06:43:49
@@ -197,6 +197,7 @@
 		;	verbose_check_termination
 		;	termination_single_args
 		;	termination_norm
+		;	termination_error_limit
 	%	- HLDS->LLDS
 		;	smart_indexing
 		;	  dense_switch_req_density
@@ -428,8 +429,9 @@
 	check_termination	-	bool(no),
 	verbose_check_termination -	bool(no),
 	termination		-	bool(no),
-	termination_single_args	-	bool(no),
+	termination_single_args	-	int(0),
 	termination_norm	-	string("total"),
+	termination_error_limit	-	int(3),
 	split_c_files		-	bool(no)
 ]).
 option_defaults_2(optimization_option, [
@@ -754,6 +756,8 @@
 long_option("term-single-arg", 		termination_single_args).
 long_option("termination-norm",		termination_norm).
 long_option("term-norm",		termination_norm).
+long_option("termination-error-limit",	termination_error_limit).
+long_option("term-err-limit",		termination_error_limit).
 
 % HLDS->LLDS optimizations
 long_option("smart-indexing",		smart_indexing).
@@ -1490,6 +1494,10 @@
 	io__write_string("\t--verb-chk-term, --verb-check-term, --verbose-check-termination\n"),
 	io__write_string("\t\tEnable termination analysis, and emit warnings for all\n"),
 	io__write_string("\t\tpredicates or functions that cannot be proved to terminate.\n"),
+	io__write_string("\t--term-single-arg <n>, --termination-single-argument-analysis <n>\n"),
+	io__write_string("\t\tWhen performing termination analysis, try analyzing\n"),
+	io__write_string("\t\trecursion on single arguments in strongly connected\n"),
+	io__write_string("\t\tcomponents of the call graph that have up to n procedures.\n"),
 	io__write_string("\t--termination-norm {simple, total, num-data-elems}\n"),
 	io__write_string("\t\tThe norm defines how termination analysis measures the size\n"),
 	io__write_string("\t\tof a memory cell. The simple norm says that size is always one.\n"),
@@ -1497,6 +1505,8 @@
 	io__write_string("\t\tThe num-data-elems norm says that it is the number of words in\n"),
 	io__write_string("\t\tthe cell that contain something other than pointers to cells of\n"),
 	io__write_string("\t\tthe same type.\n"),
+	io__write_string("\t--termination-error-limit <n>, --term-err-limit <n>\n"),
+	io__write_string("\t\tPrint at most n reasons for any single termination error.\n"),
 	io__write_string("\t--split-c-files\n"),
 	io__write_string("\t\tGenerate each C function in its own C file,\n"),
 	io__write_string("\t\tso that the linker will optimize away unused code.\n"),
Index: compiler/polymorphism.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.118
diff -u -r1.118 polymorphism.m
--- polymorphism.m	1997/10/14 09:27:53	1.118
+++ polymorphism.m	1997/11/15 02:28:20
@@ -302,7 +302,7 @@
 	pred_info_typevarset(PredInfo0, TypeVarSet0),
 	pred_info_name(PredInfo0, PredName),
 	proc_info_headvars(ProcInfo0, HeadVars0),
-	proc_info_variables(ProcInfo0, VarSet0),
+	proc_info_varset(ProcInfo0, VarSet0),
 	proc_info_vartypes(ProcInfo0, VarTypes0),
 	proc_info_goal(ProcInfo0, Goal0),
 	proc_info_argmodes(ProcInfo0, ArgModes0),
Index: compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.26
diff -u -r1.26 prog_data.m
--- prog_data.m	1997/10/09 09:39:05	1.26
+++ prog_data.m	1997/11/05 03:26:56
@@ -131,7 +131,7 @@
 			% Predname, Arity, Fact file name.
 
 	;	termination_info(pred_or_func, sym_name, list(mode),
-			termination)
+			maybe(arg_size_info), maybe(termination_info))
 			% the list(mode) is the declared argmodes of the
 			% procedure, unless there are no declared argmodes,
 			% in which case the inferred argmodes are used.
Index: compiler/prog_io_pragma.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_pragma.m,v
retrieving revision 1.8
diff -u -r1.8 prog_io_pragma.m
--- prog_io_pragma.m	1997/11/02 12:29:23	1.8
+++ prog_io_pragma.m	1997/11/25 06:20:03
@@ -327,9 +327,8 @@
     (
 	PragmaTerms = [
 	    PredAndModesTerm0,
-	    ConstTerm,
-	    TerminatesTerm,
-	    MaybeUsedArgsTerm
+	    ArgSizeTerm,
+	    TerminationTerm
 	],
 	( 
 	    PredAndModesTerm0 = term__functor(Const, Terms0, _) 
@@ -360,44 +359,35 @@
 	    ),
 	    convert_mode_list(ModeListTerm, ModeList),
 	    (			
-		ConstTerm = term__functor(term__atom("not_set"), [], _),
-		TerminationConst = not_set
+		ArgSizeTerm = term__functor(term__atom("not_set"), [], _),
+		MaybeArgSizeInfo = no
 	    ;
-		ConstTerm = term__functor( 
-		    term__atom("infinite"), [], ConstContext),
-		TerminationConst = inf(ConstContext - imported_pred)
+		ArgSizeTerm = term__functor(term__atom("infinite"), [],
+			ArgSizeContext),
+		MaybeArgSizeInfo = yes(infinite(
+			[ArgSizeContext - imported_pred]))
 	    ;
-		ConstTerm = term__functor(term__atom("set"), [IntTerm], _),
+		ArgSizeTerm = term__functor(term__atom("finite"),
+			[IntTerm, UsedArgsTerm], _),
 		IntTerm = term__functor(term__integer(Int), [], _),
-		TerminationConst = set(Int)
+		convert_bool_list(UsedArgsTerm, UsedArgs),
+		MaybeArgSizeInfo = yes(finite(Int, UsedArgs))
 	    ),
 	    (
-		TerminatesTerm = term__functor(term__atom("not_set"), [], _),
-		Terminates = not_set,
-		MaybeError = no
-	    ;
-		TerminatesTerm = term__functor(
-		    term__atom("dont_know"), [], TermContext),
-		Terminates = dont_know,
-		MaybeError = yes(TermContext - imported_pred)
-	    ;
-		TerminatesTerm = term__functor(term__atom("yes"), [], _),
-		Terminates = yes,
-		MaybeError = no
-	    ),
-	    (
-		MaybeUsedArgsTerm = term__functor(
-		    term__atom("yes"), [BoolListTerm], _),
-		convert_bool_list(BoolListTerm, BoolList),
-		MaybeUsedArgs = yes(BoolList)
+		TerminationTerm = term__functor(term__atom("not_set"), [], _),
+		MaybeTerminationInfo = no
 	    ;
-		MaybeUsedArgsTerm = term__functor(term__atom("no"), [], _),
-		MaybeUsedArgs = no
+		TerminationTerm = term__functor(term__atom("can_loop"),
+			[], TermContext),
+		MaybeTerminationInfo = yes(can_loop(
+			[TermContext - imported_pred]))
+	    ;
+		TerminationTerm = term__functor(term__atom("cannot_loop"),
+			[], _),
+		MaybeTerminationInfo = yes(cannot_loop)
 	    ),
-	    Termination = term(TerminationConst, Terminates,
-	    	MaybeUsedArgs, MaybeError),
 	    Result0 = ok(pragma(termination_info(PredOrFunc, PredName, 
-	    	ModeList, Termination)))
+	    	ModeList, MaybeArgSizeInfo, MaybeTerminationInfo)))
 	;
 	    Result0 = error("unexpected variable in pragma termination_info",
 						ErrorTerm)
@@ -408,7 +398,6 @@
 	Result = error("syntax error in `pragma termination_info'", ErrorTerm)
     ).
 			
-
 parse_pragma_type(ModuleName, "terminates", PragmaTerms,
 				ErrorTerm, _VarSet, Result) :-
 	parse_simple_pragma(ModuleName, "terminates",

[continued in part 3]
Previous message: for review: changes to termination analysis and stack tracing [1/3]
Next message: for review: changes to termination analysis and stack tracing [3/3]
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the developers mailing list