Hi! I would welcome some help to refactor the following hack: https://github.com/coq/coq/blob/master/vernac/declaremods.ml#L970
For a clean parsing/execution separation, I need module declaration primitives to return data (not just unit
). Having these different codepaths makes it inconvenient.
Not so sure this spec is sufficient to give you a hand. It would be better if you wrote the signatures and let others fill in, no?
Well, I guess that's more or less doing the work :)
Help was on removing this hack and code duplication, not on the parsing separation.
It seems pretty clear there's an impedance mismatch somewhere with these list to options conversion, and calling different functions when the list contains several elements, doesn't it?
There's nothing I'm really missing to return the values I need, it is just that this hack makes the code even worse than it is already.
The spec of the refactoring is: make the special case for empty list and single element list disappear :)
the empty list case is VernacDeclareModule
ie https://coq.github.io/doc/master/refman/language/core/modules.html#coq:cmd.Declare-Module
one element is VernacDefineModule
with a 1 element list as the last argument, ie https://coq.github.io/doc/master/refman/language/core/modules.html#coq:cmd.Module used as Module M (? args) := stuff.
multiple element is also VernacDefineModule as Module M (?args) := stuff <+ otherstuff <+ etc.
, it seems to be interpreted as Module M (?args). Include stuff. Include otherstuff. Include etc. End M.
(VernacDefineModule just does Declaremods.start_module)
Yes, exactly.
So, very suspicious to dispatch on different code paths.
I guess the cleanest would probably to have the module definition code handle multiple bodies, rather than elaborating to an interactive session. Or the other way, always do the elaboration.
But of course, I wouldn't be surprised if they do subtly different things...
It is not independent on the following question: do we want to avoid rechecking the contents of a module when computing the result of Include M <+ N
? Currently, we trust the kernel that each declaration of an included module (or of an included "functor applied to self" in the case of <+
) are already correct. Afaicj, If we want to avoid the start_module
/end_module
for M1 <+ ... <+ Mn
while still avoiding to retype-check the whole included content, we would have to move the operation M1 <+ ... <+ Mn
in the kernel, that is, moving Declareops.declare_one_include
to the kernel, and trusting it.
An orthogonal but side question is: do we want to have Include
and <+
nodes directly in the kernel, that is in structure_field_body
? The pros are to have more sharing and thus suspectingly more efficient modules (??). The cons are that this increases a bit the TCB.
Slightly related is also https://github.com/coq/coq/pull/11897.
Related is also the (not so easy) question of functionalizing further declaremods.ml
so that, typically, the side effects on the global state are only in vernacentries.ml
.
Last updated: Jun 08 2023 at 04:01 UTC