Stream: MetaCoq

Topic: Using notations for pretty printing terms


view this post on Zulip spaceloop (Oct 18 2023 at 19:37):

I'm writing a little plugin with metacoq that involves printing a Template Ast term. I would like to pretty print terms taking into account defined notations. Is this possible? If not directly, is there another way to access the table of defined notations in metacoq? Alternatively, would this be possible to do as an OCaml plugin?

view this post on Zulip Yannick Forster (Oct 18 2023 at 19:46):

There's no way to access it in MetaCoq

view this post on Zulip Yannick Forster (Oct 18 2023 at 19:48):

I'd guess that extending the TemplateMonad by a command mirroring Print Grammar would not be very hard though. If you want to give that a try, feel free to ask questions here. The MetaCoq team doesn't have enough cycles do do that atm, but we're happy to help

view this post on Zulip spaceloop (Oct 19 2023 at 08:06):

Thanks, I'd be happy to help when I find some time myself. Do you have any pointers to how/where a similar TemplateMonad command is implemented?

view this post on Zulip Jason Gross (Oct 19 2023 at 18:50):

Probably you want to start from tmLocate or tmLocateModule, which return lists of identifiers. You could make a variant that returns some sort of notation string first, and then figure out what sort of data structure you want to eventually return results in. Alternatively you could consider starting from tmPrint (if you want to just "print notations or something") or tmUnquote (if you want to have something that is like "get the printing string for this term"). The relevant code is in (I may have missed some, use git grep to find more):
https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/theories/TemplateMonad/Core.v#L42
https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/theories/TemplateMonad/Extractable.v#L44 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/theories/TemplateMonad/Common.v#L38 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/template_monad.ml#L31 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/template_monad.ml#L74 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/template_monad.ml#L112 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/template_monad.ml#L139 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/template_monad.ml#L186 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/template_monad.ml#L318 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/run_template_monad.ml#L498 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/run_extractable.ml#L178 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/run_extractable.ml#L218 https://github.com/MetaCoq/metacoq/blob/dc8a7a0f3fa28cfe58f3d806789f43903e9384be/template-coq/src/plugin_core.ml#L143

Probably you can find the right calls for Print Grammar by going git grep '"Grammar"' in Coq's source tree and seeing how Print Grammar is implemented

view this post on Zulip spaceloop (Oct 26 2023 at 07:46):

Thanks a lot for the pointers, that is really helpful :)


Last updated: Jul 23 2024 at 21:01 UTC