[m-users.] Compiler cannot infer determinism det when exhaustively pattern matching on a constant?

[Julien Fischer]

Hi,

On Thu, 1 Aug 2024 at 03:56, Anders Lundstedt
<mercury-users at anderslundstedt.se> wrote:

> I try to define a predicate by exhaustive pattern matching on a
> constant. The compiler complains:
>
> “determinism declaration not satisfied. Declared `det', inferred `nondet'.”
>
> Why?
>
>
> Example code below, showing what fails (the predicate p3) and also
> showing a workaround (the predicate p2, using helper predicate p1):
>
> :- module test.
> :- interface.
> :- type t ---> c1; c2.
> :- pred p1(t::in, t::out) is det.
> :- pred p2(t::out) is det.
> :- pred p3(t::out) is det.
> :- implementation.
> :- func c = t.
> c = c1.
> % accepted by compiler
> p1(A, B) :- (A = c1, B = c2) ; (A = c2, B = c1).
> % accepted by compiler
> p2(A) :- p1(c, A).
> % compiler error
> p3(A) :- (c = c1, A = c2) ; (c = c2, A = c1).

According to the algorithm that the compiler uses to detect switches:

        A disjunction is a switch if each disjunct has near its start
a unification
        that tests the same bound variable against a different function symbol

By that criterion, p1 is a switch (and hence det) where A is the bound variable.
The disjunct in p3 is not a switch because each disjunct begins with a
conjunction.
If you rewrite p3 to be:

     p3(A) :- (c = c1, A = c2 ; c = c2, A = c1)

it will also not be detected as a switch, since the beginning of each
disjunct is
now a (constant) function call.  However,

    p3(A) :-  C = c, (C = c1, A = c2 ; C = c2, A = c1).

is a switch.  Could we modify the switch detection rules to treat some
of the other variants
of p3 as switches?  Quite possibly, but that would be at the cost of
making the switch detection
algorithm more complicated and hence more difficult for users to
comprehend.  The current
algorithm, while limited, is quite comprehensible.

Julien.