[mercury-users] Unique and mostly-unique modes

[Peter Hawkins]

Hi...

(I'm taking usual caveat about incomplete implementations of unique 
modes as read).

I have the following module, which produces three error messages, all of 
which I think are wrong:
:- module test.
:- interface.
:- import_module io.

:- pred main(io.state::di, io.state::uo) is det.

:- implementation.

:- import_module string.
:- import_module exception.

:- type moo ---> socket(string).

:- pred read(string::out, socket::mdi, socket::muo) is semidet.
read(S, socket(S), socket(S)).

:- pred write(string::in, socket::di, socket::uo) is det.
write(S, socket(_), socket(S)).

:- pred test_pred(socket::di, socket::uo, io.state::di, io.state::uo) is 
det.
test_pred(!Socket, !IO) :-
    (if read(S0, !Socket) then
        S = S0
     else
        throw("dead")
    ),
    write("foo", !Socket),
    print(S, !IO).

main(!IO) :-
    test_pred(socket("hello"), _, !IO).


Making Mercury/cs/test.c
test.m:015: In clause for `read(out, mdi, muo)':
test.m:015:   mode error: argument 3 had the wrong instantiatedness.
test.m:015:   Final instantiatedness of `HeadVar__3' was
test.m:015:   `unique(test.socket(ground))',
test.m:015:   expected final instantiatedness was `mostly_unique'.

Surely something unique qualifies as being mostly_unique as well?

test.m:018: In clause for `write(in, di, uo)':
test.m:018:   mode error: argument 3 did not get sufficiently instantiated.
test.m:018:   Final instantiatedness of `HeadVar__3' was
test.m:018:   `unique(test.socket(ground))',
test.m:018:   expected final instantiatedness was `unique'.

How is this incorrect? Surely unique(socket(ground)) <= unique.

test.m:027: In clause for `test_pred(di, uo, di, uo)':
test.m:027:   in argument 2 of call to predicate `test.write/3':
test.m:027:   mode error: variable `STATE_VARIABLE_Socket_3' has 
instantiatedness
test.m:027:   `mostly_unique',
test.m:027:   expected instantiatedness was `unique'.

Yes, but I've ensured that you can't backtrack across the call to read, 
so clearly the object is actually unique. Is there any way to convince 
the compiler of this?

What I'm actually trying to do here is to parse input from a socket 
using a DCG. You can backtrack over calls to 'read' since I'm keeping a 
buffer of everything that has been read. You can't backtrack over 
'write' since you can't unsend things you have already sent. I could 
make 'read' take a unique object, but this would mean you couldn't 
backtrack over it, and this would remove half the point of using a DCG 
since the grammar then has to be effectively LL(1). Any suggestions as 
to how I can deal with this?

=)
Peter
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------