Termination Analysis part 1.2

[Christopher Rodd SPEIRS]

Part 1.2.  This contains term_pass2, term_util and term_errors.


%-----------------------------------------------------------------------------
%
% Copyright (C) 1997 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------
%
% term_pass2.m
% Main author: crs.
%
% This file contains the actual termination analysis.  This file processes
% through each procedure, and sets the terminates property of each one.
%
% Termination analysis:
% This goes through each of the SCC's in turn, analysing them to determine
% which predicates terminate.
% 			
%-----------------------------------------------------------------------------
:- module term_pass2.
:- interface.

:- import_module io, hlds_module, term_util.

% Analyse each predicate in the order given by
% hlds_dependency_info_get_dependency_ordering to determine whether or not
% it terminates.  Put the result of the analysis into the termination
% field of the proc_info structure..  
:- pred termination(module_info, functor_info, module_info, 
	io__state, io__state).
:- mode termination(in, in, out, di, uo) is det.

:- implementation.

:- import_module bag, hlds_pred, std_util, int, list, relation, require.
:- import_module set, hlds_goal, term_util, term_errors, bool.
:- import_module globals, options, map, term, type_util.

% Used in termination_goal to keep track of the relative sizes of variables
% between the head of a predicate and any recursive calls.
:- type termination_call
	--->	tuple(pred_proc_id, 	% The called procedure
			int, 		% The relative size of the active
					% variables, in comparison with the 
					% size of the variables in the
					% recursive call.
			bag(var), 	% The bag of active variables.
			maybe(var), 	% Only for single argrgument analysis.
					% This stores which head variable
					% is being traced by this tuple.
			term__context).	% Where the call occured.

termination(Module0, FunctorInfo, Module) -->
	{ module_info_dependency_info(Module0, DependencyInfo) },
	{ hlds_dependency_info_get_dependency_ordering(DependencyInfo, 
		DependencyOrdering) },

	termination_module(Module0, DependencyOrdering, FunctorInfo, Module).


:- pred termination_module(module_info, dependency_ordering, functor_info, 
	module_info, io__state, io__state).
:- mode termination_module(in, in, in, out, di, uo) is det.
termination_module(Module, [], _FunctorInfo, Module) --> [].
termination_module(Module0, [SCC | SCCs], FunctorInfo, Module) -->
	termination_module_check_terminates(SCC, SCC, Module0, Module1, Succ),
	( { Succ = yes } ->
		% Need to run termination checking on this SCC.
		% Initialise the relation
		{ relation__init(Relation0) },
		% Add each procedure to the relation.
		{ add_pred_procs_to_relation(SCC, Relation0, Relation1) },
		% Analyse the current SCC.
		{ init_used_args(SCC, Module1, InitUsedArgs) },
		{ call_termination_scc(SCC, FunctorInfo, Module1, Res, 
			InitUsedArgs, Relation1, Relation2) },
		( 	
			{ Res = ok },
			% Check that the relation returned is acyclic 
			% and set the termination property accordingly.
			( { relation__tsort(Relation2, _) } ->
				% All the procedures in this SCC terminate,
				% set all termination properties to yes.
				{ set_pred_proc_ids_terminates(SCC, 
					yes, no, Module1, Module3) }
			;
				( { SCC = [ proc(PredId, _) | _ ] } ->
					{ module_info_pred_info(Module1,
						PredId, PredInfo) },
					{ pred_info_context(PredInfo, 
						Context) }
				;
					{ error("Unexpected empty list in term_pass2__termination_module/6")}
				),
				% Try doing single argument analysis.
				termination_scc_single_args(SCC, FunctorInfo,
					Context - not_dag, InitUsedArgs, 
					Module1, Module3)
			)
		;
			{ Res = error(Error) },
			% Normal analysis failed, try doing single argument
			% analysis.
			termination_scc_single_args(SCC, FunctorInfo, 
				Error, InitUsedArgs, Module1, Module3)
		)
	;
		% All the termination properties are already set.
		{ Module3 = Module1 }
	),
	termination_module(Module3, SCCs, FunctorInfo, Module).


% If this predicate returns Succ = yes, then termination analysis needs to be
% run on this SCC.  If it returns Succ =  no, then the termination
% properties of this SCC have already been set.
% XXX this can be improved.  If ANY Terminates in the SCC is set to dont_know,
% then the whole SCC can be set to dont_know
:- pred termination_module_check_terminates(list(pred_proc_id), 
	list(pred_proc_id), module_info, module_info, bool, 
	io__state, io__state).
:- mode termination_module_check_terminates(in, in, in, out, out, 
		di, uo) is det.
termination_module_check_terminates([], _SCC, Module, Module, no) --> [].
termination_module_check_terminates([ PPId | PPIds ], SCC, Module0, 
		Module, Succ) -->
	{ PPId = proc(PredId, ProcId) },
	{ module_info_pred_proc_info(Module0, PredId, ProcId, _, ProcInfo) },
	{ proc_info_termination(ProcInfo, Term) },
	{ Term = term(_Const, Terminates, _UsedArgs, MaybeError) },
	( 
		{ Terminates = not_set },
		{ Succ = yes },
		{ Module = Module0 }
	;
		{ Terminates = yes },
		termination_module_check_terminates(PPIds, SCC, Module0, 
			Module, Succ)
	;
		{ Terminates = dont_know},
		{ Succ = no },
		( { MaybeError = yes(Error) } ->
			do_ppid_check_terminates(SCC, Error, Module0, Module)
		;
			{ error("term_pass2.m: unexpected value in termination_module_check_terminates/6") }
		)
	).

% This predicate runs termination_scc until a fixed point for UsedArgs 
% is reached.
:- pred call_termination_scc(list(pred_proc_id), functor_info, module_info,
	term_util__result(term_errors__error), map(pred_proc_id, set(var)),
	relation(pred_proc_id), relation(pred_proc_id)).
:- mode call_termination_scc(in, in, in, out, in, in, out) is det.
call_termination_scc(SCC, FunctorInfo, Module, Result, UsedArgs0, 
		Relation0, Relation) :-
	termination_scc(SCC, FunctorInfo, Module, Res1, UsedArgs0, UsedArgs1, 
		Relation0, Relation1),
	( 
		% If some other error prevented the analysis from proving
		% termination, then finding a fixed point will not assist
		% in proving termination, so we may as well stop here.
		( Res1 = error(_ - not_subset(_, _, _))
		; Res1 = error(_ - positive_value(_, _))
		),
		UsedArgs1 \= UsedArgs0  % If these are equal, then we are at 
					% a fixed point, so further
					% analysis will not get any better
					% results.
	->
		% We can use the new Used Args values, and try again.
		call_termination_scc(SCC, FunctorInfo, Module, Result, 
			UsedArgs1, Relation0, Relation)

	;
		Relation = Relation1,
		Result = Res1
	).

% This initialises the used arguments to be the set of input variables.
:- pred init_used_args(list(pred_proc_id), module_info, 
	map(pred_proc_id, set(var))).
:- mode init_used_args(in, in, out) is det.
init_used_args([], _, InitMap) :-
	map__init(InitMap).
init_used_args([PPId | PPIds], Module, UsedArgs) :-
	init_used_args(PPIds, Module, UsedArgs0),
	PPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	proc_info_headvars(ProcInfo, Args),
	proc_info_argmodes(ProcInfo, ArgModes),
	partition_call_args(Module, ArgModes, Args, InArgs, _OutVars),
	set__list_to_set(InArgs, ArgSet),
	map__det_insert(UsedArgs0, PPId, ArgSet, UsedArgs).

% Given a list of all the arguments of a predicate, find out which
% arguments are unused, so that they can be removed from the used arguments
% list for that predicate.
:- pred termination_scc_calc_unused_args(list(var), list(termination_call), 
	list(var)).
:- mode termination_scc_calc_unused_args(in, in, out) is det.
termination_scc_calc_unused_args(Vars, [], Vars).
termination_scc_calc_unused_args(Vars0, [X | Xs], Vars) :-
	X = tuple(_, _, VarBag, _, _),
	termination_scc_calc_unused_args_2(Vars0, VarBag, Vars1),
	termination_scc_calc_unused_args(Vars1, Xs, Vars).

:- pred termination_scc_calc_unused_args_2(list(var), bag(var), list(var)).
:- mode termination_scc_calc_unused_args_2(in, in, out) is det.
termination_scc_calc_unused_args_2([], _, []).
termination_scc_calc_unused_args_2([ X | Xs ], Vars, Ys) :-
	( bag__contains(Vars, X) ->
		% If the variable is in the bag, then it is used.
		% Therefore, it should not be in the list of unused vars
		termination_scc_calc_unused_args_2(Xs, Vars, Ys)
	;
		termination_scc_calc_unused_args_2(Xs, Vars, Ys0),
		Ys = [X | Ys0]
	).

% Process a whole SCC, to determine the termination property of each
% procedure in that SCC.   
:- pred termination_scc(list(pred_proc_id), functor_info, module_info, 
	term_util__result(term_errors__error), map(pred_proc_id, set(var)),
	map(pred_proc_id, set(var)), relation(pred_proc_id),
	relation(pred_proc_id)).
:- mode termination_scc(in, in, in, out, in, out, in, out) is det.
termination_scc([], _, _Module, ok, UsedArgs, UsedArgs, Relation, Relation).
termination_scc([ PPId | PPIds ], FunctorInfo, Module, Result, 
		UsedArgs0, UsedArgs, Relation0, Relation) :-
	% Get the goal info.
	PPId = proc(PredId, ProcId),
	module_info_pred_proc_info(Module, PredId, ProcId, _PredInfo, ProcInfo),
	proc_info_termination(ProcInfo, Termination),
	( Termination = term(_Const, dont_know, _, MaybeError) ->
		% If the termination property is set to dont_know then
		% MaybeError should contain an error.  
		( MaybeError = yes(Error) ->
			Result = error(Error)
		;
			error("term_pass2.m: Unexpected value in term_pass2:termination_scc")
		),
		UsedArgs = UsedArgs0,
		Relation = Relation0
	;
		proc_info_goal(ProcInfo, Goal),
		proc_info_vartypes(ProcInfo, VarTypes),
		Goal = GoalExpr - GoalInfo,
		% Analyse goal info. This returns a list of ppid - size
		% pairs.
		UnifyInfo = VarTypes - FunctorInfo,
		CallInfo = call_info(PPId, UsedArgs0, no),
		termination_goal(GoalExpr, GoalInfo, Module, UnifyInfo,
			CallInfo, Res0, [], Out),
		
		proc_info_argmodes(ProcInfo, ArgModes),
		proc_info_headvars(ProcInfo, Args),
		partition_call_args(Module, ArgModes, Args, InVars, _OutVars),
		bag__from_list(InVars, InVarsBag),
	
		( Res0 = ok ->
			termination_scc_calc_unused_args(Args, Out, UnUsedArgs),
			map__lookup(UsedArgs0, PPId, OldUsedArgs),
			set__delete_list(OldUsedArgs, UnUsedArgs, NewUsedArgs),
			termination_add_arcs_to_relation(PPId, Out, 
				InVarsBag, Res1, Relation0, Relation1),
			( Res1 = ok ->
				termination_scc(PPIds, FunctorInfo, Module, 
					Result, UsedArgs0, UsedArgs1, 
					Relation1, Relation)
			;
				% We failed because of positive value, or
				% because of not_subset.  Keep analysing,
				% to discover the used variables, of the other
				% procedures.
				termination_scc(PPIds, FunctorInfo, Module, 
					Res2, UsedArgs0, UsedArgs1, 
					Relation0, _Relation),
				Relation = Relation0,
				% We know that Res1 is not_subset or
				% positive_value.  If Res2 is ok, then we
				% need to return Res1 (so that the calling
				% predicate knows that the analysis
				% failed). If Res2 is an error, then it
				% needs to be returned.  If Res2 is also
				% not_subset or positive_value, then fine,
				% the analysis will be re-run.  If it is
				% some other error, then re-running the
				% analysis will not gain anything.
				( Res2 = ok ->
					Result = Res1
				;
					Result = Res2
				)
			),
			% Add the used vars from the current pass to the
			% UsedArgs map.
			map__det_update(UsedArgs1, PPId, NewUsedArgs, UsedArgs)
		;
			UsedArgs = UsedArgs0,
			Result = Res0,
			Relation = Relation0
		)
	).

% This runs single argument analysis on the goal.  This is only run if
% normal termination analysis failed.  
:- pred termination_scc_single_args(list(pred_proc_id), functor_info, 
	term_errors__error, map(pred_proc_id, set(var)), 
	module_info, module_info, io__state, io__state).
:- mode termination_scc_single_args(in, in, in, in, in, out, di, uo) is det.
termination_scc_single_args([], _, _, _, Module, Module) -->
	{ error("term_pass2__termination_scc_single_args: there should be\nat least 1 predicate in a SCC\n") }.
termination_scc_single_args([PPId | Rest], FunctorInfo, Error, UsedArgs,
		Module0, Module) -->
	globals__io_lookup_bool_option(termination_single_args, SingleArgs),
	{ SCC = [PPId | Rest] },
	{ PPId = proc(PredId, ProcId) },
	{ set__init(InitSet) },
	(
		{ SingleArgs = yes },
		{ Rest = [] },
		{ Error \= _ - imported_pred }
		% What other errors would prevent single argument analysis
		% from succeeding?
	->
		% Can do single argument analysis.
		{  module_info_pred_proc_info(Module0, PredId, ProcId, 
			_PredInfo, ProcInfo) },
		{ proc_info_goal(ProcInfo, Goal) },
		{ proc_info_vartypes(ProcInfo, VarTypes) },
		{ Goal = GoalExpr - GoalInfo },
		{ UnifyInfo = VarTypes - FunctorInfo },
		{ CallInfo = call_info(PPId, UsedArgs, yes) },
		{ termination_goal(GoalExpr, GoalInfo, Module0,
			UnifyInfo, CallInfo, Res0, [], Out) },
		( { Res0 = error(Error2) } ->
			% The context of single_arg_failed needs to be the
			% same as the context of the Normal analysis error
			% message.
			{ Error = Context - _ },
			{ Error3 = Context - single_arg_failed(Error, Error2) },
			do_ppid_check_terminates(SCC, Error3, 
				Module0, Module)
			
		; { termination_scc_single_2(Out, InitSet, InitSet) } ->
			% Single argument analysis succeded.
			{ set_pred_proc_ids_terminates(SCC, yes, yes(Error),
				Module0, Module) }
		;
			% Single argument analysis failed to prove
			% termination.  
			{ Error = Context - _ },
			{ Error2 = Context - single_arg_failed(Error) },
			do_ppid_check_terminates(SCC, Error2,
				Module0, Module)
		)
	;
		% Cant do single argument analysis.
		do_ppid_check_terminates(SCC, Error, 
			Module0, Module)
	).
		
:- pred termination_scc_single_2(list(termination_call), set(var), set(var)).
:- mode termination_scc_single_2(in, in, in) is semidet.
termination_scc_single_2([], NegSet, NonNegSet) :-
	set__difference(NegSet, NonNegSet, DiffSet),
	% Check that there is at least one head variable that is always
	% strictly decreasing in size between the head of the procedure and
	% the recursive call.
	set__remove_least(DiffSet, _, _).

termination_scc_single_2([Off | Offs], NegSet0, NonNegSet0) :-
	Off = tuple(_, Int, VarBag0, MaybeVar, _Context),
	( 	
		MaybeVar = no,
		error("termination.m: Maybevar should be yes in single argument analysis\n")
	; 
		MaybeVar = yes(HeadVar),
		( 
			Int < 0,
			% Check that the variable that was recursed on did
			% not change positions between the head and
			% recursive call.  I am not sure if the first call
			% to bag__remove is actually required to succeed
			bag__remove(VarBag0, HeadVar, VarBag1),
			\+ bag__remove_smallest(VarBag1, _, _)
		->
			set__insert(NegSet0, HeadVar, NegSet),
			termination_scc_single_2(Offs, NegSet, NonNegSet0)
		;
			set__insert(NonNegSet0, HeadVar, NonNegSet),
			termination_scc_single_2(Offs, NegSet0, NonNegSet)
		)
	).

% This adds the information from termination_goal to the relation.
% The relation is between the procedures in the current SCC. An arc
% shows that one procedure calls another with the size of the variables
% unchanged between the head and the (possibly indirect) recursive call.
% Any loops in the relation show possible non-termination. This predicate
% also checks that the calculated input variables are subsets of the actual
% input variables
:- pred termination_add_arcs_to_relation(pred_proc_id, list(termination_call), 
	bag(var), term_util__result(term_errors__error), 
	relation(pred_proc_id), relation(pred_proc_id)).
:- mode termination_add_arcs_to_relation(in, in, in, out, in, out) is det.
termination_add_arcs_to_relation(_PPid, [], _Vars, ok, Relation, Relation).
termination_add_arcs_to_relation(PPId, [X | Xs], Vars, Result, Relation0, 
		Relation) :-
	X = tuple(CalledPPId, Value, Bag, _Var, Context),
	( bag__is_subbag(Bag, Vars) ->
		compare(Res, Value, 0),
		( 
			Res = (>),
			Result = error(Context - 
				positive_value(PPId, CalledPPId)),
			Relation = Relation0
		;
			Res = (=),
			% Add the arc to the relation.
			relation__lookup_element(Relation0, PPId, Key),
			relation__lookup_element(Relation0, CalledPPId, 
				CalledKey),
			relation__add(Relation0, Key, CalledKey, Relation1),
			termination_add_arcs_to_relation(PPId, Xs, Vars, 
				Result, Relation1, Relation)
		;
			Res = (<),
			termination_add_arcs_to_relation(PPId, Xs, Vars, 
				Result, Relation0, Relation)
		)
	;
		Result = error(Context - not_subset(PPId, Bag, Vars)),
		Relation = Relation0
	).

:- pred add_pred_procs_to_relation(list(pred_proc_id), relation(pred_proc_id),
	relation(pred_proc_id)).
:- mode add_pred_procs_to_relation(in, in, out) is det.
add_pred_procs_to_relation([], Relation, Relation).
add_pred_procs_to_relation([PPId | PPIds], Relation0, Relation) :-
	relation__add_element(Relation0, PPId, _, Relation1),
	add_pred_procs_to_relation(PPIds, Relation1, Relation).

%-----------------------------------------------------------------------------%
% termination_goal is the main section of the analysis for pass 2.  It
% processes the goal of a single procedure, and returns a list of
% termination_call structures.  Each termination_call structure represents
% a single (mutually or directly) recursive call, and also tracks the
% relative size of the input variables in the recursive call, in comparison
% to the variables in the head.
:- type call_info --->
	call_info(
			% The pred_proc_id of the predicate that we are
			% currently processing.
		pred_proc_id, 
			% A map from each procedure in the current SCC to
			% the used-vars for that procedure.  It is used to
			% find whether or not a call is mutually recursive,
			% and to find the used-variables of the predicate
			% that is being called.
		map(pred_proc_id, set(var)), 
		bool % are we doing single argument analysis?
	).


:- pred termination_goal(hlds_goal_expr, hlds_goal_info, module_info, 
	unify_info, call_info, term_util__result(term_errors__error), 
	list(termination_call), list(termination_call)).
:- mode termination_goal(in, in, in, in, in, out, in, out) is det.

termination_goal(conj(Goals), 
		_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
	termination_conj(Goals, Module, UnifyInfo, CallInfo, Res, 
		Out0, Out).

% This processes calls when doing normal termination analysis (as opposed
% to single argument analysis).
termination_goal(call(CallPredId, CallProcId, Args, _IsBuiltin, _, _), 
		GoalInfo, Module, _UnifyInfo, call_info(PPId, UsedArgsMap, no), 
		Res, Out0, Out) :-
	PPId = proc(PredId, ProcId),
	CallPPId = proc(CallPredId, CallProcId),

	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
		CallProcInfo),

	proc_info_vartypes(ProcInfo, VarType),
	proc_info_argmodes(CallProcInfo, CallArgModes),
	proc_info_termination(CallProcInfo, CallTermination),
	CallTermination = term(CallTermConst, CallTerminates, CallUsedArgs, _),
	goal_info_get_context(GoalInfo, Context),

	partition_call_args(Module, CallArgModes, Args, InVars, OutVars),
	bag__from_list(InVars, InVarBag0),
	bag__from_list(OutVars, OutVarBag),

	( CallUsedArgs = yes(UsedVars) ->
		remove_unused_args(InVarBag0, Args, UsedVars,
			InVarBag1)
	;
		InVarBag1 = InVarBag0
	),

	% Step 1 - modify Out0
	( 
		CallTermConst = set(Int),
		termination_goal_modify_out(InVarBag1, OutVarBag, Int,
			Out0, Out1),
		Res0 = ok
	;
		CallTermConst = not_set,
		error("Unexpected Termination Constant in termination.m"),
		Res0 = ok,
		Out1 = Out0
	;
		CallTermConst = inf(_),
		( termination_goal_check_intersect(Out0, OutVarBag) ->
			% There is no intersection, so just continue
			Res0 = ok
		;
			Res0 = error(Context - 
				inf_termination_const(PPId, CallPPId))
		),
		Out1 = Out0
	),

	% Step 2 - do we add another arc?
	( CallTerminates = dont_know ->
		Res = error(Context - dont_know_proc_called(PPId, CallPPId)),
		Out = Out0
	; \+ check_horder_args(Args, VarType) ->
		Res = error(Context - horder_args(PPId, CallPPId)),
		Out = Out0
	;
		( map__search(UsedArgsMap, CallPPId, RecursiveUsedArgs) ->
			% The called procedure is in the map, so the call is
			% recursive - add it to Out.
			proc_info_headvars(CallProcInfo, HeadVars),
			termination_call_2(Args, HeadVars, 
				RecursiveUsedArgs, Bag),
			NewOutElem = tuple(CallPPId, 0, Bag, no, Context),
			Out = [ NewOutElem | Out1 ]
		;
			% The call is not recursive
			Out = Out1
		),
		Res = Res0
	).
	
termination_goal(call(CallPredId, CallProcId, Args, _IsBuiltin, _, _), 
		GoalInfo, Module, _UnifyInfo, 
		call_info(PPId, _UsedArgsMap, yes), Res, Out0, Out) :-
	PPId = proc(PredId, ProcId),
	CallPPId = proc(CallPredId, CallProcId),

	module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
	module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
		CallProcInfo),

	proc_info_vartypes(ProcInfo, VarType),
	proc_info_argmodes(CallProcInfo, CallArgModes),
	proc_info_headvars(CallProcInfo, HeadVars),
	proc_info_termination(CallProcInfo, CallTermination),
	CallTermination = term(_, CallTerminates, _CallUsedArgs, _),
	goal_info_get_context(GoalInfo, Context),

	partition_call_args(Module, CallArgModes, Args, InVars, OutVars),
	partition_call_args(Module, CallArgModes, HeadVars, InHeadVars, _),
	bag__from_list(OutVars, OutVarBag),

	% Step 1 - modify Out0
	( termination_goal_check_intersect(Out0, OutVarBag) ->
		% There is no intersection, so just continue.
		Res0 = ok,
		Out1 = Out0
	;
		% This analysis could be much better, but it will do for
		% now.
		Res0 = error(Context - call_in_single_arg(CallPPId)),
		Out1 = Out0
	),

	% Step 2 - do we add another arc?
	( CallTerminates = dont_know ->
		Res = error(Context - dont_know_proc_called(PPId, CallPPId)),
		Out = Out0
	; \+ check_horder_args(Args, VarType) ->
		Res = error(Context - horder_args(PPId, CallPPId)),
		Out = Out0
	;
		( CallPPId = PPId ->
			% The call is recursive - add it to Out
			termination_call(InVars, InHeadVars, PPId, 
				Context, Out1, Out)
		;
			% The call is not recursive
			Out = Out1
		),
		Res = Res0
	).

termination_goal(higher_order_call(_, _, _, _, _, _), 
		GoalInfo, _Module, _UnifyInfo, _CallInfo, Res, Out0, Out) :-
	goal_info_get_context(GoalInfo, Context),
	Res = error(Context - horder_call),
	Out = Out0.

termination_goal(switch(_Var, _CanFail, Cases, _StoreMap),
		_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
	termination_switch(Cases, Module, UnifyInfo, CallInfo, 
		Res, Out0, Out).

termination_goal(unify(_Var, _RHS, _UniMode, Unification, _Context),
		_GInfo, Module, UnifyInfo, _CallInfo, ok, Out0, Out) :-
	(
		Unification = construct(OutVar, ConsId, Args0, Modes0),
		UnifyInfo = VarTypes - FunctorInfo,
		map__lookup(VarTypes, OutVar, Type),
		% length(Args) is not necessarily equal to length(Modes)
		% for higher order constructions.
		( type_is_higher_order(Type, _, _) ->
			Out = Out0
		;
			( type_to_type_id(Type, TypeIdPrime, _) ->
				TypeId = TypeIdPrime
			;
				error("variable type in termination_goal")
			),
			functor_norm(FunctorInfo, TypeId, ConsId, Module,
				FunctorNorm, Args0, Args, Modes0, Modes),
			split_unification_vars(Args, Modes, Module, InVarBag, 
				OutVarBag0),
			bag__insert(OutVarBag0, OutVar, OutVarBag),
			termination_goal_modify_out(InVarBag, OutVarBag, 
				FunctorNorm, Out0, Out)
		)
	;
		Unification = deconstruct(InVar, ConsId, Args0, Modes0, _),
		UnifyInfo = VarTypes - FunctorInfo,
		map__lookup(VarTypes, InVar, Type),
		( type_to_type_id(Type, TypeIdPrime, _) ->
			TypeId = TypeIdPrime
		;
			error("variable type in termination analysis")
		),
		functor_norm(FunctorInfo, TypeId, ConsId, Module,
			FunctorNorm, Args0, Args, Modes0, Modes),
		split_unification_vars(Args, Modes, Module, InVarBag0,
			OutVarBag),
		bag__insert(InVarBag0, InVar, InVarBag),
		termination_goal_modify_out(InVarBag, OutVarBag, 
			(- FunctorNorm), Out0, Out)
	;
		Unification = assign(OutVar, InVar),
		bag__init(InitBag),
		bag__insert(InitBag, InVar, InVarBag),
		bag__insert(InitBag, OutVar, OutVarBag),
		termination_goal_modify_out(InVarBag, OutVarBag, 0, Out0, Out)
	;
		Unification = simple_test(_InVar1, _InVar2),
		Out = Out0
	;
		Unification = complicated_unify(_, _),
		error("Unexpected complicated_unify in term_pass2.m")
	).

termination_goal(disj(Goals, _StoreMap),
		_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
	termination_disj(Goals, Module, UnifyInfo, CallInfo, Res, Out0, Out).

termination_goal(not(GoalExpr - GoalInfo),
		_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
	termination_goal(GoalExpr, GoalInfo, Module, UnifyInfo, CallInfo, 
		Res, Out0, Out).

termination_goal(some(_Vars, GoalExpr - GoalInfo),
		_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
	termination_goal(GoalExpr, GoalInfo, Module, UnifyInfo, CallInfo, 
		Res, Out0, Out).

termination_goal(if_then_else(_Vars, CondGoal, ThenGoal, ElseGoal, _),
		_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
	CondGoal = CondExpr - CondGoalInfo,
	ThenGoal = ThenExpr - ThenGoalInfo,
	ElseGoal = ElseExpr - ElseGoalInfo,
	termination_goal(ThenExpr, ThenGoalInfo, Module, UnifyInfo, CallInfo, 
		ThenRes, Out0, ThenOut),
	termination_goal(ElseExpr, ElseGoalInfo, Module, UnifyInfo, CallInfo, 
		ElseRes, Out0, ElseOut),
	( ThenRes = error(_) ->
		Res = ThenRes,
		Out = ThenOut
	; ElseRes = error(_) ->
		Res = ElseRes,
		Out = ElseOut
	;
		% They both succeded - join the outs
		list__append(ThenOut, ElseOut, Out1),
		termination_goal(CondExpr, CondGoalInfo, Module, 
			UnifyInfo, CallInfo, Res, Out1, Out)
	).
	
termination_goal(pragma_c_code(_, _, CallPredId, CallProcId, Args, _, _, _),
		GoalInfo, Module, _UnifyInfo, _CallInfo, Res, Out, Out) :-
	module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
		CallProcInfo),
	proc_info_argmodes(CallProcInfo, CallArgModes),
	partition_call_args(Module, CallArgModes, Args, _InVars, OutVars),
	bag__from_list(OutVars, OutVarBag),
	( termination_goal_check_intersect(Out, OutVarBag) ->
		% c_code has no important output variables, so we 
		% dont need an error.
		Res = ok
	;
		goal_info_get_context(GoalInfo, Context),
		Res = error(Context - pragma_c_code)
	).

%-----------------------------------------------------------------------------%
% These following predicates all support termination_goal. 

:- pred termination_conj(list(hlds_goal), module_info, 
	unify_info, call_info, term_util__result(term_errors__error), 
	list(termination_call), list(termination_call)).
:- mode termination_conj(in, in, in, in, out, in, out) is det.
termination_conj([] , _Module, _UnifyInfo, _CallInfo, ok, Out, Out).
termination_conj([ Goal | Goals ], Module, UnifyInfo, CallInfo, 
		Res, Out0, Out) :-
	Goal = GoalExpr - GoalInfo,
	termination_conj(Goals, Module, UnifyInfo, CallInfo, 
		Res0, Out0, Out1),
	( Res0 = ok ->
		termination_goal(GoalExpr, GoalInfo, Module, 
			UnifyInfo, CallInfo, Res, Out1, Out)
	;
		Res = Res0,
		Out = Out1
	).

% Used by single argument analysis to make a seperate Out for each input
% variable in a recursive call.
:- pred termination_call(list(var), list(var), pred_proc_id, 
	term__context, list(termination_call), list(termination_call)).
:- mode termination_call(in, in, in, in, in, out) is det.
termination_call([], [], _, _, Out, Out).
termination_call([_|_], [], _, _, Out, Out) :-
	error("term_pass2__termination_call: Unmatched variables\n").
termination_call([], [_|_], _, _, Out, Out) :-
	error("term_pass2:termination_call: Unmatched variables\n").
termination_call([ Var | Vars ], [ HeadVar | HeadVars ], PPId, 
		Context, Outs0, Outs) :-
	bag__init(Bag0),
	bag__insert(Bag0, Var, Bag),
	Out = tuple(PPId, 0, Bag, yes(HeadVar), Context),
	termination_call(Vars, HeadVars, PPId, Context, 
		[Out | Outs0], Outs).

% Used to set the bag of input variables for a recursive call, according to
% the set of used arguments.
:- pred termination_call_2(list(var), list(var), set(var), bag(var)).
:- mode termination_call_2(in, in, in, out) is det.
termination_call_2([], [], _, Out) :-
	bag__init(Out).
termination_call_2([_|_], [], _, _Out) :-
	error("Unmatched vars in termination_call_2\n").
termination_call_2([], [_|_], _, _Out) :-
	error("Unmatched vars in termination_call_2\n").
termination_call_2([Var | Vars], [HeadVar | HeadVars], 
		UsedSet, OutBag) :-
	termination_call_2(Vars, HeadVars, UsedSet, OutBag0),
	( set__member(HeadVar, UsedSet) ->
		bag__insert(OutBag0, Var, OutBag)
	;
		OutBag = OutBag0
	).


:- pred termination_switch(list(case), module_info, 
	unify_info, call_info, term_util__result(term_errors__error), 
	list(termination_call), list(termination_call)).
:- mode termination_switch(in, in, in, in, out, in, out) is det.
termination_switch([] , _Module, _UnifyInfo, _CallInfo, ok, Out, Out) :-
    error("term_pass2:termination_switch: unexpected empty switch\n").
termination_switch([ Case | Cases ], Module, UnifyInfo, 
		CallInfo, Res, Out0, Out):-
	Case = case(_, Goal),
	Goal = GoalExpr - GoalInfo,

	( Cases = [] ->
		Res1 = ok,
		Out1 = Out0
	;
		termination_switch(Cases, Module, UnifyInfo, CallInfo, 
			Res1, Out0, Out1)
	),
	( Res1 = ok ->
		termination_goal(GoalExpr, GoalInfo, 
			Module, UnifyInfo, CallInfo, Res, Out0, Out2),
		list__append(Out1, Out2, Out)
	;
		Res = Res1,
		Out = Out1
	).

:- pred termination_disj(list(hlds_goal), module_info, 
	unify_info, call_info, term_util__result(term_errors__error), 
	list(termination_call), list(termination_call)).
:- mode termination_disj(in, in, in, in, out, in, out) is det.
termination_disj([] , _Module, _UnifyInfo, _CallInfo, ok, Out, Out):-
	( Out = [] ->
		true
	;
		error("term_pass2:termination_disj: Unexpected value after disjunction\n")
	).
termination_disj([ Goal | Goals ], Module, UnifyInfo, 
		CallInfo, Res, Out0, Out) :-
	Goal = GoalExpr - GoalInfo,

	( Goals = [] ->
		Res1 = ok, 
		Out1 = Out0
	;
		termination_disj(Goals, Module, UnifyInfo, CallInfo, 
			Res1, Out0, Out1)
	),
	( Res1 = ok ->
		termination_goal(GoalExpr, GoalInfo, Module, 
			UnifyInfo, CallInfo, Res, Out0, Out2),
		list__append(Out1, Out2, Out)
	;
		Res = Res1,
		Out = Out1
	).


:- pred termination_goal_check_intersect(list(termination_call), bag(var)).
:- mode termination_goal_check_intersect(in, in) is semidet.

% termination_goal_check_intersect succeeds if there is no intersection
% between any one of the Outs and the OutVarBag.
termination_goal_check_intersect([], _).
termination_goal_check_intersect([ Out | Outs ], OutVarBag) :-
	Out = tuple(_PPId, _Const, OutBag, _Var, _Context),
	\+ bag__intersect(OutBag, OutVarBag),
	termination_goal_check_intersect(Outs, OutVarBag).

:- pred termination_goal_modify_out(bag(var), bag(var), int, 
	list(termination_call), list(termination_call)).
:- mode termination_goal_modify_out(in, in, in, in, out) is det.
termination_goal_modify_out(_, _, _, [], []).
termination_goal_modify_out(InVars, OutVars, Off, 
		[Out0 | Out0s], [Out | Outs]):-
	Out0 = tuple(PPId, Int0, Vars0, Var, Context),
	( bag__intersect(OutVars, Vars0) ->
		% There is an intersection.
		bag__subtract(Vars0, OutVars, Vars1),
		bag__union(InVars, Vars1, Vars),
		Int = Int0 + Off,
		Out = tuple(PPId, Int, Vars, Var, Context)
	;
		% There is not an intersection.
		Out = Out0
	),
	termination_goal_modify_out(InVars, OutVars, Off, Out0s, Outs).








%-----------------------------------------------------------------------------
%
% 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 file contains utilities that are used by termination analysis.
%
%-----------------------------------------------------------------------------

:- module term_util.

:- interface.

:- import_module list, bool, bag, int, hlds_module, hlds_pred, hlds_data.
:- import_module term_errors, io, hlds_goal, term, prog_data, map.

	% term(TermConstant, Terminates, UsedArgs, MaybeError)
	%   TermConstant	See description below
	%   Terminates		See description below
	%   UsedArgs		This list of bool, when set, has a 1:1 
	%   			  correspondance with the arguments of the
	%   			  procedure. It stores whether the argument
	%   			  is used in producing the output
	%   			  arguments.  
	%   MaybeError		If the analysis fails to prove termination
	%   			  of a procedure, then this value indicates
	%   			  the reason that the analysis failed.
:- type termination 
	--->	 term(term_util__constant, terminates, maybe(list(bool)),
		maybe(term_errors__error)).

% term_util__constant defines the level by which a procedures arguments
% grow or shrink.  It is used to determine the termination properties of a 
% predicate.  The termination constant defines the relative sizes of input
% and output arguments in the following equation:
% | input arguments | + constant >= | output arguments |
% where | | represents a semilinear norm.
:- type term_util__constant
	--->	inf(term_errors__error)
				% The smallest constant that the analysis
				% could prove was valid is infinity.
				% Whenever a constant is set to infinity,
				% an error is associated with it which
				% states why the analysis failed to find a
				% smaller constant.
	;	not_set		% The termination constant has not been 
				% set yet.  After
				% term_pass1:proc_inequalities has been
				% run, the constant should be set for all
				% the procedures in the module.  Failure to
				% set the constant would indicate a
				% programming error.
	;	set(int).	% The termination constant has been 
				% set to int.

:- type terminates 	
	---> 	dont_know	% The analysis could not prove that the 
				% procedure terminates.
	;	not_set		% Each procedure has its `terminates' set 
				% set to not_set initially.
				% The termination analysis uses the fact
				% that if a procedure is called whose
				% terminates is not_set, then the call is
				% mutually recursive. (If the call is not
				% mutually recursive, then the analysis
				% will have already processed the
				% procedure, and would have set the
				% constant). term_pass2:termination should
				% set the terminates value of all
				% procedures.  Failure to do so indicates a
				% software error.
	;	yes.		% This procedure terminates for all 
				% possible inputs.

% The functor algorithm defines how a weight is assigned to each functor.
:- type functor_algorithm
	--->	simple		% simple assigns all non-constant 
				% functors a norm of 1.
	;	total		% All functors have a norm = arity of functor
			% Use the weight table to find the
			% weight of any constructor.
	;	use_map(weight_table)
			% Use the weight table, and use its bool list to
			% determine which arguments of any functor are to
			% be considered when calculating the norm of a
			% functor.
	;	use_map_and_args(weight_table).

:- type term_util__result(T) 
	--->	ok
	;	error(T).

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

% These types are used to assign functor weights to functor symbols
% The weight_info is assigned to a cons_id. weight(Integer, BoolList) gives
% the weight to assign to this functor symbol, and the BoolList states
% whether or not each argument of this functor should be used to calculate
% the size of the output.  That is, the BoolList has a 1:1 mapping with the
% arguments of the functor.
:- type weight_info	--->	weight(int, list(bool)).
:- type weight_table	==	map(pair(type_id, cons_id), weight_info).

% This predicate provides an initialised termination structure.
:- pred term_util__init(termination).
:- mode term_util__init(out) is det.

% This predicate calculates a weight table according to the following
% rules:
% If a type is directly recursive, its weight is given by the number of
% directly recursive arguments of this cons id.  For example, a list has
% size 1, a binary tree has size 2.  Each element of the bool list is
% assigned yes if the corresponding argument is directly recursive, and no
% otherwise.
% If a type is not directly recursive, then it is assigned a weight of 1,
% and the bool list is set to be all yes.
%
% If the bool list is used (by setting functor_algorithm to
% use_map_and_args), then the effect of this norm is that the size
% of a data structure is given by the number of data elements in the data
% structure.  If the bool list is ignored, then the size of all the
% arguments of any functor considered, then the size of a data structure is
% given by the total size of its data elements.
:- pred find_weights(module_info::in, weight_table::out) is det.

% This predicate is used to assign a norm (integer) to a functor, depending
% on its type. Depending on the functor_algorithm, this predicate may also
% modify the list of args and modes.
:- pred functor_norm(functor_info, type_id, cons_id, module_info,  int, 
	list(var), list(var), list(uni_mode), list(uni_mode)).
:- mode functor_norm(in, in, in, in, out, in, out, in, out) is det.

% This predicate should be called whenever a procedure needs its termination
% set to dont_know.  This predicate checks to see whether the termination
% is already set to dont_know, and if so it does nothing.  If the
% termination is set to yes, or not_set, it changes the termination to
% dont_know, and checks whether a 
% check_termination pragma has been defined for this predicate, and if so,
% this outputs a useful error message.
:- pred do_ppid_check_terminates(list(pred_proc_id), term_errors__error, 
	module_info, module_info, io__state, io__state).
:- mode do_ppid_check_terminates(in, in, in, out, di, uo) 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), list(bool), list(bool)).
:- mode term_util__make_bool_list(in, in, 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, list(mode), list(var), list(var),
	list(var)).
:- mode partition_call_args(in, in, in, out, 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.

% Given a list of pred_proc_ids, this predicate sets the termination
% constant of them all to the constant that is passed to it.
:- pred set_pred_proc_ids_const(list(pred_proc_id), term_util__constant,
	module_info, module_info).
:- mode set_pred_proc_ids_const(in, in, in, out) is det.

% Given a list of pred_proc_ids, this predicate sets the error and
% terminates value of them all to the values that are passed to the
% predicate.
:- pred set_pred_proc_ids_terminates(list(pred_proc_id), terminates,
	maybe(term_errors__error), module_info, module_info).
:- mode set_pred_proc_ids_terminates(in, in, in, in, out) is det.

% Fails if one or more variables in the list are higher order
:- pred check_horder_args(list(var), map(var, type)).  
:- mode check_horder_args(in, in) is semidet.	

% 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), list(uni_mode), module_info,
	bag(var), bag(var)).
:- mode split_unification_vars(in, in, in, out, out) is det.

:- implementation.

:- import_module map, std_util, require, mode_util, prog_out, type_util.
:- import_module globals, options, inst_match, assoc_list.

term_util__init(term(not_set, not_set, no, no)).

check_horder_args([], _).
check_horder_args([Arg | Args], VarType) :-
	map__lookup(VarType, Arg, Type),
	\+ type_is_higher_order(Type, _, _),
	check_horder_args(Args, VarType).

set_pred_proc_ids_const([], _Const, Module, Module).
set_pred_proc_ids_const([PPId | PPIds], Const, 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_termination(ProcInfo0, Termination0),

	Termination0 = term(_Const, Term, UsedArgs, MaybeError),
	Termination = term(Const, Term, UsedArgs, MaybeError),

	proc_info_set_termination(ProcInfo0, 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_const(PPIds, Const, Module1, Module).

set_pred_proc_ids_terminates([], _Terminates, _, Module, Module).
set_pred_proc_ids_terminates([PPId | PPIds], Terminates, MaybeError, 
		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_termination(ProcInfo0, Termination0),

	Termination0 = term(Const, _Terminates, UsedArgs, _),
	Termination = term(Const, Terminates, UsedArgs, MaybeError),

	proc_info_set_termination(ProcInfo0, 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_terminates(PPIds, Terminates, MaybeError, 
		Module1, Module).

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

% 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")
	).

partition_call_args(_, [], [_ | _], _, _) :-
	error("Unmatched variables in term_util:partition_call_args").
partition_call_args(_, [_ | _], [], _, _) :-
	error("Unmatched variables in term_util__partition_call_args").
partition_call_args(_, [], [], [], []).
partition_call_args(ModuleInfo, [ArgMode | ArgModes], [Arg | Args],
		InputArgs, OutputArgs) :-
	partition_call_args(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
	).


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

% 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(ConsIdMap), TypeId, ConsId, _Module, Int,
		Args, Args, Modes, Modes) :-
	( map__search(ConsIdMap, TypeId - ConsId, WeightInfo) ->
		WeightInfo = weight(Int, _)
	;
		Int = 0
	).
functor_norm(use_map_and_args(ConsIdMap), TypeId, ConsId, _Module, Int,
		Args0, Args, Modes0, Modes) :-
	( map__search(ConsIdMap, TypeId - ConsId, WeightInfo) ->
		WeightInfo = weight(Int, UseArgList),
		(
			functor_norm_remove_elems(UseArgList, Args0, Args1, 
				Modes0, Modes1)
		->
			Modes = Modes1,
			Args = Args1
		;
			error("Unmatched lists in term_util__functor_norm_remove_elems.")
		)
	;
		Int = 0,
		Modes = Modes0,
		Args = Args0
	).
		
% This predicate will fail if the length of the input lists are not matched.
:- pred functor_norm_remove_elems(list(bool), list(var), list(var),
	list(uni_mode), list(uni_mode)).
:- mode functor_norm_remove_elems(in, in, out, in, out) is semidet.
functor_norm_remove_elems([], [], [], [], []).
functor_norm_remove_elems([yes | Bools], [Arg0 | Args0], [Arg0 | Args], 
		[Mode0 | Modes0], [Mode0 | Modes]) :-
	functor_norm_remove_elems(Bools, Args0, Args, Modes0, Modes).
functor_norm_remove_elems([no | Bools], [_Arg0 | Args0], Args, 
		[_Mode0 | Modes0], Modes) :-
	functor_norm_remove_elems(Bools, Args0, Args, Modes0, Modes).
	


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

do_ppid_check_terminates([] , _Error, Module, Module) --> [].
do_ppid_check_terminates([ PPId | PPIds ], Error, Module0, Module) --> 
	% look up markers
	{ 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_termination(ProcInfo0, Termination0) },
	{ Termination0 = term(Const, Terminates, UsedArgs, _) },
	( { Terminates = dont_know } ->
		{ Module2 = Module0 }
	;
		{ Termination = term(Const, dont_know, UsedArgs, yes(Error)) },
		{ proc_info_set_termination(ProcInfo0, 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) },
		{ pred_info_get_marker_list(PredInfo, MarkerList) },
		globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
		% If a check_terminates pragma exists, print out an error
		% message.
		% Note that this allows the one error to be printed out
		% multiple times.  This is because one error can cause a
		% number of predicates to be non terminating, and if
		% check_terminates is defined on all of the predicates,
		% then the error is printed out for each of them.
		( 
			{ list__member(request(check_termination), MarkerList) }
		->
			term_errors__output(PredId, ProcId, Module1,
				Success),
			% Success is only no if there was no error
			% defined for this predicate.  As we just set the
			% error, term_errors__output should succeed.
			{ require(unify(Success, yes), "term_util.m: Unexpected value in do_ppid_check_terminates") },
			io__set_exit_status(1),
			{ module_info_incr_errors(Module1, Module2) }
		; % else if
			{ \+ pred_info_is_imported(PredInfo) },
			% 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 }
			;
				{ Error = _Context - TermError },
				{ \+ simple_error(TermError) }
			)
		->
			term_errors__output(PredId, ProcId, Module1,
				Success),
			% Success is only no if there was no error
			% defined for this predicate.  As we just set the
			% error, term_errors__output should succeed.
			{ require(unify(Success, yes), "term_util.m: Unexpected value in do_ppid_check_terminates") },
			{ Module2 = Module1 }
		;
			% Even though the predicate does not terminate, no
			% warning has been requested for it.
			{ Module2 = Module1 }
		)
	),
	do_ppid_check_terminates(PPIds, Error, Module2, Module).

%----------------------------------------------------------------------------%
%----------------------------------------------------------------------------%
% This predicate calculates a weight table according to the following
% rules:
% If a type is directly recursive, its weight is given by the number of
% directly recursive arguments of this cons id.  For example, a list has
% size 1, a binary tree has size 2.  Each element of the bool list is
% assigned yes if the corresponding argument is directly recursive, and no
% otherwise.
% If a type is not directly recursive, then it is assigned a weight of 1,
% and the bool list is set to be all yes.
%
% If the bool list is used, then the effect of this norm is that the size
% of a data structure is given by the number of data elements in the data
% structure.  If the bool list is ignored, and the size of all the
% arguments are considered, then the size of a data structure is given by
% the total size of its data elements.

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








%-----------------------------------------------------------------------------%
%
% Copyright (C) 1997 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%
%
% term_errors.m
% Main author: crs.
% 
% This module prints out the various error messages that are produced by
% termination.m
%
%-----------------------------------------------------------------------------%

:- module term_errors.

:- interface.
:- import_module io, bag, std_util, term, list, bool.
:- import_module hlds_module.

% term_errors__output(PredId, ProcId, Module, Success, IO0, IO).
% 	This is used to print out the errors found by termination analysis.
% 	Success returns yes if an error was successfully printed out.
% 	Success will be no if there was no termination error for that
% 	procedure.
:- pred term_errors__output(pred_id, proc_id, module_info, bool,
		io__state, io__state).
:- mode term_errors__output(in, in, in, out, di, uo) is det.


% term_errors__output_const_error(PredId, ProcId, Module, Success, IO0, IO).
% 	This prints out any errors which occured when trying to set the
% 	termination constant.  An error message will only be available if
% 	the termination constant is set to 'inf'.
% 	Success returns yes if an error was successfully printed out.
% 	Success will be no if there was no termination error for that
% 	procedure.
:- pred term_errors__output_const_error(pred_id, proc_id, module_info, bool,
		io__state, io__state).
:- mode term_errors__output_const_error(in, in, in, out, di, uo) is det.

% This is used to print out error messages for the hlds dumps.  These are
% much more concise than the normal error messages.
:- pred term_errors__output_hlds(pred_id, proc_id, module_info, 
	io__state, io__state).
:- mode term_errors__output_hlds(in, in, in, di, uo) is det.

:- type term_errors__error == pair(term__context, termination_error).
% With these error messages, they do not necessarily need to involve the
% procedure that they are assigned to.  It is possible that an error
% occured when processing other predicates in the same SCC, and therefore
% the termination (or termination constant) of this predicate was set to
% dont_know (or infinity), even though the error occured in a different
% predicate.
:- type termination_error
			% A recursive call is made with variables that are 
			% strictly larger than in the head.  Note that 
			% the recursive call may be indirect, so this does 
			% not neccessarily indicate non-termination.
			% The first PPId is the calling proc.  The second
			% PPId is the called procedure.
	--->	positive_value(pred_proc_id, pred_proc_id)
	;	horder_call
	;	pragma_c_code
	;	imported_pred
			% dont_know_proc_called(CallerProc, CalleeProc)  
			% A call was made from CallerProc to CalleeProc,
			% where the termination constant of the CalleeProc
			% is set to dont_know.
	;	dont_know_proc_called(pred_proc_id, pred_proc_id)
			% horder_args(CallerProc, CalleeProc)
			% This error message indicates that the CallerProc
			% called the CalleeProc where some of the arguments
			% are of a higher order type.
	;	horder_args(pred_proc_id, pred_proc_id)
	;	inf_termination_const(pred_proc_id, pred_proc_id)
			% not_subset(Proc, SupplierVariables, InHeadVariables)
			% This error occurs when the Supplier variables
			% (either Recursive-input suppliers or Output
			% suppliers, depending on whether the error was
			% associated with a dont_know or with a constant of
			% infinity) is not a subset of the input head
			% variables.
	;	not_subset(pred_proc_id, bag(var), bag(var))
	;	not_dag
	;	no_eqns
	;	lpsolve_failed(eqn_soln)
	;	call_in_single_arg(pred_proc_id)
			% single argument analysis did not find a head
			% variable that was decreasing in size. 
	;	single_arg_failed(term_errors__error)
			% single_arg_failed(ReasonForNormalAnalysisFailing,
			% 	ReasonForSingleArgAnalysisFailing)
	;	single_arg_failed(term_errors__error, term_errors__error)
			% the termination constant of a builtin predicate
			% is set to infinity if the types of the builtin
			% predicate may have a norm greater than 0.
	;	is_builtin
	;	does_not_term_pragma(pred_id).

% eqn_soln are used to report the results from solving the equations
% created in the first pass.  The first 4 (optimal - failure) represent
% output states from lp_solve. 
:- type eqn_soln
	---> 	optimal		
	;	infeasible
	;	unbounded
	;	failure
	;	fatal_error 	% unable to open a file, or make a system call
	;	parse_error	% unable to parse the output from lp_solve
	;	solved(list(pair(pred_proc_id, int))).

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

:- implementation.

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

simple_error(horder_call).
simple_error(pragma_c_code).
simple_error(imported_pred).
simple_error(dont_know_proc_called(_, _)).
simple_error(call_in_single_arg(_)).
simple_error(horder_args(_, _)).
simple_error(single_arg_failed(_Context - Error)) :- simple_error(Error).
simple_error(single_arg_failed(_Con1 - Err1, _Con2 - Err2)) :-
	simple_error(Err1), simple_error(Err2).
simple_error(does_not_term_pragma(_)).

term_errors__output(PredId, ProcId, Module, Success) -->
	{ module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo) },
	{ proc_info_termination(ProcInfo, Termination) },
	{ Termination = term(_Const, _Terminates, _UsedArgs, MaybeError) },
	( { MaybeError = yes(Context - Error) } ->
		prog_out__write_context(Context),
		io__write_string("Termination of "),
		hlds_out__write_pred_id(Module, PredId),
		io__nl,
		prog_out__write_context(Context),
		io__write_string("  not proved because "),
		{ ConstErrorOutput = no },
		{ ForHLDSDump = no },
		term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput,
			ForHLDSDump, Context - Error),
		{ Success = yes }
	;
		{ Success = no }
	).

term_errors__output_const_error(PredId, ProcId, Module, Success) -->
	{ module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo) },
	{ proc_info_termination(ProcInfo, Termination) },
	{ Termination = term(Const, _Terminates, _UsedArgs, _MaybeError) },
	( { Const = inf(Context - Error) } ->
		prog_out__write_context(Context),
		io__write_string("Termination constant of "),
		hlds_out__write_pred_id(Module, PredId),
		io__nl,
		prog_out__write_context(Context),
		io__write_string("  set to infinity because "),
		{ ConstErrorOutput = yes },
		{ ForHLDSDump = no },
		term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput,
			ForHLDSDump, Context - Error),
		{ Success = yes }
	; 
		{ Success = no }
	).

term_errors__output_hlds(PredId, ProcId, Module) -->
	{ module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo) },
	{ proc_info_termination(ProcInfo, Termination) },
	{ Termination = term(Const, _Terminates, _UsedArgs, MaybeError) },
	{ ForHLDSDump = yes },
	( { MaybeError = yes(TermContext - TermError) } ->
		io__write_string("% "),
		prog_out__write_context(TermContext),
		io__write_string("Termination not proved because "),
		{ ConstErrorOutput0 = no },
		term_errors__output_2(PredId,ProcId, Module, ConstErrorOutput0,
			ForHLDSDump, TermContext - TermError)
	;
		[]
	),
	( { Const = inf(ConstContext - ConstError) } ->
		io__write_string("% "),
		prog_out__write_context(ConstContext),
		io__write_string("Termination const set to inf because "),
		{ ConstErrorOutput1 = yes },
		term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput1,
			ForHLDSDump, ConstContext - ConstError)
	;
		[]
	).
	

:- pred term_errors__output_same_SCC(pred_id, module_info, term__context,
	bool, io__state, io__state).
:- mode term_errors__output_same_SCC(in, in, in, in, di, uo) is det.
term_errors__output_same_SCC(PredId, Module, Context, ForHLDSDump) -->
	io__write_string("it is in the same SCC as the\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  "),
	hlds_out__write_pred_id(Module, PredId).


% term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput,
% 	ForHLDSDump, Error, IO0, IO).
% If this predicate is called from term_errors__output_const_error, then
% ConstErrorOutput should be set to `yes' to indicate that the error
% message should describe why the constant was set to infinity.
% If ConstErrorOutput is set to `no' then term_errors__output_2 describes
% why the analysis could not prove termination.
%
% If ForHLDSDump is set to yes, then a % must be placed at the beginning of
% each line, because the output is for the HLDS dump.
% 
% This predicate is used by both term_errors__output() and
% term_errors__output_const_error() to print out the reason for the error.
% Before calling output_2, term_errors__output prints out:
% myfile.m:300: Termination of predicate `myfile:yourpredicate/3' 
% myfile.m:300:   not proved because 
%
% and term_errors__output_const_error prints out:
% myfile.m:300: Termination constant of function `myfile:myfunction/6' 
% myfile.m:300:   set to infinity because 
%
:- pred term_errors__output_2(pred_id, proc_id, module_info, bool, bool,
	term_errors__error, io__state, io__state).
:- mode term_errors__output_2(in, in, in, in, in, in, di, uo) is det.
term_errors__output_2(PredId, _ProcId, Module, _ConstErrorOutput, ForHLDSDump,
		Context - positive_value(CallerPPId, CalledPPId)) -->	
	{ CalledPPId = proc(CalledPredId, _CalledProcId) },
	{ CallerPPId = proc(CallerPredId, _CallerProcId) },
	( { PredId = CallerPredId } ->
		io__write_string("it contains a ")
	;
		term_errors__output_same_SCC(PredId, Module, Context, 
			ForHLDSDump),
		io__write_string(" which contains a ")
	),
	( { PredId = CalledPredId } ->
		io__write_string("directly\n"),
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(Context),
		io__write_string("  recursive call ")
	;
		io__write_string("recursive\n"),
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(Context),
		io__write_string("call to "),
		hlds_out__write_pred_id(Module, CalledPredId),
		io__nl,
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(Context),
		io__write_string("  ")
	),
	io__write_string("with the size of the variables increased.\n").

term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrOutput, _ForHLDSDump,
		_Context - horder_call) -->
	io__write_string("it contains a higher order call\n").

term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrOutput, _ForHLDSDump,
		_Context - pragma_c_code) -->
	io__write_string("it contains a pragma c_code() declaration\n").

term_errors__output_2(PredId, _ProcId, Module, _ConstErrorOutput, ForHLDSDump,
		Context - dont_know_proc_called(CallerPPId, CalleePPId)) -->
	{ CallerPPId = proc(CallerPredId, _CallerProcId) },
	{ CalleePPId = proc(CalleePredId, _CalleeProcId) },
	( { PredId = CallerPredId } ->
		io__write_string("it calls the ")
	;
		term_errors__output_same_SCC(CallerPredId, Module, Context,
			ForHLDSDump),
		io__write_string("which calls the ")
	),
	io__nl,
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  "),
	hlds_out__write_pred_id(Module, CalleePredId),
	io__nl,
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  which could not be proved to terminate\n").

term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrOutput, _ForHLDSDump,
		_Context - imported_pred) -->
	io__write_string("it was imported.\n").

term_errors__output_2(PredId, _ProcId, Module, _ConstErrorOutput, ForHLDSDump,
		Context - horder_args(CallerPPId, CalleePPId)) -->
	% OtherPPId may refer to the current Predicate, or it may refer to
	% another predicate in the same SCC
	{ CallerPPId = proc(CallerPredId, _CallerProcId) },
	{ CalleePPId = proc(CalleePredId, _CalleeProcId) },

	( { PredId = CallerPredId } ->
		io__write_string("it calls the ")
	;
		term_errors__output_same_SCC(CallerPredId, Module, Context,
			ForHLDSDump),
		io__write_string("which calls the")
	),
	io__nl,
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  "),
	hlds_out__write_pred_id(Module, CalleePredId),
	io__nl,
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string(
		"  where the call contains higher order argument(s)\n").

term_errors__output_2(PredId, _ProcId, Module, ConstErrorOutput, ForHLDSDump,
		Context - inf_termination_const(CallerPPId, CalleePPId)) -->
	{ CallerPPId = proc(CallerPredId, _CallerProcId) },
	{ CalleePPId = proc(CalleePredId, CalleeProcId) },
	( { PredId = CallerPredId } ->
		io__write_string("it calls the ")
	;
		term_errors__output_same_SCC(CallerPredId, Module, Context,
			ForHLDSDump),
		io__write_string("which calls the ")
	),
	io__nl,
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  "),
	hlds_out__write_pred_id(Module, CalleePredId),
	io__nl,
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string(
		"  which has a termination constant of infinity\n"),
	( 
		{ ForHLDSDump = no },
		{ ConstErrorOutput = no }
	->
		{ module_info_pred_proc_info(Module, CalleePredId, 
			CalleeProcId, _, CalleeProcInfo) },
		{ proc_info_termination(CalleeProcInfo, CalleeTermination) },
		{ CalleeTermination = term(CalleeConst, _, _, _) },
		globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
		(
			{ CalleeConst = inf(CalleeContext - CalleeConstError)},
			( 
				{ \+ simple_error(CalleeConstError) }
			;	
				{ VerboseErrors = yes }
			)
		->
			maybe_write_string(ForHLDSDump, "% "),
			prog_out__write_context(CalleeContext),
			io__write_string("  The termination constant of that predicate was set to\n"),
			maybe_write_string(ForHLDSDump, "% "),
			prog_out__write_context(CalleeContext),
			io__write_string("  infinity because "),
			{ NewConstErrorOutput = yes },
			term_errors__output_2(CalleePredId, CalleeProcId, 
				Module, NewConstErrorOutput, ForHLDSDump, 
				CalleeContext - CalleeConstError)
		;
			[]
		) 
	;
		[]
	).

% If hlds dump, should print out variables in numerical form
% If verbose errors requested (-E), should list variables
term_errors__output_2(PredId, _ProcId, Module, ConstErrorOutput, ForHLDSDump,
		Context - not_subset(OtherPPId, 
		SupplierVarsBag, HeadVarsBag)) -->
	{ OtherPPId = proc(OtherPredId, OtherProcId) },
	{ module_info_pred_proc_info(Module, OtherPredId, OtherProcId, 
		OtherPredInfo, OtherProcInfo) },
	{ pred_info_get_is_pred_or_func(OtherPredInfo, OtherPredOrFunc) },
	( { OtherPredId = PredId } ->
		[]
	;
		term_errors__output_same_SCC(OtherPredId, Module, Context,
			ForHLDSDump),
		( { ConstErrorOutput = yes } ->
			io__write_string(
				". The termination constant of that\n"),
			maybe_write_string(ForHLDSDump, "% "),
			prog_out__write_context(Context),
			io__write_string("  "),
			hlds_out__write_pred_or_func(OtherPredOrFunc),
			io__write_string(" was set to infinity because ")
		;
			io__write_string(". Termination of that\n"),
			maybe_write_string(ForHLDSDump, "% "),
			prog_out__write_context(Context),
			io__write_string("  "),
			hlds_out__write_pred_or_func(OtherPredOrFunc),
			io__write_string(" could not be proved because ")
		)
	),
	io__write_string("the analysis\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  found that the set of "),
	( { ConstErrorOutput = yes } ->
		io__write_string("output ")
	;
		io__write_string("recursive input ")
	),
	io__write_string("supplier variables\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  was not a subset of the head variables of the "),
	hlds_out__write_pred_or_func(OtherPredOrFunc),
	io__write_string(".\n"),
		% Print out the variables as calculated.
	{ proc_info_variables(OtherProcInfo, VarSet) },
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  The "),
	( { ConstErrorOutput = yes } ->
		io__write_string("output ")
	;
		io__write_string("recursive input ")
	),
	io__write_string("supplier variables are\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  "),
	{ bag__to_list(SupplierVarsBag, SupplierVars) },
	mercury_output_vars(SupplierVars, VarSet, no),
	io__nl,
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  The input head variables are\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  "),
	{ bag__to_list(HeadVarsBag, HeadVars) },
	mercury_output_vars(HeadVars, VarSet, no),
	io__nl.

term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrorOutput, ForHLDSDump,
		Context - not_dag) -->
	io__write_string("there was a cycle in the call graph of\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string(
		"  this SCC where the variables did not decrease in size\n").

term_errors__output_2(_PredId, _ProcId, _Module, ConstErrorOutput, ForHLDSDump,
		Context - no_eqns)-->
	{ require(unify(ConstErrorOutput, yes),
		"Unexpected value in term_errors__output_2(no_eqns)") },
	io__write_string("the analysis was unable to form any\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string(
		"  constraints between the arguments of the predicates\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  and functions in this SCC\n").

term_errors__output_2(_PredId, _ProcId, _Module, _ConstErrorOutput, ForHLDSDump,
		Context - lpsolve_failed(Reason)) -->
	io__write_string("the constraint solver "),
	(
 		{ Reason = optimal },
		{ error("term_errors:output_2 Unexpected return value from lp_solve") }
	;
		{ Reason = infeasible },
		io__write_string("found the\n"),
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(Context),
		io__write_string("  constraints that the analysis produced to be infeasible\n")
	;
		{ Reason = unbounded },
		io__write_string("found that the\n"),
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(Context),
		io__write_string(
			"  constraints were not strong enough to put a\n"),
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(Context),
		io__write_string(
			"  bound on the value of the change constants\n")
	;
		{ Reason = failure },
		io__write_string("was unable to\n"),
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(Context),
		io__write_string(
			"  solve the constraints that were produced\n")
	;
		{ Reason = fatal_error },
		io__set_exit_status(1),
		io__write_string("was unable to create and/or\n"),
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(Context),
		io__write_string("  remove the temporary files it required\n")
	;
		{ Reason = parse_error },
		{ error("term_errors:output_2 Unexpected return value from lp_solve") }
	;
		{ Reason = solved(_) },
		{ error("term_errors:output_2 Unexpected return value from lp_solve") }
	).

% call_in_single_arg will only be printed out as the second part of the
% single_arg_failed(NormErr, SingleErr) error.  Therefore, the following
% lines have already been printed out:
% Single argument termination analysis failed to
% prove termination because 
term_errors__output_2(_PredId, _ProcId, Module, _ConstErrorOutput, ForHLDSDump,
		Context - call_in_single_arg(PPId)) -->
	{ PPId = proc(CallPredId, _CallProcId) },
	io__write_string("it encountered a call to\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  "),
	hlds_out__write_pred_id(Module, CallPredId),
	io__nl,
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  which could not be processed.\n").

term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput, ForHLDSDump,
		Context - single_arg_failed(Error)) -->
	term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput, 
		ForHLDSDump, Error),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string(
		"  Single argument analysis failed to find a head variable\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  that was always decreasing in size.\n").

term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput, ForHLDSDump, 
		_Context - single_arg_failed(NormErr, SingleArgErr)) -->
	{ NormErr = NormalContext - NormalError }, 
	{ SingleArgErr = SingleArgContext - SingleArgError },

		% single argument analysis is independent of finding the
		% termination constant.  The error for a termination
		% constant should never be single_arg_failed.
	{ require(unify(ConstErrorOutput, no),
		"Unexpected value in term_errors__output_2") },

	term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput, 
		ForHLDSDump, NormalContext - NormalError),
	globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
	( 
		{ SingleArgError \= NormalError },
		{ VerboseErrors = yes }
	->
		% Only output a single argument error if verbose errors are
		% enabled, and it is different from the normal error
		% message.
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(SingleArgContext),
		io__write_string(
			"  Single argument termination analysis failed to\n"),
		maybe_write_string(ForHLDSDump, "% "),
		prog_out__write_context(SingleArgContext),
		io__write_string("  prove termination because "),
		term_errors__output_2(PredId, ProcId, Module, ConstErrorOutput, 
			ForHLDSDump, SingleArgContext - SingleArgError)
	;
		[]
	).

term_errors__output_2(_PredId, _ProcId, _Module, ConstErrorOutput, _ForHLDSDump,
		_Context - is_builtin) -->
	{ require(unify(ConstErrorOutput, yes), 
		"Unexpected value in term_errors:output_2") },
	io__write_string("it is a builtin predicate\n").

term_errors__output_2(PredId, _ProcId, Module, ConstErrorOutput, ForHLDSDump,
		Context - does_not_term_pragma(OtherPredId)) -->
	{ require(unify(ConstErrorOutput, no), 
		"Unexpected value in term_errors:output_2") },
	io__write_string("there was a `does_not_terminate'\n"),
	maybe_write_string(ForHLDSDump, "% "),
	prog_out__write_context(Context),
	io__write_string("  pragma defined on "),
	( { PredId = OtherPredId } ->
		{ module_info_pred_info(Module, PredId, PredInfo) },
		{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
		io__write_string("this "),
		hlds_out__write_pred_or_func(PredOrFunc),
		io__nl
	;
		io__write_string("the "),
		hlds_out__write_pred_id(Module, OtherPredId),
		io__nl
	).