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)
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
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
<+ 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
Last updated: Dec 07 2023 at 04:02 UTC