[m-rev.] for review: improve termination analysis of special preds
Julien Fischer
juliensf at cs.mu.OZ.AU
Tue Jan 11 15:07:26 AEDT 2005
Estimated hours taken: 20
Branches: main
Improve the termination analyser's handling of user-defined
special predicates.
Currently termination analysis assumes that all calls
to special predicates terminate. For those that are
user-defined this is not necessarily true.
This diff adds a new pass to the compiler that is run after
the main termination analysis pass. It checks any user-defined
special predicates and emits a warning if their termination
can not be proved.
Add a new option, `--no-warn-non-term-special-preds' that
disables this warning. The warning is only emitted when
termination analysis is enabled. The new option has
no effect if termination analysis is not enabled.
compiler/post_term_analysis.m:
New file. Add an additional pass that runs after the main
termination analysis and makes use of the information obtained
then to perform further semantic checks and optimizations.
compiler/termination.m:
Run the new pass after the main analysis.
Update the comment about the termination analyser doing the
wrong thing for user-defined special predicates.
compiler/options.m:
Parse the new option.
Update the special handler for the inhibit_warning
option so that it handles `--warn-table-with-inline'
and the new option correctly.
Fix some typos.
compiler/transform_hlds.m:
Include the new module.
compiler/notes/compiler_design.html:
Mention the new module.
doc/user_guide.texi:
Document the new option.
Fix some typos: s/occured/occurred/,
s/interative/interactive/, s/exlained/explained/
and /currect/current/
library/array.m:
library/version_array.m:
Add pragma terminates declarations to the user-defined
equality and comparison predicates for the array/1
and version_array/1 types. The termination analyser
cannot (yet) prove termination in these cases because
it cannot reason about iteration over arrays.
tests/warnings/Mercury.options:
tests/warnings/Mmakefile:
tests/warnings/warn_non_term_user_special.m:
tests/warnings/warn_non_term_user_special.exp:
Test the new option.
Index: compiler/options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/options.m,v
retrieving revision 1.439
diff -u -r1.439 options.m
--- compiler/options.m 20 Dec 2004 01:15:42 -0000 1.439
+++ compiler/options.m 10 Jan 2005 12:53:41 -0000
@@ -96,6 +96,7 @@
; warn_stubs
; warn_dead_procs
; warn_table_with_inline
+ ; warn_non_term_special_preds
% Verbosity options
; verbose
; very_verbose
@@ -761,7 +762,8 @@
warn_up_to_date - bool(yes),
warn_stubs - bool(yes),
warn_dead_procs - bool(no),
- warn_table_with_inline - bool(yes)
+ warn_table_with_inline - bool(yes),
+ warn_non_term_special_preds - bool(yes)
]).
option_defaults_2(verbosity_option, [
% Verbosity Options
@@ -1398,6 +1400,7 @@
long_option("warn-stubs", warn_stubs).
long_option("warn-dead-procs", warn_dead_procs).
long_option("warn-table-with-inline", warn_table_with_inline).
+long_option("warn-non-term-special-preds", warn_non_term_special_preds).
% verbosity options
long_option("verbose", verbose).
@@ -1420,7 +1423,7 @@
long_option("debug-rl-gen", debug_rl_gen).
long_option("debug-rl-opt", debug_rl_opt).
% debug-il-asm does very low-level printf style debugging of
- % IL assember. Each instruction is written on stdout before it
+ % IL assembler. Each instruction is written on stdout before it
% is executed. It is a temporary measure until the IL debugging
% system built into .NET improves.
long_option("debug-il-asm", debug_il_asm).
@@ -1555,7 +1558,7 @@
deep_profile_tail_recursion).
long_option("record-term-sizes-as-words", record_term_sizes_as_words).
long_option("record-term-sizes-as-cells", record_term_sizes_as_cells).
- % (c) miscellanous optional features
+ % (c) miscellaneous optional features
long_option("gc", gc).
long_option("garbage-collection", gc).
long_option("parallel", parallel).
@@ -1563,7 +1566,7 @@
long_option("type-layout", type_layout).
long_option("aditi", aditi).
long_option("aditi-calls-mercury", aditi_calls_mercury).
- % Data represention options
+ % Data representation options
long_option("reserve-tag", reserve_tag).
long_option("use-minimal-model-stack_copy", use_minimal_model_stack_copy).
long_option("use-minimal-model-own-stacks", use_minimal_model_own_stacks).
@@ -2103,7 +2106,9 @@
warn_target_code - bool(Enable),
warn_up_to_date - bool(Enable),
warn_stubs - bool(Enable),
- warn_dead_procs - bool(Enable)
+ warn_dead_procs - bool(Enable),
+ warn_table_with_inline - bool(Enable),
+ warn_non_term_special_preds - bool(Enable)
], OptionTable0, OptionTable).
special_handler(infer_all, bool(Infer), OptionTable0, ok(OptionTable)) :-
override_options([
@@ -2624,7 +2629,13 @@
"\ttarget code (e.g. gcc).",
"--no-warn-table-with-inline",
"\tDisable warnings about tabled procedures that also have",
- "\ta `pragma inline' declaration."
+ "\ta `pragma inline' declaration.",
+ "--no-warn-non-term-special-preds",
+ "\tDo not warn about types that have user-defined equality or",
+ "\tcomparison predicates, or solver type initialisation predicates",
+ "\tthat cannot be proved to terminate. This option is only",
+ "\tenabled when termination analysis is enabled.",
+ "\t(See the ""Termination Analysis Options"" section below)."
]).
:- pred options_help_verbosity(io::di, io::uo) is det.
Index: compiler/post_term_analysis.m
===================================================================
RCS file: compiler/post_term_analysis.m
diff -N compiler/post_term_analysis.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/post_term_analysis.m 11 Jan 2005 03:52:01 -0000
@@ -0,0 +1,252 @@
+%----------------------------------------------------------------------------%
+% Copyright (C) 2005 The University of Melbourne.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%----------------------------------------------------------------------------%
+%
+% File: post_term_analysis.m
+% Main author: juliensf
+%
+% This module contains various checks that rely on the information
+% produced by termination analysis.
+%
+% Currently, the only thing implemented in this module is a check to see
+% if user-defined special predicates terminate. A warning is emitted
+% for all those that do not.
+%
+%----------------------------------------------------------------------------%
+
+:- module transform_hlds.post_term_analysis.
+
+:- interface.
+
+:- import_module hlds.hlds_module.
+
+:- import_module io.
+
+:- pred post_term_analysis.process_module(module_info::in, io::di, io::uo)
+ is det.
+
+%----------------------------------------------------------------------------%
+%----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module backend_libs.
+:- import_module backend_libs.foreign.
+
+:- import_module hlds.goal_form.
+:- import_module hlds.goal_util.
+:- import_module hlds.hlds_data.
+:- import_module hlds.hlds_error_util.
+:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_out.
+:- import_module hlds.hlds_pred.
+:- import_module hlds.special_pred.
+
+
+:- import_module libs.globals.
+:- import_module libs.options.
+
+:- import_module parse_tree.error_util.
+:- import_module parse_tree.prog_data.
+
+:- import_module bool, list, map, std_util, string.
+
+%----------------------------------------------------------------------------%
+
+post_term_analysis.process_module(ModuleInfo, !IO) :-
+ warn_non_term_user_special_preds(ModuleInfo, !IO).
+
+%----------------------------------------------------------------------------%
+%
+% Warn about user-defined special predicates that do not terminate.
+%
+
+% We check the termination status of user-defined special predicates by
+% taking the body goal of the compiler generated wrapper predicate and
+% checking if that terminates. We cannot check the termination status
+% of the compiler generated wrappers directly, because termination analysis
+% always assumes that they terminate.
+%
+% Since all of the special predicates of interest here have to be defined
+% in the same module as the type that uses them, we only check locally
+% defined types. The ones for imported types will be checked when the
+% relevant module is compiled and analysed.
+
+:- pred warn_non_term_user_special_preds(module_info::in, io::di, io::uo)
+ is det.
+
+warn_non_term_user_special_preds(ModuleInfo, !IO) :-
+ globals.io_lookup_bool_option(termination, Termination, !IO),
+ globals.io_lookup_bool_option(warn_non_term_special_preds,
+ WarnSpecialPreds, !IO),
+ globals.io_lookup_bool_option(make_optimization_interface,
+ MakeOptInt, !IO),
+ globals.io_lookup_bool_option(transitive_optimization,
+ TransIntermodOpt, !IO),
+ (
+ Termination = yes, WarnSpecialPreds = yes,
+ %
+ % Don't run this pass if we are only building the
+ % optimization inferface and we are compiling
+ % with `--transitive-intermodule-optimization'
+ % enabled because we'll get more accurate results
+ % when we build the .trans_opt files. Any warnings
+ % this time around may be spurious.
+ %
+ not (MakeOptInt = yes, TransIntermodOpt = yes)
+ ->
+ module_info_get_special_pred_map(ModuleInfo,
+ SpecialPredMap),
+ module_info_types(ModuleInfo, TypeTable),
+ map.foldl(warn_non_term_user_special_pred(ModuleInfo,
+ TypeTable), SpecialPredMap, !IO)
+ ;
+ true
+ ).
+
+:- pred warn_non_term_user_special_pred(module_info::in, type_table::in,
+ special_pred::in, pred_id::in, io::di, io::uo) is det.
+
+warn_non_term_user_special_pred(ModuleInfo, TypeTable,
+ SpecialPredId - TypeCtor, PredId, !IO) :-
+ %
+ % index predicate cannot be defined by the user and should
+ % always terminate in any case.
+ %
+ ( SpecialPredId \= index ->
+ map.lookup(TypeTable, TypeCtor, TypeDefn),
+ get_type_defn_status(TypeDefn, ImportStatus),
+ (
+ status_defined_in_this_module(ImportStatus, yes)
+ ->
+ process_special_pred_for_type(ModuleInfo,
+ SpecialPredId, TypeCtor, PredId, TypeDefn, !IO)
+ ;
+ true
+ )
+ ;
+ true
+ ).
+
+ % If the specified special predicate for the given type is user-defined
+ % then check that it terminates. Emit a warning if it does not.
+ %
+:- pred process_special_pred_for_type(module_info::in,
+ special_pred_id::in, type_ctor::in, pred_id::in,
+ hlds_type_defn::in, io::di, io::uo) is det.
+
+process_special_pred_for_type(ModuleInfo, SpecialPredId, TypeCtor,
+ PredId, TypeDefn, !IO) :-
+ (
+ special_pred_needs_term_check(ModuleInfo, SpecialPredId,
+ TypeDefn)
+ ->
+ % Compiler generated special preds are always mode 0.
+ proc_id_to_int(ProcId, 0),
+ module_info_pred_proc_info(ModuleInfo,
+ PredId, ProcId, _, ProcInfo),
+ proc_info_goal(ProcInfo, BodyGoal),
+ %
+ % We cannot just look up the the termination_info because
+ % the termination status of compiler generated wrapper
+ % predicates for special preds is always set to terminates.
+ % Instead, we check if the body goal of the generated wrapper
+ % predicate terminates.
+ %
+ ( not goal_cannot_loop(ModuleInfo, BodyGoal) ->
+ get_type_defn_context(TypeDefn, Context),
+ emit_warning(Context, SpecialPredId,
+ TypeCtor, !IO)
+ ;
+ true
+ )
+ ;
+ true
+ ).
+
+ % Succeeds if the specified type of special_pred for this
+ % type needs to have its termination status checked.
+ %
+:- pred special_pred_needs_term_check(module_info::in,
+ special_pred_id::in, hlds_type_defn::in) is semidet.
+
+special_pred_needs_term_check(ModuleInfo, SpecialPredId, TypeDefn) :-
+ get_type_defn_body(TypeDefn, TypeBody),
+ (
+ % Always check solver type initialisation
+ % predicates since they are always user-defined.
+ SpecialPredId = initialise
+ ;
+ get_user_unify_compare(ModuleInfo, TypeBody,
+ UnifyCompare),
+ (
+ UnifyCompare = unify_compare(MaybeUnify,
+ MaybeCompare),
+ (
+ MaybeUnify = yes(_),
+ SpecialPredId = unify
+ ;
+ MaybeCompare = yes(_),
+ SpecialPredId = compare
+ )
+ ;
+ UnifyCompare = abstract_noncanonical_type(_),
+ unexpected(this_file, "special_pred_needs_term" ++
+ "_check/3: type is local and " ++
+ "abstract_noncanonical")
+ )
+ ).
+
+ % Succeeds if the given type has user-defined equality and/or
+ % comparison and returns the relevant information about which
+ % predicates implement it.
+ %
+:- pred get_user_unify_compare(module_info::in, hlds_type_body::in,
+ unify_compare::out) is semidet.
+
+get_user_unify_compare(_ModuleInfo, du_type(_, _, _, yes(UnifyCompare), _, _),
+ UnifyCompare).
+get_user_unify_compare(ModuleInfo, foreign_type(ForeignTypeBody),
+ UnifyCompare) :-
+ UnifyCompare = foreign_type_body_has_user_defined_eq_comp_pred(
+ ModuleInfo, ForeignTypeBody).
+get_user_unify_compare(_ModuleInfo, solver_type(_, yes(UnifyCompare)),
+ UnifyCompare).
+
+:- pred emit_warning(prog_context::in, special_pred_id::in, type_ctor::in,
+ io::di, io::uo) is det.
+
+emit_warning(Context, SpecialPred, TypeCtor, !IO) :-
+ TypeCtorString = hlds_out.type_ctor_to_string(TypeCtor),
+ (
+ SpecialPred = unify,
+ SpecialPredStr = "equality"
+ ;
+ SpecialPred = compare,
+ SpecialPredStr = "comparison"
+ ;
+ SpecialPred = initialise,
+ SpecialPredStr = "initialisation"
+ ;
+ SpecialPred = index,
+ unexpected(this_file, "emit_warning/5 index predicate.")
+ ),
+ Pieces = [words("Warning: the user-defined "),
+ fixed(SpecialPredStr ++ " predicate"),
+ words("for the type "),
+ fixed(TypeCtorString),
+ words("cannot be proven to terminate.")
+ ],
+ report_warning(Context, 0, Pieces, !IO).
+
+%----------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "post_term_analysis.m".
+
+%----------------------------------------------------------------------------%
+:- end_module post_term_analysis.
+%----------------------------------------------------------------------------%
Index: compiler/termination.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/termination.m,v
retrieving revision 1.44
diff -u -r1.44 termination.m
--- compiler/termination.m 5 Sep 2004 23:52:46 -0000 1.44
+++ compiler/termination.m 10 Jan 2005 14:09:32 -0000
@@ -85,6 +85,7 @@
:- import_module parse_tree__prog_out.
:- import_module parse_tree__prog_util.
:- import_module transform_hlds__dependency_graph.
+:- import_module transform_hlds__post_term_analysis.
:- import_module transform_hlds__term_errors.
:- import_module transform_hlds__term_norm.
:- import_module transform_hlds__term_pass1.
@@ -132,7 +133,8 @@
termination__make_opt_int(PredIds, !.Module, !IO)
;
true
- ).
+ ),
+ post_term_analysis__process_module(!.Module, !IO).
%----------------------------------------------------------------------------%
%
@@ -641,8 +643,8 @@
% If it is, then the compiler sets the termination property of the ProcIds
% accordingly.
-% XXX This does the wrong thing for calls to unify/2,
-% which might not terminate in the case of user-defined equality predicates.
+% We assume that user-defined special predicates terminate. This
+% assumption is checked later during the post_term_analysis pass.
:- pred set_compiler_gen_terminates(pred_info::in, list(proc_id)::in,
pred_id::in, module_info::in, proc_table::in, proc_table::out)
Index: compiler/transform_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/transform_hlds.m,v
retrieving revision 1.11
diff -u -r1.11 transform_hlds.m
--- compiler/transform_hlds.m 16 Oct 2004 15:07:33 -0000 1.11
+++ compiler/transform_hlds.m 4 Jan 2005 06:12:57 -0000
@@ -37,6 +37,8 @@
:- include_module term_util.
:- include_module lp. % this could alternatively go in the `libs' module
+:- include_module post_term_analysis.
+
:- include_module exception_analysis.
% Optimizations (HLDS -> HLDS)
Index: compiler/notes/compiler_design.html
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/notes/compiler_design.html,v
retrieving revision 1.94
diff -u -r1.94 compiler_design.html
--- compiler/notes/compiler_design.html 20 Dec 2004 01:15:46 -0000 1.94
+++ compiler/notes/compiler_design.html 10 Jan 2005 02:20:30 -0000
@@ -801,6 +801,9 @@
term_util.m defines the main types used in termination analysis
and contains utility predicates.
<li>
+post_term_analysis.m contains error checking routines and optimizations
+that depend upon the information obtained by termination analysis.
+<li>
lp.m is used by term_pass1.m. It implements the Linear Programming
algorithm for optimizing a set of linear constraints with respect to
a linear cost function. (XXX Perhaps this should be put in the libs.m
Index: doc/user_guide.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/user_guide.texi,v
retrieving revision 1.408
diff -u -r1.408 user_guide.texi
--- doc/user_guide.texi 9 Jan 2005 01:14:04 -0000 1.408
+++ doc/user_guide.texi 10 Jan 2005 12:12:21 -0000
@@ -3747,7 +3747,7 @@
and prints the question @samp{Expected?} for the user to answer.
In addition to asserting whether a call behaved correctly or not
-the user may also assert that a call should never have occured in the first
+the user may also assert that a call should never have occurred in the first
place, because its inputs violated some precondition of the call. For example
if an unsorted list is passed to a predicate that is only designed to work with
sorted lists. Such calls should be deemed @emph{inadmissible} by the user.
@@ -3797,7 +3797,7 @@
While browsing a @samp{mark} command may be issued to assert that
the current subterm is incorrect (see @ref{Improving the search}).
To return to the declarative debugger question issue a @samp{quit}
-command from within the interative term browser. For more information
+command from within the interactive term browser. For more information
on the use of the interactive term browser see the @samp{browse} command
in @ref{Browsing commands} or type @samp{help} from within the
interactive query browser.
@@ -3940,7 +3940,7 @@
The number of questions asked by the declarative debugger before it pinpoints
the location of a bug can be reduced by giving it extra information. The kind
of extra information that can be given and how to convey this information are
-exlained in this section.
+explained in this section.
@subsubsection Marking incorrect subterms
@@ -4048,7 +4048,7 @@
debugger to trust the predicate or function in the current question.
Alternatively the user may tell the declarative debugger to trust all the
predicates and functions in the same module as the predicate or function in the
-currect question. See the @samp{trust} command in
+current question. See the @samp{trust} command in
@ref{Declarative debugging commands}.
@c ----------------------------------------------------------------------------
@@ -4770,6 +4770,15 @@
@findex --no-warn-table-with-inline
Disable warnings about tabled procedures that also have
a `pragma inline' declaration.
+
+ at sp 1
+ at item --no-warn-non-term-special-preds
+ at findex --no-warn-non-term-special-preds
+Do not warn about types that have user-defined equality or
+comparison predicates, or solver type initialisation predicates
+that cannot be proved to terminate. This option is only
+enabled when termination analysis is enabled.
+(See @ref{Termination analysis options} for further details).
@end table
Index: library/array.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/array.m,v
retrieving revision 1.134
diff -u -r1.134 array.m
--- library/array.m 28 Sep 2004 02:09:14 -0000 1.134
+++ library/array.m 10 Jan 2005 15:33:44 -0000
@@ -395,6 +395,7 @@
:- pred array_equal(array(T)::in, array(T)::in) is semidet.
:- pragma export(array_equal(in, in), "ML_array_equal").
+:- pragma terminates(array_equal/2).
array_equal(Array1, Array2) :-
( if
@@ -424,6 +425,7 @@
:- pred array_compare(comparison_result::uo, array(T)::in, array(T)::in)
is det.
:- pragma export(array_compare(uo, in, in), "ML_array_compare").
+:- pragma terminates(array_compare/3).
array_compare(Result, Array1, Array2) :-
array__size(Array1, Size1),
Index: library/version_array.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/version_array.m,v
retrieving revision 1.4
diff -u -r1.4 version_array.m
--- library/version_array.m 8 Oct 2004 07:01:28 -0000 1.4
+++ library/version_array.m 10 Jan 2005 16:40:58 -0000
@@ -247,6 +247,7 @@
% grades.
:- type version_array(T) ---> version_array(T).
+:- pragma terminates(eq_version_array/2).
:- pred eq_version_array(version_array(T)::in, version_array(T)::in)
is semidet.
@@ -267,7 +268,7 @@
true
).
-
+:- pragma terminates(cmp_version_array/3).
:- pred cmp_version_array(comparison_result::uo,
version_array(T)::in, version_array(T)::in) is det.
Index: tests/warnings/Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/warnings/Mercury.options,v
retrieving revision 1.10
diff -u -r1.10 Mercury.options
--- tests/warnings/Mercury.options 12 Feb 2004 03:36:17 -0000 1.10
+++ tests/warnings/Mercury.options 10 Jan 2005 14:01:36 -0000
@@ -40,5 +40,6 @@
MCFLAGS-pragma_term_conflict = --enable-termination
MCFLAGS-term_indirect_warning = --check-termination
MCFLAGS-foreign_term_invalid = --enable-termination
+MCFLAGS-non_term_user_special = --enable-termination
MCFLAGS-warn_dead_procs = --warn-dead-procs --infer-all
Index: tests/warnings/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/warnings/Mmakefile,v
retrieving revision 1.35
diff -u -r1.35 Mmakefile
--- tests/warnings/Mmakefile 5 Nov 2004 05:39:08 -0000 1.35
+++ tests/warnings/Mmakefile 10 Jan 2005 14:01:27 -0000
@@ -7,6 +7,7 @@
COMPILE_PROGS= \
arg_order_rearrangment \
foreign_term_invalid \
+ non_term_user_special \
pragma_term_conflict \
term_indirect_warning \
warn_dead_procs
Index: tests/warnings/non_term_user_special.exp
===================================================================
RCS file: tests/warnings/non_term_user_special.exp
diff -N tests/warnings/non_term_user_special.exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/warnings/non_term_user_special.exp 10 Jan 2005 14:00:28 -0000
@@ -0,0 +1,9 @@
+non_term_user_special.m:007: Warning: the user-defined equality predicate for
+non_term_user_special.m:007: the type non_term_user_special.myset/1 cannot be
+non_term_user_special.m:007: proven to terminate.
+non_term_user_special.m:007: Warning: the user-defined comparison predicate for
+non_term_user_special.m:007: the type non_term_user_special.myset/1 cannot be
+non_term_user_special.m:007: proven to terminate.
+non_term_user_special.m:039: Warning: the user-defined initialisation predicate
+non_term_user_special.m:039: for the type non_term_user_special.foo/0 cannot
+non_term_user_special.m:039: be proven to terminate.
Index: tests/warnings/non_term_user_special.m
===================================================================
RCS file: tests/warnings/non_term_user_special.m
diff -N tests/warnings/non_term_user_special.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/warnings/non_term_user_special.m 10 Jan 2005 13:59:00 -0000
@@ -0,0 +1,53 @@
+:- module non_term_user_special.
+
+:- interface.
+
+:- import_module list.
+
+:- type myset(T) ---> myset(list(T))
+ where equality is my_set_equals,
+ comparison is my_set_compare.
+
+:- pred my_set_equals(myset(T)::in, myset(T)::in) is semidet.
+
+:- pred my_set_compare(builtin.comparison_result::uo, myset(T)::in,
+ myset(T)::in) is det.
+
+:- solver type foo(T).
+
+:- implementation.
+
+my_set_equals(_, _) :- loop.
+
+:- pred loop is semidet.
+
+loop :- a.
+
+:- pred a is semidet.
+:- pred b is semidet.
+
+a :- b.
+b :- a.
+
+my_set_compare(Res, _, _) :-
+ ( loop ->
+ Res = (=)
+ ;
+ Res = (=)
+ ).
+
+:- solver type foo
+ where representation is int,
+ initialisation is init_foo,
+ ground is ground,
+ any is ground.
+
+:- pragma promise_pure(init_foo/1).
+:- pred init_foo(foo::out(any)) is det.
+init_foo(X) :-
+ ( loop ->
+ Y = 42
+ ;
+ Y = 43
+ ),
+ impure X = 'representation to any foo/0'(Y).
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list