Tdiff: termination analysis (BIG!)
Christopher Rodd SPEIRS
crs at students.cs.mu.oz.au
Fri Apr 11 18:56:46 AEST 1997
Fergus,
Here is the termination analysis and transient optimization files.
I realise that this is still a work in progress, so various sections of code
still need to be improved. trans_opt.m still needs a lot of work, and the
error output in term_error.m also needs work.
in my copy of io.m, i have changed io__call_system/2 so that the
returned status is the return value of the process:
- Status = system(Command);
+ Status = system(Command) >> 8;
Unfortunatly the return value of the system command is not standard,
so this will not work on all systems. My question is, should i modify my
code so that it doesnt need this change to io.m, or should i add this change
to io.m, with the expectation that it will be improved later to use platform
independent code?
Chris
========= Log Message starts here =====
Add termination analysis to the compiler. The termination analysis annotates
each procinfo structure with termination information stating whether each
procedure is guaranteed to terminate.
Add intermodule transient optimization to the compiler. Transient
optimization information is stored in .trans_opt files. They are different
to .opt files as .trans_opt files can depend on other .trans_opt files.
doc/user_guide.texi:
Added documentation about new options added to control termination
analysis and transient optimization files.
compiler/dnf.m:
compiler/lambda.m:
Added an initialised termination structure to the call to
proc_info_create.
compiler/hlds_out.m:
Added code to output 'pragma terminates' and
'pragma check_termination'. Added code to output the
termination property of the procedure.
compiler/hlds_pred.m:
Added the check_termination and terminates pragmas to the marker
table. Also added termination to the proc_info structure, and
added predicates to access it. Added the proc_info_terminates/1
predicate, which succeeds if the procedure terminates.
compiler/make_hlds.m:
Added code to add the terminates, check_termination and
opt_terminates pragmas to the HLDS.
compiler/mercury_compile.m:
Added code to call trans_opt.m to make the transitive
optimization file, or read the transitive optimization file, as
required by the options. Also added code to call the termination
analysis.
compiler/mercury_to_mercury.m:
Added code to output the terminates, check_termination,
opt_terminates pragmas.
compiler/module_qual.m
Added code to qualify the terminates, check_termination,
opt_terminates pragmas.
compiler/modules.m:
Made sure that no warnings are emitted if terminates or
check_termination are defined in the interface.
compiler/options.m:
Added the following options:
make_transitive_opt_interface
transitive_optimization
termination
termination_single_args
compiler/prog_data.m:
Added the opt_terminates, terminates and check_termination
pragmas to the pragma_type type.
compiler/prog_io_pragma.m:
Added code to parse in the opt_terminates, terminates and
check_termination pragmas.
compiler/trans_opt.m:
Contains predicates for reading and writing transient_optimization
files.
compiler/termination.m:
The main module, that controls the termination analysis.
compiler/term_error.m:
This module contains code for printing out the error messages that
are created by termination analysis.
compiler/term_util.m:
Contains utilities used in the termination analysis. Also contains
type definitions of the types used in different parts of the
termination analysis.
compiler/term_pass1.m:
The first pass of the analysis. This pass associates a number with
each procedure. This number represents the relative sizes of input
and output variables.
compiler/term_pass2.m:
The second pass of the termination analysis. This uses the data from
pass1 to determine the termination property of each procedure.
Index: user_guide.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/user_guide.texi,v
retrieving revision 1.84
diff -u -r1.84 user_guide.texi
--- user_guide.texi 1997/03/27 03:29:44 1.84
+++ user_guide.texi 1997/04/09 12:20:17
@@ -1043,7 +1043,7 @@
@sp 1
@item -V
- at itemx --very_verbose
+ at itemx --very-verbose
Output very verbose progress messages.
@sp 1
@@ -1237,6 +1237,14 @@
The special argument value ``all''
will cause the printing of all these fields.
+ at sp 1
+ at itemx --make-transient-optimization-interface
+ at itemx --make-trans-opt
+Write the @file{@var{module}.trans_opt} file. This file is used to store
+information about the module that can be used for optimization. The
+file is transient as a @file{@var{module}.trans_opt} file may depend on other
+ at file{@var{module}.trans_opt} files.
+
@end table
@node Language semantics options
@@ -1542,6 +1550,27 @@
@item --intermodule-optimization
Perform inlining and higher-order specialization of the code for
predicates or functions imported from other modules.
+
+ at sp 1
+ at item --transient-intermodule-optimization
+ at item --trans-intermod-opt
+Use the information stored in the @file{@var{module}.trans_opt} file
+to make intermodule optimizations. The @file{@var{module}.trans_opt} is
+different to the @file{@var{module}.opt} as @file{@var{module}.trans_opt}
+files may depend on other @file{@var{module}.trans_opt} files.
+ at file{@var{module}.opt} files may only depend on the
+ at file{@var{module}.m} file.
+
+ at sp 1
+ at item --check-termination
+ at item --check-term
+ at item --term
+Enable termination analysis. Termination analysis analyses each mode of each
+predicate to see whether it terminates. @samp{pragma assert_terminates} and
+ at samp{pragma check_termination} pragmas have no effect unless termination
+analysis is enabled. When using termination,
+ at samp{--transient-intermodule-optimization} should be enabled, as it greatly
+improves the accuracy of the analysis.
@sp 1
@item --split-c-files
Index: dnf.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/dnf.m,v
retrieving revision 1.18
diff -u -r1.18 dnf.m
--- dnf.m 1997/04/07 05:39:15 1.18
+++ dnf.m 1997/04/07 05:54:27
@@ -60,6 +60,7 @@
:- import_module hlds_goal, hlds_data, prog_data, instmap.
:- import_module excess, make_hlds, mode_util.
:- import_module require, map, list, string, int, bool, std_util.
+:- import_module termination, term_util.
% Traverse the module structure.
@@ -388,8 +389,9 @@
module_info_name(ModuleInfo0, ModuleName),
SymName = qualified(ModuleName, PredName),
map__init(TVarMap), % later, polymorphism.m will fill this in.
+ termination__init(Termination),
proc_info_create(VarSet, VarTypes, ArgVars, ArgModes, Detism,
- Goal0, Context, TVarMap, ProcInfo),
+ Goal0, Context, TVarMap, Termination, ProcInfo),
pred_info_create(ModuleName, SymName, TVarSet, ArgTypes, true,
Context, local, Markers, predicate, ProcInfo, ProcId, PredInfo),
Index: hlds_out.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_out.m,v
retrieving revision 1.158
diff -u -r1.158 hlds_out.m
--- hlds_out.m 1997/03/06 05:09:05 1.158
+++ hlds_out.m 1997/04/04 08:43:19
@@ -165,6 +165,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_util.
+
hlds_out__write_type_id(Name - Arity) -->
prog_out__write_sym_name(Name),
@@ -503,6 +505,10 @@
io__write_string("obsolete").
hlds_out__write_marker(memo) -->
io__write_string("memo").
+hlds_out__write_marker(terminates) -->
+ io__write_string("terminates").
+hlds_out__write_marker(check_termination) -->
+ io__write_string("check_termination").
hlds_out__write_clauses(Indent, ModuleInfo, PredId, VarSet, AppendVarnums,
HeadVars, PredOrFunc, Clauses0, TypeQual) -->
@@ -1741,6 +1747,7 @@
{ proc_info_argmodes(Proc, HeadModes) },
{ proc_info_goal(Proc, Goal) },
{ proc_info_context(Proc, ModeContext) },
+ { proc_info_termination(Proc, Termination) },
{ Indent1 is Indent + 1 },
hlds_out__write_indent(Indent1),
@@ -1752,6 +1759,15 @@
io__write_string(" ("),
hlds_out__write_determinism(InferredDeterminism),
io__write_string("):\n"),
+ hlds_out__write_indent(Indent),
+
+ io__write_string("% Inferred Termination:"),
+ termination__out(Termination),
+ io__nl,
+ io__write_string("% Termination - UsedArgs:"),
+ termination__out_used_args(Termination),
+ io__nl,
+ termination__maybe_output_error(ModuleInfo, Termination),
hlds_out__write_var_types(Indent, VarSet, AppendVarnums,
VarTypes, TVarSet),
Index: hlds_pred.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_pred.m,v
retrieving revision 1.28
diff -u -r1.28 hlds_pred.m
--- hlds_pred.m 1997/04/07 05:39:27 1.28
+++ hlds_pred.m 1997/04/07 05:54:38
@@ -15,6 +15,7 @@
:- import_module hlds_data, hlds_goal, hlds_module, prog_data, instmap.
:- import_module bool, list, map, std_util, varset.
+:- import_module termination, term_util.
:- implementation.
@@ -203,9 +204,22 @@
; 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).
+ ; 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.
+ ; 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)
@@ -569,13 +583,14 @@
:- 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).
-:- mode proc_info_create(in, in, in, in, in, in, in, in, out) is det.
+ determinism, hlds_goal, term__context, map(tvar, var), termination,
+ proc_info).
+:- mode proc_info_create(in, in, in, in, in, in, in, in, in, out) is det.
:- pred proc_info_set_body(proc_info, varset, map(var, type), list(var),
hlds_goal, proc_info).
@@ -672,6 +687,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.
@@ -728,8 +749,11 @@
% should be passed.
liveness_info, % the initial liveness,
% for code generation
- map(tvar, var) % typeinfo vars for
+ map(tvar, var), % typeinfo vars for
% type parameters
+ termination % the termination properties of the
+ % procedure. initially 'not_set'
+ % inferred by termination.m
).
@@ -753,35 +777,36 @@
ClauseBody = conj([]) - GoalInfo,
CanProcess = yes,
map__init(TVarsMap),
+ termination__init(Termination),
NewProc = procedure(
MaybeDet, BodyVarSet, BodyTypes, HeadVars, Modes, MaybeArgLives,
ClauseBody, MContext, StackSlots, InferredDet, CanProcess,
- ArgInfo, InitialLiveness, TVarsMap
+ ArgInfo, InitialLiveness, TVarsMap, Termination
).
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).
+ CanProcess, ArgInfo, Liveness, TVarMap, Termination).
proc_info_create(VarSet, VarTypes, HeadVars, HeadModes, Detism, Goal,
- Context, TVarMap, ProcInfo) :-
+ Context, TVarMap, Termination, ProcInfo) :-
map__init(StackSlots),
set__init(Liveness),
MaybeHeadLives = no,
ProcInfo = procedure(yes(Detism), VarSet, VarTypes, HeadVars, HeadModes,
MaybeHeadLives, Goal, Context, StackSlots, Detism, yes, [],
- Liveness, TVarMap).
+ Liveness, TVarMap, Termination).
proc_info_set_body(ProcInfo0, VarSet, VarTypes, HeadVars, Goal, ProcInfo) :-
ProcInfo0 = procedure(A, _, _, _, E, F, _,
- H, I, J, K, L, M, N),
+ H, I, J, K, L, M, N, O),
ProcInfo = procedure(A, VarSet, VarTypes, HeadVars, E, F, Goal,
- H, I, J, K, L, M, N).
+ H, I, J, K, L, M, N, O).
proc_info_interface_determinism(ProcInfo, Determinism) :-
proc_info_declared_determinism(ProcInfo, MaybeDeterminism),
@@ -835,33 +860,36 @@
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, Terminat) :-
+ ProcInfo = procedure(_, _, _, _, _, _, _, _, _, _, _, _, _, _, Terminat).
+
% :- type proc_info ---> procedure(
% A maybe(determinism),% _declared_ detism
@@ -884,59 +912,64 @@
% M liveness_info % the initial liveness
% N map(tvar, var) % typeinfo vars to
% % vars.
+% O termination % Termination analys
% ).
proc_info_set_varset(ProcInfo0, VarSet, ProcInfo) :-
- ProcInfo0 = procedure(A, _, C, D, E, F, G, H, I, J, K, L, M, N),
- ProcInfo = procedure(A, VarSet, C, D, E, F, G, H, I, J, K, L, M, N).
+ 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).
proc_info_set_variables(ProcInfo0, Vars, ProcInfo) :-
- ProcInfo0 = procedure(A, _, C, D, E, F, G, H, I, J, K, L, M, N),
- ProcInfo = procedure(A, Vars, C, D, E, F, G, H, I, J, K, L, M, N).
+ 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).
proc_info_set_vartypes(ProcInfo0, Vars, ProcInfo) :-
- ProcInfo0 = procedure(A, B, _, D, E, F, G, H, I, J, K, L, M, N),
- ProcInfo = procedure(A, B, Vars, D, E, F, G, H, I, J, K, L, M, N).
+ 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).
proc_info_set_headvars(ProcInfo0, HeadVars, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, _, E, F, G, H, I, J, K, L, M, N),
- ProcInfo = procedure(A, B, C, HeadVars, E, F, G, H, I, J, K, L, M, N).
+ 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_argmodes(ProcInfo0, ArgModes, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, _, F, G, H, I, J, K, L, M, N),
- ProcInfo = procedure(A, B, C, D, ArgModes, F, G, H, I, J, K, L, M, N).
+ 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).
proc_info_set_maybe_arglives(ProcInfo0, ArgLives, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, _, G, H, I, J, K, L, M, N),
- ProcInfo = procedure(A, B, C, D, E, ArgLives, G, H, I, J, K, L, M, N).
+ 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).
proc_info_set_inferred_determinism(ProcInfo0, Detism, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, _, K, L, M, N),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I, Detism, K, L, M, N).
+ 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).
proc_info_set_can_process(ProcInfo0, CanProcess, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, _, L, M, N),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, CanProcess, L, M, N).
+ 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).
proc_info_set_goal(ProcInfo0, Goal, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, _, H, I, J, K, L, M, N),
- ProcInfo = procedure(A, B, C, D, E, F, Goal, H, I, J, K, L, M, N).
+ 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).
proc_info_set_stack_slots(ProcInfo0, StackSlots, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, _, J, K, L, M, N),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, StackSlots, J, K, L, M, N).
+ 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).
proc_info_set_arg_info(ProcInfo0, ArgInfo, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, _, M, N),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, ArgInfo, M, N).
+ 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).
proc_info_set_liveness_info(ProcInfo0, Liveness, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, _, N),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L, Liveness, N).
+ 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).
proc_info_set_typeinfo_varmap(ProcInfo0, TVarMap, ProcInfo) :-
- ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, _),
- ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, TVarMap).
+ 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).
+
+proc_info_set_termination(ProcInfo0, Terminat, ProcInfo) :-
+ ProcInfo0 = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, _),
+ ProcInfo = procedure(A, B, C, D, E, F, G, H, I, J, K, L, M, N, Terminat).
proc_info_get_used_typeinfos_setwise(ProcInfo, Vars, TypeInfoVars) :-
set__to_sorted_list(Vars, VarList),
Index: lambda.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/lambda.m,v
retrieving revision 1.25
diff -u -r1.25 lambda.m
--- lambda.m 1997/04/07 05:39:31 1.25
+++ lambda.m 1997/04/07 05:54:43
@@ -55,6 +55,7 @@
:- import_module hlds_goal, hlds_data, make_hlds.
:- import_module prog_util, mode_util, inst_match, llds.
+:- import_module termination, term_util.
:- import_module bool, string, std_util, require.
@@ -335,12 +336,13 @@
PermutedArgVars, PermutedArgModes),
map__apply_to_list(PermutedArgVars, VarTypes, ArgTypes),
+ termination__init(Termination),
% Now construct the proc_info and pred_info for the new
% single-mode predicate, using the information computed above
proc_info_create(VarSet, VarTypes, PermutedArgVars,
PermutedArgModes, Detism, LambdaGoal, LambdaContext,
- TVarMap, ProcInfo),
+ TVarMap, Termination, ProcInfo),
pred_info_create(ModuleName, PredName, TVarSet, ArgTypes,
true, LambdaContext, local, [], PredOrFunc, ProcInfo,
Index: make_hlds.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/make_hlds.m,v
retrieving revision 1.226
diff -u -r1.226 make_hlds.m
--- make_hlds.m 1997/04/07 05:39:34 1.226
+++ make_hlds.m 1997/04/09 13:03:20
@@ -59,7 +59,7 @@
:- import_module make_tags, quantification, shapes.
:- 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.
@@ -336,7 +336,8 @@
Arity, ProcId, UnusedArgs) },
( { Status \= 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) },
@@ -362,8 +363,91 @@
% clauses).
{ Pragma = fact_table(_, _, _) },
{ Module = Module0 }
+ ;
+ { Pragma = opt_terminates(PredOrFunc, SymName, Arity, ProcId,
+ Termination) },
+ % for the Status to be opt_imported, the pragma must be in
+ % a .trans_opt or .opt file. Currently
+ % :- pragma opt_terminates are only valid in .opt or
+ % .trans_opt files.
+ ( { Status \= opt_imported } ->
+ prog_out__write_context(Context),
+ io__write_string(
+ "Error: unknown pragma opt_terminates.\n"),
+ { module_info_incr_errors(Module0, Module) }
+ ;
+ { module_info_get_predicate_table(Module0, Preds) },
+ (
+ { predicate_table_search_pf_sym_arity(Preds,
+ PredOrFunc, SymName, Arity, PredIds) }
+ ->
+ ( { PredIds = [] } ->
+ prog_out__write_context(Context),
+ io__write_string("Internal Error: Predicate name not found in pragma opt_terminates\n"),
+ { module_info_incr_errors(Module0, Module) }
+ ; { PredIds = [PredId] } ->
+ { module_info_pred_proc_info(Module0, PredId,
+ ProcId, PredInfo0, ProcInfo0) },
+ { pred_info_procedures(PredInfo0, ProcTable0)},
+ { proc_info_set_termination(ProcInfo0,
+ Termination, ProcInfo) },
+ { map__det_update(ProcTable0, ProcId, ProcInfo,
+ ProcTable) },
+ { pred_info_set_procedures(PredInfo0,
+ ProcTable, PredInfo) },
+ { module_info_set_pred_info(Module0, PredId,
+ PredInfo, Module) }
+ ;
+ prog_out__write_context(Context),
+ io__write_string("Internal Error: Ambiguous predicate name\n"),
+ prog_out__write_context(Context),
+ io__write_string(
+ " in pragma opt_terminates\n"),
+ { module_info_incr_errors(Module0, Module) }
+ )
+ ;
+ prog_out__write_context(Context),
+ io__write_string("Internal Error: Predicate name not found\n"),
+ prog_out__write_context(Context),
+ io__write_string(" in pragma opt_terminates\n"),
+ { module_info_incr_errors(Module0, Module) }
+ )
+ )
+
+ ;
+ { Pragma = terminates(Name, Arity) },
+ get_pred_marker_list(Module0, Name, Arity, Context,
+ Markers, Module1),
+ ( { list__member(request(check_termination), Markers) } ->
+ % both pragma terminates and pragma check_termination
+ % have been defined on the one pred or func.
+ % emit a warning message.
+ terminates_and_check_termination_warning(Name,
+ Arity, Context)
+ ;
+ []
+ ),
+ add_pred_marker(Module1, "terminates", Name, Arity, Context,
+ [request(terminates)], Module)
+ ;
+ { Pragma = check_termination(Name, Arity) },
+ get_pred_marker_list(Module0, Name, Arity, Context,
+ Markers, Module1),
+ ( { list__member(request(terminates), Markers) } ->
+ % both pragma terminates and pragma check_termination
+ % have been defined on the one pred or func.
+ % emit a warning message.
+ terminates_and_check_termination_warning(Name,
+ Arity, Context)
+ ;
+ []
+ ),
+ add_pred_marker(Module1, "check_termination", Name, Arity,
+ Context, [request(check_termination)], Module)
).
+
+
add_item_decl_pass_2(func(_VarSet, FuncName, TypesAndModes, _RetTypeAndMode,
_MaybeDet, _Cond), _Context, Status, Module0, Status, Module)
-->
@@ -531,6 +615,29 @@
{ module_info_incr_errors(Module0, Module) }
).
+% This predicate gets all of the markers associated with a particular sym_name
+% and arity. It is used to check whether check_termination and termination
+% pragmas have been declared on the one predicate.
+:- pred get_pred_marker_list(module_info, sym_name, arity, term__context,
+ list(marker_status), module_info, io__state, io__state).
+:- mode get_pred_marker_list(in, in, in, in, out, out, di, uo) is det.
+get_pred_marker_list(Module0, Name, Arity, Context, Markers, Module) -->
+ { module_info_get_predicate_table(Module0, PredTable) },
+ (
+ { predicate_table_search_sym_arity(PredTable, Name,
+ Arity, PredIds) }
+ ->
+ { predicate_table_get_preds(PredTable, Preds) },
+ { pragma_get_markers(Preds, PredIds, Markers) },
+ { Module0 = Module }
+ ;
+ undefined_pred_or_func_error(Name, Arity, Context,
+ "Predicate not declared"),
+ { module_info_incr_errors(Module0, Module) },
+ { Markers = [] }
+ ).
+
+
%-----------------------------------------------------------------------------%
:- pred module_mark_as_external(sym_name, int, term__context,
@@ -1745,23 +1852,39 @@
pragma_set_markers(PredTable0, [PredId | PredIds], Markers, PredTable) :-
map__lookup(PredTable0, PredId, PredInfo0),
pred_info_get_marker_list(PredInfo0, MarkerList0),
- pragma_set_markers_2(Markers, MarkerList0, MarkerList),
+ pragma_append_markers_remove_dups(Markers, MarkerList0, MarkerList),
pred_info_set_marker_list(PredInfo0, MarkerList, PredInfo),
map__det_update(PredTable0, PredId, PredInfo, PredTable1),
pragma_set_markers(PredTable1, PredIds, Markers, PredTable).
-:- pred pragma_set_markers_2(list(marker_status), list(marker_status),
- list(marker_status)).
-:- mode pragma_set_markers_2(in, in, out) is det.
+% this is quite an inefficient algorithm, but it should be irrelevant
+% as both the pred_id and marker_status lists should be short.
+:- pred pragma_get_markers(pred_table, list(pred_id), list(marker_status)).
+:- mode pragma_get_markers(in, in, out) is det.
+pragma_get_markers(_PredTable, [], []).
+pragma_get_markers(PredTable, [PredId | PredIds], Markers) :-
+ map__lookup(PredTable, PredId, PredInfo),
+ pred_info_get_marker_list(PredInfo, MarkerList),
+ pragma_append_markers_remove_dups(MarkerList, MarkerList1, Markers),
+ pragma_get_markers(PredTable, PredIds, MarkerList1).
+
+
+
+
+
+% this is really a 'list__append_and_remove_dups' predicate
+:- pred pragma_append_markers_remove_dups(list(marker_status)
+ , list(marker_status), list(marker_status)).
+:- mode pragma_append_markers_remove_dups(in, in, out) is det.
-pragma_set_markers_2([], MarkerList, MarkerList).
-pragma_set_markers_2([Marker | Markers], MarkerList0, MarkerList) :-
+pragma_append_markers_remove_dups([], MarkerList, MarkerList).
+pragma_append_markers_remove_dups([Marker | Markers],MarkerList0,MarkerList) :-
( list__member(Marker, MarkerList0) ->
MarkerList1 = MarkerList0
;
MarkerList1 = [Marker | MarkerList0]
),
- pragma_set_markers_2(Markers, MarkerList1, MarkerList).
+ pragma_append_markers_remove_dups(Markers,MarkerList1,MarkerList).
%---------------------------------------------------------------------------%
@@ -3253,6 +3376,21 @@
io__write_string("'.\n"),
prog_out__write_context(Context),
io__write_string(" should have been qualified by prog_io.m.\n").
+
+
+
+:- pred terminates_and_check_termination_warning(sym_name, int, term__context
+ , io__state, io__state).
+:- mode terminates_and_check_termination_warning(in, in, in, di, uo) is det.
+terminates_and_check_termination_warning(Name, Arity, Context) -->
+ prog_out__write_context(Context),
+ report_warning("Warning: 'pragma terminates("),
+ hlds_out__write_pred_call_id(Name / Arity),
+ io__write_string(")' and\n"),
+ prog_out__write_context(Context),
+ io__write_string(" 'pragma check_termination("),
+ hlds_out__write_pred_call_id(Name / Arity),
+ io__write_string(")' defined on the one predicate\n").
%-----------------------------------------------------------------------------%
% module_add_pragma_fact_table(PredName, Arity, FileName,
Index: mercury_compile.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mercury_compile.m,v
retrieving revision 1.32
diff -u -r1.32 mercury_compile.m
--- mercury_compile.m 1997/03/05 07:11:01 1.32
+++ mercury_compile.m 1997/04/08 15:09:18
@@ -26,19 +26,20 @@
% library modules
:- import_module int, list, map, set, std_util, dir, require.
-:- import_module library, getopt, term, varset.
+:- import_module library, getopt, term, varset, bool.
% the main compiler passes (in order of execution)
:- 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 polymorphism, higher_order, inlining, dnf.
:- import_module 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.
:- import_module llds_common, llds_out.
+:- import_module termination, trans_opt.
% miscellaneous compiler modules
:- import_module prog_data, hlds_module, hlds_pred, hlds_out, llds.
@@ -208,6 +209,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 } ->
@@ -222,6 +225,11 @@
mercury_compile__maybe_output_prof_call_graph(HLDS21,
Verbose, Stats, HLDS25),
mercury_compile__middle_pass(ModuleName, HLDS25, HLDS50),
+ ( { MakeTransOptInt = yes } ->
+ trans_opt__write_optfile(HLDS50)
+ ;
+ []
+ ),
globals__io_lookup_bool_option(highlevel_c, HighLevelC),
( { HighLevelC = yes } ->
{ string__append(ModuleName, ".c", C_File) },
@@ -309,15 +317,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).
@@ -580,8 +599,11 @@
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"),
@@ -862,6 +884,26 @@
"% Program is determinism-correct.\n")
),
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 cannot 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).
Index: mercury_to_mercury.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.98
diff -u -r1.98 mercury_to_mercury.m
--- mercury_to_mercury.m 1997/04/03 01:17:53 1.98
+++ mercury_to_mercury.m 1997/04/04 08:23:41
@@ -15,7 +15,7 @@
:- interface.
:- import_module hlds_goal, hlds_data, hlds_pred, prog_data.
-:- import_module list, io, varset, term.
+:- import_module list, io, varset, term, termination.
% convert_to_mercury(ProgName, OutputFileName, Items)
:- pred convert_to_mercury(string, string, list(item_and_context),
@@ -297,6 +297,17 @@
;
{ Pragma = fact_table(Pred, Arity, FileName) },
mercury_output_pragma_fact_table(Pred, Arity, FileName)
+ ;
+ { Pragma = opt_terminates(PredOrFunc, PredName, Arity,
+ ProcId, Termination) },
+ termination__output_pragma_opt_terminates(PredOrFunc,
+ PredName, Arity, ProcId, Termination)
+ ;
+ { Pragma = terminates(Pred, Arity) },
+ mercury_output_pragma_decl(Pred, Arity, "terminates")
+ ;
+ { Pragma = check_termination(Pred, Arity) },
+ mercury_output_pragma_decl(Pred, Arity, "check_termination")
).
mercury_output_item(nothing, _) --> [].
Index: module_qual.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/module_qual.m,v
retrieving revision 1.13
diff -u -r1.13 module_qual.m
--- module_qual.m 1997/02/02 12:41:50 1.13
+++ module_qual.m 1997/02/18 04:58:54
@@ -564,6 +564,11 @@
Info, Info) --> [].
qualify_pragma(fact_table(SymName, Arity, FileName),
fact_table(SymName, Arity, FileName), Info, Info) --> [].
+qualify_pragma(opt_terminates(A, B, C, D, E), opt_terminates(A, B, C, D, E),
+ Info, Info) --> [].
+qualify_pragma(terminates(A, B), terminates(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: modules.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/modules.m,v
retrieving revision 1.33
diff -u -r1.33 modules.m
--- modules.m 1997/04/07 05:39:38 1.33
+++ modules.m 1997/04/07 05:54:55
@@ -234,11 +234,14 @@
report_warning("Warning: clause in module interface.\n"),
check_for_clauses_in_interface(Items0, Items)
;
- % `pragma obsolete' declarations are supposed to go
+ % `pragma (obsolete, terminates, 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 \= check_termination(_, _) }
->
prog_out__write_context(Context),
report_warning("Warning: pragma in module interface.\n"),
Index: options.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/options.m,v
retrieving revision 1.193
diff -u -r1.193 options.m
--- options.m 1997/03/27 03:29:09 1.193
+++ options.m 1997/04/10 11:58:37
@@ -71,6 +71,7 @@
; assume_gmake
; generate_bytecode
; generate_prolog
+ ; make_transitive_opt_interface
; prolog_dialect
; line_numbers
; auto_comments
@@ -147,6 +148,7 @@
; opt_level
; opt_space % default is to optimize time
; intermodule_optimization
+ ; transitive_optimization
; split_c_files
% - HLDS
; inlining
@@ -169,6 +171,8 @@
; follow_code
; prev_code
; optimize_dead_procs
+ ; termination
+ ; termination_single_args
% - HLDS->LLDS
; smart_indexing
; dense_switch_req_density
@@ -258,7 +262,7 @@
warn_interface_imports - bool(no),
warn_non_stratification - bool(no),
warn_missing_opt_files - bool(yes),
- warn_simple_code - bool(yes),
+ warn_simple_code - bool(no),
warn_duplicate_calls - bool(no)
]).
option_defaults_2(verbosity_option, [
@@ -289,6 +293,7 @@
option_defaults_2(aux_output_option, [
% Auxiliary Output Options
assume_gmake - bool(yes),
+ make_transitive_opt_interface - bool(no),
generate_bytecode - bool(no),
generate_prolog - bool(no),
prolog_dialect - string("default"),
@@ -386,6 +391,9 @@
opt_level - int_special,
opt_space - special,
intermodule_optimization - bool(no),
+ transitive_optimization - bool(no),
+ termination - bool(no),
+ termination_single_args - bool(no),
split_c_files - bool(no)
]).
option_defaults_2(optimization_option, [
@@ -569,6 +577,11 @@
long_option("show-dependency-graph", show_dependency_graph).
long_option("dump-hlds", dump_hlds).
long_option("verbose-dump-hlds", verbose_dump_hlds).
+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).
% language semantics options
long_option("reorder-conj", reorder_conj).
@@ -641,6 +654,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).
@@ -670,6 +688,12 @@
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("check-termination", termination).
+long_option("check-term", termination).
+long_option("term", termination).
+long_option("termination-single-argument-analysis",
+ termination_single_args).
+long_option("term-single-arg", termination_single_args).
% HLDS->LLDS optimizations
long_option("smart-indexing", smart_indexing).
@@ -1126,7 +1150,11 @@
io__write_string("\t\tWith `--dump-hlds', include extra detail in the dump.\n"),
io__write_string("\t\tEach type of detail is included in the dump if its\n"),
io__write_string("\t\tcorresponding letter occurs in the option argument\n"),
- io__write_string("\t\t(see the Mercury User's Guide for details).\n").
+ io__write_string("\t\t(see the Mercury User's Guide for details).\n"),
+ io__write_string("\t--make-transitive-optimization-interface\n"),
+ io__write_string("\t--make-trans-opt\n"),
+ io__write_string("\t\tOutput transient optimization information\n"),
+ io__write_string("\t\tinto the <module>.trans_opt file.\n").
:- pred options_help_semantics(io__state::di, io__state::uo) is det.
@@ -1343,6 +1371,14 @@
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--transient-intermodule-optimization\n"),
+ io__write_string("\t--trans-intermod-opt\n"),
+ io__write_string("\t\tImport data the transient intermodule optimization data..\n"),
+ io__write_string("\t\tThis data is stored in the <module>.trans_opt file\n"),
+ io__write_string("\t--check-termination"),
+ io__write_string("\t--check-term"),
+ io__write_string("\t--term"),
+ io__write_string("\t\tAnalyse each predicate to discover if it terminates.\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: prog_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_data.m,v
retrieving revision 1.16
diff -u -r1.16 prog_data.m
--- prog_data.m 1997/01/27 07:45:29 1.16
+++ prog_data.m 1997/02/18 00:56:19
@@ -85,49 +85,59 @@
:- 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
-
- ; 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.
-
- ; fact_table(sym_name, arity, string).
- % Predname, Arity, Fact file name.
+:- 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
+
+ ; 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.
+
+ ; fact_table(sym_name, arity, string)
+ % Predname, Arity, Fact file name.
+ ; opt_terminates(pred_or_func, sym_name, int, proc_id,
+ termination)
+ % PredName, Arity, Mode, Termination
+ % Used for inter-module termination analysis
+ % should only appear in .opt files.
+ ; terminates(sym_name, int)
+ % Predname, Arity
+ ; check_termination(sym_name, int).
+ % Predname, Arity
% For pragma c_code, there are two different calling conventions,
% one for C code that may recursively call Mercury code, and another
Index: prog_io_pragma.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_io_pragma.m,v
retrieving revision 1.4
diff -u -r1.4 prog_io_pragma.m
--- prog_io_pragma.m 1997/03/06 05:09:48 1.4
+++ prog_io_pragma.m 1997/04/09 12:27:15
@@ -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, termination.
+:- import_module string, std_util, bool, require.
parse_pragma(ModuleName, VarSet, PragmaTerms, Result) :-
(
@@ -314,6 +314,99 @@
ErrorTerm)
).
+
+
+ % pragma opt_terminates should never appear in user programs,
+ % only in .opt files.
+parse_pragma_type(ModuleName, "opt_terminates", PragmaTerms, ErrorTerm,
+ _VarSet, Result) :-
+
+ (
+ PragmaTerms = [
+ PredOrFuncTerm,
+ PredNameTerm,
+ term__functor(term__integer(Arity), [], _),
+ term__functor(term__integer(ProcInt), [], _),
+ ConstTerm,
+ TerminatesTerm,
+ MaybeUsedArgsTerm
+ ],
+ proc_id_to_int(ProcId, ProcInt),
+ (
+ PredOrFuncTerm = term__functor(
+ term__atom("predicate"), [], _),
+ PredOrFunc = predicate
+ ;
+ PredOrFuncTerm = term__functor(
+ term__atom("function"), [], _),
+ PredOrFunc = function
+ ),
+ parse_qualified_term(ModuleName, PredNameTerm,
+ "predicate name", PredNameResult),
+ PredNameResult = ok(PredName, []),
+ (
+ ConstTerm = term__functor(
+ term__atom("not_set"), [], _),
+ Const = not_set
+ ;
+ ConstTerm = term__functor(
+ term__atom("infinite"), [], _),
+ Const = inf(no)
+ ;
+ ConstTerm = term__functor(
+ term__atom("set"), [IntTerm], _),
+ IntTerm = term__functor(term__integer(Int), [], _),
+ Const = set(Int)
+ ),
+ (
+ TerminatesTerm = term__functor(
+ term__atom("not_set"), [], _),
+ Terminates = not_set
+ ;
+ TerminatesTerm = term__functor(
+ term__atom("dont_know"), [], _),
+ Terminates = dont_know
+ ;
+ TerminatesTerm = term__functor(
+ term__atom("yes"), [], _),
+ Terminates = yes
+ ),
+ (
+ 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(Const, Terminates, MaybeUsedArgs, no)
+
+ ->
+ Result = ok(pragma(opt_terminates(PredOrFunc, PredName, Arity,
+ ProcId, Termination)))
+ ;
+ Result = error("error in pragma opt_terminates", ErrorTerm)
+ ).
+
+
+
+
+parse_pragma_type(ModuleName, "assert_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, "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)).
@@ -510,4 +603,25 @@
;
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 = []
).
%-----------------------------------------------------------------------------%
% Copyright (C) 1996 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: trans_opt.m
% main author: crs
%
% This module writes out the interface for transitive intermodule optimization.
% The .trans_opt file includes:
% - pragma opt_terminates declarations for all exported preds
% All these items should be module qualified.
% Constructors should be explicitly type qualified.
%
% This module also contains predicates to read in the .trans_opt files.
%
%-----------------------------------------------------------------------------%
:- module trans_opt.
%-----------------------------------------------------------------------------%
:- interface.
:- import_module io, bool, hlds_module, modules.
:- pred trans_opt__write_optfile(module_info, io__state, io__state).
:- mode trans_opt__write_optfile(in, di, uo) is det.
% Add the items from the .trans_opt files of imported modules to
% the items for this module.
:- pred trans_opt__grab_optfiles(module_imports, module_imports, bool,
io__state, io__state).
:- mode trans_opt__grab_optfiles(in, out, out, di, uo) is det.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module hlds_pred, mercury_to_mercury, varset, term, std_util.
:- import_module prog_io, string, list, map, globals, code_util.
:- import_module passes_aux, prog_data, prog_out, options, termination.
%-----------------------------------------------------------------------------%
% Open the file "<module-name>.trans_opt", and write out the
% declarations.
trans_opt__write_optfile(Module) -->
{ module_info_name(Module, ModuleName) },
% XXX this should be .trans_opt.tmp, and it should be compared
% at the end of making the .trans_opt.tmp
{ string__append(ModuleName, ".trans_opt", OptName) },
io__open_output(OptName, Result),
(
{ Result = error(Error) },
{ io__error_message(Error, Msg) },
io__progname_base("termination.m", ProgName),
io__write_string(ProgName),
io__write_string(
": cannot open transient optimisation file '"),
io__write_string(OptName),
io__write_string("' \n"),
io__write_string(ProgName),
io__write_string(": for output: "),
io__write_string(Msg),
io__nl,
io__set_exit_status(1)
;
{ Result = ok(Stream) },
io__set_output_stream(Stream, OldStream),
{ module_info_name(Module, ModName) },
io__write_string(":- module "),
mercury_output_bracketed_constant(term__atom(ModName)),
io__write_string(".\n"),
% all predicates to write global items into the .trans_opt
% file should go here.
{ module_info_predids(Module, PredIds) },
trans_opt__write_preds(PredIds, Module),
io__set_output_stream(OldStream, _),
io__close_output(Stream)
).
:- pred trans_opt__write_preds(list(pred_id), module_info,
io__state, io__state).
:- mode trans_opt__write_preds(in, in, di, uo) is det.
trans_opt__write_preds([], _) --> [].
trans_opt__write_preds([ PredId | PredIds ], Module) -->
{ module_info_preds(Module, PredTable) },
{ map__lookup(PredTable, PredId, PredInfo) },
(
{ pred_info_is_exported(PredInfo) },
\+ { code_util__predinfo_is_builtin(PredInfo) },
\+ { code_util__compiler_generated(PredInfo) }
->
% all predicates to write predicate info into the .trans_opt
% file should go here.
{ pred_info_procedures(PredInfo, ProcTable) },
{ map__keys(ProcTable, ProcIds) },
trans_opt__write_procs(ProcIds, PredId, PredInfo)
;
[]
),
trans_opt__write_preds(PredIds, Module).
:- pred trans_opt__write_procs(list(proc_id), pred_id, pred_info,
io__state, io__state).
:- mode trans_opt__write_procs(in, in, in, di, uo) is det.
trans_opt__write_procs([], _, _) --> [].
trans_opt__write_procs([ProcId | ProcIds], PredId, PredInfo) -->
{ pred_info_procedures(PredInfo, ProcTable) },
{ map__lookup(ProcTable, ProcId, ProcInfo) },
{ pred_info_name(PredInfo, PredName) },
{ pred_info_module(PredInfo, ModuleName) },
{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
{ pred_info_arity(PredInfo, Arity) },
{ SymName = qualified(ModuleName, PredName) },
{ proc_info_termination(ProcInfo, Termination) },
% all predicates to write procedure items into the .trans_opt file
% should go here.
termination__output_pragma_opt_terminates(PredOrFunc, SymName,
Arity, ProcId, Termination),
trans_opt__write_procs(ProcIds, PredId, PredInfo).
%-----------------------------------------------------------------------------%
% Read in and process the transitive optimization interfaces.
trans_opt__grab_optfiles(Module0, Module, FoundError) -->
{ Module0 = module_imports(ModuleName, DirectImports0,
IndirectImports0, Items0, _) },
{ list__sort_and_remove_dups(DirectImports0, Imports) },
read_optimization_interfaces(Imports, [], OptItems, no, FoundError),
{ term__context_init(Context) },
{ varset__init(Varset) },
{ OptDefn = module_defn(Varset, opt_imported) - Context },
{ list__append(Items0, [ OptDefn | OptItems ], Items) },
{ Module = module_imports(ModuleName, DirectImports0,
IndirectImports0, Items, no) }.
:- pred read_optimization_interfaces(list(module_name), item_list,
item_list, bool, bool, io__state, io__state).
:- mode read_optimization_interfaces(in, in, out, in, out, di, uo) is det.
read_optimization_interfaces([], Items, Items, Error, Error) --> [].
read_optimization_interfaces([Import | Imports],
Items0, Items, Error0, Error) -->
globals__io_lookup_bool_option(very_verbose, VeryVerbose),
maybe_write_string(VeryVerbose,
"% Reading optimization interface for module"),
maybe_write_string(VeryVerbose, " `"),
maybe_write_string(VeryVerbose, Import),
maybe_write_string(VeryVerbose, "'... "),
maybe_flush_output(VeryVerbose),
maybe_write_string(VeryVerbose, "% done.\n"),
{ string__append(Import, ".trans_opt", FileName) },
prog_io__read_module(FileName, Import, yes,
ModuleError, Messages, Items1),
update_error_status(ModuleError, Messages, Error0, Error1),
{ list__append(Items0, Items1, Items2) },
read_optimization_interfaces(Imports, Items2, Items, Error1, Error).
:- pred update_error_status(module_error, message_list,
bool, bool, io__state, io__state).
:- mode update_error_status(in, in, in, out, di, uo) is det.
update_error_status(ModuleError, Messages, Error0, Error1) -->
(
{ ModuleError = no },
{ Error1 = Error0 }
;
{ ModuleError = yes },
prog_out__write_messages(Messages),
{ Error1 = yes }
;
{ ModuleError = fatal },
{ Error1 = Error0 }
).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------
%
% Copyright (C) 1995 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.
%-----------------------------------------------------------------------------
%
% termination.m
% Main author: crs.
%
% This termination analysis is based on the algorithm given by Gerhard Groeger
% and Lutz Plumer in their paper "Handling of Mutual Recursion in Automatic
% Termination Proofs for Logic Programs" which was printed in JICSLP '92
% pages 336 - 350.
%
% Currently, this implementation assumes that all c_code terminates.
%
%-----------------------------------------------------------------------------
%
:- module termination.
:- interface.
:- import_module io.
:- import_module hlds_module, term_error, term_util.
% The top level predicate. This controls all of the termination analysis
:- pred termination__pass(module_info, module_info, io__state, io__state).
:- mode termination__pass(in, out, di, uo) is det.
% this provides an initialised termination.
:- pred termination__init(termination).
:- mode termination__init(out) is det.
% this prints out a termination structure.
:- pred termination__out(termination, io__state, io__state).
:- mode termination__out(in, di, uo) is det.
% this prints out the used_ards structure
:- pred termination__out_used_args(termination, io__state, io__state).
:- mode termination__out_used_args(in, di, uo) is det.
% this prints out the constant
:- pred termination__out_const(termination, io__state, io__state).
:- mode termination__out_const(in, di, uo) is det.
% this prints out the terminates (yes/dont_know/not_set).
:- pred termination__out_terminates(termination, io__state, io__state).
:- mode termination__out_terminates(in, di, uo) is det.
% this outputs pragma opt_terminates which are used in .trans_opt and .opt
% files.
:- pred termination__output_pragma_opt_terminates(pred_or_func, sym_name,
int, proc_id, termination, io__state, io__state).
:- mode termination__output_pragma_opt_terminates(in, in, in, in, in,
di, uo) is det.
% this is used to output an error in a short form, suitable for
% printing the HLDS.
:- pred termination__maybe_output_error(module_info, termination,
io__state, io__state).
:- mode termination__maybe_output_error(in, in, di, uo) is det.
%----------------------------------------------------------------------------%
:- implementation.
:- import_module map, std_util, list, type_util, require.
:- import_module options, globals, bool, char, prog_data.
:- import_module passes_aux. % for maybe_write_string
:- import_module mercury_to_mercury.
:- import_module inst_match, mode_util, int, hlds_out, string, relation.
:- import_module hlds_data, hlds_pred, hlds_goal, dependency_graph.
:- import_module code_util, prog_out, bag, set.
:- import_module term_pass1, term_pass2.
%-----------------------------------------------------------------------------%
termination__pass(Module0, Module) -->
globals__io_lookup_bool_option(verbose, Verbose),
maybe_write_string(Verbose, "% Checking Termination .....\n"),
% globals__io_lookup_bool_option(make_optimization_interface,
% MakeOptInt),
{ module_info_ensure_dependency_info(Module0, Module1) },
{ module_info_predids(Module1, PredIds) },
check_preds(PredIds, Module1, Module2),
proc_inequalities(Module2, Module3),
termination(Module3, Module),
/**
( { MakeOptInt = yes } ->
termination__make_opt_int(PredIds, Module)
;
[]
),
**/
maybe_write_string(Verbose, "% Termination checking done.\n").
termination__init(term(not_set, not_set, no, no)).
%-----------------------------------------------------------------------------%
% These termination__out predicates are used to print out the opt_terminates
% pragmas. If they are changed, then prog_io_pragma.m must also be changed
% so that it can parse the resulting pragma opt_terminates declarations
termination__out(Termination) -->
termination__out_terminates(Termination),
io__write_string("("),
termination__out_const(Termination),
io__write_string(")").
termination__out_used_args(term(_Const, _Term, MaybeUsedArgs, _)) -->
(
{ MaybeUsedArgs = yes([]) },
io__write_string("yes([])")
;
{ MaybeUsedArgs = yes([UsedArg | UsedArgs]) },
io__write_string("yes([ "),
io__write(UsedArg),
termination__out_used_args_2(UsedArgs),
io__write_string(" ])")
;
{ MaybeUsedArgs = no },
io__write_string("no")
).
:- pred termination__out_used_args_2(list(bool), io__state, io__state).
:- mode termination__out_used_args_2(in, di, uo) is det.
termination__out_used_args_2([]) --> [].
termination__out_used_args_2([ UsedArg | UsedArgs ]) -->
io__write_string(", "),
io__write(UsedArg),
termination__out_used_args_2(UsedArgs).
termination__out_terminates(term(_, Term, _, _)) -->
termination__out_terminates_2(Term).
:- pred termination__out_terminates_2(terminates, io__state, io__state).
:- mode termination__out_terminates_2(in, di, uo) is det.
termination__out_terminates_2(not_set) -->
io__write_string("not_set").
termination__out_terminates_2(dont_know) -->
io__write_string("dont_know").
termination__out_terminates_2(yes) -->
io__write_string("yes").
termination__out_const(term(Const, _, _, _)) -->
termination__out_const_2(Const).
:- pred termination__out_const_2(term_util__constant, io__state, io__state).
:- mode termination__out_const_2(in, di, uo) is det.
termination__out_const_2(inf(_)) -->
io__write_string("infinite").
termination__out_const_2(not_set) -->
io__write_string("not_set").
termination__out_const_2(set(Int)) -->
io__write_string("set("),
io__write_int(Int),
io__write_string(")").
termination__output_pragma_opt_terminates(PredOrFunc, SymName,
Arity, ProcId, Termination) -->
io__write_string(":- pragma opt_terminates("),
hlds_out__write_pred_or_func(PredOrFunc),
io__write_string(", "),
mercury_output_bracketed_sym_name(SymName),
io__write_string(", "),
io__write_int(Arity),
io__write_string(", "),
{ proc_id_to_int(ProcId, ProcInt) },
io__write_int(ProcInt),
io__write_string(", "),
termination__out_const(Termination),
io__write_string(", "),
termination__out_terminates(Termination),
io__write_string(", "),
termination__out_used_args(Termination),
io__write_string(").\n").
termination__maybe_output_error(Module, term(Const, _, _, MaybeError)) -->
( { MaybeError = yes(Error) } ->
io__write_string("% unable to determine termination as:"),
term_error__output(no, Module, Error)
;
[]
),
( { Const = inf(yes(ConstError)) } ->
io__write_string("% unable to set const as:"),
term_error__output(no, Module, ConstError)
;
[]
).
%-----------------------------------------------------------------------------%
:- pred check_preds(list(pred_id), module_info, module_info,
io__state, io__state).
:- mode check_preds(in, in, out, di, uo) is det.
check_preds([], Module, Module, State, State).
check_preds([PredId | PredIds] , Module0, Module, State0, State) :-
module_info_preds(Module0, PredTable0),
map__lookup(PredTable0, PredId, PredInfo0),
pred_info_import_status(PredInfo0, ImportStatus),
pred_info_procedures(PredInfo0, ProcTable0),
map__keys(ProcTable0, ProcIds),
(
(
ImportStatus = exported
; ImportStatus = local
; ImportStatus = pseudo_exported
)
->
pred_info_get_marker_list(PredInfo0, Markers),
( list__member(request(terminates), Markers) ->
change_procs_terminate(ProcIds, no, yes,
no, ProcTable0, ProcTable2)
; code_util__predinfo_is_builtin(PredInfo0) ->
set_builtin_terminates(ProcIds, PredInfo0, Module0,
ProcTable0, ProcTable2)
;
ProcTable2 = ProcTable0
),
State0 = State1
; %else if
(
ImportStatus = imported
; ImportStatus = opt_decl % should this be here?
; ImportStatus = opt_imported
; ImportStatus = pseudo_imported % should this be here?
)
->
% all of the predicates that are processed here are imported
% in some way
% with imported predicates, any 'request(check_termination)'
% markers will be checked by the compiler when it compiles
% relevant source file (that the pred was imported from)
% When making the intermodule optimizations, the
% check_termination will not be checked, so it cannot
% be depended upon
pred_info_get_marker_list(PredInfo0, Markers),
globals__io_lookup_bool_option(make_optimization_interface,
MakeOptInt, State0, State1),
(
(
list__member(request(terminates), Markers)
;
MakeOptInt = no,
list__member(request(check_termination), Markers)
)
->
change_procs_terminate(ProcIds, no, yes, no,
ProcTable0, ProcTable1)
; %else if
code_util__predinfo_is_builtin(PredInfo0)
->
set_builtin_terminates(ProcIds, PredInfo0, Module0,
ProcTable0, ProcTable1)
;
% go through, changing each 'not_set' to 'dont_know'
change_procs_terminate(ProcIds, yes(not_set), dont_know,
no, ProcTable0, ProcTable1)
),
change_procs_const(ProcIds, yes(not_set), inf(no),
ProcTable1, ProcTable2)
;
% (
% ImportStatus = abstract_imported
% ; ImportStatus = abstract_exported
% ),
% this should not happen, as procedures are being processed
% here, and these import_status' refer to abstract types
error("Unexpected Import Status of a predicate"),
ProcTable2 = ProcTable0,
State0 = State1
),
(
% dont know if compiler gen/mercury_builtin preds will be
% imported or not
set_compiler_gen_terminates(ProcIds, PredInfo0,
Module0, ProcTable2, ProcTable3)
->
ProcTable = ProcTable3
;
ProcTable = ProcTable2
),
pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
map__set(PredTable0, PredId, PredInfo, PredTable),
module_info_set_preds(Module0, PredTable, Module1),
check_preds(PredIds, Module1, Module, State1, State).
:- pred set_builtin_terminates(list(proc_id), pred_info, module_info,
proc_table, proc_table).
:- mode set_builtin_terminates(in, in, in, in, out) is det.
set_builtin_terminates([], _, _, ProcTable, ProcTable).
set_builtin_terminates([ProcId | ProcIds], PredInfo, Module, ProcTable0,
ProcTable) :-
map__lookup(ProcTable0, ProcId, ProcInfo0),
( attempt_set_proc_const(Module, PredInfo, ProcInfo0) ->
% for attempt_set_proc_const to succeed, the output vars of
% that proc must all be of a type that cannot be recursive.
% hence the size of the output vars will all be size 0,
% independent on the input variables. therefore, as the
% size of the output vars do not depend on the size of the
% input vars, usedargs should be set to yes([no, no, ...])
Const = set(0),
proc_info_headvars(ProcInfo0, HeadVars),
term_util__make_bool_list_2(HeadVars, [], Bools),
UsedArgs = yes(Bools)
;
Const = inf(no),
UsedArgs = no
),
Term = term(Const, yes, UsedArgs, no),
proc_info_set_termination(ProcInfo0, Term, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1),
set_builtin_terminates(ProcIds, PredInfo, Module, ProcTable1,
ProcTable).
% this pred checs to see if the ProcId is a compiler generated pred, or a
% mercury_builtin pred. If it is, then it sets the termination property
% of the ProcIds accordingly.
:- pred set_compiler_gen_terminates(list(proc_id), pred_info, module_info,
proc_table, proc_table).
:- mode set_compiler_gen_terminates(in, in, in, in, out) is semidet.
set_compiler_gen_terminates([], _PredInfo, _Module, ProcTable, ProcTable).
set_compiler_gen_terminates([ ProcId | ProcIds ], PredInfo, Module,
ProcTable0, ProcTable) :-
pred_info_name(PredInfo, PredName),
pred_info_arity(PredInfo, Arity),
pred_info_module(PredInfo, ModuleName),
( Arity = 3 ->
(
PredName = "__Compare__"
;
ModuleName = "mercury_builtin",
PredName = "compare"
),
map__lookup(ProcTable0, ProcId, ProcInfo0),
term_util__make_bool_list(ProcInfo0,
[no, no, no], OutList),
Termination = term(set(0), yes, yes(OutList), no)
; Arity = 2 ->
(
(
PredName = "__Unify__"
;
ModuleName = "mercury_builtin",
PredName = "unify"
)
->
map__lookup(ProcTable0, ProcId, ProcInfo0),
term_util__make_bool_list(ProcInfo0,
[yes, yes], OutList),
Termination = term(set(0), yes,
yes(OutList), no)
; % else if
(
PredName = "__Index__"
;
ModuleName = "mercury_builtin",
PredName = "index"
)
->
map__lookup(ProcTable0, ProcId, ProcInfo0),
term_util__make_bool_list(ProcInfo0,
[no, no], OutList),
Termination = term(set(0), yes,
yes(OutList), no)
; % else if
% XXX what is the relationship between size of
% input and size of output in Term_To_Type and
% Type_To_Term? Which arguments are used to make
% the output variables?
PredName = "__Term_To_Type__"
->
map__lookup(ProcTable0, ProcId, ProcInfo0),
Termination = term(inf(no), yes, no, no)
;
PredName = "__Type_To_Term__",
map__lookup(ProcTable0, ProcId, ProcInfo0),
Termination = term(inf(no), yes, no, no)
)
;
ModuleName = "mercury_builtin",
map__lookup(ProcTable0, ProcId, ProcInfo0),
( attempt_set_proc_const(Module, PredInfo, ProcInfo0) ->
proc_info_headvars(ProcInfo0, HeadVars),
term_util__make_bool_list_2(HeadVars, [], Bools),
UsedArgs = yes(Bools),
Termination = term(set(0), yes, UsedArgs, no)
;
proc_info_termination(ProcInfo0, OldTerm),
OldTerm = term(OldConst, _, OldUsedArgs, _),
Termination = term(OldConst, yes, OldUsedArgs, no)
)
),
% it is a compiler generated procedure, so enter the data in
% the proc_inf
proc_info_set_termination(ProcInfo0, Termination, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1),
set_compiler_gen_terminates(ProcIds, PredInfo, Module,
ProcTable1, ProcTable).
% for attempt_set_proc_const to succeed, the output vars of
% that proc must all be of a type that cannot be recursive.
% hence the size of the output vars will all be size 0,
% independent on the input variables.
:- pred attempt_set_proc_const(module_info, pred_info, proc_info).
:- mode attempt_set_proc_const(in, in, in) is semidet.
attempt_set_proc_const(Module, PredInfo, ProcInfo) :-
pred_info_arg_types(PredInfo, _, TypeList),
proc_info_argmodes(ProcInfo, ModeList),
attempt_set_proc_const_2(TypeList, ModeList, Module).
:- pred attempt_set_proc_const_2(list(type), list(mode), module_info).
:- mode attempt_set_proc_const_2(in, in, in) is semidet.
attempt_set_proc_const_2([], [], _).
attempt_set_proc_const_2([], [_|_], _) :-
error("Unmatched vars in termination.m").
attempt_set_proc_const_2([_|_], [], _) :-
error("Unmatched vars in termination.m").
attempt_set_proc_const_2([Type | Types], [Mode | Modes], Module) :-
( mode_is_input(Module, Mode) ->
% doesnt matter what type it is
attempt_set_proc_const_2(Types, Modes, Module)
;
classify_type(Type, Module, TypeOfType),
% user_type could be a type_info, which should be called
% size 0. this is not a big problem, as most type_infos
% are input.
TypeOfType \= user_type(_),
% this could be changed, by looking up the poly type,
% and seeing if that is recursive, or could it?
TypeOfType \= polymorphic_type,
TypeOfType \= pred_type,
attempt_set_proc_const_2(Types, Modes, Module)
).
:- pred change_procs_terminate(list(proc_id), maybe(terminates), terminates,
maybe(term_error__error), proc_table, proc_table).
:- mode change_procs_terminate(in, in, in, in, in, out) is det.
change_procs_terminate([], _Find, _Replace, _, ProcTable, ProcTable).
change_procs_terminate([ProcId | ProcIds], MaybeFind, Replace, MaybeError,
ProcTable0, ProcTable) :-
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_termination(ProcInfo0, Termination),
(
Termination = term(Const, Terminates, UsedArgs, _Error),
(
MaybeFind = yes(Terminates)
;
MaybeFind = no
)
->
Termination1 = term(Const, Replace, UsedArgs, MaybeError),
proc_info_set_termination(ProcInfo0, Termination1, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1)
;
ProcTable1 = ProcTable0
),
change_procs_terminate(ProcIds, MaybeFind, Replace, MaybeError,
ProcTable1, ProcTable).
:- pred change_procs_const(list(proc_id), maybe(term_util__constant),
term_util__constant, proc_table, proc_table).
:- mode change_procs_const(in, in, in, in, out) is det.
change_procs_const([], _Find, _Replace, ProcTable, ProcTable).
change_procs_const([ProcId | ProcIds], MaybeFind, Replace, ProcTable0,
ProcTable) :-
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_termination(ProcInfo0, Termination),
(
Termination = term(Const, Term, UsedArgs, MaybeError),
(
MaybeFind = yes(Const)
;
MaybeFind = no
)
->
Termination1 = term(Replace, Term, UsedArgs, MaybeError),
proc_info_set_termination(ProcInfo0, Termination1, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable1)
;
ProcTable1 = ProcTable0
),
change_procs_const(ProcIds, MaybeFind, Replace, ProcTable1, ProcTable).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% These predicates are used to add the opt_terminates pragmas to the .opt
% file. Currently they are not used, because the .trans_opt file does a
% much better job.
:- pred termination__make_opt_int(list(pred_id), module_info, io__state,
io__state).
:- mode termination__make_opt_int(in, in, di, uo) is det.
termination__make_opt_int(PredIds, Module) -->
{ module_info_name(Module, ModuleName) },
{ string__append(ModuleName, ".opt", OptFileName) },
io__open_append(OptFileName, OptFileRes),
( { OptFileRes = ok(OptFile) } ->
io__set_output_stream(OptFile, OldStream),
termination__make_opt_int_2(PredIds, Module),
io__set_output_stream(OldStream, _),
io__close_output(OptFile)
;
% damn thing
io__write_strings(["Cannot open `",
OptFileName, "' for output\n"]),
io__set_exit_status(1)
).
:- pred termination__make_opt_int_2(list(pred_id), module_info,
io__state, io__state).
:- mode termination__make_opt_int_2(in, in, di, uo) is det.
termination__make_opt_int_2([], _Module) --> [].
termination__make_opt_int_2([ PredId | PredIds ], Module) -->
{ module_info_preds(Module, PredTable) },
{ map__lookup(PredTable, PredId, PredInfo) },
{ pred_info_import_status(PredInfo, ImportStatus) },
{ pred_info_procedures(PredInfo, ProcTable) },
{ pred_info_procids(PredInfo, ProcIds) },
{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
{ pred_info_name(PredInfo, PredName) },
{ pred_info_module(PredInfo, ModuleName) },
{ SymName = qualified(ModuleName, PredName) },
{ pred_info_arity(PredInfo, Arity) },
( { ImportStatus = exported } ->
termination__make_opt_int_3(PredId, ProcIds, ProcTable,
PredOrFunc, SymName, Arity)
;
[]
),
termination__make_opt_int_2(PredIds, Module).
:- pred termination__make_opt_int_3(pred_id, list(proc_id), proc_table,
pred_or_func, sym_name, arity, io__state, io__state).
:- mode termination__make_opt_int_3(in, in, in, in, in, in, di, uo) is det.
termination__make_opt_int_3(_PredId, [], _, _, _, _) --> [].
termination__make_opt_int_3(PredId, [ ProcId | ProcIds ], ProcTable,
PredOrFunc, SymName, Arity) -->
{ map__lookup(ProcTable, ProcId, ProcInfo) },
{ proc_info_termination(ProcInfo, Termination) },
termination__output_pragma_opt_terminates(PredOrFunc, SymName,
Arity, ProcId, Termination),
termination__make_opt_int_3(PredId, ProcIds, ProcTable, PredOrFunc,
SymName, Arity).
%-----------------------------------------------------------------------------
%
% Copyright (C) 1995 University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------
%
% term_pass1.m
% Main author: crs.
%
% This file contains the first pass of the termination analysis.
% It sets the termination constant for all procedures, and also sets the
% terminates value for some procedures. (eg if the pred contains higher
% order arguments or calls.)
%
%-----------------------------------------------------------------------------
%
:- module term_pass1.
:- interface.
:- import_module io, hlds_module.
% get dependency ordering, and call proc_ineq_2 with them
:- pred proc_inequalities(module_info, module_info, io__state,
io__state).
:- mode proc_inequalities(in, out, di, uo) is det.
:- implementation.
:- import_module term_util, hlds_pred, hlds_goal, hlds_data, int, bag.
:- import_module term_error, list, require, bool, std_util, char, map, string.
:- import_module mode_util.
% this section contains proc_inequalities and its supporting functions.
% proc_inequalities goes through the dependency ordering, applying
% goal_inequality to each SCC in turn, and solving the resulting constraints
% Types used only in this section
%
% term_pass1__equation stores a single constraint
% the constraint is of the form:
% pred_proc_id - list(pred_proc_id) >= term_util__constant
:- type term_pass1__equation
---> eqn(term_util__constant, pred_proc_id, list(pred_proc_id)).
proc_inequalities(Module0, Module) -->
{ module_info_dependency_info(Module0, DependencyInfo) },
{ hlds_dependency_info_get_dependency_ordering(DependencyInfo,
DependencyOrdering) },
proc_inequalities_2(Module0, DependencyOrdering, Module).
:- pred proc_inequalities_2(module_info, dependency_ordering,
module_info, io__state, io__state).
:- mode proc_inequalities_2(in, in, out, di, uo) is det.
proc_inequalities_2(Module, [], Module) --> [].
proc_inequalities_2(Module0, [ SCC | SCCs ], Module) -->
proc_inequalities_3(Module0, SCC, SCC, [], Module2),
proc_inequalities_2(Module2, SCCs, Module).
:- pred proc_inequalities_3(module_info, list(pred_proc_id),
list(pred_proc_id), list(term_pass1__equation), module_info,
io__state, io__state).
:- mode proc_inequalities_3(in, in, in, in, out, di, uo) is det.
proc_inequalities_3(Module0, [], SCC, Offs0, Module) -->
% step one: solve eqns
{ proc_inequalities_3_remove_useless_offsets(Offs0, Offs, Succ) },
% XXX what is the correct context to use when referring to
% a whole SCC?
( { SCC = [proc(PredId, _)] } ->
{ module_info_pred_info(Module0, PredId, PredInfo) },
{ pred_info_context(PredInfo, Context) }
;
{ term__context_init(Context) }
),
( { Succ = no } ->
% There is a directly recursive call where the variables
% grow between the head and recursive call. Therefore the
% output is infinitly larger than the input.
% e.g. foo(A) :- foo([1|A]).
{ set_pred_proc_ids_const(SCC, inf(no), Module0, Module) }
; { Offs = [] } ->
%io__write_string("There were no equations in this SCC\n"),
% this probably means that it is analysing a builtin pred
% which has no body.
% XXX what is the correct context to use when referring to
% a whole SCC?
{ set_pred_proc_ids_const(SCC, inf(yes(Context - no_eqns)),
Module0, Module) }
;
solve_eqns(Offs, SCC, Soln),
% step two: put results back into module
( { Soln = solved(SolutionList) } ->
%Yeah, it worked
{ module_info_preds(Module0, PredTable0) },
{ proc_inequalities_set_module(SolutionList,
PredTable0, PredTable) },
{ module_info_set_preds(Module0, PredTable, Module) }
; { Soln = optimal } ->
% damn error - print it out, and youre done
% all 'optimal' results should have been changed into
% a list of solutions
{ error("Unexpected Value in termination.m\n") },
{ Module0 = Module }
;
{ set_pred_proc_ids_const(SCC,
inf(yes(Context - lpsolve_failed(Soln))),
Module0, Module) }
)
).
proc_inequalities_3(Module0, [ PPId | PPIds ], SCC, Offs0, Module) -->
{ PPId = proc(PredId, ProcId) },
{ module_info_pred_proc_info(Module0, PredId, ProcId, _PredInfo,
ProcInfo) },
{ proc_info_termination(ProcInfo, Termination) },
( { Termination = term(not_set, _, _, _) } ->
{ goal_inequality(Module0, PredId, ProcId, Offs1, Res,
Module1) },
( { Res = error(Error) } ->
%VERBOSE
%io__write_string("G_Inequ err: "),
%term_error__output(yes(PredId), Module1, Error),
%io__write_string("\nOn Pred: "),
%hlds_out__write_pred_proc_id(Module1, PredId, ProcId),
%io__nl,
% damn, the bloody thing failed.
% set all term_util__constants to inf
{ set_pred_proc_ids_const(SCC, inf(yes(Error)),
Module0, Module2) },
(
{ (
Error = _ - horder_call
; Error = _ - horder_args(_)
) }
->
do_ppid_check_terminates(SCC, yes(Error),
Module2, Module)
;
{ Module = Module2 }
)
;
{ list__append(Offs0, Offs1, Offs) },
proc_inequalities_3(Module1, PPIds, SCC, Offs, Module)
)
;
( { SCC = [ PPId ] } ->
% This proc is in its own SCC.
% its term const could have been set from
% an intermodule optimization, or because it is
% imported. either way, it should just be left
{ Module = Module0 }
;
% Hmm, this shouldnt happen...
{ Module = Module0 },
{ error("Unexpected setting of termination constant")}
)
).
% this removes offsets where there are no variables
:- pred proc_inequalities_3_remove_useless_offsets(
list(term_pass1__equation), list(term_pass1__equation), bool).
:- mode proc_inequalities_3_remove_useless_offsets(in, out, out) is det.
proc_inequalities_3_remove_useless_offsets([], [], yes).
proc_inequalities_3_remove_useless_offsets([ Off0 | Offs0 ], Offs, Succ) :-
( Off0 = eqn(Const, PPId, [ PPId ]) ->
% in this case there is direct recursion
(
(
Const = set(Int),
Int > 0
;
Const = inf(_)
)
->
% in this case the recursive call is with larger
% variables. Hence the output could be unbounded
Succ = no,
Offs = Offs0
;
proc_inequalities_3_remove_useless_offsets(Offs0,
Offs, Succ)
)
;
proc_inequalities_3_remove_useless_offsets(Offs0, Offs1, Succ),
Offs = [ Off0 | Offs1]
).
:- pred proc_inequalities_set_module( list(pair(pred_proc_id, int)),
pred_table , pred_table).
:- mode proc_inequalities_set_module(in, in, out) is det.
proc_inequalities_set_module([], PredTable, PredTable).
proc_inequalities_set_module([ Soln | Solns ], PredTable0, PredTable) :-
Soln = PPId - Int,
Const = set(Int),
PPId = proc(PredId, ProcId),
map__lookup(PredTable0, PredId, PredInfo),
pred_info_procedures(PredInfo, ProcTable),
map__lookup(ProcTable, ProcId, ProcInfo),
proc_info_termination(ProcInfo, term(Const0, B, C, D)),
( Const0 = not_set ->
%YYY
%c_puts("proc"),
%c_put_term(PPId, term(Const, B, C, D)),
proc_info_set_termination(ProcInfo, term(Const, B, C, D),
ProcInfo1)
;
% this can happen if an imported pred was in the same
% SCC as some local preds, or if somehow some equations
% were made for an imported pred.
error("proc_inequalities_set_module: SoftwareError"),
ProcInfo1 = ProcInfo
),
map__set(ProcTable, ProcId, ProcInfo1, ProcTable1),
pred_info_set_procedures(PredInfo, ProcTable1, PredInfo1),
map__set(PredTable0, PredId, PredInfo1, PredTable1),
proc_inequalities_set_module(Solns, PredTable1, PredTable).
%-----------------------------------------------------------------------------%
% This section contains goal_inequality and its supporting functions.
% goal_inequality processes a goal, and finds an inequality relating the
% sizeof(input arguments) to the sizeof(output arguments). If it finds a
% valid inequality, then it returns the offset of the inequality (with Res
% set to ok). If no inequality can be found, then it returns Res = error().
:- pred goal_inequality(module_info, pred_id, proc_id,
list(term_pass1__equation), term_util__result(term_error__error),
module_info).
:- mode goal_inequality(in, in, in, out, out, out) is det.
goal_inequality(ModuleInfo0, PredId, ProcId, Offs, Res, ModuleInfo) :-
module_info_preds(ModuleInfo0, PredTable0),
map__lookup(PredTable0, PredId, PredInfo0),
pred_info_procedures(PredInfo0, ProcTable0),
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_headvars(ProcInfo0, Args),
proc_info_argmodes(ProcInfo0, ArgModes),
proc_info_goal(ProcInfo0, GoalExpr - GoalInfo),
partition_call_args(ModuleInfo0, ArgModes, Args, InVars, OutVars),
bag__from_list(InVars, InVarsBag),
bag__from_list(OutVars, OutVarsBag),
PPId = proc(PredId, ProcId),
goal_inequality_2(GoalExpr, GoalInfo, ModuleInfo0, total, PPId, Offs0,
Res1, OutVarsBag, InVars2Bag),
( Res1 = ok ->
Offs = Offs0,
( bag__is_subbag(InVars2Bag, InVarsBag) ->
Res = ok,
% setting the UsedArgs part of the termination
% type
proc_info_termination(ProcInfo0, Term0),
Term0 = term(Const, Terminates, _UsedArgs, MaybeError),
goal_inequality_used_args(Args, InVars2Bag, UsedArgs),
Term1 = term(Const, Terminates, yes(UsedArgs),
MaybeError),
proc_info_set_termination(ProcInfo0, Term1, 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(ModuleInfo0, PredTable,
ModuleInfo)
;
pred_info_context(PredInfo0, Context),
Res = error(Context -
not_subset(InVars2Bag, InVarsBag)),
ModuleInfo = ModuleInfo0
)
;
Offs = [],
Res = Res1,
ModuleInfo = ModuleInfo0
).
:- pred goal_inequality_used_args(list(var), bag(var), list(bool)).
:- mode goal_inequality_used_args(in, in, out) is det.
goal_inequality_used_args([], _InVarsBag, []).
goal_inequality_used_args([ Arg | Args ], InVarsBag, [ UsedArg | UsedArgs ]):-
( bag__contains(InVarsBag, Arg) ->
UsedArg = yes
;
UsedArg = no
),
goal_inequality_used_args(Args, InVarsBag, UsedArgs).
% goal_inequality_2 fails if it cannot form an inequality. i.e. there are
% horder calls, horder args, or pragma-c-code.
% The last two arguments are variables that hold the currently ground variables
% As the predicate moves through the goal, these variable-lists are modified
% as the ground variables change
:- pred goal_inequality_2(hlds_goal_expr, hlds_goal_info, module_info,
unify_info, pred_proc_id, list(term_pass1__equation),
term_util__result(term_error__error), bag(var), bag(var)).
:- mode goal_inequality_2(in, in, in, in, in, out, out, in, out) is det.
goal_inequality_2(conj([]), _, _Module, _, PPId, Offs, ok, Vars, Vars) :-
Offs = [eqn(set(0), PPId, [])].
goal_inequality_2(conj([ Goal | Goals ]), _GoalInfo, ModuleInfo, UnifyInfo,
PPId, Offs, Res, Vars0, Vars) :-
goal_inequality_2_conj(Goal, Goals, ModuleInfo, UnifyInfo, PPId,
Offs, Res, Vars0, Vars).
% this fails (returns Res=error) if:
% there are higher order arguments
% The terminates is 'dont_know'
% if terminates is 'dont_know' then, the called pred was imported,
% and may not terinate
% the termination constant is infinite
goal_inequality_2(call(CallPredId, CallProcId, Args, _IsBuiltin, _, _SymName),
GoalInfo, ModuleInfo, _UnifyInfo, PPId, Offs, Res, Vars0, Vars) :-
PPId = proc(PredId, ProcId),
CallPPId = proc(CallPredId, CallProcId),
module_info_pred_proc_info(ModuleInfo, PredId, ProcId, _PredInfo,
ProcInfo),
module_info_pred_proc_info(ModuleInfo, CallPredId,
CallProcId, _CallPredInfo, CallProcInfo),
goal_info_get_context(GoalInfo, Context),
proc_info_vartypes(ProcInfo, VarType),
proc_info_argmodes(CallProcInfo, CallArgModes),
proc_info_termination(CallProcInfo, CallTermination),
CallTermination = term(CallTermConst, CallTerminates, CallUsedArgs, _),
partition_call_args(ModuleInfo, CallArgModes, Args, InVars, OutVars),
bag__from_list(InVars, InVarsBag0),
bag__from_list(OutVars, OutVarsBag),
(
CallUsedArgs = yes(UsedVars)
->
remove_unused_args(InVarsBag0, Args, UsedVars,
InVarsBag1)
; %else if
(
PredId = CallPredId,
ProcId = CallProcId
)
->
% this is a directly recursive call. if a var is
% exactly the same in the head as the recursive call
% then it doesnt need to be in the InVarsBag, so
% remove it. If the var is an output var, then
% it wont get removed from the InVarsBag, as its not
% in there to begin with. NOTE this depends on the
% fact that the one var cannot be both input and output
% in a single call.
proc_info_headvars(CallProcInfo, CallArgs),
goal_inequality_2_call_2(InVarsBag0, Args, CallArgs,
InVarsBag1)
;
InVarsBag1 = InVarsBag0
),
( bag__intersect(Vars0, OutVarsBag) ->
( CallTerminates = dont_know ->
Res = error(Context - dont_know_proc_called(CallPPId)),
Vars = Vars0,
Offs = []
; \+ check_horder_args(Args, VarType) ->
Res = error(Context - horder_args(CallPPId)),
Vars = Vars0,
Offs = []
;
% if control reaches here, then there are no horder
% args, and pred is not imported
bag__subtract(Vars0, OutVarsBag, Vars1),
bag__union(Vars1, InVarsBag1, Vars),
(
CallTermConst = not_set,
Res = ok,
Offs = [eqn(set(0), PPId, [CallPPId])]
;
CallTermConst = set(Int),
Res = ok,
Offs = [eqn(set(Int), PPId, [])]
;
CallTermConst = inf(_),
Offs = [],
Res = error(Context -
inf_termination_const(CallPPId))
)
)
;
Offs = [],
Res = ok,
Vars = Vars0
).
goal_inequality_2(higher_order_call(_, _, _, _, _),
GoalInfo, _ModuleInfo, _, _PPId, [], Error, Vars, Vars) :-
goal_info_get_context(GoalInfo, Context),
Error = error(Context - horder_call).
goal_inequality_2(switch(SwitchVar, _CanFail, Cases, _StoreMap),
GoalInfo, ModuleInfo, UnifyInfo, PPId, Offs, Res, Vars0, Vars) :-
goal_inequality_2_switch(Cases, SwitchVar, GoalInfo, ModuleInfo,
UnifyInfo, PPId, Offs, Res, Vars0, Vars).
goal_inequality_2(unify(_Var, _RHS, _UnifyMode, Unification, _UnifyContext),
_GoalInfo, Module, FunctorAlg, PPId, Offs, ok, Vars0, Vars) :-
(
Unification = construct(OutVar, ConsId, Args, UniModes),
split_unification_vars(Args, UniModes, Module,
InVarsBag , OutVarsBag),
bag__insert(OutVarsBag, OutVar, OutVarsBag0),
( bag__intersect(Vars0, OutVarsBag0) ->
bag__subtract(Vars0, OutVarsBag0, Vars1),
bag__union(Vars1, InVarsBag, Vars),
functor_norm(FunctorAlg, ConsId, Module,
FunctorNorm),
Offs = [eqn(set(FunctorNorm), PPId, [])]
;
Vars0 = Vars,
Offs = []
)
;
Unification = deconstruct(InVar, ConsId, Args, UniModes, _),
split_unification_vars(Args, UniModes, Module,
InVarsBag , OutVarsBag),
bag__insert(InVarsBag, InVar, InVarsBag0),
( bag__intersect(Vars0, OutVarsBag) ->
bag__subtract(Vars0, OutVarsBag, Vars1),
bag__union(Vars1, InVarsBag0, Vars),
functor_norm(FunctorAlg, ConsId, Module,
FunctorNorm),
Offs = [eqn(set(- FunctorNorm), PPId, [])]
;
Offs = [eqn(set(0), PPId, [])],
Vars = Vars0
)
;
Unification = assign(OutVar, InVar),
( bag__remove(Vars0, OutVar, Vars1) ->
Offs = [eqn(set(0), PPId, [])],
bag__insert(Vars1, InVar, Vars)
;
Vars0 = Vars,
Offs = []
)
;
Unification = simple_test(_InVar1, _InVar2),
Vars0 = Vars,
Offs = []
;
Unification = complicated_unify(_, _),
error("Unexpected complicated_unify in termination.m"),
Vars0 = Vars,
Offs = []
).
goal_inequality_2(disj([], _), _, _Module, _, _PPId, [], ok, _Vars, Vars) :-
% no variables are bound in an empty disjunction (fail), so it
% does not make sense to define an equation relating input
% variables to output variables.
bag__init(Vars).
goal_inequality_2(disj([ Goal | Goals ], _StoreMap),
GoalInfo, Module, UnifyInfo, PPId, Offs, Res, Vars0, Vars) :-
goal_inequality_2_disj(Goal, Goals, GoalInfo, Module, UnifyInfo,
PPId, Offs, Res, Vars0, Vars).
% as we are trying to form a relationship between variables sizes, and no
% variables can be bound in a not, we dont need to evaluate inside the not
goal_inequality_2(not(_), _GoalInfo, _Module, _, _PPId, [], ok, _Vars, Vars) :-
bag__init(Vars).
goal_inequality_2(some(_Vars, GoalExpr - GoalInfo), _, ModuleInfo, UnifyInfo,
PPId, Offs, Res, Vars0, Vars) :-
goal_inequality_2(GoalExpr, GoalInfo, ModuleInfo, UnifyInfo,
PPId, Offs, Res, Vars0, Vars).
goal_inequality_2(if_then_else(_Vars, IfGoal, ThenGoal, ElseGoal, _StoreMap),
GoalInfo, ModuleInfo, UnifyInfo, PPId, Offs,
Res, Vars0, Vars) :-
IfGoal = IfGoalExpr - IfGoalInfo,
ThenGoal = ThenGoalExpr - ThenGoalInfo,
ElseGoal = ElseGoalExpr - ElseGoalInfo,
goal_inequality_2(ThenGoalExpr, ThenGoalInfo, ModuleInfo, UnifyInfo,
PPId, Offs0, Res0, Vars0, Vars1),
goal_inequality_2(ElseGoalExpr, ElseGoalInfo, ModuleInfo, UnifyInfo,
PPId, Offs1, Res1, Vars0, Vars2),
( Res0 = error(_) ->
Res = Res0,
Vars = Vars1,
Offs = Offs0
; Res1 = error(_) ->
Res = Res1,
Vars = Vars2,
Offs = Offs1
; bag__subset_compare(VarRes, Vars1, Vars2) ->
( VarRes = (<) ->
Vars3 = Vars2
;
Vars3 = Vars1
),
goal_inequality_2(IfGoalExpr, IfGoalInfo, ModuleInfo,
UnifyInfo, PPId, Offs2, Res, Vars3, Vars),
( Res = error(_) ->
Offs = Offs2
;
join_offsets(Offs0, Offs2, Offs3),
join_offsets(Offs1, Offs2, Offs4),
list__append(Offs3, Offs4, Offs)
)
;
goal_info_get_context(GoalInfo, Context),
Res = error(Context - ite_wrong_vars(Vars1, Vars2)),
Vars = Vars0,
Offs = []
).
goal_inequality_2(pragma_c_code(_, _, CallPredId, CallProcId, Args, _, _),
GoalInfo, Module, _UnifyInfo, _PPId, [], Res, Vars, Vars) :-
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_argmodes(CallProcInfo, CallArgModes),
partition_call_args(Module, CallArgModes, Args, _InVars, OutVars),
bag__from_list(OutVars, OutVarBag),
( bag__intersect(Vars, OutVarBag) ->
goal_info_get_context(GoalInfo, Context),
Res = error(Context - pragma_c_code)
;
% c_code has no important output vars, so we need no error
Res = ok
).
%-----------------------------------------------------------------------------%
:- pred goal_inequality_2_conj(hlds_goal, list(hlds_goal),
module_info, unify_info, pred_proc_id, list(term_pass1__equation),
term_util__result(term_error__error), bag(var), bag(var)).
:- mode goal_inequality_2_conj(in, in, in, in, in, out, out, in, out) is det.
goal_inequality_2_conj(Goal, [], ModuleInfo, UnifyInfo, PPId, Offs, Res,
Vars0, Vars) :-
Goal = GoalExpr - GoalInfo,
goal_inequality_2(GoalExpr, GoalInfo, ModuleInfo, UnifyInfo,
PPId, Offs, Res, Vars0, Vars).
goal_inequality_2_conj(Goal, [ Goal2 | Goals ], ModuleInfo, UnifyInfo, PPId,
Offs, Res, Vars0, Vars) :-
goal_inequality_2_conj(Goal2, Goals, ModuleInfo, UnifyInfo,
PPId, Offs0, Res1 , Vars0, Vars1),
( Res1 = ok ->
Goal = GoalExpr - GoalInfo,
goal_inequality_2(GoalExpr, GoalInfo, ModuleInfo, UnifyInfo,
PPId, Offs1, Res, Vars1, Vars),
join_offsets(Offs0, Offs1, Offs)
;
Res = Res1,
Vars = Vars1,
Offs = Offs0
).
% Removes from the InVarsBag variables that have not changed between the
% head, and the recursive call.
% bar(A, B, C) :-
% ...
% bar(D, B, A)
% ...
% HeadArgs = [A, B, C], CallArgs = [D, B, A].
% in this case remove B from InVarsBag
:- pred goal_inequality_2_call_2(bag(var), list(var), list(var), bag(var)).
:- mode goal_inequality_2_call_2(in, in, in, out) is det.
goal_inequality_2_call_2(Vars, [], [], Vars).
goal_inequality_2_call_2(Vars, [], [_|_], Vars) :-
error("Unmatched vars in termination.m").
goal_inequality_2_call_2(Vars, [_|_], [], Vars) :-
error("Unmatched vars in termination.m").
goal_inequality_2_call_2(Vars0, [ Call | Calls ], [Head | Heads ], Vars) :-
( Call = Head ->
% Call/Head are the same, so remove them from Vars
% Whenever Call/Head is an output var, it will not
% be in Vars, as Vars is InVarsBag.
bag__delete(Vars0, Call, Vars1)
;
Vars1 = Vars0
),
goal_inequality_2_call_2(Vars1, Calls, Heads, Vars).
:- pred goal_inequality_2_switch(list(case), var, hlds_goal_info,
module_info, unify_info, pred_proc_id, list(term_pass1__equation),
term_util__result(term_error__error), bag(var), bag(var)).
:- mode goal_inequality_2_switch(in, in, in, in, in, in, out, out,
in, out) is det.
goal_inequality_2_switch([], _, _, _ModuleInfo, _, _PPId,
[], ok, Vars, Vars) :-
error("Unexpected empty switch").
goal_inequality_2_switch([ Case | Cases ], SwitchVar, SwitchGoalInfo,
Module, UnifyInfo, PPId, Offs, Res, Vars0, Vars) :-
Case = case(_ConsId, Goal),
Goal = GoalExpr - GoalInfo,
goal_inequality_2(GoalExpr, GoalInfo, Module, UnifyInfo,
PPId, Offs1, Res1, Vars0, Vars1),
( Res1 = error(_) ->
Res = Res1,
Vars = Vars1,
Offs = Offs1
; Cases = [] ->
Res = Res1,
Vars = Vars1,
Offs = Offs1
;
goal_inequality_2_switch(Cases, SwitchVar, SwitchGoalInfo,
Module, UnifyInfo, PPId, Offs2, Res2, Vars0, Vars2),
( Res2 = error(_) ->
Res = Res2,
Vars = Vars2,
Offs = Offs2
; bag__subset_compare(VarRes, Vars1, Vars2) ->
list__append(Offs1, Offs2, Offs),
( VarRes = (<) ->
Vars = Vars2
;
Vars = Vars1
),
Res = ok
;
goal_info_get_context(GoalInfo, Context),
Res = error(Context - switch_wrong_vars(Vars1, Vars2)),
Vars = Vars0,
Offs = []
)
).
:- pred goal_inequality_2_disj(hlds_goal, list(hlds_goal), hlds_goal_info,
module_info, unify_info, pred_proc_id, list(term_pass1__equation),
term_util__result(term_error__error), bag(var), bag(var)).
:- mode goal_inequality_2_disj(in, in, in, in, in, in, out, out,
in, out) is det.
goal_inequality_2_disj(Goal, [], _, Module, UnifyInfo, PPId,
Offs, Res, Vars0, Vars) :-
Goal = GoalExpr - GoalInfo,
goal_inequality_2(GoalExpr, GoalInfo, Module, UnifyInfo,
PPId, Offs, Res, Vars0, Vars).
goal_inequality_2_disj(Goal, [Goal2 | Goals], DisjGoalInfo, Module,
UnifyInfo, PPId, Offs, Res, Vars0, Vars) :-
goal_inequality_2_disj(Goal2, Goals, DisjGoalInfo, Module,
UnifyInfo, PPId, Offs1, Res1, Vars0, Vars1),
Goal = GoalExpr - GoalInfo,
goal_inequality_2(GoalExpr, GoalInfo, Module, UnifyInfo,
PPId, Offs2, Res2, Vars0, Vars2),
( Res1 = error(_) ->
Res = Res1,
Vars = Vars1,
Offs = Offs1
; Res2 = error(_) ->
Res = Res2,
Vars = Vars2,
Offs = Offs2
; bag__subset_compare(VarRes, Vars1, Vars2) ->
( VarRes = (<) ->
Vars = Vars2
;
Vars = Vars1
),
list__append(Offs1, Offs2, Offs),
Res = ok
;
goal_info_get_context(DisjGoalInfo, Context),
Res = error(Context - disj_wrong_vars(Vars1, Vars2)),
Vars = Vars0,
Offs = []
).
%-----------------------------------------------------------------------------%
% support functions for goal_inequality
:- pred join_offsets(list(term_pass1__equation), list(term_pass1__equation),
list(term_pass1__equation)).
:- mode join_offsets(in, in, out) is det.
join_offsets(In1, In2, Out) :-
( In2 = [] ->
Out = In1
;
(
In1 = [],
Out = In2
;
In1 = [X | Xs],
list__map(eqn_add(X), In2, Out1),
( Xs = [] ->
Out = Out1
;
join_offsets(Xs, In2, Out0),
list__append(Out0, Out1, Out)
)
%list__merge_and_remove_dups(Out0, Out1, Out)
)
).
% adds two equations together
:- pred eqn_add(term_pass1__equation, term_pass1__equation,
term_pass1__equation).
:- mode eqn_add(in, in, out) is det.
eqn_add(eqn(Const1, PPId1, PPList1), eqn(Const2, PPId2, PPList2), Out) :-
( PPId1 = PPId2 ->
( ( Const1 = not_set ; Const2 = not_set ) ->
OutConst = not_set
; ( Const1 = inf(_) ; Const2 = inf(_) ) ->
OutConst = inf(no)
; ( Const1 = set(Num1), Const2 = set(Num2)) ->
OutNum = Num1 + Num2,
OutConst = set(OutNum)
;
% This really cant happen, as Const1 and Const2 can
% only be (not_set ; inf ; set(int))
% as the disjunction is not flattened, mercury cant
% work it out, and would call the pred semidet
error("Internal software error in termination.m\n")
),
list__append(PPList1, PPList2, OutPPList),
Out = eqn(OutConst, PPId1, OutPPList)
;
% it makes no sense to add equations with different PPId
% values. Its like trying to add apples to oranges
error("termination:eqn_add was called with illegal arguments\n")
).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% Solve the list of constraints
% output is of the form required by lp_solve (not yet)
% which is : input = [eqn(Const, PPid, [PPidList])]
% max: .......
% c1: PPid - (PPidList) > Const;
% c2: PPid - (PPidList) > Const;
% where PPid (proc(PredId, ProcId)) is printed as ' aPredId_ProcId '
%
:- pred solve_eqns(list(term_pass1__equation), list(pred_proc_id), eqn_soln,
io__state, io__state).
:- mode solve_eqns(in, in, out, di, uo) is det.
solve_eqns(Equations, PPIds, Soln) -->
io__progname_base("termination.m", ProgName),
io__tmpnam(ConstraintFile),
io__tmpnam(OutputFile),
solve_eqns_constraint_file(Equations, PPIds, ConstraintFile,
ConstraintSucc),
( { ConstraintSucc = yes } ->
% run lp_solve
io__get_environment_var("LPSOLVE", Lpsolve0),
( { Lpsolve0 = yes(Lpsolve1) } ->
{ Lpsolve = Lpsolve1 }
;
{ Lpsolve = "lp_solve" }
),
{ string__append_list([
Lpsolve,
" <",
ConstraintFile,
" > ",
OutputFile], Command) },
io__call_system(Command, Res0),
% Test the return value
(
{ Res0 = ok(RetVal) },
{ lpsolve_ret_val(RetVal, Result) },
( { Result = optimal } ->
% Wohoo, lp_solve worked out an answer!!
solve_eqns_output_file(OutputFile, Soln0),
( { Soln0 = solved(_) } ->
[]
;
io__write_string("solve_eqns_parse_output_file failed on the following file:\n"),
{ string__append_list([
"cat ",
OutputFile,
" ",
ConstraintFile], Command1) },
io__call_system(Command1, _RetVal),
io__write_string("----------- end of file --------\n")
)
;
% Damn, it failed, interpret result,
% and were done
io__write_string("lp_solve failed on the following input file:\n"),
{ string__append_list([
"cat ",
ConstraintFile], Command1) },
io__call_system(Command1, _RetVal),
io__write_string("----------- end of file --------\n"),
{ Soln0 = Result }
)
;
{ Res0 = error(Error0) },
{ io__error_message(Error0, Msg0) },
io__write_strings([
ProgName,
": Error with system call `",
Command,
"' : ",
Msg0,
"\n" ]),
io__set_exit_status(1),
{ Soln0 = fatal_error }
),
% dont forget to close, and delete files!!
io__remove_file(ConstraintFile, Res1),
( { Res1 = error(Error1) } ->
{ io__error_message(Error1, Msg1) },
io__write_strings([
ProgName,
": Error unlinking temporary file `",
ConstraintFile,
"' : ",
Msg1,
"\n" ]),
io__set_exit_status(1),
{ Soln1 = fatal_error }
;
{ Soln1 = Soln0 }
),
io__remove_file(OutputFile, Res2),
( { Res2 = error(Error2) } ->
{ io__error_message(Error2, Msg2) },
io__write_strings([
"Error unlinking temporary file `",
OutputFile,
"' : ",
Msg2,
"\n" ]),
io__set_exit_status(1),
{ Soln = fatal_error }
;
{ Soln = Soln1 }
)
;
% failed to make constraint file
{ Soln = fatal_error }
).
% this really shouldnt be called with Equations=[].
:- pred solve_eqns_constraint_file(list(term_pass1__equation),
list(pred_proc_id), string, bool, io__state, io__state).
:- mode solve_eqns_constraint_file(in, in, in, out, di, uo) is det.
solve_eqns_constraint_file(Equations, PPIds, ConstraintFile, Success) -->
io__open_output(ConstraintFile, Res),
( { Res = error(Error) },
% error message and quit
io__progname_base("termination.m", ProgName),
{ io__error_message(Error, Msg) },
io__write_string(ProgName),
io__write_string(": cannot open temporary file `"),
io__write_string(ConstraintFile),
io__write_string("' for output: "),
io__write_string(Msg),
io__write_string("\n"),
io__set_exit_status(1),
{ Success = no }
;
{ Res = ok(Stream) },
( { Equations = [] } ->
{ Success = no }
;
io__set_output_stream(Stream, OldStream),
% create the constraint file
output_eqns(Equations, PPIds, Success),
io__set_output_stream(OldStream, _),
io__close_output(Stream)
)
).
:- pred solve_eqns_output_file(string, eqn_soln, io__state, io__state).
:- mode solve_eqns_output_file(in, out, di, uo) is det.
solve_eqns_output_file(OutputFile, Soln) -->
% Wohoo, lp_solve worked out an answer!!
io__open_input(OutputFile, OutputRes),
( { OutputRes = error(Error) },
io__progname_base("termination.m", ProgName),
{ io__error_message(Error, Msg) },
io__write_string(ProgName),
io__write_string(": cannot open temporary file `"),
io__write_string(OutputFile),
io__write_string("' for input: "),
io__write_string(Msg),
io__write_string("\n"),
io__set_exit_status(1),
{ Soln = fatal_error }
;
{ OutputRes = ok(Stream) },
io__set_input_stream(Stream, OldStream),
% need to interpret it now
solve_eqns_parse_output_file(Soln),
io__set_input_stream(OldStream, _),
io__close_input(Stream)
).
:- pred solve_eqns_parse_output_file(eqn_soln, io__state, io__state).
:- mode solve_eqns_parse_output_file(out, di, uo) is det.
solve_eqns_parse_output_file(Soln) -->
io__read_line(Res1),
( { Res1 = ok(_) } ->
solve_eqns_parse_output_file_2(Soln0, MaybeBVal),
( { Soln0 = solved(Result0) } ->
( { MaybeBVal = yes(BVal) } ->
{ solve_eqns_output_file_2(Result0, BVal,
Result) },
{ Soln = solved(Result) }
;
io__write_string("no bval\n"),
{ Soln = parse_error }
)
;
io__write_string(
"parse_output_file returned not solved\n"),
{ Soln = parse_error }
)
;
{ Soln = parse_error }
).
:- pred solve_eqns_output_file_2(list(pair(pred_proc_id, int)), int,
list(pair(pred_proc_id, int))).
:- mode solve_eqns_output_file_2(in, in, out) is det.
solve_eqns_output_file_2([], _, []).
solve_eqns_output_file_2([X | Xs], BVal, [Y | Ys]) :-
X = PPId - XVal, % pair deconstruction
YVal = XVal - BVal, % subtraction
Y = PPId - YVal, % pair construction
solve_eqns_output_file_2(Xs, BVal, Ys).
:- pred solve_eqns_parse_output_file_2(eqn_soln, maybe(int), io__state,
io__state).
:- mode solve_eqns_parse_output_file_2(out, out, di, uo) is det.
solve_eqns_parse_output_file_2(Soln, BVal) -->
io__read_line(Res1),
( { Res1 = ok([ X | Xs ]) } ->
(
{ X = 'a' },
{ char_list_remove_int(Xs, PredInt, Xs1) },
{ Xs1 = [ '_' | Xs2 ] },
{ char_list_remove_int(Xs2, ProcInt, Xs3) },
{ char_list_remove_whitespace(Xs3, Xs4) },
{ char_list_remove_int(Xs4, Value, _Xs5) }
->
% have found a soln
{ pred_id_to_int(PredId, PredInt) },
{ proc_id_to_int(ProcId, ProcInt) },
solve_eqns_parse_output_file_2(Soln0, BVal),
( { Soln0 = solved(SolnList) } ->
{ NewSoln = proc(PredId, ProcId) - Value },
{ Soln = solved([NewSoln | SolnList ]) }
;
{ Soln = Soln0 }
)
;
{ X = 'b' },
{ char_list_remove_whitespace(Xs, Xs1) },
{ char_list_remove_int(Xs1, Value, _Xs2) }
->
solve_eqns_parse_output_file_2(Soln, _Bval),
{ BVal = yes(Value) }
;
{ Soln = parse_error },
{ BVal = no }
)
; { Res1 = eof } ->
{ Soln = solved([]) },
{ BVal = no }
;
{ Soln = parse_error },
{ BVal = no }
).
:- pred char_list_remove_int(list(char), int, list(char)).
:- mode char_list_remove_int(in, out, out) is semidet.
char_list_remove_int([X | Xs], Int, ListOut) :-
char__is_digit(X),
char__to_int(X, Int0),
Int1 = Int0 - 48, % char__to_int('0', 48).
char_list_remove_int_2(Xs, Int1, Int, ListOut).
:- pred char_list_remove_int_2(list(char), int, int, list(char)).
:- mode char_list_remove_int_2(in, in, out, out) is semidet.
char_list_remove_int_2([], Int, Int, []).
char_list_remove_int_2([X | Xs], Int0, Int, ListOut) :-
( char__is_digit(X) ->
char__to_int(X, Int1),
Int2 = Int0 * 10 + Int1 - 48,
char_list_remove_int_2(Xs, Int2, Int, ListOut)
;
ListOut = [ X | Xs ],
Int = Int0
).
:- pred char_list_remove_whitespace(list(char), list(char)).
:- mode char_list_remove_whitespace(in, out) is det.
char_list_remove_whitespace([], []).
char_list_remove_whitespace([ X | Xs ], Out) :-
( char__is_whitespace(X) ->
char_list_remove_whitespace(Xs, Out)
;
Out = [ X | Xs ]
).
:- pred lpsolve_ret_val(int, eqn_soln).
:- mode lpsolve_ret_val(in, out) is det.
lpsolve_ret_val(Int, Result) :-
( Int = -1 -> Result = fatal_error
; Int = 0 -> Result = optimal
; Int = 1 -> Result = failure
; Int = 2 -> Result = infeasible
; Int = 3 -> Result = unbounded
; Int = 4 -> Result = failure
; Int = 5 -> Result = failure
; Result = failure
).
%-----------------------------------------------------------------------------%
:- pred output_eqns(list(term_pass1__equation), list(pred_proc_id),
bool, io__state , io__state).
:- mode output_eqns(in, in, out, di, uo) is det.
output_eqns(Xs, PPIds, Success) -->
% output: 'max: # b - PPIds'
io__write_string("max: "),
{ list__length(PPIds, Length) },
io__write_int(Length),
io__write_string(" b "),
output_eqn_2(PPIds),
io__write_string(";\n"),
output_eqns_2(Xs, 1, Success).
:- pred output_eqns_2(list(term_pass1__equation), int,
bool, io__state , io__state).
:- mode output_eqns_2(in, in, out, di, uo) is det.
output_eqns_2([], _Count, yes) --> [].
output_eqns_2([ X | Xs ], Count, Succ) -->
output_eqn(X, Count, Succ0),
( { Succ0 = yes } ->
{ Count1 is Count + 1 },
output_eqns_2(Xs, Count1, Succ)
;
{ Succ = Succ0 }
).
:- pred output_eqn(term_pass1__equation, int, bool, io__state,
io__state).
:- mode output_eqn(in, in, out, di, uo) is det.
% each constraint is of the form:
% c#: # b + PPId - (PPIdList) > Const;
% each PPId is printed as `aPredId_ProcId'
% As each PPId can be negative, and lp_solve allows only positive
% variables, we introduce a dummy variable 'b' such that
% Actual PPId value = returned PPId value - b, where the returned value is
% always non-negative
output_eqn(Eqn, Count, Succ) -->
{ Eqn = eqn(Const, PPId, PPIdList0) },
( { list__delete_first(PPIdList0, PPId, PPIdList1) } ->
{ Deleted = yes },
{ PPIdList = PPIdList1 }
;
{ Deleted = no },
{ PPIdList = PPIdList0 }
),
{ list__length(PPIdList, Length) },
(
{ Length = 0 },
{ Deleted = yes }
->
% nothing on the LHS of the constraint
{ Succ = no} % XXX is this correct, or should we return
% the fact that we didnt output a constraint
% currently if we dont print out any constraints
% then lp_solve fails.
;
( { Deleted = yes } ->
{ Length1 = Length }
;
{ Length1 = Length - 1}
),
% output 'c#: '
io__write_char('c'),
io__write_int(Count),
io__write_string(": "),
% maybe output '# b '
( { Length1 = 0 } ->
[]
;
io__write_int(Length1),
io__write_string(" b ")
),
% maybe output ' + PPId'
( { Deleted = yes } ->
[]
;
io__write_string(" + a"),
output_eqn_ppid(PPId)
),
% output 'PPIdList > Const;'
output_eqn_2(PPIdList),
io__write_string(" > "),
( { Const = set(Int) } ->
io__write_int(Int),
{ Succ = yes }
;
{ Succ = no }
),
io__write_string(";\n")
).
% outputs each of the PPId's in the form: ' - aPredId_ProcId'
:- pred output_eqn_2(list(pred_proc_id), io__state, io__state).
:- mode output_eqn_2(in, di, uo) is det.
output_eqn_2([]) --> [].
output_eqn_2([ X | Xs ]) -->
io__write_string(" - a"),
output_eqn_ppid(X),
output_eqn_2(Xs).
% outputs a PPId in the form "PredId_ProcId"
:- pred output_eqn_ppid(pred_proc_id, io__state, io__state).
:- mode output_eqn_ppid(in, di, uo) is det.
output_eqn_ppid(proc(PredId, ProcId)) -->
{ pred_id_to_int(PredId, PredInt) },
{ proc_id_to_int(ProcId, ProcInt) },
io__write_int(PredInt),
io__write_char('_'),
io__write_int(ProcInt).
%-----------------------------------------------------------------------------
%
% Copyright (C) 1995 University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------
%
% term_pass2.m
% Main author: crs.
%
% This file contains the actual termination analysis. This file goes
% through each procedure, and sets the terminates property of each one.
%
% Termination analysis:
% This goes through each of the SCC's in turn, analysing them to determine
% which predicates terminate.
%
%-----------------------------------------------------------------------------
:- module term_pass2.
:- interface.
:- import_module io, hlds_module.
:- pred termination(module_info, module_info, io__state, io__state).
:- mode termination(in, out, di, uo) is det.
:- implementation.
:- import_module bag, hlds_pred, std_util, int, list, relation, require.
:- import_module set, hlds_goal, term_util, term_error, bool.
:- import_module globals, options.
% used in termination_3_goal to keep track of the relative sizes of variables
% between the head of a pred and any recursive calls.
% the last argument is only used when doing single argument analysis. It
% stores which headvar was initially placed in this tuple.
:- type termination_3
---> tuple(pred_proc_id, % The called proc
int, % the relative size of the active
% vars, in comparison with the
% recursive call
bag(var), % tha bag of active vars
maybe(var), % only for single arg. analysis
% stores which headvar is being
% traced by this tuple
term__context). % Where the call occured
termination(Module0, Module) -->
{ module_info_dependency_info(Module0, DependencyInfo) },
{ hlds_dependency_info_get_dependency_ordering(DependencyInfo,
DependencyOrdering) },
termination_2(Module0, DependencyOrdering, Module).
:- pred termination_2(module_info, dependency_ordering, module_info, io__state,
io__state).
:- mode termination_2(in, in, out, di, uo) is det.
termination_2(Module, [], Module) --> [].
termination_2(Module0, [SCC | SCCs], Module) -->
% YYY
%{ c_puts("termination_2") },
termination_2_check_terminates(SCC, SCC, Module0, Module1, Succ),
( { Succ = yes } ->
% need to run termination checking
% initialise the relation
{ relation__init(Relation0) },
% add each proc to the relation
{ add_pred_procs_to_relation(SCC, Relation0, Relation1) },
% go and analyse the SCC
{ termination_3(SCC, Module1, Res, Relation1, Relation2) },
(
{ Res = ok },
% check that the relation returned is a dag
% and set termination accordingly
( { relation__tsort(Relation2, _) } ->
%{ c_puts("Tsort success") },
% yeah, all the procs in this SCC terminate
% set all procs to yes
{ set_pred_proc_ids_terminates(SCC,
yes, no, Module1, Module3) }
;
%{ c_puts("Tsort fail") },
% damn, need to set all the procs to dont_know
( { SCC = [ proc(PredId, _) | _ ] } ->
{ module_info_pred_info(Module1,
PredId, PredInfo) },
{ pred_info_context(PredInfo,
Context) }
;
{ term__context_init(Context) }
),
termination_3_single_args(SCC,
Context - not_dag, Module1, Module3)
)
;
{ Res = error(Error) },
%term_error__output(yes(PredId), Module1, Error),
termination_3_single_args(SCC, Error, Module1, Module3)
)
;
% all the termination properties are already set
{ Module3 = Module0 }
),
% recurse
termination_2(Module3, SCCs, Module).
% if this pred returns Succ = yes, then termination analysis needs to be
% run on this SCC. If it returns Succ = no, then the termination
% properties of this SCC have already been set.
:- pred termination_2_check_terminates(list(pred_proc_id), list(pred_proc_id),
module_info, module_info, bool, io__state, io__state).
:- mode termination_2_check_terminates(in, in, in, out, out, di, uo) is det.
termination_2_check_terminates([], _SCC, Module, Module, no) --> [].
termination_2_check_terminates([ PPId | PPIds ], SCC,Module0, Module, Succ) -->
{ PPId = proc(PredId, ProcId) },
{ module_info_pred_proc_info(Module0, PredId, ProcId, _, ProcInfo) },
{ proc_info_termination(ProcInfo, Term) },
{ Term = term(_Const, Terminates, _UsedArgs, MaybeError) },
(
{ Terminates = not_set },
{ Succ = yes },
{ Module = Module0 }
;
{ Terminates = yes },
termination_2_check_terminates(PPIds, SCC, Module0,
Module, Succ)
;
{ Terminates = dont_know},
{ Succ = no },
do_ppid_check_terminates(SCC, MaybeError, Module0,
Module)
).
:- pred termination_3(list(pred_proc_id), module_info,
term_util__result(term_error__error), relation(pred_proc_id),
relation(pred_proc_id)).
:- mode termination_3(in, in, out, in, out) is det.
termination_3([], _Module, ok, Relation, Relation).
termination_3([ PPId | PPIds ], Module, Result, Relation0, Relation) :-
% get goal info
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module, PredId, ProcId, PredInfo, ProcInfo),
proc_info_termination(ProcInfo, Termination),
( Termination = term(_Const, dont_know, _UsedArgs, _Error) ->
pred_info_context(PredInfo, Context),
Result = error(Context - dont_know_proc(PPId)),
Relation = Relation0
;
proc_info_goal(ProcInfo, Goal),
Goal = GoalExpr - GoalInfo,
% analyse goal info
termination_3_goal(GoalExpr, GoalInfo, Module, total,
call_info(PPId, Relation0, no), Res0, [], Out),
% get back list of ppid - size pairs
proc_info_argmodes(ProcInfo, ArgModes),
proc_info_headvars(ProcInfo, Args),
partition_call_args(Module, ArgModes, Args, InVars, _OutVars),
bag__from_list(InVars, InVarsBag),
( Res0 = ok ->
termination_3_add_arcs_to_relation(PPId, Out, InVarsBag,
Res1, Relation0, Relation1),
( Res1 = ok ->
termination_3(PPIds, Module, Result, Relation1,
Relation)
;
Relation = Relation0,
Result = Res1
)
;
Result = Res0,
Relation = Relation0
)
).
% this runs single argument analysis on the goal. This is only run if
% normal termination analysis failed.
:- pred termination_3_single_args(list(pred_proc_id), term_error__error,
module_info, module_info, io__state, io__state).
:- mode termination_3_single_args(in, in, in, out, di, uo) is det.
termination_3_single_args([], _, Module, Module) -->
{ error("termination.m: there should be at least 1 predicate in a SCC\n") }.
termination_3_single_args([PPId | Rest], Error, Module0, Module) -->
globals__io_lookup_bool_option(termination_single_args, SingleArgs),
{ SCC = [PPId | Rest] },
{ PPId = proc(PredId, ProcId) },
{ relation__init(Relation0) },
{ set__init(InitSet) },
(
{ SingleArgs = yes },
{ Rest = [] },
{ Error \= _ - dont_know_proc(_) }
% and Error=???
->
% can do single args
{ module_info_pred_proc_info(Module0, PredId, ProcId,
_PredInfo, ProcInfo) },
{ proc_info_goal(ProcInfo, Goal) },
{ Goal = GoalExpr - GoalInfo },
{ termination_3_goal(GoalExpr, GoalInfo, Module0,
total, call_info(PPId, Relation0, yes), Res0,[],Out) },
( { Res0 = error(Error2) } ->
% just need a dummy context
{ Error = Context - _ },
{ Error3 = Context - single_arg_failed(Error, Error2) },
do_ppid_check_terminates(SCC, yes(Error3),
Module0, Module)
; { termination_3_single_2(Out, InitSet, InitSet) } ->
% yeah, single arg succeded
{ set_pred_proc_ids_terminates(SCC, yes, yes(Error),
Module0, Module) }
;
% single arg failed - bummer
{ Error = Context - _ },
{ Error2 = Context - single_arg_failed(Error) },
do_ppid_check_terminates(SCC, yes(Error2),
Module0, Module)
)
;
% cant do single args
do_ppid_check_terminates(SCC, yes(Error),
Module0, Module)
).
:- pred termination_3_single_2(list(termination_3), set(var), set(var)).
:- mode termination_3_single_2(in, in, in) is semidet.
termination_3_single_2([], NegSet, NonNegSet) :-
set__difference(NegSet, NonNegSet, DiffSet),
% check that there is at least 1 headvar that is always strictly
% decreasing
set__remove_least(DiffSet, _, _).
termination_3_single_2([Off | Offs], NegSet0, NonNegSet0) :-
Off = tuple(_, Int, VarBag0, MaybeVar, _Context),
(
MaybeVar = no,
error("termination.m: Maybevar should be yes in single argument analysis\n")
;
MaybeVar = yes(HeadVar),
(
Int < 0,
% check that the var that was recursed on did not
% changeplace between the head and recursive call.
% I am not sure if the first call is actually
% required to succeed
bag__remove(VarBag0, HeadVar, VarBag1),
\+ bag__remove_smallest(VarBag1, _, _)
->
set__insert(NegSet0, HeadVar, NegSet),
termination_3_single_2(Offs, NegSet, NonNegSet0)
;
set__insert(NonNegSet0, HeadVar, NonNegSet),
termination_3_single_2(Offs, NegSet0, NonNegSet)
)
).
% this adds the information from termination_3_goal to the relation.
% the relation is between the procs in the current SCC, with an arc showing
% that one proc calls another with the size of the variables unchanged between
% the head and the (possibly indirect) recursive call. Any loops in the
% relation show possible non-termination
% this also checks that the calculated input vars are subsets of the actual
% input vars
:- pred termination_3_add_arcs_to_relation(pred_proc_id, list(termination_3),
bag(var), term_util__result(term_error__error),
relation(pred_proc_id), relation(pred_proc_id)).
:- mode termination_3_add_arcs_to_relation(in, in, in, out, in, out) is det.
termination_3_add_arcs_to_relation(_PPid, [], _Vars, ok, Relation, Relation).
termination_3_add_arcs_to_relation(PPId, [X | Xs], Vars, Result, Relation0,
Relation) :-
X = tuple(CalledPPId, Value, Bag, _Var, Context),
( bag__is_subbag(Bag, Vars) ->
compare(Res, Value, 0),
(
Res = (>),
Result = error(Context -
positive_value(PPId, CalledPPId)),
Relation = Relation0
;
Res = (=),
% add to relation
relation__lookup_element(Relation0, PPId, Key),
relation__lookup_element(Relation0, CalledPPId,
CalledKey),
relation__add(Relation0, Key, CalledKey, Relation1),
termination_3_add_arcs_to_relation(PPId, Xs, Vars,
Result, Relation1, Relation)
;
Res = (<),
termination_3_add_arcs_to_relation(PPId, Xs, Vars,
Result, Relation0, Relation)
)
;
Result = error(Context - not_subset(Bag, Vars)),
Relation = Relation0
).
:- pred add_pred_procs_to_relation(list(pred_proc_id), relation(pred_proc_id),
relation(pred_proc_id)).
:- mode add_pred_procs_to_relation(in, in, out) is det.
add_pred_procs_to_relation([], Relation, Relation).
add_pred_procs_to_relation([PPId | PPIds], Relation0, Relation) :-
relation__add_element(Relation0, PPId, _, Relation1),
add_pred_procs_to_relation(PPIds, Relation1, Relation).
%-----------------------------------------------------------------------------%
% The relation that is passed in is a relation containing all of the procs
% in the current SCC. It is used to check whether a call is recursive or not.
:- type call_info --->
call_info(
pred_proc_id,
relation(pred_proc_id),
bool % are we doing single arg.
).
:- pred termination_3_goal(hlds_goal_expr, hlds_goal_info, module_info,
unify_info, call_info, term_util__result(term_error__error),
list(termination_3), list(termination_3)).
:- mode termination_3_goal(in, in, in, in, in, out, in, out) is det.
termination_3_goal(conj(Goals),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_3_goal_conj(Goals, Module, UnifyInfo, CallInfo, Res,
Out0, Out).
% termination_3_goal(call switches on the call_info argument as well.
termination_3_goal(call(CallPredId, CallProcId, Args, _IsBuiltin, _, _),
GoalInfo, Module, _UnifyInfo, call_info(PPId, Relation, no),
Res, Out0, Out) :-
PPId = proc(PredId, ProcId),
CallPPId = proc(CallPredId, CallProcId),
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_vartypes(ProcInfo, VarType),
proc_info_argmodes(CallProcInfo, CallArgModes),
proc_info_termination(CallProcInfo, CallTermination),
CallTermination = term(CallTermConst, CallTerminates, CallUsedArgs, _),
goal_info_get_context(GoalInfo, Context),
partition_call_args(Module, CallArgModes, Args, InVars, OutVars),
bag__from_list(InVars, InVarBag0),
bag__from_list(OutVars, OutVarBag),
( CallUsedArgs = yes(UsedVars) ->
remove_unused_args(InVarBag0, Args, UsedVars,
InVarBag1)
;
InVarBag1 = InVarBag0
),
% step 1 - modify Out0
(
CallTermConst = set(Int),
termination_3_modify_out(InVarBag1, OutVarBag, Int,
Out0, Out1),
Res0 = ok
;
CallTermConst = not_set,
error("Unexpected Termination Constant in termination.m"),
Res0 = ok,
Out1 = Out0
;
CallTermConst = inf(_),
( termination_3_check_intersect(Out0, OutVarBag) ->
% there is no intersection, so just continue
Res0 = ok
;
Res0 = error(Context - inf_termination_const(CallPPId))
),
Out1 = Out0
),
% step 2 - do we add another arc?
( CallTerminates = dont_know ->
Res = error(Context - dont_know_proc_called(CallPPId)),
Out = Out0
; \+ check_horder_args(Args, VarType) ->
Res = error(Context - horder_args(CallPPId)),
Out = Out0
;
( relation__search_element(Relation, CallPPId, _) ->
% the called proc is in the relation, so call is
% recursive - add it to Out
NewOutElem = tuple(CallPPId, 0, InVarBag0, no, Context),
Out = [ NewOutElem | Out1 ]
;
% The call is not recursive
Out = Out1
),
Res = Res0
).
termination_3_goal(call(CallPredId, CallProcId, Args, _IsBuiltin, _, _),
GoalInfo, Module, _UnifyInfo, call_info(PPId, _Relation, yes),
Res, Out0, Out) :-
PPId = proc(PredId, ProcId),
CallPPId = proc(CallPredId, CallProcId),
% could(should) do sanity check that PPId is the only PPId in
% Relation, but i dont see a reasonable way to do it.
module_info_pred_proc_info(Module, PredId, ProcId, _, ProcInfo),
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_vartypes(ProcInfo, VarType),
proc_info_argmodes(CallProcInfo, CallArgModes),
proc_info_headvars(CallProcInfo, HeadVars),
proc_info_termination(CallProcInfo, CallTermination),
CallTermination = term(_, CallTerminates, _CallUsedArgs, _),
goal_info_get_context(GoalInfo, Context),
partition_call_args(Module, CallArgModes, Args, InVars, OutVars),
partition_call_args(Module, CallArgModes, HeadVars, InHeadVars, _),
bag__from_list(OutVars, OutVarBag),
% step 1 - modify Out0
( termination_3_check_intersect(Out0, OutVarBag) ->
% there is no intersection, so just continue
Res0 = ok,
Out1 = Out0
;
% This analysis could be much better, but it will do for
% now.
Res0 = error(Context - call_in_single_arg(CallPPId)),
Out1 = Out0
),
% step 2 - do we add another arc?
( CallTerminates = dont_know ->
Res = error(Context - dont_know_proc_called(CallPPId)),
Out = Out0
; \+ check_horder_args(Args, VarType) ->
Res = error(Context - horder_args(CallPPId)),
Out = Out0
;
( CallPPId = PPId ->
% call is recursive - add it to Out
termination_3_goal_call(InVars, InHeadVars, PPId,
Context, Out1, Out)
;
% The call is not recursive
Out = Out1
),
Res = Res0
).
termination_3_goal(higher_order_call(_, _, _, _, _),
GoalInfo, _Module, _UnifyInfo, _CallInfo, Res, Out0, Out) :-
goal_info_get_context(GoalInfo, Context),
Res = error(Context - horder_call),
Out = Out0.
termination_3_goal(switch(_Var, _CanFail, Cases, _StoreMap),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_3_goal_switch(Cases, Module, UnifyInfo, CallInfo,
Res, Out0, Out).
termination_3_goal(unify(_Var, _RHS, _UniMode, Unification, _Context),
_GoalInfo, Module, FunctorAlg, _CallInfo, ok, Out0, Out) :-
bag__init(InitBag),
(
Unification = construct(OutVar, ConsId, Args, Modes),
split_unification_vars(Args, Modes, Module, InVarBag,
OutVarBag0),
bag__insert(OutVarBag0, OutVar, OutVarBag),
functor_norm(FunctorAlg, ConsId, Module, FunctorNorm),
termination_3_modify_out(InVarBag, OutVarBag,
FunctorNorm, Out0, Out)
;
Unification = deconstruct(InVar, ConsId, Args, Modes, _),
split_unification_vars(Args, Modes, Module, InVarBag0,
OutVarBag),
bag__insert(InVarBag0, InVar, InVarBag),
functor_norm(FunctorAlg, ConsId, Module, FunctorNorm),
termination_3_modify_out(InVarBag, OutVarBag,
(- FunctorNorm), Out0, Out)
;
Unification = assign(OutVar, InVar),
bag__insert(InitBag, InVar, InVarBag),
bag__insert(InitBag, OutVar, OutVarBag),
termination_3_modify_out(InVarBag, OutVarBag, 0, Out0, Out)
;
Unification = simple_test(_InVar1, _InVar2),
Out = Out0
;
Unification = complicated_unify(_, _),
error("Unexpected complicated_unify in termination.m"),
Out = Out0
).
termination_3_goal(disj(Goals, _StoreMap),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_3_goal_disj(Goals, Module, UnifyInfo, CallInfo, Res,
Out0, Out).
termination_3_goal(not(GoalExpr - GoalInfo),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_3_goal(GoalExpr, GoalInfo, Module, UnifyInfo, CallInfo,
Res, Out0, Out).
termination_3_goal(some(_Vars, GoalExpr - GoalInfo),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
termination_3_goal(GoalExpr, GoalInfo, Module, UnifyInfo, CallInfo,
Res, Out0, Out).
termination_3_goal(if_then_else(_Vars, CondGoal, ThenGoal, ElseGoal, _),
_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
CondGoal = CondExpr - CondGoalInfo,
ThenGoal = ThenExpr - ThenGoalInfo,
ElseGoal = ElseExpr - ElseGoalInfo,
termination_3_goal(ThenExpr, ThenGoalInfo, Module, UnifyInfo, CallInfo,
ThenRes, Out0, ThenOut),
termination_3_goal(ElseExpr, ElseGoalInfo, Module, UnifyInfo, CallInfo,
ElseRes, Out0, ElseOut),
( ThenRes = error(_) ->
Res = ThenRes,
Out = ThenOut
; ElseRes = error(_) ->
Res = ElseRes,
Out = ElseOut
;
% yeah, they both worked - join the outs
list__append(ThenOut, ElseOut, Out1),
termination_3_goal(CondExpr, CondGoalInfo, Module,
UnifyInfo, CallInfo, Res, Out1, Out)
).
termination_3_goal(pragma_c_code(_, _, CallPredId, CallProcId, Args, _, _),
GoalInfo, Module, _UnifyInfo, _CallInfo, Res, Out, Out) :-
module_info_pred_proc_info(Module, CallPredId, CallProcId, _,
CallProcInfo),
proc_info_argmodes(CallProcInfo, CallArgModes),
partition_call_args(Module, CallArgModes, Args, _InVars, OutVars),
bag__from_list(OutVars, OutVarBag),
( termination_3_check_intersect(Out, OutVarBag) ->
% c_code has no important output vars, so we need no error
Res = ok
;
goal_info_get_context(GoalInfo, Context),
Res = error(Context - pragma_c_code)
).
%-----------------------------------------------------------------------------%
% These following predicates all support termination_3_goal.
:- pred termination_3_goal_conj(list(hlds_goal), module_info,
unify_info, call_info, term_util__result(term_error__error),
list(termination_3), list(termination_3)).
:- mode termination_3_goal_conj(in, in, in, in, out, in, out) is det.
termination_3_goal_conj([] , _Module, _UnifyInfo, _CallInfo, ok, Out, Out).
termination_3_goal_conj([ Goal | Goals ], Module, UnifyInfo, CallInfo,
Res, Out0, Out) :-
Goal = GoalExpr - GoalInfo,
termination_3_goal_conj(Goals, Module, UnifyInfo, CallInfo,
Res0, Out0, Out1),
( Res0 = ok ->
termination_3_goal(GoalExpr, GoalInfo, Module,
UnifyInfo, CallInfo, Res, Out1, Out)
;
Res = Res0,
Out = Out1
).
:- pred termination_3_goal_call(list(var), list(var), pred_proc_id,
term__context, list(termination_3), list(termination_3)).
:- mode termination_3_goal_call(in, in, in, in, in, out) is det.
termination_3_goal_call([], [], _, _, Out, Out).
termination_3_goal_call([_|_], [], _, _, Out, Out) :-
error("Unmatched vars in termination_3_goal_call\n").
termination_3_goal_call([], [_|_], _, _, Out, Out) :-
error("Unmatched vars in termination_3_goal_call\n").
termination_3_goal_call([ Var | Vars ], [ HeadVar | HeadVars ], PPId,
Context, Outs0, Outs) :-
bag__init(Bag0),
bag__insert(Bag0, Var, Bag),
Out = tuple(PPId, 0, Bag, yes(HeadVar), Context),
termination_3_goal_call(Vars, HeadVars, PPId, Context,
[Out | Outs0], Outs).
:- pred termination_3_goal_switch(list(case), module_info,
unify_info, call_info, term_util__result(term_error__error),
list(termination_3), list(termination_3)).
:- mode termination_3_goal_switch(in, in, in, in, out, in, out) is det.
termination_3_goal_switch([] , _Module, _UnifyInfo, _CallInfo, ok, Out, Out).
termination_3_goal_switch([ Case | Cases ], Module, UnifyInfo,
CallInfo, Res, Out0, Out):-
Case = case(_, Goal),
Goal = GoalExpr - GoalInfo,
termination_3_goal_switch(Cases, Module, UnifyInfo, CallInfo,
Res0, Out0, Out1),
( Res0 = ok ->
termination_3_goal(GoalExpr, GoalInfo,
Module, UnifyInfo, CallInfo, Res, Out0, Out2),
list__append(Out1, Out2, Out)
;
Res = Res0,
Out = Out1
).
:- pred termination_3_goal_disj(list(hlds_goal), module_info,
unify_info, call_info, term_util__result(term_error__error),
list(termination_3), list(termination_3)).
:- mode termination_3_goal_disj(in, in, in, in, out, in, out) is det.
termination_3_goal_disj([] , _Module, _UnifyInfo, _CallInfo, ok, Out, Out):-
( Out = [] ->
true
;
error("why are variables bound after a fail???\n")
).
termination_3_goal_disj([ Goal | Goals ], Module, UnifyInfo,
CallInfo, Res, Out0, Out) :-
Goal = GoalExpr - GoalInfo,
termination_3_goal_disj(Goals, Module, UnifyInfo, CallInfo,
Res1, Out0, Out1),
( Res1 = ok ->
termination_3_goal(GoalExpr, GoalInfo, Module,
UnifyInfo, CallInfo, Res, Out0, Out2),
list__append(Out1, Out2, Out)
;
Res = Res1,
Out = Out1
).
:- pred termination_3_check_intersect(list(termination_3), bag(var)).
:- mode termination_3_check_intersect(in, in) is semidet.
% succeeds if there is no intersection between one of the Outs and the
% OutVarBag
termination_3_check_intersect([ ], _).
termination_3_check_intersect([ Out | Outs ], OutVarBag) :-
Out = tuple(_PPId, _Const, OutBag, _Var, _Context),
\+ bag__intersect(OutBag, OutVarBag),
termination_3_check_intersect(Outs, OutVarBag).
:- pred termination_3_modify_out(bag(var), bag(var), int, list(termination_3),
list(termination_3)).
:- mode termination_3_modify_out(in, in, in, in, out) is det.
termination_3_modify_out(_, _, _, [], []).
termination_3_modify_out(InVars, OutVars, Off, [Out0 | Out0s], [Out | Outs]):-
Out0 = tuple(PPId, Int0, Vars0, Var, Context),
( bag__intersect(OutVars, Vars0) ->
% there is an intersection
bag__subtract(Vars0, OutVars, Vars1),
bag__union(InVars, Vars1, Vars),
Int = Int0 + Off,
Out = tuple(PPId, Int, Vars, Var, Context)
;
% there is not an intersection
Out = Out0
),
termination_3_modify_out(InVars, OutVars, Off, Out0s, Outs).
%-----------------------------------------------------------------------------
%
% Copyright (C) 1995 University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------
%
% term_util.m
% Main author: crs.
%
% This file contains utilities that are used by termination analysis.
%
%-----------------------------------------------------------------------------
:- module term_util.
:- interface.
:- import_module list, bool, bag, int, hlds_module, hlds_pred, hlds_data.
:- import_module term_error, io, hlds_goal.
:- type termination
---> term(term_util__constant, terminates, maybe(list(bool)),
maybe(term_error__error)).
% the final list has a 1:1 correspondance with the arguments of the
% proc. it stores whether the arg is used in producing the
% output args.
% term_util__constant defines the level by which a predicates arguments
% grow or shrink. It is used to determine the termination properties of a
% predicate. The termination constant defines the relative sizes of input
% and output arguments in the following equation:
% | input arguments | + constant >= | output arguments |
% where | | represents a semilinear norm.
:- type term_util__constant
---> inf(maybe(term_error__error))
% could not find a limiting value
; not_set % Has not been set yet
; set(int). % has been set to int
:- type terminates
---> dont_know % cannot prove that the proc terminates
; not_set % the initial value of terminates for each proc
% the termination analysis uses the fact
% that if a proc is called, whose
% termination is not_set, then the call is
% mutually recursive. if the called proc
% is not recursive, then its termination
% will have already been set.
; yes. % YES this proc terminates for all possible
% inputs.
:- type functor_algorithm
---> simple % simple just assigns all functors a norm of 1
; total. % all functors have a norm = arity of functor
:- type term_util__result(T)
---> ok
; error(T).
:- type unify_info == functor_algorithm.
% This predicate is used to assign a norm (integer) to a functor, depending
% on its type.
:- pred functor_norm(functor_algorithm, cons_id, module_info, int).
:- mode functor_norm(in, in, in, out) is det.
% This predicate should be called whenever a procedure needs its termination
% set to dont_know. This predicate checks to see whether the termination
% is already set to dont_know, and if so it does nothing. If the
% termination is set to yes, or not_set, it changes the termination to
% dont_know, and checks whether a
% check_termination pragma has been defined for this predicate, and if so,
% this outputs a useful error message.
:- pred do_ppid_check_terminates(list(pred_proc_id), maybe(term_error__error),
module_info, module_info, io__state, io__state).
:- mode do_ppid_check_terminates(in, in, in, out, di, uo) is det.
%
:- pred term_util__make_bool_list(proc_info, list(bool), list(bool)).
:- mode term_util__make_bool_list(in, in, out) is det.
:- pred term_util__make_bool_list_2(list(var), list(bool), list(bool)).
:- mode term_util__make_bool_list_2(in, in, out) is det.
:- pred partition_call_args(module_info, list(mode),
list(var), list(var), list(var)).
:- mode partition_call_args(in, in, in, out, out) is det.
% removes vars from the InVarBag that are not used in the call
:- pred remove_unused_args(bag(var), list(var), list(bool), bag(var)).
:- mode remove_unused_args(in, in, in, out) is det.
:- pred set_pred_proc_ids_const(list(pred_proc_id), term_util__constant,
module_info, module_info).
:- mode set_pred_proc_ids_const(in, in, in, out) is det.
:- pred set_pred_proc_ids_terminates(list(pred_proc_id), terminates,
maybe(term_error__error), module_info, module_info).
:- mode set_pred_proc_ids_terminates(in, in, in, in, out) is det.
% Fails if one or more vars are higher order
:- pred check_horder_args(list(var), map(var, type)).
:- mode check_horder_args(in, in) is semidet.
:- pred split_unification_vars(list(var), list(uni_mode), module_info,
bag(var), bag(var)).
:- mode split_unification_vars(in, in, in, out, out) is det.
:- implementation.
:- import_module map, std_util, require, mode_util, prog_out, type_util.
split_unification_vars([], Modes, _ModuleInfo, Vars, Vars) :-
bag__init(Vars),
( Modes = [] ->
true
;
error("Error in termination.m")
).
split_unification_vars([Arg | Args], Modes, ModuleInfo,
InVars,OutVars):-
( Modes = [UniMode | UniModes] ->
split_unification_vars(Args, UniModes, ModuleInfo,
InVars0, OutVars0),
UniMode = ((_VarInit - ArgInit) -> (_VarFinal - ArgFinal)),
( %if
inst_is_bound(ModuleInfo, ArgInit)
->
(
% is input var
bag__insert(InVars0, Arg, InVars),
OutVars = OutVars0
)
; %elseif
(
inst_is_free(ModuleInfo, ArgInit),
inst_is_bound(ModuleInfo, ArgFinal)
)
->
%is outputvar
InVars = InVars0,
bag__insert(OutVars0, Arg, OutVars)
; %else
InVars = InVars0,
OutVars = OutVars0
)
;
error("Error in termination.m")
).
check_horder_args([], _).
check_horder_args([Arg | Args], VarType) :-
map__lookup(VarType, Arg, Type),
\+ type_is_higher_order(Type, _, _),
check_horder_args(Args, VarType).
set_pred_proc_ids_const([], _Const, Module, Module).
set_pred_proc_ids_const([PPId | PPIds], Const, Module0, Module) :-
PPId = proc(PredId, ProcId),
module_info_pred_proc_info(Module0, PredId, ProcId, PredInfo0,
ProcInfo0),
pred_info_procedures(PredInfo0, ProcTable0),
proc_info_termination(ProcInfo0, Termination0),
Termination0 = term(_Const, Term, UsedArgs, MaybeError),
Termination = term(Const, Term, UsedArgs, MaybeError),
% YYY
%c_put_term(PPId, Termination),
proc_info_set_termination(ProcInfo0, Termination, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
module_info_set_pred_info(Module0, PredId, PredInfo, Module1),
set_pred_proc_ids_const(PPIds, Const, Module1, Module).
set_pred_proc_ids_terminates([], _Terminates, _, Module, Module).
set_pred_proc_ids_terminates([PPId | PPIds], Terminates, MaybeError,
Module0, Module) :-
module_info_preds(Module0, PredTable0),
PPId = proc(PredId, ProcId),
map__lookup(PredTable0, PredId, PredInfo0),
pred_info_procedures(PredInfo0, ProcTable0),
map__lookup(ProcTable0, ProcId, ProcInfo0),
proc_info_termination(ProcInfo0, Termination0),
Termination0 = term(Const, _Terminates, UsedArgs, _),
Termination = term(Const, Terminates, UsedArgs, MaybeError),
% YYY
%c_put_term(PPId, Termination),
proc_info_set_termination(ProcInfo0, Termination, ProcInfo),
map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable),
pred_info_set_procedures(PredInfo0, ProcTable, PredInfo),
map__det_update(PredTable0, PredId, PredInfo, PredTable),
module_info_set_preds(Module0, PredTable, Module1),
set_pred_proc_ids_terminates(PPIds, Terminates, MaybeError,
Module1, Module).
remove_unused_args(Vars, [], [], Vars).
remove_unused_args(Vars, [], [_X | _Xs], Vars) :-
error("Unmatched Vars in termination.m").
remove_unused_args(Vars, [_X | _Xs], [], Vars) :-
error("Unmatched Vars in termination.m").
remove_unused_args(Vars0, [ Arg | Args ], [ UsedVar | UsedVars ], Vars) :-
( UsedVar = yes ->
% the var is used, so leave it
remove_unused_args(Vars0, Args, UsedVars, Vars)
;
% the var is not used in producing output vars, so dont
% include it as an input var
% UsedVar=no for all output vars, and bag__remove would
% fail on all output vars, as they wont be in InVarBag
bag__delete(Vars0, Arg, Vars1),
remove_unused_args(Vars1, Args, UsedVars, Vars)
).
partition_call_args(_, [], [_ | _], _, _) :-
error("partition_call_args").
partition_call_args(_, [_ | _], [], _, _) :-
error("partition_call_args").
partition_call_args(_, [], [], [], []).
partition_call_args(ModuleInfo, [ArgMode | ArgModes], [Arg | Args],
InputArgs, OutputArgs) :-
partition_call_args(ModuleInfo, ArgModes, Args,
InputArgs1, OutputArgs1),
( mode_is_input(ModuleInfo, ArgMode) ->
InputArgs = [Arg | InputArgs1],
OutputArgs = OutputArgs1
; mode_is_output(ModuleInfo, ArgMode) ->
InputArgs = InputArgs1,
OutputArgs = [Arg | OutputArgs1]
;
InputArgs = InputArgs1,
OutputArgs = OutputArgs1
).
term_util__make_bool_list(ProcInfo, Bools, Out) :-
proc_info_headvars(ProcInfo, HeadVars0),
list__length(Bools, Arity),
( list__drop(Arity, HeadVars0, HeadVars1) ->
HeadVars = HeadVars1
;
error("Unmatched variables in termination.m"),
HeadVars = HeadVars0
),
term_util__make_bool_list_2(HeadVars, Bools, Out).
term_util__make_bool_list_2([], Bools, Bools).
term_util__make_bool_list_2([ _ | Vars ], Bools, [no | Out]) :-
term_util__make_bool_list_2(Vars, Bools, Out).
functor_norm(simple, ConsId, _, Int) :-
(
ConsId = cons(_, Arity),
Arity \= 0
->
Int = 1
;
Int = 0
).
functor_norm(total, ConsId, _Module, Int) :-
( ConsId = cons(_, Arity) ->
Int = Arity
;
Int = 1
).
do_ppid_check_terminates([] , _MaybeError, Module, Module) --> [].
do_ppid_check_terminates([ PPId | PPIds ], MaybeError, Module0, Module) -->
% look up markers
{ PPId = proc(PredId, ProcId) },
{ module_info_preds(Module0, PredTable0) },
{ map__lookup(PredTable0, PredId, PredInfo0) },
{ pred_info_procedures(PredInfo0, ProcTable0) },
{ map__lookup(ProcTable0, ProcId, ProcInfo0) },
{ proc_info_termination(ProcInfo0, Termination0) },
{ Termination0 = term(Const, Terminates, UsedArgs, _) },
( { Terminates = dont_know } ->
{ Module2 = Module0 }
;
{ Termination = term(Const, dont_know, UsedArgs, MaybeError) },
{ proc_info_set_termination(ProcInfo0, Termination, ProcInfo)},
{ map__det_update(ProcTable0, ProcId, ProcInfo, ProcTable) },
{ pred_info_set_procedures(PredInfo0, ProcTable, PredInfo) },
{ map__det_update(PredTable0, PredId, PredInfo, PredTable) },
{ module_info_set_preds(Module0, PredTable, Module1) },
{ pred_info_get_marker_list(PredInfo, MarkerList) },
% if check_terminates exists, print out error
( { list__member(request(check_termination), MarkerList) } ->
( { MaybeError = yes(Error) } ->
term_error__output(yes(PredId), Module1, Error)
;
% this really shouldnt happen. The only
% time that MaybeError is no should be if
% the pred is imported, and imported preds
% with check_termination defined on them
% should have termnates set to yes.
{ pred_info_context(PredInfo, Context) },
prog_out__write_context(Context),
io__write_string(
"Unable to check termination\n")
),
{ module_info_incr_errors(Module1, Module2) },
io__set_exit_status(1)
;
{ Module2 = Module0 }
)
),
do_ppid_check_terminates(PPIds, MaybeError, Module2, Module).
%-----------------------------------------------------------------------------%
%
% Copyright (C) 1995 University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%
%
% term_error.m
% Main author: crs.
%
% This module prints out the various error messages that are produced by
% termination.m
%
%-----------------------------------------------------------------------------%
:- module term_error.
:- interface.
:- import_module io, hlds_module.
:- import_module bag, termination, std_util.
% This pred currently has 2 purposes. The first is for printing normal error
% messages. These are printed if a pragma check_termination has been
% defined for that predicate. If so, then term_error__output should be
% called with the first argument as yes(PredId) where PredId is the
% predicate that had the check_termination pragma defined for it. By
% calling it this way, the error messages that are printed out are much
% more detailed. The other use is in printing out the HLDS, this is done
% by setting the first argument to no, which causes a much more concise
% printout. Perhaps it would be better to have 2 seperate predicates
:- pred term_error__output(maybe(pred_id), module_info,
term_error__error, io__state, io__state).
:- mode term_error__output(in, in, in, di, uo) is det.
:- type term_error__error == pair(term__context, termination_error).
:- type termination_error
---> positive_value(pred_proc_id, pred_proc_id)
% a recursive call is made with variables that are
% strictly larger than in the head. note that
% the recursive call may be indirect, so this does
% not neccessarily indicate non-termination.
% The first PPId is the calling proc. The second
% PPId is the called proc, and the context is the
% line where the call occurs.
; not_subset(bag(var), bag(var))
; horder_call
; pragma_c_code
; dont_know_proc(pred_proc_id)
; dont_know_proc_called(pred_proc_id)
; horder_args(pred_proc_id)
; inf_termination_const(pred_proc_id)
; ite_wrong_vars(bag(var), bag(var))
; switch_wrong_vars(bag(var), bag(var))
; disj_wrong_vars(bag(var), bag(var))
; not_dag
; no_eqns
; lpsolve_failed(eqn_soln)
; call_in_single_arg(pred_proc_id)
; single_arg_failed(term_error__error)
; single_arg_failed(term_error__error, term_error__error).
% eqn_soln are used to report the results from solving the equations
% created in the first pass. The first 4 (optimal - failure) represent
% output states from lp_solve.
:- type eqn_soln
---> optimal
; infeasible
; unbounded
; failure
; fatal_error % unable to open a file, or make a system call
; parse_error % unable to parse the output from lp_solve
; solved(list(pair(pred_proc_id, int))).
:- implementation.
:- import_module hlds_out, prog_out, hlds_pred.
term_error__output(MaybePredId, Module,
Context - positive_value(CallerPPId, CalledPPId)) -->
( { MaybePredId = yes(PredId) } ->
{ CalledPPId = proc(CalledPredId, _CalledProcId) },
{ CallerPPId = proc(CallerPredId, _CallerProcId) },
prog_out__write_context(Context),
io__write_string("Unable to check termination in predicate:\n"),
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, PredId),
( { PredId = CallerPredId } ->
io__write_string("as it contains a\n")
;
io__nl,
prog_out__write_context(Context),
io__write_string(
"as it is in the same SCC as the following predicate\n"
),
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, CallerPredId),
io__write_string(". That predicate contains a\n")
),
prog_out__write_context(Context),
( { PredId = CalledPredId } ->
io__write_string("directly recursive call")
;
io__write_string("recursive call to"),
hlds_out__write_pred_id(Module, CalledPredId),
io__nl,
prog_out__write_context(Context)
),
io__write_string("with the size of the variables increased.\n")
;
% only for hlds_dump
{ CalledPPId = proc(CalledPredId, _CalledProcId) },
{ CallerPPId = proc(CallerPredId, _CallerProcId) },
prog_out__write_context(Context),
io__write_string("this SCC contains a recursive call from "),
hlds_out__write_pred_id(Module, CallerPredId),
io__write_string("to "),
hlds_out__write_pred_id(Module, CalledPredId),
io__write_string("with the size of the variables increased.\n")
).
term_error__output(MaybePredId, Module, Context - horder_call) -->
prog_out__write_context(Context),
( { MaybePredId = yes(PredId) } ->
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("horder_call\n").
term_error__output(MaybePredId, Module, Context - pragma_c_code) -->
prog_out__write_context(Context),
( { MaybePredId = yes(PredId) } ->
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("pragma_c_code\n").
term_error__output(MaybePredId, Module,
Context - dont_know_proc_called(PPId)) -->
{ PPId = proc(CallPredId, _ProcId) },
( { MaybePredId = yes(PredId) } ->
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, PredId),
io__nl,
prog_out__write_context(Context)
;
[]
),
io__write_string("dont_know_proc_called"),
( { MaybePredId = yes(_) } ->
io__nl
;
[]
),
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, CallPredId),
io__nl.
term_error__output(MaybePredId,Module,
Context - dont_know_proc(_PPId)) -->
prog_out__write_context(Context),
( { MaybePredId = yes(PredId) } ->
hlds_out__write_pred_id(Module, PredId),
io__nl,
prog_out__write_context(Context)
;
[]
),
io__write_string("dont_know_proc\n").
term_error__output(MaybePredId, Module, Context - horder_args(_PPId)) -->
prog_out__write_context(Context),
( { MaybePredId = yes(PredId) } ->
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("horder_args\n").
term_error__output(MaybePredId, Module,
Context - inf_termination_const(PPId)) -->
{ PPId = proc(CallPredId, _ProcId) },
( { MaybePredId = yes(PredId) } ->
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, PredId),
io__nl,
prog_out__write_context(Context),
io__write_string("inf_termination_const"),
io__nl
;
io__write_string("inf_termination_const")
),
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, CallPredId),
io__nl.
term_error__output(MaybePredId, Module,
Context - ite_wrong_vars(Vars1, Vars2)) -->
prog_out__write_context(Context),
( { MaybePredId = yes(PredId) } ->
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("ite_wrong_vars\nVars1: "),
term_error__output_2(Vars1),
io__write_string("\nVars2: "),
term_error__output_2(Vars2).
term_error__output(MaybePredId, Module,
Context - switch_wrong_vars(Vars1, Vars2)) -->
prog_out__write_context(Context),
( { MaybePredId = yes(PredId) } ->
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("switch_wrong_vars\nVars1: "),
term_error__output_2(Vars1),
io__write_string("\nVars2: "),
term_error__output_2(Vars2).
term_error__output(MaybePredId, Module,
Context - disj_wrong_vars(Vars1, Vars2)) -->
prog_out__write_context(Context),
( { MaybePredId = yes(PredId) } ->
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("disj_wrong_vars\nVars1: "),
term_error__output_2(Vars1),
io__write_string("\nVars2: "),
term_error__output_2(Vars2).
term_error__output(MaybePredId, Module,
Context - not_subset(Vars1, Vars2)) -->
( { MaybePredId = yes(PredId) } ->
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("not_subset\nCalculated: "),
term_error__output_2(Vars1),
io__write_string("\nDeclared: "),
term_error__output_2(Vars2),
io__nl.
term_error__output(MaybePredId, Module, Context - not_dag) -->
( { MaybePredId = yes(PredId) } ->
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("not_dag\n").
term_error__output(MaybePredId, Module, Context - no_eqns) -->
( { MaybePredId = yes(PredId) } ->
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("no_eqns\n").
term_error__output(MaybePredId, Module, Context - lpsolve_failed(_Reason)) -->
( { MaybePredId = yes(PredId) } ->
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, PredId)
;
[]
),
io__write_string("lpsolve_failed\n").
term_error__output(MaybePredId, Module,
Context - call_in_single_arg(PPId)) -->
{ PPId = proc(CallPredId, _ProcId) },
( { MaybePredId = yes(PredId) } ->
prog_out__write_context(Context),
io__write_string("While processing "),
hlds_out__write_pred_id(Module, PredId),
io__nl,
prog_out__write_context(Context),
io__write_string("single argument analysis encountered a "),
io__write_string("call that could not be processed\n")
;
io__write_string("single argument analysis encountered a "),
io__write_string("call that could not be processed ")
),
prog_out__write_context(Context),
hlds_out__write_pred_id(Module, CallPredId),
io__nl.
term_error__output(MaybePredId, Module,
_Context - single_arg_failed(Error)) -->
io__write_string(
"Single argument analysis failed to find a head variable that was\n"),
io__write_string(
"always decreasing in size. Normal termination analysis failed \n"),
io__write_string("for the following reason\n"),
term_error__output(MaybePredId, Module, Error).
term_error__output(MaybePredId, Module,
_Context - single_arg_failed(Error1, Error2)) -->
term_error__output(MaybePredId, Module, Error1),
term_error__output(MaybePredId, Module, Error2).
:- pred term_error__output_2(bag(var), io__state, io__state).
:- mode term_error__output_2(in, di, uo) is det.
term_error__output_2(Vs) -->
( { bag__remove_smallest(Vs, V, Vs0) } ->
{ term__var_to_int(V, Num) },
io__write_int(Num),
io__write_string(" "),
term_error__output_2(Vs0)
;
[]
).
More information about the developers
mailing list