Stream: Coq users

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


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 <-->).

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Sep 21 2021 at 12:55):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 21 2021 at 13:15):

Thanks @Ana de Almeida Borges

view this post on Zulip Michael Soegtrop (Nov 12 2021 at 09:04):

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

view this post on Zulip Michael Soegtrop (Nov 12 2021 at 09:05):

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

view this post on Zulip 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!

view this post on Zulip Pierre Rousselin (Oct 07 2022 at 12:06):

Great ! Thanks a lot !


Last updated: Feb 04 2023 at 21:02 UTC