Parenthesizing custom syntax

Stream: metaprogramming / tactics

[Sergei Stepanenko]

Hi all!
I think misunderstand something about parenthesizers for custom syntax.
Is there a canonical way parenthesize delaborator output based on the specified precedence? (Or doing it in the delaborator is simply wrong?)

E.g., in the example below, I try to invoke

let stx ← parenthesizeCategory `term_lang stx

expecting it to add parenthesis to syntax.
However, the final output doesn't contain parenthesis. Is it parenthesizeCategory not doing anything? Or parenthesis are removed by something in-between delaboration and printing?

Thank you in advance and sorry if it was already asked on Zulip. I found only examples for custom parsers.

MWE

import Lean
import Qq

open Lean Elab Meta PrettyPrinter Delaborator SubExpr Qq

inductive A where
| a : A
| b : A → A → A

declare_syntax_cat term_lang

syntax "(" term_lang ")" : term_lang
syntax:50 term_lang:50 ppSpace "∧" ppSpace term_lang:51 : term_lang
syntax "⊤" : term_lang

partial def elabA : TSyntax `term_lang → TermElabM Q(A)
  | `(term_lang| ($t:term_lang)) => elabA t
  | `(term_lang| ⊤) => pure q(@A.a)
  | `(term_lang| $t1:term_lang ∧ $t2:term_lang) => do
    let t1' ← elabA t1
    let t2' ← elabA t2
    pure q(@A.b $t1' $t2')
  | _ => throwUnsupportedSyntax

elab "⟪" t:term_lang "⟫" : term => elabA t

@[delab app.A.a]
def delab_a : Delab := do
  let e ← getExpr
  guard $ e.isAppOfArity' `A.a 0
  withAnnotateTermInfo `(⟪⊤⟫)

@[delab app.A.b]
def delab_b : Delab := do
  let e ← getExpr
  guard <| e.isAppOfArity' `A.b 2
  let `(⟪$x⟫) ← withNaryArg 0 <| delab | failure
  let `(⟪$y⟫) ← withNaryArg 1 <| delab | failure
  let stx ← `(⟪$x:term_lang ∧ $y:term_lang⟫)
  let stx ← parenthesizeCategory `term_lang stx
  Pure.pure <| TSyntax.mk stx

def test : A := ⟪(⊤ ∧ ⊤) ∧ (⊤ ∧ ⊤)⟫
#print test
-- Got: ⟪⊤ ∧ ⊤ ∧ ⊤ ∧ ⊤⟫
-- Expected: ⟪⊤ ∧ ⊤ ∧ (⊤ ∧ ⊤)⟫ or ⟪(⊤ ∧ ⊤) ∧ (⊤ ∧ ⊤)⟫

[Robin Arnez]

You need to register a category parenthesizer:

open Parenthesizer in
@[category_parenthesizer term_lang]
def term_lang.parenthesizer : CategoryParenthesizer := fun prec => do
  maybeParenthesize `term_lang false (fun stx => Unhygienic.run `(term_lang| ($(⟨stx⟩):term_lang))) prec <|
    parenthesizeCategoryCore `term_lang prec

[Sergei Stepanenko]

Robin Arnez said:

You need to register a category parenthesizer:

open Parenthesizer in
@[category_parenthesizer term_lang]
def term_lang.parenthesizer : CategoryParenthesizer := fun prec => do
  maybeParenthesize `term_lang false (fun stx => Unhygienic.run `(term_lang| ($(⟨stx⟩):term_lang))) prec <|
    parenthesizeCategoryCore `term_lang prec

Thanks! Works perfectly!