Discharge on the fly in the kernel

[herbelin]

Since #14727, the kernel has all the information to support discharging of declarations at the time of declaration. This was experimented in #17888 and this PR is the internal kernel part of #17888.

It implements the following:

• kernel names include a section path in their name (encoded using MPdot)
• in safe_typing.ml: add all generalisations of a declaration at the time of the declaration rather than at the end of the section

No user-level changes if I'm not mistaken.

Depends on #18062.

TODO: double-check what really needs to be in Safe_typing.section_data

[ppedrot]

I think that this PR is already implementing too much, insofar as it's geared towards one specific instances of the extensions we discussed yesterday. Namely,

kernel names include a section path in their name (encoded using MPdot)

is already assuming we'll be accessing the various specializations at the same time. Since we don't have any equations on these yet I think it's a bad idea to include this in this PR. Especially if we have to revert it at some point (e.g. if we go for Georges' proposal for instance).

Can we just get

add all generalisations of a declaration at the time of the declaration rather than at the end of the section

to start with something consensual?

[herbelin]

I'm not fully sure I understand the difference that you are making. Do you mean that you'd prefer to have a kernel name (as it is now) pointing to the list of all generalizations rather than having one kernel name per generalization? Closing a section would then be dropping the more specific body in each list vs dropping the kernel name pointing to the more specific body?

[ppedrot]

I don't want the Constant type to be changed (for now), and instead of relying on the environment to get the various constant bodies, we should have one single list of bodies per constant.

[herbelin]

So, to confirm, you mean changing Environ.mind_key and Environ.add_mind from

type mind_key = mutual_inductive_body * link_info ref  
val add_mind : MutInd.t -> mutual_inductive_body -> env -> env

to

type mind_key = mutual_inductive_body list * link_info ref 
val add_mind : MutInd.t -> mutual_inductive_body list -> env -> env

and the same for constants?

[SkySkimmer]

I would put the discharged versions in the section data, not the environment if they're not meant to be accessed by most things

[herbelin]

I would put the discharged versions in the section data, not the environment if they're not meant to be accessed by most things

Note that, if, up to know, only the vm is interested in the discharge data, it can directly access the API of cooking.ml without needing a PR. From my point of view, what justifies the PR is that it eventually comes with a user access to the data, so this suggests that listing our wishes is the priority (as far as I'm concerned, my idea was the one given in the header of #17888.)

[ppedrot]

it can directly access the API of cooking.ml without needing a PR

This is expensive, since we need to recook the terms. If we do it once in a centralized place this is much simpler and faster.

[herbelin]

if we do it once in a centralized place this is much simpler and faster.

Sure, but if it is about putting this data in the section_data, it might just be enough to add a field there with the result of Discharge.cook_inductive applied to Section.segment_of_inductive, with minimal modification to Safe_typing.close_section.

So, before unravelling what I did, and maybe having to ununravel afterwards, I would prefer to have a better view of what model we want to eventually provide.

For instance, regarding the vm, is it something of the form lookup_fully_generalized_constant : Constant.t -> env -> constant_body that would be needed?

[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.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.