Stream: Coq devs & plugin devs

Topic: Inlining data in Δ-resolver


view this post on Zulip 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:

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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)?

view this post on Zulip 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)?

view this post on Zulip Pierre-Marie Pédrot (Dec 27 2021 at 11:10):

Rather the second option, for backwards compatibility.

view this post on Zulip 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: Feb 05 2023 at 20:03 UTC