Bug in delaborator?

Stream: lean4

[Siddhartha Gadgil]

It seems that the delaborator has a bug where parenthesis are missing when needed in some cases (unless the bug is in formatTerm and Syntax.reprint. The code that gives this is:

import Lean

open Lean Meta PrettyPrinter in
def delabView (name: Name) : MetaM String :=
    do
    let info ←  getConstInfo name
    let term := info.value?.get!
    let stx ←  delab term
    let fmt ←  formatTerm stx
    return fmt.pretty

def egComp {α β γ α' : Type} (f : α' → β → γ) (g : (a : α) → α')
    (a : α) (b : β) :=  f (g a) b

#print egComp /- def egComp : {α β γ α' : Type} → (α' → β → γ) → (α → α') → α → β → γ :=
-- fun {α β γ α'} f g a b => f (g a) b -/

#eval delabView `egComp -- "fun {α β γ α'} f g a b => f g a b"

The parenthesis in (g a) are dropped in the last case. If I use Syntax.reprint I get the same error. However going straight from the expression to format is fine as in the print statement. Since I am using custom delaborators for data extraction, I need to do this in two steps (debugging my code showed what seems an upstream bug).

[Siddhartha Gadgil]

Looking at the syntax, the problem seems to be in Syntax.reprint as well as formatTerm. The right-hand side is as follows:

Lean.Syntax.node
          (Lean.SourceInfo.synthetic { byteIdx := 87381 } { byteIdx := 87381 } false)
          `Lean.Parser.Term.app
          #[Lean.Syntax.ident
              (Lean.SourceInfo.synthetic { byteIdx := 1398096 } { byteIdx := 1398096 } false)
              "f".toSubstring
              `f
              [],
            Lean.Syntax.node
              (Lean.SourceInfo.none)
              `null
              #[Lean.Syntax.node
                  (Lean.SourceInfo.synthetic { byteIdx := 1398097 } { byteIdx := 1398097 } false)
                  `Lean.Parser.Term.app
                  #[Lean.Syntax.ident
                      (Lean.SourceInfo.synthetic { byteIdx := 5592388 } { byteIdx := 5592388 } false)
                      "g".toSubstring
                      `g
                      [],
                    Lean.Syntax.node
                      (Lean.SourceInfo.none)
                      `null
                      #[Lean.Syntax.ident
                          (Lean.SourceInfo.synthetic { byteIdx := 5592389 } { byteIdx := 5592389 } false)
                          "a".toSubstring
                          `a
                          []]],
                Lean.Syntax.ident
                  (Lean.SourceInfo.synthetic { byteIdx := 349525 } { byteIdx := 349525 } false)
                  "b".toSubstring
                  `b
                  []]]

[Siddhartha Gadgil]

I see my mistake. If I use ppTerm the result is correct.
Still, should the above be considered a bug?

[Sebastian Ullrich]

If you look at the definition of ppExpr, you will find three components it is made up of:

• delaborator
• parenthesizer
• formatter

At this point you can probably guess which step you are missing :)

[Siddhartha Gadgil]

Where is the parenthesizer (just to learn - in my code I will use ppTerm).

[Sebastian Ullrich]

The main entry point ppTerm uses is docs#Lean.PrettyPrinter.parenthesizeCategory