[mercury-users] semidet vs unique updating

[Mark Brown]

On 19-Oct-2001, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> Instead of using `mdi' and `muo',
> I think what is wanted is something like this:
> 
> 	:- mode cdi == mostly_unique >> dead.
> 
>  	:- pred queue__get(queue(T)::cdi, T::uo, queue(T)::uo) is semidet.
> 
> The `mostly_unique' initial inst means that this is the only reference
> for forward execution, but there might be additional references
> on backtracking.  The `dead' final inst means that after the call
> succeeds, there are no more references at all.
> 
> Unfortunately this is not quite enough, because in general you'd want to
> use `cdi, uo' pairs, as in  and the problem would be that the current
> mode checking algorithm would complain that the uo mode arguments have
> inst `mostly_unique' rather than `unique' at the end of the call.
> 
> However, I think using `cdi == mostly_unique >> dead' and `uo' is
> the right way to express what is wanted; I suspect that if the mode
> checking algorithm was a bit more clever, it could keep track of which
> mostly_unique objects were guaranteed to become unique at the end of
> the call and thus be able to correctly handle cases like the
> `cdi, uo, uo' mode of queue__get above.
> 

What precisely is the condition that would guarantee uniqueness of a
mostly unique object?  If this condition really is satisfied, then you
could use unsafe_promise_unique to make up for incompleteness in the
mode checking algorithm, right?  That way you wouldn't need to wait for
the algorithm to become more clever.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------