[m-rev.] for review: fix singleton warnings for code with explicit quantification

[Julien Fischer]

On Sat, 10 Jun 2023, Zoltan Somogyi wrote:

> Fix singleton warnings for code with 'some [...]' goals.
> 
> The code in make_hlds_warn.m that is intended to generate singleton warnings
> hasn't ever been able to handle code containing 'some [...]' goals properly.
> The reason is that
> 
> - add_clause.m invokes make_hlds_warn.m only *after* it does quantification
>   on the body of the clause being added to the HLDS, but
> 
> - quantification has always replaced all lists of quantified variables
>   with the empty list.
> 
> This meant that
> 
> - we never could report code in which the only occurrence of a variable
>   was in a list of quantified variables, which is something we *should*
>   warn about, and
> 
> - we always did generate a singleton warning for code such as
>   "some [Val] map.search(Map, Key, Val)", which is something we *should not*
>   warn about.
> 
> This diff fixes this problem.
> 
> The main change is a mechanism that allows us to tell quantification.m
> to keep lists of quantified variables intact. However, since the rest
> of the compiler does not react well to these lists not being empty,
> this diff
> 
> - gets make_hlds_warn.m to report whether the clause body goal, in which
>   quantification.m was told to preserve any lists of quantified variables,
>   *actually contained* any nonempty lists of quantified variables, and
> 
> - if it did, then we invoke quantification.m again, this time telling it
>   to nuke all lists of quantified variables.
> 
> This nuking has to be done relatively rarely, because only a very small
> fraction of clauses contain any explicit quantification.
> 
> (An alternative design would be for make_hlds_warn.m to always nuke
> any noempty list of quantified variables it traversed. However, this would

s/noempty/nonempty/

> require *always* rebuilding the clause body goal, which would probably
> be slower on average.

You're missing a closing parenthesis there.

> The above is the main change in this diff. However, the change that is
> responsible for the bulk of the diff is the addition of a flag to
> exist_quant scopes to specify whether that scope was created by the user
> or by the compiler. This is needed because if make_hlds_warn.m sees code
> such as "some [Val] map.search(Map, Key, Val)", it definitely *should*
> generate a warning about Val being singleton (if it does not occur outside
> this code) if the "some [Val]" scope was put there by the compiler.

Do you mean was *not* put there by the compiler? That last sentence is
not particularly clear.

...

> diff --git a/compiler/quantification.m b/compiler/quantification.m
> index 7e41c73b9..a20c78994 100644
> --- a/compiler/quantification.m
> +++ b/compiler/quantification.m
> @@ -87,8 +87,34 @@
>  :- pred requantify_proc_general(nonlocals_to_recompute::in,
>      proc_info::in, proc_info::out) is det.
> 
> +:- type maybe_keep_quant
> +    --->    do_not_keep_quant       % Throw away lists of quantified vars.
> +    ;       keep_quant.             % Keep lists of quantified vars.

I would name that type "maybe_keep_quant_vars" and also append "_vars"
to each of its constructors.

> +
> +    % implicitly_quantify_clause_body_general_vs(NonLocalsToRecompute,
> +    %   KeepQuant, HeadVars, Warnings, !Goal,
> +    %   !VarSet, !VarTypes, !RttiVarMaps):
> +    % implicitly_quantify_clause_body_general_vs(NonLocalsToRecompute,
> +    %   HeadVars, Warnings, !Goal, !VarTable, !RttiVarMaps):
> +    %
> +    % Do the job described at the top-of-module comment. Find out the scope
> +    % of each variable, rename (actually, re-number) apart variables with
> +    % distinct scopes that happen to share the same name, and fill in
> +    % the nonlocals slots of all the goal_infos. Use either !VarSet and
> +    % !VarTypes, or !VarTable, to create renamed-apart copies of variables.
> +    %
> +    % If KeepQuant is keep_quant, the keep the variables listed in exist_quant
> +    % scopes, and in the quantified-vars slots of if-then-elses. If KeepQuant
> +    % is do_not_keep_quant, then replace both with the empty list of variables.
> +    % Since obviously the var_table version is invoked only by compiler phases
> +    % that run when var_tables are available, i.e. after typecheck, and
> +    % we (actually, make_hlds_warn.m) need the lists of quantified variables
> +    % only during the make-hlds phase of the compiler, the var_table version
> +    % does not take a maybe_keep_quant argument, but does its work
> +    % as if it was set to do_not_keep_quant.
> +    %
>  :- pred implicitly_quantify_clause_body_general_vs(nonlocals_to_recompute::in,
> -    list(prog_var)::in, list(quant_warning)::out,
> +    maybe_keep_quant::in, list(prog_var)::in, list(quant_warning)::out,
>      hlds_goal::in, hlds_goal::out, prog_varset::in, prog_varset::out,
>      vartypes::in, vartypes::out, rtti_varmaps::in, rtti_varmaps::out) is det.
>  :- pred implicitly_quantify_clause_body_general(nonlocals_to_recompute::in,

...

> @@ -333,10 +365,13 @@ quantify_goal(NonLocalsToRecompute, Goal0, Goal, !Info) :-
>          Goal = hlds_goal(!.GoalExpr, !.GoalInfo)
>      ).
> 
> -    % After this pass, explicit quantifiers are redundant, since all variables
> -    % which were explicitly quantified have been renamed apart. So we don't
> -    % keep them. We need to keep the structure, though, so that mode analysis
> -    % doesn't try to reorder through quantifiers. (Actually it would make sense

Missing closing parenthesis.

> +    % If the qi_keep_quant is do_not_keep_quant, then we are past the compiler

s/qi_keep_quant/qi_keep_quant field/

> +    % phases that needed explicit quantifiers, and the code of quantification.m
> +    % never needs it, since all variables which were explicitly quantified
> +    % would have been renamed apart during its first invocation. So we keep
> +    % lists of quantified variables only if qi_keep_quant is keep_quant.
> +    % We need to keep the structure, though, so that mode analysis doesn't
> +    % try to reorder through quantifiers. (Actually it would make sense
>      % to allow mode analysis to do that, but the reference manual says it
>      % doesn't, so we don't.) Thus we replace `scope(exist_quant(Vars), Goal0)'
>      % with an empty quantifier `scope(exist_quant([]), Goal)'.

That looks fine otherwise.

Julien.