diff --git a/compiler/add_pragma_decl.m b/compiler/add_pragma_decl.m
index 16526dd47..1936147f9 100644
--- a/compiler/add_pragma_decl.m
+++ b/compiler/add_pragma_decl.m
@@ -101,10 +101,12 @@
 :- import_module parse_tree.prog_data_pragma.
 :- import_module parse_tree.prog_item_pred_proc_id.
 :- import_module parse_tree.prog_util.
-:- import_module transform_hlds.
-:- import_module transform_hlds.term_constr_main_types.
-:- import_module transform_hlds.term_constr_util.
-:- import_module transform_hlds.term_util.
+:- import_module termination.
+:- import_module termination.term_constr.
+:- import_module termination.term_constr.term_constr_main_types.
+:- import_module termination.term_constr.term_constr_util.
+:- import_module termination.term_osi.
+:- import_module termination.term_osi.term_osi_util.
 
 :- import_module bag.
 :- import_module int.
diff --git a/compiler/complexity.m b/compiler/complexity.m
index 27dab18e7..cf9f376af 100644
--- a/compiler/complexity.m
+++ b/compiler/complexity.m
@@ -89,7 +89,8 @@
 :- import_module parse_tree.prog_type_construct.
 :- import_module parse_tree.set_of_var.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.term_norm.
+:- import_module termination.
+:- import_module termination.term_norm.
 
 :- import_module assoc_list.
 :- import_module bool.
diff --git a/compiler/goal_form.m b/compiler/goal_form.m
index 1dbd30c8a..4fc56fd7f 100644
--- a/compiler/goal_form.m
+++ b/compiler/goal_form.m
@@ -251,9 +251,11 @@
 :- import_module hlds.proc_info_types.
 :- import_module parse_tree.prog_data_foreign.
 :- import_module parse_tree.prog_data_pragma.
+:- import_module termination.
+:- import_module termination.term_constr.
+:- import_module termination.term_constr.term_constr_main_types.
 :- import_module transform_hlds.
 :- import_module transform_hlds.exception_analysis.
-:- import_module transform_hlds.term_constr_main_types.
 
 :- import_module int.
 :- import_module maybe.
diff --git a/compiler/hlds_out_pred.m b/compiler/hlds_out_pred.m
index 10edc9503..999c3b80e 100644
--- a/compiler/hlds_out_pred.m
+++ b/compiler/hlds_out_pred.m
@@ -107,8 +107,9 @@
 :- import_module parse_tree.prog_type.
 :- import_module parse_tree.prog_util.
 :- import_module parse_tree.set_of_var.
-:- import_module transform_hlds.
-:- import_module transform_hlds.term_util.
+:- import_module termination.
+:- import_module termination.term_osi.
+:- import_module termination.term_osi.term_osi_util.
 
 :- import_module assoc_list.
 :- import_module bool.
diff --git a/compiler/hlds_pred.m b/compiler/hlds_pred.m
index a2e55f97f..cecef7f6c 100644
--- a/compiler/hlds_pred.m
+++ b/compiler/hlds_pred.m
@@ -477,7 +477,6 @@
 :- import_module parse_tree.prog_util.
 :- import_module parse_tree.set_of_var.
 :- import_module parse_tree.vartypes.
-:- import_module transform_hlds.
 
 :- import_module pair.
 :- import_module require.
diff --git a/compiler/hlds_proc.m b/compiler/hlds_proc.m
index 2cb234628..dada2ef53 100644
--- a/compiler/hlds_proc.m
+++ b/compiler/hlds_proc.m
@@ -31,9 +31,11 @@
 :- import_module parse_tree.prog_data_pragma.
 :- import_module parse_tree.set_of_var.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.
-:- import_module transform_hlds.term_constr_main_types.
-:- import_module transform_hlds.term_util.
+:- import_module termination.
+:- import_module termination.term_constr.
+:- import_module termination.term_constr.term_constr_main_types.
+:- import_module termination.term_osi.
+:- import_module termination.term_osi.term_osi_util.
 
 :- import_module list.
 :- import_module map.
diff --git a/compiler/intermod_analysis.m b/compiler/intermod_analysis.m
index 036836bf6..2e9855110 100644
--- a/compiler/intermod_analysis.m
+++ b/compiler/intermod_analysis.m
@@ -164,11 +164,14 @@
 :- import_module parse_tree.prog_data_pragma.
 :- import_module parse_tree.prog_item_pred_proc_id.
 :- import_module parse_tree.var_table.
+:- import_module termination.
+:- import_module termination.term_constr.
+:- import_module termination.term_constr.term_constr_data.
+:- import_module termination.term_constr.term_constr_main_types.
+:- import_module termination.term_constr.term_constr_util.
+:- import_module termination.term_osi.
+:- import_module termination.term_osi.term_osi_util.
 :- import_module transform_hlds.intermod_order_pred_info.
-:- import_module transform_hlds.term_constr_data.
-:- import_module transform_hlds.term_constr_main_types.
-:- import_module transform_hlds.term_constr_util.
-:- import_module transform_hlds.term_util.
 
 :- import_module bool.
 :- import_module cord.
diff --git a/compiler/mercury_compile_middle_passes.m b/compiler/mercury_compile_middle_passes.m
index 6a5194bf6..1fb7b894c 100644
--- a/compiler/mercury_compile_middle_passes.m
+++ b/compiler/mercury_compile_middle_passes.m
@@ -72,6 +72,11 @@
 :- import_module parse_tree.parse_tree_out.
 :- import_module parse_tree.parse_tree_out_info.
 :- import_module parse_tree.write_error_spec.
+:- import_module termination.
+:- import_module termination.term_constr.
+:- import_module termination.term_constr.term_constr_main.
+:- import_module termination.term_osi.
+:- import_module termination.term_osi.term_osi_main.
 :- import_module top_level.mercury_compile_front_end.
 :- import_module transform_hlds.
 :- import_module transform_hlds.accumulator.
@@ -112,8 +117,6 @@
 :- import_module transform_hlds.stm_expand.
 :- import_module transform_hlds.table_gen.
 :- import_module transform_hlds.tabling_analysis.
-:- import_module transform_hlds.term_constr_main.
-:- import_module transform_hlds.termination.
 :- import_module transform_hlds.trailing_analysis.
 :- import_module transform_hlds.tupling.
 :- import_module transform_hlds.unneeded_code.
diff --git a/compiler/size_prof.m b/compiler/size_prof.m
index 492bf920e..3367d8590 100644
--- a/compiler/size_prof.m
+++ b/compiler/size_prof.m
@@ -139,7 +139,8 @@
 :- import_module parse_tree.prog_type_test.
 :- import_module parse_tree.set_of_var.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.term_norm.
+:- import_module termination.
+:- import_module termination.term_norm.
 
 :- import_module assoc_list.
 :- import_module bool.
diff --git a/compiler/term_constr.m b/compiler/term_constr.m
new file mode 100644
index 000000000..694aeaa1d
--- /dev/null
+++ b/compiler/term_constr.m
@@ -0,0 +1,37 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%-----------------------------------------------------------------------------%
+% Copyright (C) 2026 The Mercury team.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%-----------------------------------------------------------------------------%
+%
+% This package contains our second termination analysis system.
+%
+% This system is described in Julien Fischer: Termination analysis
+% for Mercury using convex constraints, Honours report,
+% Department of Computer Science and Software Engineering,
+% The University of Melbourne, August 2002. This paper is available
+% from the Mercury project's papers page.
+%
+%-----------------------------------------------------------------------------%
+
+:- module termination.term_constr.
+:- interface.
+
+:- include_module term_constr_main.
+:- include_module term_constr_main_types.
+:- include_module term_constr_data.
+:- include_module term_constr_util.
+
+:- implementation.
+
+:- include_module term_constr_initial.
+:- include_module term_constr_build.    % pass 1
+:- include_module term_constr_fixpoint. % pass 1
+:- include_module term_constr_pass2.
+:- include_module term_constr_errors.
+
+%-----------------------------------------------------------------------------%
+:- end_module termination.term_constr.
+%-----------------------------------------------------------------------------%
diff --git a/compiler/term_constr_build.m b/compiler/term_constr_build.m
index f8bc24282..e42ec0a09 100644
--- a/compiler/term_constr_build.m
+++ b/compiler/term_constr_build.m
@@ -20,14 +20,14 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_constr_build.
+:- module termination.term_constr.term_constr_build.
 :- interface.
 
 :- import_module hlds.
 :- import_module hlds.hlds_dependency_graph.
 :- import_module hlds.hlds_module.
-:- import_module transform_hlds.term_constr_errors.
-:- import_module transform_hlds.term_norm.
+:- import_module termination.term_constr.term_constr_errors.
+:- import_module termination.term_norm.
 
 :- import_module bool.
 :- import_module list.
@@ -84,9 +84,9 @@
 :- import_module parse_tree.prog_type_test.
 :- import_module parse_tree.set_of_var.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.term_constr_data.
-:- import_module transform_hlds.term_constr_main_types.
-:- import_module transform_hlds.term_constr_util.
+:- import_module termination.term_constr.term_constr_data.
+:- import_module termination.term_constr.term_constr_main_types.
+:- import_module termination.term_constr.term_constr_util.
 
 :- import_module int.
 :- import_module map.
@@ -1304,5 +1304,5 @@ upper_bound_constraints(Norm, ModuleInfo, Var, TypeCtor, Ctors, Constraints) :-
     ).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_constr_build.
+:- end_module termination.term_constr.term_constr_build.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_constr_data.m b/compiler/term_constr_data.m
index 7a422f082..47429f5b4 100644
--- a/compiler/term_constr_data.m
+++ b/compiler/term_constr_data.m
@@ -107,7 +107,7 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_constr_data.
+:- module termination.term_constr.term_constr_data.
 
 :- interface.
 
@@ -119,7 +119,7 @@
 :- import_module libs.polyhedron.
 :- import_module parse_tree.
 :- import_module parse_tree.prog_data.
-:- import_module transform_hlds.term_constr_errors.
+:- import_module termination.term_constr.term_constr_errors.
 
 :- import_module bool.
 :- import_module io.
@@ -777,5 +777,5 @@ indent_line(Stream, N, !IO) :-
     ).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_constr_data.
+:- end_module termination.term_constr.term_constr_data.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_constr_errors.m b/compiler/term_constr_errors.m
index 9ed6bfb76..20fb9f316 100644
--- a/compiler/term_constr_errors.m
+++ b/compiler/term_constr_errors.m
@@ -12,7 +12,7 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_constr_errors.
+:- module termination.term_constr.term_constr_errors.
 :- interface.
 
 :- import_module hlds.
@@ -80,7 +80,8 @@
 :- import_module libs.
 :- import_module libs.globals.
 :- import_module libs.options.
-:- import_module transform_hlds.term_util.
+:- import_module termination.term_osi.  % ZZZ
+:- import_module termination.term_osi.term_osi_util.
 
 :- import_module bool.
 :- import_module cord.
@@ -323,5 +324,5 @@ term2_error_kind_is_direct(ErrorKind) = IsDirect :-
     ).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_constr_errors.
+:- end_module termination.term_constr.term_constr_errors.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_constr_fixpoint.m b/compiler/term_constr_fixpoint.m
index a28211528..45bd83eee 100644
--- a/compiler/term_constr_fixpoint.m
+++ b/compiler/term_constr_fixpoint.m
@@ -15,18 +15,18 @@
 %
 % NOTE: the code in this module should not refer to things in the HLDS
 % (with the exception of the termination2_info slots in the
-%  proc_sub_info structure)
+% proc_sub_info structure)
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_constr_fixpoint.
+:- module termination.term_constr.term_constr_fixpoint.
 :- interface.
 
 :- import_module hlds.
 :- import_module hlds.hlds_module.
 :- import_module hlds.pred_proc_id.
-:- import_module transform_hlds.term_constr_data.
-:- import_module transform_hlds.term_constr_errors.
+:- import_module termination.term_constr.term_constr_data.
+:- import_module termination.term_constr.term_constr_errors.
 
 :- import_module list.
 :- import_module set.
@@ -68,8 +68,8 @@
 :- import_module libs.lp_rational.
 :- import_module libs.options.
 :- import_module libs.polyhedron.
-:- import_module transform_hlds.term_constr_main_types.
-:- import_module transform_hlds.term_constr_util.
+:- import_module termination.term_constr.term_constr_main_types.
+:- import_module termination.term_constr.term_constr_util.
 
 :- import_module bool.
 :- import_module int.
@@ -490,5 +490,5 @@ fixpoint_options_init(Widening, MaxMatrixSize) =
     fixpoint_options(Widening, MaxMatrixSize).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_constr_fixpoint.
+:- end_module termination.term_constr.term_constr_fixpoint.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_constr_initial.m b/compiler/term_constr_initial.m
index cdf0e2252..ceb656b68 100644
--- a/compiler/term_constr_initial.m
+++ b/compiler/term_constr_initial.m
@@ -30,7 +30,7 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_constr_initial.
+:- module termination.term_constr.term_constr_initial.
 :- interface.
 
 :- import_module hlds.
@@ -73,11 +73,12 @@
 :- import_module parse_tree.prog_data.
 :- import_module parse_tree.prog_data_pragma.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.term_constr_data.
-:- import_module transform_hlds.term_constr_errors.
-:- import_module transform_hlds.term_constr_main_types.
-:- import_module transform_hlds.term_constr_util.
-:- import_module transform_hlds.term_util.
+:- import_module termination.term_constr.term_constr_data.
+:- import_module termination.term_constr.term_constr_errors.
+:- import_module termination.term_constr.term_constr_main_types.
+:- import_module termination.term_constr.term_constr_util.
+:- import_module termination.term_osi.  % ZZZ
+:- import_module termination.term_osi.term_osi_util.
 
 :- import_module bool.
 :- import_module int.
@@ -705,5 +706,5 @@ initialise_size_var_maps([ProcId | ProcIds], !ProcTable) :-
     initialise_size_var_maps(ProcIds, !ProcTable).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_constr_initial.
+:- end_module termination.term_constr.term_constr_initial.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_constr_main.m b/compiler/term_constr_main.m
index d8dd0e270..865e5df07 100644
--- a/compiler/term_constr_main.m
+++ b/compiler/term_constr_main.m
@@ -28,9 +28,9 @@
 %   This pass fills in the argument size and termination properties of
 %   builtin predicates, and also sets the termination properties of
 %   predicates that have either termination pragmas, or have termination
-%   assertions among their foreign_proc attributes. It also sets up
-%   information imported from `.opt' and `.trans_opt' files.
-%   XXX "sets up" in what sense?
+%   assertions among their foreign_proc attributes. It also incorporates
+%   information imported from termination2 pragmas in `.opt' and `.trans_opt'
+%   files into our data structures.
 %
 %   This pass is in term_constr_initial.m.
 %
@@ -77,7 +77,7 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_constr_main.
+:- module termination.term_constr.term_constr_main.
 :- interface.
 
 :- import_module hlds.
@@ -107,14 +107,14 @@
 :- import_module libs.globals.
 :- import_module libs.options.
 :- import_module parse_tree.prog_data_pragma.
-:- import_module transform_hlds.term_constr_build.
-:- import_module transform_hlds.term_constr_data.
-:- import_module transform_hlds.term_constr_errors.
-:- import_module transform_hlds.term_constr_fixpoint.
-:- import_module transform_hlds.term_constr_initial.
-:- import_module transform_hlds.term_constr_main_types.
-:- import_module transform_hlds.term_constr_pass2.
-:- import_module transform_hlds.term_norm.
+:- import_module termination.term_constr.term_constr_build.
+:- import_module termination.term_constr.term_constr_data.
+:- import_module termination.term_constr.term_constr_errors.
+:- import_module termination.term_constr.term_constr_fixpoint.
+:- import_module termination.term_constr.term_constr_initial.
+:- import_module termination.term_constr.term_constr_main_types.
+:- import_module termination.term_constr.term_constr_pass2.
+:- import_module termination.term_norm.
 
 :- import_module bool.
 :- import_module maybe.
@@ -345,5 +345,5 @@ proc_needs_ar_built(ModuleInfo, PPId) :-
     ).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_constr_main.
+:- end_module termination.term_constr.term_constr_main.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_constr_main_types.m b/compiler/term_constr_main_types.m
index 3113ff02d..27d8ae7a3 100644
--- a/compiler/term_constr_main_types.m
+++ b/compiler/term_constr_main_types.m
@@ -15,15 +15,15 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_constr_main_types.
+:- module termination.term_constr.term_constr_main_types.
 :- interface.
 
 :- import_module libs.
 :- import_module libs.polyhedron.
 :- import_module parse_tree.
 :- import_module parse_tree.prog_data_pragma.
-:- import_module transform_hlds.term_constr_data.
-:- import_module transform_hlds.term_constr_errors.
+:- import_module termination.term_constr.term_constr_data.
+:- import_module termination.term_constr.term_constr_errors.
 
 :- import_module list.
 :- import_module maybe.
@@ -222,5 +222,5 @@ term2_info_set_head_vars(X, !Term2Info) :-
     !Term2Info ^ t2i_head_vars := X.
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_constr_main_types.
+:- end_module termination.term_constr.term_constr_main_types.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_constr_pass2.m b/compiler/term_constr_pass2.m
index 040b30f0f..9b86a6c08 100644
--- a/compiler/term_constr_pass2.m
+++ b/compiler/term_constr_pass2.m
@@ -19,13 +19,13 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_constr_pass2.
+:- module termination.term_constr.term_constr_pass2.
 :- interface.
 
 :- import_module hlds.
 :- import_module hlds.hlds_module.
 :- import_module hlds.pred_proc_id.
-:- import_module transform_hlds.term_constr_main_types.
+:- import_module termination.term_constr.term_constr_main_types.
 
 %---------------------------------------------------------------------------%
 
@@ -58,9 +58,9 @@
 :- import_module libs.rat.
 :- import_module parse_tree.
 :- import_module parse_tree.prog_data_pragma.
-:- import_module transform_hlds.term_constr_data.
-:- import_module transform_hlds.term_constr_errors.
-:- import_module transform_hlds.term_constr_util.
+:- import_module termination.term_constr.term_constr_data.
+:- import_module termination.term_constr.term_constr_errors.
+:- import_module termination.term_constr.term_constr_util.
 
 :- import_module assoc_list.
 :- import_module bimap.
@@ -703,5 +703,5 @@ write_edge(Stream, ModuleInfo, SizeVarSet, Edge, !IO) :-
     io.write_string(Stream, " :- \n\n", !IO).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_constr_pass2.
+:- end_module termination.term_constr.term_constr_pass2.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_constr_util.m b/compiler/term_constr_util.m
index d3bfb1721..86ca19116 100644
--- a/compiler/term_constr_util.m
+++ b/compiler/term_constr_util.m
@@ -14,7 +14,7 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_constr_util.
+:- module termination.term_constr.term_constr_util.
 :- interface.
 
 :- import_module hlds.
@@ -28,8 +28,8 @@
 :- import_module parse_tree.prog_data.
 :- import_module parse_tree.prog_data_pragma.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.term_constr_data.
-:- import_module transform_hlds.term_constr_main_types.
+:- import_module termination.term_constr.term_constr_data.
+:- import_module termination.term_constr.term_constr_main_types.
 
 :- import_module bool.
 :- import_module io.
@@ -214,8 +214,8 @@
 :- import_module hlds.type_util.
 :- import_module libs.rat.
 :- import_module parse_tree.prog_type.
-:- import_module transform_hlds.term_constr_errors.
-:- import_module transform_hlds.term_norm.
+:- import_module termination.term_constr.term_constr_errors.
+:- import_module termination.term_norm.
 
 :- import_module pair.
 :- import_module require.
@@ -484,5 +484,5 @@ dump_size_varset_loop(Stream, VarSet, [Var | Vars], !IO) :-
     dump_size_varset_loop(Stream, VarSet, Vars, !IO).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_constr_util.
+:- end_module termination.term_constr.term_constr_util.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_norm.m b/compiler/term_norm.m
index 770765ae9..7de6db7d5 100644
--- a/compiler/term_norm.m
+++ b/compiler/term_norm.m
@@ -14,7 +14,7 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_norm.
+:- module termination.term_norm.
 :- interface.
 
 :- import_module hlds.
@@ -544,5 +544,5 @@ zero_size_type_category(CtorCat, ZeroSize) :-
     ).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_norm.
+:- end_module termination.term_norm.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_osi.m b/compiler/term_osi.m
new file mode 100644
index 000000000..0639a924c
--- /dev/null
+++ b/compiler/term_osi.m
@@ -0,0 +1,41 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%-----------------------------------------------------------------------------%
+% Copyright (C) 2026 The Mercury team.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%-----------------------------------------------------------------------------%
+%
+% This package contains our first termination analysis system.
+%
+% This termination analysis is based on the algorithm given by Gerhard Groeger
+% and Lutz Plumer in their paper "Handling of Mutual Recursion in Automatic
+% Termination Proofs for Logic Programs"  which was printed in JICSLP '92
+% (the proceedings of the Joint International Conference and Symposium on
+% Logic Programming in 1992), pages 336 - 350.
+%
+% Details about this implementation are covered in:
+% Chris Speirs, Zoltan Somogyi, and Harald Sondergaard: Termination
+% analysis for Mercury. In P. Van Hentenryck, editor, Static Analysis:
+% Proceedings of the 4th International Symposium, Lecture Notes in Computer
+% Science, Springer, 1997. A more detailed version is available for download
+% from the Mercury project's papers page.
+%
+%-----------------------------------------------------------------------------%
+
+:- module termination.term_osi.
+:- interface.
+
+:- include_module term_osi_main.
+:- include_module term_osi_util.
+
+:- implementation.
+
+:- include_module term_osi_pass1.
+:- include_module term_osi_pass2.
+:- include_module term_osi_traversal.
+:- include_module term_osi_errors.
+
+%-----------------------------------------------------------------------------%
+:- end_module termination.term_osi.
+%-----------------------------------------------------------------------------%
diff --git a/compiler/term_errors.m b/compiler/term_osi_errors.m
similarity index 99%
rename from compiler/term_errors.m
rename to compiler/term_osi_errors.m
index ddb57caa8..b7a2b4140 100644
--- a/compiler/term_errors.m
+++ b/compiler/term_osi_errors.m
@@ -15,7 +15,7 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_errors.
+:- module termination.term_osi.term_osi_errors.
 :- interface.
 
 :- import_module hlds.
@@ -173,7 +173,7 @@
 :- import_module libs.options.
 :- import_module parse_tree.prog_data_pragma.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.term_util.
+:- import_module termination.term_osi.term_osi_util.
 
 :- import_module cord.
 :- import_module int.
@@ -626,5 +626,5 @@ term_error_kind_is_fatal_error(ErrorKind) = IsFatal :-
     ).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_errors.
+:- end_module termination.term_osi.term_osi_errors.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_osi_main.m b/compiler/term_osi_main.m
new file mode 100644
index 000000000..7ed7b257d
--- /dev/null
+++ b/compiler/term_osi_main.m
@@ -0,0 +1,912 @@
+%---------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%---------------------------------------------------------------------------%
+% Copyright (C) 1997-2001, 2003-2012 The University of Melbourne.
+% Copyright (C) 2014-2020, 2022-2026 The Mercury Team.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%---------------------------------------------------------------------------%
+%
+% File: term_osi_main.m.
+% Main author: crs (when this file was named termination.m).
+% Significant modifications by zs.
+%
+%---------------------------------------------------------------------------%
+
+:- module termination.term_osi.term_osi_main.
+:- interface.
+
+:- import_module hlds.
+:- import_module hlds.hlds_module.
+:- import_module parse_tree.
+:- import_module parse_tree.error_spec.
+
+:- import_module list.
+
+%---------------------------------------------------------------------------%
+
+    % Perform termination analysis on the module.
+    %
+:- pred analyse_termination_in_module(module_info::in, module_info::out,
+    list(diag_spec)::out) is det.
+
+%---------------------------------------------------------------------------%
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module hlds.hlds_dependency_graph.
+:- import_module hlds.hlds_error_util.
+:- import_module hlds.hlds_goal.
+:- import_module hlds.hlds_markers.
+:- import_module hlds.hlds_pred.
+:- import_module hlds.hlds_pred_tests.
+:- import_module hlds.hlds_proc.
+:- import_module hlds.pred_name.
+:- import_module hlds.pred_proc_id.
+:- import_module hlds.status.
+:- import_module libs.
+:- import_module libs.dependency_graph.
+:- import_module libs.globals.
+:- import_module libs.options.
+:- import_module mdbcomp.
+:- import_module mdbcomp.builtin_modules.
+:- import_module mdbcomp.prim_data.
+:- import_module parse_tree.prog_data.
+:- import_module parse_tree.prog_data_foreign.
+:- import_module parse_tree.prog_data_pragma.
+:- import_module termination.term_norm.
+:- import_module termination.term_osi.term_osi_errors.
+:- import_module termination.term_osi.term_osi_pass1.
+:- import_module termination.term_osi.term_osi_pass2.
+:- import_module termination.term_osi.term_osi_util.
+:- import_module termination.term_post_analysis.
+
+:- import_module bool.
+:- import_module map.
+:- import_module maybe.
+:- import_module pair.
+:- import_module require.
+:- import_module set.
+:- import_module term.
+:- import_module unit.
+
+%---------------------------------------------------------------------------%
+
+analyse_termination_in_module(!ModuleInfo, !:Specs) :-
+    module_info_get_globals(!.ModuleInfo, Globals),
+    globals.get_termination_norm(Globals, TermNorm),
+    FunctorInfo = set_functor_info(!.ModuleInfo, TermNorm),
+    globals.lookup_int_option(Globals, termination_error_limit, MaxErrors),
+    globals.lookup_int_option(Globals, termination_path_limit, MaxPaths),
+    PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths),
+
+    % Process builtin and compiler-generated predicates, and user-supplied
+    % pragmas.
+    should_we_believe_check_termination_markers(!.ModuleInfo,
+        BelieveCheckTerm),
+    module_info_get_valid_pred_ids(!.ModuleInfo, PredIds),
+    term_preprocess_preds(BelieveCheckTerm, PredIds, !ModuleInfo),
+
+    % Process all the SCCs of the call graph in a bottom-up order.
+    module_info_ensure_dependency_info(!ModuleInfo, DepInfo),
+    SCCs = dependency_info_get_bottom_up_sccs(DepInfo),
+
+    % Set the termination status of foreign_procs based on the foreign code
+    % attributes.
+    !:Specs = [],
+    check_foreign_code_attributes(SCCs, !ModuleInfo, !Specs),
+
+    % Ensure that termination pragmas for a procedure do not conflict with
+    % termination pragmas for other procedures in the SCC.
+    check_pragmas_are_consistent(SCCs, !ModuleInfo, !Specs),
+
+    list.foldl2(analyse_termination_in_scc(PassInfo), SCCs,
+        !ModuleInfo, !Specs),
+    run_post_term_analysis(!.ModuleInfo, PostSpecs),
+    !:Specs = PostSpecs ++ !.Specs,
+
+    module_info_get_proc_analysis_kinds(!.ModuleInfo, ProcAnalysisKinds0),
+    set.insert(pak_termination, ProcAnalysisKinds0, ProcAnalysisKinds),
+    module_info_set_proc_analysis_kinds(ProcAnalysisKinds, !ModuleInfo).
+
+%---------------------------------------------------------------------------%
+%
+% Handle foreign code attributes.
+%
+
+% Set the termination status for any procedures implemented using the foreign
+% language interface. If the terminates/does_not_terminate attribute has been
+% set then we set the termination status of the procedure accordingly.
+% Otherwise the procedure is considered to be terminating if it does not call
+% Mercury and non-terminating if it does.
+%
+% We also check that the foreign code attributes do not conflict with any
+% termination pragmas that have been supplied for the procedure.
+
+:- pred check_foreign_code_attributes(list(scc)::in,
+    module_info::in, module_info::out,
+    list(diag_spec)::in, list(diag_spec)::out) is det.
+
+check_foreign_code_attributes(SCCs, !ModuleInfo, !Specs) :-
+    list.foldl2(check_foreign_code_attributes_in_scc, SCCs,
+        !ModuleInfo, !Specs).
+
+:- pred check_foreign_code_attributes_in_scc(scc::in,
+    module_info::in, module_info::out,
+    list(diag_spec)::in, list(diag_spec)::out) is det.
+
+check_foreign_code_attributes_in_scc(SCC, !ModuleInfo, !Specs) :-
+    set.to_sorted_list(SCC, PPIds),
+    (
+        PPIds = [],
+        unexpected($pred, "empty SCC")
+    ;
+        PPIds = [PPId],
+        module_info_pred_proc_info(!.ModuleInfo, PPId, PredInfo, ProcInfo0),
+        proc_info_get_goal(ProcInfo0, Goal),
+        Goal = hlds_goal(GoalExpr, _GoalInfo),
+        ( if GoalExpr = call_foreign_proc(Attributes, _, _, _, _, _, _) then
+            check_foreign_code_attributes_of_proc(!.ModuleInfo, PPId,
+                PredInfo, Attributes, ProcInfo0, ProcInfo, !Specs),
+            module_info_set_pred_proc_info(PPId, PredInfo, ProcInfo,
+                !ModuleInfo)
+        else
+            true
+        )
+    ;
+        PPIds = [_, _ | _]
+        % Foreign code proc cannot be mutually recursive.
+    ).
+
+:- pred check_foreign_code_attributes_of_proc(module_info::in,
+    pred_proc_id::in, pred_info::in, foreign_proc_attributes::in,
+    proc_info::in, proc_info::out,
+    list(diag_spec)::in, list(diag_spec)::out) is det.
+
+check_foreign_code_attributes_of_proc(ModuleInfo, PPId, _PredInfo, Attributes,
+        !ProcInfo, !Specs) :-
+% XXX This *should* be enough to make termination analysis decide that
+% the difftime and therefore compare_time_t_reps predicates in library/time.m
+% terminate *without* an explicit terminates pragma, but it is NOT enough.
+%
+%   pred_info_get_arg_types(PredInfo, ArgTypes),
+%   proc_info_get_argmodes(!.ProcInfo, ArgModes),
+%   ( if all_outputs_are_builtins(ModuleInfo, ArgTypes, ArgModes, Nos) then
+%       % XXX norm dependent
+%       ArgSizeInfo = finite(0, Nos),
+%       proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo), !ProcInfo)
+%   else
+%       true
+%   ),
+    proc_info_get_maybe_termination_info(!.ProcInfo, MaybeTermination),
+    proc_info_get_context(!.ProcInfo, Context),
+    (
+        MaybeTermination = no,
+        ( if attributes_imply_termination(Attributes) then
+            TermStatus = yes(cannot_loop(unit)),
+            proc_info_set_maybe_termination_info(TermStatus, !ProcInfo)
+        else
+            TermErr = term_error(Context, does_not_term_foreign(PPId)),
+            TermStatus = yes(can_loop([TermErr])),
+            proc_info_set_maybe_termination_info(TermStatus, !ProcInfo)
+        )
+    ;
+        % If there was a `:- pragma terminates' declaration for this procedure,
+        % then check that the foreign code attributes do not contradict this.
+        MaybeTermination = yes(cannot_loop(_)),
+        ProcTerminates = get_terminates(Attributes),
+        (
+            ProcTerminates = proc_does_not_terminate,
+            TermErr = term_error(Context, inconsistent_annotations),
+            TermStatus = yes(can_loop([TermErr])),
+            % XXX intermod
+            proc_info_set_maybe_termination_info(TermStatus, !ProcInfo),
+            ProcNamePieces = describe_one_proc_name(ModuleInfo,
+                yes(color_subject), should_module_qualify, PPId),
+            Pieces = [words("Warning:") | ProcNamePieces] ++
+                [words("has a")] ++
+                color_as_inconsistent([pragma_decl("terminates"),
+                    words("declaration,")]) ++
+                [words("but also has the")] ++
+                color_as_inconsistent([quote("does_not_terminate"),
+                    words("foreign code attribute")]) ++
+                [words("set."), nl],
+            Severity = severity_warning(warn_requested_by_option),
+            Spec = spec($pred, Severity, phase_read_files, Context, Pieces),
+            !:Specs = [Spec | !.Specs]
+        ;
+            ( ProcTerminates = proc_terminates
+            ; ProcTerminates = depends_on_mercury_calls
+            )
+        )
+    ;
+        % If there was a `:- pragma does_not_terminate' declaration
+        % for this procedure, then check that the foreign code attributes
+        % do not contradict this.
+        MaybeTermination = yes(can_loop(TermErrs0)),
+        ProcTerminates = get_terminates(Attributes),
+        (
+            ProcTerminates = proc_terminates,
+            TermErr = term_error(Context, inconsistent_annotations),
+            TermErrs = [TermErr | TermErrs0],
+            TermStatus = yes(can_loop(TermErrs)),
+            % XXX intermod
+            proc_info_set_maybe_termination_info(TermStatus, !ProcInfo),
+            ProcNamePieces = describe_one_proc_name(ModuleInfo,
+                yes(color_subject), should_module_qualify, PPId),
+            Pieces = [words("Warning:") | ProcNamePieces] ++
+                [words("has a")] ++
+                color_as_inconsistent([pragma_decl("does_not_terminate"),
+                    words("declaration,")]) ++
+                [words("but also has the")] ++
+                color_as_inconsistent([quote("terminates"),
+                    words("foreign code attribute")]) ++
+                [words("set."), nl],
+            Severity = severity_warning(warn_requested_by_option),
+            Spec = spec($pred, Severity, phase_read_files, Context, Pieces),
+            !:Specs = [Spec | !.Specs]
+        ;
+            ( ProcTerminates = proc_does_not_terminate
+            ; ProcTerminates = depends_on_mercury_calls
+            )
+        )
+    ).
+
+% XXX This is part of the non-working, commented-out code at the top of
+% check_foreign_code_attributes_of_proc.
+%
+% :- pred all_outputs_are_builtins(module_info::in,
+%     list(mer_type)::in, list(mer_mode)::in, list(bool)::out) is semidet.
+%
+% all_outputs_are_builtins(_, [], [], []).
+% all_outputs_are_builtins(_, [], [_ | _], []) :-
+%     unexpected($pred, "list length mismatch").
+% all_outputs_are_builtins(_, [_ | _], [], []) :-
+%     unexpected($pred, "list length mismatch").
+% all_outputs_are_builtins(ModuleInfo, [Type | Types], [Mode | Modes], Nos) :-
+%     all_outputs_are_builtins(ModuleInfo, Types, Modes, TailNos),
+%     ( if mode_is_output(ModuleInfo, Mode) then
+%         Type = builtin_type(_)
+%     else
+%         true
+%     ),
+%     Nos = [no | TailNos].
+
+%---------------------------------------------------------------------------%
+%
+% Check termination pragmas for consistency.
+%
+
+% Check that any user-supplied termination information (from pragma
+% terminates/does_not_terminate) is consistent for each SCC in the program.
+%
+% The information will not be consistent if:
+% (1) One or more procs. in the SCC has a terminates pragma *and* one or more
+%     procs. in the SCC has a does_not_terminate pragma.
+% (2) One or more procs. in the SCC has a termination pragma (of either sort),
+%     *and* the termination status of one or more procs. in the SCC is
+%     unknown. (We check this after checking for the first case, so the
+%     termination info. for the known procs. will be consistent.)
+%
+% In the first case set the termination for all procs. in the SCC to can_loop
+% and emit a warning. In the second, set the termination of any procedures
+% whose termination status is unknown to be the same as those whose
+% termination status is known.
+
+:- pred check_pragmas_are_consistent(list(scc)::in,
+    module_info::in, module_info::out,
+    list(diag_spec)::in, list(diag_spec)::out) is det.
+
+check_pragmas_are_consistent(SCCs, !ModuleInfo, !Specs) :-
+    list.foldl2(check_scc_pragmas_are_consistent, SCCs, !ModuleInfo, !Specs).
+
+:- pred check_scc_pragmas_are_consistent(scc::in,
+    module_info::in, module_info::out,
+    list(diag_spec)::in, list(diag_spec)::out) is det.
+
+check_scc_pragmas_are_consistent(SCC, !ModuleInfo, !Specs) :-
+    classify_termination_status(!.ModuleInfo,  set.to_sorted_list(SCC),
+        set.init, KnownPredNamesIdsSet, set.init, KnownContextSet,
+        set.init, KnownTermStatusSet, set.init, UnknownPPIdSet),
+    KnownTermStatuses = set.to_sorted_list(KnownTermStatusSet),
+    (
+        KnownTermStatuses = []
+        % We don't know the termination status of any procedure in the SCC.
+    ;
+        KnownTermStatuses = [KnownTermStatus],
+        % We know the termination status of at least one procedure in the SCC,
+        % and all the procedures that do have known termination statuses
+        % have the same termination status.
+        set.foldl(set_termination_info(KnownTermStatus),
+            UnknownPPIdSet, !ModuleInfo)
+    ;
+        KnownTermStatuses = [_, _ | _],
+        % We know the termination status of at least two procedures
+        % in the SCC, and those procedures have two *different*
+        % termination statuses.
+
+        % Emit a warning, and then assume that they all loop.
+        LeastContext = list.det_head(set.to_sorted_list(KnownContextSet)),
+        NewTermStatus =
+            can_loop([term_error(LeastContext, inconsistent_annotations)]),
+        set.foldl(set_termination_info(NewTermStatus), SCC, !ModuleInfo),
+
+        PredNamesIds = set.to_sorted_list(KnownPredNamesIdsSet),
+        PredNamePieces = describe_several_pred_names(!.ModuleInfo,
+            yes(color_subject), should_module_qualify,
+            list.map(pair.snd, PredNamesIds)),
+        Pieces = [words("Warning:")] ++ PredNamePieces ++
+            [words("are mutually recursive,"),
+            words("but some of their termination pragmas are")] ++
+            color_as_incorrect([words("inconsistent.")]) ++
+            [nl],
+        Severity = severity_warning(warn_requested_by_option),
+        Spec = spec($pred, Severity, phase_read_files, LeastContext, Pieces),
+        !:Specs = [Spec | !.Specs]
+    ).
+
+:- pred classify_termination_status(module_info::in, list(pred_proc_id)::in,
+    set(pair(string, pred_id))::in, set(pair(string, pred_id))::out,
+    set(prog_context)::in, set(prog_context)::out,
+    set(termination_info)::in, set(termination_info)::out,
+    set(pred_proc_id)::in, set(pred_proc_id)::out) is det.
+
+classify_termination_status(_, [],
+        !KnownPredNamesIds, !KnownContexts,
+        !KnownTermStatuses, !UnknownPPIds).
+classify_termination_status(ModuleInfo, [PPId | PPIds],
+        !KnownPredNamesIds, !KnownContexts,
+        !KnownTermStatuses, !UnknownPPIds) :-
+    module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, ProcInfo),
+    proc_info_get_maybe_termination_info(ProcInfo, MaybeTermStatus),
+    (
+        MaybeTermStatus = yes(TermStatus),
+        PredName = pred_info_name(PredInfo),
+        PPId = proc(PredId, _ProcId),
+        set.insert(PredName - PredId, !KnownPredNamesIds),
+        % XXX We should be getting the context from the *Proc*Info.
+        pred_info_get_context(PredInfo, Context),
+        set.insert(Context, !KnownContexts),
+        set.insert(TermStatus, !KnownTermStatuses)
+    ;
+        MaybeTermStatus = no,
+        set.insert(PPId, !UnknownPPIds)
+    ),
+    classify_termination_status(ModuleInfo, PPIds,
+        !KnownPredNamesIds, !KnownContexts,
+        !KnownTermStatuses, !UnknownPPIds).
+
+%---------------------------------------------------------------------------%
+%
+% Run termination analysis on a single SCC.
+%
+
+    % For each SCC, we first find out the relationships among the sizes of the
+    % arguments of the procedures of the SCC, and then attempt to prove
+    % termination of the procedures.
+    %
+:- pred analyse_termination_in_scc(pass_info::in, scc::in,
+    module_info::in, module_info::out,
+    list(diag_spec)::in, list(diag_spec)::out) is det.
+
+analyse_termination_in_scc(PassInfo, SCC, !ModuleInfo, !Specs) :-
+    IsArgSizeKnown =
+        ( pred(PPId::in) is semidet :-
+            module_info_pred_proc_info(!.ModuleInfo, PPId, _, ProcInfo),
+            proc_info_get_maybe_arg_size_info(ProcInfo, yes(_))
+        ),
+    set.filter(IsArgSizeKnown, SCC, _SCCArgSizeKnown, SCCArgSizeUnknown),
+    ( if set.is_empty(SCCArgSizeUnknown) then
+        ArgSizeErrors = [],
+        TermErrors = []
+    else
+        find_arg_sizes_in_scc(!.ModuleInfo, PassInfo, SCCArgSizeUnknown,
+            ArgSizeResult, TermErrors),
+        (
+            ArgSizeResult = arg_size_ok(Solutions, OutputSupplierMap),
+            set_finite_arg_size_infos(Solutions, OutputSupplierMap,
+                !ModuleInfo),
+            ArgSizeErrors = []
+        ;
+            ArgSizeResult = arg_size_error(Errors),
+            set.foldl(set_infinite_arg_size_info(infinite(Errors)),
+                SCCArgSizeUnknown, !ModuleInfo),
+            ArgSizeErrors = Errors
+        )
+    ),
+    set.filter(is_termination_known(!.ModuleInfo), SCC,
+        _SCCTerminationKnown, SCCTerminationUnknown),
+    ( if set.is_empty(SCCTerminationUnknown) then
+        % We may possibly have encountered inconsistent
+        % terminates/does_not_terminate pragmas for this SCC, so we need to
+        % report errors here as well.
+        % XXX That comment does not make sense here.
+        true
+    else
+        IsFatal =
+            ( pred(Error::in) is semidet :-
+                Error = term_error(_Context, ErrorKind),
+                term_error_kind_is_fatal_error(ErrorKind) = yes
+            ),
+        list.filter(IsFatal, ArgSizeErrors, FatalErrors),
+        BothErrors = TermErrors ++ FatalErrors,
+        (
+            BothErrors = [_ | _],
+            % These errors prevent pass 2 from proving termination
+            % in any case, so we may as well not prove it quickly.
+            PassInfo = pass_info(_, MaxErrors, _),
+            list.take_upto(MaxErrors, BothErrors, ReportedErrors),
+            TerminationResult = can_loop(ReportedErrors)
+        ;
+            BothErrors = [],
+            module_info_get_globals(!.ModuleInfo, Globals),
+            globals.lookup_int_option(Globals, termination_single_args,
+                SingleArgs),
+            prove_termination_in_scc(!.ModuleInfo, PassInfo,
+                SCCTerminationUnknown, SingleArgs, TerminationResult)
+        ),
+        set.foldl(set_termination_info(TerminationResult),
+            SCCTerminationUnknown, !ModuleInfo),
+        (
+            TerminationResult = can_loop(TerminationErrors),
+            maybe_report_termination_errors(!.ModuleInfo, SCC,
+                TerminationErrors, !Specs)
+        ;
+            TerminationResult = cannot_loop(_)
+        )
+    ).
+
+%---------------------------------------------------------------------------%
+
+    % This predicate takes the results from solve_equations and inserts these
+    % results into the module info.
+    %
+:- pred set_finite_arg_size_infos(list(pair(pred_proc_id, int))::in,
+    used_args::in, module_info::in, module_info::out) is det.
+
+set_finite_arg_size_infos([], _, !ModuleInfo).
+set_finite_arg_size_infos([Soln | Solns], OutputSupplierMap, !ModuleInfo) :-
+    Soln = PPId - Gamma,
+    PPId = proc(PredId, ProcId),
+    module_info_pred_proc_info(!.ModuleInfo, PredId, ProcId,
+        PredInfo0, ProcInfo0),
+    map.lookup(OutputSupplierMap, PPId, OutputSuppliers),
+    ArgSizeInfo = finite(Gamma, OutputSuppliers),
+    % XXX intermod
+    proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo), ProcInfo0, ProcInfo),
+    pred_info_set_proc_info(ProcId, ProcInfo, PredInfo0, PredInfo),
+    module_info_set_pred_info(PredId, PredInfo, !ModuleInfo),
+    set_finite_arg_size_infos(Solns, OutputSupplierMap, !ModuleInfo).
+
+:- pred set_infinite_arg_size_info(arg_size_info::in, pred_proc_id::in,
+    module_info::in, module_info::out) is det.
+
+set_infinite_arg_size_info(ArgSizeInfo, PPId, !ModuleInfo) :-
+    PPId = proc(PredId, ProcId),
+    module_info_pred_proc_info(!.ModuleInfo, PredId, ProcId,
+        PredInfo0, ProcInfo0),
+    % XXX intermod
+    proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo), ProcInfo0, ProcInfo),
+    pred_info_set_proc_info(ProcId, ProcInfo, PredInfo0, PredInfo),
+    module_info_set_pred_info(PredId, PredInfo, !ModuleInfo).
+
+%---------------------------------------------------------------------------%
+
+:- pred set_termination_info(termination_info::in, pred_proc_id::in,
+    module_info::in, module_info::out) is det.
+
+set_termination_info(TerminationInfo, PPId, !ModuleInfo) :-
+    PPId = proc(PredId, ProcId),
+    module_info_pred_proc_info(!.ModuleInfo, PredId, ProcId,
+        PredInfo0, ProcInfo0),
+    % XXX intermod
+    proc_info_set_maybe_termination_info(yes(TerminationInfo),
+        ProcInfo0, ProcInfo),
+    pred_info_set_proc_info(ProcId, ProcInfo, PredInfo0, PredInfo),
+    module_info_set_pred_info(PredId, PredInfo, !ModuleInfo).
+
+%---------------------------------------------------------------------------%
+
+:- pred maybe_report_termination_errors(module_info::in, scc::in,
+    list(term_error)::in,
+    list(diag_spec)::in, list(diag_spec)::out) is det.
+
+maybe_report_termination_errors(ModuleInfo, SCC, Errors, !Specs) :-
+    decide_what_term_errors_to_report(ModuleInfo, SCC, Errors,
+        MaybeErrorsToReport),
+    (
+        MaybeErrorsToReport = no
+    ;
+        MaybeErrorsToReport = yes(ErrorsToReport),
+        report_term_errors(ModuleInfo, SCC, ErrorsToReport, !Specs)
+    ).
+
+:- pred decide_what_term_errors_to_report(module_info::in, scc::in,
+    list(term_error)::in, maybe(list(term_error))::out) is det.
+
+decide_what_term_errors_to_report(ModuleInfo, SCC, Errors,
+        MaybeErrorsToReport) :-
+    % NOTE The code of this predicate follows the same logic as the
+    % code of decide_what_term2_errors_to_report in term_constr_errors.m.
+    % Although there are differences in the data types they operate on
+    % and the options they consult, any changes here probably require
+    % corresponding changes there as well.
+
+    module_info_get_globals(ModuleInfo, Globals),
+    globals.lookup_bool_option(Globals, termination_check, NormalErrors),
+    globals.lookup_bool_option(Globals, termination_check_verbose,
+        VerboseErrors),
+    ( if
+        IsCheckTerm =
+            ( pred(PPId::in) is semidet :-
+                module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, _),
+                not pred_info_is_imported(PredInfo),
+                pred_info_get_markers(PredInfo, Markers),
+                marker_is_present(Markers, marker_check_termination)
+            ),
+        set.filter(IsCheckTerm, SCC, CheckTermPPIds),
+        set.is_non_empty(CheckTermPPIds)
+    then
+        % If any procedure in the SCC has a check_terminates pragma,
+        % print out one error message for the whole SCC and indicate an error.
+        MaybeErrorsToReport = yes(Errors)
+    else if
+        IsNonImported =
+            ( pred(PPId::in) is semidet :-
+                module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, _),
+                not pred_info_is_imported(PredInfo)
+            ),
+        set.filter(IsNonImported, SCC, NonImportedPPIds),
+        set.is_non_empty(NonImportedPPIds)
+    then
+        (
+            VerboseErrors = yes,
+            % If verbose errors is enabled, then output both direct and
+            % indirect errors.
+            % (See term_errors.m for details of direct and indirect errors.)
+            MaybeErrorsToReport = yes(Errors)
+        ;
+            VerboseErrors = no,
+            (
+                NormalErrors = yes,
+                % We prefer reporting only the direct errors, but if there are
+                % no direct errors, then output all the errors, which will then
+                % all be indirect errors. This is better than giving no error
+                % at all, which would lead to a message reporting that
+                % termination could not be proven for "unknown reasons".
+                IsDirect =
+                    ( pred(Error::in) is semidet :-
+                        Error = term_error(_, ErrorKind),
+                        term_error_kind_is_direct_error(ErrorKind) = yes
+                    ),
+                list.filter(IsDirect, Errors, DirectErrors),
+                (
+                    DirectErrors = [],
+                    MaybeErrorsToReport = yes(Errors)
+                ;
+                    DirectErrors = [_ | _],
+                    MaybeErrorsToReport = yes(DirectErrors)
+                )
+            ;
+                NormalErrors = no,
+                MaybeErrorsToReport = no
+            )
+        )
+    else
+        MaybeErrorsToReport = no
+    ).
+
+%---------------------------------------------------------------------------%
+
+    % This predicate preprocesses each predicate and sets the termination
+    % property if possible. This is done as follows.
+    %
+    % Set the termination to cannot_loop if:
+    % - there is a terminates pragma defined for the predicate;
+    % - there is a `check_termination' pragma defined for the predicate,
+    %   and it is imported, and the compiler is not currently generating
+    %   the intermodule optimization file; or
+    % - the predicate is a builtin predicate or is compiler generated (This
+    %   also sets the termination constant and UsedArgs).
+    %
+    % Set the termination to can_loop if:
+    % - there is a `does_not_terminate' pragma defined for this predicate; or
+    % - the predicate is imported and there is no other source of
+    %   information about it (termination_info pragmas, terminates pragmas,
+    %   check_termination pragmas, builtin/compiler generated).
+    %
+:- pred term_preprocess_preds(maybe_believe_check_termination::in,
+    list(pred_id)::in, module_info::in, module_info::out) is det.
+
+term_preprocess_preds(_, [], !ModuleInfo).
+term_preprocess_preds(BelieveCheckTerm, [PredId | PredIds], !ModuleInfo) :-
+    term_preprocess_pred(BelieveCheckTerm, PredId, !ModuleInfo),
+    term_preprocess_preds(BelieveCheckTerm, PredIds, !ModuleInfo).
+
+:- pred term_preprocess_pred(maybe_believe_check_termination::in,
+    pred_id::in, module_info::in, module_info::out) is det.
+
+term_preprocess_pred(BelieveCheckTerm, PredId, !ModuleInfo) :-
+    module_info_pred_info(!.ModuleInfo, PredId, PredInfo0),
+    pred_info_get_status(PredInfo0, PredStatus),
+    pred_info_get_context(PredInfo0, Context),
+    pred_info_get_proc_table(PredInfo0, ProcTable0),
+    pred_info_get_markers(PredInfo0, Markers),
+    ProcIds = pred_info_all_proc_ids(PredInfo0),
+    ( if
+        % It is possible for compiler generated/mercury builtin predicates
+        % to be imported or locally defined, so they must be covered here,
+        % separately.
+        set_compiler_gen_terminates(!.ModuleInfo, PredId, PredInfo0,
+            ProcIds, ProcTable0, ProcTable1)
+    then
+        ProcTable2 = ProcTable1
+    else if
+        pred_status_defined_in_this_module(PredStatus) = yes
+    then
+        % Since we cannot see their definition, we consider procedures
+        % which have a `:- pragma external_{pred/func}' to be imported.
+        ( if marker_is_present(Markers, marker_terminates) then
+            change_procs_termination_info(ProcIds, yes, cannot_loop(unit),
+                ProcTable0, ProcTable2)
+        else
+            ProcTable2 = ProcTable0
+        )
+    else
+        % Not defined in this module.
+
+        % All of the predicates that are processed in this section are imported
+        % in some way. With imported predicates, any 'check_termination'
+        % pragmas will be checked by the compiler when it compiles the
+        % relevant source file (that the predicate was imported from).
+        % When making the intermodule optimizations, the check_termination
+        % will not be checked when the relevant source file is compiled,
+        % so it cannot be depended upon.
+        ( if
+            (
+                marker_is_present(Markers, marker_terminates)
+            ;
+                BelieveCheckTerm = do_believe_check_termination,
+                marker_is_present(Markers, marker_check_termination)
+            )
+        then
+            change_procs_termination_info(ProcIds, yes, cannot_loop(unit),
+                ProcTable0, ProcTable1)
+        else
+            TerminationError = term_error(Context, imported_pred),
+            TerminationInfo = can_loop([TerminationError]),
+            change_procs_termination_info(ProcIds, no, TerminationInfo,
+                ProcTable0, ProcTable1)
+        ),
+        ArgSizeError = term_error(Context, imported_pred),
+        ArgSizeInfo = infinite([ArgSizeError]),
+        change_procs_arg_size_info(ProcIds, no, ArgSizeInfo,
+            ProcTable1, ProcTable2)
+    ),
+    ( if marker_is_present(Markers, marker_does_not_terminate) then
+        RequestError = term_error(Context, does_not_term_pragma(PredId)),
+        RequestTerminationInfo = can_loop([RequestError]),
+        change_procs_termination_info(ProcIds, yes,
+            RequestTerminationInfo, ProcTable2, ProcTable)
+    else
+        ProcTable = ProcTable2
+    ),
+    pred_info_set_proc_table(ProcTable, PredInfo0, PredInfo),
+    module_info_set_pred_info(PredId, PredInfo, !ModuleInfo).
+
+%---------------------------------------------------------------------------%
+
+    % This predicate checks each ProcId in the list to see if it is a compiler
+    % generated predicate, or a predicate from builtin.m or private_builtin.m.
+    % If it is, then the compiler sets the termination property of the ProcIds
+    % accordingly.
+    %
+    % We assume that user-defined special predicates terminate. This assumption
+    % is checked later during the post_term_analysis pass.
+    %
+:- pred set_compiler_gen_terminates(module_info::in,
+    pred_id::in, pred_info::in, list(proc_id)::in,
+    proc_table::in, proc_table::out) is semidet.
+
+set_compiler_gen_terminates(ModuleInfo, PredId, PredInfo, ProcIds,
+        !ProcTable) :-
+    % XXX This code looks to be a near-identical copy of the predicate
+    % of the same name in term_constr_initial.m.
+    ( if
+        pred_info_is_builtin(PredInfo)
+    then
+        set_builtin_terminates(ProcIds, PredId, PredInfo, ModuleInfo,
+            !ProcTable)
+    else if
+        % Compiler-generated unify/compare/index predicates always terminate.
+        % The else part checks for that.
+        %
+        % The then part checks for something else: for the predicate being
+        % named "unify", "index" or "compare", and defined in a builtin module.
+        % In practice, this is an unnecessarily roundabout way to  assert that
+        % builtin.unify and builtin.compare always terminate.
+        %
+        % This assertion was correct when this code was written in 1997/8,
+        % but has not been true since 2005, when we added user-specified
+        % type-specific unify and compare predicates to the language.
+        % This is because the user-specified unify/compare predicates
+        % may not always terminate.
+        %
+        % We should therefore delete the test and the then part.
+        % XXX However, doing so leads to the failure of several test cases:
+        %   term/exception_analysis_test2
+        %   term/existential_error1
+        %   term/occur
+        %   term/overlap
+        %   term/pl7_6_2c
+        %   term/pl8_3_1a
+        %   term/subset
+        % Until the addition of a "terminates" pragma for compare_time_t_reps,
+        % it also caused the building of time.c in the stage 2 library to fail.
+        %
+        % The best solution for this problem is
+        %
+        % - delete the condition and then-part here;
+        % - add "terminates" pragmas for unify, compare (and
+        %   compare_representation) in library/builtin.m, but then
+        % - generate an error if any user-specified unify or compare predicate
+        %   cannot be proven to terminate.
+        ( if
+            ModuleName = pred_info_module(PredInfo),
+            Name = pred_info_name(PredInfo),
+            pred_info_get_orig_arity(PredInfo, PredFormArity),
+            PredFormArity = pred_form_arity(PredFormArityInt),
+            special_pred_name_arity(SpecPredId0, Name, _, PredFormArityInt),
+            any_mercury_builtin_module(ModuleName)
+        then
+            SpecialPredId = SpecPredId0
+        else
+            pred_info_get_origin(PredInfo, Origin),
+            Origin = origin_compiler(made_for_uci(SpecialPredId, _))
+        )
+    then
+        set_generated_terminates(ProcIds, SpecialPredId, !ProcTable)
+    else
+        fail
+    ).
+
+:- pred set_generated_terminates(list(proc_id)::in, special_pred_id::in,
+    proc_table::in, proc_table::out) is det.
+
+set_generated_terminates([], _, !ProcTable).
+set_generated_terminates([ProcId | ProcIds], SpecialPredId, !ProcTable) :-
+    map.lookup(!.ProcTable, ProcId, ProcInfo0),
+    proc_info_get_headvars(ProcInfo0, HeadVars),
+    special_pred_id_to_termination(SpecialPredId, HeadVars,
+        ArgSize, Termination),
+    proc_info_set_maybe_arg_size_info(yes(ArgSize), ProcInfo0, ProcInfo1),
+    proc_info_set_maybe_termination_info(yes(Termination),
+        ProcInfo1, ProcInfo),
+    map.det_update(ProcId, ProcInfo, !ProcTable),
+    set_generated_terminates(ProcIds, SpecialPredId, !ProcTable).
+
+    % XXX The ArgSize argument for unify predicates may not be correct
+    % in the case where the type has user-defined equality.
+    %
+:- pred special_pred_id_to_termination(special_pred_id::in,
+    list(prog_var)::in, arg_size_info::out, termination_info::out) is det.
+
+special_pred_id_to_termination(SpecialPredId, HeadVars, ArgSize,
+        Termination) :-
+    (
+        SpecialPredId = spec_pred_compare,
+        term_osi_util.make_bool_list(HeadVars, [no, no, no], OutList),
+        ArgSize = finite(0, OutList),
+        Termination = cannot_loop(unit)
+    ;
+        SpecialPredId = spec_pred_unify,
+        term_osi_util.make_bool_list(HeadVars, [yes, yes], OutList),
+        ArgSize = finite(0, OutList),
+        Termination = cannot_loop(unit)
+    ;
+        SpecialPredId = spec_pred_index,
+        term_osi_util.make_bool_list(HeadVars, [no, no], OutList),
+        ArgSize = finite(0, OutList),
+        Termination = cannot_loop(unit)
+    ).
+
+    % The list of proc_ids must refer to builtin predicates. This predicate
+    % sets the termination information of builtin predicates.
+    %
+:- pred set_builtin_terminates(list(proc_id)::in, pred_id::in, pred_info::in,
+    module_info::in, proc_table::in, proc_table::out) is det.
+
+set_builtin_terminates([], _, _, _, !ProcTable).
+set_builtin_terminates([ProcId | ProcIds], PredId, PredInfo, ModuleInfo,
+        !ProcTable) :-
+    map.lookup(!.ProcTable, ProcId, ProcInfo0),
+    ( if all_args_input_or_zero_size(ModuleInfo, PredInfo, ProcInfo0) then
+        % The size of the output arguments will all be 0, independent of the
+        % size of the input variables.
+        % UsedArgs should be set to yes([no, no, ...]).
+        proc_info_get_headvars(ProcInfo0, HeadVars),
+        term_osi_util.make_bool_list(HeadVars, [], UsedArgs),
+        ArgSizeInfo = yes(finite(0, UsedArgs))
+    else
+        pred_info_get_context(PredInfo, Context),
+        Error = is_builtin(PredId),
+        ArgSizeError = term_error(Context, Error),
+        ArgSizeInfo = yes(infinite([ArgSizeError]))
+    ),
+    % XXX intermod
+    proc_info_set_maybe_arg_size_info(ArgSizeInfo, ProcInfo0, ProcInfo1),
+    proc_info_set_maybe_termination_info(yes(cannot_loop(unit)),
+        ProcInfo1, ProcInfo),
+    map.det_update(ProcId, ProcInfo, !ProcTable),
+    set_builtin_terminates(ProcIds, PredId, PredInfo, ModuleInfo, !ProcTable).
+
+%---------------------------------------------------------------------------%
+
+    % This predicate sets the arg_size_info property of the given list of
+    % procedures.
+    %
+    % change_procs_arg_size_info(ProcList, Override, TerminationInfo,
+    %       ProcTable, ProcTable)
+    %
+    % If Override is yes, then this predicate overrides any existing arg_size
+    % information. If Override is no, then it leaves the proc_info of a
+    % procedure unchanged unless the proc_info had no arg_size information
+    % (i.e. the maybe(arg_size_info) field was set to "no").
+    %
+:- pred change_procs_arg_size_info(list(proc_id)::in, bool::in,
+    arg_size_info::in, proc_table::in, proc_table::out) is det.
+
+change_procs_arg_size_info([], _, _, !ProcTable).
+change_procs_arg_size_info([ProcId | ProcIds], Override, ArgSize,
+        !ProcTable) :-
+    map.lookup(!.ProcTable, ProcId, ProcInfo0),
+    ( if
+        ( Override = yes
+        ; proc_info_get_maybe_arg_size_info(ProcInfo0, no)
+        )
+    then
+        proc_info_set_maybe_arg_size_info(yes(ArgSize), ProcInfo0, ProcInfo),
+        map.det_update(ProcId, ProcInfo, !ProcTable)
+    else
+        true
+    ),
+    change_procs_arg_size_info(ProcIds, Override, ArgSize, !ProcTable).
+
+    % change_procs_termination_info(ProcList, Override, TerminationInfo,
+    %     !ProcTable):
+    %
+    % This predicate sets the termination_info property of the given list of
+    % procedures.
+    %
+    % If Override is yes, then this predicate overrides any existing
+    % termination information. If Override is no, then it leaves the proc_info
+    % of a procedure unchanged unless the proc_info had no termination
+    % information (i.e. the maybe(termination_info) field was set to "no").
+    %
+:- pred change_procs_termination_info(list(proc_id)::in, bool::in,
+    termination_info::in, proc_table::in, proc_table::out) is det.
+
+change_procs_termination_info([], _, _, !ProcTable).
+change_procs_termination_info([ProcId | ProcIds], Override, Termination,
+        !ProcTable) :-
+    map.lookup(!.ProcTable, ProcId, ProcInfo0),
+    ( if
+        (
+            Override = yes
+        ;
+            proc_info_get_maybe_termination_info(ProcInfo0, no)
+        )
+    then
+        % XXX intermod
+        proc_info_set_maybe_termination_info(yes(Termination),
+            ProcInfo0, ProcInfo),
+        map.det_update(ProcId, ProcInfo, !ProcTable)
+    else
+        true
+    ),
+    change_procs_termination_info(ProcIds, Override, Termination, !ProcTable).
+
+%---------------------------------------------------------------------------%
+:- end_module termination.term_osi.term_osi_main.
+%---------------------------------------------------------------------------%
diff --git a/compiler/term_pass1.m b/compiler/term_osi_pass1.m
similarity index 98%
rename from compiler/term_pass1.m
rename to compiler/term_osi_pass1.m
index 8a679e10e..673ac7d15 100644
--- a/compiler/term_pass1.m
+++ b/compiler/term_osi_pass1.m
@@ -21,14 +21,14 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_pass1.
+:- module termination.term_osi.term_osi_pass1.
 :- interface.
 
 :- import_module hlds.
 :- import_module hlds.hlds_module.
 :- import_module hlds.pred_proc_id.
-:- import_module transform_hlds.term_errors.
-:- import_module transform_hlds.term_util.
+:- import_module termination.term_osi.term_osi_errors.
+:- import_module termination.term_osi.term_osi_util.
 
 :- import_module list.
 :- import_module pair.
@@ -65,7 +65,7 @@
 :- import_module parse_tree.prog_data.
 :- import_module parse_tree.prog_data_pragma.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.term_traversal.
+:- import_module termination.term_osi.term_osi_traversal.
 
 :- import_module bag.
 :- import_module bool.
@@ -472,5 +472,5 @@ pred_proc_var(PPId, Var, !Varset, !PPVars) :-
     ).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_pass1.
+:- end_module termination.term_osi.term_osi_pass1.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_pass2.m b/compiler/term_osi_pass2.m
similarity index 98%
rename from compiler/term_pass2.m
rename to compiler/term_osi_pass2.m
index 508042366..acc434d31 100644
--- a/compiler/term_pass2.m
+++ b/compiler/term_osi_pass2.m
@@ -16,13 +16,13 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_pass2.
+:- module termination.term_osi.term_osi_pass2.
 :- interface.
 
 :- import_module hlds.
 :- import_module hlds.hlds_module.
 :- import_module hlds.pred_proc_id.
-:- import_module transform_hlds.term_util.
+:- import_module termination.term_osi.term_osi_util.
 
 %---------------------------------------------------------------------------%
 
@@ -45,8 +45,8 @@
 :- import_module parse_tree.
 :- import_module parse_tree.prog_data.
 :- import_module parse_tree.prog_data_pragma.
-:- import_module transform_hlds.term_errors.
-:- import_module transform_hlds.term_traversal.
+:- import_module termination.term_osi.term_osi_errors.
+:- import_module termination.term_osi.term_osi_traversal.
 
 :- import_module assoc_list.
 :- import_module bag.
@@ -631,5 +631,5 @@ zero_or_positive_weight_cycles_from_neighbour(CallWeights,
 map_to_no(_, no).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_pass2.
+:- end_module termination.term_osi.term_osi_pass2.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_traversal.m b/compiler/term_osi_traversal.m
similarity index 99%
rename from compiler/term_traversal.m
rename to compiler/term_osi_traversal.m
index a8117084e..b8c84feee 100644
--- a/compiler/term_traversal.m
+++ b/compiler/term_osi_traversal.m
@@ -18,7 +18,7 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_traversal.
+:- module termination.term_osi.term_osi_traversal.
 :- interface.
 
 :- import_module hlds.
@@ -28,9 +28,9 @@
 :- import_module parse_tree.
 :- import_module parse_tree.prog_data.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.term_errors.
-:- import_module transform_hlds.term_norm.
-:- import_module transform_hlds.term_util.
+:- import_module termination.term_norm.
+:- import_module termination.term_osi.term_osi_errors.
+:- import_module termination.term_osi.term_osi_util.
 
 :- import_module bag.
 :- import_module list.
@@ -745,5 +745,5 @@ params_get_max_paths(Params, X) :-
     X = Params ^ term_trav_max_paths.
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_traversal.
+:- end_module termination.term_osi.term_osi_traversal.
 %---------------------------------------------------------------------------%
diff --git a/compiler/term_util.m b/compiler/term_osi_util.m
similarity index 98%
rename from compiler/term_util.m
rename to compiler/term_osi_util.m
index 0436440b3..254dbf31f 100644
--- a/compiler/term_util.m
+++ b/compiler/term_osi_util.m
@@ -17,7 +17,7 @@
 %
 %---------------------------------------------------------------------------%
 
-:- module transform_hlds.term_util.
+:- module termination.term_osi.term_osi_util.
 :- interface.
 
 :- import_module hlds.
@@ -31,8 +31,8 @@
 :- import_module parse_tree.prog_data_foreign.
 :- import_module parse_tree.prog_data_pragma.
 :- import_module parse_tree.var_table.
-:- import_module transform_hlds.term_errors.
-:- import_module transform_hlds.term_norm.
+:- import_module termination.term_norm.
+:- import_module termination.term_osi.term_osi_errors.
 
 :- import_module bag.
 :- import_module bool.
@@ -436,5 +436,5 @@ should_we_believe_check_termination_markers(ModuleInfo, Believe) :-
     ).
 
 %---------------------------------------------------------------------------%
-:- end_module transform_hlds.term_util.
+:- end_module termination.term_osi.term_osi_util.
 %---------------------------------------------------------------------------%
diff --git a/compiler/post_term_analysis.m b/compiler/term_post_analysis.m
similarity index 99%
rename from compiler/post_term_analysis.m
rename to compiler/term_post_analysis.m
index 92c2a79b8..d8bea72e9 100644
--- a/compiler/post_term_analysis.m
+++ b/compiler/term_post_analysis.m
@@ -19,7 +19,7 @@
 %
 %----------------------------------------------------------------------------%
 
-:- module transform_hlds.post_term_analysis.
+:- module termination.term_post_analysis.
 :- interface.
 
 :- import_module hlds.
@@ -306,5 +306,5 @@ generate_non_term_user_special_warning(Context, SpecialPred, TypeCtor,
     !:Specs = [Spec | !.Specs].
 
 %----------------------------------------------------------------------------%
-:- end_module transform_hlds.post_term_analysis.
+:- end_module termination.term_post_analysis.
 %----------------------------------------------------------------------------%
diff --git a/compiler/termination.m b/compiler/termination.m
index fa7a05c4e..3555cf623 100644
--- a/compiler/termination.m
+++ b/compiler/termination.m
@@ -1,929 +1,31 @@
-%---------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
 % vim: ft=mercury ts=4 sw=4 et
-%---------------------------------------------------------------------------%
-% Copyright (C) 1997-2001, 2003-2012 The University of Melbourne.
-% Copyright (C) 2014-2020, 2022-2026 The Mercury Team.
+%-----------------------------------------------------------------------------%
+% Copyright (C) 2026 The Mercury team.
 % This file may only be copied under the terms of the GNU General
 % Public License - see the file COPYING in the Mercury distribution.
-%---------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
 %
-% File: termination.m.
-% Main author: crs.
-% Significant modifications by zs.
+% This package contains our two termination analysis systems.
 %
-% This termination analysis is based on the algorithm given by Gerhard Groeger
-% and Lutz Plumer in their paper "Handling of Mutual Recursion in Automatic
-% Termination Proofs for Logic Programs"  which was printed in JICSLP '92 (the
-% proceedings of the Joint International Conference and Symposium on Logic
-% Programming 1992) pages 336 - 350.
+% At the moment, they are wholly separate, but they do contain
+% some very similar code. If these are ever factored out, this package
+% is the natural home of the results.
 %
-% Details about this implementation are covered in:
-% Chris Speirs, Zoltan Somogyi, and Harald Sondergaard. Termination
-% analysis for Mercury. In P. Van Hentenryck, editor, Static Analysis:
-% Proceedings of the 4th International Symposium, Lecture Notes in Computer
-% Science. Springer, 1997. A more detailed version is available for
-% download from the papers page of mercurylang.org.
-%
-% The termination analysis may use a number of different norms to calculate
-% the size of a term. These are set by using the --termination-norm string
-% option.
-%
-%---------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
 
-:- module transform_hlds.termination.
+:- module termination.
 :- interface.
 
-:- import_module hlds.
-:- import_module hlds.hlds_module.
-:- import_module parse_tree.
-:- import_module parse_tree.error_spec.
+:- include_module term_osi.     % Our first termination analyser.
+:- include_module term_constr.  % Our second termination analyser.
 
-:- import_module list.
-
-%---------------------------------------------------------------------------%
-
-    % Perform termination analysis on the module.
-    %
-:- pred analyse_termination_in_module(module_info::in, module_info::out,
-    list(diag_spec)::out) is det.
-
-%---------------------------------------------------------------------------%
-%---------------------------------------------------------------------------%
+:- include_module term_norm.
 
 :- implementation.
 
-:- import_module hlds.hlds_dependency_graph.
-:- import_module hlds.hlds_error_util.
-:- import_module hlds.hlds_goal.
-:- import_module hlds.hlds_markers.
-:- import_module hlds.hlds_pred.
-:- import_module hlds.hlds_pred_tests.
-:- import_module hlds.hlds_proc.
-:- import_module hlds.pred_name.
-:- import_module hlds.pred_proc_id.
-:- import_module hlds.status.
-:- import_module libs.
-:- import_module libs.dependency_graph.
-:- import_module libs.globals.
-:- import_module libs.options.
-:- import_module mdbcomp.
-:- import_module mdbcomp.builtin_modules.
-:- import_module mdbcomp.prim_data.
-:- import_module parse_tree.prog_data.
-:- import_module parse_tree.prog_data_foreign.
-:- import_module parse_tree.prog_data_pragma.
-:- import_module transform_hlds.post_term_analysis.
-:- import_module transform_hlds.term_errors.
-:- import_module transform_hlds.term_norm.
-:- import_module transform_hlds.term_pass1.
-:- import_module transform_hlds.term_pass2.
-:- import_module transform_hlds.term_util.
+:- include_module term_post_analysis.
 
-:- import_module bool.
-:- import_module map.
-:- import_module maybe.
-:- import_module pair.
-:- import_module require.
-:- import_module set.
-:- import_module term.
-:- import_module unit.
-
-%---------------------------------------------------------------------------%
-
-analyse_termination_in_module(!ModuleInfo, !:Specs) :-
-    module_info_get_globals(!.ModuleInfo, Globals),
-    globals.get_termination_norm(Globals, TermNorm),
-    FunctorInfo = set_functor_info(!.ModuleInfo, TermNorm),
-    globals.lookup_int_option(Globals, termination_error_limit, MaxErrors),
-    globals.lookup_int_option(Globals, termination_path_limit, MaxPaths),
-    PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths),
-
-    % Process builtin and compiler-generated predicates, and user-supplied
-    % pragmas.
-    should_we_believe_check_termination_markers(!.ModuleInfo,
-        BelieveCheckTerm),
-    module_info_get_valid_pred_ids(!.ModuleInfo, PredIds),
-    term_preprocess_preds(BelieveCheckTerm, PredIds, !ModuleInfo),
-
-    % Process all the SCCs of the call graph in a bottom-up order.
-    module_info_ensure_dependency_info(!ModuleInfo, DepInfo),
-    SCCs = dependency_info_get_bottom_up_sccs(DepInfo),
-
-    % Set the termination status of foreign_procs based on the foreign code
-    % attributes.
-    !:Specs = [],
-    check_foreign_code_attributes(SCCs, !ModuleInfo, !Specs),
-
-    % Ensure that termination pragmas for a procedure do not conflict with
-    % termination pragmas for other procedures in the SCC.
-    check_pragmas_are_consistent(SCCs, !ModuleInfo, !Specs),
-
-    list.foldl2(analyse_termination_in_scc(PassInfo), SCCs,
-        !ModuleInfo, !Specs),
-    run_post_term_analysis(!.ModuleInfo, PostSpecs),
-    !:Specs = PostSpecs ++ !.Specs,
-
-    module_info_get_proc_analysis_kinds(!.ModuleInfo, ProcAnalysisKinds0),
-    set.insert(pak_termination, ProcAnalysisKinds0, ProcAnalysisKinds),
-    module_info_set_proc_analysis_kinds(ProcAnalysisKinds, !ModuleInfo).
-
-%---------------------------------------------------------------------------%
-%
-% Handle foreign code attributes.
-%
-
-% Set the termination status for any procedures implemented using the foreign
-% language interface. If the terminates/does_not_terminate attribute has been
-% set then we set the termination status of the procedure accordingly.
-% Otherwise the procedure is considered to be terminating if it does not call
-% Mercury and non-terminating if it does.
-%
-% We also check that the foreign code attributes do not conflict with any
-% termination pragmas that have been supplied for the procedure.
-
-:- pred check_foreign_code_attributes(list(scc)::in,
-    module_info::in, module_info::out,
-    list(diag_spec)::in, list(diag_spec)::out) is det.
-
-check_foreign_code_attributes(SCCs, !ModuleInfo, !Specs) :-
-    list.foldl2(check_foreign_code_attributes_in_scc, SCCs,
-        !ModuleInfo, !Specs).
-
-:- pred check_foreign_code_attributes_in_scc(scc::in,
-    module_info::in, module_info::out,
-    list(diag_spec)::in, list(diag_spec)::out) is det.
-
-check_foreign_code_attributes_in_scc(SCC, !ModuleInfo, !Specs) :-
-    set.to_sorted_list(SCC, PPIds),
-    (
-        PPIds = [],
-        unexpected($pred, "empty SCC")
-    ;
-        PPIds = [PPId],
-        module_info_pred_proc_info(!.ModuleInfo, PPId, PredInfo, ProcInfo0),
-        proc_info_get_goal(ProcInfo0, Goal),
-        Goal = hlds_goal(GoalExpr, _GoalInfo),
-        ( if GoalExpr = call_foreign_proc(Attributes, _, _, _, _, _, _) then
-            check_foreign_code_attributes_of_proc(!.ModuleInfo, PPId,
-                PredInfo, Attributes, ProcInfo0, ProcInfo, !Specs),
-            module_info_set_pred_proc_info(PPId, PredInfo, ProcInfo,
-                !ModuleInfo)
-        else
-            true
-        )
-    ;
-        PPIds = [_, _ | _]
-        % Foreign code proc cannot be mutually recursive.
-    ).
-
-:- pred check_foreign_code_attributes_of_proc(module_info::in,
-    pred_proc_id::in, pred_info::in, foreign_proc_attributes::in,
-    proc_info::in, proc_info::out,
-    list(diag_spec)::in, list(diag_spec)::out) is det.
-
-check_foreign_code_attributes_of_proc(ModuleInfo, PPId, _PredInfo, Attributes,
-        !ProcInfo, !Specs) :-
-% XXX This *should* be enough to make termination analysis decide that
-% the difftime and therefore compare_time_t_reps predicates in library/time.m
-% terminate *without* an explicit terminates pragma, but it is NOT enough.
-%
-%   pred_info_get_arg_types(PredInfo, ArgTypes),
-%   proc_info_get_argmodes(!.ProcInfo, ArgModes),
-%   ( if all_outputs_are_builtins(ModuleInfo, ArgTypes, ArgModes, Nos) then
-%       % XXX norm dependent
-%       ArgSizeInfo = finite(0, Nos),
-%       proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo), !ProcInfo)
-%   else
-%       true
-%   ),
-    proc_info_get_maybe_termination_info(!.ProcInfo, MaybeTermination),
-    proc_info_get_context(!.ProcInfo, Context),
-    (
-        MaybeTermination = no,
-        ( if attributes_imply_termination(Attributes) then
-            TermStatus = yes(cannot_loop(unit)),
-            proc_info_set_maybe_termination_info(TermStatus, !ProcInfo)
-        else
-            TermErr = term_error(Context, does_not_term_foreign(PPId)),
-            TermStatus = yes(can_loop([TermErr])),
-            proc_info_set_maybe_termination_info(TermStatus, !ProcInfo)
-        )
-    ;
-        % If there was a `:- pragma terminates' declaration for this procedure,
-        % then check that the foreign code attributes do not contradict this.
-        MaybeTermination = yes(cannot_loop(_)),
-        ProcTerminates = get_terminates(Attributes),
-        (
-            ProcTerminates = proc_does_not_terminate,
-            TermErr = term_error(Context, inconsistent_annotations),
-            TermStatus = yes(can_loop([TermErr])),
-            % XXX intermod
-            proc_info_set_maybe_termination_info(TermStatus, !ProcInfo),
-            ProcNamePieces = describe_one_proc_name(ModuleInfo,
-                yes(color_subject), should_module_qualify, PPId),
-            Pieces = [words("Warning:") | ProcNamePieces] ++
-                [words("has a")] ++
-                color_as_inconsistent([pragma_decl("terminates"),
-                    words("declaration,")]) ++
-                [words("but also has the")] ++
-                color_as_inconsistent([quote("does_not_terminate"),
-                    words("foreign code attribute")]) ++
-                [words("set."), nl],
-            Severity = severity_warning(warn_requested_by_option),
-            Spec = spec($pred, Severity, phase_read_files, Context, Pieces),
-            !:Specs = [Spec | !.Specs]
-        ;
-            ( ProcTerminates = proc_terminates
-            ; ProcTerminates = depends_on_mercury_calls
-            )
-        )
-    ;
-        % If there was a `:- pragma does_not_terminate' declaration
-        % for this procedure, then check that the foreign code attributes
-        % do not contradict this.
-        MaybeTermination = yes(can_loop(TermErrs0)),
-        ProcTerminates = get_terminates(Attributes),
-        (
-            ProcTerminates = proc_terminates,
-            TermErr = term_error(Context, inconsistent_annotations),
-            TermErrs = [TermErr | TermErrs0],
-            TermStatus = yes(can_loop(TermErrs)),
-            % XXX intermod
-            proc_info_set_maybe_termination_info(TermStatus, !ProcInfo),
-            ProcNamePieces = describe_one_proc_name(ModuleInfo,
-                yes(color_subject), should_module_qualify, PPId),
-            Pieces = [words("Warning:") | ProcNamePieces] ++
-                [words("has a")] ++
-                color_as_inconsistent([pragma_decl("does_not_terminate"),
-                    words("declaration,")]) ++
-                [words("but also has the")] ++
-                color_as_inconsistent([quote("terminates"),
-                    words("foreign code attribute")]) ++
-                [words("set."), nl],
-            Severity = severity_warning(warn_requested_by_option),
-            Spec = spec($pred, Severity, phase_read_files, Context, Pieces),
-            !:Specs = [Spec | !.Specs]
-        ;
-            ( ProcTerminates = proc_does_not_terminate
-            ; ProcTerminates = depends_on_mercury_calls
-            )
-        )
-    ).
-
-% XXX This is part of the non-working, commented-out code at the top of
-% check_foreign_code_attributes_of_proc.
-%
-% :- pred all_outputs_are_builtins(module_info::in,
-%     list(mer_type)::in, list(mer_mode)::in, list(bool)::out) is semidet.
-%
-% all_outputs_are_builtins(_, [], [], []).
-% all_outputs_are_builtins(_, [], [_ | _], []) :-
-%     unexpected($pred, "list length mismatch").
-% all_outputs_are_builtins(_, [_ | _], [], []) :-
-%     unexpected($pred, "list length mismatch").
-% all_outputs_are_builtins(ModuleInfo, [Type | Types], [Mode | Modes], Nos) :-
-%     all_outputs_are_builtins(ModuleInfo, Types, Modes, TailNos),
-%     ( if mode_is_output(ModuleInfo, Mode) then
-%         Type = builtin_type(_)
-%     else
-%         true
-%     ),
-%     Nos = [no | TailNos].
-
-%---------------------------------------------------------------------------%
-%
-% Check termination pragmas for consistency.
-%
-
-% Check that any user-supplied termination information (from pragma
-% terminates/does_not_terminate) is consistent for each SCC in the program.
-%
-% The information will not be consistent if:
-% (1) One or more procs. in the SCC has a terminates pragma *and* one or more
-%     procs. in the SCC has a does_not_terminate pragma.
-% (2) One or more procs. in the SCC has a termination pragma (of either sort),
-%     *and* the termination status of one or more procs. in the SCC is
-%     unknown. (We check this after checking for the first case, so the
-%     termination info. for the known procs. will be consistent.)
-%
-% In the first case set the termination for all procs. in the SCC to can_loop
-% and emit a warning. In the second, set the termination of any procedures
-% whose termination status is unknown to be the same as those whose
-% termination status is known.
-
-:- pred check_pragmas_are_consistent(list(scc)::in,
-    module_info::in, module_info::out,
-    list(diag_spec)::in, list(diag_spec)::out) is det.
-
-check_pragmas_are_consistent(SCCs, !ModuleInfo, !Specs) :-
-    list.foldl2(check_scc_pragmas_are_consistent, SCCs, !ModuleInfo, !Specs).
-
-:- pred check_scc_pragmas_are_consistent(scc::in,
-    module_info::in, module_info::out,
-    list(diag_spec)::in, list(diag_spec)::out) is det.
-
-check_scc_pragmas_are_consistent(SCC, !ModuleInfo, !Specs) :-
-    classify_termination_status(!.ModuleInfo,  set.to_sorted_list(SCC),
-        set.init, KnownPredNamesIdsSet, set.init, KnownContextSet,
-        set.init, KnownTermStatusSet, set.init, UnknownPPIdSet),
-    KnownTermStatuses = set.to_sorted_list(KnownTermStatusSet),
-    (
-        KnownTermStatuses = []
-        % We don't know the termination status of any procedure in the SCC.
-    ;
-        KnownTermStatuses = [KnownTermStatus],
-        % We know the termination status of at least one procedure in the SCC,
-        % and all the procedures that do have known termination statuses
-        % have the same termination status.
-        set.foldl(set_termination_info(KnownTermStatus),
-            UnknownPPIdSet, !ModuleInfo)
-    ;
-        KnownTermStatuses = [_, _ | _],
-        % We know the termination status of at least two procedures
-        % in the SCC, and those procedures have two *different*
-        % termination statuses.
-
-        % Emit a warning, and then assume that they all loop.
-        LeastContext = list.det_head(set.to_sorted_list(KnownContextSet)),
-        NewTermStatus =
-            can_loop([term_error(LeastContext, inconsistent_annotations)]),
-        set.foldl(set_termination_info(NewTermStatus), SCC, !ModuleInfo),
-
-        PredNamesIds = set.to_sorted_list(KnownPredNamesIdsSet),
-        PredNamePieces = describe_several_pred_names(!.ModuleInfo,
-            yes(color_subject), should_module_qualify,
-            list.map(pair.snd, PredNamesIds)),
-        Pieces = [words("Warning:")] ++ PredNamePieces ++
-            [words("are mutually recursive,"),
-            words("but some of their termination pragmas are")] ++
-            color_as_incorrect([words("inconsistent.")]) ++
-            [nl],
-        Severity = severity_warning(warn_requested_by_option),
-        Spec = spec($pred, Severity, phase_read_files, LeastContext, Pieces),
-        !:Specs = [Spec | !.Specs]
-    ).
-
-:- pred classify_termination_status(module_info::in, list(pred_proc_id)::in,
-    set(pair(string, pred_id))::in, set(pair(string, pred_id))::out,
-    set(prog_context)::in, set(prog_context)::out,
-    set(termination_info)::in, set(termination_info)::out,
-    set(pred_proc_id)::in, set(pred_proc_id)::out) is det.
-
-classify_termination_status(_, [],
-        !KnownPredNamesIds, !KnownContexts,
-        !KnownTermStatuses, !UnknownPPIds).
-classify_termination_status(ModuleInfo, [PPId | PPIds],
-        !KnownPredNamesIds, !KnownContexts,
-        !KnownTermStatuses, !UnknownPPIds) :-
-    module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, ProcInfo),
-    proc_info_get_maybe_termination_info(ProcInfo, MaybeTermStatus),
-    (
-        MaybeTermStatus = yes(TermStatus),
-        PredName = pred_info_name(PredInfo),
-        PPId = proc(PredId, _ProcId),
-        set.insert(PredName - PredId, !KnownPredNamesIds),
-        % XXX We should be getting the context from the *Proc*Info.
-        pred_info_get_context(PredInfo, Context),
-        set.insert(Context, !KnownContexts),
-        set.insert(TermStatus, !KnownTermStatuses)
-    ;
-        MaybeTermStatus = no,
-        set.insert(PPId, !UnknownPPIds)
-    ),
-    classify_termination_status(ModuleInfo, PPIds,
-        !KnownPredNamesIds, !KnownContexts,
-        !KnownTermStatuses, !UnknownPPIds).
-
-%---------------------------------------------------------------------------%
-%
-% Run termination analysis on a single SCC.
-%
-
-    % For each SCC, we first find out the relationships among the sizes of the
-    % arguments of the procedures of the SCC, and then attempt to prove
-    % termination of the procedures.
-    %
-:- pred analyse_termination_in_scc(pass_info::in, scc::in,
-    module_info::in, module_info::out,
-    list(diag_spec)::in, list(diag_spec)::out) is det.
-
-analyse_termination_in_scc(PassInfo, SCC, !ModuleInfo, !Specs) :-
-    IsArgSizeKnown =
-        ( pred(PPId::in) is semidet :-
-            module_info_pred_proc_info(!.ModuleInfo, PPId, _, ProcInfo),
-            proc_info_get_maybe_arg_size_info(ProcInfo, yes(_))
-        ),
-    set.filter(IsArgSizeKnown, SCC, _SCCArgSizeKnown, SCCArgSizeUnknown),
-    ( if set.is_empty(SCCArgSizeUnknown) then
-        ArgSizeErrors = [],
-        TermErrors = []
-    else
-        find_arg_sizes_in_scc(!.ModuleInfo, PassInfo, SCCArgSizeUnknown,
-            ArgSizeResult, TermErrors),
-        (
-            ArgSizeResult = arg_size_ok(Solutions, OutputSupplierMap),
-            set_finite_arg_size_infos(Solutions, OutputSupplierMap,
-                !ModuleInfo),
-            ArgSizeErrors = []
-        ;
-            ArgSizeResult = arg_size_error(Errors),
-            set.foldl(set_infinite_arg_size_info(infinite(Errors)),
-                SCCArgSizeUnknown, !ModuleInfo),
-            ArgSizeErrors = Errors
-        )
-    ),
-    set.filter(is_termination_known(!.ModuleInfo), SCC,
-        _SCCTerminationKnown, SCCTerminationUnknown),
-    ( if set.is_empty(SCCTerminationUnknown) then
-        % We may possibly have encountered inconsistent
-        % terminates/does_not_terminate pragmas for this SCC, so we need to
-        % report errors here as well.
-        % XXX That comment does not make sense here.
-        true
-    else
-        IsFatal =
-            ( pred(Error::in) is semidet :-
-                Error = term_error(_Context, ErrorKind),
-                term_error_kind_is_fatal_error(ErrorKind) = yes
-            ),
-        list.filter(IsFatal, ArgSizeErrors, FatalErrors),
-        BothErrors = TermErrors ++ FatalErrors,
-        (
-            BothErrors = [_ | _],
-            % These errors prevent pass 2 from proving termination
-            % in any case, so we may as well not prove it quickly.
-            PassInfo = pass_info(_, MaxErrors, _),
-            list.take_upto(MaxErrors, BothErrors, ReportedErrors),
-            TerminationResult = can_loop(ReportedErrors)
-        ;
-            BothErrors = [],
-            module_info_get_globals(!.ModuleInfo, Globals),
-            globals.lookup_int_option(Globals, termination_single_args,
-                SingleArgs),
-            prove_termination_in_scc(!.ModuleInfo, PassInfo,
-                SCCTerminationUnknown, SingleArgs, TerminationResult)
-        ),
-        set.foldl(set_termination_info(TerminationResult),
-            SCCTerminationUnknown, !ModuleInfo),
-        (
-            TerminationResult = can_loop(TerminationErrors),
-            maybe_report_termination_errors(!.ModuleInfo, SCC,
-                TerminationErrors, !Specs)
-        ;
-            TerminationResult = cannot_loop(_)
-        )
-    ).
-
-%---------------------------------------------------------------------------%
-
-    % This predicate takes the results from solve_equations and inserts these
-    % results into the module info.
-    %
-:- pred set_finite_arg_size_infos(list(pair(pred_proc_id, int))::in,
-    used_args::in, module_info::in, module_info::out) is det.
-
-set_finite_arg_size_infos([], _, !ModuleInfo).
-set_finite_arg_size_infos([Soln | Solns], OutputSupplierMap, !ModuleInfo) :-
-    Soln = PPId - Gamma,
-    PPId = proc(PredId, ProcId),
-    module_info_pred_proc_info(!.ModuleInfo, PredId, ProcId,
-        PredInfo0, ProcInfo0),
-    map.lookup(OutputSupplierMap, PPId, OutputSuppliers),
-    ArgSizeInfo = finite(Gamma, OutputSuppliers),
-    % XXX intermod
-    proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo), ProcInfo0, ProcInfo),
-    pred_info_set_proc_info(ProcId, ProcInfo, PredInfo0, PredInfo),
-    module_info_set_pred_info(PredId, PredInfo, !ModuleInfo),
-    set_finite_arg_size_infos(Solns, OutputSupplierMap, !ModuleInfo).
-
-:- pred set_infinite_arg_size_info(arg_size_info::in, pred_proc_id::in,
-    module_info::in, module_info::out) is det.
-
-set_infinite_arg_size_info(ArgSizeInfo, PPId, !ModuleInfo) :-
-    PPId = proc(PredId, ProcId),
-    module_info_pred_proc_info(!.ModuleInfo, PredId, ProcId,
-        PredInfo0, ProcInfo0),
-    % XXX intermod
-    proc_info_set_maybe_arg_size_info(yes(ArgSizeInfo), ProcInfo0, ProcInfo),
-    pred_info_set_proc_info(ProcId, ProcInfo, PredInfo0, PredInfo),
-    module_info_set_pred_info(PredId, PredInfo, !ModuleInfo).
-
-%---------------------------------------------------------------------------%
-
-:- pred set_termination_info(termination_info::in, pred_proc_id::in,
-    module_info::in, module_info::out) is det.
-
-set_termination_info(TerminationInfo, PPId, !ModuleInfo) :-
-    PPId = proc(PredId, ProcId),
-    module_info_pred_proc_info(!.ModuleInfo, PredId, ProcId,
-        PredInfo0, ProcInfo0),
-    % XXX intermod
-    proc_info_set_maybe_termination_info(yes(TerminationInfo),
-        ProcInfo0, ProcInfo),
-    pred_info_set_proc_info(ProcId, ProcInfo, PredInfo0, PredInfo),
-    module_info_set_pred_info(PredId, PredInfo, !ModuleInfo).
-
-%---------------------------------------------------------------------------%
-
-:- pred maybe_report_termination_errors(module_info::in, scc::in,
-    list(term_error)::in,
-    list(diag_spec)::in, list(diag_spec)::out) is det.
-
-maybe_report_termination_errors(ModuleInfo, SCC, Errors, !Specs) :-
-    decide_what_term_errors_to_report(ModuleInfo, SCC, Errors,
-        MaybeErrorsToReport),
-    (
-        MaybeErrorsToReport = no
-    ;
-        MaybeErrorsToReport = yes(ErrorsToReport),
-        report_term_errors(ModuleInfo, SCC, ErrorsToReport, !Specs)
-    ).
-
-:- pred decide_what_term_errors_to_report(module_info::in, scc::in,
-    list(term_error)::in, maybe(list(term_error))::out) is det.
-
-decide_what_term_errors_to_report(ModuleInfo, SCC, Errors,
-        MaybeErrorsToReport) :-
-    % NOTE The code of this predicate follows the same logic as the
-    % code of decide_what_term2_errors_to_report in term_constr_errors.m.
-    % Although there are differences in the data types they operate on
-    % and the options they consult, any changes here probably require
-    % corresponding changes there as well.
-
-    module_info_get_globals(ModuleInfo, Globals),
-    globals.lookup_bool_option(Globals, termination_check, NormalErrors),
-    globals.lookup_bool_option(Globals, termination_check_verbose,
-        VerboseErrors),
-    ( if
-        IsCheckTerm =
-            ( pred(PPId::in) is semidet :-
-                module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, _),
-                not pred_info_is_imported(PredInfo),
-                pred_info_get_markers(PredInfo, Markers),
-                marker_is_present(Markers, marker_check_termination)
-            ),
-        set.filter(IsCheckTerm, SCC, CheckTermPPIds),
-        set.is_non_empty(CheckTermPPIds)
-    then
-        % If any procedure in the SCC has a check_terminates pragma,
-        % print out one error message for the whole SCC and indicate an error.
-        MaybeErrorsToReport = yes(Errors)
-    else if
-        IsNonImported =
-            ( pred(PPId::in) is semidet :-
-                module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, _),
-                not pred_info_is_imported(PredInfo)
-            ),
-        set.filter(IsNonImported, SCC, NonImportedPPIds),
-        set.is_non_empty(NonImportedPPIds)
-    then
-        (
-            VerboseErrors = yes,
-            % If verbose errors is enabled, then output both direct and
-            % indirect errors.
-            % (See term_errors.m for details of direct and indirect errors.)
-            MaybeErrorsToReport = yes(Errors)
-        ;
-            VerboseErrors = no,
-            (
-                NormalErrors = yes,
-                % We prefer reporting only the direct errors, but if there are
-                % no direct errors, then output all the errors, which will then
-                % all be indirect errors. This is better than giving no error
-                % at all, which would lead to a message reporting that
-                % termination could not be proven for "unknown reasons".
-                IsDirect =
-                    ( pred(Error::in) is semidet :-
-                        Error = term_error(_, ErrorKind),
-                        term_error_kind_is_direct_error(ErrorKind) = yes
-                    ),
-                list.filter(IsDirect, Errors, DirectErrors),
-                (
-                    DirectErrors = [],
-                    MaybeErrorsToReport = yes(Errors)
-                ;
-                    DirectErrors = [_ | _],
-                    MaybeErrorsToReport = yes(DirectErrors)
-                )
-            ;
-                NormalErrors = no,
-                MaybeErrorsToReport = no
-            )
-        )
-    else
-        MaybeErrorsToReport = no
-    ).
-
-%---------------------------------------------------------------------------%
-
-    % This predicate preprocesses each predicate and sets the termination
-    % property if possible. This is done as follows.
-    %
-    % Set the termination to cannot_loop if:
-    % - there is a terminates pragma defined for the predicate;
-    % - there is a `check_termination' pragma defined for the predicate,
-    %   and it is imported, and the compiler is not currently generating
-    %   the intermodule optimization file; or
-    % - the predicate is a builtin predicate or is compiler generated (This
-    %   also sets the termination constant and UsedArgs).
-    %
-    % Set the termination to can_loop if:
-    % - there is a `does_not_terminate' pragma defined for this predicate; or
-    % - the predicate is imported and there is no other source of
-    %   information about it (termination_info pragmas, terminates pragmas,
-    %   check_termination pragmas, builtin/compiler generated).
-    %
-:- pred term_preprocess_preds(maybe_believe_check_termination::in,
-    list(pred_id)::in, module_info::in, module_info::out) is det.
-
-term_preprocess_preds(_, [], !ModuleInfo).
-term_preprocess_preds(BelieveCheckTerm, [PredId | PredIds], !ModuleInfo) :-
-    term_preprocess_pred(BelieveCheckTerm, PredId, !ModuleInfo),
-    term_preprocess_preds(BelieveCheckTerm, PredIds, !ModuleInfo).
-
-:- pred term_preprocess_pred(maybe_believe_check_termination::in,
-    pred_id::in, module_info::in, module_info::out) is det.
-
-term_preprocess_pred(BelieveCheckTerm, PredId, !ModuleInfo) :-
-    module_info_pred_info(!.ModuleInfo, PredId, PredInfo0),
-    pred_info_get_status(PredInfo0, PredStatus),
-    pred_info_get_context(PredInfo0, Context),
-    pred_info_get_proc_table(PredInfo0, ProcTable0),
-    pred_info_get_markers(PredInfo0, Markers),
-    ProcIds = pred_info_all_proc_ids(PredInfo0),
-    ( if
-        % It is possible for compiler generated/mercury builtin predicates
-        % to be imported or locally defined, so they must be covered here,
-        % separately.
-        set_compiler_gen_terminates(!.ModuleInfo, PredId, PredInfo0,
-            ProcIds, ProcTable0, ProcTable1)
-    then
-        ProcTable2 = ProcTable1
-    else if
-        pred_status_defined_in_this_module(PredStatus) = yes
-    then
-        % Since we cannot see their definition, we consider procedures
-        % which have a `:- pragma external_{pred/func}' to be imported.
-        ( if marker_is_present(Markers, marker_terminates) then
-            change_procs_termination_info(ProcIds, yes, cannot_loop(unit),
-                ProcTable0, ProcTable2)
-        else
-            ProcTable2 = ProcTable0
-        )
-    else
-        % Not defined in this module.
-
-        % All of the predicates that are processed in this section are imported
-        % in some way. With imported predicates, any 'check_termination'
-        % pragmas will be checked by the compiler when it compiles the
-        % relevant source file (that the predicate was imported from).
-        % When making the intermodule optimizations, the check_termination
-        % will not be checked when the relevant source file is compiled,
-        % so it cannot be depended upon.
-        ( if
-            (
-                marker_is_present(Markers, marker_terminates)
-            ;
-                BelieveCheckTerm = do_believe_check_termination,
-                marker_is_present(Markers, marker_check_termination)
-            )
-        then
-            change_procs_termination_info(ProcIds, yes, cannot_loop(unit),
-                ProcTable0, ProcTable1)
-        else
-            TerminationError = term_error(Context, imported_pred),
-            TerminationInfo = can_loop([TerminationError]),
-            change_procs_termination_info(ProcIds, no, TerminationInfo,
-                ProcTable0, ProcTable1)
-        ),
-        ArgSizeError = term_error(Context, imported_pred),
-        ArgSizeInfo = infinite([ArgSizeError]),
-        change_procs_arg_size_info(ProcIds, no, ArgSizeInfo,
-            ProcTable1, ProcTable2)
-    ),
-    ( if marker_is_present(Markers, marker_does_not_terminate) then
-        RequestError = term_error(Context, does_not_term_pragma(PredId)),
-        RequestTerminationInfo = can_loop([RequestError]),
-        change_procs_termination_info(ProcIds, yes,
-            RequestTerminationInfo, ProcTable2, ProcTable)
-    else
-        ProcTable = ProcTable2
-    ),
-    pred_info_set_proc_table(ProcTable, PredInfo0, PredInfo),
-    module_info_set_pred_info(PredId, PredInfo, !ModuleInfo).
-
-%---------------------------------------------------------------------------%
-
-    % This predicate checks each ProcId in the list to see if it is a compiler
-    % generated predicate, or a predicate from builtin.m or private_builtin.m.
-    % If it is, then the compiler sets the termination property of the ProcIds
-    % accordingly.
-    %
-    % We assume that user-defined special predicates terminate. This assumption
-    % is checked later during the post_term_analysis pass.
-    %
-:- pred set_compiler_gen_terminates(module_info::in,
-    pred_id::in, pred_info::in, list(proc_id)::in,
-    proc_table::in, proc_table::out) is semidet.
-
-set_compiler_gen_terminates(ModuleInfo, PredId, PredInfo, ProcIds,
-        !ProcTable) :-
-    % XXX This code looks to be a near-identical copy of the predicate
-    % of the same name in term_constr_initial.m.
-    ( if
-        pred_info_is_builtin(PredInfo)
-    then
-        set_builtin_terminates(ProcIds, PredId, PredInfo, ModuleInfo,
-            !ProcTable)
-    else if
-        % Compiler-generated unify/compare/index predicates always terminate.
-        % The else part checks for that.
-        %
-        % The then part checks for something else: for the predicate being
-        % named "unify", "index" or "compare", and defined in a builtin module.
-        % In practice, this is an unnecessarily roundabout way to  assert that
-        % builtin.unify and builtin.compare always terminate.
-        %
-        % This assertion was correct when this code was written in 1997/8,
-        % but has not been true since 2005, when we added user-specified
-        % type-specific unify and compare predicates to the language.
-        % This is because the user-specified unify/compare predicates
-        % may not always terminate.
-        %
-        % We should therefore delete the test and the then part.
-        % XXX However, doing so leads to the failure of several test cases:
-        %   term/exception_analysis_test2
-        %   term/existential_error1
-        %   term/occur
-        %   term/overlap
-        %   term/pl7_6_2c
-        %   term/pl8_3_1a
-        %   term/subset
-        % Until the addition of a "terminates" pragma for compare_time_t_reps,
-        % it also caused the building of time.c in the stage 2 library to fail.
-        %
-        % The best solution for this problem is
-        %
-        % - delete the condition and then-part here;
-        % - add "terminates" pragmas for unify, compare (and
-        %   compare_representation) in library/builtin.m, but then
-        % - generate an error if any user-specified unify or compare predicate
-        %   cannot be proven to terminate.
-        ( if
-            ModuleName = pred_info_module(PredInfo),
-            Name = pred_info_name(PredInfo),
-            pred_info_get_orig_arity(PredInfo, PredFormArity),
-            PredFormArity = pred_form_arity(PredFormArityInt),
-            special_pred_name_arity(SpecPredId0, Name, _, PredFormArityInt),
-            any_mercury_builtin_module(ModuleName)
-        then
-            SpecialPredId = SpecPredId0
-        else
-            pred_info_get_origin(PredInfo, Origin),
-            Origin = origin_compiler(made_for_uci(SpecialPredId, _))
-        )
-    then
-        set_generated_terminates(ProcIds, SpecialPredId, !ProcTable)
-    else
-        fail
-    ).
-
-:- pred set_generated_terminates(list(proc_id)::in, special_pred_id::in,
-    proc_table::in, proc_table::out) is det.
-
-set_generated_terminates([], _, !ProcTable).
-set_generated_terminates([ProcId | ProcIds], SpecialPredId, !ProcTable) :-
-    map.lookup(!.ProcTable, ProcId, ProcInfo0),
-    proc_info_get_headvars(ProcInfo0, HeadVars),
-    special_pred_id_to_termination(SpecialPredId, HeadVars,
-        ArgSize, Termination),
-    proc_info_set_maybe_arg_size_info(yes(ArgSize), ProcInfo0, ProcInfo1),
-    proc_info_set_maybe_termination_info(yes(Termination),
-        ProcInfo1, ProcInfo),
-    map.det_update(ProcId, ProcInfo, !ProcTable),
-    set_generated_terminates(ProcIds, SpecialPredId, !ProcTable).
-
-    % XXX The ArgSize argument for unify predicates may not be correct
-    % in the case where the type has user-defined equality.
-    %
-:- pred special_pred_id_to_termination(special_pred_id::in,
-    list(prog_var)::in, arg_size_info::out, termination_info::out) is det.
-
-special_pred_id_to_termination(SpecialPredId, HeadVars, ArgSize,
-        Termination) :-
-    (
-        SpecialPredId = spec_pred_compare,
-        term_util.make_bool_list(HeadVars, [no, no, no], OutList),
-        ArgSize = finite(0, OutList),
-        Termination = cannot_loop(unit)
-    ;
-        SpecialPredId = spec_pred_unify,
-        term_util.make_bool_list(HeadVars, [yes, yes], OutList),
-        ArgSize = finite(0, OutList),
-        Termination = cannot_loop(unit)
-    ;
-        SpecialPredId = spec_pred_index,
-        term_util.make_bool_list(HeadVars, [no, no], OutList),
-        ArgSize = finite(0, OutList),
-        Termination = cannot_loop(unit)
-    ).
-
-    % The list of proc_ids must refer to builtin predicates. This predicate
-    % sets the termination information of builtin predicates.
-    %
-:- pred set_builtin_terminates(list(proc_id)::in, pred_id::in, pred_info::in,
-    module_info::in, proc_table::in, proc_table::out) is det.
-
-set_builtin_terminates([], _, _, _, !ProcTable).
-set_builtin_terminates([ProcId | ProcIds], PredId, PredInfo, ModuleInfo,
-        !ProcTable) :-
-    map.lookup(!.ProcTable, ProcId, ProcInfo0),
-    ( if all_args_input_or_zero_size(ModuleInfo, PredInfo, ProcInfo0) then
-        % The size of the output arguments will all be 0, independent of the
-        % size of the input variables.
-        % UsedArgs should be set to yes([no, no, ...]).
-        proc_info_get_headvars(ProcInfo0, HeadVars),
-        term_util.make_bool_list(HeadVars, [], UsedArgs),
-        ArgSizeInfo = yes(finite(0, UsedArgs))
-    else
-        pred_info_get_context(PredInfo, Context),
-        Error = is_builtin(PredId),
-        ArgSizeError = term_error(Context, Error),
-        ArgSizeInfo = yes(infinite([ArgSizeError]))
-    ),
-    % XXX intermod
-    proc_info_set_maybe_arg_size_info(ArgSizeInfo, ProcInfo0, ProcInfo1),
-    proc_info_set_maybe_termination_info(yes(cannot_loop(unit)),
-        ProcInfo1, ProcInfo),
-    map.det_update(ProcId, ProcInfo, !ProcTable),
-    set_builtin_terminates(ProcIds, PredId, PredInfo, ModuleInfo, !ProcTable).
-
-%---------------------------------------------------------------------------%
-
-    % This predicate sets the arg_size_info property of the given list of
-    % procedures.
-    %
-    % change_procs_arg_size_info(ProcList, Override, TerminationInfo,
-    %       ProcTable, ProcTable)
-    %
-    % If Override is yes, then this predicate overrides any existing arg_size
-    % information. If Override is no, then it leaves the proc_info of a
-    % procedure unchanged unless the proc_info had no arg_size information
-    % (i.e. the maybe(arg_size_info) field was set to "no").
-    %
-:- pred change_procs_arg_size_info(list(proc_id)::in, bool::in,
-    arg_size_info::in, proc_table::in, proc_table::out) is det.
-
-change_procs_arg_size_info([], _, _, !ProcTable).
-change_procs_arg_size_info([ProcId | ProcIds], Override, ArgSize,
-        !ProcTable) :-
-    map.lookup(!.ProcTable, ProcId, ProcInfo0),
-    ( if
-        ( Override = yes
-        ; proc_info_get_maybe_arg_size_info(ProcInfo0, no)
-        )
-    then
-        proc_info_set_maybe_arg_size_info(yes(ArgSize), ProcInfo0, ProcInfo),
-        map.det_update(ProcId, ProcInfo, !ProcTable)
-    else
-        true
-    ),
-    change_procs_arg_size_info(ProcIds, Override, ArgSize, !ProcTable).
-
-    % change_procs_termination_info(ProcList, Override, TerminationInfo,
-    %     !ProcTable):
-    %
-    % This predicate sets the termination_info property of the given list of
-    % procedures.
-    %
-    % If Override is yes, then this predicate overrides any existing
-    % termination information. If Override is no, then it leaves the proc_info
-    % of a procedure unchanged unless the proc_info had no termination
-    % information (i.e. the maybe(termination_info) field was set to "no").
-    %
-:- pred change_procs_termination_info(list(proc_id)::in, bool::in,
-    termination_info::in, proc_table::in, proc_table::out) is det.
-
-change_procs_termination_info([], _, _, !ProcTable).
-change_procs_termination_info([ProcId | ProcIds], Override, Termination,
-        !ProcTable) :-
-    map.lookup(!.ProcTable, ProcId, ProcInfo0),
-    ( if
-        (
-            Override = yes
-        ;
-            proc_info_get_maybe_termination_info(ProcInfo0, no)
-        )
-    then
-        % XXX intermod
-        proc_info_set_maybe_termination_info(yes(Termination),
-            ProcInfo0, ProcInfo),
-        map.det_update(ProcId, ProcInfo, !ProcTable)
-    else
-        true
-    ),
-    change_procs_termination_info(ProcIds, Override, Termination, !ProcTable).
-
-%---------------------------------------------------------------------------%
-:- end_module transform_hlds.termination.
-%---------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+:- end_module termination.
+%-----------------------------------------------------------------------------%
diff --git a/compiler/transform_hlds.m b/compiler/transform_hlds.m
index df338b122..f3407ef7a 100644
--- a/compiler/transform_hlds.m
+++ b/compiler/transform_hlds.m
@@ -32,15 +32,6 @@
 
 :- include_module closure_analysis.
 
-% The first termination analysis system.
-:- include_module termination.
-    :- include_module term_util.
-
-% The second termination analysis system.
-:- include_module term_constr_main.
-    :- include_module term_constr_main_types.
-    :- include_module term_constr_util.
-
 :- include_module exception_analysis.
 :- include_module trailing_analysis.
 :- include_module tabling_analysis.
@@ -97,22 +88,6 @@
     :- include_module intermod_order_pred_info.
     :- include_module intermod_status.
 
-% The first termination analysis system.
-    :- include_module post_term_analysis.
-    :- include_module term_pass1.
-    :- include_module term_pass2.
-    :- include_module term_traversal.
-    :- include_module term_errors.
-    :- include_module term_norm.
-
-% The second termination analysis system.
-    :- include_module term_constr_initial.
-    :- include_module term_constr_build.        % pass 1
-    :- include_module term_constr_fixpoint.     % pass 1
-    :- include_module term_constr_pass2.        % pass 2
-    :- include_module term_constr_data.
-    :- include_module term_constr_errors.
-
 % Deforestation, also called partial deduction (hence the "pd" prefix").
     :- include_module constraint.
     :- include_module pd_debug.