Make Precedence of operators visible in one click

[bblfish]

Agda makes it very nice to write condensed mathematical formulae. But it is often very difficult to work out what the precedence of parts of a formulae are if one does not know the domain very well. The reader needs to know the precedence of each binary operator to know what an operator applies to. This requires the reader to hunt around different files to finding out the precedence settings for each operator, calculate in mentally how this affects the meaning of a formula, etc... By the time one has done all this one will likely have forgotten what one was trying to do.

It would be great if on highlighting a formula agda-mode could on the click of a button provisionally insert all the parentheses. This would often drastically reduce the work required to understand what is going on.

[banacorn]

Is it possible to inspect the precedence of an operator on Emacs?

[bblfish]

I don't think so, but there seems to be interest in adding it. See this conversation in zulip.

[bblfish]

Here are a few examples of code from the Graphs library of Agda Categories.

Line 229 we have:

    M₁≡ : ∀ {A B} {f : A G.⇒ B} → M.M₁ f ▸ M₀≡ G′.≈ M₀≡ ◂ M′.M₁ f

After adding parenthesis and verifying by compiling it became a lot clearer:

M₁≡ : ∀ {A B} {f : A G.⇒ B} → (((M.M₁ f) ▸ M₀≡) G′.≈ (M₀≡ ◂ (M′.M₁ f)))

Interestingly yesterday evening as I had carefully read all the definitions, that reading was clear to me, but this morning I could no longer remember this.

Line 251 we have:

    M₁ j f ▸ ≡.sym (M₀≡ eq)

After adding the following parenthesis and testing by compiling it made a lot more sense:

    (M₁ j f) ▸ (≡.sym (M₀≡ eq)) -- rhs: the M₀ field of eq, turned around,

I can easily imagine a lot more complicated examples, and I believe I have come across such code in the past.

This makes me think that having a feature that would quickly add parenthesis would be in a way a bridge to Lisp users. They must have developed a brain module that can ignore parentheses they see explicity written, whereas Agda professionals must have developed one that adds them. ;-)

[banacorn]

If we can access the syntax tree of an expression, then we can do whatever we want on that expression, including (but not limited to) adding those parentheses back to make precedence visible.

That was what I intended when I started Agda's JSON protocol (but I stopped working on it for some reason :p)

Perhaps we can bring these features back, with the advent of LSP