Stream: Coq users

Topic: Command to know if notation is left or right assoc ?

Pierre Rousselin (Sep 20 2021 at 14:52):

Hello,
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).

Ana de Almeida Borges (Sep 20 2021 at 15:06):

I also don't know. As a workaround, you can temporarily Set Printing Parentheses. to find out.

Andrés Goens (Sep 20 2021 at 15:09):

Try using Print Grammar constr. (see here for details https://coq.inria.fr/refman/user-extensions/syntax-extensions.html)
I

Ana de Almeida Borges (Sep 20 2021 at 15:11):

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.

Andrés Goens (Sep 20 2021 at 15:11):

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 <-->).

Emilio Jesús Gallego Arias (Sep 21 2021 at 12:14):

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.

Ana de Almeida Borges (Sep 21 2021 at 12:55):

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

Emilio Jesús Gallego Arias (Sep 21 2021 at 13:15):

Thanks @Ana de Almeida Borges

Michael Soegtrop (Nov 12 2021 at 09:04):

There is Print Grammar constr. which prints the current grammar of Gallina terms.

Michael Soegtrop (Nov 12 2021 at 09:05):

See https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Print-Grammar.

Ana de Almeida Borges (Oct 06 2022 at 16:51):

@Pierre Rousselin we ended up implementing Print Notation, so from Coq 8.16 on you can just use it to find these things out!

Pierre Rousselin (Oct 07 2022 at 12:06):

Great ! Thanks a lot !

Last updated: Oct 01 2023 at 18:01 UTC