I am fairly new to this and sorry if it has some obvious solution I did not find. Is there a way to know if a binary infix notation is left or right associative ?
I only know of
Locate "+". for instance, but it does not display this information (priority is also hidden).
I also don't know. As a workaround, you can temporarily
Set Printing Parentheses. to find out.
Print Grammar constr. (see here for details https://coq.inria.fr/refman/user-extensions/syntax-extensions.html)
My hack for finding the priority is to (try to) redefine the notation at some random level. For example:
Notation "a + b" := (a - b) (at level 0).
Since "+" is not actually defined at level 0, Coq complains with a very informative message:
Error: Notation "_ + _" is already defined at level 50 with arguments constr at level 50, constr at next level while it is now required to be at level 0 with arguments constr at next level, constr at next level.
you should see something like this:
| "95" RIGHTA [ SELF; "<->"; NEXT ]
where the number (
95 here) is the precedence (lower will be parsed first), then
RIGHTA tells you it's rigth associative and then you see the notation (in this case
Actually we could do much better, unless I'm missing something, we could add some kind of
Print Notation command; that kind of functionality is exposed in serapi, so users can do:
(Query () (Unparsing "_ + _")) (Answer 0 Ack) (Answer 0 (ObjList ((CoqUnparsing (((UnpBox (PpHOVB 0) ((() (UnpMetaVar (LevelLe 50) (Left))) (() (UnpTerminal " +")) (() (UnpCut (PpBrk 1 0))) (() (UnpMetaVar (LevelLt 50) (Right)))))) 50) () (((notgram_level (InConstrEntry 50 ((LevelLe 50) (LevelLt 50)))) (notgram_assoc (LeftA)) (notgram_notation (InConstrEntry "_ + _")) (notgram_prods (((GramConstrNonTerminal (ETProdConstr InConstrEntry ((NumLevel 50) (BorderProd Left (LeftA)))) ((Id x))) (GramConstrTerminal (PKEYWORD +)) (GramConstrNonTerminal (ETProdConstr InConstrEntry ((NumLevel 50) (BorderProd Right (LeftA)))) ((Id y)))))) (notgram_typs ((ETConstr InConstrEntry () ((NumLevel 50) (BorderProd Left (LeftA)))) (ETConstr InConstrEntry () ((NumLevel 50) (BorderProd Right (LeftA))))))))))))
you can see the full info in the several records. So maybe indeed worth opening a bug to put this code into Coq.
Thanks @Ana de Almeida Borges
Print Grammar constr. which prints the current grammar of Gallina terms.
@Pierre Rousselin we ended up implementing
Print Notation, so from Coq 8.16 on you can just use it to find these things out!
Great ! Thanks a lot !
Last updated: Feb 04 2023 at 21:02 UTC