[mercury-users] Determinism question

[Nicholas James Nethercote]

Hi,

I'm wondering about what happens when you have a conjunction of the form
(semidet, erroneous)... the compiler infers such a conjunction as `failure'.
For example:

%---------------------------------------------------------------------------%
:- module hmm.
%---------------------------------------------------------------------------%
:- interface.
:- import_module io.
:- pred main(state::di, state::uo) is det.
%---------------------------------------------------------------------------%
:- implementation.
:- import_module require.

main -->
    ( { interesting_case(3) } ->
        write_string("success\n")
    ;
        write_string("failure\n")
    ).

:- pred interesting_case(int::in).
interesting_case(X) :-
    semidet_pred(X),
    error("foo").

:- pred semidet_pred(int::in) is semidet.
semidet_pred(3).
%---------------------------------------------------------------------------%

The compiler gives the warning:

    hmm.m:014: Warning: the condition of this if-then-else cannot succeed.
    hmm.m:012: Warning: the negated goal cannot succeed.

The Mercury Reference Manual says this about `failure' and `erroneous':

    If all possible calls to a particular mode of a predicate or function fail
    without producing a solution, then that mode has a determinism of failure. 

    If all possible calls to a particular mode of a predicate or function lead
    to a runtime error, i.e. neither succeed nor fail, then that mode has a
    determinism of erroneous.

But then it has this summary diagram:

                    Maximum number of solutions
    Can fail?       0               1               > 1
    no              erroneous       det             multi
    yes             failure         semidet         nondet

The information is subtly different - if we are working from the table, the
procedure is clearly `failure';  if we are working from the sentences, the case
isn't really covered.  

So are the sentences just imprecisely worded, or is there some deeper
explanation?

And another thing - if interesting_case/1 above is inferred as failure, is
there a possibility that a call to it might be optimised away and replace with
`fail'?  Because that would change the behaviour of the above program.  Or does
the compiler check whether a `failure' procedure might throw an error before it
optimises it away like that?

Thanks.
--
Nick Nethercote
njn at cs.mu.oz.au
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------