[m-rev.] for review: pre_quantification.m

[Zoltan Somogyi]

On Tue, 4 Jul 2017 00:03:40 +1000 (AEST), Julien Fischer <jfischer at opturion.com> wrote:
> > +% If lambda goals didn't exist, each zone zone would be identified
> 
> zone zone

Fixed.

> > +:- func from_int_for_enum(int) = uint is semidet.
> > +
> > +from_int_for_enum(I) = U :-
> > +    uint.from_int(I, U).
> 
> Are you sure about that?   It will fail for I < 0, even though the to_int/1
> method can return a value < 0 (e.g. to_int(max_uint)).  Since ints and uints
> must have the same size it's possible to convert between the two "without loss
> of information" (as required by enum.m) simply by casting in either direction.

You have put your finger on an interesting set of issues.

Yes, we could make the enum methods from_int and to_int both use casts
for uint's instance declaration, but since the from_int method is declared to be
a *semidet* function, and casting is det in both directions, we would need to
add an otherwise totally unnecessary semidet_succeed to it.

In fact, there should be no need for casts at all. The representation of enum types
in the Mercury runtime is as nonnegative integers allocated consecutively from zero
on up. These are effectively unsigned ints, so the two methods of the enum
type class should actually be to_uint and from_uint. The only reason they aren't
is that the uint type didn't exist when the enum typeclass was designed.

> (As an aisde, the documentation in enum.m doesn't state the conditions
> under which the from_int/1 method is expected to fail.)

It is there, implicit in the maths notation if you look hard enough,
but not in plain english.

I will post a proposed diff fixing this hole in the docs.

> The change looks fine otherwise.

OK. I think I will commit it after changing pre_quantification.m to use ints
instead of uints, and backing out the change to library/uint.m.

Zoltan.