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

[Julien Fischer]

Hi Zoltan,

On Fri, 30 Jun 2017, Zoltan Somogyi wrote:

> For review by anyone.
>
> A change like this will need a small addition to the reference manual
> and an entry in NEWS, but I would prefer to wait with that until we have
> used this new capability ourselves for a while.


> Implicitly rename apart vars occurring only in trace goals.

...

> diff --git a/compiler/pre_quantification.m b/compiler/pre_quantification.m
> index e69de29..aaf22c6 100644
> --- a/compiler/pre_quantification.m
> +++ b/compiler/pre_quantification.m


> +%-----------------------------------------------------------------------------%
> +%
> +% The pre-quantification algorithm is based on dividing the clause body
> +% into one or more zones, each identified by a non-negative integer.
> +% The zones are based on viewing the clause body as a tree:
> +%
> +% - with each goal being a node,
> +% - atomic goals being leaf nodes, and
> +% - each compound goal having a subtree for each subgoal.
> +%
> +% If lambda goals didn't exist, each zone zone would be identified

zone zone

...

> diff --git a/library/uint.m b/library/uint.m
> index dc3f8d9..014abdb 100644
> --- a/library/uint.m
> +++ b/library/uint.m
> @@ -18,10 +18,15 @@
>  :- module uint.
>  :- interface.
> 
> +:- import_module enum.
>  :- import_module pretty_printer.
>
>  %---------------------------------------------------------------------------%
> 
> +:- instance enum(uint).
> +
> +%---------------------------------------------------------------------------%
> +
>      % Convert an int to a uint.
>      % Fails if the int is less than zero.
>      %
> @@ -194,6 +199,13 @@
>
>  %---------------------------------------------------------------------------%
> 
> +:- instance enum(uint) where [
> +    func(to_int/1) is uint.cast_to_int,
> +    func(from_int/1) is uint.from_int_for_enum
> +].
> +
> +%---------------------------------------------------------------------------%
> +
>  :- pragma foreign_proc("C",
>      from_int(I::in, U::out),
>      [will_not_call_mercury, promise_pure, thread_safe, will_not_modify_trail],
> @@ -222,10 +234,16 @@
>      SUCCESS_INDICATOR = (I < 0) ? false : true;
>  ").
> 
> +:- 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.

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

The change looks fine otherwise.

Julien.