Maxime Dénès (Mar 14 2022 at 13:14): Maxime Dénès (Mar 14 2022 at 13:14):Hi! I'm wondering if the declaration of printing rules should be considered something that happens at parsing time or at execution time. Currently it seems to me that "specific" printing rules are declared with notation interpretation https://github.com/coq/coq/blob/cd406a522900fe08e1b0c1dcafb28eb699edf4ac/vernac/metasyntax.ml#L1442 whereas "generic" printing rules are declared with syntax extentions https://github.com/coq/coq/blob/cd406a522900fe08e1b0c1dcafb28eb699edf4ac/vernac/metasyntax.ml#L838
Emilio Jesús Gallego Arias (Mar 14 2022 at 13:18):Do you want to be able to print ASTs without executing the Notation command?
Emilio Jesús Gallego Arias (Mar 14 2022 at 13:19):Last time I looked that stuff seemed fairly orthogonal so it should be easy to separate, but I am not super up to date, maybe @Ana de Almeida Borges @Ali Caglayan @Hugo Herbelin know more these days
Maxime Dénès (Mar 14 2022 at 13:20):Emilio Jesús Gallego Arias said:
Do you want to be able to print ASTs without executing the Notation command?
Good question. For VsCoq I don't think it will be required, but I guess it could be useful for coqdoc, linters, etc.
Maxime Dénès (Mar 14 2022 at 13:21):Also for metaprogramming at the vernac level
Enrico Tassi (Mar 14 2022 at 13:22):But without interpreting terms, what would you like to print? Ideally, with just the parsing phase run, one should be only able to print constr_expr
Enrico Tassi (Mar 14 2022 at 13:23):I don't know the code of metasyntax you point to, but printing rules are from glob to constr_expr no?
Gaëtan Gilbert (Mar 14 2022 at 13:23):I think it's the format stuff so from constr_expr to pp
Maxime Dénès (Mar 14 2022 at 13:23):I don't know this code either, I'm afraid.
Maxime Dénès (Mar 14 2022 at 13:24):@Gaëtan Gilbert Do you know what a "generic" or "specific" rule is?
Enrico Tassi (Mar 14 2022 at 13:24):right, that one can be parsing
Enrico Tassi (Mar 14 2022 at 13:24):Of course a specific rule is less generic than a generic one ;-P
Gaëtan Gilbert (Mar 14 2022 at 13:24):just a guess, but maybe specific means there was an explicit format string
Enrico Tassi (Mar 14 2022 at 13:24):It's all commuting squares, really
Maxime Dénès (Mar 14 2022 at 13:26):If I read the code correctly, a generic notation is a specific notation and a boolean.
Maxime Dénès (Mar 14 2022 at 13:34):Enrico Tassi said:
right, that one can be parsing
doesn't it require scopes, though?
Enrico Tassi (Mar 14 2022 at 14:17):I don't think so, scopes enable/disable an interpretation (the one with a glob term).
Maxime Dénès (Mar 14 2022 at 15:01):but the declaration of specific rules takes a scope
Maxime Dénès (Mar 14 2022 at 15:02):(not in the rule itself, on the side)
Ana de Almeida Borges (Mar 14 2022 at 17:02):Sorry, I don't know enough to help here.
Last updated: Oct 13 2024 at 01:02 UTC