Maxime Dénès (Mar 11 2022 at 12:17): Maxime Dénès (Mar 11 2022 at 12:17):Hi! I would welcome some help to refactor the following hack: https://github.com/coq/coq/blob/master/vernac/declaremods.ml#L970
Maxime Dénès (Mar 11 2022 at 12:18):For a clean parsing/execution separation, I need module declaration primitives to return data (not just unit). Having these different codepaths makes it inconvenient.
Enrico Tassi (Mar 11 2022 at 13:29):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?
Maxime Dénès (Mar 11 2022 at 13:39):Well, I guess that's more or less doing the work :)
Maxime Dénès (Mar 11 2022 at 13:40):Help was on removing this hack and code duplication, not on the parsing separation.
Maxime Dénès (Mar 11 2022 at 13:42):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?
Maxime Dénès (Mar 11 2022 at 13:44):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.
Maxime Dénès (Mar 11 2022 at 13:46):The spec of the refactoring is: make the special case for empty list and single element list disappear :)
Gaëtan Gilbert (Mar 11 2022 at 14:16):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)
Maxime Dénès (Mar 11 2022 at 14:16):Yes, exactly.
Maxime Dénès (Mar 11 2022 at 14:17):So, very suspicious to dispatch on different code paths.
Maxime Dénès (Mar 11 2022 at 14:19):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.
Maxime Dénès (Mar 11 2022 at 14:19):But of course, I wouldn't be surprised if they do subtly different things...
Hugo Herbelin (Mar 11 2022 at 18:51):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.
Hugo Herbelin (Mar 11 2022 at 18:52):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.
Hugo Herbelin (Mar 11 2022 at 18:52):Slightly related is also https://github.com/coq/coq/pull/11897.
Hugo Herbelin (Mar 11 2022 at 18:53):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: Dec 07 2023 at 04:02 UTC