Is it possible to get parentheses' positions or an operator's associativity from an AST?

Miscellaneous
1

Hi. While I was writing a Coq formatter, I encountered a problem of not being able to get information of parentheses.

Consider the following Theorem (from Induction: Proof by Induction in Software Foundation).

Theorem add_assoc : ∀ n m p : nat,
  n + (m + p) = (n + m) + p.

The parentheses in (n + m) + p are actually unnecessary as + has left-associativity, but the ones in n + (m + p) are necessary. The problem is that I couldn’t find a way to get the information of where parentheses are from an AST (Vernacexpr.vernac_control). (Btw, in Haskell, I could get the information via HsPar of HsExpr).

I thought I’d infer the parentheses’ positions from an AST by comparing the level of the operator of the reversed side (LHS if the operator has right associativity, and vice versa) if I got an operator’s associativity (either left or right assoc.). However, I couldn’t find the way for this either.

Is it possible to get parentheses’ positions or an operator’s associativity, or is there another way to pretty-print the theorem with parentheses?

I’m using Coq 8.17.1.

2

Hello.

“Print Grammar term.” shows the levels and associativity for each operator as part of the grammar. Consider this a clue to discovering how to get this information programmatically. I wouldn’t recommend parsing the output of this command. Keep in mind that commands can change the expression grammar and the set of operators dynamically with Notations.

3

Thank you for the tips. Unfortunately, it seems that only the printing function is public, and all the other necessary ones are private. I may end up with parsing the command output.

4

It turned out that I could get an operator’s associativity by Notgram_ops.grammar_of_notation.