[m-rev.] for review: fix contravariance mode bug
David Overton
dmo at cs.mu.OZ.AU
Mon Jul 28 18:50:26 AEST 2003
On Fri, Jul 25, 2003 at 06:30:04AM +1000, Mercury wrote:
> The following program fails to compile, due to a problem with
> co/contravariance in higher-order inst matching.
>
> :- module bug2.
> :- interface.
> :- import_module io.
>
> :- pred main(io__state::di, io__state::uo) is det.
>
> :- implementation.
> :- import_module list, bool.
>
> main -->
> ( { q(p) } ->
> print("yes"), nl
> ;
> print("no"), nl
> ).
>
> :- type intlist == list(int).
> :- inst nonempty ---> [ground|list].
> :- inst list ---> [ground|list] ; [].
>
> :- pred p(intlist, intlist).
> :- mode p((list -> nonempty), (free -> nonempty)) is semidet.
>
> p([X], [X]).
> p([X,Y|Zs], [Y,X|Zs]).
>
> :- pred q(pred(intlist, intlist)).
> :- mode q(pred((nonempty -> nonempty), (free -> list)) is semidet) is semidet.
>
> q(P) :- P([1], L), L \= [].
Estimated hours taken: 8
Branches: main
compiler/inst_match.m:
Fix a bug which was causing the mode system to be
overly-conservative: pred_inst_matches was requiring initial
insts of higher-order arguments to match invariantly rather than
contravariantly. The bug was caused by my change to add support
for mode polymorphism. In that change I added a call to
inst_matches_initial to compute the inst variable substitution
for the higher-order inst.
This change modifies inst_matches_final to compute the substitution
that was previously computed by inst_matches_initial, thus
allowing the call to inst_matches_initial to be removed.
However, because the initial inst test is required to be
contravariant, the call to inst_matches_final swaps the
argument insts. We must allow for this inside
inst_matches_final when computing the substitution.
Also add a predicate inst_matches_initial_no_implied_modes which
is similar to inst_matches_initial, but does not allow implied
modes to match. The predicate inst_matches_final was previously
being used for this task, but it does not handle constrained
inst variables correctly.
compiler/modecheck_call.m:
compiler/modes.m:
Use inst_matches_initial_no_implied_modes instead of
inst_matches_final, where appropriate.
tests/hard_coded/Mmakefile:
tests/hard_coded/contravariance_bug.m:
tests/hard_coded/contravariance_bug.exp:
Add a test case supplied by Fergus.
tests/hard_coded/Mmakefile:
tests/hard_coded/contravariance_poly.m:
tests/hard_coded/contravariance_poly.exp:
Add another test case, similar to the above, but using
polymorphic modes.
Index: compiler/inst_match.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_match.m,v
retrieving revision 1.54
diff -u -r1.54 inst_match.m
--- compiler/inst_match.m 25 Jul 2003 02:27:19 -0000 1.54
+++ compiler/inst_match.m 28 Jul 2003 06:25:04 -0000
@@ -85,6 +85,20 @@
inst_var_sub, inst_var_sub).
:- mode inst_matches_initial(in, in, in, in, out, in, out) is semidet.
+ % This version of inst_matches_initial does not allow implied modes.
+ % This makes it almost the same as inst_matches_final. The only
+ % different is in the way it handles constrained_inst_vars.
+
+:- pred inst_matches_initial_no_implied_modes(inst, inst, type, module_info).
+:- mode inst_matches_initial_no_implied_modes(in, in, in, in) is semidet.
+
+ % A version of the above that also computes the inst_var_sub.
+
+:- pred inst_matches_initial_no_implied_modes(inst, inst, type, module_info,
+ module_info, inst_var_sub, inst_var_sub).
+:- mode inst_matches_initial_no_implied_modes(in, in, in, in, out, in, out)
+ is semidet.
+
% inst_matches_final(InstA, InstB, ModuleInfo):
% Succeed iff InstA is compatible with InstB,
% i.e. iff InstA will satisfy the final inst
@@ -327,13 +341,28 @@
error("inst_matches_initial: missing inst_var_sub")
).
+inst_matches_initial_no_implied_modes(InstA, InstB, Type, ModuleInfo) :-
+ Info0 = init_inst_match_info(ModuleInfo) ^ calculate_sub := forward,
+ inst_matches_final_2(InstA, InstB, yes(Type), Info0, _).
+
+inst_matches_initial_no_implied_modes(InstA, InstB, Type, ModuleInfo0,
+ ModuleInfo, Sub0, Sub) :-
+ Info0 = (init_inst_match_info(ModuleInfo0)
+ ^ calculate_sub := forward)
+ ^ maybe_sub := yes(Sub0),
+ inst_matches_final_2(InstA, InstB, yes(Type), Info0, Info),
+ ModuleInfo = Info ^ module_info,
+ yes(Sub) = Info ^ maybe_sub.
+
:- pred inst_matches_initial_1(inst, inst, type, module_info, module_info,
maybe(inst_var_sub), maybe(inst_var_sub)).
:- mode inst_matches_initial_1(in, in, in, in, out, in, out) is semidet.
inst_matches_initial_1(InstA, InstB, Type, ModuleInfo0, ModuleInfo,
MaybeSub0, MaybeSub) :-
- Info0 = init_inst_match_info(ModuleInfo0) ^ maybe_sub := MaybeSub0,
+ Info0 = (init_inst_match_info(ModuleInfo0)
+ ^ maybe_sub := MaybeSub0)
+ ^ calculate_sub := forward,
inst_matches_initial_2(InstA, InstB, yes(Type), Info0, Info),
ModuleInfo = Info^module_info,
MaybeSub = Info ^ maybe_sub.
@@ -358,10 +387,25 @@
module_info :: module_info,
expansions :: expansions,
maybe_sub :: maybe(inst_var_sub),
+ calculate_sub :: calculate_sub,
uniqueness_comparison :: uniqueness_comparison,
any_matches_any :: bool
).
+ % The calculate_sub type determines how the inst var substitution
+ % should be calculated.
+:- type calculate_sub
+ ---> forward
+ % Calculate in the (normal) forward direction
+ % (used by inst_matches_initial).
+ ; reverse
+ % Calculate in the reverse direction. Used by the call
+ % to inst_matches_final from pred_inst_argmodes_match
+ % to ensure contravariance of the initial argument
+ % insts of higher order pred insts.
+ ; none.
+ % Do not calculate inst var substitions.
+
:- func sub(inst_match_info) = inst_var_sub is semidet.
sub(Info) = Sub :-
@@ -375,12 +419,32 @@
:- func init_inst_match_info(module_info) = inst_match_info.
init_inst_match_info(ModuleInfo) =
- inst_match_info(ModuleInfo, Exp, no, match, yes) :-
+ inst_match_info(ModuleInfo, Exp, no, none, match, yes) :-
set__init(Exp).
-:- pred inst_matches_initial_2(inst, inst, maybe(type),
+:- pred swap_sub(pred(inst_match_info, inst_match_info),
inst_match_info, inst_match_info).
-:- mode inst_matches_initial_2(in, in, in, in, out) is semidet.
+:- mode swap_sub(pred(in, out) is semidet, in, out) is semidet.
+
+swap_sub(P, Info0, Info) :-
+ CalculateSub = Info0 ^ calculate_sub,
+ Info1 = Info0 ^ calculate_sub := swap_calculate_sub(CalculateSub),
+ P(Info1, Info2),
+ Info = Info2 ^ calculate_sub := CalculateSub.
+
+:- func swap_calculate_sub(calculate_sub) = calculate_sub.
+
+swap_calculate_sub(forward) = reverse.
+swap_calculate_sub(reverse) = forward.
+swap_calculate_sub(none) = none.
+
+:- type inst_matches_pred ==
+ pred(inst, inst, maybe(type), inst_match_info, inst_match_info).
+:- inst inst_matches_pred ==
+ (pred(in, in, in, in, out) is semidet).
+
+:- pred inst_matches_initial_2 `with_type` inst_matches_pred.
+:- mode inst_matches_initial_2 `with_inst` inst_matches_pred.
inst_matches_initial_2(InstA, InstB, Type, Info0, Info) :-
ThisExpansion = InstA - InstB,
@@ -391,21 +455,43 @@
inst_expand(Info0^module_info, InstA, InstA2),
inst_expand(Info0^module_info, InstB, InstB2),
set__insert(Info0^expansions, ThisExpansion, Expansions1),
- inst_matches_initial_3(InstA2, InstB2, Type,
+ handle_inst_var_subs(inst_matches_initial_2,
+ inst_matches_initial_4, InstA2, InstB2, Type,
Info0^expansions := Expansions1, Info)
).
-:- pred inst_matches_initial_3(inst, inst, maybe(type),
- inst_match_info, inst_match_info).
-:- mode inst_matches_initial_3(in, in, in, in, out) is semidet.
+:- pred handle_inst_var_subs(inst_matches_pred, inst_matches_pred) `with_type`
+ inst_matches_pred.
+:- mode handle_inst_var_subs(in(inst_matches_pred), in(inst_matches_pred))
+ `with_inst` inst_matches_pred.
-inst_matches_initial_3(InstA, InstB, Type, Info0, Info) :-
+handle_inst_var_subs(Recurse, Continue, InstA, InstB, Type, Info0, Info) :-
+ CalculateSub = Info0 ^ calculate_sub,
+ (
+ CalculateSub = forward,
+ handle_inst_var_subs_2(Recurse, Continue, InstA, InstB,
+ Type, Info0, Info)
+ ;
+ CalculateSub = reverse,
+ handle_inst_var_subs_2(swap_args(Recurse), swap_args(Continue),
+ InstB, InstA, Type, Info0, Info)
+ ;
+ CalculateSub = none,
+ Continue(InstA, InstB, Type, Info0, Info)
+ ).
+
+:- pred handle_inst_var_subs_2(inst_matches_pred, inst_matches_pred) `with_type`
+ inst_matches_pred.
+:- mode handle_inst_var_subs_2(in(inst_matches_pred), in(inst_matches_pred))
+ `with_inst` inst_matches_pred.
+
+handle_inst_var_subs_2(Recurse, Continue, InstA, InstB, Type, Info0, Info) :-
( InstB = constrained_inst_vars(InstVarsB, InstB1) ->
% InstB is a constrained_inst_var with upper bound InstB1.
% We need to check that InstA matches_initial InstB1 and add the
% appropriate inst_var substitution.
- inst_matches_initial_2(InstA, InstB1, Type, Info0, Info1),
+ Recurse(InstA, InstB1, Type, Info0, Info1),
ModuleInfo0 = Info1^module_info,
@@ -419,14 +505,19 @@
Info2 = Info1 ^ module_info := ModuleInfo1,
update_inst_var_sub(InstVarsB, Inst, Type, Info2, Info)
; InstA = constrained_inst_vars(_InstVarsA, InstA1) ->
- inst_matches_initial_2(InstA1, InstB, Type, Info0, Info)
+ Recurse(InstA1, InstB, Type, Info0, Info)
;
- inst_matches_initial_4(InstA, InstB, Type, Info0, Info)
+ Continue(InstA, InstB, Type, Info0, Info)
).
-:- pred inst_matches_initial_4(inst, inst, maybe(type),
- inst_match_info, inst_match_info).
-:- mode inst_matches_initial_4(in, in, in, in, out) is semidet.
+:- pred swap_args(inst_matches_pred) `with_type` inst_matches_pred.
+:- mode swap_args(in(inst_matches_pred)) `with_inst` inst_matches_pred.
+
+swap_args(P, InstA, InstB, Type, Info0, Info) :-
+ P(InstB, InstA, Type, Info0, Info).
+
+:- pred inst_matches_initial_4 `with_type` inst_matches_pred.
+:- mode inst_matches_initial_4 `with_inst` inst_matches_pred.
% To avoid infinite regress, we assume that
% inst_matches_initial is true for any pairs of insts which
@@ -644,44 +735,10 @@
{ PredInstB = pred_inst_info(function, ArgModes, _Det) },
{ Arity = list__length(ArgModes) },
{ PredInstA = pred_inst_info_standard_func_mode(Arity) },
- pred_inst_matches_initial(PredInstA, PredInstB, Type).
+ pred_inst_matches_2(PredInstA, PredInstB, Type).
ground_inst_info_matches_initial(higher_order(PredInstA),
higher_order(PredInstB), _, MaybeType) -->
- pred_inst_matches_initial(PredInstA, PredInstB, MaybeType).
-
-:- pred pred_inst_matches_initial(pred_inst_info, pred_inst_info, maybe(type),
- inst_match_info, inst_match_info).
-:- mode pred_inst_matches_initial(in, in, in, in, out) is semidet.
-
-pred_inst_matches_initial(pred_inst_info(PredOrFunc, ModesA, Det),
- pred_inst_info(PredOrFunc, ModesB, Det), MaybeType) -->
- { maybe_get_higher_order_arg_types(MaybeType, length(ModesA),
- MaybeTypes) },
- pred_inst_argmodes_matches_initial(ModesA, ModesB, MaybeTypes),
- (
- Sub =^ sub
- ->
- { mode_list_apply_substitution(ModesA, Sub, ModesASub) },
- { mode_list_apply_substitution(ModesB, Sub, ModesBSub) }
- ;
- { ModesASub = ModesA },
- { ModesBSub = ModesB }
- ),
- pred_inst_argmodes_matches(ModesASub, ModesBSub, MaybeTypes).
-
-:- pred pred_inst_argmodes_matches_initial(list(mode), list(mode),
- list(maybe(type)), inst_match_info, inst_match_info).
-:- mode pred_inst_argmodes_matches_initial(in, in, in, in, out) is semidet.
-
-pred_inst_argmodes_matches_initial([], [], []) --> [].
-pred_inst_argmodes_matches_initial([ModeA|ModeAs], [ModeB|ModeBs],
- [Type|Types]) -->
- ModuleInfo0 =^ module_info,
- { mode_get_insts(ModuleInfo0, ModeA, InitialA, FinalA) },
- { mode_get_insts(ModuleInfo0, ModeB, InitialB, FinalB) },
- inst_matches_initial_2(InitialA, InitialB, Type),
- inst_matches_initial_2(FinalA, FinalB, Type),
- pred_inst_argmodes_matches_initial(ModeAs, ModeBs, Types).
+ pred_inst_matches_2(PredInstA, PredInstB, MaybeType).
pred_inst_matches(PredInstA, PredInstB, ModuleInfo) :-
pred_inst_matches_1(PredInstA, PredInstB, no, ModuleInfo).
@@ -737,7 +794,7 @@
ModuleInfo =^ module_info,
{ mode_get_insts(ModuleInfo, ModeA, InitialA, FinalA) },
{ mode_get_insts(ModuleInfo, ModeB, InitialB, FinalB) },
- inst_matches_final_2(InitialB, InitialA, MaybeType),
+ swap_sub(inst_matches_final_2(InitialB, InitialA, MaybeType)),
inst_matches_final_2(FinalA, FinalB, MaybeType),
pred_inst_argmodes_matches(ModeAs, ModeBs, MaybeTypes).
@@ -885,9 +942,8 @@
Info0 = init_inst_match_info(ModuleInfo),
inst_matches_final_2(InstA, InstB, yes(Type), Info0, _).
-:- pred inst_matches_final_2(inst, inst, maybe(type),
- inst_match_info, inst_match_info).
-:- mode inst_matches_final_2(in, in, in, in, out) is semidet.
+:- pred inst_matches_final_2 `with_type` inst_matches_pred.
+:- mode inst_matches_final_2 `with_inst` inst_matches_pred.
inst_matches_final_2(InstA, InstB, MaybeType, Info0, Info) :-
ThisExpansion = InstA - InstB,
@@ -899,13 +955,13 @@
inst_expand(Info0^module_info, InstA, InstA2),
inst_expand(Info0^module_info, InstB, InstB2),
set__insert(Info0^expansions, ThisExpansion, Expansions1),
- inst_matches_final_3(InstA2, InstB2, MaybeType,
+ handle_inst_var_subs(inst_matches_final_2, inst_matches_final_3,
+ InstA2, InstB2, MaybeType,
Info0^expansions := Expansions1, Info)
).
-:- pred inst_matches_final_3(inst, inst, maybe(type),
- inst_match_info, inst_match_info).
-:- mode inst_matches_final_3(in, in, in, in, out) is semidet.
+:- pred inst_matches_final_3 `with_type` inst_matches_pred.
+:- mode inst_matches_final_3 `with_inst` inst_matches_pred.
inst_matches_final_3(any(UniqA), any(UniqB), _, I, I) :-
unique_matches_final(UniqA, UniqB).
@@ -1059,9 +1115,8 @@
Info0 = init_inst_match_info(ModuleInfo),
inst_matches_binding_2(InstA, InstB, yes(Type), Info0, _).
-:- pred inst_matches_binding_2(inst, inst, maybe(type), inst_match_info,
- inst_match_info).
-:- mode inst_matches_binding_2(in, in, in, in, out) is semidet.
+:- pred inst_matches_binding_2 `with_type` inst_matches_pred.
+:- mode inst_matches_binding_2 `with_inst` inst_matches_pred.
inst_matches_binding_2(InstA, InstB, MaybeType, Info0, Info) :-
ThisExpansion = InstA - InstB,
@@ -1077,9 +1132,8 @@
Info0^expansions := Expansions1, Info)
).
-:- pred inst_matches_binding_3(inst, inst, maybe(type), inst_match_info,
- inst_match_info).
-:- mode inst_matches_binding_3(in, in, in, in, out) is semidet.
+:- pred inst_matches_binding_3 `with_type` inst_matches_pred.
+:- mode inst_matches_binding_3 `with_inst` inst_matches_pred.
% Note that `any' is *not* considered to match `any' unless
% Info ^ any_matches_any = yes or the type is not a solver type (and does not
Index: compiler/modecheck_call.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_call.m,v
retrieving revision 1.43
diff -u -r1.43 modecheck_call.m
--- compiler/modecheck_call.m 18 Mar 2003 02:43:39 -0000 1.43
+++ compiler/modecheck_call.m 28 Jul 2003 06:09:38 -0000
@@ -921,16 +921,16 @@
;
MaybeArgInst = yes(ArgInst),
(
- inst_matches_final(ArgInst, InstA, Type,
- ModuleInfo)
+ inst_matches_initial_no_implied_modes(ArgInst,
+ InstA, Type, ModuleInfo)
->
Arg_mf_A = yes
;
Arg_mf_A = no
),
(
- inst_matches_final(ArgInst, InstB, Type,
- ModuleInfo)
+ inst_matches_initial_no_implied_modes(ArgInst,
+ InstB, Type, ModuleInfo)
->
Arg_mf_B = yes
;
@@ -948,12 +948,18 @@
% or comparing with the arg inst doesn't help,
% then compare the two proc insts
%
- ( inst_matches_final(InstA, InstB, Type, ModuleInfo) ->
+ (
+ inst_matches_initial_no_implied_modes(InstA,
+ InstB, Type, ModuleInfo)
+ ->
A_mf_B = yes
;
A_mf_B = no
),
- ( inst_matches_final(InstB, InstA, Type, ModuleInfo) ->
+ (
+ inst_matches_initial_no_implied_modes(InstB,
+ InstA, Type, ModuleInfo)
+ ->
B_mf_A = yes
;
B_mf_A = no
Index: compiler/modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modes.m,v
retrieving revision 1.271
diff -u -r1.271 modes.m
--- compiler/modes.m 25 Jul 2003 06:30:05 -0000 1.271
+++ compiler/modes.m 28 Jul 2003 06:06:39 -0000
@@ -1893,21 +1893,8 @@
ModuleInfo, Subst0, Subst1)
;
NeedExactMatch = yes,
- inst_matches_final(VarInst, Inst, Type, ModuleInfo0),
- ModuleInfo = ModuleInfo0,
- Subst1 = Subst0
- % WARNING:
- % The code above (Subst1 = Subst0) assumes that there
- % are no inst variables in the mode of the callee.
- % Currently this will always true, since
- % `NeedExactMatch' will be `yes' only if we are
- % doing mode inference on the callee, and mode
- % inference currently will not infer polymorphic modes.
- % But that assumption might not always hold in future.
- % An alternative would be to call inst_matches_initial
- % here too, just to calculate the inst substitution.
- % But that would be less efficient, so (at least
- % for now) we don't do it.
+ inst_matches_initial_no_implied_modes(VarInst, Inst,
+ Type, ModuleInfo0, ModuleInfo, Subst0, Subst1)
)
->
Subst = Subst1,
@@ -2099,7 +2086,8 @@
% the initial inst specified in the pred's mode declaration,
% then it's not a call to an implied mode, it's an exact
% match with a genuine mode.
- inst_matches_final(VarInst1, InitialInst, VarType, ModuleInfo0)
+ inst_matches_initial_no_implied_modes(VarInst1, InitialInst,
+ VarType, ModuleInfo0)
->
Var = Var0,
ExtraGoals = ExtraGoals0,
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.203
diff -u -r1.203 Mmakefile
--- tests/hard_coded/Mmakefile 22 Jul 2003 07:04:26 -0000 1.203
+++ tests/hard_coded/Mmakefile 28 Jul 2003 06:32:22 -0000
@@ -25,6 +25,8 @@
constraint \
constraint_order \
construct_test \
+ contravariance_bug \
+ contravariance_poly \
curry \
curry2 \
cut_test \
Index: tests/hard_coded/contravariance_bug.exp
===================================================================
RCS file: tests/hard_coded/contravariance_bug.exp
diff -N tests/hard_coded/contravariance_bug.exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/contravariance_bug.exp 28 Jul 2003 02:07:27 -0000
@@ -0,0 +1 @@
+yes
Index: tests/hard_coded/contravariance_bug.m
===================================================================
RCS file: tests/hard_coded/contravariance_bug.m
diff -N tests/hard_coded/contravariance_bug.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/contravariance_bug.m 28 Jul 2003 03:25:51 -0000
@@ -0,0 +1,30 @@
+:- module contravariance_bug.
+:- interface.
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+:- import_module list, bool.
+
+main -->
+ ( { q(p) } ->
+ print("yes"), nl
+ ;
+ print("no"), nl
+ ).
+
+:- type intlist == list(int).
+:- inst nonempty ---> [ground|list].
+:- inst list ---> [ground|list] ; [].
+
+:- pred p(intlist, intlist).
+:- mode p((list -> nonempty), (free -> nonempty)) is semidet.
+
+p([X], [X]).
+p([X,Y|Zs], [Y,X|Zs]).
+
+:- pred q(pred(intlist, intlist)).
+:- mode q(pred((nonempty -> nonempty), (free -> list)) is semidet) is semidet.
+
+q(P) :- P([1], L), L \= [].
Index: tests/hard_coded/contravariance_poly.exp
===================================================================
RCS file: tests/hard_coded/contravariance_poly.exp
diff -N tests/hard_coded/contravariance_poly.exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/contravariance_poly.exp 28 Jul 2003 06:31:53 -0000
@@ -0,0 +1 @@
+yes
Index: tests/hard_coded/contravariance_poly.m
===================================================================
RCS file: tests/hard_coded/contravariance_poly.m
diff -N tests/hard_coded/contravariance_poly.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/contravariance_poly.m 28 Jul 2003 03:33:37 -0000
@@ -0,0 +1,33 @@
+:- module contravariance_poly.
+:- interface.
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+:- import_module list, bool.
+
+main -->
+ ( { q(p) } ->
+ print("yes"), nl
+ ;
+ print("no"), nl
+ ).
+
+:- inst nonempty(I) ---> [I | list(I)].
+:- inst list(I) ---> [I | list(I)] ; [].
+
+:- type intlist == list(int).
+:- inst bit == bound(0 ; 1).
+
+:- pred p(intlist, intlist).
+:- mode p((list(I) -> nonempty(I)), (free -> nonempty(I))) is semidet.
+
+p([X], [X]).
+p([X,Y|Zs], [Y,X|Zs]).
+
+:- pred q(pred(intlist, intlist)).
+:- mode q(pred((nonempty(bit) -> nonempty(bit)), (free -> list(bit)))
+ is semidet) is semidet.
+
+q(P) :- P([1], L), L \= [].
--
David Overton Uni of Melbourne +61 3 8344 1354
dmo at cs.mu.oz.au Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo Mobile Phone +61 4 0337 4393
--------------------------------------------------------------------------
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