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?

There's no way to access it in MetaCoq

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

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?

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

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

Last updated: Jul 23 2024 at 21:01 UTC