[m-rev.] for review: constrained polymorphic insts

[David Overton]

On Thu, Feb 21, 2002 at 08:48:34PM +1100, Fergus Henderson wrote:
> The main problem I can see is that it doesn't handle uniqueness correctly.
> 
> ...
> > inst_match.m:
> > @@ -1036,6 +1067,8 @@
> >  inst_is_clobbered(_, bound(mostly_clobbered, _)).
> >  inst_is_clobbered(_, inst_var(_)) :-
> >          error("internal error: uninstantiated inst parameter").
> > +inst_is_clobbered(ModuleInfo, constrained_inst_var(_, Inst)) :-
> > +	inst_is_clobbered(ModuleInfo, Inst).
> 
> This is not safe.
> 
> We know that constrained_inst_var(V, Inst) matches_final Inst.
> But this does not imply that constrained_inst_var(V, Inst) is
> clobbered iff Inst is clobbered.
> 
> In particular, V might be `unique', which matches_final `clobbered',
> but V is not clobbered.
> 
> inst_is_clobbered is used by get_var_lives,
> which is used to initialize the live_vars set in the mode_info.
> An argument whose final inst is `V =< clobbered' will get
> excluded from the live_vars set, even though it might still
> be referred to be the caller.
> 
> E.g. consider this example:
> 
> 	:- mode q(di, uo).
> 	q(X, Z) :-
> 		alias(X, Y),
> 		destroy(X),
> 		Z = Y.
> 
> 	:- mode alias(I =< clobbered) >> (I =< clobbered),
> 			free >> (I =< clobbered)).
> 	alias(A, A).
> 	% i.e. alias(HeadVar__1, HeadVar__2) :- HeadVar__1 = A, HeadVar__2 = A.
> 
> 	:- mode destroy(di).
> 	:- pragma c_code(destroy(X::di), "...").
> 
> In the call to `alias', X has initial inst `unique', which matches_final
> `clobbered', so the inst parameter `I' will get bound to `unique'.
> 
> But in the body of `alias', the unification of
> `HeadVar__2' with `A' will be permitted, because
> both variables will be considered dead at that point.
> 
> So this example is mode-correct, but leads to the `uo' mode argument
> of q/2 being clobbered.

I think it _is_ safe.  The conditions that hold for 'I =< Inst' are:

	abstractly_unify_inst(dead, I, Inst, fake_unify) = I,
AND
	inst_matches_final(I, Inst).
	
In the example you give above, the substitution for I is determined by
abstractly unifying `unique' and `clobbered' to get `clobbered'.
Attempting to compile this example gives the following error message:

	clob.m:019: In clause for `q(di, uo)':
	clob.m:019:   in argument 1 of call to predicate `clob:alias/2':
	clob.m:019:   unique-mode error: the called procedure would clobber
	clob.m:019:   its argument, but variable `X' is still live.

This is not really explained clearly in the reference manual since it
would require adding a lot more detail about the rest of the mode system
than is currently present in that document.

Ah, I've just notice the documentation I've added for the `inst' type is
incorrect.  I will ammend that.



David
-- 
David Overton      Computer Science and Software Engineering
PhD Student        The University of Melbourne   +61 3 8344 9159
Research Fellow    Monash University (Clayton)   +61 3 9905 5779
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------