Fix #16288: wrongly self-referencing extraction of primitive projections in functors

[herbelin]

Fixes #16288 (usual problem of imperative tables not being updated in functors).

• Added / updated test-suite.
• Added changelog.

[herbelin]

@coqbot run full ci

[herbelin]

The failure in itauto is because the PR now extracts the constant form of a primitive projection only if the Coq code refers to it. Previously, a projection in the primitive form was elaborated in the projection in constant form, so, even if the Coq code referred only to the primitive form (Proj), the constant form (Const) was inferred detected as used and therefore extracted. Example:

Set Primitive Projections.
Module Import A.
Record t := {a:bool;b:bool}.
End A.
Definition c x := x.(a).
Require Import Extraction.
Recursive Extraction c.

• before:

  type bool = | True | False
  module A = struct type t = { a : bool; b : bool } (** val a : t -> bool **) let a t0 = t0.a end
  (** val c : A.t -> bool **) let c x = x.A.a

• after:

  type bool = | True | False
  module A = struct type t = { a : bool; b : bool } end
  (** val c : A.t -> bool **) let c x = x.A.a

@coq/extraction-maintainers: that would probably not be too much a problem to say that when a projection in primitive form is used, we effectively extract the projection in constant form (even if strictly speaking not needed). In case you have an opinion, would I implement this for optimal compatibility, or do you think we can as well renounce to it (then, third-party developments mixing extracted Coq code with private OCaml code, such as itauto, will have to use in OCaml the x.a notation rather than the applicative notation a x)?

[SkySkimmer]

I think the new behaviour is correct, it means that if using the constant form is desired then the user must say Extraction a instead of getting t by side effect extracting something that does not use it.

[herbelin]

I should also have said that the new behavior creates a difference between "primitive" and non "primitive" projections, which maybe is weakening the flexibility in using or not the "Primitive Projections" flag.

So, maybe, the extraction of the constant form should be removed also in the non primitive case, on the basis that in the extracted OCaml code of non primitive projections, only the dot notation is used too (except in a functor, where the same limitation as in the current report applies: the table telling that a constant is a (non primitive) projections is not active in a functor, so a non primitive projection is printed applicatively in a functor).

[herbelin]

After more digging, I could summarize the situation in issue #17337. In particular, prior to this PR, there is a difference of behavior wrt inlining between being at toplevel (where inlined functions are pruned) or in a module (where inlined functions, especially projections, are not pruned). I made #17341 to address this and this now shows the itauto failure even without this PR. In particular, I'm now leaning towards changing itauto.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[herbelin]

Rerunning CI, since it is a long time ago

@coqbot run full ci

[herbelin]

This is an old PR looking for an assigne. @ppedrot, would you have some time by chance?

[ppedrot]

This is a bit outside of my expertise area... There are weird spec considerations as well. I'll see if I can grok this.

[ppedrot]

I'm a bit puzzled about why you simply don't write the miniML matching directly instead of getting it by the composition of fake_match_projection + extract_term, but I guess it's a bit more uniform this way.

[ppedrot]

Merging soon if nobody complains.

[herbelin]

Thanks!

[ppedrot]

@coqbot merge now