[mercury-users] semidet vs unique updating

[Mark Brown]

On 15-Oct-2001, Michael Day <mikeday at bigpond.net.au> wrote:
> 
> Hi,
> 
> Consider queue__get operating on a unique queue. The normal mode of get
> looks like this:
> 
> :- pred queue__get(queue(T), T, queue(T)).
> :- mode queue__get(in, out, out) is semidet.
> 
> I can't see how to maintain that interface and preserve uniqueness.
> 
> :- mode queue__get(di, uo, uo) is semidet.
> 
> This won't work, as once queue__get has been called its first argument is
> dead, and it can't fail and backtrack.
> 
> :- mode queue__get(ui, uo, uo) is semidet.
> 
> This will work (assuming we fudge around compiler ui mode inadequacy) but
> it doesn't say what we mean; the predicate can succeed and the first
> argument will still be around, requiring the predicate to make a copy of
> the queue to ensure uniqueness (or lie to the compiler and face its
> terrible vengeance).

Presumably your intended semantics is that the queue should be unchanged
if the call fails.  A problem with this is that in general the call
may perform some of the destructive update before the failure occurs,
and these updates will need to be somehow undone if the implementation
is to be sound.

> 
> Can a mode be constructed like this:
> 
> 	unique >> dead on success, unique on failure ?
> 

No; this doesn't make sense.  The initial inst (to the left of the '>>')
describes the instantiatedness at the time of calling the predicate, and
the final inst (to the right of the '>>') describes it at the time of
successful exit.  When a predicate fails, backtracking will have brought
us to a point equivalent to the point of call -- that is, the variables
should have the same bindings as they had at the point of call.  In
other words, at failure the "initial" inst applies and the "final" inst
is irrelevant.  The RHS of '>>' cannot say anything about the inst at
failure.

This is analogous with Byrd's box model, where the 'call' and 'fail'
ports are on the left (initial) side of the box, and the 'exit' and
'redo' ports are on the right (final) side.

You should take a look at mostly_unique and mostly_dead insts, which
are described in the "Backtrackable destructive update" section of the
reference manual.  These may be closer to what you want.

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