Stream: Coq devs & plugin devs

Topic: Printing in parsing vs execution


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Mar 14 2022 at 13:21):

Also for metaprogramming at the vernac level

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Mar 14 2022 at 13:23):

I think it's the format stuff so from constr_expr to pp

view this post on Zulip Maxime Dénès (Mar 14 2022 at 13:23):

I don't know this code either, I'm afraid.

view this post on Zulip Maxime Dénès (Mar 14 2022 at 13:24):

@Gaëtan Gilbert Do you know what a "generic" or "specific" rule is?

view this post on Zulip Enrico Tassi (Mar 14 2022 at 13:24):

right, that one can be parsing

view this post on Zulip Enrico Tassi (Mar 14 2022 at 13:24):

Of course a specific rule is less generic than a generic one ;-P

view this post on Zulip Gaëtan Gilbert (Mar 14 2022 at 13:24):

just a guess, but maybe specific means there was an explicit format string

view this post on Zulip Enrico Tassi (Mar 14 2022 at 13:24):

It's all commuting squares, really

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Mar 14 2022 at 14:17):

I don't think so, scopes enable/disable an interpretation (the one with a glob term).

view this post on Zulip Maxime Dénès (Mar 14 2022 at 15:01):

but the declaration of specific rules takes a scope

view this post on Zulip Maxime Dénès (Mar 14 2022 at 15:02):

(not in the rule itself, on the side)

view this post on Zulip Ana de Almeida Borges (Mar 14 2022 at 17:02):

Sorry, I don't know enough to help here.


Last updated: Feb 02 2023 at 15:04 UTC