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

[Julien Fischer]

Hi Zoltan,

On Mon, 3 Jul 2017, Zoltan Somogyi wrote:

> On Tue, 4 Jul 2017 00:03:40 +1000 (AEST), Julien Fischer <jfischer at opturion.com> wrote:
>
>>> +:- 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.

Actually, we don't have to add an unnecessary semidet_succeed, the
following will suffice.

     :- instance enum(uint) where [
         func(to_int/1) is uint.cast_to_int,
         func(from_int/1) is uint.cast_from_int
     ].

The determinism checker won't warn about method implementations where
the implementation has a tighter determinism than that declared for the
method in the tyepclass delcaration.  (It's why the existing enum
instance for the int type simply uses the identity function in both
directions.)

> 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.

foreign_enums are an exception to that since their representation (at
least in C grades) allows them use negative integers, non consecutively
allocated integers ...

Julien.