[m-dev.] more correctness problems

[Peter Stuckey]

On 03/04/2006, at 9:51 AM, Ralph Becket wrote:

> Peter Stuckey, Monday,  3 April 2006:
>> But a better solution to this is
>> 	member(out(I), in(list(I))  I <= any
>> where it is clear that the any doesnt get instantiated,  To support 
>> this
>> we have to improve the mode analysis for mode variables.
>
> Can you explain that?  It isn't at all clear to me why the any wouldn't
> be further constrained (e.g., by unification).
>

The only constraint that touches an any variable which is guaranteed not
to further constraint it are det ones.

e.g.

	plus(fdint::in(any), fdint::in(any), fdint::out(any)) is det.

The most usual case of this is equality in the right modes.

	fdint::out(any) = fdint::in(any)

Consider

:- pred member(fdint::out(any), list(fdint)::in(list(any))) is multi.

member(X, [A|_) :- X = A.
member(X, [_|R]) :- member(X,R).

This is correct for notional mode

- pred member(fdint::out(any), list(fdint)::same(list(any))) is multi.
                                                                         
====

Actually now I see your question.  How do I know the definition is not

member(X, [Y,Z|_]) :- Y = Z, X = Y.

In HAL we solved this by having an EQ class and doing EQ and SOLVER 
class
annotation AFTER MODE ANALYSIS.

The first version of member does not use EQ, it just uses copying
The second version does (for Y = Z).

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------