Stream: Coq users

Topic: Parsing levels


view this post on Zulip Clément Pit-Claudel (May 19 2020 at 21:18):

Hi all. Can someone explain why the following makes sense? Print Grammar Constr says level 9 is LEFTA, but then complains that it's right associative:

Print Grammar constr. (* | "9" LEFTA *)
Notation "'Ob'" := 0 (at level 9, left associativity). (* Works *)
Notation "'A' x" := (x + x) (at level 9, left associativity). (* Fails *)
(* The command has indeed failed with message: *)
(* Level 9 is already declared right associative while it is now expected to be left associative. *)

view this post on Zulip Kenji Maillard (May 19 2020 at 21:33):

I don't have a clue why it happens but It's probably related to the content of level 9, if you try with the (empty in my case) level 8:

Notation "'A' x 'A'" := (x + x) (at level 8, left associativity). (* Works *)
Notation "'B' x" := (x + x) (at level 8, left associativity). (* Fails  but works if you remove the previous line *)

and in the level 9 there seem to be a notation along the lines of "'..' something '..'".

view this post on Zulip Clément Pit-Claudel (May 20 2020 at 01:27):

Huh, I didn't realize the second one would fail either

view this post on Zulip Clément Pit-Claudel (May 20 2020 at 01:34):

https://github.com/coq/coq/issues/12373

view this post on Zulip Paolo Giarrusso (May 20 2020 at 11:48):

For these sort of questions I often end up browsing the camlp5 manual

view this post on Zulip Paolo Giarrusso (May 20 2020 at 11:49):

actually, I’d first read carefully the chapter on notations of the Coq reference manual, and then if that fails go to camlp5.

view this post on Zulip Paolo Giarrusso (May 20 2020 at 11:51):

If you want to define notations which partially overlap, you also need to read about left-factoring and understand how LL(1) parsing works...

view this post on Zulip Paolo Giarrusso (May 20 2020 at 11:52):

(it sounds like this specific issue is an actual bug, but that’s the advice that I wish I got an year ago, so hope it helps somebody)

view this post on Zulip Clément Pit-Claudel (May 20 2020 at 14:00):

Paolo G. Giarrusso said:

actually, I’d first read carefully the chapter on notations of the Coq reference manual, and then if that fails go to camlp5.

Yup, I've done that many times :)


Last updated: Jan 27 2023 at 01:03 UTC