[m-rev.] for review: improve checking of `any' in negated context

[David Overton]

On Wed, May 28, 2003 at 11:37:43PM +1000, David Overton wrote:
> On Wed, May 28, 2003 at 02:19:25PM +1000, Fergus Henderson wrote:
> > I'm still struggling to convince myself that this change is safe,
> > i.e. that it doesn't allow any cases which ought to be mode errors.
> 
> Actually, I'm not convinced now either.  I'll need to think about it a
> bit more.

The change change wasn't safe.  It allowed the test case below which
should be a mode error.  Here is the interdiff for the fix.


diff -u compiler/inst_match.m compiler/inst_match.m
--- compiler/inst_match.m	28 May 2003 03:30:46 -0000
+++ compiler/inst_match.m	29 May 2003 00:00:36 -0000
@@ -155,6 +155,13 @@
 	%	 that `any' does not match itself.  It is used to check
 	%	 whether variables get bound in negated contexts.
 
+:- pred inst_matches_binding_allow_any_any(inst, inst, type, module_info).
+:- mode inst_matches_binding_allow_any_any(in, in, in, in) is semidet.
+
+	% inst_matches_binding_allow_any_any is the same as
+	% inst_matches_binding except that it also allows `any' to
+	% match `any'.
+
 %-----------------------------------------------------------------------------%
 
 	% pred_inst_matches(PredInstA, PredInstB, ModuleInfo)
@@ -333,16 +340,26 @@
 
 :- type expansions == set(pair(inst)).
 
+	% The uniqueness_comparison type is used by the predicate
+	% compare_uniqueness to determine what order should be used for
+	% comparing two uniqueness annotations.
+
 :- type uniqueness_comparison
 	--->	match
+			% We are doing a "matches" comparison, e.g. at a
+			% predicate call or the end of a procedure body.
 	;	instantiated.
+			% We are comparing two insts for how "instantiated" they
+			% are.  The uniqueness order here should be the reverse
+			% of the order used for matching.
 
 :- type inst_match_info
 	--->	inst_match_info(
 			module_info	:: module_info,
 			expansions	:: expansions,
 			maybe_sub	:: maybe(inst_var_sub),
-			uniqueness_comparison	:: uniqueness_comparison
+			uniqueness_comparison	:: uniqueness_comparison,
+			any_matches_any	:: bool
 		).
 
 :- func sub(inst_match_info) = inst_var_sub is semidet.
@@ -357,8 +374,8 @@
 
 :- func init_inst_match_info(module_info) = inst_match_info.
 
-init_inst_match_info(ModuleInfo) = inst_match_info(ModuleInfo, Exp, no, match)
-		:-
+init_inst_match_info(ModuleInfo) =
+		inst_match_info(ModuleInfo, Exp, no, match, yes) :-
 	set__init(Exp).
 
 :- pred inst_matches_initial_2(inst, inst, maybe(type), 
@@ -416,7 +433,7 @@
 	% occur in `Expansions'.
 
 inst_matches_initial_4(any(UniqA), any(UniqB), _, I, I) :-
-	I ^ uniqueness_comparison = match,
+	I ^ any_matches_any = yes,
 	compare_uniqueness(I ^ uniqueness_comparison, UniqA, UniqB).
 inst_matches_initial_4(any(_), free, _, I, I).
 inst_matches_initial_4(free, any(_), _, I, I).
@@ -1016,11 +1033,17 @@
 	).
 
 inst_is_at_least_as_instantiated(InstA, InstB, Type, ModuleInfo) :-
-	Info = init_inst_match_info(ModuleInfo) ^ 
-			uniqueness_comparison := instantiated,
+	Info = (init_inst_match_info(ModuleInfo)
+			^ uniqueness_comparison := instantiated)
+			^ any_matches_any := no,
 	inst_matches_initial_2(InstA, InstB, yes(Type), Info, _).
 
 inst_matches_binding(InstA, InstB, Type, ModuleInfo) :-
+	Info0 = init_inst_match_info(ModuleInfo)
+		^ any_matches_any := no,
+	inst_matches_binding_2(InstA, InstB, yes(Type), Info0, _).
+
+inst_matches_binding_allow_any_any(InstA, InstB, Type, ModuleInfo) :-
 	Info0 = init_inst_match_info(ModuleInfo),
 	inst_matches_binding_2(InstA, InstB, yes(Type), Info0, _).
 
@@ -1046,8 +1069,11 @@
 		inst_match_info).
 :- mode inst_matches_binding_3(in, in, in, in, out) is semidet.
 
-% Note that `any' is *not* considered to match `any'.
+% Note that `any' is *not* considered to match `any' unless 
+% Info ^ any_matches_any = yes.
 inst_matches_binding_3(free, free, _, I, I).
+inst_matches_binding_3(any(_), any(_), _, I, I) :-
+	I ^ any_matches_any = yes.
 inst_matches_binding_3(bound(_UniqA, ListA), bound(_UniqB, ListB), MaybeType,
 		Info0, Info) :-
 	bound_inst_list_matches_binding(ListA, ListB, MaybeType, Info0, Info).
diff -u compiler/modes.m compiler/modes.m
--- compiler/modes.m	28 May 2003 03:30:46 -0000
+++ compiler/modes.m	29 May 2003 00:00:36 -0000
@@ -2043,7 +2043,9 @@
 				% with a free variable.
 				MaybeUInst = yes(UInst),
 				inst_is_at_least_as_instantiated(Inst, UInst,
-					Type, ModuleInfo)
+					Type, ModuleInfo),
+				inst_matches_binding_allow_any_any(Inst,
+					Inst0, Type, ModuleInfo)
 			)
 		->
 			set__singleton_set(WaitingVars, Var0),
only in patch2:
unchanged:
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/bind_in_negated.m	29 May 2003 00:00:37 -0000
@@ -0,0 +1,20 @@
+:- module bind_in_negated.
+:- interface.
+
+:- type foo ---> f(int, int).
+
+:- pred p(foo, foo, foo).
+:- mode p(bound(f(free, ground)) >> ground,
+	  bound(f(ground, free)) >> ground,
+	  out) is det.
+
+:- implementation.
+
+p(A, B, C) :-
+	( A = B ->
+		C = A
+	;
+		C = f(1, 1),
+		A = f(1, _),
+		B = f(_, 1)
+	).
only in patch2:
unchanged:
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/bind_in_negated.err_exp	29 May 2003 00:00:37 -0000
@@ -0,0 +1,6 @@
+bind_in_negated.m:014: In clause for `p((bound(f(free, ground)) -> ground), (bound(f(ground, free)) -> ground), out)':
+bind_in_negated.m:014:   scope error: attempt to bind a non-local variable
+bind_in_negated.m:014:   inside the condition of an if-then-else.
+bind_in_negated.m:014:   Variable `A' has instantiatedness `bound(bind_in_negated.f(free, ground))',
+bind_in_negated.m:014:   expected instantiatedness was `bound(bind_in_negated.f(ground, ground))'.
+For more information, try recompiling with `-E'.
only in patch2:
unchanged:
--- tests/invalid/Mmakefile	19 May 2003 14:24:35 -0000	1.136
+++ tests/invalid/Mmakefile	29 May 2003 00:00:37 -0000
@@ -33,6 +33,7 @@
 	any_mode \
 	assert_in_interface \
 	bigtest \
+	bind_in_negated \
 	bind_var_errors \
 	builtin_int \
 	builtin_proc \

-- 
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
--------------------------------------------------------------------------