Stream: Coq users

Topic: Notation with similar prefix


view this post on Zulip Matthis Kruse (May 15 2021 at 17:12):

Hey, I'm trying to add two notations:
Notation "E '[' e ']'" := (fill_hole E e) (at level 75).
And
Notation "e '[' y '/' x ']'" := (esubst x y e) (at level 80, y at level 10).
Unfortunately, they clash and I can't get them to work properly. Either I get "Unknown interpretation for _ / _" for notations of the form "e[y/x]", or, if I wiggle the levels around, I get '/' expected after [term level 10] for terms of the form "E[e]". I wonder what is necessary to make both coexist. e and E differ in their types.
Thanks in advance!

view this post on Zulip Matthis Kruse (May 15 2021 at 18:23):

Alright, I've managed to resolve this by virtue of more or less randomly changing levels and associativity.

Notation "E '[' e ']'" := (fill_hole E e) (at level 1, e at next level, no associativity).
Notation "e '[' y '/' x ']'" := (esubst x y e) (at level 1, y at next level, left associativity).

...does the trick. :-)

view this post on Zulip Paolo Giarrusso (May 15 2021 at 19:14):

FWIW that looks good but if you need it again: the rule is that priorities in the common prefix must be identical, and you probably want to spell them out to be sure.

view this post on Zulip Paolo Giarrusso (May 15 2021 at 19:16):

This enables Coq to transform the grammar (by “left factoring”) to fit the limitations of the LL(1) parsing engine; the Coq manual does have a bit more info.

view this post on Zulip Yosuke Ito (May 17 2021 at 12:00):

Thanks, Paolo. As Matthis did, I was also struggling to introduce new notations in Coq. I carefully read the reference manual, but I could not figure it out. Your comment is really helpful.

view this post on Zulip Paolo Giarrusso (May 17 2021 at 19:12):

FWIW, the relevant section is https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules; improvements welcome.

view this post on Zulip Yosuke Ito (May 20 2021 at 11:40):

Thank you for sharing the link. The reference manual (and maybe other experts) recommends Print Grammar constr to see how the notations are defined, but I am not able to understand the output. To figure out the output, should I read https://camlp5.github.io/doc/htmlc/grammars.html ? (I think I need to study OCaml first.)

view this post on Zulip Paolo Giarrusso (May 20 2021 at 22:08):

Yeah the Camlp5 manual is indeed helpful, especially for features like SELF and NEXT

view this post on Zulip Yosuke Ito (May 21 2021 at 11:28):

OK. I'll try to read it. Thanks for your advice! :wink:


Last updated: Jan 28 2023 at 05:02 UTC