[m-rev.] for review: new termination analyser (part 3 of 6)
Julien Fischer
juliensf at cs.mu.OZ.AU
Thu Mar 24 15:45:29 AEDT 2005
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.506
diff -u -r1.506 make_hlds.m
--- compiler/make_hlds.m 22 Mar 2005 06:40:06 -0000 1.506
+++ compiler/make_hlds.m 22 Mar 2005 06:49:30 -0000
@@ -130,6 +130,8 @@
:- import_module hlds__special_pred.
:- import_module libs__globals.
:- import_module libs__options.
+:- import_module libs__polyhedron.
+:- import_module libs__lp_rational.
:- import_module ll_backend.
:- import_module ll_backend__fact_table.
:- import_module ll_backend__llds.
@@ -147,6 +149,8 @@
:- import_module parse_tree__prog_util.
:- import_module parse_tree__prog_type.
:- import_module recompilation.
+:- import_module transform_hlds__term_constr_util.
+:- import_module transform_hlds__termination2.
:- import_module transform_hlds__term_util.
:- import_module assoc_list.
@@ -866,6 +870,9 @@
% these pragmas
Pragma = termination_info(_, _, _, _, _)
;
+ % As for termination_info pragmas
+ Pragma = termination2_info(_, _, _, _, _, _, _)
+ ;
Pragma = terminates(Name, Arity),
add_pred_marker("terminates", Name, Arity, ImportStatus, Context,
terminates, [check_termination, does_not_terminate], !ModuleInfo,
@@ -881,7 +888,6 @@
Context, check_termination, [terminates, does_not_terminate],
!ModuleInfo, !IO)
).
-
add_item_decl_pass_2(Item, _Context, !Status, !ModuleInfo, !IO) :-
Item = pred_or_func(_TypeVarSet, _InstVarSet, _ExistQVars,
PredOrFunc, SymName, TypesAndModes, _WithType, _WithInst,
@@ -999,6 +1005,7 @@
module_add_clause(VarSet, PredOrFunc, PredName, Args, Body, !.Status,
Context, GoalType, !ModuleInfo, !QualInfo, !IO).
+
add_item_clause(Item, !Status, Context, !ModuleInfo, !QualInfo, !IO) :-
Item = type_defn(_TVarSet, SymName, TypeParams, TypeDefn, _Cond),
% If this is a solver type then we need to also add clauses
@@ -1115,6 +1122,15 @@
MaybeArgSizeInfo, MaybeTerminationInfo, Context,
!ModuleInfo, !IO)
;
+ Pragma = termination2_info(PredOrFunc, SymName, ModeList,
+ HeadVarIds, MaybeSuccessArgSizeInfo,
+ MaybeFailureArgSizeInfo, MaybeTerminationInfo)
+ ->
+ add_pragma_termination2_info(PredOrFunc, SymName, ModeList,
+ HeadVarIds, MaybeSuccessArgSizeInfo,
+ MaybeFailureArgSizeInfo, MaybeTerminationInfo, Context,
+ !ModuleInfo, !IO)
+ ;
Pragma = reserve_tag(TypeName, TypeArity)
->
add_pragma_reserve_tag(TypeName, TypeArity, !.Status,
@@ -2027,6 +2043,92 @@
).
%-----------------------------------------------------------------------------%
+
+:- pred add_pragma_termination2_info(pred_or_func::in, sym_name::in,
+ list(mode)::in, list(int)::in, maybe(pragma_constr_arg_size_info)::in,
+ maybe(pragma_constr_arg_size_info)::in,
+ maybe(pragma_termination_info)::in, prog_context::in, module_info::in,
+ module_info::out, io::di, io::uo) is det.
+add_pragma_termination2_info(PredOrFunc, SymName, ModeList, HeadVarIds,
+ MaybePragmaSuccessArgSizeInfo, MaybePragmaFailureArgSizeInfo,
+ MaybePragmaTerminationInfo,
+ Context, !ModuleInfo, !IO) :-
+ module_info_get_predicate_table(!.ModuleInfo, Preds),
+ list.length(ModeList, Arity),
+ (
+ predicate_table_search_pf_sym_arity(Preds,
+ is_fully_qualified, PredOrFunc, SymName, Arity, PredIds),
+ PredIds \= []
+ ->
+ ( PredIds = [PredId] ->
+ module_info_preds(!.ModuleInfo, PredTable0),
+ map.lookup(PredTable0, PredId, PredInfo0),
+ pred_info_procedures(PredInfo0, ProcTable0),
+ map.to_assoc_list(ProcTable0, ProcList),
+ (
+ get_procedure_matching_declmodes(ProcList,
+ ModeList, !.ModuleInfo, ProcId)
+ ->
+ map.lookup(ProcTable0, ProcId, ProcInfo0),
+ add_context_to_constr_termination_info(
+ MaybePragmaTerminationInfo, Context,
+ MaybeTerminationInfo),
+
+ some [!TermInfo] (
+ proc_info_get_termination2_info(ProcInfo0, !:TermInfo),
+
+ !:TermInfo = !.TermInfo ^ import_headvarids
+ := yes(HeadVarIds),
+ !:TermInfo = !.TermInfo ^ import_success :=
+ MaybePragmaSuccessArgSizeInfo,
+ !:TermInfo = !.TermInfo ^ import_failure :=
+ MaybePragmaFailureArgSizeInfo,
+ !:TermInfo = !.TermInfo ^ term_status :=
+ MaybeTerminationInfo,
+
+ proc_info_set_termination2_info(!.TermInfo,
+ ProcInfo0, ProcInfo)
+ ),
+ map__det_update(ProcTable0, ProcId, ProcInfo,
+ ProcTable),
+ pred_info_set_procedures(ProcTable, PredInfo0,
+ PredInfo),
+ map__det_update(PredTable0, PredId, PredInfo,
+ PredTable),
+ module_info_set_preds(PredTable, !ModuleInfo)
+ ;
+ module_info_incr_errors(!ModuleInfo),
+ prog_out__write_context(Context, !IO),
+ io.write_string(
+ "Error: `:- pragma termination2_info' " ++
+ "declaration for undeclared mode of ", !IO),
+ hlds_out.write_simple_call_id(PredOrFunc,
+ SymName/Arity, !IO),
+ io.write_string(".\n", !IO)
+ )
+ ;
+ prog_out.write_context(Context, !IO),
+ io.write_string("Error: ambiguous predicate name ", !IO),
+ hlds_out.write_simple_call_id(PredOrFunc, SymName/Arity, !IO),
+ io.nl(!IO),
+ prog_out.write_context(Context, !IO),
+ io.write_string(
+ " in `pragma termination2_info'.\n", !IO),
+ module_info_incr_errors(!ModuleInfo)
+ )
+ ;
+ % XXX This happens in `.trans_opt' files sometimes --
+ % so just ignore it
+ true
+ /***
+ **** undefined_pred_or_func_error(
+ **** SymName, Arity, Context,
+ **** "`:- pragma termination2_info' declaration"),
+ **** { module_info_incr_errors(!ModuleInfo) }
+ ***/
+ ).
+
+%------------------------------------------------------------------------------%
:- pred add_pragma_termination_info(pred_or_func::in, sym_name::in,
list(mode)::in, maybe(pragma_arg_size_info)::in,
Index: compiler/mercury_compile.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_compile.m,v
retrieving revision 1.330
diff -u -r1.330 mercury_compile.m
--- compiler/mercury_compile.m 22 Mar 2005 06:40:08 -0000 1.330
+++ compiler/mercury_compile.m 22 Mar 2005 06:49:31 -0000
@@ -69,6 +69,7 @@
:- import_module transform_hlds__lambda.
:- import_module backend_libs__type_ctor_info.
:- import_module transform_hlds__termination.
+:- import_module transform_hlds__termination2.
:- import_module transform_hlds__exception_analysis.
:- import_module transform_hlds__higher_order.
:- import_module transform_hlds__accumulator.
@@ -2122,6 +2123,7 @@
globals__lookup_bool_option(Globals, verbose, Verbose),
globals__lookup_bool_option(Globals, statistics, Stats),
globals__lookup_bool_option(Globals, termination, Termination),
+ globals__lookup_bool_option(Globals, termination2, Termination2),
globals__lookup_bool_option(Globals, analyse_exceptions,
ExceptionAnalysis),
@@ -2135,6 +2137,7 @@
(
( IntermodArgs = yes
; Termination = yes
+ ; Termination2 = yes
; ExceptionAnalysis = yes
)
->
@@ -2157,7 +2160,13 @@
mercury_compile__maybe_termination(
Verbose, Stats, !HLDS, !IO)
;
- true
+ true
+ ),
+ ( Termination2 = yes ->
+ mercury_compile__maybe_termination2(
+ Verbose, Stats, !HLDS, !IO)
+ ;
+ true
)
;
io__set_exit_status(1, !IO)
@@ -2200,8 +2209,8 @@
is_bool(_).
-:- pred mercury_compile__output_trans_opt_file(module_info::in,
- io::di, io::uo) is det.
+:- pred mercury_compile__output_trans_opt_file(module_info::in, io::di,
+ io::uo) is det.
mercury_compile__output_trans_opt_file(HLDS0, !IO) :-
globals__io_lookup_bool_option(verbose, Verbose, !IO),
@@ -2210,8 +2219,11 @@
HLDS1, !IO),
mercury_compile__maybe_dump_hlds(HLDS1, 118, "exception_analysis",
!IO),
- mercury_compile__maybe_termination(Verbose, Stats, HLDS1, HLDS, !IO),
- mercury_compile__maybe_dump_hlds(HLDS, 120, "termination", !IO),
+ mercury_compile__maybe_termination(Verbose, Stats, HLDS1, HLDS2, !IO),
+ mercury_compile__maybe_dump_hlds(HLDS2, 120, "termination", !IO),
+ mercury_compile__maybe_termination2(Verbose, Stats, HLDS2, HLDS,
+ !IO),
+ mercury_compile__maybe_dump_hlds(HLDS, 121, "termination_2", !IO),
trans_opt__write_optfile(HLDS, !IO).
:- pred mercury_compile__frontend_pass_by_phases(module_info::in,
@@ -2333,6 +2345,9 @@
mercury_compile__maybe_termination(Verbose, Stats, !HLDS, !IO),
mercury_compile__maybe_dump_hlds(!.HLDS, 120, "termination", !IO),
+ mercury_compile__maybe_termination2(Verbose, Stats, !HLDS, !IO),
+ mercury_compile__maybe_dump_hlds(!.HLDS, 121, "termination2", !IO),
+
mercury_compile__maybe_type_ctor_infos(Verbose, Stats, !HLDS, !IO),
mercury_compile__maybe_dump_hlds(!.HLDS, 125, "type_ctor_infos", !IO),
@@ -2901,6 +2916,28 @@
"% Termination checking done.\n", !IO),
maybe_report_stats(Stats, !IO)
;
+ true
+ ).
+
+:- pred mercury_compile__maybe_termination2(bool::in, bool::in,
+ module_info::in, module_info::out, io::di, io::uo) is det.
+
+mercury_compile__maybe_termination2(Verbose, Stats, !HLDS, !IO) :-
+ globals__io_lookup_bool_option(polymorphism, Polymorphism, !IO),
+ globals__io_lookup_bool_option(termination2, Termination2, !IO),
+ % Termination analysis requires polymorphism to be run,
+ % as termination analysis does not handle complex unification.
+ (
+ Polymorphism = yes,
+ Termination2 = yes
+ ->
+ maybe_write_string(Verbose, "% Detecting termination 2...\n",
+ !IO),
+ termination2__pass(!HLDS, !IO),
+ maybe_write_string(Verbose, "% Termination 2 checking done.\n",
+ !IO),
+ maybe_report_stats(Stats, !IO)
+ ;
true
).
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.252
diff -u -r1.252 mercury_to_mercury.m
--- compiler/mercury_to_mercury.m 22 Mar 2005 06:40:08 -0000 1.252
+++ compiler/mercury_to_mercury.m 22 Mar 2005 06:49:31 -0000
@@ -295,7 +295,7 @@
:- pred write_pragma_termination_info(pred_or_func::in, sym_name::in,
list(mode)::in, prog_context::in,
maybe(generic_arg_size_info(T))::in,
- maybe(generic_termination_info(T))::in, io::di, io::uo) is det.
+ maybe(generic_termination_info(S, T))::in, io::di, io::uo) is det.
% Write the given arg size info. Verbose if the second arg is yes.
@@ -304,7 +304,7 @@
% Write the given termination info. Verbose if the second arg is yes.
-:- pred write_maybe_termination_info(maybe(generic_termination_info(T))::in,
+:- pred write_maybe_termination_info(maybe(generic_termination_info(S, T))::in,
bool::in, io::di, io::uo) is det.
:- pred mercury_output_where_attributes(tvarset::in,
@@ -367,6 +367,7 @@
:- import_module libs__globals.
:- import_module libs__options.
+:- import_module libs__rat.
:- import_module parse_tree__prog_io_util.
:- import_module parse_tree__prog_out.
:- import_module parse_tree__prog_util.
@@ -660,6 +661,13 @@
Context, MaybePragmaArgSizeInfo,
MaybePragmaTerminationInfo)
;
+ { Pragma = termination2_info(PredOrFunc, PredName,
+ ModeList, HeadVarIds, SuccessInfo, FailureInfo,
+ MaybeTermination) },
+ write_pragma_termination2_info(PredOrFunc, PredName,
+ ModeList, HeadVarIds, SuccessInfo, FailureInfo,
+ MaybeTermination, Context)
+ ;
{ Pragma = terminates(Pred, Arity) },
mercury_output_pragma_decl(Pred, Arity, predicate, "terminates")
;
@@ -4056,7 +4064,7 @@
MaybeTerminationInfo = no,
io__write_string("not_set", !IO)
;
- MaybeTerminationInfo = yes(cannot_loop),
+ MaybeTerminationInfo = yes(cannot_loop(_)),
io__write_string("cannot_loop", !IO)
;
MaybeTerminationInfo = yes(can_loop(Error)),
@@ -4069,3 +4077,101 @@
true
)
).
+
+%-----------------------------------------------------------------------------%
+%
+% Code to output termination2_info pragmas.
+%
+
+:- pred write_pragma_termination2_info(pred_or_func::in, sym_name::in,
+ list(mode)::in, list(int)::in, maybe(pragma_constr_arg_size_info)::in,
+ maybe(pragma_constr_arg_size_info)::in,
+ maybe(pragma_termination_info)::in, prog_context::in,
+ io::di, io::uo) is det.
+
+write_pragma_termination2_info(PredOrFunc, PredName, ModeList, HeadVarIds,
+ MaybeSuccess, MaybeFailure, MaybeTermination, Context,
+ !IO) :-
+ io.write_string(":- pragma termination2_info(", !IO),
+ (
+ PredOrFunc = predicate,
+ mercury_output_pred_mode_subdecl(varset.init, PredName,
+ ModeList, no, Context, !IO)
+ ;
+ PredOrFunc = function,
+ pred_args_to_func_args(ModeList, FuncModeList, RetMode),
+ mercury_output_func_mode_subdecl(varset.init, PredName,
+ FuncModeList, RetMode, no, Context, !IO)
+ ),
+ io.write_string(", ", !IO),
+ write_head_var_ids(HeadVarIds, !IO),
+ io.write_string(", ", !IO),
+ write_maybe_pragma_constr_arg_size_info(MaybeSuccess, !IO),
+ io.write_string(", ", !IO),
+ write_maybe_pragma_constr_arg_size_info(MaybeFailure, !IO),
+ io.write_string(", ", !IO),
+ write_maybe_pragma_termination_info(MaybeTermination, !IO),
+ io.write_string(").\n", !IO).
+
+:- pred write_head_var_ids(list(int)::in, io::di, io::uo) is det.
+
+write_head_var_ids(VarIds, !IO) :-
+ io.write_char('[', !IO),
+ io.write_list(VarIds, ", ", io.write_int, !IO),
+ io.write_char('[', !IO).
+
+:- pred write_maybe_pragma_constr_arg_size_info(
+ maybe(pragma_constr_arg_size_info)::in, io::di, io::uo) is det.
+
+write_maybe_pragma_constr_arg_size_info(no, !IO) :-
+ io.write_string("not_set", !IO).
+write_maybe_pragma_constr_arg_size_info(yes(ArgSizeInfo), !IO) :-
+ io.write_string("constaints(", !IO),
+ io.write_char('[', !IO),
+ io.write_list(ArgSizeInfo, ", ", write_arg_size_constr, !IO),
+ io.write_char('[', !IO).
+
+:- pred write_arg_size_constr(arg_size_constr::in, io::di, io::uo) is det.
+
+write_arg_size_constr(Constraint, !IO) :-
+ (
+ Constraint = le(Terms, Constant),
+ OpStr = "le("
+ ;
+ Constraint = eq(Terms, Constant),
+ OpStr = "eq("
+ ),
+ io.write_string(OpStr, !IO),
+ io.write_char('[', !IO),
+ io.write_list(Terms, ", ", write_arg_size_term, !IO),
+ io.write_string("], ", !IO),
+ rat.write_rat(Constant, !IO),
+ io.write_char(')', !IO).
+
+:- pred write_arg_size_term(arg_size_term::in, io::di, io::uo) is det.
+
+write_arg_size_term(VarId - Coefficient, !IO) :-
+ io.write_string("term(", !IO),
+ io.write_int(VarId, !IO),
+ io.write_string(", ", !IO),
+ rat.write_rat(Coefficient, !IO),
+ io.write_char(')', !IO).
+
+:- pred write_maybe_pragma_termination_info(maybe(pragma_termination_info)::in,
+ io::di, io::uo) is det.
+
+write_maybe_pragma_termination_info(no, !IO) :-
+ io.write_string("not_set", !IO).
+write_maybe_pragma_termination_info(yes(Termination), !IO) :-
+ (
+ Termination = can_loop(_),
+ TerminationStr = "can_loop"
+ ;
+ Termination = cannot_loop(_),
+ TerminationStr = "cannot_loop"
+ ),
+ io.write_string(TerminationStr, !IO).
+
+%-----------------------------------------------------------------------------%
+:- end_module mercury_to_mercury.
+%-----------------------------------------------------------------------------%
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.99
diff -u -r1.99 module_qual.m
--- compiler/module_qual.m 24 Mar 2005 02:00:30 -0000 1.99
+++ compiler/module_qual.m 24 Mar 2005 02:26:57 -0000
@@ -1034,6 +1034,12 @@
termination_info(PredOrFunc, SymName, ModeList, Args, Term),
!Info, !IO) :-
qualify_mode_list(ModeList0, ModeList, !Info, !IO).
+qualify_pragma(termination2_info(PredOrFunc, SymName, ModeList0, HeadVars,
+ SuccessArgs, FailureArgs, Term),
+ termination2_info(PredOrFunc, SymName, ModeList, HeadVars,
+ SuccessArgs, FailureArgs, Term),
+ !Info, !IO) :-
+ qualify_mode_list(ModeList0, ModeList, !Info, !IO).
qualify_pragma(X at terminates(_, _), X, !Info, !IO).
qualify_pragma(X at does_not_terminate(_, _), X, !Info, !IO).
qualify_pragma(X at check_termination(_, _), X, !Info, !IO).
Index: compiler/modules.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modules.m,v
retrieving revision 1.322
diff -u -r1.322 modules.m
--- compiler/modules.m 22 Mar 2005 06:40:14 -0000 1.322
+++ compiler/modules.m 22 Mar 2005 06:49:33 -0000
@@ -2024,6 +2024,7 @@
pragma_allowed_in_interface(exceptions(_, _, _, _, _), no).
pragma_allowed_in_interface(type_spec(_, _, _, _, _, _, _, _), yes).
pragma_allowed_in_interface(termination_info(_, _, _, _, _), yes).
+pragma_allowed_in_interface(termination2_info(_,_,_, _, _, _, _), yes).
pragma_allowed_in_interface(terminates(_, _), yes).
pragma_allowed_in_interface(does_not_terminate(_, _), yes).
pragma_allowed_in_interface(check_termination(_, _), yes).
Index: compiler/options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/options.m,v
retrieving revision 1.453
diff -u -r1.453 options.m
--- compiler/options.m 23 Mar 2005 01:50:08 -0000 1.453
+++ compiler/options.m 23 Mar 2005 07:05:01 -0000
@@ -116,6 +116,7 @@
; debug_modes_pred_id
; debug_det
; debug_opt
+ ; debug_term % term = constraint termination analysis
; debug_opt_pred_id
; debug_pd % pd = partial deduction/deforestation
; debug_rl_gen
@@ -500,6 +501,17 @@
; termination_norm
; termination_error_limit
; termination_path_limit
+ %
+ % Stuff for the new termination analyser.
+ %
+ ; termination2
+ ; check_termination2
+ ; verbose_check_termination2
+ ; termination2_norm
+ ; widening_limit
+ ; arg_size_analysis_only
+ ; propagate_failure_constrs
+ ; term2_maximum_matrix_size
; analyse_exceptions
; untuple
; tuple
@@ -805,6 +817,7 @@
debug_modes_verbose - bool(no),
debug_modes_pred_id - int(-1),
debug_det - bool(no),
+ debug_term - bool(no),
debug_opt - bool(no),
debug_opt_pred_id - int(-1),
debug_pd - bool(no),
@@ -1063,6 +1076,16 @@
termination_error_limit - int(3),
termination_path_limit - int(256),
split_c_files - bool(no),
+ termination2 - bool(no),
+ termination2_norm - string("total"),
+ check_termination2 - bool(no),
+ verbose_check_termination2 - bool(no),
+ widening_limit - int(4),
+ arg_size_analysis_only - bool(no),
+ propagate_failure_constrs - bool(yes),
+ % XXX This is just a guess - I'm not sure what sensible
+ % value for this is.
+ term2_maximum_matrix_size - int(70),
analyse_exceptions - bool(no)
]).
option_defaults_2(optimization_option, [
@@ -1455,6 +1478,8 @@
long_option("debug-modes-pred-id", debug_modes_pred_id).
long_option("debug-determinism", debug_det).
long_option("debug-det", debug_det).
+long_option("debug-termination", debug_term).
+long_option("debug-term", debug_term).
long_option("debug-opt", debug_opt).
long_option("debug-opt-pred-id", debug_opt_pred_id).
long_option("debug-pd", debug_pd).
@@ -1811,6 +1836,26 @@
long_option("term-err-limit", termination_error_limit).
long_option("termination-path-limit", termination_path_limit).
long_option("term-path-limit", termination_path_limit).
+long_option("enable-termination2", termination2).
+long_option("enable-term2", termination2).
+long_option("check-termination2", check_termination2).
+long_option("check-term2", check_termination2).
+long_option("chk-term2", check_termination2).
+long_option("verbose-check-termination2",verbose_check_termination2).
+long_option("verb-check-term2", verbose_check_termination2).
+long_option("verb-chk-term2", verbose_check_termination2).
+long_option("termination2-widening-limit", widening_limit).
+long_option("term2-widening-limit", widening_limit).
+long_option("arg-size-analysis-only", arg_size_analysis_only).
+long_option("termination2-propagate-failure-constraints",
+ propagate_failure_constrs).
+long_option("term2-propagate-failure-constraints",
+ propagate_failure_constrs).
+long_option("term2-propagate-failure-constrs", propagate_failure_constrs).
+long_option("termination2-norm", termination2_norm).
+long_option("term2-norm", termination2_norm).
+long_option("termination2-maximum-matrix-size", term2_maximum_matrix_size).
+long_option("term2-max-matrix-size", term2_maximum_matrix_size).
long_option("analyse-exceptions", analyse_exceptions).
long_option("untuple", untuple).
long_option("tuple", tuple).
@@ -2733,6 +2778,10 @@
"\tmode checking of the predicate or function with the specified pred id.",
"--debug-det, --debug-determinism",
"\tOutput detailed debugging traces of determinism analysis.",
+% The new termination analyser is currently a work-in-progress.
+%
+ %"--debug-term, --debug-termination",
+ %"\tOutput detailed debugging traces of the termination2 analysis.",
"--debug-opt",
"\tOutput detailed debugging traces of the optimization process.",
"--debug-opt-pred-id <n>",
@@ -3050,8 +3099,46 @@
"--term-path-limit <n>, --termination-path-limit <n>",
"\tPerform termination analysis only on predicates",
"\twith at most <n> paths (default: 256)."
- ]).
+% The following options are used to control the new termination analyser.
+% They are currently disabled because that is still a work-in-progress.
+%
+% "--enable-term2, --enable-termination2",
+% "\tAnalyse each predicate to discover if it terminates. ",
+% "\tThis uses an alternative termination analysis based",
+% "\tconvex constraints.",
+% "--chk-term2, --check-termination2",
+% "\tEnable the alternative termination analysis, and emit warnings for",
+% "\tsome predicates or functions that cannot be proved to terminate. In",
+% "\tmany cases where the compiler is unable to prove termination",
+% "\tthe problem is either a lack of information about the",
+% "\ttermination properties of other predicates, or because language",
+% "\tconstructs (such as higher order calls) were used which could",
+% "\tnot be analysed. In these cases the compiler does not emit a",
+% "\twarning of non-termination, as it is likely to be spurious.",
+% "--verb-chk-term2, --verb-check-term2, --verbose-check-termination2",
+% "--termination2-norm {simple, total, num-data-elems}",
+% "\tTell the alternative termination analyser which norm to use.",
+% "\tSee the description of the `--termination-norm' option for a",
+% "\tdescription of the different types of norm available."
+% "--term2-widening-limit <n>, --termination2-widening-limit <n>",
+% "\tSet the threshold for the number of iterations after which the",
+% "\targument size analyser invokes widening.",
+% "--term2-propagate-failure-constrs, --termination2-propagate-failure-constraints",
+% "\tMake the argument analyser infer information about the sizes of any"
+% "\tinputs to a goal in contexts where that goal fails."
+% "--term2-max-matrix-size <n>, --termination2-maximum-matrix-size <n>",
+% "\tLimit the sizes of constraints systems in the analyser to <n>",
+% "\tconstraints. Use approximations of some constraint operations,",
+% "\tsuch as projection, if this threshold is exceeded. This will",
+% "\tspeed up the analysis at the cost of reduced precision.",
+
+% This option is for developers only.
+% It is useful for benchmarking the argument size analysis.
+% "--term2-argument-size-analysis-only, --term2-arg-size-analysis-only",
+% "\tPerform argument size analysis on each SCC but do not",
+% "\tattempt to infer termination,"
+ ]).
:- pred options_help_compilation_model(io::di, io::uo) is det.
Index: compiler/polyhedron.m
===================================================================
RCS file: compiler/polyhedron.m
diff -N compiler/polyhedron.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/polyhedron.m 23 Mar 2005 22:47:06 -0000
@@ -0,0 +1,628 @@
+%------------------------------------------------------------------------------%
+% Copyright (C) 2003 The University of Melbourne.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%------------------------------------------------------------------------------%
+%
+% file: polyhedron.m
+% main author: juliensf
+
+% Provides closed convex polyhedra over Q^n.
+% These are useful as an abstract domain for describing numerical
+% relational information.
+
+% The set of closed convex polyhedra is partially ordered by subset
+% inclusion. It forms a lattice with intersection as the binary meet
+% operation and convex hull as the binary join operation.
+
+% This module includes procedures for:
+% - computing the intersection of two convex polyhedra
+% - computing the convex hull of two convex polyhedra
+% - approximating the convex union of two convex polyhedra by means
+% other than the convex hull when that becomes too computationally
+% expensive.
+% - converting a convex polyhedron to and from an equivalent system
+% of linear constraints.
+
+% It also includes an implementation of widening for convex polyhedra.
+
+% NOTE: many of the operations in this module require you to pass in
+% the varset that the variables in the constraints that define the polyhedron
+% were allocated from. This because the code for computing the convex hull
+% and the linear solver in lp_rational.m need to allocate fresh temporary
+% variables.
+%
+% XXX We could avoid this with some extra work.
+
+% TODO:
+% * See if using the double description method is any faster.
+
+%------------------------------------------------------------------------------%
+
+:- module libs.polyhedron.
+
+:- interface.
+
+:- import_module libs.lp_rational.
+
+:- import_module io.
+:- import_module list.
+:- import_module map.
+:- import_module set.
+:- import_module std_util.
+
+%------------------------------------------------------------------------------%
+
+:- type polyhedron.
+
+:- type polyhedra == list(polyhedron).
+
+%------------------------------------------------------------------------------%
+
+ % The `empty' polyhedron. Equivalent to the constraint `false'.
+ %
+:- func polyhedron.empty = polyhedron.
+
+ % Identity polyhedron with respect to intersection and convex union.
+ %
+ % e.g. P /\ identity = P
+ % P \/ identity = P (where \/ is the convex union)
+ %
+ % This is useful as an initial value when folding over a list of
+ % polyhedra.
+ %
+:- func polyhedron.identity = polyhedron.
+
+ % Constructs a convex polyhedron from a system of linear constraints.
+ %
+:- func polyhedron.from_constraints(constraints) = polyhedron.
+
+ % Returns a system of constraints whose solution space defines
+ % the given polyhedron.
+ %
+:- func polyhedron.constraints(polyhedron) = constraints.
+
+ % As above but throws an exception if the given polyhedron is empty.
+ %
+:- func polyhedron.non_false_constraints(polyhedron) = constraints.
+
+ % Succeeds iff the given polyhedron is the empty polyhedron.
+ %
+ % NOTE: this only succeeds if the polyhedron is actually *known*
+ % to be empty. It might fail even when the constraint set is
+ % is inconsistent. You currently need to call polyhedron.optimize
+ % to force this to always work.
+ %
+:- pred polyhedron.is_empty(polyhedron::in) is semidet.
+
+ % Succeeds iff the given polyhedron is the `universe' polyhedron,
+ % that is the one whose constraint representation corresponds to `true'.
+ % (ie. it is unbounded in all dimensions).
+ %
+:- pred polyhedron.is_universe(polyhedron::in) is semidet.
+
+ % Optimizes the representation of a polyhedron.
+ % At the moment this performs a consistency check and then
+ % replaces the polyhedron by empty if necessary.
+ %
+:- pred polyhedron.optimize(lp_varset::in, polyhedron::in, polyhedron::out)
+ is det.
+
+ % polyhedron.intersection(A, B, C).
+ % The polyhedron `C' is the intersection of the the
+ % polyhedra `A' and `B'.
+ %
+:- func polyhedron.intersection(polyhedron, polyhedron) = polyhedron.
+:- pred polyhedron.intersection(polyhedron::in, polyhedron::in,
+ polyhedron::out) is det.
+
+ % Returns a polyhedron that is a closed convex approximation of
+ % union of the two polyhedra.
+ %
+:- func polyhedron.convex_union(lp_varset, polyhedron, polyhedron) =
+ polyhedron.
+:- pred polyhedron.convex_union(lp_varset::in, polyhedron::in, polyhedron::in,
+ polyhedron::out) is det.
+
+ % As above but takes an extra argument that weakens the approximation
+ % even further if the size of the internal matrices exceeds the
+ % supplied threshold
+ %
+:- func polyhedron.convex_union(lp_varset, maybe(int), polyhedron,
+ polyhedron) = polyhedron.
+:- pred polyhedron.convex_union(lp_varset::in, maybe(int)::in, polyhedron::in,
+ polyhedron::in, polyhedron::out) is det.
+
+ % Approximate a (convex) polyhedron by a rectangular region
+ % whose sides are parallel to the axes.
+ %
+:- func polyhedron.bounding_box(polyhedron, lp_varset) = polyhedron.
+
+ % polyhedron.widen(A, B, Varset) = C.
+ % Remove faces from the polyhedron `A' to form the polyhedron `C'
+ % according to the rules that the smallest number of faces
+ % should be removed and that `C' must be a superset of `B'.
+ % This operation is not commutative.
+ %
+:- func polyhedron.widen(polyhedron, polyhedron, lp_varset) = polyhedron.
+
+ % project_all(Varset, Variables, Polyhedra) returns a list
+ % of polyhedra in which the variables listed have been eliminated
+ % from each polyhedron.
+ %
+:- func polyhedron.project_all(lp_varset, lp_vars, polyhedra) = polyhedra.
+
+:- func polyhedron.project(lp_vars, lp_varset, polyhedron) = polyhedron.
+:- pred polyhedron.project(lp_vars::in, lp_varset::in, polyhedron::in,
+ polyhedron::out) is det.
+
+ % XXX It might be nicer to think of this as relabelling the axes.
+ % Conceptually it alters the names of the variables in the polyhedron
+ % without explicitly converting it back into constraint form - this
+ % is easy to do (at the moment) as the polyhedra are represented
+ % as constraints anyway.
+ %
+:- func polyhedron.substitute_vars(lp_vars, lp_vars, polyhedron) = polyhedron.
+:- func polyhedron.substitute_vars(map(lp_var, lp_var), polyhedron) =
+ polyhedron.
+
+ % polyhedron.zero_vars(Set, Polyhedron0) = Polyhedron <=>
+ %
+ % Constraints0 = polyhedron.constraints(Polyhedron0),
+ % Constraints = lp_rational.set_vars_to_zero(
+ % Set, Constraints0)
+ % Polyhedron = polyhedron.from_constraints(Constraints)
+ %
+ % This is a little more efficient than the above because
+ % we don't end up traversing the list of constraints as much.
+ %
+:- func polyhedron.zero_vars(set(lp_var), polyhedron) = polyhedron.
+
+ % Print out the polyhedron using the names of the variables in the
+ % varset.
+ %
+:- pred polyhedron.write_polyhedron(polyhedron::in, lp_varset::in, io::di,
+ io::uo) is det.
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module libs.lp_rational.
+:- import_module libs.rat.
+
+:- import_module bool.
+:- import_module exception.
+:- import_module int.
+:- import_module string.
+:- import_module svmap.
+:- import_module svvarset.
+:- import_module varset.
+
+%------------------------------------------------------------------------------%
+
+ % XXX The constructor eqns/1 should really be called something
+ % more meaningful.
+ %
+:- type polyhedron
+ ---> eqns(constraints)
+ ; empty_poly.
+
+%------------------------------------------------------------------------------%
+%
+% Creation of polyhedra.
+%
+
+polyhedron.empty = empty_poly.
+
+polyhedron.identity = eqns([]).
+
+ % This does the following:
+ % - checks if the constraint is false.
+ % - simplifies the representation of the constraint.
+ % - calls intersection/3 (which does further simplifications).
+ %
+polyhedron.from_constraints([]) = eqns([]).
+polyhedron.from_constraints([C | Cs]) = Polyhedron :-
+ ( lp_rational.is_false(C) ->
+ Polyhedron = empty
+ ;
+ Polyhedron0 = polyhedron.from_constraints(Cs),
+ Polyhedron = polyhedron.intersection(eqns([C]), Polyhedron0)
+ ).
+
+polyhedron.constraints(eqns(Constraints)) = Constraints.
+polyhedron.constraints(empty_poly) = [lp_rational.false_constraint].
+
+polyhedron.non_false_constraints(eqns(Constraints)) = Constraints.
+polyhedron.non_false_constraints(empty_poly) =
+ throw("non_false_constraints/1: empty polyhedron.").
+
+polyhedron.is_empty(empty_poly).
+
+polyhedron.is_universe(eqns(Constraints)) :-
+ list.all_true(lp_rational.nonneg_constr, Constraints).
+
+polyhedron.optimize(_, empty_poly, empty_poly).
+polyhedron.optimize(Varset, eqns(Constraints0), Result) :-
+ Constraints = simplify_constraints(Constraints0),
+ ( inconsistent(Varset, Constraints) ->
+ Result = empty_poly
+ ;
+ Result = eqns(Constraints)
+ ).
+
+%------------------------------------------------------------------------------%
+%
+% Intersection
+%
+
+polyhedron.intersection(PolyA, PolyB, polyhedron.intersection(PolyA, PolyB)).
+
+polyhedron.intersection(empty_poly, _) = empty_poly.
+polyhedron.intersection(eqns(_), empty_poly) = empty_poly.
+polyhedron.intersection(eqns(MatrixA), eqns(MatrixB)) = eqns(Constraints) :-
+ Constraints0 = MatrixA ++ MatrixB,
+ restore_equalities(Constraints0, Constraints1),
+ Constraints = simplify_constraints(Constraints1).
+
+%------------------------------------------------------------------------------%
+%
+% Convex union.
+%
+% XXX At the moment this just calls convex_hull; it should actually back
+% out of the convex_hull calculation if it gets too expensive (we can
+% keep track of the size of the matrices during projection) and use a
+% bounding box approximation instead.
+%
+
+polyhedron.convex_union(Varset, PolyhedronA, PolyhedronB) = Polyhedron :-
+ convex_union(Varset, no, PolyhedronA, PolyhedronB, Polyhedron).
+
+polyhedron.convex_union(Varset, PolyhedronA, PolyhedronB, Polyhedron) :-
+ convex_union(Varset, no, PolyhedronA, PolyhedronB, Polyhedron).
+
+polyhedron.convex_union(Varset, MaxMatrixSize, PolyhedronA, PolyhedronB)
+ = Polyhedron :-
+ convex_union(Varset, MaxMatrixSize, PolyhedronA, PolyhedronB,
+ Polyhedron).
+
+polyhedron.convex_union(_, _, empty_poly, empty_poly, empty_poly).
+polyhedron.convex_union(_, _, eqns(Constraints), empty_poly, eqns(Constraints)).
+polyhedron.convex_union(_, _, empty_poly, eqns(Constraints), eqns(Constraints)).
+polyhedron.convex_union(Varset, MaybeMaxSize, eqns(ConstraintsA),
+ eqns(ConstraintsB), Hull) :-
+ convex_hull([ConstraintsA, ConstraintsB], Hull, MaybeMaxSize, Varset).
+
+%------------------------------------------------------------------------------%
+%
+% Convex hull calculation.
+%
+
+% The following transformation for computing the convex hull is described in
+% the paper:
+%
+% F. Benoy and A. King. Inferring Argument Size Relationships with CLPR(R).
+% Logic-based Program Synthesis and Transformation,
+% LNCS 1207: pp. 204-223, 1997.
+%
+% Further details can be found in:
+%
+% F. Benoy, A. King, and F. Mesnard.
+% Computing Convex Hulls with a Linear Solver
+% Theory and Practice of Logic Programming 5(1&2):259-271, 2005.
+
+:- type convex_hull_result
+ ---> ok(polyhedron)
+ ; aborted.
+
+:- type var_map == map(lp_var, lp_var).
+
+:- type var_maps == list(var_map).
+
+ % We introduce sigma variables into the constraints as
+ % part of the transformation (See the above papers for details).
+ %
+:- type sigma_var == lp_var.
+
+:- type sigma_vars == list(sigma_var).
+
+:- type polyhedra_info
+ ---> polyhedra_info(
+ var_maps :: var_maps,
+ % There is one of these for each polyhedron.
+ % It maps the original variables in the
+ % constraints to the temporary variables
+ % introduced by the the transformation.
+ % A variable that occurs in more than one
+ % polyhedron is mapped to a separate
+ % temporary variable for each one.
+
+ sigmas :: sigma_vars,
+ % The sigma variables introduced by the
+ % transformation.
+
+ poly_varset :: lp_varset
+ % The varset the variables are allocated.
+ % The temporary and sigma variables need
+ % to be allocated from this as well in order
+ % to prevent clashes when using the solver.
+ ).
+
+:- type constr_info
+ ---> constr_info(
+ var_map :: var_map,
+ % Map from original variables
+ % to new (temporary) ones.
+ % There is one of these for
+ % each constraint.
+
+ constr_varset :: lp_varset
+ ).
+
+:- pred convex_hull(list(constraints)::in, polyhedron::out, maybe(int)::in,
+ lp_varset::in) is det.
+
+convex_hull([], _, _, _) :- throw("convex_hull/4: empty list").
+convex_hull([Poly], eqns(Poly), _, _).
+convex_hull(Polys @ [_,_|_], ConvexHull, MaybeMaxSize, Varset0) :-
+ %
+ % Perform the matrix transformation from the paper
+ % by Benoy and King. Rename variables and add sigma
+ % constraints as necessary.
+ %
+ PolyInfo0 = polyhedra_info([], [], Varset0),
+ transform_polyhedra(Polys, Matrix0, PolyInfo0, PolyInfo),
+ PolyInfo = polyhedra_info(VarMaps, Sigmas, Varset),
+ add_sigma_constraints(Sigmas, Matrix0, Matrix1),
+ Matrix = add_last_constraints(Matrix1, VarMaps),
+ AppendValues = (func(Map, Varlist0) = Varlist :-
+ Varlist = Varlist0 ++ map.values(Map)
+ ),
+ VarsToEliminate = Sigmas ++ list.foldl(AppendValues, VarMaps, []),
+ %
+ % Calculate the closure of the convex hull of the original
+ % polyhedra by projecting the constraints in the transformed
+ % matrix onto the original variables (ie. eliminate all the
+ % sigma and temporary variables). Since the resulting matrix
+ % tends to contain a large number of redundant constraints,
+ % we need to do a redundancy check after this.
+ %
+ lp_rational.project(VarsToEliminate, Varset, MaybeMaxSize, Matrix,
+ ProjectionResult),
+ (
+ % XXX We should try using a bounding box first.
+ ProjectionResult = aborted,
+ ConvexHull = eqns(lp_rational.nonneg_box(VarsToEliminate, Matrix))
+ ;
+ ProjectionResult = inconsistent,
+ ConvexHull = empty_poly
+ ;
+ some [!Hull] (
+ ProjectionResult = ok(!:Hull),
+ restore_equalities(!Hull),
+ % XXX We should try removing this call to
+ % simplify constraints.
+ !:Hull = simplify_constraints(!.Hull),
+ ( remove_some_entailed_constraints(Varset, !Hull) ->
+ ConvexHull = eqns(!.Hull)
+ ;
+ ConvexHull = empty_poly
+ )
+ )
+ ).
+
+:- pred transform_polyhedra(list(constraints)::in, constraints::out,
+ polyhedra_info::in, polyhedra_info::out) is det.
+
+transform_polyhedra(Polys, Eqns, !PolyInfo) :-
+ list.foldl2(transform_polyhedron, Polys, [], Eqns, !PolyInfo).
+
+:- pred transform_polyhedron(constraints::in, constraints::in,
+ constraints::out, polyhedra_info::in, polyhedra_info::out) is det.
+
+transform_polyhedron(Poly, Polys0, Polys, !PolyInfo) :-
+ some [!Varset] (
+ !.PolyInfo = polyhedra_info(VarMaps, Sigmas, !:Varset),
+ svvarset.new_var(Sigma, !Varset),
+ list.map_foldl2(transform_constraint(Sigma), Poly, NewEqns,
+ map.init, VarMap, !Varset),
+ Polys = NewEqns ++ Polys0,
+ !:PolyInfo = polyhedra_info([VarMap | VarMaps],
+ [Sigma | Sigmas], !.Varset)
+ ).
+
+ % transform_constraint: takes a constraint (with original variables) and the
+ % sigma variable to add, and returns the constraint where the original
+ % variables are substituted for new ones and where the sigma variable
+ % is included. The map of old to new variables is updated if necessary.
+ %
+:- pred transform_constraint(lp_var::in, constraint::in, constraint::out,
+ var_map::in, var_map::out, lp_varset::in, lp_varset::out) is det.
+
+transform_constraint(Sigma, !Constraint, !VarMap, !Varset) :-
+ some [!Terms] (
+ constraint(!.Constraint, !:Terms, Op, Const),
+ list.map_foldl2(change_var, !Terms, !VarMap, !Varset),
+ list.cons( Sigma - (-Const), !Terms),
+ !:Constraint = constraint(!.Terms, Op, zero)
+ ).
+
+ % change_var: takes a Var-Num pair with an old variable and
+ % returns one with a new variable which the old variable maps
+ % to. Updates the map of old to new variables if necessary.
+ %
+:- pred change_var(lp_term::in, lp_term::out, var_map::in, var_map::out,
+ lp_varset::in, lp_varset::out) is det.
+
+change_var(!Term, !VarMap, !Varset) :-
+ some [!Var] (
+ !.Term = !:Var - Coefficient,
+ %
+ % Have we already mapped this original variable to a new one?
+ %
+ ( !:Var = !.VarMap ^ elem(!.Var) ->
+ true
+ ;
+ svvarset.new_var(NewVar, !Varset),
+ svmap.det_insert(!.Var, NewVar, !VarMap),
+ !:Var = NewVar
+ ),
+ !:Term = !.Var - Coefficient
+ ).
+
+:- pred add_sigma_constraints(sigma_vars::in,
+ constraints::in, constraints::out) is det.
+
+add_sigma_constraints(Sigmas, !Constraints) :-
+ %
+ % Add non-negativity constraints for each sigma variable.
+ %
+ SigmaConstraints = list.map(make_nonneg_constr, Sigmas),
+ list.append(SigmaConstraints, !Constraints),
+ %
+ % The sum of all the sigma variables is one.
+ %
+ SigmaTerms = list.map(lp_term, Sigmas),
+ list.cons(constraint(SigmaTerms, (=), one), !Constraints).
+
+ % Add a constraint specifying that each variable is the sum of the
+ % temporary variables to which it has been mapped.
+ %
+:- func add_last_constraints(constraints, var_maps) = constraints.
+
+add_last_constraints(!.Constraints, VarMaps) = !:Constraints :-
+ Keys = get_keys_from_maps(VarMaps),
+ NewLastConstraints = set.filter_map(make_last_constraint(VarMaps),
+ Keys),
+ list.append(set.to_sorted_list(NewLastConstraints), !Constraints).
+
+ % Return the set of keys in the given list of maps.
+ %
+:- func get_keys_from_maps(var_maps) = set(lp_var).
+
+get_keys_from_maps(Maps) = list.foldl(get_keys_from_map, Maps, set.init).
+
+:- func get_keys_from_map(var_map, set(lp_var)) = set(lp_var).
+
+get_keys_from_map(Map, KeySet) = set.insert_list(KeySet, map.keys(Map)).
+
+:- func make_last_constraint(var_maps, lp_var) = constraint is semidet.
+
+make_last_constraint(VarMaps, OriginalVar) = Constraint :-
+ list.foldl(make_last_terms(OriginalVar), VarMaps, [], LastTerms),
+ Constraint = constraint([OriginalVar - one | LastTerms], (=), zero).
+
+:- pred make_last_terms(lp_var::in, var_map::in, lp_terms::in, lp_terms::out)
+ is semidet.
+
+make_last_terms(OriginalVar, VarMap, !Terms) :-
+ NewVar = VarMap ^ elem(OriginalVar),
+ list.cons(NewVar - (-one), !Terms).
+
+%------------------------------------------------------------------------------%
+%
+% Approximation of polyhedron by a bounding box.
+%
+
+polyhedron.bounding_box(empty_poly, _) = empty_poly.
+polyhedron.bounding_box(eqns(Constraints), Varset) =
+ eqns(lp_rational.bounding_box(Varset, Constraints)).
+
+%------------------------------------------------------------------------------%
+%
+% Widening
+%
+
+polyhedron.widen(empty_poly, empty_poly, _) = empty_poly.
+polyhedron.widen(eqns(_), empty_poly, _) = throw("widen/2: empty polyhedron").
+polyhedron.widen(empty_poly, eqns(_), _) = throw("widen/2: empty polyhedron").
+polyhedron.widen(eqns(Poly1), eqns(Poly2), Varset) = eqns(WidenedEqns) :-
+ WidenedEqns = list.filter(entailed(Varset, Poly2), Poly1).
+
+%------------------------------------------------------------------------------%
+%
+% Projection.
+%
+
+polyhedron.project_all(Varset, Locals, Polyhedra) =
+ list.map((func(Poly0) = Poly :-
+ (
+ Poly0 = eqns(Constraints0),
+ lp_rational.project(Locals, Varset, Constraints0,
+ ProjectionResult),
+ (
+ ProjectionResult = aborted,
+ throw("project_all/4: abort from project.")
+ ;
+ ProjectionResult = inconsistent,
+ Poly = empty_poly
+ ;
+ ProjectionResult = ok(Constraints1),
+ restore_equalities(Constraints1, Constraints),
+ Poly = eqns(Constraints)
+ )
+ ;
+ Poly0 = empty_poly,
+ Poly = empty_poly
+ )
+ ), Polyhedra).
+
+polyhedron.project(Vars, Varset, Polyhedron0) = Polyhedron :-
+ polyhedron.project(Vars, Varset, Polyhedron0, Polyhedron).
+
+polyhedron.project(_, _, empty_poly, empty_poly).
+polyhedron.project(Vars, Varset, eqns(Constraints0), Result) :-
+ lp_rational.project(Vars, Varset, Constraints0, ProjectionResult),
+ (
+ ProjectionResult = aborted,
+ throw("project/4: abort from project")
+ ;
+ ProjectionResult = inconsistent,
+ Result = empty_poly
+ ;
+ ProjectionResult = ok(Constraints1),
+ restore_equalities(Constraints1, Constraints),
+ Result = eqns(Constraints)
+ ).
+%------------------------------------------------------------------------------%
+%
+% Variable substitution.
+%
+
+polyhedron.substitute_vars(OldVars, NewVars, Polyhedron0) = Polyhedron :-
+ Constraints0 = polyhedron.non_false_constraints(Polyhedron0),
+ Constraints = lp_rational.substitute_vars(OldVars, NewVars,
+ Constraints0),
+ Polyhedron = polyhedron.from_constraints(Constraints).
+
+polyhedron.substitute_vars(SubstMap, Polyhedron0) = Polyhedron :-
+ Constraints0 = polyhedron.non_false_constraints(Polyhedron0),
+ Constraints = lp_rational.substitute_vars(SubstMap, Constraints0),
+ Polyhedron = polyhedron.from_constraints(Constraints).
+
+%------------------------------------------------------------------------------%
+%
+% Zeroing out variables.
+%
+
+polyhedron.zero_vars(_, empty_poly) = empty_poly.
+polyhedron.zero_vars(Vars, eqns(Constraints0)) = eqns(Constraints) :-
+ Constraints = lp_rational.set_vars_to_zero(Vars, Constraints0).
+
+%------------------------------------------------------------------------------%
+%
+% Printing.
+%
+
+polyhedron.write_polyhedron(empty_poly, _, !IO) :-
+ io.write_string("\tEmpty\n", !IO).
+polyhedron.write_polyhedron(eqns([]), _, !IO) :-
+ io.write_string("\tUniverse\n", !IO).
+polyhedron.write_polyhedron(eqns(Constraints @ [_|_]), Varset, !IO) :-
+ lp_rational.write_constraints(Constraints, Varset, !IO).
+
+%------------------------------------------------------------------------------%
+:- end_module libs.polyhedron.
+%------------------------------------------------------------------------------%
Index: compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.121
diff -u -r1.121 prog_data.m
--- compiler/prog_data.m 22 Mar 2005 06:40:18 -0000 1.121
+++ compiler/prog_data.m 24 Mar 2005 04:10:03 -0000
@@ -20,6 +20,8 @@
:- import_module libs__globals.
:- import_module libs__options.
+:- import_module libs__rat.
+
:- import_module mdbcomp__prim_data.
:- import_module recompilation.
@@ -495,6 +497,16 @@
% trans_opt files.
)
+ ; termination2_info(
+ pred_or_func,
+ sym_name,
+ list(mode),
+ list(int),
+ maybe(pragma_constr_arg_size_info),
+ maybe(pragma_constr_arg_size_info),
+ maybe(pragma_termination_info)
+ )
+
; terminates(
term_name :: sym_name,
term_arity :: arity
@@ -629,21 +641,38 @@
% There is no finite integer for which the
% above equation is true.
-:- type generic_termination_info(ErrorInfo)
- ---> cannot_loop % This procedure definitely terminates for all
- % possible inputs.
+:- type generic_termination_info(TermInfo, ErrorInfo)
+ ---> cannot_loop(TermInfo) % This procedure definitely terminates
+ % for all possible inputs.
; can_loop(ErrorInfo).
% This procedure might not terminate.
:- type pragma_arg_size_info == generic_arg_size_info(unit).
-:- type pragma_termination_info == generic_termination_info(unit).
+:- type pragma_termination_info == generic_termination_info(unit, unit).
+
+%
+% Stuff for the `termination2_info' pragma.
+%
+
+ % This is the form in which termination information from other
+ % modules (imported via `.opt' or `.trans_opt' files) comes.
+ % We convert this to an intermediate form and let the termination
+ % analyser convert it to the correct form.
+
+:- type arg_size_constr
+ ---> le(list(arg_size_term), rat)
+ ; eq(list(arg_size_term), rat).
+
+:- type arg_size_term == pair(int, rat).
+
+:- type pragma_constr_arg_size_info == list(arg_size_constr).
%
% Stuff for the `unused_args' pragma.
%
% This `mode_num' type is only used for mode numbers written out in
- % automatically-generateed `pragma unused_args' pragmas in `.opt'
+ % automatically-generated `pragma unused_args' pragmas in `.opt'
% files.
% The mode_num gets converted to an HLDS proc_id by make_hlds.m.
% We don't want to use the `proc_id' type here since the parse tree
@@ -666,7 +695,7 @@
; conditional.
% Whether the procedure will not throw an
% exception depends upon the value of one
- % or more polymorpyhic arguments.
+ % or more polymorphic arguments.
% XXX This needs to be extended for ho
% preds. (See exception_analysis.m for
% more details).
@@ -756,7 +785,7 @@
; import(
string, % Pragma imported C func name
string, % Code to handle return value
- string, % Comma seperated variables which
+ string, % Comma separated variables which
% the import function is called
% with.
Index: compiler/prog_io_pragma.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_pragma.m,v
retrieving revision 1.80
diff -u -r1.80 prog_io_pragma.m
--- compiler/prog_io_pragma.m 22 Mar 2005 06:40:19 -0000 1.80
+++ compiler/prog_io_pragma.m 22 Mar 2005 06:49:34 -0000
@@ -36,6 +36,8 @@
:- implementation.
:- import_module libs__globals.
+:- import_module libs__lp_rational.
+:- import_module libs__rat.
:- import_module parse_tree__prog_io.
:- import_module parse_tree__prog_io_goal.
:- import_module parse_tree__prog_util.
@@ -1113,7 +1115,7 @@
MaybeTerminationInfo = yes(can_loop(unit))
;
TerminationTerm = term__functor(term__atom("cannot_loop"), [], _),
- MaybeTerminationInfo = yes(cannot_loop)
+ MaybeTerminationInfo = yes(cannot_loop(unit))
),
Result0 = ok(pragma(termination_info(PredOrFunc, PredName,
ModeList, MaybeArgSizeInfo, MaybeTerminationInfo)))
@@ -1123,6 +1125,48 @@
Result = error("syntax error in `:- pragma termination_info' " ++
"declaration", ErrorTerm)
).
+
+parse_pragma_type(ModuleName, "termination2_info", PragmaTerms, ErrorTerm,
+ _VarSet, Result) :-
+ (
+ PragmaTerms = [
+ PredAndModesTerm0,
+ HeadVarListTerm,
+ SuccessArgSizeTerm,
+ FailureArgSizeTerm,
+ TerminationTerm
+ ],
+ parse_pred_or_func_and_arg_modes(yes(ModuleName), PredAndModesTerm0,
+ ErrorTerm, "`:- pragma termination2_info' declaration",
+ NameAndModesResult),
+ NameAndModesResult = ok(PredName - PredOrFunc, ModeList),
+ convert_int_list(HeadVarListTerm, HeadVarListResult),
+ HeadVarListResult = ok(HeadVars),
+ parse_arg_size_constraints(SuccessArgSizeTerm, SuccessArgSizeResult),
+ SuccessArgSizeResult = ok(SuccessArgSizeInfo),
+ parse_arg_size_constraints(FailureArgSizeTerm, FailureArgSizeResult),
+ FailureArgSizeResult = ok(FailureArgSizeInfo),
+ (
+ TerminationTerm = term__functor(term__atom("not_set"), [], _),
+ MaybeTerminationInfo = no
+ ;
+ TerminationTerm = term__functor(term__atom("can_loop"), [], _),
+ MaybeTerminationInfo = yes(can_loop(unit))
+ ;
+ TerminationTerm = term__functor(term__atom("cannot_loop"),
+ [], _),
+ MaybeTerminationInfo = yes(cannot_loop(unit))
+ ),
+ Result0 = ok(pragma(termination2_info(PredOrFunc, PredName,
+ ModeList, HeadVars, SuccessArgSizeInfo,
+ FailureArgSizeInfo, MaybeTerminationInfo)))
+ ->
+ Result = Result0
+ ;
+ Result = error(
+ "syntax error in `:- pragma termination2_info' declaration",
+ ErrorTerm)
+ ).
parse_pragma_type(ModuleName, "terminates", PragmaTerms, ErrorTerm, _VarSet,
Result) :-
@@ -1138,6 +1182,13 @@
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",
+ (pred(Name::in, Arity::in, Pragma::out) is det :-
+ Pragma = check_termination(Name, Arity)),
+ PragmaTerms, ErrorTerm, Result).
+
parse_pragma_type(ModuleName, "exceptions", PragmaTerms, ErrorTerm, _VarSet,
Result) :-
(
@@ -1187,13 +1238,6 @@
Result = error("error in `:- pragma exceptions'", ErrorTerm)
).
-parse_pragma_type(ModuleName, "check_termination", PragmaTerms, ErrorTerm,
- _VarSet, Result) :-
- parse_simple_pragma(ModuleName, "check_termination",
- (pred(Name::in, Arity::in, Pragma::out) is det :-
- Pragma = check_termination(Name, Arity)),
- PragmaTerms, ErrorTerm, Result).
-
% This parses a pragma that refers to a predicate or function.
%
:- pred parse_simple_pragma(module_name::in, string::in,
@@ -1717,6 +1761,7 @@
Result = error(ErrorMsg, Term)
).
+
:- pred convert_bool_list(term::in, list(bool)::out) is semidet.
convert_bool_list(ListTerm, Bools) :-
@@ -1780,3 +1825,64 @@
term__coerce_var(TypeVar0, TypeVar),
convert_type(SpecTypeTerm0, SpecType),
TypeSpec = TypeVar - SpecType.
+
+%------------------------------------------------------------------------------%%
+%
+% Parsing termination2_info pragmas.
+%
+
+:- pred parse_arg_size_constraints(term::in,
+ maybe1(maybe(list(arg_size_constr)))::out) is semidet.
+
+parse_arg_size_constraints(ArgSizeTerm, Result) :-
+ (
+ ArgSizeTerm = term__functor(term__atom("not_set"), [], _),
+ Result = ok(no)
+ ;
+ ArgSizeTerm = term__functor(term__atom("constraints"),
+ [Constraints0], _),
+ convert_list(Constraints0, parse_arg_size_constraint,
+ ConstraintsResult),
+ ConstraintsResult = ok(Constraints),
+ Result = ok(yes(Constraints))
+ ).
+
+:- pred parse_arg_size_constraint(term::in, arg_size_constr::out) is semidet.
+
+parse_arg_size_constraint(Term, Constr) :-
+ (
+ Term = term__functor(term__atom("le"),
+ [Terms, ConstantTerm], _),
+ convert_list(Terms, parse_lp_term, TermsResult),
+ TermsResult = ok(LPTerms),
+ parse_rational(ConstantTerm, Constant),
+ Constr = le(LPTerms, Constant)
+
+ ;
+ Term = term__functor(term__atom("eq"),
+ [Terms, ConstantTerm], _),
+ convert_list(Terms, parse_lp_term, TermsResult),
+ TermsResult = ok(LPTerms),
+ parse_rational(ConstantTerm, Constant),
+ Constr = eq(LPTerms, Constant)
+ ).
+
+:- pred parse_lp_term(term::in, pair(int, rat)::out) is semidet.
+
+parse_lp_term(Term, LpTerm) :-
+ Term = term__functor(term__atom("term"), [VarIdTerm, CoeffTerm], _),
+ VarIdTerm = term__functor(term__integer(VarId), [], _),
+ parse_rational(CoeffTerm, Coeff),
+ LpTerm = VarId - Coeff.
+
+:- pred parse_rational(term::in, rat::out) is semidet.
+
+parse_rational(Term, Rational) :-
+ Term = term__functor(term__atom("r"), [NumerTerm, DenomTerm], _),
+ NumerTerm = term__functor(term__integer(Numer), [], _),
+ DenomTerm = term__functor(term__integer(Denom), [], _),
+ Rational = rat__rat(Numer, Denom).
+
+%------------------------------------------------------------------------------%
+:- end_module prog_io_pragma.
+%------------------------------------------------------------------------------%
Index: compiler/rat.m
===================================================================
RCS file: compiler/rat.m
diff -N compiler/rat.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/rat.m 23 Mar 2005 00:08:49 -0000
@@ -0,0 +1,231 @@
+%-----------------------------------------------------------------------------%
+% Copyright (C) 1997-1998, 2003 The University of Melbourne.
+% This file may only be copied under the terms of the GNU Library General
+% Public License - see the file COPYING.LIB in the Mercury distribution.
+%-----------------------------------------------------------------------------%
+%
+% file: rat.m
+% authors: vjteag, juliensf
+%
+% Implements a rational number type using fixed precision integers.
+% The functionality here is limited to that which is used in the
+% lp_rational module.
+%
+% NOTE: if you actually want a general purpose rational number type then use
+% the rational module in the standard library. The stuff in this
+% module is pretty heavily geared towards a few specific tasks that
+% are part of the termination analysis.
+%
+% TODO:
+% - overflow checking would be nice
+%
+%-----------------------------------------------------------------------------%
+
+:- module libs.rat.
+
+:- interface.
+
+:- import_module int.
+:- import_module io.
+:- import_module string.
+
+%-----------------------------------------------------------------------------%
+
+:- type rat.
+
+:- pred '<'(rat::in, rat::in) is semidet.
+
+:- pred '>'(rat::in, rat::in) is semidet.
+
+:- pred '=<'(rat::in, rat::in) is semidet.
+
+:- pred '>='(rat::in, rat::in) is semidet.
+
+:- func rat.rat(int) = rat.
+
+:- func rat.rat(int, int) = rat.
+
+:- func '+'(rat) = rat.
+
+:- func '-'(rat) = rat.
+
+:- func rat + rat = rat.
+
+:- func rat - rat = rat.
+
+:- func rat * rat = rat.
+
+:- func rat / rat = rat.
+
+:- func rat.numer(rat) = int.
+
+:- func rat.denom(rat) = int.
+
+:- func rat.abs(rat) = rat.
+
+:- func rat.one = rat.
+
+:- func rat.zero = rat.
+
+ % Convert a rational to a string of the form: "(<Num>/<Denom>)".
+ %
+:- func rat.to_string(rat) = string.
+
+ % Write a rat in the form: r(<Numerator>, <Denominator>).
+ %
+:- pred rat.write_rat(rat::in, io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module exception.
+
+ % The normal form of a rat number has the following
+ % properties:
+ % - numerator and denominator have no common factors.
+ % - denominator is positive.
+ % - denominator is not zero.
+ % - if numerator is zero, then denominator is one.
+ %
+ % These invariants must be preserved by any rat number
+ % constructed using this module since the equality predicate
+ % on rats is simply Mercury's default unification
+ % predicate =/2. If the invariants were not maintained,
+ % we would have pathologies like r(-1,2) \= r(1,-2).
+ %
+ % The rat_norm/2 function generates rationals in this
+ % normal form.
+ %
+:- type rat ---> r(int, int).
+
+'<'(X, Y) :- cmp(X, Y) = (<).
+
+'>'(X, Y) :- cmp(X, Y) = (>).
+
+'=<'(X, Y) :-
+ Cmp = cmp(X, Y),
+ (Cmp = (<) ; Cmp = (=)).
+
+'>='(X, Y) :-
+ Cmp = cmp(X, Y),
+ (Cmp = (>) ; Cmp = (=)).
+
+rat.rat(Int) = rat_norm(Int, 1).
+
+rat.rat(Num, Den) = rat_norm(Num, Den).
+
+rat.one = r(1, 1).
+
+rat.zero = r(0, 1).
+
+'+'(Rat) = Rat.
+
+'-'(r(Num, Den)) = r(-Num, Den).
+
+r(An, Ad) + r(Bn, Bd) = rat_norm(Numer, M) :-
+ M = lcm(Ad, Bd),
+ CA = M // Ad,
+ CB = M // Bd,
+ Numer = An * CA + Bn * CB.
+
+X - Y = X + (-Y).
+
+ % XXX: need we call rat_norm here?
+r(An, Ad) * r(Bn, Bd) = rat_norm(Numer, Denom) :-
+ G1 = gcd(An, Bd),
+ G2 = gcd(Ad, Bn),
+ Numer = (An // G1) * (Bn // G2),
+ Denom = (Ad // G2) * (Bd // G1).
+
+X / Y = X * rat.reciprocal(Y).
+
+:- func rat.reciprocal(rat) = rat.
+
+reciprocal(r(Num, Den)) =
+ ( if Num = 0
+ then throw("rat.reciprocal/1: division by zero")
+ else r(signum(Num) * Den, int.abs(Num))
+ ).
+
+rat.numer(r(Num, _)) = Num.
+
+rat.denom(r(_, Den)) = Den.
+
+rat.abs(r(Num, Den)) = r(int.abs(Num), Den).
+
+:- func rat_norm(int, int) = rat.
+
+rat_norm(Num, Den) = Rat :-
+ ( Den = 0 -> throw("rat.rat_norm: division by zero")
+ ; Num = 0 -> Rat = r(0, 1)
+ ;
+ G = gcd(Num, Den),
+ Num2 = Num * signum(Den),
+ Den2 = int.abs(Den),
+ Rat = r(Num2 // G, Den2 // G)
+ ).
+
+:- func gcd(int, int) = int.
+
+gcd(A, B) = gcd_2(int.abs(A), int.abs(B)).
+
+:- func gcd_2(int, int) = int.
+
+gcd_2(A, B) = ( B = 0 -> A ; gcd_2(B, A rem B) ).
+
+:- func lcm(int, int) = int.
+
+lcm(A, B) =
+ ( A = 0 -> 0
+ ; B = 0 -> 0
+ ; int.abs((A // gcd(A, B)) * B)
+ ).
+
+:- func signum(int) = int.
+
+signum(N) = ( N = 0 -> 0 ; N < 0 -> -1 ; 1 ).
+
+ % Builtin comparison does not give a natural ordering
+ % on rats.
+:- func cmp(rat, rat) = comparison_result.
+
+cmp(X, Y) = Cmp :-
+ Diff = X - Y,
+ ( is_zero(Diff) -> Cmp = (=)
+ ; is_negative(Diff) -> Cmp = (<)
+ ; Cmp = (>)
+ ).
+
+:- pred is_zero(rat::in) is semidet.
+
+is_zero(r(0, _)).
+
+:- pred is_negative(rat::in) is semidet.
+
+is_negative(r(Num, _)) :- Num < 0.
+
+rat.to_string(r(Num, Denom)) =
+ ( Num = 0 ->
+ "0"
+ ;
+ "(" ++ string.int_to_string(Num) ++
+ ( Denom = 1 ->
+ ""
+ ;
+ "/" ++ string.int_to_string(Denom)
+ )
+ ++ ")"
+ ).
+
+write_rat(r(Numerator, Denominator), !IO) :-
+ io.write_string("r(", !IO),
+ io.write_int(Numerator, !IO),
+ io.write_string(", ", !IO),
+ io.write_int(Denominator, !IO),
+ io.write_char(')', !IO).
+
+%------------------------------------------------------------------------------%
+:- end_module libs.rat.
+%------------------------------------------------------------------------------%
Index: compiler/recompilation.version.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation.version.m,v
retrieving revision 1.14
diff -u -r1.14 recompilation.version.m
--- compiler/recompilation.version.m 22 Mar 2005 06:40:22 -0000 1.14
+++ compiler/recompilation.version.m 23 Mar 2005 23:24:44 -0000
@@ -626,7 +626,10 @@
is_pred_pragma(promise_semipure(Name, Arity), yes(no - Name / Arity)).
is_pred_pragma(termination_info(PredOrFunc, Name, Modes, _, _),
yes(yes(PredOrFunc) - Name / Arity)) :-
- adjust_func_arity(PredOrFunc, Arity, list__length(Modes)).
+ adjust_func_arity(PredOrFunc, Arity, list__length(Modes)).
+is_pred_pragma(termination2_info(PredOrFunc, Name, Modes, _, _, _, _),
+ yes(yes(PredOrFunc) - Name / Arity)) :-
+ adjust_func_arity(PredOrFunc, Arity, list__length(Modes)).
is_pred_pragma(terminates(Name, Arity), yes(no - Name / Arity)).
is_pred_pragma(does_not_terminate(Name, Arity), yes(no - Name / Arity)).
is_pred_pragma(check_termination(Name, Arity), yes(no - Name / Arity)).
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list