[mercury-users] Determinism question

[Peter Hawkins]

Hi...

In the following code, why can the determinism checker verify that the 
first mode of foo is semidet, but not the first mode of bar?

As far as I can see both satisfy the requirement of section 6.4 of the 
reference manual:
-----
If you just want to see if a nondeterministic goal is satisfiable or 
not, without needing to know what variable bindings it produces, then 
there is no problem - determinism analysis considers |nondet| and 
|multi| goals with no non-local output variables to be |semidet| and 
|det| respectively.
----

I get the following output when I attempt to compile the following code:
$ mmc --make --grade hlc.gc t
Making Mercury/int3s/t.int3
Making Mercury/cs/t.c
t.m:038: In `bar(in, in, out)':
t.m:038:   error: determinism declaration not satisfied.
t.m:038:   Declared `semidet', inferred `nondet'.
t.m:041:   call to `t.ndindex0(in, out, out)' can succeed more than once.
** Error making `Mercury/cs/t.c'.


:- module t.
:- interface.
:- import_module io.

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

:- implementation.
:- import_module list.
:- import_module int.
:- import_module string.

    % ndindex0
    % Like list.index0, but can be used non-deterministically as well
:- pred ndindex0(list(T), int, T).
:- mode ndindex0(in, in, out) is semidet.
:- mode ndindex0(in, out, out) is nondet.

:- pragma promise_pure(ndindex0/3).
ndindex0(Xs::in, N::in, Out::out) :-
    index0(Xs, N, Out).

ndindex0([X|Xs]::in, N::out, Out::out) :-
    (
        N = 0,
        Out = X
    ;
        ndindex0(Xs, N0, Out),
        N = N0 + 1
    ).

:- pred foo(list(int), int).
:- mode foo(in, in) is semidet.
:- mode foo(in, out) is nondet.
foo(List, Val) :-
    ndindex0(List, _, Val).

:- pred bar(list(int), int, int).
:- mode bar(in, in, out) is semidet.
:- mode bar(in, out, out) is nondet.
bar(List, Val, Val2) :-
    ndindex0(List, _, Val),
    Val2 = Val + 1.

main(!IO) :-
    if bar([1, 2, 3], 2, _)
    then print("yes\n", !IO)
    else print("no\n", !IO).

I've worked around the problem with some impure code, but I'd like to 
know what's going on here.

(Incidentally, would there be any objection to adding an additional mode 
to list.index* along the lines of the code above?)

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