[mercury-users] Unique mode problem: what's the difference?

[Ralph Becket]

Hi,

I have a bug in some code using mostly unique modes (it's a term
unifier.)  I'm not entirely sure what is going wrong...

The procedure leading me to grief has the following signature:

:- pred occurs(var(S), list(term(S)), store(S), store(S)).
:- mode occurs(in, in, mdi, muo) is semidet.

(don't worry about the first two arguments).  Now, If I write the following
elsewhere in my program

:- pred unify(term(S), term_type(S), term(S), term_type(S), store(S),
store(S)).
:- mode unify(in, in, in, in, mdi, muo) is semidet.

...

unify(T1, free, _T2, functor(Name2, Arity2, Args2)) -->
        \+ occurs(T1, Args2),
        tr_store__set_mutvar(T1, functor(Name2, Arity2, Args2)).

I get the following error report (shown using -E):

logic.m:078: In clause for `unify(in, in, in, in, mdi, muo)':
logic.m:078:   mode error in conjunction. The next 3 error messages
logic.m:078:   indicate possible causes of this error.
logic.m:077: In clause for `unify(in, in, in, in, mdi, muo)':
logic.m:077:   in argument 3 of call to predicate `logic:occurs/4':
logic.m:077:   unique-mode error: the called procedure would clobber
logic.m:077:   its argument, but variable `DCG_0' is still live.
logic.m:078: In clause for `unify(in, in, in, in, mdi, muo)':
logic.m:078:   in argument 3 of call to predicate `tr_store:set_mutvar/4':
logic.m:078:   unique-mode error: the called procedure would clobber
logic.m:078:   its argument, but variable `DCG_0' is still live.
logic.m:076: In clause for `unify(in, in, in, in, mdi, muo)':
logic.m:076:   in argument 6 of clause head:
logic.m:076:   mode error in unification of `HeadVar__6' and `DCG_2'.
logic.m:076:   Variable `HeadVar__6' has instantiatedness `free',
logic.m:076:   variable `DCG_2' has instantiatedness `free'.

If I rewrite the offending clause to be

unify(T1, free, _T2, functor(Name2, Arity2, Args2)) -->
        ( if occurs(T1, Args) then
                { fail }
          else
                tr_store__set_mutvar(T1, functor(Name2, Arity2, Args2))
        ).

then the error message goes away.  However, looking closely at the language
definition, we find that

(1) negation has the following semantics

\+ P  <=>  ( if P then fail else true )

(2) and the DCG transformation works as follows

unify(T1, free, _T2, functor(Name2, Arity2, Args2), DCG0, DCG) -->
        ( if (\+ occurs(T1, Args, DCG0, DCG_Dummy), DCG1 = DCG0) then
                fail, DCG = DCG1
          else
                tr_store__set_mutvar(T1,
functor(Name2,Arity2,Args2),DCG0,DCG)
        ).

At first blush it seems DCG0 is being destroyed in the condition of the if
by
the call to occurs/4 - but that occurs in a negated context, so surely it
isn't destroyed?  I'm much confused and if anyone could explain to me where
my reasoning takes a jump to the left I'd be v. grateful.

Cheers,

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