I am trying to write a command that opens and closes a module. In the code for the synterp phase, I run Declaremods.Synterp.start_module
and Declaremods.Synterp.end_module
and in the code for the interp phase, I run the same functions using Declaremods.Interp
. Now, when I use the command in a .v
file, between the two interp functions, Global.current_modpath
returns test.B
and then when closing the module, Lib.Interp.end_module
returns theoldprefix
test
(i.e. without the name of the module) so that Safe_typing.check_current_label
complains that the labels B
and test
do not match. What am I doing wrong?
I am not sure about your exact problem but this thread here might be helpful: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Synterp.2FInterp.20and.20.60Lib.2Ecurrent_mp.60
Yes, thank you. It was indeed a useful thread, this is where I found Global
and SYNTERP AS
.
It is probably much clearer with a code snippet:
VERNAC COMMAND EXTEND TOTO CLASSIFIED AS SIDEFF
| [ "Cmd" ] SYNTERP AS _ {
let _ = Declaremods.Synterp.start_module None (Names.Id.of_string "B") [] (Declaremods.Check []) in
let _ = Declaremods.Synterp.end_module () in
()
} -> { let _ = Declaremods.Interp.start_module None (Names.Id.of_string "B") [] (Declaremods.Check []) in
let _ = Declaremods.Interp.end_module () in
() }
END
If you want to meta program the vernacular you have to align the synterp states. That is, the synterp state in which you run Declaremods.Interp.end_module ()
must be the one obtained by running Declaremods.Synterp.end_module ()
.
At least, this is what I do in Coq-Elpi, see https://github.com/LPCIC/coq-elpi/blob/8656694e2bb1f6afee7b8a3b1948cb88ca7a4c70/src/coq_elpi_builtins_synterp.ml#L631-L647
(and it works, thanks to the very much appreciated contribution of the the Bedrock's crew).
In short, Coq saves 1 state for you (after the synterp action) and restores it before running the matching interp action.
If your action is a composite one, you need to do the hard work. Instead of passing ()
from one phase to the other, you should pass a list of intermediate states you did freeze by hand and then interleave their unfreeze with the interp actions.
Or use Coq-Elpi ;-)
Ah, excellent, thank you. For the record, the following works:
VERNAC COMMAND EXTEND TOTO CLASSIFIED AS SIDEFF
| [ "Cmd" ] SYNTERP AS states {
let states = [] in
let _ = Declaremods.Synterp.start_module None (Names.Id.of_string "B") [] (Declaremods.Check []) in
let states = Vernacstate.Synterp.freeze () :: states in
let _ = Declaremods.Synterp.end_module () in
let states = Vernacstate.Synterp.freeze () :: states in
List.rev states
} -> {
let states = match states with
| [] -> assert false
| state :: states -> Vernacstate.Synterp.unfreeze state; states in
let _ = Declaremods.Interp.start_module None (Names.Id.of_string "B") [] (Declaremods.Check []) in
let _ = match states with
| [] -> assert false
| state :: states -> Vernacstate.Synterp.unfreeze state; states in
let _ = Declaremods.Interp.end_module () in
() }
END
Well, certainly, but that would defeat the point of torturing myself by doing things the hard way :)
If you find yourself doing too much state handling, it may be worth taking the code from Elpi and put it in Coq itself.
I'm talking about the data structure that logs these states and lets you organize them in groups of related actions. In turn this makes it easier to combine existing bricks and avoid mistakes that are easy to do with the flat list of states you use in the code up there (a brick may consume a state that does not belong to it). Kudos to @Janno and @Rodolphe Lepigre for that nice piece of code.
Note that using Vernacstate
from command-level plugin code is really not allowed in the current design of the vernac layer, even if it works today. So indeed, if support for this is needed it should be added to the vernac layer.
possibly just Summary is enough
Last updated: Oct 13 2024 at 01:02 UTC