Matthis Kruse (May 15 2021 at 17:12): 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!
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. :-)
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.
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.
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.
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.
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.)
Paolo Giarrusso (May 20 2021 at 22:08):Yeah the Camlp5 manual is indeed helpful, especially for features like SELF and NEXT
Yosuke Ito (May 21 2021 at 11:28):OK. I'll try to read it. Thanks for your advice! :wink:
Last updated: Oct 03 2023 at 02:34 UTC