Stream: Coq devs & plugin devs

Topic: Start module with declaremods


view this post on Zulip Quentin VERMANDE (Apr 05 2024 at 13:59):

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?

view this post on Zulip Janno (Apr 05 2024 at 14:10):

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

view this post on Zulip Quentin VERMANDE (Apr 05 2024 at 14:12):

Yes, thank you. It was indeed a useful thread, this is where I found Global and SYNTERP AS.

view this post on Zulip Quentin VERMANDE (Apr 06 2024 at 09:21):

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

view this post on Zulip Enrico Tassi (Apr 06 2024 at 20:31):

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 ;-)

view this post on Zulip Quentin VERMANDE (Apr 06 2024 at 20:54):

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 :)

view this post on Zulip Enrico Tassi (Apr 06 2024 at 21:17):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2024 at 10:49):

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.

view this post on Zulip Gaëtan Gilbert (Apr 07 2024 at 11:05):

possibly just Summary is enough


Last updated: Oct 13 2024 at 01:02 UTC