Stream: Coq devs & plugin devs

Topic: Inlining data in Δ-resolver

Hugo Herbelin (Dec 21 2021 at 09:55):

I realize that the Δ-resolver of the module system includes more than the Δ-equalities coming from aliasing in the module system: it contains also the inlining levels, both the abstract ones and the effective ones (details below).

I'd be tempted to clarify things a lot by splitting the three roles:

• the Δ-resolver with only Δ-equalities (current mod_delta field)
• the abstract inliner stored in the module type that contains them (say in a new field created for that purpose)
• the effective inliner living only for the time of the substitution used at module application (thus not stored in the environment, to the exception of the substitutions accumulated on opaque terms)

I know that @Pierre-Marie Pédrot has ongoing work on the module system. Would that be compatible?

Details on the current uses of the mod_delta data:

• Proper Δ-equalities coming from Module M := P and Module M. ... Include P. ... End M. are represented as M↦Equiv P, or M.c↦Equiv P.c
• Abstract inlining hints coming from Module Type T. ... Parameter Inline(50) c : t. ... End T. are represented as T.c↦Inline (50,None)
• Effective inlining coming from M <+ F [inline at level 60], when F is defined say by Module F (X:T) ...with T as above and Module M. Definition c := u. End M., are represented as X.c↦ Inline (60,Some u)

Pierre-Marie Pédrot (Dec 26 2021 at 17:08):

My main goal is to get rid of the dual name representation for kernel objects, I think this is somewhat orthogonal to your proposals.

Pierre-Marie Pédrot (Dec 26 2021 at 17:09):

i.e. instead of claiming that two names are aliased and never checking this in the environment, we only have one name and a reified variant of constant_body that states that a definition / inductive type aliases to another one.

Hugo Herbelin (Dec 27 2021 at 10:30):

You mean adding an extra case Alias to Def, Undef etc. in constant_body (and an Alias case for inductive too)? and recomputing the "canonical" name from it?

Hugo Herbelin (Dec 27 2021 at 10:32):

Or having an extra Alias field in addition to the Def, Undef, ... fields (which would tell which exact form of user names are used in the dependencies in the body)?

Hugo Herbelin (Dec 27 2021 at 10:37):

Or having all internal references in the body and type of a constant referring to the canonical name of other names and using the nametab to revert the canonical names into user-friendly names (but that seems a bit risky compatibility-wise)?

Pierre-Marie Pédrot (Dec 27 2021 at 11:10):

Rather the second option, for backwards compatibility.

Hugo Herbelin (Dec 29 2021 at 08:37):

Pierre-Marie Pédrot said:

My main goal is to get rid of the dual name representation for kernel objects, I think this is somewhat orthogonal to your proposals.

But then, would you still need to maintain Δ-equations in the current mod_delta? Afaiu, their purpose is to quickly build dual names + saturating upwards the constants to inline. With an Alias, there would be no more need to pre-saturate upwards the inliner, and without dual names, the need for mod_delta disappears at all. As for the other components of mod_delta, the inlining levels and inlining map, with what I explored, they would go elsewhere: levels are attached to module types (or even simply collected on demand, rather than cached) and inlining maps stored in the module substitutions.

Last updated: May 28 2023 at 16:30 UTC