[mercury-users] semidet vs unique updating

[Michael Day]

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

Right "in general" it will. What if the operation can be decomposed like
this:

get(Q0, T, Q) :-
	( if not_empty(Q0) then
		get_det(Q0, T, Q)
	else
		fail
	).

:- mode not_empty(ui) is semidet.
:- mode get_det(di, uo, uo) is det.

what possible modes can det have in this case? Is di,uo,uo still as
precise as it can get, even though it is clear that Q0 will not be
modified 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.

Right.

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

Is that basically a request to the compiler to make a copy automatically
to allow backtracking? What I'm looking for here is a way to tell the
compiler that making a copy is unnecessary, be it implicit or explicit.
Alternatively I could just provide not_empty and get_det and leave the
user to call them, but it seems like the compiler should be able to see
that it's not modified.

Michael

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