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

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


For review by anyone.

Below is the first part of the new termination analyser.  The
purpose of this diff is chiefly to add the argument size analyser,
the termination checker included in this diff is just a placeholder;
I intend to replace at some point.

For those that are curious the new analyser currently proves termination
of about 47% of the procedures exported from the standard library, which
is identical to the old analyser (without single argument analysis
enabled - the old analyser does better with single argument analysis).
For the rest of the compiler I only have figures for the new analyser:

	compiler   - 44.6%
	mdbcomp    - 64%
	browser    - 46%
	analysis   - 19.4% (**)

This, again, is the percentage of exported predicates (the figures
were obtained by looking at the .trans_opt files).

** The modules in this directory make extensive use of typeclasses,
   which neither termination analyser can handle (at the moment).

Julien.


Estimated hours taken: lots
Branches: main

Add the first part of the new termination analyser.  This includes most
of the argument size analyser and a simple termination checker - I'll
add a more extensive one as part of another diff.  The one included here
is only a placeholder and is roughly equivalent to the one used by the
existing termination analyser.

The new analysis abstracts term size relationships over a domain of
(rational) convex constraints.  The resulting size relationships are, in
many cases, more precise than we can obtain with the old analysis.  This
means that we should be able to prove termination in more cases.  The
tradeoff for this increased precision is that the new termination
analysis is slower than the old one.  We should also be able to adapt
the new analyser to handle things like higher-order constructs and
intermodule mutual recursion more easily than the old one.

The code for writing termination2_info pragmas to .opt and .trans_opt
files is currently commented out.  It will need to stay that way until
after this change bootstraps and after the tests/term directory as been
reworked (the .trans_opt_exp files need to updated and some new test
cases have to added - I'll do this as part of separate diff).

It isn't clear what the relationship between the new analyser and the
existing one should be, so at the moment they are as independent of each
other as possible.

compiler/termination2.m:
	New file.  Invokes the the other passes of the new analysis
	and handles the output termination2_info pragmas to .opt
	and .trans_opt files.

	XXX I've disable the writing out of termination2_info
	pragmas to the (transitive-)intermodule optimization files
	until I've updated the test suite.

compiler/term_constr_data.m:
	New file.  Defines the main data structures used by the
	new analysis.

compiler/term_constr_initial.m:
	New file.  Sets up information for builtin and compiler
	generated procedures and process information about
	imported procedures.  Also handles termination pragmas.

compiler/term_constr_build.m:
	New file.  Converts the HLDS representation of a procedure
	into the abstract representation that we use during the rest
	of the analysis.

compiler/term_constr_fixpoint.m:
	New file.  Perform a fixpoint calculation in order to derive
	interargument size relationships for a procedure (in the
	form of convex constraints).

compiler/term_constr_pass2.m:
	New file.  A rudimentary termination checker that is roughly
	equivalent to what the existing termination analysis does.
	This is just a placeholder.

compiler/term_constr_util.m:
	New file.  Utility predicates that are used by the above modules.

compiler/term_constr_errors.m:
	New file.  Equivalent to term_errors.m for the new analyser.

compiler/rat.m:
	Provide rational numbers over fixed precision integers.
	Originally committed on the termination2 branch.

compiler/lp_rational.m:
	Provides the necessary machinery for manipulating systems
	of linear constraints.  Originally committed on the termination2
	branch although most of this version new.  (Some bits of the
	version on the termination2 branch are now in polyhedron.m).
	The linear solver is essentially the one that is currently
	in lp.m converted to use rationals rather than floats.

compiler/polyhedron.m:
	New file.  An ADT that provides convex polyhedra over the
	rationals (or at least over rats).  The abstraction barrier was
	designed so that we could experiment with different representations
	for the polyhedra.

compiler/term_norm:
	Clean up the documentation of this module.
	Make set_functor_info into a function.
	Add a function for finding a lower bound on the weight of a functor.

compiler/trans_opt.m:
	Output termination2_info pragmas in .trans_opt files.

compiler/transform_hlds.m:
	Include the new termination analyser.

compiler/goal_form.m:
	When checking whether a goal can loop or not use
	information form the new termination analyser as well as
	the old one.

compiler/globals.m:
compiler/handle_options:
compiler/options.m:
	Add options to control the new analyser.  The documentation
	is currently commented out.

	XXX The user guide still needs to be updated.

compiler/hlds_out.m:
	Add hlds_out.write_pred_proc_id/4.

compiler/hlds_pred.m:
	Add a slot in the proc_sub_info structure for the
	termination2_info structure.

compiler/rat.m:
	Provide rational numbers over fixed precision integers.

compiler/lp_rational.m:
	Provide the constraint machinery required by the analyser.

compiler/make_hlds.m:
	Handle imports of termination2_info pragmas.

compiler/mercury_compile.m:
	Run the new pass.  Currently, we do this directly after
	the old termination analysis pass.

compiler/mercury_to_mercury.m:
	Add code to output termination2_info pragmas.

compiler/libs.m:
	Include the rat, polyhedron and lp_rational modules.

compiler/prog_data.m:
	Define the types necessary for termination2_info pragmas.

	Make the cannot_loop constructor of the generic_termination_info type
	have a polymorphic argument.  The new analyser stores information
	in it.

	Fix some spelling errors in some of the comments

compiler/prog_io_pragma.m:
	Parse termination2_info pragmas.

compiler/error_util.m:
	Add function versions of sorry/2 and unexpected/2.

compiler/module_qual.m:
compiler/modules.m:
compiler/recompilation.version.m:
	Minor changes caused by the above.

Workspace:/home/earth/juliensf/ws-term2/
Index: compiler/error_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/error_util.m,v
retrieving revision 1.34
diff -u -r1.34 error_util.m
--- compiler/error_util.m	24 Mar 2005 02:00:24 -0000	1.34
+++ compiler/error_util.m	24 Mar 2005 02:26:54 -0000
@@ -146,6 +146,7 @@
 	% Use this for features that should be implemented (or at
 	% least could be implemented).
 	%
+:- func sorry(string, string) = _ is erroneous.
 :- pred sorry(string::in, string::in) is erroneous.

 	% unexpected(ModuleName, Message)
@@ -154,6 +155,7 @@
 	% Use this to handle cases which are not expected to arise (i.e.
 	% bugs).
 	%
+:- func unexpected(string, string) = _ is erroneous.
 :- pred unexpected(string::in, string::in) is erroneous.

 	% Record the fact that a warning has been issued; set the exit status
@@ -662,11 +664,13 @@

 	% Call error/1 with a "Sorry, not implemented" message.
 	%
+sorry(Module, What) = _ :- sorry(Module, What).
 sorry(Module, What) :-
 	string__format("%s: Sorry, not implemented: %s",
 		[s(Module), s(What)], ErrorMessage),
 	error(ErrorMessage).

+unexpected(Module, What) = _ :- unexpected(Module, What).
 unexpected(Module, What) :-
 	string__format("%s: Unexpected: %s",
 		[s(Module), s(What)], ErrorMessage),
Index: compiler/globals.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/globals.m,v
retrieving revision 1.66
diff -u -r1.66 globals.m
--- compiler/globals.m	24 Mar 2005 02:00:26 -0000	1.66
+++ compiler/globals.m	24 Mar 2005 02:26:54 -0000
@@ -120,7 +120,7 @@
 	% Access predicates for the `globals' structure.

 :- pred globals__init(option_table::di, compilation_target::di, gc_method::di,
-	tags_method::di, termination_norm::di,
+	tags_method::di, termination_norm::di, termination_norm::di,
 	trace_level::di, trace_suppress_items::di,
 	maybe_thread_safe::di, globals::uo) is det.

@@ -132,6 +132,8 @@
 :- pred globals__get_tags_method(globals::in, tags_method::out) is det.
 :- pred globals__get_termination_norm(globals::in, termination_norm::out)
 	is det.
+:- pred globals__get_termination2_norm(globals::in, termination_norm::out)
+	is det.
 :- pred globals__get_trace_level(globals::in, trace_level::out) is det.
 :- pred globals__get_trace_suppress(globals::in, trace_suppress_items::out)
 	is det.
@@ -192,7 +194,7 @@
 	% io__state using io__set_globals and io__get_globals.

 :- pred globals__io_init(option_table::di, compilation_target::in,
-	gc_method::in, tags_method::in,
+	gc_method::in, tags_method::in, termination_norm::in,
 	termination_norm::in, trace_level::in, trace_suppress_items::in,
 	maybe_thread_safe::in, io::di, io::uo) is det.

@@ -207,7 +209,12 @@
 :- pred globals__io_get_tags_method(tags_method::out, io::di, io::uo) is det.
 :- pred globals__io_get_termination_norm(termination_norm::out,
 	io::di, io::uo) is det.
+
+:- pred globals__io_get_termination2_norm(termination_norm::out,
+	io::di, io::uo) is det.
+
 :- pred globals__io_get_trace_level(trace_level::out, io::di, io::uo) is det.
+
 :- pred globals__io_get_trace_suppress(trace_suppress_items::out,
 	io::di, io::uo) is det.
 :- pred globals__io_get_maybe_thread_safe(maybe_thread_safe::out,
@@ -327,6 +334,7 @@
 			gc_method 		:: gc_method,
 			tags_method 		:: tags_method,
 			termination_norm 	:: termination_norm,
+			termination2_norm	:: termination_norm,
 			trace_level 		:: trace_level,
 			trace_suppress_items	:: trace_suppress_items,
 			source_file_map		:: maybe(source_file_map),
@@ -335,9 +343,10 @@
 		).

 globals__init(Options, Target, GC_Method, TagsMethod,
-		TerminationNorm, TraceLevel, TraceSuppress, MaybeThreadSafe,
+		TerminationNorm, Termination2Norm, TraceLevel, TraceSuppress,
+		MaybeThreadSafe,
 	globals(Options, Target, GC_Method, TagsMethod,
-		TerminationNorm, TraceLevel, TraceSuppress,
+		TerminationNorm, Termination2Norm, TraceLevel, TraceSuppress,
 		no, no, MaybeThreadSafe)).

 globals__get_options(Globals, Globals ^ options).
@@ -345,6 +354,7 @@
 globals__get_gc_method(Globals, Globals ^ gc_method).
 globals__get_tags_method(Globals, Globals ^ tags_method).
 globals__get_termination_norm(Globals, Globals ^ termination_norm).
+globals__get_termination2_norm(Globals, Globals ^ termination2_norm).
 globals__get_trace_level(Globals, Globals ^ trace_level).
 globals__get_trace_suppress(Globals, Globals ^ trace_suppress_items).
 globals__get_source_file_map(Globals, Globals ^ source_file_map).
@@ -481,20 +491,21 @@
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%

-globals__io_init(Options, Target, GC_Method, TagsMethod,
-		TerminationNorm, TraceLevel, TraceSuppress,
-		MaybeThreadSafe) -->
-	{ copy(Target, Target1) },
-	{ copy(GC_Method, GC_Method1) },
-	{ copy(TagsMethod, TagsMethod1) },
-	{ copy(TerminationNorm, TerminationNorm1) },
-	{ copy(TraceLevel, TraceLevel1) },
-	{ copy(TraceSuppress, TraceSuppress1) },
-	{ copy(MaybeThreadSafe, MaybeThreadSafe1) },
-	{ globals__init(Options, Target1, GC_Method1, TagsMethod1,
-		TerminationNorm1, TraceLevel1, TraceSuppress1,
-		MaybeThreadSafe1, Globals) },
-	globals__io_set_globals(Globals).
+globals__io_init(Options, Target, GC_Method, TagsMethod, TerminationNorm,
+		Termination2Norm, TraceLevel, TraceSuppress, MaybeThreadSafe,
+		!IO) :-
+	copy(Target, Target1),
+	copy(GC_Method, GC_Method1),
+	copy(TagsMethod, TagsMethod1),
+	copy(TerminationNorm, TerminationNorm1),
+	copy(Termination2Norm, Termination2Norm1),
+	copy(TraceLevel, TraceLevel1),
+	copy(TraceSuppress, TraceSuppress1),
+	copy(MaybeThreadSafe, MaybeThreadSafe1),
+	globals__init(Options, Target1, GC_Method1, TagsMethod1,
+		TerminationNorm1, Termination2Norm1, TraceLevel1,
+		TraceSuppress1, MaybeThreadSafe1, Globals),
+	globals__io_set_globals(Globals, !IO).

 globals__io_get_target(Target) -->
 	globals__io_get_globals(Globals),
@@ -511,6 +522,10 @@
 globals__io_get_termination_norm(TerminationNorm) -->
 	globals__io_get_globals(Globals),
 	{ globals__get_termination_norm(Globals, TerminationNorm) }.
+
+globals__io_get_termination2_norm(Termination2Norm, !IO) :-
+	globals__io_get_globals(Globals, !IO),
+	globals__get_termination2_norm(Globals, Termination2Norm).

 globals__io_get_trace_level(TraceLevel) -->
 	globals__io_get_globals(Globals),
Index: compiler/goal_form.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/goal_form.m,v
retrieving revision 1.12
diff -u -r1.12 goal_form.m
--- compiler/goal_form.m	24 Mar 2005 02:00:26 -0000	1.12
+++ compiler/goal_form.m	24 Mar 2005 02:26:55 -0000
@@ -119,6 +119,7 @@
 :- import_module hlds__hlds_data.
 :- import_module parse_tree__prog_data.
 :- import_module transform_hlds__term_util.
+:- import_module transform_hlds__termination2.

 :- import_module bool.
 :- import_module int.
@@ -187,8 +188,14 @@
 		call(PredId, ProcId, _, _, _, _)) :-
 	MaybeModuleInfo = yes(ModuleInfo),
 	module_info_pred_proc_info(ModuleInfo, PredId, ProcId, _, ProcInfo),
-	proc_info_get_maybe_termination_info(ProcInfo, MaybeTermInfo),
-	MaybeTermInfo = yes(cannot_loop).
+	(
+		proc_info_get_maybe_termination_info(ProcInfo, MaybeTermInfo),
+		MaybeTermInfo = yes(cannot_loop(_))
+	;
+		proc_info_get_termination2_info(ProcInfo, Term2Info),
+		Term2Info ^ term_status = yes(cannot_loop(_))
+
+	).
 goal_cannot_loop_expr(_, unify(_, _, _, Uni, _)) :-
 	(
 		Uni = assign(_, _)
Index: compiler/handle_options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/handle_options.m,v
retrieving revision 1.224
diff -u -r1.224 handle_options.m
--- compiler/handle_options.m	24 Mar 2005 02:00:28 -0000	1.224
+++ compiler/handle_options.m	24 Mar 2005 02:26:55 -0000
@@ -163,13 +163,13 @@
 postprocess_options(error(ErrorMessage), [ErrorMessage], !IO).
 postprocess_options(ok(OptionTable0), Errors, !IO) :-
 	check_option_values(OptionTable0, OptionTable, Target, GC_Method,
-		TagsMethod, TermNorm, TraceLevel, TraceSuppress,
+		TagsMethod, TermNorm, Term2Norm, TraceLevel, TraceSuppress,
 		MaybeThreadSafe, [], CheckErrors),
 	(
 		CheckErrors = [],
 		postprocess_options_2(OptionTable, Target, GC_Method,
-			TagsMethod, TermNorm, TraceLevel, TraceSuppress,
-			MaybeThreadSafe, [], Errors, !IO)
+			TagsMethod, TermNorm, Term2Norm, TraceLevel,
+			TraceSuppress, MaybeThreadSafe, [], Errors, !IO)
 	;
 		CheckErrors = [_ | _],
 		Errors = CheckErrors
@@ -177,11 +177,12 @@

 :- pred check_option_values(option_table::in, option_table::out,
 	compilation_target::out, gc_method::out, tags_method::out,
-	termination_norm::out, trace_level::out, trace_suppress_items::out,
-	maybe_thread_safe::out, list(string)::in, list(string)::out) is det.
+	termination_norm::out, termination_norm::out, trace_level::out,
+	trace_suppress_items::out, maybe_thread_safe::out,
+	list(string)::in, list(string)::out) is det.

 check_option_values(OptionTable0, OptionTable, Target, GC_Method, TagsMethod,
-		TermNorm, TraceLevel, TraceSuppress, MaybeThreadSafe,
+		TermNorm, Term2Norm, TraceLevel, TraceSuppress, MaybeThreadSafe,
 		!Errors) :-
 	map__lookup(OptionTable0, target, Target0),
 	(
@@ -241,6 +242,18 @@
 			"`--termination-norm'\n\t(must be " ++
 			"`simple', `total' or `num-data-elems').", !Errors)
 	),
+	map__lookup(OptionTable0, termination2_norm, Term2Norm0),
+	(
+		Term2Norm0 = string(Term2NormStr),
+		convert_termination_norm(Term2NormStr, Term2NormPrime)
+	->
+		Term2Norm = Term2NormPrime
+	;
+		Term2Norm = simple,	% dummy
+		add_error("Invalid argument to option " ++
+			"`--termination2-norm'\n\t(must be" ++
+			"`simple', `total' or `num-data-elems').", !Errors)
+	),
 	map__lookup(OptionTable0, trace, Trace),
 	map__lookup(OptionTable0, exec_trace, ExecTraceOpt),
 	map__lookup(OptionTable0, decl_debug, DeclDebugOpt),
@@ -313,18 +326,22 @@
 	% of repeated appends to be a problem.
 	list__append(Errors0, [Error], Errors).

+	% NOTE: each termination analyser has its own norm setting.
+	%
 :- pred postprocess_options_2(option_table::in, compilation_target::in,
 	gc_method::in, tags_method::in, termination_norm::in,
-	trace_level::in, trace_suppress_items::in, maybe_thread_safe::in,
-	list(string)::in, list(string)::out, io::di, io::uo) is det.
+	termination_norm::in, trace_level::in, trace_suppress_items::in,
+	maybe_thread_safe::in, list(string)::in, list(string)::out,
+	io::di, io::uo) is det.

 postprocess_options_2(OptionTable0, Target, GC_Method, TagsMethod0,
-		TermNorm, TraceLevel, TraceSuppress, MaybeThreadSafe,
-		!Errors) -->
+		TermNorm, Term2Norm, TraceLevel, TraceSuppress,
+		MaybeThreadSafe, !Errors) -->
 	{ unsafe_promise_unique(OptionTable0, OptionTable1) }, % XXX
 	globals__io_init(OptionTable1, Target, GC_Method, TagsMethod0,
-		TermNorm, TraceLevel, TraceSuppress, MaybeThreadSafe),
-
+		TermNorm, Term2Norm, TraceLevel, TraceSuppress,
+		MaybeThreadSafe),
+
 	% Conservative GC implies --no-reclaim-heap-*
 	( { gc_is_conservative(GC_Method) = yes } ->
 		globals__io_set_option(
@@ -622,6 +639,11 @@
 	option_implies(check_termination, termination, bool(yes)),
 	option_implies(check_termination, warn_missing_trans_opt_files,
 		bool(yes)),
+	option_implies(verbose_check_termination2, check_termination2,
+		bool(yes)),
+	option_implies(check_termination2, termination2, bool(yes)),
+	option_implies(check_termination2, warn_missing_trans_opt_files,
+		bool(yes)),
 	option_implies(make_transitive_opt_interface, transitive_optimization,
 		bool(yes)),
 	option_implies(transitive_optimization, intermodule_optimization,
@@ -1462,7 +1484,7 @@
 	;
 		[]
 	).
-
+
 	% These option implications only affect the low-level (LLDS) code
 	% generator.  They may in fact be harmful if set for the high-level
 	% code generator, because sometimes the same option has different
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.350
diff -u -r1.350 hlds_out.m
--- compiler/hlds_out.m	22 Mar 2005 06:39:59 -0000	1.350
+++ compiler/hlds_out.m	22 Mar 2005 06:49:29 -0000
@@ -72,6 +72,9 @@
 :- pred hlds_out__write_pred_id(module_info::in, pred_id::in, io::di, io::uo)
 	is det.

+:- pred hlds_out__write_pred_proc_id(module_info::in, pred_proc_id::in, io::di,
+	io::uo) is det.
+
 :- pred hlds_out__write_pred_proc_id(module_info::in, pred_id::in, proc_id::in,
 	io::di, io::uo) is det.

@@ -403,6 +406,9 @@
 		io__write_string("deleted predicate ", !IO),
 		io__write_int(PredIdInt, !IO)
 	).
+
+hlds_out__write_pred_proc_id(ModuleInfo, proc(PredId, ProcId), !IO) :-
+	hlds_out__write_pred_proc_id(ModuleInfo, PredId, ProcId, !IO).

 hlds_out__write_pred_proc_id(ModuleInfo, PredId, ProcId, !IO) :-
 	hlds_out__write_pred_id(ModuleInfo, PredId, !IO),
Index: compiler/hlds_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
retrieving revision 1.159
diff -u -r1.159 hlds_pred.m
--- compiler/hlds_pred.m	22 Mar 2005 06:40:00 -0000	1.159
+++ compiler/hlds_pred.m	23 Mar 2005 21:33:22 -0000
@@ -27,6 +27,7 @@
 :- import_module mdbcomp__prim_data.
 :- import_module parse_tree__prog_data.
 :- import_module transform_hlds__term_util.
+:- import_module transform_hlds__termination2.

 :- import_module assoc_list.
 :- import_module bool.
@@ -1289,7 +1290,7 @@
 		% Approximate the termination information
 		% for the new procedure.
 	( goal_cannot_loop(ModuleInfo0, Goal0) ->
-		TermInfo = yes(cannot_loop)
+		TermInfo = yes(cannot_loop(unit))
 	;
 		TermInfo = no
 	),
@@ -1865,14 +1866,14 @@
 	maybe(list(mode))::in, list(mode)::in, maybe(list(is_live))::in,
 	maybe(determinism)::in, is_address_taken::in, proc_info::out) is det.

-:- pred proc_info_set(prog_context::in,prog_varset::in, vartypes::in,
+:- pred proc_info_set(prog_context::in, prog_varset::in, vartypes::in,
 	list(prog_var)::in, inst_varset::in, list(mode)::in,
 	maybe(list(is_live))::in, maybe(determinism)::in, determinism::in,
 	hlds_goal::in, bool::in,
 	type_info_varmap::in, typeclass_info_varmap::in,
 	maybe(arg_size_info)::in, maybe(termination_info)::in,
-	is_address_taken::in, stack_slots::in, maybe(list(arg_info))::in,
-	liveness_info::in, proc_info::out) is det.
+	termination2_info::in, is_address_taken::in, stack_slots::in,
+	maybe(list(arg_info))::in, liveness_info::in, proc_info::out) is det.

 :- pred proc_info_create(prog_context::in, prog_varset::in, vartypes::in,
 	list(prog_var)::in, inst_varset::in, list(mode)::in,
@@ -1984,6 +1985,12 @@
 	maybe(untuple_proc_info)::in,
 	proc_info::in, proc_info::out) is det.

+:- pred proc_info_get_termination2_info(proc_info::in,
+	termination2_info::out) is det.
+
+:- pred proc_info_set_termination2_info(termination2_info::in,
+	proc_info::in, proc_info::out) is det.
+
 :- pred proc_info_head_modes_constraint(proc_info::in, mode_constraint::out)
 	is det.

@@ -2180,6 +2187,10 @@
 					% The termination properties of the
 					% procedure. Set by termination
 					% analysis.
+		termination2		:: termination2_info,
+					% Termination properties and argument
+					% size constraints for the procedure.
+					% Set by termination2 analysis.
 		is_address_taken	:: is_address_taken,
 					% Is the address of this procedure
 					% taken? If yes, we will need to use
@@ -2295,24 +2306,26 @@
 	CanProcess = yes,
 	map__init(TVarsMap),
 	map__init(TCVarsMap),
+	Term2Info = termination2__term2_info_init,
 	NewProc = proc_info(MContext, BodyVarSet, BodyTypes, HeadVars,
 		InstVarSet, DeclaredModes, Modes, no, MaybeArgLives,
 		MaybeDet, InferredDet, ClauseBody, CanProcess, ModeErrors,
 		TVarsMap, TCVarsMap, eval_normal,
-		proc_sub_info(no, no, IsAddressTaken, StackSlots,
+		proc_sub_info(no, no, Term2Info, IsAddressTaken, StackSlots,
 		ArgInfo, InitialLiveness, no, no, no, no, no)).

 proc_info_set(Context, BodyVarSet, BodyTypes, HeadVars, InstVarSet, HeadModes,
 		HeadLives, DeclaredDetism, InferredDetism, Goal, CanProcess,
-		TVarMap, TCVarsMap, ArgSizes, Termination, IsAddressTaken,
-		StackSlots, ArgInfo, Liveness, ProcInfo) :-
+		TVarMap, TCVarsMap, ArgSizes, Termination, Termination2,
+		IsAddressTaken, StackSlots, ArgInfo, Liveness, ProcInfo) :-
 	ModeErrors = [],
 	ProcInfo = proc_info(Context, BodyVarSet, BodyTypes, HeadVars,
 		InstVarSet, no, HeadModes, no, HeadLives,
 		DeclaredDetism, InferredDetism, Goal, CanProcess, ModeErrors,
 		TVarMap, TCVarsMap, eval_normal,
-		proc_sub_info(ArgSizes, Termination, IsAddressTaken,
-		StackSlots, ArgInfo, Liveness, no, no, no, no, no)).
+		proc_sub_info(ArgSizes, Termination, Termination2,
+		IsAddressTaken, StackSlots, ArgInfo, Liveness, no, no, no,
+			no, no)).

 proc_info_create(Context, VarSet, VarTypes, HeadVars, InstVarSet,
 		HeadModes, Detism, Goal, TVarMap, TCVarsMap,
@@ -2328,11 +2341,12 @@
 	set__init(Liveness),
 	MaybeHeadLives = no,
 	ModeErrors = [],
+	Term2Info = termination2__term2_info_init,
 	ProcInfo = proc_info(Context, VarSet, VarTypes, HeadVars,
 		InstVarSet, no, HeadModes, no, MaybeHeadLives,
 		MaybeDeclaredDetism, Detism, Goal, yes, ModeErrors,
 		TVarMap, TCVarsMap, eval_normal,
-		proc_sub_info(no, no, IsAddressTaken,
+		proc_sub_info(no, no, Term2Info, IsAddressTaken,
 		StackSlots, no, Liveness, no, no, no, no, no)).

 proc_info_set_body(VarSet, VarTypes, HeadVars, Goal, TI_VarMap, TCI_VarMap,
@@ -2483,6 +2497,13 @@
 		MaybeArgInfo0 = no,
 		error("proc_info_arg_info: arg_pass_info not set")
 	).
+
+proc_info_get_termination2_info(ProcInfo, Termination2Info) :-
+	Termination2Info = ProcInfo ^ proc_sub_info ^ termination2.
+
+proc_info_set_termination2_info(Termination2Info, !ProcInfo) :-
+	!:ProcInfo = !.ProcInfo ^ proc_sub_info ^ termination2 :=
+		Termination2Info.

 proc_info_get_typeinfo_vars(Vars, VarTypes, TVarMap, TypeInfoVars) :-
 	set__to_sorted_list(Vars, VarList),
Index: compiler/libs.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/libs.m,v
retrieving revision 1.3
diff -u -r1.3 libs.m
--- compiler/libs.m	16 Mar 2003 08:01:27 -0000	1.3
+++ compiler/libs.m	9 Mar 2005 03:43:17 -0000
@@ -26,6 +26,11 @@
 :- include_module process_util.
 :- include_module timestamp.

+% Constraint machinery for the termination analyser.
+:- include_module lp_rational.
+:- include_module polyhedron.
+:- include_module rat.
+
 :- end_module libs.

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

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------



More information about the reviews mailing list