for review: changes to termination analysis and stack tracing [3/3]
Zoltan Somogyi
zs at cs.mu.oz.au
Tue Dec 2 15:19:58 AEDT 1997
[continued from part 2]
Index: compiler/quantification.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/quantification.m,v
retrieving revision 1.53
diff -u -r1.53 quantification.m
--- quantification.m 1997/09/01 14:04:33 1.53
+++ quantification.m 1997/11/15 02:28:28
@@ -122,13 +122,13 @@
OutsideVars, Goal, Varset, VarTypes, Warnings).
requantify_proc(ProcInfo0, ProcInfo) :-
- proc_info_variables(ProcInfo0, Varset0),
+ proc_info_varset(ProcInfo0, Varset0),
proc_info_vartypes(ProcInfo0, VarTypes0),
proc_info_headvars(ProcInfo0, HeadVars),
proc_info_goal(ProcInfo0, Goal0),
implicitly_quantify_clause_body(HeadVars, Goal0, Varset0, VarTypes0,
Goal, Varset, VarTypes, _),
- proc_info_set_variables(ProcInfo0, Varset, ProcInfo1),
+ proc_info_set_varset(ProcInfo0, Varset, ProcInfo1),
proc_info_set_vartypes(ProcInfo1, VarTypes, ProcInfo2),
proc_info_set_goal(ProcInfo2, Goal, ProcInfo).
Index: compiler/saved_vars.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/saved_vars.m,v
retrieving revision 1.11
diff -u -r1.11 saved_vars.m
--- saved_vars.m 1997/09/01 14:04:35 1.11
+++ saved_vars.m 1997/11/15 02:28:39
@@ -47,7 +47,7 @@
write_proc_progress_message("% Minimizing saved vars in ",
PredId, ProcId, ModuleInfo0),
{ proc_info_goal(ProcInfo0, Goal0) },
- { proc_info_variables(ProcInfo0, Varset0) },
+ { proc_info_varset(ProcInfo0, Varset0) },
{ proc_info_vartypes(ProcInfo0, VarTypes0) },
{ init_slot_info(Varset0, VarTypes0, SlotInfo0) },
@@ -68,7 +68,7 @@
% hlds_out__write_goal(Goal, ModuleInfo, Varset, 0, ""),
{ proc_info_set_goal(ProcInfo0, Goal, ProcInfo1) },
- { proc_info_set_variables(ProcInfo1, Varset, ProcInfo2) },
+ { proc_info_set_varset(ProcInfo1, Varset, ProcInfo2) },
{ proc_info_set_vartypes(ProcInfo2, VarTypes, ProcInfo) }.
%-----------------------------------------------------------------------------%
Index: compiler/simplify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/simplify.m,v
retrieving revision 1.47
diff -u -r1.47 simplify.m
--- simplify.m 1997/11/24 07:27:00 1.47
+++ simplify.m 1997/11/25 07:33:13
@@ -75,7 +75,7 @@
globals__io_get_globals(Globals, State0, State1),
det_info_init(ModuleInfo0, PredId, ProcId, Globals, DetInfo0),
proc_info_get_initial_instmap(Proc0, ModuleInfo0, InstMap0),
- proc_info_variables(Proc0, VarSet0),
+ proc_info_varset(Proc0, VarSet0),
proc_info_vartypes(Proc0, VarTypes0),
simplify_info_init(DetInfo0, Simplify, InstMap0,
VarSet0, VarTypes0, Info0),
@@ -92,7 +92,7 @@
simplify__proc_2(Proc0, Proc1, Info1, Info2, State2, State3),
simplify_info_get_msgs(Info2, Msgs1),
simplify_info_get_det_info(Info2, DetInfo1),
- proc_info_variables(Proc1, VarSet1),
+ proc_info_varset(Proc1, VarSet1),
proc_info_vartypes(Proc1, VarTypes1),
simplify_info_init(DetInfo1,
simplify(no, no, Once, no, no, Excess, no, Prop),
@@ -134,7 +134,7 @@
simplify_info_get_varset(Info1, VarSet),
simplify_info_get_var_types(Info1, VarTypes),
proc_info_set_goal(Proc0, Goal, Proc1),
- proc_info_set_variables(Proc1, VarSet, Proc2),
+ proc_info_set_varset(Proc1, VarSet, Proc2),
proc_info_set_vartypes(Proc2, VarTypes, Proc3),
( simplify_info_requantify(Info1) ->
requantify_proc(Proc3, Proc4),
Index: compiler/trans_opt.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/trans_opt.m,v
retrieving revision 1.2
diff -u -r1.2 trans_opt.m
--- trans_opt.m 1997/10/09 09:39:25 1.2
+++ trans_opt.m 1997/11/13 09:16:31
@@ -159,6 +159,7 @@
:- 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) },
@@ -168,13 +169,14 @@
{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
{ pred_info_context(PredInfo, Context) },
{ SymName = qualified(ModuleName, PredName) },
- { proc_info_termination(ProcInfo, Termination) },
+ { proc_info_get_maybe_arg_size_info(ProcInfo, ArgSize) },
+ { proc_info_get_maybe_termination_info(ProcInfo, Termination) },
{ proc_info_declared_argmodes(ProcInfo, ModeList) },
% All predicates to write procedure items into the .trans_opt file
% should go here.
- termination__output_pragma_termination_info(PredOrFunc, SymName,
- ModeList, Termination, Context),
+ termination__write_pragma_termination_info(PredOrFunc, SymName,
+ ModeList, Context, ArgSize, Termination),
trans_opt__write_procs(ProcIds, PredId, PredInfo).
Index: compiler/unused_args.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unused_args.m,v
retrieving revision 1.36
diff -u -r1.36 unused_args.m
--- unused_args.m 1997/11/24 07:27:14 1.36
+++ unused_args.m 1997/11/25 07:33:19
@@ -909,7 +909,7 @@
map__from_corresponding_lists(HeadVars, VarTypeList, VarTypes1),
% the varset should probably be fixed up, but it
% shouldn't make too much difference
- proc_info_variables(OldProc0, Varset0),
+ proc_info_varset(OldProc0, Varset0),
remove_listof_elements(HeadVars, 1, UnusedArgs, NewHeadVars),
GoalExpr = call(NewPredId, NewProcId, NewHeadVars,
not_builtin, no, qualified(PredModule, PredName)),
@@ -1068,7 +1068,7 @@
proc_info_headvars(ProcInfo0, HeadVars0),
proc_info_argmodes(ProcInfo0, ArgModes0),
- proc_info_variables(ProcInfo0, Varset0),
+ proc_info_varset(ProcInfo0, Varset0),
proc_info_goal(ProcInfo0, Goal0),
remove_listof_elements(HeadVars0, 1, UnusedArgs, HeadVars),
remove_listof_elements(ArgModes0, 1, UnusedArgs, ArgModes),
Index: compiler/notes/compiler_design.html
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/notes/compiler_design.html,v
retrieving revision 1.8
diff -u -r1.8 compiler_design.html
--- compiler_design.html 1997/11/08 13:12:08 1.8
+++ compiler_design.html 1997/11/15 01:09:59
@@ -350,10 +350,8 @@
<li> inlining (i.e. unfolding) of simple procedures (inlining.m)
-<li> constraint propagation (constraint.m) <br>
- <p>
-
- Not yet working.
+<li> pushing constraints as far left as possible (constraint.m);
+ this does not yet work.
<li> issue warnings about unused arguments from predicates, and create
specialized versions without them (unused_args.m); type_infos are
@@ -367,11 +365,12 @@
<li> elimination of useless assignments, assignments that merely introduce
another name for an already existing variable (excess.m).
-<li> reducing the number of variables that have to be saved across procedure calls
- (saved_vars.m). We do this by putting the code that generates the value of
- a variable just before the use of that variable, duplicating the variable
- and the code that produces it if necessary, provided the cost of doing so
- is smaller than the cost of saving and restoring the variable would be.
+<li> reducing the number of variables that have to be saved across
+ procedure calls (saved_vars.m). We do this by putting the code that
+ generates the value of a variable just before the use of that variable,
+ duplicating the variable and the code that produces it if necessary,
+ provided the cost of doing so is smaller than the cost of saving and
+ restoring the variable would be.
</ul>
@@ -669,10 +668,8 @@
<dd>
These modules contain stuff for handling the special
compiler-generated predicates which are generated for
- each type: unify/2, compare/3, index/1 (used in the
- implementation of compare/3), and also type_to_term/2
- and term_to_type/2 (but those last two are disabled
- at the moment).
+ each type: unify/2, compare/3, and index/1 (used in the
+ implementation of compare/3).
<dt> dependency_graph.m:
<dd>
Index: doc/user_guide.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/user_guide.texi,v
retrieving revision 1.107
diff -u -r1.107 user_guide.texi
--- user_guide.texi 1997/11/21 08:08:28 1.107
+++ user_guide.texi 1997/11/25 07:38:38
@@ -132,12 +132,12 @@
these are generated automatically by the compiler,
using the @samp{--make-interface} (or @samp{--make-int})
and @samp{--make-short-interface} (or @samp{--make-short-int}) options.
-Files ending in @file{.opt} are
+Files ending in @file{.opt} are
interface files used in inter-module optimization,
-and are created using the @samp{--make-optimization-interface}
+and are created using the @samp{--make-optimization-interface}
(or @samp{--make-opt-int}) option.
- at c Files ending in @file{.trans_opt} are interface files used in
- at c transitive inter-module optimization, and are created using the
+ at c Files ending in @file{.trans_opt} are interface files used in
+ at c transitive inter-module optimization, and are created using the
@c @samp{--make-transitive-optimization-interface} option.
Since the interface of a module changes less often than its implementation,
@@ -225,7 +225,7 @@
@c @example
@c mmc -make-trans-opt @var{module1}.m @var{module2}.m ...
@c @end example
- at c
+ at c
Given that you have made all the interface files,
one way to create an executable for a multi-module program
is to compile all the modules at the same time
@@ -684,7 +684,7 @@
NU-Prolog has logical alternatives
to the non-logical Prolog operations,
and since Mercury supports both syntaxes,
-you can use NU-Prolog's logical alternatives to avoid this problem.
+you can use NU-Prolog's logical alternatives to avoid this problem.
However, during the development of the Mercury compiler
we had to abandon their use for efficiency reasons.
@@ -807,15 +807,15 @@
Removes all the automatically generated files.
In addition to the files removed by @var{main-module}.clean, this
removes the @samp{.date}, @samp{.int}, @samp{.int2}, @samp{.int3},
- at samp{.opt}, @samp{.optdate}, @samp{.date3},
- at c @samp{.trans_opt}, @samp{.trans_optdate},
+ at samp{.opt}, @samp{.optdate}, @samp{.date3},
+ at c @samp{.trans_opt}, @samp{.trans_optdate},
@samp{.d}, and @samp{.dep} belonging to one of the modules of the program,
and also the various possible executables for the program ---
- at samp{@var{main-module}},
- at samp{@var{main-module}.nu},
- at samp{@var{main-module}.nu.save},
- at samp{@var{main-module}.nu.debug},
- at samp{@var{main-module}.nu.debug.save},
+ at samp{@var{main-module}},
+ at samp{@var{main-module}.nu},
+ at samp{@var{main-module}.nu.save},
+ at samp{@var{main-module}.nu.debug},
+ at samp{@var{main-module}.nu.debug.save},
@samp{@var{main-module}.sicstus}, and
@samp{@var{main-module}.sicstus.debug}.
@@ -863,7 +863,7 @@
@end table
Other variables also exist - see
- at file{@var{prefix}/lib/mercury/mmake/Mmake.vars} for a complete list.
+ at file{@var{prefix}/lib/mercury/mmake/Mmake.vars} for a complete list.
If you wish to temporarily change the flags passed to an executable,
rather than setting the various @samp{FLAGS} variables directly, one can
@@ -886,7 +886,7 @@
@chapter Libraries
Often you will want to use a particular set of Mercury modules
-in more than one program. The Mercury implementation
+in more than one program. The Mercury implementation
includes support for developing libraries, i.e. sets of Mercury modules
intended for reuse. It allows separate compilation of libraries
and, on many platforms, it supports shared object libraries.
@@ -934,7 +934,7 @@
Static libraries are created using the standard tools @samp{ar}
and @samp{ranlib}.
Shared libraries are created using the @samp{--make-shared-lib}
-option to @samp{ml}.
+option to @samp{ml}.
The automatically-generated Make rules for @samp{libmypackage}
will look something like this:
@@ -1029,9 +1029,9 @@
The @samp{-I} options in @samp{MCFLAGS} tell @samp{mmc} where to find
the interface files. The @samp{-R} options in @samp{MLFLAGS} tell
the loader where to find shared libraries, and the @samp{-L}
-options tell the linker where to find libraries.
+options tell the linker where to find libraries.
(Note that the @samp{-R} options must precede the @samp{-L} options.)
-The @samp{-l} options tell the linker which libraries to link with.
+The @samp{-l} options tell the linker which libraries to link with.
The extras arguments to @samp{c2init} specified in the @samp{C2INITLFLAGS}
variable tell @samp{c2init} where to find the @samp{.init} files for the
libraries, so that it can generate appropriate initialization code.
@@ -1143,8 +1143,8 @@
@node Displaying the profile
@section Displaying the profile
-To display the profile, just type @samp{mprof}. This will read the
- at file{Prof.*} files and display the flat profile in a nice human-readable
+To display the profile, just type @samp{mprof}. This will read the
+ at file{Prof.*} files and display the flat profile in a nice human-readable
format. If you also want to see the call graph profile, which takes a lot
longer to generate, type @samp{mprof -c}.
@@ -1156,7 +1156,7 @@
@node Analysis of results
@section Analysis of results
-The profile output consists of three major sections. These are
+The profile output consists of three major sections. These are
named the call graph profile, the flat profile and the alphabetic listing.
The call graph profile presents the local call graph of each
@@ -1198,26 +1198,26 @@
called/total children
<spontaneous>
-[1] 100.0 0.00 0.75 0 call_engine_label [1]
+[1] 100.0 0.00 0.75 0 call_engine_label [1]
0.00 0.75 1/1 do_interpreter [3]
-----------------------------------------------
0.00 0.75 1/1 do_interpreter [3]
-[2] 100.0 0.00 0.75 1 io__run/0(0) [2]
+[2] 100.0 0.00 0.75 1 io__run/0(0) [2]
0.00 0.00 1/1 io__init_state/2(0) [11]
0.00 0.74 1/1 main/2(0) [4]
-----------------------------------------------
0.00 0.75 1/1 call_engine_label [1]
-[3] 100.0 0.00 0.75 1 do_interpreter [3]
+[3] 100.0 0.00 0.75 1 do_interpreter [3]
0.00 0.75 1/1 io__run/0(0) [2]
-----------------------------------------------
0.00 0.74 1/1 io__run/0(0) [2]
-[4] 99.9 0.00 0.74 1 main/2(0) [4]
+[4] 99.9 0.00 0.74 1 main/2(0) [4]
0.00 0.74 1/1 sort/2(0) [5]
0.00 0.00 1/1 print_list/3(0) [16]
0.00 0.00 1/10 io__write_string/3(0) [18]
@@ -1225,7 +1225,7 @@
-----------------------------------------------
0.00 0.74 1/1 main/2(0) [4]
-[5] 99.9 0.00 0.74 1 sort/2(0) [5]
+[5] 99.9 0.00 0.74 1 sort/2(0) [5]
0.05 0.65 1/1 list__perm/2(0) [6]
0.00 0.09 40320/40320 sorted/1(0) [10]
@@ -1233,35 +1233,35 @@
8 list__perm/2(0) [6]
0.05 0.65 1/1 sort/2(0) [5]
-[6] 86.6 0.05 0.65 1+8 list__perm/2(0) [6]
+[6] 86.6 0.05 0.65 1+8 list__perm/2(0) [6]
0.00 0.60 5914/5914 list__insert/3(2) [7]
8 list__perm/2(0) [6]
-----------------------------------------------
0.00 0.60 5914/5914 list__perm/2(0) [6]
-[7] 80.0 0.00 0.60 5914 list__insert/3(2) [7]
+[7] 80.0 0.00 0.60 5914 list__insert/3(2) [7]
0.60 0.60 5914/5914 list__delete/3(3) [8]
-----------------------------------------------
40319 list__delete/3(3) [8]
0.60 0.60 5914/5914 list__insert/3(2) [7]
-[8] 80.0 0.60 0.60 5914+40319 list__delete/3(3) [8]
+[8] 80.0 0.60 0.60 5914+40319 list__delete/3(3) [8]
40319 list__delete/3(3) [8]
-----------------------------------------------
0.00 0.00 3/69283 tree234__set/4(0) [15]
0.09 0.09 69280/69283 sorted/1(0) [10]
-[9] 13.3 0.10 0.10 69283 compare/3(0) [9]
+[9] 13.3 0.10 0.10 69283 compare/3(0) [9]
0.00 0.00 3/3 __Compare___io__stream/0(0) [20]
0.00 0.00 69280/69280 builtin_compare_int/3(0) [27]
-----------------------------------------------
0.00 0.09 40320/40320 sort/2(0) [5]
-[10] 13.3 0.00 0.09 40320 sorted/1(0) [10]
+[10] 13.3 0.00 0.09 40320 sorted/1(0) [10]
0.09 0.09 69280/69283 compare/3(0) [9]
-----------------------------------------------
@@ -1274,29 +1274,29 @@
@samp{main/2} is the entry point to the user's program.)
Each entry of the call graph profile consists of three sections, the parent
-procedures, the current procedure and the children procedures.
+procedures, the current procedure and the children procedures.
Reading across from the left, for the current procedure the fields are:
@itemize @bullet
@item
-The unique index number for the current procedure.
+The unique index number for the current procedure.
(The index numbers are used only to make it easier to find
a particular entry in the call graph.)
@item
The percentage of total execution time spent in the current procedure
-and all its descendents.
+and all its descendents.
As noted above, this is only a statistical approximation.
@item
-The ``self'' time: the time spent executing code that is
-part of current procedure.
+The ``self'' time: the time spent executing code that is
+part of current procedure.
As noted above, this is only a statistical approximation.
@item
The descendent time: the time spent in the
-current procedure and all its descendents.
+current procedure and all its descendents.
As noted above, this is only a statistical approximation.
@item
@@ -1307,7 +1307,7 @@
These numbers are exact, not approximate.
@item
-The name of the procedure followed by its index number.
+The name of the procedure followed by its index number.
@end itemize
The predicate or function names are not just followed by their arity but
@@ -1318,7 +1318,7 @@
Now for the parent and child procedures the self and descendent time have
slightly different meanings. For the parent procedures the self and descendent
-time represent the proportion of the current procedure's self and descendent
+time represent the proportion of the current procedure's self and descendent
time due to that parent. These times are obtained using the assumption that
each call contributes equally to the total time of the current procedure.
@c XXX is that really true? Do we really make that assumption?
@@ -1333,16 +1333,16 @@
@menu
* Invocation overview::
-* Verbosity options::
-* Warning options::
-* Output options::
-* Auxiliary output options::
+* Verbosity options::
+* Warning options::
+* Output options::
+* Auxiliary output options::
* Language semantics options::
* Compilation model options::
-* Code generation options::
-* Optimization options::
-* Link options::
-* Miscellaneous options::
+* Code generation options::
+* Optimization options::
+* Link options::
+* Miscellaneous options::
@end menu
@node Invocation overview
@@ -1423,7 +1423,7 @@
@sp 1
@item --warn-non-stratification
-Warn about possible non-stratification of the predicates/functions in the
+Warn about possible non-stratification of the predicates/functions in the
module.
Non-stratification occurs when a predicate/function can call itself
negatively through some path along its call graph.
@@ -1506,7 +1506,7 @@
and all of its dependencies to @file{@var{module}.dep}.
@item --generate-module-order
-Output the strongly connected components of the module
+Output the strongly connected components of the module
dependency graph in top-down order to @file{@var{module}.order}.
Implies @samp{--generate-dependencies}.
@@ -1533,10 +1533,10 @@
@c @item --make-transitive-optimization-interface
@c @itemx --make-trans-opt
@c Write the @file{@var{module}.trans_opt} file. This file is used to store
- at c information used for inter-module optimization. The information is read
- at c in when the compiler is invoked with the @samp{--transitive-optimization}
- at c option. The file is called ``transitive'' because a
- at c @file{@var{module}.trans_opt} file may depend on other
+ at c information used for inter-module optimization. The information is read
+ at c in when the compiler is invoked with the @samp{--transitive-optimization}
+ at c option. The file is called ``transitive'' because a
+ at c @file{@var{module}.trans_opt} file may depend on other
@c @file{@var{module}.trans_opt} files.
@c
@sp 1
@@ -1551,7 +1551,7 @@
@itemx --pretty-print
@itemx --convert-to-mercury
Convert to Mercury. Output to file @file{@var{module}.ugly}.
-This option acts as a Mercury ugly-printer.
+This option acts as a Mercury ugly-printer.
(It would be a pretty-printer, except that comments are stripped
and nested if-then-elses are indented too much --- so the result
is rather ugly.)
@@ -1862,7 +1862,7 @@
Similar to @samp{--profiling}, except that this option only gathers
timing information, not call counts. For the results to be useful,
call counts for an identical run of your program need to be gathered
-using @samp{--profiling} or @samp{--profile-calls}.
+using @samp{--profiling} or @samp{--profile-calls}.
The only advantage of using @samp{--profile-time} and @samp{--profile-calls}
to gather timing information and call counts in seperate runs,
rather than just using @samp{--profiling} to gather them both at once,
@@ -1874,7 +1874,7 @@
@item @code{--debug} (grades: any grade containing @samp{.debug})
Enable debugging.
Pass the @samp{-g} flag to the C compiler, instead of @samp{-DSPEED},
-to enable debugging of the generated C code.
+to enable debugging of the generated C code.
This option also implies @samp{--no-c-optimize}.
Debugging support is currently extremely primitive -
this option is probably not useful to anyone except the Mercury implementors.
@@ -1900,7 +1900,7 @@
(This option is not intended for general use.)
Don't output base_type_layout structures or references to them.
This option will generate smaller executables, but will not allow the
-use of code that uses the layout information (e.g. @samp{functor},
+use of code that uses the layout information (e.g. @samp{functor},
@samp{arg}). Using such code will result in undefined behaviour at
runtime. The C code also needs to be compiled with
@samp{-DNO_TYPE_LAYOUT}.
@@ -1954,7 +1954,7 @@
@sp 1
@item --fact-table-max-array-size @var{size}
-Specify the maximum number of elements in a single
+Specify the maximum number of elements in a single
@samp{pragma fact_table} data array (default: 1024).
The data for fact tables is placed into multiple C arrays, each with a
maximum size given by this option. The reason for doing this is that
@@ -2058,7 +2058,7 @@
@c different to the @file{@var{module}.opt} as @file{@var{module}.trans_opt}
@c files may depend on other @file{@var{module}.trans_opt} files.
@c @file{@var{module}.opt} files may only depend on the
- at c @file{@var{module}.m} file.
+ at c @file{@var{module}.m} file.
@c
@sp 1
@item --enable-termination
@@ -2075,19 +2075,40 @@
@itemx --check-term
@itemx --chk-term
Enable termination analysis, and emit warnings for some predicates or
-functions that cannot be proved to terminate. In many cases the
-compiler is unable to prove termination the problem is either a lack of
-information about the termination properties of other predicates, or
-because the program used language constructs (such as higher order
-calls) which could not be analysed. In these cases the compiler does
+functions that cannot be proved to terminate. In many cases in which the
+compiler is unable to prove termination, the problem is either a lack of
+information about the termination properties of other predicates, or the
+fact that the program used language constructs (such as higher order
+calls) which cannot be analysed. In these cases the compiler does
not emit a warning of non-termination, as it is likely to be spurious.
@sp 1
@item --verbose-check-termination
@itemx --verb-check-term
@itemx --verb-chk-term
-Enable termination analysis, and emit warnings for all predicates or
-functions that cannot be proved to terminate.
+Enable termination analysis, and emit warnings for all predicates or
+functions that cannot be proved to terminate.
+
+ at sp 1
+ at item --termination-single-argument-analysis @var{limit}
+ at itemx --term-single-arg @var{limit}
+When performing termination analysis, try analyzing
+recursion on single arguments in strongly connected
+components of the call graph that have up to @var{limit} procedures.
+
+ at sp 1
+ at item --termination-norm @var{norm}
+The norm defines how termination analysis measures the size
+of a memory cell. The @samp{simple} norm says that size is always one.
+The @samp{total} norm says that it is the number of words in the cell.
+The @samp{num-data-elems} norm says that it is the number of words in
+the cell that contain something other than pointers to cells of
+the same type.
+
+ at sp 1
+ at item --termination-error-limit @var{limit}
+ at itemx --term-err-limit @var{limit}
+Print at most @var{n} reasons for any single termination error.
@sp 1
@item --split-c-files
@@ -2137,7 +2158,7 @@
@item --intermod-inline-simple-threshold @var{threshold}
Similar to --inline-simple-threshold, except used to determine which
-predicates should be included in @samp{.opt} files. Note that changing this
+predicates should be included in @samp{.opt} files. Note that changing this
between writing the @samp{.opt} file and compiling to C may cause link errors,
and too high a value may result in reduced performance.
@@ -2396,7 +2417,7 @@
@table @code
@item -I @var{dir}
@itemx --search-directory @var{dir}
-Append @var{dir} to the list of directories to be searched for
+Append @var{dir} to the list of directories to be searched for
imported modules.
@item --intermod-directory @var{dir}
@@ -2466,7 +2487,7 @@
A list of options for the Mercury runtime that gets
linked into every Mercury program.
Options are available to set the size of the different memory
-areas, and to enable various debugging traces.
+areas, and to enable various debugging traces.
Set @samp{MERCURY_OPTIONS} to @samp{-h} for help.
@sp 1
@@ -2559,7 +2580,7 @@
it is possible to do so. Here's what you need to do.
@itemize @bullet
- at item You must specify the name of the new compiler.
+ at item You must specify the name of the new compiler.
You can do this either by setting the @samp{MERCURY_C_COMPILER}
environment variable, by adding
@samp{MGNUC=MERCURY_C_COMPILER=@dots{} mgnuc} to your @samp{Mmake} file,
@@ -2571,7 +2592,7 @@
@samp{-std} option to @samp{cc}).
@item
-You must use the grade @samp{none} or @samp{none.gc}.
+You must use the grade @samp{none} or @samp{none.gc}.
You can specify the grade in one of three ways: by setting the
@samp{MERCURY_DEFAULT_GRADE} environment variable, by adding a line
@samp{GRADE=@dots{}} to your @samp{Mmake} file, or by using the
Index: library/bag.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/bag.m,v
retrieving revision 1.12
diff -u -r1.12 bag.m
--- bag.m 1997/10/04 06:16:50 1.12
+++ bag.m 1997/11/25 04:29:50
@@ -16,7 +16,7 @@
:- interface.
-:- import_module list.
+:- import_module list, assoc_list.
:- type bag(T).
@@ -42,7 +42,14 @@
:- pred bag__to_list(bag(T), list(T)).
:- mode bag__to_list(in, out) is det.
- % Given a bag, produce a sorted list with no duplicates
+ % Given a bag, produce a sorted list containing all the values in
+ % the bag. Each value will appear in the list once, with the
+ % associated value giving the number of times that it appears
+ % in the bag.
+:- pred bag__to_assoc_list(bag(T), assoc_list(T, int)).
+:- mode bag__to_assoc_list(in, out) is det.
+
+ % Given a bag, produce a sorted list with no duplicates
% containing all the values in the bag.
:- pred bag__to_list_without_duplicates(bag(T), list(T)).
:- mode bag__to_list_without_duplicates(in, out) is det.
@@ -80,7 +87,7 @@
% each element in SubBag is removed from Bag0 to produce Bag.
% If an element exists in SubBag, but not in Bag, then that
% element is not removed.
- % e.g. bag__subtract({1, 1, 2, 2, 3 }, {1, 1, 2, 3, 3, 3}, {2}).
+ % e.g. bag__subtract({1, 1, 2, 2, 3 }, {1, 1, 2, 3, 3, 3}, {2}).
:- pred bag__subtract(bag(T), bag(T), bag(T)).
:- mode bag__subtract(in, in, out) is det.
@@ -103,6 +110,16 @@
:- pred bag__intersect(bag(T), bag(T)).
:- mode bag__intersect(in, in) is semidet.
+ % The third bag is the smallest bag that has both the first two bags
+ % as subbags. If an element X is present N times in one of the first
+ % two bags, X will be present at least N times in the third bag.
+ % E.g. {1, 1, 2} upper_bound {2, 2, 3} = {1, 1, 2, 2, 3}
+ % If the two input bags are known to be unequal in size, then
+ % making the first bag the larger bag will usually be more
+ % efficient.
+:- pred bag__least_upper_bound(bag(T), bag(T), bag(T)).
+:- mode bag__least_upper_bound(in, in, out) is det.
+
% Fails if the first bag is not a subbag of the second.
% bag__is_subbag(A, B). implies that every element in the bag A
% is also in the bag B. If an element is in bag A multiple times, it
@@ -120,7 +137,7 @@
:- pred bag__remove_smallest(bag(T), T, bag(T)).
:- mode bag__remove_smallest(in, out, out) is semidet.
- % Compares the two bags, and returns whether the first bag is a
+ % Compares the two bags, and returns whether the first bag is a
% subset (<), is equal (=), or is a superset (>) of the second.
% bag__subset_compare(<, {apple, orange}, {apple, apple, orange}).
% bag__subset_compare(=, {apple, orange}, {apple, orange}).
@@ -131,9 +148,10 @@
%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%
+
:- implementation.
-:- import_module map, int, require, assoc_list, std_util.
+:- import_module map, int, require, std_util.
:- type bag(T) == map(T, int).
@@ -167,15 +185,13 @@
bag__init(Bag0),
bag__insert_list(Bag0, List, Bag).
-bag__to_list_without_duplicates(Bag, List) :-
- map__keys(Bag, List).
-
bag__to_list(Bag, List) :-
map__to_assoc_list(Bag, AssocList),
bag__to_list_2(AssocList, List).
:- pred bag__to_list_2(assoc_list(T, int), list(T)).
:- mode bag__to_list_2(in, out) is det.
+
bag__to_list_2([], []).
bag__to_list_2([X - Int | Xs ], Out) :-
( Int =< 0 ->
@@ -185,7 +201,12 @@
bag__to_list_2([X - NewInt | Xs], Out0),
Out = [X | Out0]
).
-
+
+bag__to_assoc_list(Bag, AssocList) :-
+ map__to_assoc_list(Bag, AssocList).
+
+bag__to_list_without_duplicates(Bag, List) :-
+ map__keys(Bag, List).
%---------------------------------------------------------------------------%
@@ -245,11 +266,10 @@
Bag = Bag0
).
-
bag__union(A, B, Out) :-
( map__remove_smallest(B, Key, BVal, B0) ->
( map__search(A, Key, AVal) ->
- NewVal = AVal + BVal,
+ NewVal is AVal + BVal,
map__det_update(A, Key, NewVal, A0)
;
map__det_insert(A, Key, BVal, A0)
@@ -258,8 +278,6 @@
;
Out = A
).
-
-
bag__intersect(A, B, Out) :-
bag__init(Out0),
@@ -267,6 +285,7 @@
:- pred bag__intersect_2(bag(T), bag(T), bag(T), bag(T)).
:- mode bag__intersect_2(in, in, in, out) is det.
+
bag__intersect_2(A, B, Out0, Out) :-
( map__remove_smallest(A, Key, AVal,A0) ->
( map__search(B, Key, BVal) ->
@@ -288,6 +307,19 @@
bag__intersect(A0, B)
).
+bag__least_upper_bound(A, B, Out) :-
+ ( map__remove_smallest(B, Key, BVal, B0) ->
+ ( map__search(A, Key, AVal) ->
+ int__max(AVal, BVal, NewVal),
+ map__det_update(A, Key, NewVal, A0)
+ ;
+ map__det_insert(A, Key, BVal, A0)
+ ),
+ bag__least_upper_bound(A0, B0, Out)
+ ;
+ Out = A
+ ).
+
%---------------------------------------------------------------------------%
bag__is_subbag(SubBag, BigBag) :-
@@ -310,7 +342,7 @@
Bag = Bag1
).
- % compares the two bags, and returns whether the first bag is a
+ % compares the two bags, and returns whether the first bag is a
% subset (<), is equal (=), or is a superset (>) of the second
% bag__subset_compare(<, {apple, orange}, {apple, apple, orange}).
% bag__subset_compare(=, {apple, orange}, {apple, orange}).
@@ -322,7 +354,7 @@
( map__remove_smallest(A, Key, AVal, A0) ->
( map__remove(B, Key, BVal, B0) ->
compare(ValRes, AVal, BVal),
- (
+ (
ValRes = (>),
bag__is_subbag(B0, A0),
Res = (>)
Index: library/list.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/list.m,v
retrieving revision 1.78
diff -u -r1.78 list.m
--- list.m 1997/09/02 23:05:45 1.78
+++ list.m 1997/11/17 00:31:15
@@ -154,6 +154,13 @@
:- pred list__take(int, list(T), list(T)).
:- mode list__take(in, in, out) is semidet.
+ % list__take_upto(Len, List, Start):
+ % `Start' is the first `Len' elements of `List'.
+ % If `List' has fewer elements than that, return the entire list.
+ %
+:- pred list__take_upto(int, list(T), list(T)).
+:- mode list__take_upto(in, in, out) is det.
+
% list__drop(Len, List, End):
% `End' is the remainder of `List' after removing the
% first `Len' elements.
@@ -797,9 +804,26 @@
N > 0
->
N1 is N - 1,
- As = [A|As1],
- Bs = [A|Bs1],
+ As = [A | As1],
+ Bs = [A | Bs1],
list__take(N1, As1, Bs1)
+ ;
+ Bs = []
+ ).
+
+list__take_upto(N, As, Bs) :-
+ (
+ N > 0
+ ->
+ N1 is N - 1,
+ (
+ As = [A | As1],
+ Bs = [A | Bs1],
+ list__take_upto(N1, As1, Bs1)
+ ;
+ As = [],
+ Bs = []
+ )
;
Bs = []
).
Index: library/set.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/set.m,v
retrieving revision 1.47
diff -u -r1.47 set.m
--- set.m 1997/11/02 08:50:39 1.47
+++ set.m 1997/11/15 07:39:57
@@ -182,6 +182,11 @@
:- pred set__difference(set(T), set(T), set(T)).
:- mode set__difference(in, in, out) is det.
+ % `set__count(Set, Count)' is true iff `Set' has `Count' elements.
+
+:- pred set__count(set(T), int).
+:- mode set__count(in, out) is det.
+
%--------------------------------------------------------------------------%
:- implementation.
@@ -258,6 +263,9 @@
set__difference(SetA, SetB, Set) :-
set_ordlist__difference(SetA, SetB, Set).
+
+set__count(Set, Count) :-
+ set_ordlist__count(Set, Count).
%--------------------------------------------------------------------------%
%--------------------------------------------------------------------------%
Index: library/set_ordlist.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/set_ordlist.m,v
retrieving revision 1.5
diff -u -r1.5 set_ordlist.m
--- set_ordlist.m 1997/07/27 15:07:11 1.5
+++ set_ordlist.m 1997/11/15 07:34:27
@@ -162,7 +162,7 @@
:- mode set_ordlist__intersect(in, in, in) is semidet.
% `set_ordlist__power_intersect(A, B)' is true iff `B' is the
- % intersection of all the sets in `A'
+ % intersection of all the sets in `A'.
:- pred set_ordlist__power_intersect(set_ordlist(set_ordlist(T)),
set_ordlist(T)).
@@ -170,12 +170,18 @@
% `set_ordlist__difference(SetA, SetB, Set)' is true iff `Set' is the
% set containing all the elements of `SetA' except those that
- % occur in `SetB'
+ % occur in `SetB'.
:- pred set_ordlist__difference(set_ordlist(T), set_ordlist(T),
set_ordlist(T)).
:- mode set_ordlist__difference(in, in, out) is det.
+ % `set_ordlist__count(Set, Count)' is true iff `Set' has
+ % `Count' elements.
+
+:- pred set_ordlist__count(set_ordlist(T), int).
+:- mode set_ordlist__count(in, out) is det.
+
%--------------------------------------------------------------------------%
:- implementation.
@@ -336,5 +342,10 @@
R = (>),
set_ordlist__difference([X|Xs], Ys, Set)
).
+
+%--------------------------------------------------------------------------%
+
+set_ordlist__count(Set, Count) :-
+ list__length(Set, Count).
%--------------------------------------------------------------------------%
Index: tests/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/Mmakefile,v
retrieving revision 1.1
diff -u -r1.1 Mmakefile
--- Mmakefile 1997/02/13 21:38:45 1.1
+++ Mmakefile 1997/11/03 01:25:06
@@ -1,4 +1,4 @@
-SUBDIRS = benchmarks general hard_coded invalid misc_tests valid warnings
+SUBDIRS = benchmarks general hard_coded invalid misc_tests term valid warnings
NUPROLOG_SUBDIRS = benchmarks general
main_target: check
New File: tests/term/Mmakefile
===================================================================
#-----------------------------------------------------------------------------#
main_target: check
include ../Mmake.common
#-----------------------------------------------------------------------------#
PROGS= \
ack \
append \
arit_exp \
associative \
dds1_2 \
dds3_13 \
dds3_14 \
dds3_15 \
dds3_17 \
dds3_8 \
fold \
list \
lte \
map \
member \
mergesort \
mergesort_ap \
mergesort_t \
mmatrix \
money \
naive_rev \
occur \
ordered \
overlap \
permutation \
pl1_1 \
pl1_2 \
pl2_3_1 \
pl3_1_1 \
pl3_5_6 \
pl3_5_6a \
pl4_01 \
pl4_4_3 \
pl4_4_6a \
pl4_5_2 \
pl4_5_3a \
pl5_2_2 \
pl6_1_1 \
pl7_2_9 \
pl7_6_2a \
pl7_6_2b \
pl7_6_2c \
pl8_2_1 \
pl8_2_1a \
pl8_3_1 \
pl8_3_1a \
pl8_4_1 \
pl8_4_2 \
queens \
quicksort \
select \
subset \
sum \
vangelder
modules:
@echo $(PROGS)
New File: tests/term/ack.m
===================================================================
:- module ack.
:- interface.
:- type nat ---> zero ; s(nat).
:- pred ack(nat, nat, nat).
:- mode ack(in, in, out) is det.
:- implementation.
% int(zero).
% int(s(X)) :- int(X).
ack(zero, N, s(N)). % :- int(N).
ack(s(M), zero, A) :-
ack(M, s(zero), A).
ack(s(M), s(N), A) :-
ack(s(M), N, A1),
ack(M, A1, A).
New File: tests/term/ack.trans_opt_exp
===================================================================
:- module ack.
:- pragma termination_info(ack:ack(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/append.m
===================================================================
:- module append.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred app(list(T), list(T), list(T)).
:- mode app(out, out, in) is multi.
:- implementation.
app([X|Xs], Ys, [X|Zs]) :-
app(Xs, Ys, Zs).
app([], Ys, Ys).
New File: tests/term/append.trans_opt_exp
===================================================================
:- module append.
:- pragma termination_info(append:app(mercury_builtin:out, mercury_builtin:out,
mercury_builtin:in), finite(0, [no, no, no, yes]), cannot_loop).
New File: tests/term/arit_exp.m
===================================================================
:- module arit_exp.
:- interface.
:- type expr ---> expr + expr ; expr * expr ; - expr ; int(int).
:- pred e(expr).
:- mode e(in) is semidet.
:- implementation.
e(X+Y) :-
f(X),
e(Y).
e(X) :-
f(X).
:- pred f(expr).
:- mode f(in) is semidet.
f(X*Y) :-
g(X),
f(Y).
f(X) :-
g(X).
:- pred g(expr).
:- mode g(in) is semidet.
g(-(X)) :-
e(X).
g(int(_X)).
New File: tests/term/arit_exp.trans_opt_exp
===================================================================
:- module arit_exp.
:- pragma termination_info(arit_exp:e(mercury_builtin:in), finite(0, [no]), cannot_loop).
New File: tests/term/associative.m
===================================================================
:- module associative.
:- interface.
:- type expr ---> base ; op(expr, expr).
:- pred normal_form(expr, expr).
:- mode normal_form(in, out) is det.
:- implementation.
normal_form(F, N) :-
( rewrite(F, F1) ->
normal_form(F1, N)
;
N = F
).
:- pred rewrite(expr, expr).
:- mode rewrite(in, out) is semidet.
rewrite(In, Out) :-
( In = op(op(A, B), C) ->
Out = op(A, op(B, C))
;
In = op(A, op(B, C)),
Out = op(A, L),
rewrite(op(B, C), L)
).
New File: tests/term/associative.trans_opt_exp
===================================================================
:- module associative.
:- pragma termination_info(associative:normal_form(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), can_loop).
New File: tests/term/dds1_2.m
===================================================================
:- module dds1_2.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred permute(list(T)::in, list(T)::out) is nondet.
:- implementation.
permute([], []).
permute([X|Y], [U|V]) :-
delete(U, [X|Y], W),
permute(W, V).
:- pred delete(T, list(T), list(T)).
:- mode delete(out, in, out).
delete(X, [X|Y], Y).
delete(U, [X|Y], [X|Z]) :-
delete(U, Y, Z).
New File: tests/term/dds1_2.trans_opt_exp
===================================================================
:- module dds1_2.
:- pragma termination_info(dds1_2:permute(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/dds3_13.m
===================================================================
:- module dds3_13.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred duplicate(list(T)::in, list(T)::out) is det.
:- implementation.
duplicate([], []).
duplicate([X | Y], [X, X | Z]) :-
duplicate(Y, Z).
New File: tests/term/dds3_13.trans_opt_exp
===================================================================
:- module dds3_13.
:- pragma termination_info(dds3_13:duplicate(mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/dds3_14.m
===================================================================
:- module dds3_14.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred sum(list(int)::in, list(int)::in, list(int)::out) is semidet.
:- implementation.
:- import_module int.
sum([], [], []).
sum([X1 | Y1], [X2 | Y2], [X3 | Y3]) :-
X3 is X1+X2,
sum(Y1, Y2, Y3).
New File: tests/term/dds3_14.trans_opt_exp
===================================================================
:- module dds3_14.
:- pragma termination_info(dds3_14:sum(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/dds3_15.m
===================================================================
:- module dds3_15.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred merge(list(int)::in, list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
merge([], X, X).
merge(X, [], X).
merge([X | Xs], [Y | Ys], [X | Zs]) :-
X =< Y,
merge(Xs, [Y | Ys], Zs).
merge([X | Xs], [Y | Ys], [Y | Zs]) :-
Y > X,
merge([X | Xs], Ys, Zs).
New File: tests/term/dds3_15.trans_opt_exp
===================================================================
:- module dds3_15.
:- pragma termination_info(dds3_15:merge(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [yes, yes, no]), cannot_loop).
New File: tests/term/dds3_17.m
===================================================================
:- module dds3_17.
:- interface.
:- type expr ---> true ; false ; or(expr, expr) ; and(expr, expr).
:- pred dis(expr::in) is semidet.
:- pred con(expr::in) is semidet.
:- implementation.
dis(or(B1, B2)) :-
con(B1),
dis(B2).
dis(B) :-
con(B).
con(and(B1, B2)) :-
dis(B1),
con(B2).
con(B) :-
bool(B).
:- pred bool(expr).
:- mode bool(in).
bool(true).
bool(false).
New File: tests/term/dds3_17.trans_opt_exp
===================================================================
:- module dds3_17.
:- pragma termination_info(dds3_17:dis(mercury_builtin:in), finite(0, [no]), cannot_loop).
:- pragma termination_info(dds3_17:con(mercury_builtin:in), finite(0, [no]), cannot_loop).
New File: tests/term/dds3_8.m
===================================================================
:- module dds3_8.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reverse(list(T)::in, list(T)::out, list(T)::in) is det.
:- implementation.
reverse([], X, X).
reverse([X | Y], Z, U) :-
reverse(Y, Z, [X | U]).
New File: tests/term/dds3_8.trans_opt_exp
===================================================================
:- module dds3_8.
:- pragma termination_info(dds3_8:reverse(mercury_builtin:in, mercury_builtin:out, mercury_builtin:in), finite(0, [no, yes, no, yes]), cannot_loop).
New File: tests/term/fold.m
===================================================================
:- module fold.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- type sym ---> a ; b ; c ; d.
:- pred fold(sym, list(sym), sym).
:- mode fold(in, in, out) is semidet.
:- implementation.
fold(X, [Y | Ys], Z) :-
xop(X, Y, V),
fold(V, Ys, Z).
fold(X, [], X).
:- pred xop(sym, sym, sym).
:- mode xop(in, in, out).
xop(a, b, c).
New File: tests/term/fold.trans_opt_exp
===================================================================
:- module fold.
:- pragma termination_info(fold:fold(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no, no]), cannot_loop).
New File: tests/term/list.m
===================================================================
:- module list.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred list(list(T)::in) is semidet.
:- implementation.
list([_H | Ts]) :-
list(Ts).
list([]).
New File: tests/term/list.trans_opt_exp
===================================================================
:- module list.
:- pragma termination_info(list:list(mercury_builtin:in), finite(0, [no, no]), cannot_loop).
New File: tests/term/lte.m
===================================================================
:- module lte.
:- interface.
:- pred goal is semidet.
:- implementation.
:- type nat ---> zero ; s(nat).
goal :-
lte(X, s(s(s(s(zero))))),
even(X).
:- pred lte(nat, nat).
:- mode lte(out, in).
lte(s(X), s(Y)) :-
lte(X, Y).
lte(zero, _Y).
:- pred even(nat).
:- mode even(in).
even(s(s(X))) :-
even(X).
even(zero).
New File: tests/term/lte.trans_opt_exp
===================================================================
:- module lte.
:- pragma termination_info(lte:goal, finite(0, []), cannot_loop).
New File: tests/term/map.m
===================================================================
:- module map.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred map(list(x)::in, list(x)::out) is semidet.
:- type x ---> val_i ; val_j ; val_k.
:- implementation.
:- pred p(x, x).
:- mode p(in, out).
p(val_i, val_j).
map([X | Xs], [Y | Ys]) :-
p(X, Y),
map(Xs, Ys).
map([], []).
New File: tests/term/map.trans_opt_exp
===================================================================
:- module map.
:- pragma termination_info(map:map(mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/member.m
===================================================================
:- module member.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred member(T::out, list(T)::in) is nondet.
:- implementation.
member(X, [_Y| Xs]) :-
member(X, Xs).
member(X, [X| _Xs]).
New File: tests/term/member.trans_opt_exp
===================================================================
:- module member.
:- pragma termination_info(member:member(mercury_builtin:out, mercury_builtin:in), finite(-1, [no, no, yes]), cannot_loop).
New File: tests/term/mergesort.m
===================================================================
:- module mergesort.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
mergesort([], []).
mergesort([X], [X]).
mergesort([X, Y | Xs], Ys) :-
split([X, Y | Xs], X1s, X2s),
mergesort(X1s, Y1s),
mergesort(X2s, Y2s),
merge(Y1s, Y2s, Ys).
:- pred split(list(T), list(T), list(T)).
:- mode split(in, out, out).
split([], [], []).
split([X | Xs], [X | Ys], Zs) :-
split(Xs, Zs, Ys).
:- pred merge(list(int), list(int), list(int)).
:- mode merge(in, in, out).
merge([], Xs, Xs).
merge(Xs, [], Xs).
merge([X | Xs], [Y | Ys], [X | Zs]) :-
X =< Y,
merge(Xs, [Y | Ys], Zs).
merge([X | Xs], [Y | Ys], [Y | Zs]) :-
X > Y,
merge([X | Xs], Ys, Zs).
New File: tests/term/mergesort.trans_opt_exp
===================================================================
:- module mergesort.
:- pragma termination_info(mergesort:mergesort(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), can_loop).
New File: tests/term/mergesort_ap.m
===================================================================
% this is a version of mergesort that appears in
% K. A. Apt and D. Pedreschi, Modular Termination Proofs for Logic and Pure
% Prolog Programs, Dipartimento di Informatica, Universita di Pisa, 1993
% mergesort(Xs, Ys, Xs) if Ys is an ordered permutation of the list Xs
:- module mergesort_ap.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out, list(int)::in) is nondet.
:- implementation.
:- import_module int.
mergesort([], [], _Ls).
mergesort([X], [X], _Ls).
mergesort([X, Y | Xs], Ys, [H | Ls]) :-
split([X, Y | Xs], X1s, X2s, [H | Ls]),
mergesort(X1s, Y1s, Ls),
mergesort(X2s, Y2s, Ls),
merge(Y1s, Y2s, Ys, [H | Ls]).
:- pred split(list(T), list(T), list(T), list(T)).
:- mode split(in, out, out, in).
split([], [], [], _Ls).
split([X | Xs], [X | Ys], Zs, [_H | Ls]) :-
split(Xs, Zs, Ys, Ls).
:- pred merge(list(int), list(int), list(int), list(int)).
:- mode merge(in, in, out, in).
merge([], Xs, Xs, _Ls).
merge(Xs, [], Xs, _Ls).
merge([X | Xs], [Y | Ys], [X | Zs], [_H | Ls]) :-
X =< Y,
merge(Xs, [Y | Ys], Zs, Ls).
merge([X | Xs], [Y | Ys], [Y | Zs], [_H | Ls]) :-
X > Y,
merge([X | Xs], Ys, Zs, Ls).
New File: tests/term/mergesort_ap.trans_opt_exp
===================================================================
:- module mergesort_ap.
:- pragma termination_info(mergesort_ap:mergesort(mercury_builtin:in, mercury_builtin:out, mercury_builtin:in), finite(0, [yes, no, no]), cannot_loop).
New File: tests/term/mergesort_t.m
===================================================================
:- module mergesort_t.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
mergesort([], []).
mergesort([X], [X]).
mergesort([X, Y | Xs], Ys) :-
split2([X, Y | Xs], X1s, X2s),
mergesort(X1s, Y1s),
mergesort(X2s, Y2s),
merge(Y1s, Y2s, Ys).
:- pred split(list(T), list(T), list(T)).
:- mode split(in, out, out).
split(Xs, Ys, Zs) :-
split0(Xs, Ys, Zs).
split(Xs, Ys, Zs) :-
split1(Xs, Ys, Zs).
split(Xs, Ys, Zs) :-
split2(Xs, Ys, Zs).
:- pred split0(list(T), list(T), list(T)).
:- mode split0(in, out, out).
split0([], [], []).
:- pred split1(list(T), list(T), list(T)).
:- mode split1(in, out, out).
split1([X], [X], []).
:- pred split2(list(T), list(T), list(T)).
:- mode split2(in, out, out).
split2([X, Y | Xs], [X | Ys], [Y | Zs]) :-
split(Xs, Ys, Zs).
:- pred merge(list(int), list(int), list(int)).
:- mode merge(in, in, out).
merge([], Xs, Xs).
merge(Xs, [], Xs).
merge([X | Xs], [Y | Ys], [X | Zs]) :-
X=<Y,
merge(Xs, [Y | Ys], Zs).
merge([X | Xs], [Y | Ys], [X | Zs]) :-
X>Y,
merge([X | Xs], Ys, Zs).
New File: tests/term/mergesort_t.trans_opt_exp
===================================================================
:- module mergesort_t.
:- pragma termination_info(mergesort_t:mergesort(mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/mmatrix.m
===================================================================
%------------------------------------------------------------------------------
% Benchmark Program - matrix*matrix multiplication
%
% Copyright by Manuel Hermenegildo
% Date: January 17 1986
%
%------------------------------------------------------------------------------
:- module mmatrix.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mmultiply(list(list(int)), list(list(int)), list(list(int))).
:- mode mmultiply(in, in, out) is semidet.
:- implementation.
:- import_module int.
mmultiply([], _, []).
mmultiply([V0 | Rest], V1, [Result | Others]) :-
mmultiply(Rest, V1, Others),
multiply(V1, V0, Result).
:- pred multiply(list(list(int)), list(int), list(int)).
:- mode multiply(in, in, out).
multiply([], _, []).
multiply([V0 | Rest], V1, [Result | Others]) :-
multiply(Rest, V1, Others),
vmul(V0, V1, Result).
:- pred vmul(list(int), list(int), int).
:- mode vmul(in, in, out).
vmul([], [], 0).
vmul([H1 | T1], [H2 | T2], Result) :-
vmul(T1, T2, Newresult),
Product is H1*H2,
Result is Product+Newresult.
New File: tests/term/mmatrix.trans_opt_exp
===================================================================
:- module mmatrix.
:- pragma termination_info(mmatrix:mmultiply(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/money.m
===================================================================
/*-----------------------------------------------------------------------------
Program: Cryptarithmetic puzzle SENDMORY
Author: Rong Yang (adapted)
Date:
Notes:
1. To run:
?- money(S, E, N, D, M, O, R, Y).
2. Solution is reached in the domain approach so as to recognize determinism
as the ecuations are being resolved.
3. After-checks are used and calc/5 ordering is better (L to R).
compiled it takes about 50 sec.
-----------------------------------------------------------------------------*/
:- module money.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred solve(list(int)::out) is nondet.
:- implementation.
:- import_module int.
solve([S, E, N, D, M, O, R, Y]) :-
money(S, E, N, D, M, O, R, Y).
:- pred money(int, int, int, int, int, int, int, int).
:- mode money(out, out, out, out, out, out, out, out).
money(S, E, N, D, M, O, R, Y) :-
carry(C1),
carry(C2),
carry(C3),
carry(C4),
C4 = M,
M \= 0,
domain([S, E, N, D, M, O, R, Y], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]),
S \= 0,
calc(C3, S, M, C4, O),
calc(C2, E, O, C3, N),
calc(C1, N, R, C2, E),
calc( 0, D, E, C1, Y).
:- pred calc(int, int, int, int, int).
:- mode calc(in, in, in, in, in).
calc(C0, D, E, C1, Y) :-
sum(C0, D, CD),
sum(CD, E, S),
carry10(C1, C10),
sum(C10, Y, S).
:- pred sum(int, int, int).
:- mode sum(in, in, out).
sum(X, Y, Z) :-
Z is X+Y.
:- pred domain(list(T), list(T)).
:- mode domain(out, in).
domain([], _).
domain([X1 | R], L) :-
del(X1, L, NL),
domain(R, NL).
:- pred del(T, list(T), list(T)).
:- mode del(out, in, out).
del(X, [X | T], T).
del(X, [Y | T], [Y | NT]) :-
del(X, T, NT).
:- pred carry(int).
:- mode carry(out).
carry(1).
carry(0).
:- pred carry10(int, int).
:- mode carry10(in, out).
carry10(0, 0).
carry10(1, 10).
New File: tests/term/money.trans_opt_exp
===================================================================
:- module money.
:- pragma termination_info(money:solve(mercury_builtin:out), finite(10, [no]), cannot_loop).
New File: tests/term/naive_rev.m
===================================================================
:- module naive_rev.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reverse(list(T)::in, list(T)::out) is det.
:- implementation.
reverse([X | Xs], Ys) :-
reverse(Xs, Zs),
app(Zs, [X], Ys).
reverse([], []).
:- pred app(list(T)::in, list(T)::in, list(T)::out).
app([X | Xs], Ys, [X | Zs]) :-
app(Xs, Ys, Zs).
app([], Ys, Ys).
New File: tests/term/naive_rev.trans_opt_exp
===================================================================
:- module naive_rev.
:- pragma termination_info(naive_rev:reverse(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/occur.m
===================================================================
%------------------------------------------------------------------------------
% Benchmark Program - Counting occurrences in lists
%
% Author: B. Ramkumar and L. V. Kale
% Date:
%
% To test: run o/1.
%------------------------------------------------------------------------------
% Benchmark is o(31), runs with -A1 -E256 -C128
:- module occur.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred occurall(list(int), list(list(int)), list(list(int))).
:- mode occurall(in, in, out) is nondet.
:- implementation.
:- import_module int.
occurall([], _X, []).
occurall([X | Y], Z, [[X, W] | V]) :-
occur(X, Z, W),
occurall(Y, Z, V).
:- pred occur(T1, list(list(T1)), int).
:- mode occur(in, in, out).
occur(_X, [], 0).
occur(X, [Y | Z], W) :-
(
count(X, Y, A),
occur(X, Z, B)
->
W is A + B
;
fail
).
:- pred count(T1, list(T1), int).
:- mode count(in, in, out).
count(_X, [], 0).
count(X, [Y | Z], W) :-
( count(X, Z, W1) ->
addx(X, Y, W1, W)
;
fail
).
:- pred addx(T1, T1, int, int).
:- mode addx(in, in, in, out).
addx(X, X, W1, W) :-
W is W1 + 1.
addx(X, Y, W1, W1) :-
X \= Y.
New File: tests/term/occur.trans_opt_exp
===================================================================
:- module occur.
:- pragma termination_info(occur:occurall(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/ordered.m
===================================================================
:- module ordered.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred ordered(list(int)::in) is semidet.
:- implementation.
:- import_module int.
ordered([]).
ordered([_X]).
ordered([X,Y | Xs]) :-
X =< Y,
ordered([Y | Xs]).
New File: tests/term/ordered.trans_opt_exp
===================================================================
:- module ordered.
:- pragma termination_info(ordered:ordered(mercury_builtin:in), finite(0, [no]), cannot_loop).
New File: tests/term/overlap.m
===================================================================
:- module overlap.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred overlap(list(T)::in, list(T)::in) is semidet.
:- implementation.
overlap(Xs, Ys) :-
member(X, Xs),
member(X, Ys).
% has_a_or_b(Xs) :- overlap(Xs, [a, b]).
:- pred member(T, list(T)).
:- mode member(out, in).
member(X, [_Y | Xs]) :-
member(X, Xs).
member(X, [X | _Xs]).
New File: tests/term/overlap.trans_opt_exp
===================================================================
:- module overlap.
:- pragma termination_info(overlap:overlap(mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no]), cannot_loop).
New File: tests/term/permutation.m
===================================================================
:- module permutation.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred perm(list(T)::in, list(T)::out) is nondet.
:- implementation.
perm(Xs, [X | Ys]) :-
app(X1s, [X | X2s], Xs),
app(X1s, X2s, Zs),
perm(Zs, Ys).
perm([], []).
:- pred app(list(T), list(T), list(T)).
:- mode app(out, out, in).
:- mode app(in, in, out).
app([X | Xs], Ys, [X | Zs]) :-
app(Xs, Ys, Zs).
app([], Ys, Ys).
New File: tests/term/permutation.trans_opt_exp
===================================================================
:- module permutation.
:- pragma termination_info(permutation:perm(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/pl1_1.m
===================================================================
:- module pl1_1.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out) is det.
:- mode append(out, out, in) is multi.
% :- mode append(out, in, out) is nondet. NOT WELL MODED
:- implementation.
append([], L, L).
append([H | L1], L2, [H | L3]) :-
append(L1, L2, L3).
New File: tests/term/pl1_1.trans_opt_exp
===================================================================
:- module pl1_1.
:- pragma termination_info(pl1_1:append(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, yes, no]), cannot_loop).
:- pragma termination_info(pl1_1:append(mercury_builtin:out, mercury_builtin:out, mercury_builtin:in), finite(0, [no, no, no, yes]), cannot_loop).
New File: tests/term/pl1_2.m
===================================================================
:- module pl1_2.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred perm(list(T)::in, list(T)::out) is nondet.
:- implementation.
perm([], []).
perm(L, [H | T]) :-
append(V, [H | U], L),
append(V, U, W),
perm(W, T).
:- pred append(list(T), list(T), list(T)).
:- mode append(out, out, in).
:- mode append(in, in, out).
append([], Y, Y).
append([H | X], Y, [H | Z]) :-
append(X, Y, Z).
New File: tests/term/pl1_2.trans_opt_exp
===================================================================
:- module pl1_2.
:- pragma termination_info(pl1_2:perm(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/pl2_3_1.m
===================================================================
:- module pl2_3_1.
:- interface.
:- type node ---> a ; b ; c.
:- pred p(node::in, node::out) is multi.
:- implementation.
p(X, Z) :-
q(X, Y),
p(Y, Z).
p(X, X).
:- pred q(node, node).
:- mode q(in, out).
q(a, b).
New File: tests/term/pl2_3_1.trans_opt_exp
===================================================================
:- module pl2_3_1.
:- pragma termination_info(pl2_3_1:p(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), can_loop).
New File: tests/term/pl3_1_1.m
===================================================================
:- module pl3_1_1.
:- interface.
:- pred a is semidet. % DIAGNOSED BY COMPILER
:- pred b is semidet. % DIAGNOSED BY COMPILER
:- pred c is semidet. % DIAGNOSED BY COMPILER
:- pred d is semidet. % DIAGNOSED BY COMPILER
:- pred e is semidet. % DIAGNOSED BY COMPILER
:- pred f is semidet. % DIAGNOSED BY COMPILER
:- pred g is semidet. % DIAGNOSED BY COMPILER
:- implementation.
a :- b.
a :- e.
b :- c.
c :- d.
d :- b.
e :- f.
f :- g.
g :- e.
New File: tests/term/pl3_1_1.trans_opt_exp
===================================================================
:- module pl3_1_1.
:- pragma termination_info(pl3_1_1:a, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:b, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:c, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:d, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:e, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:f, finite(0, []), can_loop).
:- pragma termination_info(pl3_1_1:g, finite(0, []), can_loop).
New File: tests/term/pl3_5_6.m
===================================================================
:- module pl3_5_6.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred p(list(int)::out) is nondet.
:- implementation.
p(X) :-
l(X),
q(X).
:- pred q(list(T)).
:- mode q(in).
q([_A]).
:- pred r(int).
:- mode r(out).
r(1).
:- pred l(list(int)).
:- mode l(out). % DIAGNOSED BY COMPILER
l([]).
l([H | T]) :-
r(H),
l(T).
New File: tests/term/pl3_5_6.trans_opt_exp
===================================================================
:- module pl3_5_6.
:- pragma termination_info(pl3_5_6:p(mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl3_5_6a.m
===================================================================
:- module pl3_5_6a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred p(list(int)::out) is nondet.
:- implementation.
p([A]) :-
l([A]).
:- pred q(list(T)).
:- mode q(in).
q([_A]).
:- pred r(int).
:- mode r(out).
r(1).
:- pred l(list(int)).
:- mode l(out). % DIAGNOSED BY COMPILER
l([]).
l([H | T]) :-
r(H),
l(T).
New File: tests/term/pl3_5_6a.trans_opt_exp
===================================================================
:- module pl3_5_6a.
:- pragma termination_info(pl3_5_6a:p(mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl4_01.m
===================================================================
:- module pl4_01.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred append3(list(T), list(T), list(T), list(T)).
:- mode append3(in, in, in, out) is det.
:- mode append3(out, out, out, in) is multi.
:- implementation.
append3(A, B, C, D) :-
append(A, B, E),
append(E, C, D).
:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out).
:- mode append(out, out, in).
append([], L, L).
append([H | L1], L2, [H | L3]) :-
append(L1, L2, L3).
New File: tests/term/pl4_01.trans_opt_exp
===================================================================
:- module pl4_01.
:- pragma termination_info(pl4_01:append3(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, yes, yes, no]), cannot_loop).
:- pragma termination_info(pl4_01:append3(mercury_builtin:out, mercury_builtin:out, mercury_builtin:out, mercury_builtin:in), finite(0, [no, no, no, no, yes]), cannot_loop).
New File: tests/term/pl4_4_3.m
===================================================================
:- module pl4_4_3.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred merge(list(int)::in, list(int)::in, list(int)::out) is nondet.
:- import_module int.
:- implementation.
merge(X, [], X).
merge([], X, X).
merge([A | X], [B | Y], [A | Z]) :-
A =< B,
merge(X, [B | Y], Z).
merge([A | X], [B | Y], [B | Z]) :-
A > B,
merge([A | X], Y, Z).
New File: tests/term/pl4_4_3.trans_opt_exp
===================================================================
:- module pl4_4_3.
:- pragma termination_info(pl4_4_3:merge(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), finite(0, [yes, yes, no]), cannot_loop).
New File: tests/term/pl4_4_6a.m
===================================================================
:- module pl4_4_6a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred perm(list(T)::in, list(T)::out) is nondet.
:- implementation.
perm([], []).
perm([X | L], Z) :-
perm(L, Y),
insert(X, Y, Z).
:- pred insert(T, list(T), list(T)).
:- mode insert(in, in, out).
insert(X, [], [X]).
insert(X, L, [X | L]).
insert(X, [H | L1], [H | L2]) :-
insert(X, L1, L2).
New File: tests/term/pl4_4_6a.trans_opt_exp
===================================================================
:- module pl4_4_6a.
:- pragma termination_info(pl4_4_6a:perm(mercury_builtin:in, mercury_builtin:out), finite(0, [no, yes, no]), cannot_loop).
New File: tests/term/pl4_5_2.m
===================================================================
:- module pl4_5_2.
:- interface.
:- type expr ---> expr + expr
; num(int).
:- pred s(expr::in, expr::out) is nondet.
:- implementation.
:- import_module int.
s(A+(B+C), D) :-
s((A+B)+C, D).
s(A+B, C) :-
s(B+A, C).
s(X+num(0), X).
s(X+Y, Z) :-
s(X, A),
s(Y, B),
s(A+B, Z).
s(A+B, C) :-
A = num(Anum),
B = num(Bnum),
Cnum is Anum + Bnum,
C = num(Cnum).
New File: tests/term/pl4_5_2.trans_opt_exp
===================================================================
:- module pl4_5_2.
:- pragma termination_info(pl4_5_2:s(mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl4_5_3a.m
===================================================================
:- module pl4_5_3a.
:- interface.
:- type node ---> a ; b ; c.
:- pred p(node).
:- mode p(in) is semidet. % DIAGNOSED BY COMPILER
:- mode p(out) is multi.
:- implementation.
p(b).
p(a) :-
p(_X).
New File: tests/term/pl4_5_3a.trans_opt_exp
===================================================================
:- module pl4_5_3a.
:- pragma termination_info(pl4_5_3a:p(mercury_builtin:in), finite(0, [no]), can_loop).
:- pragma termination_info(pl4_5_3a:p(mercury_builtin:out), finite(0, [no]), can_loop).
New File: tests/term/pl5_2_2.m
===================================================================
:- module pl5_2_2.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred turing(t_tuple, state, list(p_tuple), t_tuple).
:- mode turing(in, in, in, out) is nondet.
:- type t_tuple ---> t(list(sym), sym, list(sym)).
:- type p_tuple ---> p(state, sym, state, sym, dir).
:- type sym ---> blank ; nonblank.
:- type dir ---> r ; l.
:- type state ---> halt ; nonhalt.
:- implementation.
turing(t(X, Y, Z), S, P, t(X, Y, Z)) :-
member(p(S, Y, halt, _W, _D), P).
turing(t(X, Y, [R | L]), S, P, T) :-
member(p(S, Y, S1, W, r), P),
turing(t([W | X], R, L), S1, P, T).
turing(t(X, Y, []), S, P, T) :-
member(p(S, Y, S1, W, r), P),
turing(t([W | X], blank, []), S1, P, T).
turing(t([X | L], Y, R), S, P, T) :-
member(p(S, Y, S1, W, l), P),
turing(t(L, X, [W | R]), S1, P, T).
turing(t([], Y, R), S, P, T) :-
member(p(S, Y, S1, W, l), P),
turing(t([], blank, [W | R]), S1, P, T).
:- pred member(T, list(T)).
:- mode member(out, in) is nondet.
member(H, [H | _L]).
member(X, [_H | L]) :-
member(X, L).
New File: tests/term/pl5_2_2.trans_opt_exp
===================================================================
:- module pl5_2_2.
:- pragma termination_info(pl5_2_2:turing(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl6_1_1.m
===================================================================
:- module pl6_1_1.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred qsort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
qsort([], []).
qsort([H | L], S) :-
split(L, H, A, B),
qsort(A, A1),
qsort(B, B1),
append(A1, [H | B1], S).
:- pred split(list(int), int, list(int), list(int)).
:- mode split(in, in, out, out).
split([], _Y, [], []).
split([X | Xs], Y, [X | Ls], Bs) :-
X =< Y,
split(Xs, Y, Ls, Bs).
split([X | Xs], Y, Ls, [X | Bs]) :-
X > Y,
split(Xs, Y, Ls, Bs).
:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out).
append([], L, L).
append([H | L1], L2, [H | L3]) :-
append(L1, L2, L3).
New File: tests/term/pl6_1_1.trans_opt_exp
===================================================================
:- module pl6_1_1.
:- pragma termination_info(pl6_1_1:qsort(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), cannot_loop).
New File: tests/term/pl7_2_9.m
===================================================================
:- module pl7_2_9.
:- interface.
:- pred mult(nat::in, nat::in, nat::out) is det.
:- type nat ---> zero ; s(nat).
:- implementation.
mult(zero, _Y, zero).
mult(s(X), Y, Z) :-
mult(X, Y, Z1),
add(Z1, Y, Z).
:- pred add(nat, nat, nat).
:- mode add(in, in, out).
add(zero, Y, Y).
add(s(X), Y, s(Z)) :-
add(X, Y, Z).
New File: tests/term/pl7_2_9.trans_opt_exp
===================================================================
:- module pl7_2_9.
:- pragma termination_info(pl7_2_9:mult(mercury_builtin:in, mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/pl7_6_2a.m
===================================================================
:- module pl7_6_2a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reach(T::in, T::in, list(list(T))::in) is semidet.
:- implementation.
reach(X, Y, Edges) :-
member([X, Y], Edges).
reach(X, Z, Edges) :-
member([X, Y], Edges),
reach(Y, Z, Edges).
:- pred member(T, list(T)).
:- mode member(in, in).
:- mode member(out, in).
member(H, [H | _L]).
member(X, [_H | L]) :-
member(X, L).
New File: tests/term/pl7_6_2a.trans_opt_exp
===================================================================
:- module pl7_6_2a.
:- pragma termination_info(pl7_6_2a:reach(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no, no]), can_loop).
New File: tests/term/pl7_6_2b.m
===================================================================
:- module pl7_6_2b.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reach(T::in, T::in, list(list(T))::in, list(T)::in) is semidet.
:- implementation.
reach(X, Y, Edges, _Visited) :-
member([X, Y], Edges).
reach(X, Z, Edges, Visited) :-
member([X, Y], Edges),
\+ member(Y, Visited),
reach(Y, Z, Edges, [Y | Visited]).
:- pred member(T, list(T)).
:- mode member(in, in).
:- mode member(out, in).
member(H, [H | _L]).
member(X, [_H | L]) :-
member(X, L).
New File: tests/term/pl7_6_2b.trans_opt_exp
===================================================================
:- module pl7_6_2b.
:- pragma termination_info(pl7_6_2b:reach(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no, no, no]), can_loop).
New File: tests/term/pl7_6_2c.m
===================================================================
:- module pl7_6_2c.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred reach(T::in, T::in, list(list(T))::in, list(T)::in) is semidet.
:- implementation.
reach(X, Y, Edges, _Not_Visited) :-
member([X, Y], Edges).
reach(X, Z, Edges, Not_Visited) :-
member([X, Y], Edges),
member(Y, Not_Visited),
delete(Y, Not_Visited, V1),
reach(Y, Z, Edges, V1).
:- pred member(T, list(T)).
:- mode member(in, in).
:- mode member(out, in).
member(H, [H | _L]).
member(X, [_H | L]) :-
member(X, L).
:- pred delete(T, list(T), list(T)).
:- mode delete(out, in, out).
delete(X, [X | Y], Y).
delete(X, [H | T1], [H | T2]) :-
delete(X, T1, T2).
New File: tests/term/pl7_6_2c.trans_opt_exp
===================================================================
:- module pl7_6_2c.
:- pragma termination_info(pl7_6_2c:reach(mercury_builtin:in, mercury_builtin:in, mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no, no, no]), cannot_loop).
New File: tests/term/pl8_2_1.m
===================================================================
:- module pl8_2_1.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
mergesort([], []).
mergesort([E], [E]).
mergesort([E, F | U], V) :-
s([E, F | U], W, Y),
mergesort(W, X),
mergesort(Y, Z),
merge(X, Z, V).
:- pred merge(list(int), list(int), list(int)).
:- mode merge(in, in, out).
merge(X, [], X).
merge([], X, X).
merge([A | X], [B | Y], [A | Z]) :-
A =< B,
merge(X, [B | Y], Z).
merge([A | X], [B | Y], [B | Z]) :-
A > B,
merge([A | X], Y, Z).
:- pred s(list(T), list(T), list(T)).
:- mode s(in, out, out).
s([], [], []).
s([E | U], [E | V], W) :-
s(U, W, V).
New File: tests/term/pl8_2_1.trans_opt_exp
===================================================================
:- module pl8_2_1.
:- pragma termination_info(pl8_2_1:mergesort(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), can_loop).
New File: tests/term/pl8_2_1a.m
===================================================================
:- module pl8_2_1a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred mergesort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
mergesort([], []).
mergesort([E], [E]).
mergesort([X, Y | Z], U) :-
s(Z, V, W),
mergesort([X | V], X1),
mergesort([Y | W], Y1),
merge(X1, Y1, U).
:- pred merge(list(int), list(int), list(int)).
:- mode merge(in, in, out).
merge([], X, X).
merge([A | X], [B | Y], [A | Z]) :-
A =< B,
merge(X, [B | Y], Z).
merge([A | X], [B | Y], [B | Z]) :-
A > B,
merge([A | X], Y, Z).
:- pred s(list(T), list(T), list(T)).
:- mode s(in, out, out).
s([], [], []).
s([E | U], [E | V], W) :-
s(U, W, V).
New File: tests/term/pl8_2_1a.trans_opt_exp
===================================================================
:- module pl8_2_1a.
:- pragma termination_info(pl8_2_1a:mergesort(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), cannot_loop).
New File: tests/term/pl8_3_1.m
===================================================================
:- module pl8_3_1.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred xminsort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
xminsort([], []).
xminsort(L, [X | L1]) :-
xmin1(X, L),
remove(X, L, L2),
xminsort(L2, L1).
:- pred xmin1(int, list(int)).
:- mode xmin1(out, in).
xmin1(M, [X | L]) :-
xmin2(X, M, L).
:- pred xmin2(int, int, list(int)).
:- mode xmin2(in, out, in).
xmin2(X, X, []).
xmin2(X, A, [M | L]) :-
xmin(X, M, B),
xmin2(B, A, L).
:- pred xmin(int, int, int).
:- mode xmin(in, in, out).
xmin(X, Y, X) :-
X =< Y.
xmin(X, Y, Y) :-
X > Y.
:- pred remove(T, list(T), list(T)).
:- mode remove(in, in, out).
remove(_N, [], []).
remove(N, [N | L], L).
remove(N, [M | L], [M | L1]) :-
N \= M,
remove(N, L, L1).
New File: tests/term/pl8_3_1.trans_opt_exp
===================================================================
:- module pl8_3_1.
:- pragma termination_info(pl8_3_1:xminsort(mercury_builtin:in, mercury_builtin:out), infinite, can_loop).
New File: tests/term/pl8_3_1a.m
===================================================================
:- module pl8_3_1a.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred xminsort(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
xminsort([], []).
xminsort(L, [X | L1]) :-
xmin1(X, L),
remove(X, L, L2),
xminsort(L2, L1).
:- pred xmin1(int, list(int)).
:- mode xmin1(out, in).
xmin1(M, [X | L]) :-
xmin2(X, M, L).
:- pred xmin2(int, int, list(int)).
:- mode xmin2(in, out, in).
xmin2(X, X, []).
xmin2(X, A, [M | L]) :-
xmin(X, M, B),
xmin2(B, A, L).
:- pred xmin(int, int, int).
:- mode xmin(in, in, out).
xmin(X, Y, X) :-
X =< Y.
xmin(X, Y, Y) :-
X > Y.
:- pred remove(T, list(T), list(T)).
:- mode remove(in, in, out).
%remove(N, [], []). (this case cannot occur in our program)
remove(N, [N | L], L).
remove(N, [M | L], [M | L1]) :-
\+ N = M,
remove(N, L, L1).
New File: tests/term/pl8_3_1a.trans_opt_exp
===================================================================
:- module pl8_3_1a.
:- pragma termination_info(pl8_3_1a:xminsort(mercury_builtin:in, mercury_builtin:out), infinite, cannot_loop).
New File: tests/term/pl8_4_1.m
===================================================================
:- module pl8_4_1.
:- interface.
:- type nat ---> zero ; s(nat).
:- pred even(nat::in) is semidet.
:- pred odd(nat::in) is semidet.
:- implementation.
even(zero).
even(s(X)) :-
odd(X).
odd(s(X)) :-
even(X).
New File: tests/term/pl8_4_1.trans_opt_exp
===================================================================
:- module pl8_4_1.
:- pragma termination_info(pl8_4_1:even(mercury_builtin:in), finite(0, [no]), cannot_loop).
:- pragma termination_info(pl8_4_1:odd(mercury_builtin:in), finite(0, [no]), cannot_loop).
New File: tests/term/pl8_4_2.m
===================================================================
:- module pl8_4_2.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- type token ---> a ; b ; c ; plus ; times ; lparen ; rparen.
:- pred e(list(token)::in, list(token)::out) is nondet.
:- implementation.
e(L, T) :- t(L, T).
e(L, T) :- t(L, [plus | C]), e(C, T).
:- pred t(list(token), list(token)).
:- mode t(in, out).
t(L, T) :- n(L, T).
t(L, T) :- n(L, [times | C]), t(C, T).
:- pred n(list(token), list(token)).
:- mode n(in, out).
n([L | T], T) :-
z(L).
n([lparen | A], B) :-
e(A, [rparen | B]).
:- pred z(token).
:- mode z(in).
z(a).
z(b).
z(c).
New File: tests/term/pl8_4_2.trans_opt_exp
===================================================================
:- module pl8_4_2.
:- pragma termination_info(pl8_4_2:e(mercury_builtin:in, mercury_builtin:out), finite(-1, [yes, no]), cannot_loop).
New File: tests/term/queens.m
===================================================================
:- module queens.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred queens(list(int), list(int)).
:- mode queens(in, out) is nondet.
:- implementation.
:- import_module int.
queens(X, Y) :-
perm(X, Y),
safe(Y).
:- pred perm(list(T), list(T)).
:- mode perm(in, out).
perm([], []).
perm([X | Y], [V | Res]) :-
delete(V, [X | Y], Rest),
perm(Rest, Res).
:- pred delete(T, list(T), list(T)).
:- mode delete(out, in, out).
delete(X, [X | Y], Y).
delete(X, [F | T], [F | R]) :-
delete(X, T, R).
:- pred safe(list(int)).
:- mode safe(in).
safe([]).
safe([X | Y]) :-
noattack(X, Y, 1),
safe(Y).
:- pred noattack(int, list(int), int).
:- mode noattack(in, in, di).
noattack(_X, [], _N).
noattack(X, [F | T], N) :-
X \= F,
X \= F + N,
F \= X + N,
N1 is N + 1,
noattack(X, T, N1).
New File: tests/term/queens.trans_opt_exp
===================================================================
:- module queens.
:- pragma termination_info(queens:queens(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), cannot_loop).
New File: tests/term/quicksort.m
===================================================================
:- module quicksort.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred qs(list(int)::in, list(int)::out) is nondet.
:- implementation.
:- import_module int.
qs([X | Xs], Ys) :-
part(X, Xs, Littles, Bigs),
qs(Littles, Ls),
qs(Bigs, Bs),
app(Ls, [X | Bs], Ys).
qs([], []).
:- pred part(int, list(int), list(int), list(int)).
:- mode part(in, in, out, out).
part(X, [Y | Xs], [Y | Ls], Bs) :-
X > Y,
part(X, Xs, Ls, Bs).
part(X, [Y | Xs], Ls, [Y | Bs]) :-
X =< Y,
part(X, Xs, Ls, Bs).
part(_X, [], [], []).
:- pred app(list(int), list(int), list(int)).
:- mode app(in, in, out).
app([X | Xs], Ys, [X | Zs]) :-
app(Xs, Ys, Zs).
app([], Ys, Ys).
New File: tests/term/quicksort.trans_opt_exp
===================================================================
:- module quicksort.
:- pragma termination_info(quicksort:qs(mercury_builtin:in, mercury_builtin:out), finite(0, [yes, no]), cannot_loop).
New File: tests/term/runtests
===================================================================
#!/bin/sh
# Test whether the termination analysis algorithm of the Mercury compiler
# is working right.
# Return a status of 0 (true) if everything is all right, and 1 otherwise.
set -x
stdoptions="--make-trans-opt --enable-termination"
options="$stdoptions --term-single-arg 5 --term-norm simple"
modules=`mmake modules`
cat /dev/null > .allres
failure=""
for module in $modules
do
/bin/rm $module.trans_opt > /dev/null 2>&1
lmc3 -C $options $module > $module.out 2>&1
if test "$?" = 0
then
diff -u $module.trans_opt $module.trans_opt_exp > $module.res
cat $module.res >> .allres
else
failure="$failure $module"
fi
done
if test ! -s .allres -a "$failure" = ""
then
echo "the tests in the term directory succeeded"
rm -f .allres
exit 0
else
echo "the tests in the term directory failed"
echo "the following modules had the compiler fail:"
echo $failure
echo "the differences are:"
cat .allres
exit 1
fi
New File: tests/term/select.m
===================================================================
:- module select.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred select(T::out, list(T)::in, list(T)::out) is nondet.
:- implementation.
select(X, [X | Xs], Xs).
select(X, [Y | Xs], [Y | Zs]) :-
select(X, Xs, Zs).
New File: tests/term/select.trans_opt_exp
===================================================================
:- module select.
:- pragma termination_info(select:select(mercury_builtin:out, mercury_builtin:in, mercury_builtin:out), finite(-1, [no, no, yes, no]), cannot_loop).
New File: tests/term/subset.m
===================================================================
:- module subset.
:- interface.
:- type list(T) ---> [] ; [T | list(T)].
:- pred subset(list(T), list(T)).
:- mode subset(in, in) is semidet.
:- mode subset(out, in) is multi. % gets warning
:- implementation.
subset([X | Xs], Ys) :-
member(X, Ys),
subset(Xs, Ys).
subset([], _Ys).
:- pred member(T, list(T)).
:- mode member(out, in).
member(X, [_Y | Xs]) :-
member(X, Xs).
member(X, [X | _Xs]).
New File: tests/term/subset.trans_opt_exp
===================================================================
:- module subset.
:- pragma termination_info(subset:subset(mercury_builtin:in, mercury_builtin:in), finite(0, [no, no, no]), cannot_loop).
:- pragma termination_info(subset:subset(mercury_builtin:out, mercury_builtin:in), infinite, can_loop).
New File: tests/term/sum.m
===================================================================
:- module sum.
:- interface.
:- pred sum(nat, nat, nat).
% :- mode sum(out, in, out) is nondet. SECOND CLAUSE NOT WELL MODED
:- mode sum(out, out, in) is multi.
:- type nat ---> zero ; s(nat).
:- implementation.
sum(X, s(Y), s(Z)) :-
sum(X, Y, Z).
sum(X, zero, X).
New File: tests/term/sum.trans_opt_exp
===================================================================
:- module sum.
:- pragma termination_info(sum:sum(mercury_builtin:out, mercury_builtin:out, mercury_builtin:in), finite(0, [no, no, yes]), cannot_loop).
New File: tests/term/vangelder.m
===================================================================
% The vangelder example from Lindenstrauss and Sagiv
% (takes them more than four minutes to crack).
:- module vangelder.
:- interface.
:- type foo ---> a ; b ; c ; f(foo).
:- pred q(foo, foo).
:- mode q(in, in) is semidet.
:- implementation.
q(X, Y) :-
e(X, Y).
q(X, f(f(X))) :-
p(X, f(f(X))),
q(X, f(X)).
q(X, f(f(Y))) :-
p(X, f(Y)).
:- pred p(foo, foo).
:- mode p(in, in) is semidet.
p(X, Y) :-
e(X, Y).
p(X, f(Y)) :-
r(X, f(Y)),
p(X, Y).
:- pred r(foo, foo).
:- mode r(in, in) is semidet.
r(X, Y) :-
e(X, Y).
r(X, f(Y)) :-
q(X, Y),
r(X, Y).
r(f(X), f(X)) :-
t(f(X), f(X)).
:- pred t(foo, foo).
:- mode t(in, in) is semidet.
t(X, Y) :-
e(X, Y).
t(f(X), f(Y)) :-
q(f(X), f(Y)),
t(X, Y).
:- pred e(foo, foo).
:- mode e(in, in) is semidet.
e(a, b).
New File: tests/term/vangelder.trans_opt_exp
===================================================================
:- module vangelder.
:- pragma termination_info(vangelder:q(mercury_builtin:in, mercury_builtin:in), finite(0, [no, no]), can_loop).
More information about the developers
mailing list