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:
mod_delta
field)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:
Module M := P
and Module M. ... Include P. ... End M.
are represented as M
↦Equiv P
, or M.c
↦Equiv P.c
Module Type T. ... Parameter Inline(50) c : t. ... End T.
are represented as T.c
↦Inline (50,None)
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)
My main goal is to get rid of the dual name representation for kernel objects, I think this is somewhat orthogonal to your proposals.
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.
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?
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)?
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)?
Rather the second option, for backwards compatibility.
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: Nov 29 2023 at 19:01 UTC