Termination Analysis 2.2
Christopher Rodd SPEIRS
crs at students.cs.mu.oz.au
Mon Oct 6 02:21:37 AEST 1997
Here is part 2.2 - enjoy.
Index: compiler/globals.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/globals.m,v
retrieving revision 1.22
diff -u -r1.22 globals.m
--- 1.22 1997/07/27 15:00:22
+++ globals.m 1997/08/30 05:56:31
@@ -45,6 +45,12 @@
; nu
; sicstus.
+:- type termination_norm
+ ---> simple
+ ; total
+ ; num_data_elems
+ ; size_data_elems.
+
:- pred convert_gc_method(string::in, gc_method::out) is semidet.
:- pred convert_tags_method(string::in, tags_method::out) is semidet.
@@ -55,13 +61,15 @@
:- pred convert_prolog_dialect(string::in, prolog_dialect::out) is semidet.
+:- pred convert_termination_norm(string::in, termination_norm::out) is semidet.
+
%-----------------------------------------------------------------------------%
% Access predicates for the `globals' structure.
:- pred globals__init(option_table::di, gc_method::di, tags_method::di,
- args_method::di, type_info_method::di, prolog_dialect::di, globals::uo)
- is det.
+ args_method::di, type_info_method::di, prolog_dialect::di,
+ termination_norm::di, globals::uo) is det.
:- pred globals__get_options(globals::in, option_table::out) is det.
:- pred globals__get_gc_method(globals::in, gc_method::out) is det.
@@ -70,6 +78,8 @@
:- pred globals__get_type_info_method(globals::in, type_info_method::out)
is det.
:- pred globals__get_prolog_dialect(globals::in, prolog_dialect::out) is det.
+:- pred globals__get_termination_norm(globals::in, termination_norm::out)
+ is det.
:- pred globals__set_options(globals::in, option_table::in, globals::out)
is det.
@@ -83,6 +93,8 @@
globals::out) is det.
:- pred globals__set_prolog_dialect(globals::in, prolog_dialect::in,
globals::out) is det.
+:- pred globals__set_termination_norm(globals::in, termination_norm::in,
+ globals::out) is det.
:- pred globals__lookup_option(globals::in, option::in, option_data::out)
is det.
@@ -112,7 +124,7 @@
:- pred globals__io_init(option_table::di, gc_method::in, tags_method::in,
args_method::in, type_info_method::in, prolog_dialect::in,
- io__state::di, io__state::uo) is det.
+ termination_norm::in, io__state::di, io__state::uo) is det.
:- pred globals__io_get_gc_method(gc_method::out,
io__state::di, io__state::uo) is det.
@@ -129,6 +141,9 @@
:- pred globals__io_get_prolog_dialect(prolog_dialect::out,
io__state::di, io__state::uo) is det.
+:- pred globals__io_get_termination_norm(termination_norm::out,
+ io__state::di, io__state::uo) is det.
+
:- pred globals__io_get_globals(globals::out, io__state::di, io__state::uo)
is det.
@@ -192,6 +207,11 @@
convert_prolog_dialect("Sicstus-Prolog", sicstus).
convert_prolog_dialect("SICStus-Prolog", sicstus).
+convert_termination_norm("simple", simple).
+convert_termination_norm("total", total).
+convert_termination_norm("num-data-elems", num_data_elems).
+convert_termination_norm("size-data-elems", size_data_elems).
+
%-----------------------------------------------------------------------------%
:- type globals
@@ -201,35 +221,40 @@
tags_method,
args_method,
type_info_method,
- prolog_dialect
+ prolog_dialect,
+ termination_norm
).
globals__init(Options, GC_Method, TagsMethod, ArgsMethod,
- TypeInfoMethod, PrologDialect,
+ TypeInfoMethod, PrologDialect, TerminationNorm,
globals(Options, GC_Method, TagsMethod, ArgsMethod,
- TypeInfoMethod, PrologDialect)).
+ TypeInfoMethod, PrologDialect, TerminationNorm)).
-globals__get_options(globals(Options, _, _, _, _, _), Options).
-globals__get_gc_method(globals(_, GC_Method, _, _, _, _), GC_Method).
-globals__get_tags_method(globals(_, _, TagsMethod, _, _, _), TagsMethod).
-globals__get_args_method(globals(_, _, _, ArgsMethod, _, _), ArgsMethod).
-globals__get_type_info_method(globals(_, _, _, _, TypeInfoMethod, _),
+globals__get_options(globals(Options, _, _, _, _, _, _), Options).
+globals__get_gc_method(globals(_, GC_Method, _, _, _, _, _), GC_Method).
+globals__get_tags_method(globals(_, _, TagsMethod, _, _, _, _), TagsMethod).
+globals__get_args_method(globals(_, _, _, ArgsMethod, _, _, _), ArgsMethod).
+globals__get_type_info_method(globals(_, _, _, _, TypeInfoMethod, _, _),
TypeInfoMethod).
-globals__get_prolog_dialect(globals(_, _, _, _, _, PrologDialect),
+globals__get_prolog_dialect(globals(_, _, _, _, _, PrologDialect, _),
PrologDialect).
+globals__get_termination_norm(globals(_, _, _, _, _, _, TerminationNorm),
+ TerminationNorm).
-globals__set_options(globals(_, B, C, D, E, F), Options,
- globals(Options, B, C, D, E, F)).
-globals__set_gc_method(globals(A, _, C, D, E, F), GC_Method,
- globals(A, GC_Method, C, D, E, F)).
-globals__set_tags_method(globals(A, B, _, D, E, F), TagsMethod,
- globals(A, B, TagsMethod, D, E, F)).
-globals__set_args_method(globals(A, B, C, _, E, F), ArgsMethod,
- globals(A, B, C, ArgsMethod, E, F)).
-globals__set_type_info_method(globals(A, B, C, D, _, F), TypeInfoMethod,
- globals(A, B, C, D, TypeInfoMethod, F)).
-globals__set_prolog_dialect(globals(A, B, C, D, E, _), PrologDialect,
- globals(A, B, C, D, E, PrologDialect)).
+globals__set_options(globals(_, B, C, D, E, F, G), Options,
+ globals(Options, B, C, D, E, F, G)).
+globals__set_gc_method(globals(A, _, C, D, E, F, G), GC_Method,
+ globals(A, GC_Method, C, D, E, F, G)).
+globals__set_tags_method(globals(A, B, _, D, E, F, G), TagsMethod,
+ globals(A, B, TagsMethod, D, E, F, G)).
+globals__set_args_method(globals(A, B, C, _, E, F, G), ArgsMethod,
+ globals(A, B, C, ArgsMethod, E, F, G)).
+globals__set_type_info_method(globals(A, B, C, D, _, F, G), TypeInfoMethod,
+ globals(A, B, C, D, TypeInfoMethod, F, G)).
+globals__set_prolog_dialect(globals(A, B, C, D, E, _, G), PrologDialect,
+ globals(A, B, C, D, E, PrologDialect, G)).
+globals__set_termination_norm(globals(A, B, C, D, E, F, _), TerminationNorm,
+ globals(A, B, C, D, E, F, TerminationNorm)).
globals__lookup_option(Globals, Option, OptionData) :-
globals__get_options(Globals, OptionTable),
@@ -288,14 +313,15 @@
%-----------------------------------------------------------------------------%
globals__io_init(Options, GC_Method, TagsMethod, ArgsMethod,
- TypeInfoMethod, PrologDialect) -->
+ TypeInfoMethod, PrologDialect, TerminationNorm) -->
{ copy(GC_Method, GC_Method1) },
{ copy(TagsMethod, TagsMethod1) },
{ copy(ArgsMethod, ArgsMethod1) },
{ copy(TypeInfoMethod, TypeInfoMethod1) },
{ copy(PrologDialect, PrologDialect1) },
+ { copy(TerminationNorm, TerminationNorm1) },
{ globals__init(Options, GC_Method1, TagsMethod1, ArgsMethod1,
- TypeInfoMethod1, PrologDialect1, Globals) },
+ TypeInfoMethod1, PrologDialect1, TerminationNorm1, Globals) },
globals__io_set_globals(Globals).
globals__io_get_gc_method(GC_Method) -->
@@ -318,6 +344,10 @@
globals__io_get_globals(Globals),
{ globals__get_prolog_dialect(Globals, PrologDIalect) }.
+globals__io_get_termination_norm(TerminationNorm) -->
+ globals__io_get_globals(Globals),
+ { globals__get_termination_norm(Globals, TerminationNorm) }.
+
globals__io_get_globals(Globals) -->
io__get_globals(UnivGlobals),
{
Index: compiler/handle_options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/handle_options.m,v
retrieving revision 1.30
diff -u -r1.30 handle_options.m
--- 1.30 1997/10/03 04:55:36
+++ handle_options.m 1997/10/04 09:14:40
@@ -58,6 +58,8 @@
MakeShortInterface),
globals__io_lookup_bool_option(make_optimization_interface,
MakeOptimizationInt),
+ globals__io_lookup_bool_option(make_transitive_opt_interface,
+ MakeTransOptInt),
globals__io_lookup_bool_option(convert_to_mercury,
ConvertToMercury),
globals__io_lookup_bool_option(convert_to_goedel,
@@ -66,7 +68,7 @@
globals__io_lookup_bool_option(errorcheck_only, ErrorcheckOnly),
globals__io_lookup_bool_option(compile_to_c, CompileToC),
globals__io_lookup_bool_option(compile_only, CompileOnly),
- { bool__or_list([GenerateDependencies,
+ { bool__or_list([GenerateDependencies, MakeTransOptInt,
MakeInterface, MakeShortInterface, MakeOptimizationInt,
ConvertToMercury, ConvertToGoedel, TypecheckOnly,
ErrorcheckOnly, CompileToC, CompileOnly], NotLink) },
@@ -137,10 +139,21 @@
{ Percent >= 1 },
{ Percent =< 100 }
->
- postprocess_options_2(OptionTable,
- GC_Method, TagsMethod, ArgsMethod,
- TypeInfoMethod, PrologDialect),
- { Error = no }
+ { map__lookup(OptionTable,
+ termination_norm, TermNorm0) },
+ (
+ { TermNorm0 = string(TermNormStr) },
+ { convert_termination_norm(
+ TermNormStr, TermNorm) }
+ ->
+ postprocess_options_2(OptionTable,
+ GC_Method, TagsMethod, ArgsMethod,
+ TypeInfoMethod, PrologDialect,
+ TermNorm),
+ { Error = no }
+ ;
+ { Error = yes("Invalid argument to option `--termination-norm'\n\t(must be `simple', `total' or `num-data-elems').") }
+ )
;
{ Error = yes("Invalid argument to option `--fact-table-hash-percent-full'\n (must be an integer between 1 and 100)") }
)
@@ -163,12 +176,13 @@
{ Error = yes("Invalid grade option") }
).
-:- pred postprocess_options_2(option_table, gc_method, tags_method, args_method,
- type_info_method, prolog_dialect, io__state, io__state).
-:- mode postprocess_options_2(in, in, in, in, in, in, di, uo) is det.
+:- pred postprocess_options_2(option_table, gc_method, tags_method,
+ args_method, type_info_method, prolog_dialect, termination_norm,
+ io__state, io__state).
+:- mode postprocess_options_2(in, in, in, in, in, in, in, di, uo) is det.
postprocess_options_2(OptionTable, GC_Method, TagsMethod, ArgsMethod,
- TypeInfoMethod, PrologDialect) -->
+ TypeInfoMethod, PrologDialect, TermNorm) -->
% work around for NU-Prolog problems
( { map__search(OptionTable, heap_space, int(HeapSpace)) }
->
@@ -179,16 +193,14 @@
{ copy(OptionTable, OptionTable1) }, % XXX
globals__io_init(OptionTable1, GC_Method, TagsMethod, ArgsMethod,
- TypeInfoMethod, PrologDialect),
+ TypeInfoMethod, PrologDialect, TermNorm),
% --gc conservative implies --no-reclaim-heap-*
( { GC_Method = conservative } ->
globals__io_set_option(
- reclaim_heap_on_semidet_failure, bool(no)
- ),
+ reclaim_heap_on_semidet_failure, bool(no)),
globals__io_set_option(
- reclaim_heap_on_nondet_failure, bool(no)
- )
+ reclaim_heap_on_nondet_failure, bool(no))
;
[]
),
@@ -229,21 +241,16 @@
globals__io_set_option(num_tag_bits, int(NumTagBits)),
+ % --verbose-check-termination implies --check-termination
+ option_implies(verbose_check_termination, check_termination,bool(yes)),
+ % --check-termination implies --enable-termination
+ option_implies(check_termination, termination, bool(yes)),
+
% --split-c-files implies --procs-per-c-function 1
- globals__io_lookup_bool_option(split_c_files, Split_C_Files),
- ( { Split_C_Files = yes } ->
- globals__io_set_option(procs_per_c_function, int(1))
- ;
- []
- ),
+ option_implies(split_c_files, procs_per_c_function, int(1)),
% --very-verbose implies --verbose
- globals__io_lookup_bool_option(very_verbose, VeryVerbose),
- ( { VeryVerbose = yes } ->
- globals__io_set_option(verbose, bool(yes))
- ;
- []
- ),
+ option_implies(very_verbose, verbose, bool(yes)),
% -D all is really -D "abcdefghijklmnopqrstuvwxyz"
globals__io_lookup_string_option(verbose_dump_hlds, VerboseDump),
@@ -280,22 +287,14 @@
% --intermod-unused-args implies --intermodule-optimization and
% --optimize-unused-args.
- globals__io_lookup_bool_option(intermod_unused_args, Intermod),
- ( { Intermod = yes } ->
- globals__io_set_option(intermodule_optimization, bool(yes)),
- globals__io_set_option(optimize_unused_args, bool(yes))
- ;
- []
- ),
+ option_implies(intermod_unused_args, intermodule_optimization,
+ bool(yes)),
+ option_implies(intermod_unused_args, optimize_unused_args, bool(yes)),
% Don't do the unused_args optimization when making the
% optimization interface.
- globals__io_lookup_bool_option(make_optimization_interface, MakeOpt),
- ( { MakeOpt = yes } ->
- globals__io_set_option(optimize_unused_args, bool(no))
- ;
- []
- ),
+ option_implies(make_optimization_interface, optimize_unused_args,
+ bool(no)),
% If --use-search-directories-for-intermod is true, append the
% search directories to the list of directories to search for
@@ -313,12 +312,19 @@
;
[]
),
-
% --optimize-frames requires --optimize-labels and --optimize-jumps
- globals__io_lookup_bool_option(optimize_frames, OptFrames),
- ( { OptFrames = yes } ->
- globals__io_set_option(optimize_labels, bool(yes)),
- globals__io_set_option(optimize_jumps, bool(yes))
+ option_implies(optimize_frames, optimize_labels, bool(yes)),
+ option_implies(optimize_frames, optimize_jumps, bool(yes)).
+
+% option_implies(SourceBoolOption, ImpliedOption, ImpliedOptionValue, IO0, IO).
+% If the SourceBoolOption is set to yes, then the ImpliedOption is set
+% to ImpliedOptionValue.
+:- pred option_implies(option::in, option::in, option_data::in,
+ io__state::di, io__state::uo) is det.
+option_implies(SourceOption, ImpliedOption, ImpliedOptionValue) -->
+ globals__io_lookup_bool_option(SourceOption, SourceOptionValue),
+ ( { SourceOptionValue = yes } ->
+ globals__io_set_option(ImpliedOption, ImpliedOptionValue)
;
[]
).
Index: compiler/hlds_goal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_goal.m,v
retrieving revision 1.40
diff -u -r1.40 hlds_goal.m
--- 1.40 1997/09/01 14:01:56
+++ hlds_goal.m 1997/10/02 01:20:56
@@ -84,6 +84,10 @@
unify_rhs, % whatever is on the right hand side
% of the unification
unify_mode, % the mode of the unification
+ % (this field might not make a lot
+ % of sense for higher-order
+ % unifications, because polymorphism.m
+ % does not update it properly)
unification, % this field says what category of
% unification it is, and contains
% information specific to each category
@@ -252,6 +256,10 @@
% expression, this is the list of
% modes of the non-local variables
% of the lambda expression.
+ % (this field might not make a lot
+ % of sense for higher-order
+ % unifications, because polymorphism.m
+ % does not update it properly)
)
% A deconstruction unification is a unification with a functor
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.172
diff -u -r1.172 hlds_out.m
--- 1.172 1997/09/01 14:02:10
+++ hlds_out.m 1997/10/02 01:21:02
@@ -47,6 +47,13 @@
:- pred hlds_out__cons_id_to_string(cons_id, string).
:- mode hlds_out__cons_id_to_string(in, out) is det.
+ % hlds_out__write_pred_id/4 writes out a message such as
+ % predicate `foo:bar/3'
+ % or function `foo:myfoo/5'
+ % unless the predicate name begins with a double underscore "__",
+ % in which case mercury_output_term is used to print out the
+ % predicate's (or function's) name.
+
:- pred hlds_out__write_pred_id(module_info, pred_id, io__state, io__state).
:- mode hlds_out__write_pred_id(in, in, di, uo) is det.
@@ -170,6 +177,8 @@
:- import_module bool, int, string, list, set, map, std_util, assoc_list.
:- import_module term, term_io, varset, require, getopt.
+:- import_module termination, term_errors.
+
hlds_out__write_type_id(Name - Arity) -->
prog_out__write_sym_name(Name),
@@ -504,6 +513,9 @@
hlds_out__marker_name(magic, "magic").
hlds_out__marker_name(obsolete, "obsolete").
hlds_out__marker_name(memo, "memo").
+hlds_out__marker_name(terminates, "terminates").
+hlds_out__marker_name(check_termination, "check_termination").
+hlds_out__marker_name(does_not_terminate, "does_not_terminate").
hlds_out__write_marker(Marker) -->
{ hlds_out__marker_name(Marker, Name) },
@@ -1848,6 +1860,7 @@
{ proc_info_argmodes(Proc, HeadModes) },
{ proc_info_goal(Proc, Goal) },
{ proc_info_context(Proc, ModeContext) },
+ { proc_info_termination(Proc, Termination) },
{ proc_info_typeinfo_varmap(Proc, TypeInfoMap) },
{ Indent1 is Indent + 1 },
@@ -1860,6 +1873,21 @@
io__write_string(" ("),
hlds_out__write_determinism(InferredDeterminism),
io__write_string("):\n"),
+ hlds_out__write_indent(Indent),
+
+
+ globals__io_lookup_string_option(verbose_dump_hlds, Verbose),
+ ( { string__contains_char(Verbose, 't') } ->
+ io__write_string("% Inferred termination: "),
+ termination__out(Termination),
+ io__nl,
+ io__write_string("% Termination - used args: "),
+ termination__out_used_args(Termination),
+ io__nl,
+ term_errors__output_hlds(PredId, ProcId, ModuleInfo)
+ ;
+ []
+ ),
hlds_out__write_var_types(Indent, VarSet, AppendVarnums,
VarTypes, TVarSet),
Index: compiler/hlds_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
retrieving revision 1.35
diff -u -r1.35 hlds_pred.m
--- 1.35 1997/07/27 15:00:33
+++ hlds_pred.m 1997/10/04 08:24:29
@@ -15,6 +15,7 @@
:- import_module hlds_data, hlds_goal, hlds_module, llds, prog_data, instmap.
:- import_module bool, list, map, std_util, term, varset.
+:- import_module term_util.
:- implementation.
@@ -209,10 +210,37 @@
; magic % Requests that this predicate be transformed
% using the magic set transformation
% Used for pragma(memo).
- ; memo. % Requests that this predicate be evaluated
+ ; memo % Requests that this predicate be evaluated
% using memoing.
% Used for pragma(memo).
+ % The terminates and does_not_terminate
+ % pragmas are kept as markers to ensure
+ % that conflicting declarations are not
+ % made by the user. Otherwise, the
+ % information could be added to the
+ % ProcInfos directly.
+ ; terminates % The user guarantees that this predicate
+ % will terminate for all (finite?) input
+ % The `done' status could be meaningful,
+ % but it is currently not used.
+ ; does_not_terminate
+ % States that this predicate does not
+ % terminate. This is useful for pragma c
+ % code, which the compiler assumes to be
+ % terminating.
+ % The `done' status could be meaningful,
+ % but it is currently not used.
+ ; check_termination
+ % The user requires the compiler to guarantee
+ % the termination of this predicate.
+ % If the compiler cannot guarantee termination
+ % then it must give an error message.
+ % The `done' status could be meaningful,
+ % but it is currently not used.
+ .
+
+
:- type marker_status
---> request(marker)
; done(marker).
@@ -576,9 +604,9 @@
:- pred proc_info_set(maybe(determinism), varset, map(var, type), list(var),
list(mode), maybe(list(is_live)), hlds_goal, term__context,
stack_slots, determinism, bool, list(arg_info), liveness_info,
- map(tvar, var), proc_info).
+ map(tvar, var), termination, proc_info).
:- mode proc_info_set(in, in, in, in, in, in, in, in, in, in, in, in, in, in,
- out) is det.
+ in, out) is det.
:- pred proc_info_create(varset, map(var, type), list(var), list(mode),
determinism, hlds_goal, term__context, map(tvar, var), proc_info).
@@ -679,6 +707,12 @@
:- pred proc_info_set_stack_slots(proc_info, stack_slots, proc_info).
:- mode proc_info_set_stack_slots(in, in, out) is det.
+:- pred proc_info_termination(proc_info, termination).
+:- mode proc_info_termination(in, out) is det.
+
+:- pred proc_info_set_termination(proc_info, termination, proc_info).
+:- mode proc_info_set_termination(in, in, out) is det.
+
:- pred proc_info_set_can_process(proc_info, bool, proc_info).
:- mode proc_info_set_can_process(in, in, out) is det.
@@ -727,7 +761,7 @@
% (or the context of the first clause,
% if there was no mode declaration).
stack_slots, % stack allocations
- determinism, % _inferred_ det'ism
+ determinism, % _inferred_ determinism
bool, % no if we must not process this
% procedure yet (used to delay
% mode checking etc. for complicated
@@ -743,8 +777,11 @@
% for code generation
map(tvar, var), % typeinfo vars for
% type parameters
+ termination, % The termination properties of the
+ % procedure. Initially 'not_set'.
+ % Final value inferred by termination.m
maybe(list(mode))
- % declared modes of args
+ % declared modes of arguments.
).
@@ -769,35 +806,37 @@
ClauseBody = conj([]) - GoalInfo,
CanProcess = yes,
map__init(TVarsMap),
+ term_util__init(Termination),
NewProc = procedure(
MaybeDet, BodyVarSet, BodyTypes, HeadVars, Modes, MaybeArgLives,
ClauseBody, MContext, StackSlots, InferredDet, CanProcess,
- ArgInfo, InitialLiveness, TVarsMap, DeclaredModes
+ ArgInfo, InitialLiveness, TVarsMap, Termination, DeclaredModes
).
proc_info_set(DeclaredDetism, BodyVarSet, BodyTypes, HeadVars, HeadModes,
HeadLives, Goal,
Context, StackSlots, InferredDetism, CanProcess,
- ArgInfo, Liveness, TVarMap, ProcInfo) :-
+ ArgInfo, Liveness, TVarMap, Termination, ProcInfo) :-
ProcInfo = procedure(
DeclaredDetism, BodyVarSet, BodyTypes, HeadVars, HeadModes,
HeadLives, Goal, Context, StackSlots, InferredDetism,
- CanProcess, ArgInfo, Liveness, TVarMap, no).
+ CanProcess, ArgInfo, Liveness, TVarMap, Termination, no).
proc_info_create(VarSet, VarTypes, HeadVars, HeadModes, Detism, Goal,
Context, TVarMap, ProcInfo) :-
map__init(StackSlots),
set__init(Liveness),
+ term_util__init(Termination),
MaybeHeadLives = no,
ProcInfo = procedure(yes(Detism), VarSet, VarTypes, HeadVars, HeadModes,
MaybeHeadLives, Goal, Context, StackSlots, Detism, yes, [],
- Liveness, TVarMap, no).
+ Liveness, TVarMap, Termination, no).
proc_info_set_body(ProcInfo0, VarSet, VarTypes, HeadVars, Goal, ProcInfo) :-
ProcInfo0 = procedure(A, _, _, _, E, F, _,
- H, I, J, K, L, M, N, O),
+ H, I, J, K, L, M, N, O, P),
ProcInfo = procedure(A, VarSet, VarTypes, HeadVars, E, F, Goal,
- H, I, J, K, L, M, N, O).
+ H, I, J, K, L, M, N, O, P).
proc_info_interface_determinism(ProcInfo, Determinism) :-
proc_info_declared_determinism(ProcInfo, MaybeDeterminism),
@@ -846,46 +885,46 @@
instmap__from_assoc_list(InstAL, InstMap).
proc_info_declared_determinism(ProcInfo, Detism) :-
- ProcInfo = procedure(Detism, _, _, _, _, _, _, _, _, _, _, _, _, _, _).
+ ProcInfo = procedure(Detism, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _).
proc_info_variables(ProcInfo, VarSet) :-
- ProcInfo = procedure(_, VarSet, _, _, _, _, _, _, _, _, _, _, _, _, _).
+ ProcInfo = procedure(_, VarSet, _, _, _, _, _, _, _, _, _, _, _, _, _, _).
proc_info_vartypes(ProcInfo, VarTypes) :-
- ProcInfo = procedure(_, _, VarTypes, _, _, _, _, _,
- _, _, _, _, _, _, _).
+ ProcInfo = procedure(_, _, VarTypes, _, _, _, _, _,
+ _, _, _, _, _, _, _, _).
proc_info_headvars(ProcInfo, HeadVars) :-
- ProcInfo = procedure(_, _, _, HeadVars, _, _, _, _, _,
- _, _, _, _, _, _).
+ ProcInfo = procedure(_, _, _, HeadVars, _, _, _, _,
+ _, _, _, _, _, _, _, _).
proc_info_argmodes(ProcInfo, Modes) :-
- ProcInfo = procedure(_, _, _, _, Modes, _, _, _, _, _, _, _, _, _, _).
+ ProcInfo = procedure(_, _, _, _, Modes, _, _, _, _, _, _, _, _, _, _, _).
proc_info_maybe_arglives(ProcInfo, ArgLives) :-
- ProcInfo = procedure(_, _, _, _, _, ArgLives, _, _, _,
- _, _, _, _, _, _).
+ ProcInfo = procedure(_, _, _, _, _, ArgLives,
+ _, _, _, _, _, _, _, _, _, _).
proc_info_goal(ProcInfo, Goal) :-
- ProcInfo = procedure(_, _, _, _, _, _, Goal, _, _, _, _, _, _, _, _).
+ ProcInfo = procedure(_, _, _, _, _, _, Goal, _, _, _, _, _, _, _, _, _).
proc_info_context(ProcInfo, Context) :-
- ProcInfo = procedure(_, _, _, _, _, _, _, Context,
- _, _, _, _, _, _, _).
+ ProcInfo = procedure(_, _, _, _, _, _, _, Context, _, _, _, _, _, _, _, _).
proc_info_stack_slots(ProcInfo, StackSlots) :-
- ProcInfo = procedure(_, _, _, _, _, _, _, _, StackSlots,
- _, _, _, _, _, _).
+ ProcInfo = procedure(_, _, _, _, _, _, _, _, StackSlots,
+ _, _, _, _, _, _, _).
proc_info_inferred_determinism(ProcInfo, Detism) :-
- ProcInfo = procedure(_, _, _, _, _, _, _, _, _, Detism, _, _, _, _, _).
+ ProcInfo = procedure(_, _, _, _, _, _, _, _, _, Detism, _, _, _, _, _, _).
proc_info_can_process(ProcInfo, CanProcess) :-
- ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, CanProcess,
- _, _, _, _).
-proc_info_arg_info(ProcInfo, ArgInfo) :-
- ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, ArgInfo,
- _, _, _).
+ ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, CanProcess,
+ _, _, _, _, _).
+proc_info_arg_info(ProcInfo, ArgInfo) :-
+ ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, ArgInfo,
+ _, _, _, _).
proc_info_liveness_info(ProcInfo, Liveness) :-
- ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, Liveness,
- _, _).
+ ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, Liveness,
+ _, _, _).
proc_info_typeinfo_varmap(ProcInfo, TVarMap) :-
- ProcInfo = procedure(_, _, _, _, _, _, _,
- _, _, _, _, _, _, TVarMap, _).
-
+ ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, _, TVarMap, _, _).
+proc_info_termination(ProcInfo, Termination) :-
+ ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, _, _,
+ Termination, _).
proc_info_maybe_declared_argmodes(ProcInfo, MaybeArgModes) :-
- ProcInfo = procedure(_, _, _, _, _, _, _,
- _, _, _, _, _, _, _, MaybeArgModes).
+ ProcInfo = procedure(_, _, _, _, _, _, _,
+ _, _, _, _, _, _, _, _, MaybeArgModes).
proc_info_declared_argmodes(ProcInfo, ArgModes) :-
proc_info_maybe_declared_argmodes(ProcInfo, MaybeArgModes),
@@ -916,69 +955,72 @@
% M liveness_info % the initial liveness
% N map(tvar, var) % typeinfo vars to
% % vars.
-% O maybe(list(mode)) % declared modes
+% O termination % Termination analys
+% P maybe(list(mode)) % declared modes
% % of args
% ).
proc_info_set_varset(ProcInfo0, VarSet, ProcInfo) :-
- ProcInfo0 = procedure(A, _, C, D, E, F, G, H, I, J, K, L, M, N, O),
- ProcInfo = procedure(A, VarSet, C, D, E, F, G, H, I, J, K, L, M, N, O).
+ ProcInfo0 = procedure(A, _, C, D, E, F, G, H, I, J, K, L, M, N, O, P),
+ ProcInfo = procedure(A, VarSet, C, D, E, F, G, H, I, J, K, L, M, N, O, P).
proc_info_set_variables(ProcInfo0, Vars, ProcInfo) :-
- ProcInfo0 = procedure(A, _, C, D, E, F, G, H, I, J, K, L, M, N, O),
- ProcInfo = procedure(A, Vars, C, D, E, F, G, H, I, J, K, L, M, N, O).
+ ProcInfo0 = procedure(A, _, C, D, E, F, G, H, I, J, K, L, M, N, O, P),
+ ProcInfo = procedure(A, Vars, C, D, E, F, G, H, I, J, K, L, M, N, O, P).
proc_info_set_vartypes(ProcInfo0, Vars, ProcInfo) :-
- ProcInfo0 = procedure(A, B, _, D, E, F, G, H, I, J, K, L, M, N, O),
- ProcInfo = procedure(A, B, Vars, D, E, F, G, H, I, J, K, L, M, N, O).
+ ProcInfo0 = procedure(A, B, _, D, E, F, G, H, I, J, K, L, M, N, O, P),
+ ProcInfo = procedure(A, B, Vars, D, E, F, G, H, I, J, K, L, M, N, O, P).
-proc_info_set_headvars(ProcInfo0, HeadVars, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, _, E, F, G, H, I, J, K, L, M, N, O),
- ProcInfo = procedure(A, B, C, HeadVars, E, F, G, H,
- I, J, K, L, M, N, O).
+proc_info_set_headvars(ProcInfo0, HdVars, ProcInfo) :-
+ ProcInfo0 = procedure(A, B, C, _, E, F, G, H, I, J, K, L, M, N, O, P),
+ ProcInfo = procedure(A, B, C, HdVars, E, F, G, H, I, J, K, L, M, N, O, P).
proc_info_set_argmodes(ProcInfo0, ArgModes, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, _, F, G, H, I, J, K, L, M, N, O),
- ProcInfo = procedure(A, B, C, D, ArgModes, F, G, H, I,
- J, K, L, M, N, O).
+ ProcInfo0 = procedure(A, B, C, D, _, F, G, H, I, J, K, L, M, N, O, P),
+ ProcInfo = procedure(A, B, C, D, ArgModes, F, G, H, I,
+ J, K, L, M, N, O, P).
proc_info_set_maybe_arglives(ProcInfo0, ArgLives, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, _, G, H, I, J, K, L, M, N, O),
- ProcInfo = procedure(A, B, C, D, E, ArgLives, G, H, I, J,
- K, L, M, N, O).
+ ProcInfo0 = procedure(A, B, C, D, E, _, G, H, I, J, K, L, M, N, O, P),
+ ProcInfo = procedure(A, B, C, D, E, ArgLives, G, H, I,
+ J, K, L, M, N, O, P).
proc_info_set_inferred_determinism(ProcInfo0, Detism, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I, Detism, K, L, M, N, O).
+ ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P),
+ ProcInfo = procedure(A, B, C, D, E, F, G, H, I, Detism, K, L, M, N, O, P).
proc_info_set_can_process(ProcInfo0, CanProcess, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, _, L, M, N, O),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, CanProcess,
- L, M, N, O).
+ ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, _, L, M, N, O, P),
+ ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, CanProcess,
+ L, M, N, O, P).
proc_info_set_goal(ProcInfo0, Goal, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, _, H, I, J, K, L, M, N, O),
- ProcInfo = procedure(A, B, C, D, E, F, Goal, H, I, J, K, L, M, N, O).
+ ProcInfo0 = procedure(A, B, C, D, E, F, _, H, I, J, K, L, M, N, O, P),
+ ProcInfo = procedure(A, B, C, D, E, F, Goal, H, I, J, K, L, M, N, O, P).
proc_info_set_stack_slots(ProcInfo0, StackSlots, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, _, J, K, L, M, N, O),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, StackSlots,
- J, K, L, M, N, O).
+ ProcInfo0 = procedure(A, B, C, D, E, F, G, H, _, J, K, L, M, N, O, P),
+ ProcInfo = procedure(A, B, C, D, E, F, G, H, StackSlots, J, K,
+ L, M, N, O, P).
proc_info_set_arg_info(ProcInfo0, ArgInfo, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, _, M, N, O),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, ArgInfo,
- M, N, O).
+ ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, _, M, N, O, P),
+ ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, ArgInfo, M, N, O, P).
proc_info_set_liveness_info(ProcInfo0, Liveness, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, _, N, O),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L, Liveness,
- N, O).
+ ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, _, N, O, P),
+ ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L, Liveness,
+ N, O, P).
proc_info_set_typeinfo_varmap(ProcInfo0, TVarMap, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, _, O),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I,
- J, K, L, M, TVarMap, O).
+ ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, _, O, P),
+ ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, TVarMap, O, P).
+
+proc_info_set_termination(ProcInfo0, Terminat, ProcInfo) :-
+ ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, _, P),
+ ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L,
+ M, N, Terminat, P).
proc_info_get_typeinfo_vars_setwise(ProcInfo, Vars, TypeInfoVars) :-
set__to_sorted_list(Vars, VarList),
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.240
diff -u -r1.240 make_hlds.m
--- 1.240 1997/09/30 14:54:24
+++ make_hlds.m 1997/10/04 08:27:29
@@ -61,7 +61,7 @@
:- import_module make_tags, quantification, (inst).
:- import_module code_util, unify_proc, special_pred, type_util, mode_util.
:- import_module mercury_to_mercury, passes_aux, clause_to_proc, inst_match.
-:- import_module fact_table.
+:- import_module fact_table, term_util.
:- import_module string, char, int, set, bintree, list, map, require.
:- import_module bool, getopt, assoc_list, term, term_io, varset.
@@ -325,8 +325,8 @@
{ pred_info_procedures(PredInfo, Procs) },
{ map__to_assoc_list(Procs, ExistingProcs) },
(
- { get_matching_procedure(ExistingProcs, Modes,
- Module0, ProcId) }
+ { get_procedure_matching_declmodes(
+ ExistingProcs, Modes, Module0, ProcId)}
->
{ module_info_get_pragma_exported_procs(Module0,
PragmaExportedProcs0) },
@@ -354,7 +354,8 @@
{ Status = item_status(ImportStatus, _) },
( { ImportStatus \= opt_imported } ->
prog_out__write_context(Context),
- io__write_string("Error: unknown pragma unused_args.\n"),
+ io__write_string(
+ "Error: unknown pragma unused_args.\n"),
{ module_info_incr_errors(Module0, Module) }
;
{ module_info_get_predicate_table(Module0, Preds) },
@@ -380,6 +381,84 @@
% clauses).
{ Pragma = fact_table(_, _, _) },
{ Module = Module0 }
+ ;
+ { Pragma = termination_info(PredOrFunc, SymName, ModeList,
+ Termination) },
+ { module_info_get_predicate_table(Module0, Preds) },
+ { list__length(ModeList, Arity) },
+ (
+ { predicate_table_search_pf_sym_arity(Preds,
+ PredOrFunc, SymName, Arity, PredIds) }
+ ->
+ ( { PredIds = [] } ->
+ prog_out__write_context(Context),
+ undefined_pred_or_func_error(SymName, Arity, Context,
+ ":- pragma termination_info declaration"),
+ { module_info_incr_errors(Module0, Module) }
+ ; { PredIds = [PredId] } ->
+ { module_info_preds(Module0, PredTable0) },
+ { map__lookup(PredTable0, PredId, PredInfo0) },
+ { pred_info_procedures(PredInfo0, ProcTable0)},
+ { map__to_assoc_list(ProcTable0, ProcList) },
+ (
+ { get_procedure_matching_declmodes(ProcList,
+ ModeList, Module0, ProcId) }
+ ->
+ { map__lookup(ProcTable0, ProcId, ProcInfo0) },
+ { proc_info_set_termination(ProcInfo0,
+ Termination, ProcInfo) },
+ { map__det_update(ProcTable0, ProcId, ProcInfo,
+ ProcTable) },
+ { pred_info_set_procedures(PredInfo0,
+ ProcTable, PredInfo) },
+ { map__det_update(PredTable0, PredId, PredInfo,
+ PredTable) },
+ { module_info_set_preds(Module0, PredTable,
+ Module) }
+ ;
+ { module_info_incr_errors(Module0, Module) },
+ prog_out__write_context(Context),
+ io__write_string(
+ "Error: `:- pragma termination_info' "),
+ io__write_string(
+ "declaration for undeclared mode of "),
+ hlds_out__write_call_id(PredOrFunc,
+ SymName/Arity),
+ io__write_string(".\n")
+ )
+ ;
+ prog_out__write_context(Context),
+ io__write_string("Error: Ambiguous predicate name"),
+ hlds_out__write_call_id(PredOrFunc, SymName/Arity),
+ io__nl,
+ prog_out__write_context(Context),
+ io__write_string(" in pragma termination_info\n"),
+ { module_info_incr_errors(Module0, Module) }
+ )
+ ;
+ prog_out__write_context(Context),
+ undefined_pred_or_func_error(SymName, Arity, Context,
+ ":- pragma termination_info declaration"),
+ { module_info_incr_errors(Module0, Module) }
+ )
+ ;
+ { Pragma = terminates(Name, Arity) },
+ add_pred_marker(Module0, "terminates", Name, Arity,
+ Context, [request(terminates)],
+ [request(check_termination),
+ request(does_not_terminate)], Module)
+ ;
+ { Pragma = does_not_terminate(Name, Arity) },
+ add_pred_marker(Module0, "does_not_terminate", Name, Arity,
+ Context, [request(does_not_terminate)],
+ [request(check_termination), request(terminates)],
+ Module)
+ ;
+ { Pragma = check_termination(Name, Arity) },
+ add_pred_marker(Module0, "check_termination", Name, Arity,
+ Context, [request(check_termination)],
+ [request(terminates), request(does_not_terminate)],
+ Module)
).
add_item_decl_pass_2(func(_VarSet, FuncName, TypesAndModes, _RetTypeAndMode,
@@ -551,7 +630,12 @@
add_pred_marker(Module0, PragmaName, Name, Arity, Context, Markers,
ConflictMarkers, Module) -->
{ module_info_get_predicate_table(Module0, PredTable0) },
+ % check that the pragma is module qualified.
(
+ { Name = unqualified(_) }
+ ->
+ { error("add_pred_marker: unqualified name") }
+ ; % else if
{ predicate_table_search_sym_arity(PredTable0, Name,
Arity, PredIds) }
->
@@ -1699,7 +1783,7 @@
{ map__to_assoc_list(Procs, ExistingProcs) },
{ pragma_get_modes(PVars, Modes) },
(
- { get_matching_procedure(ExistingProcs, Modes,
+ { get_procedure_matching_argmodes(ExistingProcs, Modes,
ModuleInfo0, ProcId) }
->
{ pred_info_clauses_info(PredInfo1, Clauses0) },
@@ -1822,23 +1906,39 @@
%---------------------------------------------------------------------------%
- % Find the procedure with modes which match the ones we want.
-
-:- pred get_matching_procedure(assoc_list(proc_id, proc_info), list(mode),
- module_info, proc_id).
-:- mode get_matching_procedure(in, in, in, out) is semidet.
+ % Find the procedure with argmodes which match the ones we want.
-get_matching_procedure([P|Procs], Modes, ModuleInfo, OurProcId) :-
+:- pred get_procedure_matching_argmodes(assoc_list(proc_id, proc_info),
+ list(mode), module_info, proc_id).
+:- mode get_procedure_matching_argmodes(in, in, in, out) is semidet.
+get_procedure_matching_argmodes([P|Procs], Modes, ModuleInfo, OurProcId) :-
P = ProcId - ProcInfo,
proc_info_argmodes(ProcInfo, ArgModes),
( mode_list_matches(Modes, ArgModes, ModuleInfo) ->
OurProcId = ProcId
;
- get_matching_procedure(Procs, Modes, ModuleInfo, OurProcId)
+ get_procedure_matching_argmodes(Procs, Modes, ModuleInfo,
+ OurProcId)
+ ).
+
+ % Find the procedure with declared argmodes which match the ones
+ % we want. If there was no mode declaration, then use the inferred
+ % argmodes.
+:- pred get_procedure_matching_declmodes(assoc_list(proc_id, proc_info),
+ list(mode), module_info, proc_id).
+:- mode get_procedure_matching_declmodes(in, in, in, out) is semidet.
+get_procedure_matching_declmodes([P|Procs], Modes, ModuleInfo, OurProcId) :-
+ P = ProcId - ProcInfo,
+ proc_info_declared_argmodes(ProcInfo, ArgModes),
+ ( mode_list_matches(Modes, ArgModes, ModuleInfo) ->
+ OurProcId = ProcId
+ ;
+ get_procedure_matching_declmodes(Procs, Modes, ModuleInfo,
+ OurProcId)
).
-:- pred mode_list_matches(list(mode)::in, list(mode)::in,
- module_info::in) is semidet.
+:- pred mode_list_matches(list(mode), list(mode), module_info).
+:- mode mode_list_matches(in, in, in) is semidet.
mode_list_matches([], [], _).
mode_list_matches([Mode1 | Modes1], [Mode2 | Modes2], ModuleInfo) :-
Index: compiler/mercury_compile.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_compile.m,v
retrieving revision 1.55
diff -u -r1.55 mercury_compile.m
--- 1.55 1997/10/03 04:55:41
+++ mercury_compile.m 1997/10/04 14:39:13
@@ -32,9 +32,9 @@
:- import_module handle_options, prog_io, modules, module_qual, equiv_type.
:- import_module make_hlds, typecheck, modes.
:- import_module switch_detection, cse_detection, det_analysis, unique_modes.
-:- import_module simplify, intermod, bytecode_gen, bytecode, (lambda).
-:- import_module polymorphism, intermod, higher_order, inlining, dnf.
-:- import_module constraint, unused_args, dead_proc_elim, saved_vars.
+:- import_module simplify, intermod, trans_opt, bytecode_gen, bytecode.
+:- import_module (lambda), polymorphism, termination, higher_order, inlining.
+:- import_module dnf, constraint, unused_args, dead_proc_elim, saved_vars.
:- import_module lco, liveness, stratify.
:- import_module follow_code, live_vars, arg_info, store_alloc.
:- import_module code_gen, optimize, export, base_type_info, base_type_layout.
@@ -46,7 +46,6 @@
:- import_module dependency_graph.
:- import_module options, globals, passes_aux.
-
%-----------------------------------------------------------------------------%
main -->
@@ -208,6 +207,8 @@
globals__io_lookup_bool_option(errorcheck_only, ErrorCheckOnly),
globals__io_lookup_bool_option(make_optimization_interface,
MakeOptInt),
+ globals__io_lookup_bool_option(make_transitive_opt_interface,
+ MakeTransOptInt),
( { TypeCheckOnly = yes } ->
[]
; { ErrorCheckOnly = yes } ->
@@ -218,6 +219,8 @@
; { MakeOptInt = yes } ->
% only run up to typechecking when making the .opt file
[]
+ ; { MakeTransOptInt = yes } ->
+ mercury_compile__output_trans_opt_file(HLDS21)
;
mercury_compile__maybe_output_prof_call_graph(HLDS21,
Verbose, Stats, HLDS25),
@@ -260,7 +263,7 @@
{ ModuleImports0 = module_imports(Module, LongDeps, ShortDeps, _, _) },
write_dependency_file(Module, LongDeps, ShortDeps, FactDeps), !,
- % Errors in .opt files result in software errors.
+ % Errors in .opt and .trans_opt files result in software errors.
mercury_compile__maybe_grab_optfiles(ModuleImports0, Verbose,
ModuleImports1, IntermodError), !,
@@ -318,15 +321,26 @@
globals__io_lookup_bool_option(intermodule_optimization, UseOptInt),
globals__io_lookup_bool_option(make_optimization_interface,
MakeOptInt),
+ globals__io_lookup_bool_option(transitive_optimization, TransOpt),
( { UseOptInt = yes, MakeOptInt = no } ->
maybe_write_string(Verbose, "% Reading .opt files...\n"),
maybe_flush_output(Verbose),
- intermod__grab_optfiles(Imports0, Imports, Error),
+ intermod__grab_optfiles(Imports0, Imports1, Error1),
maybe_write_string(Verbose, "% Done.\n")
;
- { Imports = Imports0 },
- { Error = no }
- ).
+ { Imports1 = Imports0 },
+ { Error1 = no }
+ ),
+ ( { TransOpt = yes } ->
+ maybe_write_string(Verbose, "% Reading .trans_opt files..\n"),
+ maybe_flush_output(Verbose),
+ trans_opt__grab_optfiles(Imports1, Imports, Error2),
+ maybe_write_string(Verbose, "% Done.\n")
+ ;
+ { Imports = Imports1 },
+ { Error2 = no }
+ ),
+ { bool__or(Error1, Error2, Error) }.
:- pred mercury_compile__expand_equiv_types(item_list, bool, bool, item_list,
bool, eqv_map, io__state, io__state).
@@ -453,6 +467,8 @@
globals__io_lookup_bool_option(intermod_unused_args, IntermodArgs),
globals__io_lookup_bool_option(verbose, Verbose),
globals__io_lookup_bool_option(statistics, Stats),
+ globals__io_lookup_bool_option(termination, Termination),
+
( { MakeOptInt = yes } ->
intermod__write_optfile(HLDS0, HLDS1),
@@ -460,14 +476,25 @@
% determinism analysis and polymorphism, then run unused_args
% to append the unused argument information to the `.opt.tmp'
% file written above.
- ( { IntermodArgs = yes } ->
+ ( { IntermodArgs = yes ; Termination = yes } ->
mercury_compile__frontend_pass_2_by_phases(
HLDS1, HLDS2, FoundModeError),
( { FoundModeError = no } ->
mercury_compile__maybe_polymorphism(HLDS2,
Verbose, Stats, HLDS3),
- mercury_compile__maybe_unused_args(HLDS3,
- Verbose, Stats, HLDS)
+ ( { IntermodArgs = yes } ->
+ mercury_compile__maybe_unused_args(
+ HLDS3, Verbose, Stats, HLDS4)
+ ;
+ { HLDS4 = HLDS3 }
+ ),
+ ( { Termination = yes } ->
+ mercury_compile__maybe_termination(
+ HLDS4, Verbose, Stats, HLDS)
+ ;
+ { HLDS = HLDS4 }
+ )
+
;
io__set_exit_status(1),
{ HLDS = HLDS2 }
@@ -483,6 +510,23 @@
{ HLDS = HLDS0 }
).
+
+:- pred mercury_compile__output_trans_opt_file(module_info,
+ io__state, io__state).
+:- mode mercury_compile__output_trans_opt_file(in, di, uo) is det.
+mercury_compile__output_trans_opt_file(HLDS25) -->
+ globals__io_lookup_bool_option(verbose, Verbose),
+ globals__io_lookup_bool_option(statistics, Stats),
+
+ mercury_compile__maybe_polymorphism(HLDS25, Verbose, Stats, HLDS26),
+ mercury_compile__maybe_dump_hlds(HLDS26, "26", "polymorphism"), !,
+
+ mercury_compile__maybe_termination(HLDS26, Verbose, Stats, HLDS28),
+ mercury_compile__maybe_dump_hlds(HLDS28, "28", "termination"), !,
+
+ trans_opt__write_optfile(HLDS28).
+
+
:- pred mercury_compile__frontend_pass_2(module_info, module_info,
bool, io__state, io__state).
% :- mode mercury_compile__frontend_pass_2(di, uo, out, di, uo) is det.
@@ -602,9 +646,12 @@
globals__io_lookup_bool_option(verbose, Verbose),
globals__io_lookup_bool_option(statistics, Stats),
- mercury_compile__maybe_polymorphism(HLDS25, Verbose, Stats, HLDS28), !,
- mercury_compile__maybe_dump_hlds(HLDS28, "28", "polymorphism"), !,
+ mercury_compile__maybe_polymorphism(HLDS25, Verbose, Stats, HLDS26),
+ mercury_compile__maybe_dump_hlds(HLDS26, "26", "polymorphism"), !,
+ mercury_compile__maybe_termination(HLDS26, Verbose, Stats, HLDS28),
+ mercury_compile__maybe_dump_hlds(HLDS28, "28", "termination"), !,
+
mercury_compile__maybe_base_type_infos(HLDS28, Verbose, Stats, HLDS29),
!,
mercury_compile__maybe_dump_hlds(HLDS29, "29", "base_type_infos"), !,
@@ -904,6 +951,26 @@
),
maybe_report_stats(Stats).
+:- pred mercury_compile__maybe_termination(module_info, bool, bool,
+ module_info, io__state, io__state).
+:- mode mercury_compile__maybe_termination(in, in, in, out, di, uo) is det.
+
+mercury_compile__maybe_termination(HLDS0, Verbose, Stats, HLDS) -->
+ globals__io_lookup_bool_option(polymorphism, Polymorphism),
+ globals__io_lookup_bool_option(termination, Termination),
+ % Termination analysis requires polymorphism to be run,
+ % as termination analysis does not handle complex unification
+ (
+ { Polymorphism = yes },
+ { Termination = yes }
+ ->
+ maybe_write_string(Verbose, "% Detecting termination...\n"),
+ termination__pass(HLDS0, HLDS),
+ maybe_report_stats(Stats)
+ ;
+ { HLDS = HLDS0 }
+ ).
+
:- pred mercury_compile__check_unique_modes(module_info, bool, bool,
module_info, bool, io__state, io__state).
:- mode mercury_compile__check_unique_modes(in, in, in, out, out, di, uo)
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.118
diff -u -r1.118 mercury_to_mercury.m
--- 1.118 1997/09/15 14:04:14
+++ mercury_to_mercury.m 1997/10/02 01:21:38
@@ -156,7 +156,7 @@
:- implementation.
:- import_module prog_out, prog_util, hlds_pred, hlds_out, instmap.
-:- import_module globals, options.
+:- import_module globals, options, termination.
:- import_module bool, int, string, set, term_io, lexer, std_util, require.
%-----------------------------------------------------------------------------%
@@ -303,6 +303,20 @@
;
{ Pragma = fact_table(Pred, Arity, FileName) },
mercury_output_pragma_fact_table(Pred, Arity, FileName)
+ ;
+ { Pragma = termination_info(PredOrFunc, PredName,
+ ModeList, Termination) },
+ termination__output_pragma_termination_info(PredOrFunc,
+ PredName, ModeList, Termination, Context)
+ ;
+ { Pragma = terminates(Pred, Arity) },
+ mercury_output_pragma_decl(Pred, Arity, "terminates")
+ ;
+ { Pragma = does_not_terminate(Pred, Arity) },
+ mercury_output_pragma_decl(Pred, Arity, "does_not_terminate")
+ ;
+ { Pragma = check_termination(Pred, Arity) },
+ mercury_output_pragma_decl(Pred, Arity, "check_termination")
).
mercury_output_item(nothing, _) --> [].
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.23
diff -u -r1.23 module_qual.m
--- 1.23 1997/09/14 09:24:29
+++ module_qual.m 1997/10/02 01:21:47
@@ -608,6 +608,15 @@
Info, Info) --> [].
qualify_pragma(fact_table(SymName, Arity, FileName),
fact_table(SymName, Arity, FileName), Info, Info) --> [].
+qualify_pragma(termination_info(PredOrFunc, SymName, ModeList0, Termination),
+ termination_info(PredOrFunc, SymName, ModeList, Termination),
+ Info0, Info) -->
+ qualify_mode_list(ModeList0, ModeList, Info0, Info).
+qualify_pragma(terminates(A, B), terminates(A, B), Info, Info) --> [].
+qualify_pragma(does_not_terminate(A, B), does_not_terminate(A, B),
+ Info, Info) --> [].
+qualify_pragma(check_termination(A, B), check_termination(A, B), Info,
+ Info) --> [].
:- pred qualify_pragma_vars(list(pragma_var)::in, list(pragma_var)::out,
mq_info::in, mq_info::out, io__state::di, io__state::uo) is det.
Index: compiler/modules.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modules.m,v
retrieving revision 1.40
diff -u -r1.40 modules.m
--- 1.40 1997/09/14 05:03:33
+++ modules.m 1997/10/02 01:21:49
@@ -248,11 +248,16 @@
report_warning("Warning: clause in module interface.\n"),
check_for_clauses_in_interface(Items0, Items)
;
- % `pragma obsolete' declarations are supposed to go
- % in the interface, but all other pragma declarations
- % should go in the implementation.
+ % pragma `obsolete', `terminates', `does_not_terminate'
+ % `termination_info' and `check_termination' declarations
+ % are supposed to go in the interface, but all other pragma
+ % declarations should go in the implementation.
{ Item0 = pragma(Pragma) },
- { Pragma \= obsolete(_, _) }
+ { Pragma \= obsolete(_, _) },
+ { Pragma \= terminates(_, _) },
+ { Pragma \= does_not_terminate(_, _) },
+ { Pragma \= check_termination(_, _) },
+ { Pragma \= termination_info(_, _, _, _) }
->
prog_out__write_context(Context),
report_warning("Warning: pragma in module interface.\n"),
Index: compiler/options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/options.m,v
retrieving revision 1.204
diff -u -r1.204 options.m
--- 1.204 1997/10/03 04:55:44
+++ options.m 1997/10/05 09:03:21
@@ -23,8 +23,20 @@
:- pred short_option(char::in, option::out) is semidet.
:- pred long_option(string::in, option::out) is semidet.
:- pred option_defaults(option::out, option_data::out) is nondet.
+
:- pred special_handler(option::in, special_data::in, option_table::in,
maybe_option_table::out) is semidet.
+% special_handler(Option, ValueForThatOption, OptionTableIn,
+% MaybeOptionTableOut).
+% This predicate is invoked whenever getopt finds an option
+% (long or short) designated as special, with special_data holding
+% the argument of the option (if any). The predicate can change the
+% option table in arbitrary ways in the course of handling the option,
+% or it can return an error message.
+% The canonical examples of special options are -O options in compilers,
+% which set many other options at once.
+% The MaybeOptionTableOut may either be ok(OptionTableOut), or it may
+% be error(ErrorString).
:- pred options_help(io__state::di, io__state::uo) is det.
@@ -60,6 +72,7 @@
; make_short_interface
; make_interface
; make_optimization_interface
+ ; make_transitive_opt_interface
; generate_dependencies
; convert_to_mercury
; convert_to_goedel
@@ -148,6 +161,7 @@
; opt_level
; opt_space % default is to optimize time
; intermodule_optimization
+ ; transitive_optimization
; split_c_files
% - HLDS
; inlining
@@ -171,6 +185,11 @@
; follow_code
; prev_code
; optimize_dead_procs
+ ; termination
+ ; check_termination
+ ; verbose_check_termination
+ ; termination_single_args
+ ; termination_norm
% - HLDS->LLDS
; smart_indexing
; dense_switch_req_density
@@ -281,6 +300,7 @@
make_short_interface - bool(no),
make_interface - bool(no),
make_optimization_interface - bool(no),
+ make_transitive_opt_interface - bool(no),
convert_to_mercury - bool(no),
convert_to_goedel - bool(no),
typecheck_only - bool(no),
@@ -389,6 +409,12 @@
opt_level - int_special,
opt_space - special,
intermodule_optimization - bool(no),
+ transitive_optimization - bool(no),
+ check_termination - bool(no),
+ verbose_check_termination - bool(no),
+ termination - bool(no),
+ termination_single_args - bool(no),
+ termination_norm - string("total"),
split_c_files - bool(no)
]).
option_defaults_2(optimization_option, [
@@ -554,6 +580,11 @@
long_option("make-optimisation-interface",
make_optimization_interface).
long_option("make-opt-int", make_optimization_interface).
+long_option("make-transitive-optimization-interface",
+ make_transitive_opt_interface).
+long_option("make-transitive-optimisation-interface",
+ make_transitive_opt_interface).
+long_option("make-trans-opt", make_transitive_opt_interface).
long_option("convert-to-mercury", convert_to_mercury).
long_option("convert-to-Mercury", convert_to_mercury).
long_option("pretty-print", convert_to_mercury).
@@ -649,6 +680,11 @@
long_option("optimise-space", opt_space).
long_option("intermodule-optimization", intermodule_optimization).
long_option("intermodule-optimisation", intermodule_optimization).
+long_option("transitive-intermodule-optimization",
+ transitive_optimization).
+long_option("transitive-intermodule-optimisation",
+ transitive_optimization).
+long_option("trans-intermod-opt", transitive_optimization).
% HLDS->HLDS optimizations
long_option("inlining", inlining).
@@ -680,6 +716,19 @@
long_option("optimize-constructor-last-call", optimize_constructor_last_call).
long_option("optimize-dead-procs", optimize_dead_procs).
long_option("optimise-dead-procs", optimize_dead_procs).
+long_option("enable-termination", termination).
+long_option("enable-term", termination).
+long_option("check-termination", check_termination).
+long_option("check-term", check_termination).
+long_option("chk-term", check_termination).
+long_option("verbose-check-termination",verbose_check_termination).
+long_option("verb-check-term", verbose_check_termination).
+long_option("verb-chk-term", verbose_check_termination).
+long_option("termination-single-argument-analysis",
+ termination_single_args).
+long_option("term-single-arg", termination_single_args).
+long_option("termination-norm", termination_norm).
+long_option("term-norm", termination_norm).
% HLDS->LLDS optimizations
long_option("smart-indexing", smart_indexing).
@@ -1084,6 +1133,10 @@
io__write_string("\t\tWrite inter-module optimization information to\n"),
io__write_string("\t\t`<module>.opt'.\n"),
io__write_string("\t\tThis option should only be used by mmake.\n"),
+% io__write_string("\t--make-transitive-optimization-interface\n"),
+% io__write_string("\t--make-trans-opt\n"),
+% io__write_string("\t\tOutput transitive optimization information\n"),
+% io__write_string("\t\tinto the <module>.trans_opt file.\n"),
io__write_string("\t-G, --convert-to-goedel\n"),
io__write_string("\t\tConvert to Goedel. Output to file `<module>.loc'.\n"),
io__write_string("\t\tNote that some Mercury language constructs cannot\n"),
@@ -1357,6 +1410,31 @@
io__write_string("\t\tPerform inlining and higher-order specialization of\n"),
io__write_string("\t\tthe code for predicates imported from other modules.\n"),
io__write_string("\t\tThis option must be set throughout the compilation process.\n"),
+% io__write_string("\t--transitive-intermodule-optimization\n"),
+% io__write_string("\t--trans-intermod-opt\n"),
+% io__write_string("\t\tImport the transitive intermodule optimization data.\n"),
+% io__write_string("\t\tThis data is imported from <module>.trans_opt files.\n"),
+ io__write_string("\t--enable-termination"),
+ io__write_string("\t--enable-term"),
+ io__write_string("\t\tAnalyse each predicate to discover if it terminates.\n"),
+ io__write_string("\t--check-termination"),
+ io__write_string("\t--check-term"),
+ io__write_string("\t--chk-term"),
+ io__write_string("\t\tEnable termination analysis, and emit warnings for some\n"),
+ io__write_string("\t\tpredicates or functions that cannot be proved to terminate. In\n"),
+ io__write_string("\t\tmany cases where the compiler is unable to prove termination\n"),
+ io__write_string("\t\tthe problem is either a lack of information about the\n"),
+ io__write_string("\t\ttermination properties of other predicates, or because language\n"),
+ io__write_string("\t\tconstructs (such as higher order calls) were used which could\n"),
+ io__write_string("\t\tnot be analysed. In these cases the compiler does not emit a\n"),
+ io__write_string("\t\twarning of non-termination, as it is likely to be spurious.\n"),
+ io__write_string("\t--verbose-check-termination"),
+ io__write_string("\t--verb-check-term"),
+ io__write_string("\t--verb-chk-term"),
+ io__write_string("\t\tEnable termination analysis, and emit warnings for all\n"),
+ io__write_string("\t\tpredicates or functions that cannot be proved to terminate.\n"),
+ io__write_string("\t--termination-norm"),
+ io__write_string("\t\tSet the norm to be used when doing termination analysis.\n"),
io__write_string("\t--split-c-files\n"),
io__write_string("\t\tGenerate each C function in its own C file,\n"),
io__write_string("\t\tso that the linker will optimize away unused code.\n"),
Index: compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.25
diff -u -r1.25 prog_data.m
--- 1.25 1997/09/14 09:24:30
+++ prog_data.m 1997/10/04 08:51:08
@@ -19,7 +19,7 @@
:- interface.
:- import_module hlds_data, hlds_pred, (inst).
-:- import_module list, map, varset, term, std_util.
+:- import_module term_util, list, map, varset, term, std_util.
%-----------------------------------------------------------------------------%
@@ -29,109 +29,129 @@
% the error/warning message, and the
% term to which it relates
-:- type program ---> module(
- module_name,
- item_list
- ).
+:- type program
+ ---> module(
+ module_name,
+ item_list
+ ).
:- type item_list == list(item_and_context).
:- type item_and_context == pair(item, term__context).
-:- type item ---> pred_clause(varset, sym_name, list(term), goal)
- % VarNames, PredName, HeadArgs, ClauseBody
+:- type item
+ ---> pred_clause(varset, sym_name, list(term), goal)
+ % VarNames, PredName, HeadArgs, ClauseBody
+
+ ; func_clause(varset, sym_name, list(term), term, goal)
+ % VarNames, PredName, HeadArgs, Result, ClauseBody
+
+ ; type_defn(varset, type_defn, condition)
+ ; inst_defn(varset, inst_defn, condition)
+ ; mode_defn(varset, mode_defn, condition)
+ ; module_defn(varset, module_defn)
+
+ ; pred(varset, sym_name, list(type_and_mode),
+ maybe(determinism), condition)
+ % VarNames, PredName, ArgTypes, Deterministicness, Cond
+
+ ; func(varset, sym_name, list(type_and_mode), type_and_mode,
+ maybe(determinism), condition)
+ % VarNames, PredName, ArgTypes, ReturnType,
+ % Deterministicness, Cond
+
+ ; pred_mode(varset, sym_name, list(mode), maybe(determinism),
+ condition)
+ % VarNames, PredName, ArgModes, Deterministicness,
+ % Cond
+
+ ; func_mode(varset, sym_name, list(mode), mode,
+ maybe(determinism), condition)
+ % VarNames, PredName, ArgModes, ReturnValueMode,
+ % Deterministicness, Cond
+
+ ; pragma(pragma_type)
+
+ ; nothing.
+ % used for items that should be ignored (currently only
+ % NU-Prolog `when' declarations, which are silently ignored
+ % for backwards compatibility).
+
+:- type type_and_mode
+ ---> type_only(type)
+ ; type_and_mode(type, mode).
+
+:- type pragma_type
+ ---> c_header_code(string)
+
+ ; c_code(string)
+
+ ; c_code(may_call_mercury, sym_name, pred_or_func,
+ list(pragma_var), varset, string)
+ % Whether or not the C code may call Mercury,
+ % PredName, Predicate or Function, Vars/Mode,
+ % VarNames, C Code
+
+ ; c_code(may_call_mercury, sym_name,
+ pred_or_func, list(pragma_var),
+ list(string), list(string),
+ varset, string)
+ % Whether or not the C code may call Mercury,
+ % PredName, Predicate or Function, Vars/Mode,
+ % SavedeVars, LabelNames, VarNames, C Code
+
+ ; memo(sym_name, arity)
+ % Predname, Arity
+
+ ; inline(sym_name, arity)
+ % Predname, Arity
+
+ ; no_inline(sym_name, arity)
+ % Predname, Arity
+
+ ; obsolete(sym_name, arity)
+ % Predname, Arity
+
+ ; export(sym_name, pred_or_func, list(mode),
+ string)
+ % Predname, Predicate/function, Modes,
+ % C function name.
+
+ ; source_file(string)
+ % Source file name.
+
+ ; unused_args(pred_or_func, sym_name, int,
+ proc_id, list(int))
+ % PredName, Arity, Mode, Optimized pred name,
+ % Removed arguments.
+ % Used for inter-module unused argument
+ % removal, should only appear in .opt files.
+
+ ; fact_table(sym_name, arity, string)
+ % Predname, Arity, Fact file name.
+
+ ; termination_info(pred_or_func, sym_name, list(mode),
+ termination)
+ % the list(mode) is the declared argmodes of the
+ % procedure, unless there are no declared argmodes,
+ % in which case the inferred argmodes are used.
+ % This pragma is used to define information about a
+ % predicates termination properties. It is most
+ % useful where the compiler has insufficient
+ % information to be able to analyse the predicate.
+ % This includes c_code, and imported predicates.
+ % termination_info pragmas are used in opt and
+ % trans_opt files.
- ; func_clause(varset, sym_name, list(term), term,
- goal)
- % VarNames, PredName, HeadArgs, Result,
- % ClauseBody
-
- ; type_defn(varset, type_defn, condition)
- ; inst_defn(varset, inst_defn, condition)
- ; mode_defn(varset, mode_defn, condition)
- ; module_defn(varset, module_defn)
-
- ; pred(varset, sym_name, list(type_and_mode),
- maybe(determinism), condition)
- % VarNames, PredName, ArgTypes,
- % Deterministicness, Cond
-
- ; func(varset, sym_name, list(type_and_mode),
- type_and_mode,
- maybe(determinism), condition)
- % VarNames, PredName, ArgTypes,
- % ReturnType,
- % Deterministicness, Cond
-
- ; pred_mode(varset, sym_name, list(mode),
- maybe(determinism), condition)
- % VarNames, PredName, ArgModes,
- % Deterministicness, Cond
-
- ; func_mode(varset, sym_name, list(mode), mode,
- maybe(determinism), condition)
- % VarNames, PredName, ArgModes,
- % ReturnValueMode,
- % Deterministicness, Cond
-
- ; pragma(pragma_type)
-
- ; nothing.
- % used for items that should be ignored
- % (currently only NU-Prolog `when' declarations,
- % which are silently ignored for backwards
- % compatibility).
-
-:- type type_and_mode ---> type_only(type)
- ; type_and_mode(type, mode).
-
-:- type pragma_type ---> c_header_code(string)
- ; c_code(string)
-
- ; c_code(may_call_mercury, sym_name, pred_or_func,
- list(pragma_var), varset, string)
- % Whether or not the C code may call Mercury,
- % PredName, Predicate or Function, Vars/Mode,
- % VarNames, C Code
-
- ; c_code(may_call_mercury, sym_name,
- pred_or_func, list(pragma_var),
- list(string), list(string),
- varset, string)
- % Whether or not the C code may call Mercury,
- % PredName, Predicate or Function, Vars/Mode,
- % SavedeVars, LabelNames, VarNames, C Code
-
- ; memo(sym_name, int)
- % Predname, Arity
-
- ; inline(sym_name, int)
- % Predname, Arity
-
- ; no_inline(sym_name, int)
- % Predname, Arity
-
- ; obsolete(sym_name, int)
- % Predname, Arity
-
- ; export(sym_name, pred_or_func, list(mode),
- string)
- % Predname, Predicate/function, Modes,
- % C function name.
-
- ; source_file(string)
- % Source file name.
-
- ; unused_args(pred_or_func, sym_name, int,
- proc_id, list(int))
- % PredName, Arity, Mode, Optimized pred name,
- % Removed arguments.
- % Used for inter-module unused argument
- % removal, should only appear in .opt files.
+ ; terminates(sym_name, arity)
+ % Predname, Arity
- ; fact_table(sym_name, arity, string).
- % Predname, Arity, Fact file name.
+ ; does_not_terminate(sym_name, arity)
+ % Predname, Arity
+ ; check_termination(sym_name, arity).
+ % Predname, Arity
+
% For pragma c_code, there are two different calling conventions,
% one for C code that may recursively call Mercury code, and another
% more efficient one for the case when we know that the C code will
@@ -140,10 +160,11 @@
---> may_call_mercury
; will_not_call_mercury.
-:- type pragma_var ---> pragma_var(var, string, mode).
- % variable, name, mode
- % we explicitly store the name because we
- % need the real name in code_gen
+:- type pragma_var
+ ---> pragma_var(var, string, mode).
+ % variable, name, mode
+ % we explicitly store the name because we need the real
+ % name in code_gen
%-----------------------------------------------------------------------------%
@@ -155,21 +176,22 @@
% clause/4 defined above
:- type goal == pair(goal_expr, term__context).
-:- type goal_expr ---> (goal,goal)
- ; true
- % could use conj(goals) instead
- ; {goal;goal} % {...} quotes ';'/2.
- ; fail
- % could use disj(goals) instead
- ; not(goal)
- ; some(vars,goal)
- ; all(vars,goal)
- ; implies(goal,goal)
- ; equivalent(goal,goal)
- ; if_then(vars,goal,goal)
- ; if_then_else(vars,goal,goal,goal)
- ; call(sym_name, list(term))
- ; unify(term, term).
+:- type goal_expr
+ ---> (goal,goal)
+ ; true
+ % could use conj(goals) instead
+ ; {goal;goal} % {...} quotes ';'/2.
+ ; fail
+ % could use disj(goals) instead
+ ; not(goal)
+ ; some(vars,goal)
+ ; all(vars,goal)
+ ; implies(goal,goal)
+ ; equivalent(goal,goal)
+ ; if_then(vars,goal,goal)
+ ; if_then_else(vars,goal,goal,goal)
+ ; call(sym_name, list(term))
+ ; unify(term, term).
:- type goals == list(goal).
:- type vars == list(var).
@@ -183,13 +205,13 @@
% type_defn/3 define above
-:- type type_defn ---> du_type(sym_name, list(type_param),
- list(constructor),
- maybe(equality_pred)
- )
- ; uu_type(sym_name, list(type_param), list(type))
- ; eqv_type(sym_name, list(type_param), type)
- ; abstract_type(sym_name, list(type_param)).
+:- type type_defn
+ ---> du_type(sym_name, list(type_param), list(constructor),
+ maybe(equality_pred)
+ )
+ ; uu_type(sym_name, list(type_param), list(type))
+ ; eqv_type(sym_name, list(type_param), type)
+ ; abstract_type(sym_name, list(type_param)).
:- type constructor == pair(sym_name, list(constructor_arg)).
@@ -220,8 +242,9 @@
% The compiler will ignore these assertions - they are intended
% to be used by other tools, such as the debugger.
-:- type condition ---> true
- ; where(term).
+:- type condition
+ ---> true
+ ; where(term).
%-----------------------------------------------------------------------------%
@@ -232,8 +255,9 @@
% inst_defn/3 defined above
-:- type inst_defn ---> eqv_inst(sym_name, list(inst_param), inst)
- ; abstract_inst(sym_name, list(inst_param)).
+:- type inst_defn
+ ---> eqv_inst(sym_name, list(inst_param), inst)
+ ; abstract_inst(sym_name, list(inst_param)).
% probably inst parameters should be variables not terms
:- type inst_param == term.
@@ -257,17 +281,16 @@
% and `ground_inst' and `any_inst' are special cases of `unify_inst'.
% The reason for having the special cases is efficiency.
-:- type inst_name ---> user_inst(sym_name, list(inst))
- ; merge_inst(inst, inst)
- ; unify_inst(is_live, inst, inst, unify_is_real)
- ; ground_inst(inst_name, is_live, uniqueness,
- unify_is_real)
- ; any_inst(inst_name, is_live, uniqueness,
- unify_is_real)
- ; shared_inst(inst_name)
- ; mostly_uniq_inst(inst_name)
- ; typed_ground(uniqueness, type)
- ; typed_inst(type, inst_name).
+:- type inst_name
+ ---> user_inst(sym_name, list(inst))
+ ; merge_inst(inst, inst)
+ ; unify_inst(is_live, inst, inst, unify_is_real)
+ ; ground_inst(inst_name, is_live, uniqueness, unify_is_real)
+ ; any_inst(inst_name, is_live, uniqueness, unify_is_real)
+ ; shared_inst(inst_name)
+ ; mostly_uniq_inst(inst_name)
+ ; typed_ground(uniqueness, type)
+ ; typed_inst(type, inst_name).
% Note: `is_live' records liveness in the sense used by
% mode analysis. This is not the same thing as the notion of liveness
@@ -297,10 +320,12 @@
% mode_defn/3 defined above
-:- type mode_defn ---> eqv_mode(sym_name, list(inst_param), mode).
+:- type mode_defn
+ ---> eqv_mode(sym_name, list(inst_param), mode).
-:- type (mode) ---> ((inst) -> (inst))
- ; user_defined_mode(sym_name, list(inst)).
+:- type (mode)
+ ---> ((inst) -> (inst))
+ ; user_defined_mode(sym_name, list(inst)).
% mode/4 defined above
@@ -309,69 +334,82 @@
% This is how module-system declarations (such as imports
% and exports) are represented.
-:- type module_defn ---> module(module_name)
- ; interface
- ; implementation
- ; imported
- % This is used internally by the compiler,
- % to identify declarations which originally
- % came from some other module imported with
- % a `:- import_module' declaration.
- ; used
- % This is used internally by the compiler,
- % to identify declarations which originally
- % came from some other module and for which
- % all uses must be module qualified. This
- % applies to items from modules imported using
- % `:- use_module', and items from `.opt'
- % and `.int2' files.
- ; external(sym_name_specifier)
- ; opt_imported
- % This is used internally by the compiler,
- % to identify items which originally
- % came from a .opt file.
- ; end_module(module_name)
- ; export(sym_list)
- ; import(sym_list)
- ; use(sym_list).
-:- type sym_list ---> sym(list(sym_specifier))
- ; pred(list(pred_specifier))
- ; func(list(func_specifier))
- ; cons(list(cons_specifier))
- ; op(list(op_specifier))
- ; adt(list(adt_specifier))
- ; type(list(type_specifier))
- ; module(list(module_specifier)).
-:- type sym_specifier ---> sym(sym_name_specifier)
- ; typed_sym(typed_cons_specifier)
- ; pred(pred_specifier)
- ; func(func_specifier)
- ; cons(cons_specifier)
- ; op(op_specifier)
- ; adt(adt_specifier)
- ; type(type_specifier)
- ; module(module_specifier).
-:- type pred_specifier ---> sym(sym_name_specifier)
- ; name_args(sym_name, list(type)).
+:- type module_defn
+ ---> module(module_name)
+ ; interface
+ ; implementation
+ ; imported
+ % This is used internally by the compiler,
+ % to identify declarations which originally
+ % came from some other module imported with
+ % a `:- import_module' declaration.
+ ; used
+ % This is used internally by the compiler,
+ % to identify declarations which originally
+ % came from some other module and for which
+ % all uses must be module qualified. This
+ % applies to items from modules imported using
+ % `:- use_module', and items from `.opt'
+ % and `.int2' files.
+ ; external(sym_name_specifier)
+ ; opt_imported
+ % This is used internally by the compiler,
+ % to identify items which originally
+ % came from a .opt file.
+ ; end_module(module_name)
+ ; export(sym_list)
+ ; import(sym_list)
+ ; use(sym_list).
+
+:- type sym_list
+ ---> sym(list(sym_specifier))
+ ; pred(list(pred_specifier))
+ ; func(list(func_specifier))
+ ; cons(list(cons_specifier))
+ ; op(list(op_specifier))
+ ; adt(list(adt_specifier))
+ ; type(list(type_specifier))
+ ; module(list(module_specifier)).
+
+:- type sym_specifier
+ ---> sym(sym_name_specifier)
+ ; typed_sym(typed_cons_specifier)
+ ; pred(pred_specifier)
+ ; func(func_specifier)
+ ; cons(cons_specifier)
+ ; op(op_specifier)
+ ; adt(adt_specifier)
+ ; type(type_specifier)
+ ; module(module_specifier).
+:- type pred_specifier
+ ---> sym(sym_name_specifier)
+ ; name_args(sym_name, list(type)).
:- type func_specifier == cons_specifier.
-:- type cons_specifier ---> sym(sym_name_specifier)
- ; typed(typed_cons_specifier).
-:- type typed_cons_specifier --->
- name_args(sym_name, list(type))
- ; name_res(sym_name_specifier, type)
- ; name_args_res(sym_name,
- list(type), type).
+:- type cons_specifier
+ ---> sym(sym_name_specifier)
+ ; typed(typed_cons_specifier).
+:- type typed_cons_specifier
+ ---> name_args(sym_name, list(type))
+ ; name_res(sym_name_specifier, type)
+ ; name_args_res(sym_name, list(type), type).
:- type adt_specifier == sym_name_specifier.
:- type type_specifier == sym_name_specifier.
-:- type op_specifier ---> sym(sym_name_specifier)
- % operator fixity specifiers not yet implemented
- ; fixity(sym_name_specifier, fixity).
-:- type fixity ---> infix ; prefix ; postfix ;
- binary_prefix ; binary_postfix.
-:- type sym_name_specifier ---> name(sym_name)
- ; name_arity(sym_name, arity).
-:- type sym_name ---> unqualified(string)
- ; qualified(module_specifier, string).
+:- type op_specifier
+ ---> sym(sym_name_specifier)
+ % operator fixity specifiers not yet implemented
+ ; fixity(sym_name_specifier, fixity).
+:- type fixity
+ ---> infix
+ ; prefix
+ ; postfix
+ ; binary_prefix
+ ; binary_postfix.
+:- type sym_name_specifier
+ ---> name(sym_name)
+ ; name_arity(sym_name, arity).
+:- type sym_name
+ ---> unqualified(string)
+ ; qualified(module_specifier, string).
:- type module_specifier == string.
:- type module_name == string.
Index: compiler/prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.163
diff -u -r1.163 prog_io.m
--- 1.163 1997/09/15 18:04:16
+++ prog_io.m 1997/10/02 01:22:05
@@ -1407,17 +1407,17 @@
parse_mode_decl_pred(ModuleName, VarSet, ModeDefn, Result)
).
+ % People never seem to remember what the right operator to use in a
+ % `:- mode' declaration is, so the syntax is forgiving. We allow
+ % `::', the standard one which has the right precedence, but we
+ % also allow `==' just to be nice.
:- pred mode_op(term, term, term).
:- mode mode_op(in, out, out) is semidet.
mode_op(term__functor(term__atom(Op), [H, B], _), H, B) :-
- % People never seem to remember what the right
- % operator to use in a `:- mode' declaration is,
- % so the syntax is forgiving.
- % We allow `::', the standard one which has the right
- % precedence, but we also allow `==' just to be nice.
- ( Op = "::"
- -> true
- ; Op = "=="
+ ( Op = "::" ->
+ true
+ ;
+ Op = "=="
).
:- pred convert_mode_defn(string, term, term, maybe1(mode_defn)).
Index: compiler/prog_io_pragma.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_pragma.m,v
retrieving revision 1.6
diff -u -r1.6 prog_io_pragma.m
--- 1.6 1997/07/27 15:01:29
+++ prog_io_pragma.m 1997/10/04 08:55:44
@@ -22,8 +22,8 @@
:- implementation.
-:- import_module prog_io_goal, hlds_pred.
-:- import_module string, std_util.
+:- import_module prog_io_goal, hlds_pred, term_util, term_errors.
+:- import_module string, std_util, bool, require.
parse_pragma(ModuleName, VarSet, PragmaTerms, Result) :-
(
@@ -321,6 +321,114 @@
ErrorTerm)
).
+parse_pragma_type(ModuleName, "termination_info", PragmaTerms, ErrorTerm,
+ _VarSet, Result) :-
+ (
+ PragmaTerms = [
+ PredAndModesTerm0,
+ ConstTerm,
+ TerminatesTerm,
+ MaybeUsedArgsTerm
+ ],
+ (
+ PredAndModesTerm0 = term__functor(Const, Terms0, _)
+ ->
+ (
+ Const = term__atom("="),
+ Terms0 = [FuncAndModesTerm, FuncResultTerm0]
+ ->
+ % function
+ PredOrFunc = function,
+ PredAndModesTerm = FuncAndModesTerm,
+ FuncResultTerm = [FuncResultTerm0]
+ ;
+ % predicate
+ PredOrFunc = predicate,
+ PredAndModesTerm = PredAndModesTerm0,
+ FuncResultTerm = []
+ ),
+ parse_qualified_term(ModuleName, PredAndModesTerm,
+ "pragma termination_info declaration", PredNameResult),
+ PredNameResult = ok(PredName, ModeListTerm0),
+ (
+ PredOrFunc = predicate,
+ ModeListTerm = ModeListTerm0
+ ;
+ PredOrFunc = function,
+ list__append(ModeListTerm0, FuncResultTerm, ModeListTerm)
+ ),
+ convert_mode_list(ModeListTerm, ModeList),
+ (
+ ConstTerm = term__functor(term__atom("not_set"), [], _),
+ TerminationConst = not_set
+ ;
+ ConstTerm = term__functor(
+ term__atom("infinite"), [], ConstContext),
+ TerminationConst = inf(ConstContext - imported_pred)
+ ;
+ ConstTerm = term__functor(term__atom("set"), [IntTerm], _),
+ IntTerm = term__functor(term__integer(Int), [], _),
+ TerminationConst = set(Int)
+ ),
+ (
+ TerminatesTerm = term__functor(term__atom("not_set"), [], _),
+ Terminates = not_set,
+ MaybeError = no
+ ;
+ TerminatesTerm = term__functor(
+ term__atom("dont_know"), [], TermContext),
+ Terminates = dont_know,
+ MaybeError = yes(TermContext - imported_pred)
+ ;
+ TerminatesTerm = term__functor(term__atom("yes"), [], _),
+ Terminates = yes,
+ MaybeError = no
+ ),
+ (
+ MaybeUsedArgsTerm = term__functor(
+ term__atom("yes"), [BoolListTerm], _),
+ convert_bool_list(BoolListTerm, BoolList),
+ MaybeUsedArgs = yes(BoolList)
+ ;
+ MaybeUsedArgsTerm = term__functor(term__atom("no"), [], _),
+ MaybeUsedArgs = no
+ ),
+ Termination = term(TerminationConst, Terminates,
+ MaybeUsedArgs, MaybeError),
+ Result0 = ok(pragma(termination_info(PredOrFunc, PredName,
+ ModeList, Termination)))
+ ;
+ Result0 = error("unexpected variable in pragma termination_info",
+ ErrorTerm)
+ )
+ ->
+ Result = Result0
+ ;
+ Result = error("Syntax error in pragma termination_info", ErrorTerm)
+ ).
+
+
+parse_pragma_type(ModuleName, "terminates", PragmaTerms,
+ ErrorTerm, _VarSet, Result) :-
+ parse_simple_pragma(ModuleName, "terminates",
+ lambda([Name::in, Arity::in, Pragma::out] is det,
+ Pragma = terminates(Name, Arity)),
+ PragmaTerms, ErrorTerm, Result).
+
+parse_pragma_type(ModuleName, "does_not_terminate", PragmaTerms,
+ ErrorTerm, _VarSet, Result) :-
+ parse_simple_pragma(ModuleName, "does_not_terminate",
+ lambda([Name::in, Arity::in, Pragma::out] is det,
+ Pragma = does_not_terminate(Name, Arity)),
+ PragmaTerms, ErrorTerm, Result).
+
+parse_pragma_type(ModuleName, "check_termination", PragmaTerms,
+ ErrorTerm, _VarSet, Result) :-
+ parse_simple_pragma(ModuleName, "check_termination",
+ lambda([Name::in, Arity::in, Pragma::out] is det,
+ Pragma = check_termination(Name, Arity)),
+ PragmaTerms, ErrorTerm, Result).
+
:- pred parse_simple_pragma(module_name, string,
pred(sym_name, int, pragma_type),
list(term), term, maybe1(item)).
@@ -450,8 +558,8 @@
Result = error(Msg, Term)
)
;
- Result = error("unexpected variable in pragma(c_code, ...)",
- PredAndVarsTerm0)
+ Result = error("unexpected variable in pragma c_code",
+ PredAndVarsTerm0)
).
% parse the variable list in the pragma c code declaration.
@@ -518,3 +626,24 @@
Result = error("error in int list",
term__functor(Functor, Args, Context))
).
+
+:- pred convert_bool_list(term::in, list(bool)::out) is semidet.
+
+convert_bool_list(term__functor(Functor, Args, _), Bools) :-
+ (
+ Functor = term__atom("."),
+ Args = [term__functor(AtomTerm, [], _), RestTerm],
+ (
+ AtomTerm = term__atom("yes"),
+ Bool = yes
+ ;
+ AtomTerm = term__atom("no"),
+ Bool = no
+ ),
+ convert_bool_list(RestTerm, RestList),
+ Bools = [ Bool | RestList ]
+ ;
+ Functor = term__atom("[]"),
+ Args = [],
+ Bools = []
+ ).
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.73
diff -u -r1.73 reference_manual.texi
--- 1.73 1997/09/27 19:53:41
+++ reference_manual.texi 1997/10/05 10:13:18
@@ -3415,11 +3415,16 @@
also choose to support additional pragmas with implementation-dependent
semantics.
-The University of Melbourne Mercury implemenation supports the following
+The University of Melbourne Mercury implementation supports the following
additional pragmas:
@menu
-* Fact tables:: Support for very large tables of facts
+* Fact tables:: Support for very large tables of facts.
+* Termination Analysis:: Information about a predicate or functions
+ termination properties can be given to the
+ compiler. Pragmas are also available to
+ force the compiler to prove termination of
+ a given predicate or function.
@end menu
@node Fact tables
@@ -3457,5 +3462,79 @@
predicates or functions defined as fact tables can only have
arguments of types @samp{string}, @samp{int} or @samp{float}.
+ at node Termination Analysis
+ at subsection Termination Analysis
+
+The compiler includes a termination analyser which can be used to prove
+termination of predicates and functions. Details of the analysis are
+available in "Termination Analysis for Mercury" by Chris Speirs, Zoltan
+Somogyi and Harald S at o{}ndergaard. In P. Van Hentenryck, editor, "Static
+Analysis: Proceedings of the 4th International Symposium", Lecture Notes
+in Computer Science. Springer, 1997. A longer version is available for
+download from http://www.cs.mu.oz.au/publications/tr_db/mu_97_09.ps.gz
+
+The analysis is based around an algorithm proposed by Gerhard Gr@"oger
+and Lutz Pl@"umer in their paper "Handling of mutual recursion in
+automatic termination proofs for logic programs." in K. Apt, editor,
+The Proceedings of the Joint International Conference and Symposium on
+Logic Programming, pager 336-350. MIT Press, 1992.
+
+The analyser is enabled by the option @samp{--enable-termination}, which
+can be abbreviated to @samp{--enable-term}. When termination analysis
+is enabled, any predicates or functions with a @samp{check_termination}
+pragma defined on them will have their termination checked, and if
+termination cannot be proved, the compiler will emit an error message
+detailing the reason that termination could not be proved and then quit.
+
+The option @samp{--check-termination} option, which may be abbreviated
+to @samp{--check-term} or @samp{--chk-term}, forces the compiler to
+check the termination of all predicates in the module.
+It is common for the compiler to be unable to prove termination of some
+predicates and functions because they call other predicates which could
+not be proved to terminate or because they use language features (such
+as higher order calls) which cannot be analysed.
+In this case, the compiler only emits a warning for these
+predicates and functions if the @samp{-E} option is enabled.
+For every predicate or function that the compiler cannot prove
+termination, a warning message is emitted, but compilation continues.
+The @samp{--check-termination} option implies the
+ at samp{--enable-termination} option.
+
+The accuracy of the termination analysis is substantially degraded if
+intermodule optimization is not enabled. Unless intermodule
+optimization is enabled, the compiler must assume that any imported
+predicate may not terminate.
+
+Currently the compiler assumes that all c code terminates for any input.
+If this is not the case, a @samp{pragma does_not_terminate} declaration
+may be used to inform the compiler that this c_code may not terminate.
+
+The following declarations can be used to inform the compiler of a
+predicate or functions termination properties, or to force the compiler
+to prove termination of a given predicate or function.
+
+ at example
+:- pragma terminates(@var{Name}/@var{Arity}).
+ at end example
+This declaration may be used to inform the compiler that this predicate
+or function is guaranteed to terminate for any input. This is useful
+when the compiler cannot prove termination of some predicates or
+functions which are in turn preventing the compiler from proving
+termination of other predicates or functions.
+
+ at example
+:- pragma does_not_terminate(@var{Name}/@var{Arity}).
+ at end example
+This declaration may be used to inform the compiler that this predicate
+does not necessarily terminate for any input. This is useful for c
+code, which the compiler assumes to terminate by default.
+
+ at example
+:- pragma check_termination(@var{Name}/@var{Arity}).
+ at end example
+This pragma forces the compiler to prove termination of this predicate.
+If it cannot prove the termination of the specified predicate or
+function then the compiler will quit with an error message.
+
@contents
@bye
Index: doc/user_guide.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/user_guide.texi,v
retrieving revision 1.98
diff -u -r1.98 user_guide.texi
--- 1.98 1997/10/03 04:56:13
+++ user_guide.texi 1997/10/05 09:04:27
@@ -136,6 +136,9 @@
interface files used in inter-module optimization,
and are created using the @samp{--make-optimization-interface}
(or @samp{--make-opt-int}) option.
+ at c Files ending in @file{.trans_opt} are interface files used in
+ at c transitive inter-module otimization, and are created using the
+ at c @samp{--make-transitive-optimization-interface} option.
Since the interface of a module changes less often than its implementation,
the @file{.int}, @file{.int2}, @file{.int3}, and @file{.opt}
@@ -222,6 +225,13 @@
mmc --make-opt-int @var{module1}.m @var{module2}.m ...
@end example
+ at c If you are going to compile with @samp{--transitive-intermodule-optimization}
+ at c enabled, then you also need to create the transitive optimization files.
+
+ at c @example
+ at c mmc -make-trans-opt @var{module1}.m @var{module2}.m ...
+ at c @end example
+ at c
Given that you have made all the interface files,
one way to create an executable for a multi-module program
is to compile all the modules at the same time
@@ -613,7 +623,8 @@
Removes all the automatically generated files.
In addition to the files removed by @var{main-module}.clean, this
removes the @samp{.date}, @samp{.int}, @samp{.int2}, @samp{.int3},
- at samp{.opt}, @samp{.optdate},
+ at samp{.opt}, @samp{.optdate}, @samp{.date3},
+ at c @samp{.trans_opt}, @samp{.trans_optdate},
@samp{.d}, and @samp{.dep} belonging to one of the modules of the program,
and also the various possible executables for the program ---
@samp{@var{main-module}},
@@ -831,7 +842,7 @@
Here @samp{VPATH} is a colon-separated list of path names specifying
directories that Mmake will search for interface files.
-The @samp{-I} options in @samp{MCFLAGS} tell @samp{mc} where to find
+The @samp{-I} options in @samp{MCFLAGS} tell @samp{mmc} where to find
the interface files. The @samp{-R} options in @samp{MLFLAGS} tell
the loader where to find shared libraries, and the @samp{-L}
options tell the linker where to find libraries.
@@ -1226,7 +1237,7 @@
@sp 1
@item -V
- at itemx --very_verbose
+ at itemx --very-verbose
Output very verbose progress messages.
@sp 1
@@ -1301,6 +1312,15 @@
Write information used for inter-module optimization to
@file{@var{module}.opt}.
+ at c @sp 1
+ at c @item --make-transitive-optimization-interface
+ at c @itemx --make-trans-opt
+ at c Write the @file{@var{module}.trans_opt} file. This file is used to store
+ at c information used for inter-module optimization. The information is read
+ at c in when the compiler is invoked with the --transitive-otimization
+ at c option. The file is transitive as a @file{@var{module}.trans_opt} file
+ at c may depend on other @file{@var{module}.trans_opt} files.
+ at c
@sp 1
@item -G
@itemx --convert-to-goedel
@@ -1423,6 +1443,7 @@
p - pre-birth, post-birth, pre-death and post-death sets of goals,
r - resume points of goals,
s - store maps of goals,
+t - results of termination analysis,
u - unification categories,
v - variable numbers in variable names.
The special argument value ``all''
@@ -1740,7 +1761,7 @@
@sp 1
@item --opt-space
- at item --optimize-space
+ at itemx --optimize-space
Turn on optimizations that reduce code size
and turn off optimizations that significantly increase code size.
@end table
@@ -1750,6 +1771,45 @@
Perform inlining and higher-order specialization of the code for
predicates or functions imported from other modules.
+ at c @sp 1
+ at c @item --transitive-intermodule-optimization
+ at c @item --trans-intermod-opt
+ at c Use the information stored in other @file{@var{module}.trans_opt} files
+ at c to make intermodule optimizations. The @file{@var{module}.trans_opt} is
+ at c different to the @file{@var{module}.opt} as @file{@var{module}.trans_opt}
+ at c files may depend on other @file{@var{module}.trans_opt} files.
+ at c @file{@var{module}.opt} files may only depend on the
+ at c @file{@var{module}.m} file.
+ at c
+ at sp 1
+ at item --enable-termination
+ at itemx --enable-term
+Enable termination analysis. Termination analysis analyses each mode of
+each predicate to see whether it terminates. @samp{pragma terminates},
+ at samp{pragma does_not_terminate} and @samp{pragma check_termination}
+pragmas have no effect unless termination analysis is enabled. When
+using termination, @samp{--intermodule-optimization} should be enabled,
+as it greatly improves the accuracy of the analysis.
+
+ at sp 1
+ at item --check-termination
+ at itemx --check-term
+ at itemx --chk-term
+Enable termination analysis, and emit warnings for some predicates or
+functions that cannot be proved to terminate. In many cases where the
+compiler is unable to prove termination the problem is either a lack of
+information about the termination properties of other predicates, or
+because language constructs (such as higher order calls) were used which
+could not be analysed. In these cases the compiler does not emit a
+warning of non-termination, as it is likely to be spurious.
+
+ at sp 1
+ at item --verbose-check-termination
+ at itemx --verb-check-term
+ at itemx --verb-chk-term
+Enable termination analysis, and emit warnings for all predicates or
+functions that cannot be proved to terminate.
+
@sp 1
@item --split-c-files
Generate each C function in its own C file,
More information about the developers
mailing list