[mercury-users] inferred determinism

[Fergus Henderson]

On 26-Feb-2002, Michael Day <mikeday at bigpond.net.au> wrote:
> 
> The compiler infers a determinism of nondet for the predicate foo below,
> unless the call to `zero' in the first clause is replaced by the literal
> value 0. But it's an output argument, so why should it care?
> 
> :- pred foo(int, list(T)).
> :- mode foo(out, in) is det.
> 
> foo(zero, []).
> foo(N, [_|Xs]) :- foo(N0, Xs), N = N0+1.
> 
> :- func zero = int.
> zero = 0.

Switch detection will not look past function calls.
It only looks for unifications that occur before the
first function call or predicate call in the clause.
(One reason for this is that moving unifications across function
calls could change whether or not the program terminates;
e.g. consider the case where `zero' loops.)

In this example, the unification of the first argument
of foo/2 with `zero' involves a function call.
The unification of the second argument with `[]'
occurs after this, so it is not visible to switch detection.

If you instead write that clause as

	foo(N, []) :- N = zero.

then it should work fine.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------