disappearing brackets when pretty printing syntax

Stream: lean4

[Tomas Skrivan]

I have a problem with disappearing brackets when pretty printing syntax

import Lean

declare_syntax_cat myterm

syntax ident : myterm
syntax num : myterm
syntax:70 myterm:70 " * " myterm:71 : myterm
syntax:65 myterm:65 " + " myterm:66 : myterm
syntax "(" myterm ")" : myterm
syntax "return " myterm : myterm

open Lean PrettyPrinter in
run_meta
  let x ← `(myterm| a + b)
  let stx ← `(myterm| $x * d)
  let r ← `(myterm| return $stx:myterm)
  logInfo m!"before: {stx}"
  logInfo m!"after: {r}"

prints

before: (a + b) * d
after: return a + b * d

Why did the bracket around a + b disappeared on the last line?

[Jakub Nowak]

Because it's parsed as (return a) + (b * d) I think? Nope, that's not true.

[Jakub Nowak]

The brackets in before: aren't the brackets you defined in syntax "(" myterm ")" : myterm. In fact, you can comment this line and the brackets will still be there. I'm guessing the brackets were introduced by delabolator. It's still surprising why there are brackets in before:, but not in after:.

[Tomas Skrivan]

Yeah true, the bracket is not there as a syntax object. How can I add brackets automatically based on precedences?

[František Silváši 🦉]

I suspect custom syntactic categories don't get their parenthesizer by default, because I can fix this with just forwarding what is practically a default implementation:

open PrettyPrinter Parenthesizer in
@[category_parenthesizer myterm]
def mytermParenthesizer : CategoryParenthesizer := fun prec ↦
  maybeParenthesize
    `myterm
    false
    (fun stx ↦ Unhygienic.run `(myterm|($(⟨stx⟩):myterm)))
    prec
    (parenthesizeCategoryCore `myterm prec)

open Lean PrettyPrinter in
/--
info: before: (a✝ + b✝) * d✝
---
info: after: return (a✝ + b✝) * d✝
-/
#guard_msgs in
run_meta
  let x ← `(myterm| a + b)
  let stx ← `(myterm| $x * d)
  let r ← `(myterm| return $stx:myterm)
  logInfo m!"before: {stx}"
  logInfo m!"after: {r}"