[m-rev.] for review: better quad comparison predicates

[Peter Wang]

On Tue, 05 Mar 2024 04:26:42 +1100 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> Implement compare predicates using nested switches ...
> 

> diff --git a/compiler/unify_proc.m b/compiler/unify_proc.m
> index 262c6085f..9d2eca35a 100644
> --- a/compiler/unify_proc.m
> +++ b/compiler/unify_proc.m
...
> +    % This is possible because the typechecker can now handle the switches
> +    % that we generate. This ability depends on a natural property of these
> +    % switches: they are all on X or Y, both of which are argument variables
> +    % with declared types. This allows the compiler to effectively ignore
> +    % the unifications netween X or Y on the one hand the cons_ids in the
> +    % switch cases on the other hand, since (a) these implied unifications
> +    % should be type correct by construction, and (b) processing them
> +    % wouldn't tell the typechecker anything it does not already know.
> +    %

This comment is a bit garbled.

> -:- pred generate_compare_du_quad_switch_on_x(spec_pred_defn_info::in,
> -    uc_options::in, list(constructor_repn)::in, list(constructor_repn)::in,
> +    % generate_compare_du_quad_outer_switch_arms(SpecDefnInfo, UCOptions,
> +    %   CtorRepns, R, X, Y, !.ConsIdsLt, !.ConsIdsEqGt, !Cases, !Info):
> +    %
> +    % Generate one arm of the outer switch (on X), which is itself a complete
> +    % inner switch (on Y) for each constructor in CtorRepns. X and Y are
> +    % the terms being compared, and R is the result. !.ConsIdsLt are all
> +    % the cons_ids that should compare as less-than the first constructor
> +    % in CtorRepns, while !.ConsIdsEqGt are all the cons_ids that should
> +    % compare as greater then or requal to that same constructor.

equal

> -generate_compare_case(SpecDefnInfo, UCOptions, LinearOrQuad, CtorRepn,
> +generate_compare_case(SpecDefnInfo, UCOptions, ConsIdsMatch, CtorRepn,
>          R, X, Y, Case, !Info) :-
>      CtorRepn = ctor_repn(_Ordinal, MaybeExistConstraints, FunctorName,
>          ConsTag, ArgRepns, FunctorArity, _Ctxt),
> @@ -1712,13 +1836,23 @@ generate_compare_case(SpecDefnInfo, UCOptions, LinearOrQuad, CtorRepn,
>              umc_explicit, [], GoalUnifyX),
>          generate_return_equal(R, Context, EqualGoal),
>          (
> -            LinearOrQuad = linear,
> -            % The disjunct we are generating is executed only if the index
> -            % values of X and Y are the same, so if X is bound to a constant,
> -            % Y must also be bound to that same constant.
> +            ConsIdsMatch = cons_ids_known_to_match,
> +            % We get called with cons_ids_known_to_match in two cases.
> +            %
> +            % - If we are generating the body of the compare predicate
> +            %   using the linear method. With that method, we compare
> +            %   the two inpiut terms only if the type's index predicate 

input

> +            %   says that they have the same cons_id. This test is done
> +            %   at runtime.
> +            %
> +            % - If we are generating the body of the compare predicate
> +            %   using the quadratic method, but the type consists of
> +            %   only one data constructor. In that case, *all* values
> +            %   of the type have that data constructor. This test is done
> +            %   at compile time.
>              GoalList = [GoalUnifyX, EqualGoal]
>          ;
> -            LinearOrQuad = quad,
> +            ConsIdsMatch = cons_ids_not_known_to_match,
>              create_pure_atomic_complicated_unification(Y, RHS, Context,
>                  umc_explicit, [], GoalUnifyY),
>              GoalList = [GoalUnifyX, GoalUnifyY, EqualGoal]

Peter