[Subsumed] Towards a single code path for the "using" clause + small improvement of "using Type" for co/fixpoints

[herbelin]

The using clause was stored either in the Proof.t (for definitions generating proofs) or in the CInfo.t (for definitions with immediate proof, one for each component if a co/fixpoint). The PR makes a single choice by putting it instead in Info.t. In particular:

• this addresses pending XXX comments in vernacentries.ml
• this is a step towards having a single execution path for interactive and non-interactive Definition/Fixpoint (and eventually towards Unifying the syntax of Theorem, Definition, Fixpoint, etc. rfcs#42)

Note that we renounce to have one using per member of the CInfo.t on the assumption that the components of CInfo.t are mutually dependent, thus, having to share the same section variables (did I miss other uses of CInfo.t than for mutual definitions?).

In particular, we enhance a bit the effect of using Type on mutual definitions, taking all types together into account so that the dependencies are computed for the block of co/fixpoints as a whole.

@gares, @ejgallego: I believe it goes in the direction that you defended, I hope I'm not wrong.

• Added / updated test-suite.
• overlay: Adapt to Coq PR #18742: clause "using" moved from CInfo to Info LPCIC/coq-elpi#609

[herbelin]

I added another small using "Type" bug with Program Fixpoint: bodies were wrongly taken into account:

Require Import Program.
Section S.
Variables a : nat.
#[using="Type", warning="-non-recursive"]
Program Fixpoint b (n:nat) : nat := (fun _ => 0) a.
End S.
Print b.
(* "fun _ : nat => fix b (n : nat) : nat := 0" instead of "fix b (n : nat) : nat := 0" *)

[herbelin]

Actually, I'm confused about the meaning to give to Type. What Type is doing in the code, before the PR, is to collect all variables statically known at Gallina declaration time, so including the body when one is present, and, indeed, this is what is interesting to do in practice. So, maybe Type should be kept as it is, and the meaning of Type in the documentation be instead clarified.

Another curiosity in passing, which impacts the computation of using, is that some commands eventually contract beta-redexes present in the body or the type:

• Program Fixpoint beta-reduces both the bodies and types
• Program Definition beta-reduces the type but not the body
• Definition/Fixpoint/Theorem do not beta-reduce

[herbelin]

It is still unclear what would be the best semantics of Type of using. Enrico seems ok with an interpretation of Type as variables in the type of the declaration rather than as variables occurring at definition time, that is as the PR is currently. So, maybe can we proceed?

[ejgallego]

@herbelin , thanks for the PR, the patch looks good, but we already have using in the proof info field; I wonder if we can just remove that using parameter at all from Info.t / CInfo.t ?

[ejgallego]

Indeed, it seems to me that we have only two relevant cases:

• proof using
• init of interactive proofs

I've tried going deeper in #18890 , let me know what you think.

If we think the approach in that PR is better, I will finish the XXX (minor), I have to run now so I posted the current WIP code in that PR.

[herbelin]

@ejgallego:

I wonder if we can just remove that using parameter at all from Info.t / CInfo.t ?

I put using in Info.t as a way to factorize its presence in both ProgramDecl.t and Proof.t (corresponding to prg_using and Proof.using in your PR). The way it is done in #18890 is ok to me.

[herbelin]

Your PR is good. Once the design decision of rejecting or accepting using on non-interactive declarations is taken, I propose to merge your PR, which additionally should solve the issue of using on mutual fixpoints, once the XXX XXX are addressed there.

You can also add the tests I made to your PR.

[ejgallego]

@herbelin alternative PR seems ready, with the tests developed here; I think you can close this one then; thanks for all the help and careful comments!

[herbelin]

Replaced by #18890.