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

[David Overton]

On Wed, May 28, 2003 at 11:09:34AM +1000, David Overton wrote:
> 
> Estimated hours taken: 5
> Branches: main
> 
> Allow more precise (i.e. less conservative) mode checking in the case that an
> `any' inst occurs in a negated context.  Normally we must disallow this
> because we do not know whether the inst has become more instantiated over the
> negated goal.  However, if the inst has simply been unified with `free' then
> we know that it cannot have become more instantiated.  This change checks
> for, and allows, that case.

I was a bit hasty with this.  With the inst_is_at_least_as_instantiated
partial order with need to disallow the (any, any) case since it is not
definite that the first inst is at least as instantiated as the second.

Here is an interdiff.


David

diff -u compiler/inst_match.m compiler/inst_match.m
--- compiler/inst_match.m	28 May 2003 01:04:17 -0000
+++ compiler/inst_match.m	28 May 2003 02:13:22 -0000
@@ -127,10 +127,8 @@
 	% 	succeeds iff InstA is at least as instantiated as InstB.  This
 	% 	defines a partial order which is the same as
 	% 	inst_matches_initial except that uniqueness comparisons are
-	% 	reversed.  This gives us the partial order of which
-	% 	abstractly_unify_inst(dead, ...) is the greatest lower bound.
-	% 	It describes the allowable changes in the inst of a variable
-	% 	over the forward execution of a goal.
+	% 	reversed and we don't allow
+	% 	inst_is_at_least_as_instantiated(any, any).  
 
 :- pred inst_is_at_least_as_instantiated(inst, inst, type, module_info).
 :- mode inst_is_at_least_as_instantiated(in, in, in, in) is semidet.
@@ -418,6 +416,7 @@
 	% occur in `Expansions'.
 
 inst_matches_initial_4(any(UniqA), any(UniqB), _, I, I) :-
+	I ^ uniqueness_comparison = match,
 	compare_uniqueness(I ^ uniqueness_comparison, UniqA, UniqB).
 inst_matches_initial_4(any(_), free, _, I, I).
 inst_matches_initial_4(free, any(_), _, I, I).
diff -u compiler/modes.m compiler/modes.m
--- compiler/modes.m	28 May 2003 01:04:17 -0000
+++ compiler/modes.m	28 May 2003 02:13:22 -0000
@@ -2033,7 +2033,7 @@
 			mode_info_var_is_locked(ModeInfo1, Var0, Reason0),
 			\+ (
 				% ...unless the goal is a unification and the
-				% var was unified with something less
+				% var was unified with something no more
 				% instantiated than itself.
 				% This allows for the case of `any = free', for
 				% example. The call to
@@ -2043,8 +2043,6 @@
 				% with a free variable.
 				MaybeUInst = yes(UInst),
 				inst_is_at_least_as_instantiated(Inst, UInst,
-					Type, ModuleInfo),
-				\+ inst_is_at_least_as_instantiated(UInst, Inst,
 					Type, ModuleInfo)
 			)
 		->

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