Parenthesizing in new notation

Stream: metaprogramming / tactics

[Robert Maxton]

Is there any simple way of adjusting parenthesization in notation without going so far as to just write your own delaborator? I've written exactly one of those so far and it was less than trivial, so I'm really hoping there's an option or something I can invoke.

The specific thing I want is, I've defined the following notations for comonadic extract and extend:

/-- Flipped `extend`. If `extract` is also defined, then if `f : w α → β`,
  `<⇑>f` is the lift of `f` along `extract`.`-/
  @[simp, reducible] def Extend.extend' [Extend w] : (w α → β) → w α → w β := flip Extend.extend

  --Fancy notation: ∘ has lower precedence than <$>, =>> and → have higher
  --precedence than <$> so that `f→ <$> x` is parsed the only way it makes sense,
  --but we also want `x =>> f ∘ g` to be parsed as "passing `x` to `f ∘ g`" (which is
  --also the only way that makes sense). There's no solution to that precedence
  --order, so we specially handle the `f ∘ g` case in the notation.

  @[inherit_doc Extend.extend] syntax (name := «term_=>>_»)
    term:108 " =>> " term:109 atomic(" ∘ " term:109)? : term
  macro_rules
  | `($x =>> $f) => ``(Extend.extend $x $f)
  | `($x =>> $f ∘ $g) => ``(Extend.extend $x ($f ∘ $g))

  open Lean PrettyPrinter.Delaborator SubExpr in
  @[delab app.Comonad.Extend.extend]
  partial def delabExtend : Delab := --...

  @[inherit_doc] prefix:max "<⇑>" => Extend.extend'
  @[inherit_doc] postfix:108 " →" => Extract.extract

All well and good. However , all three notations share the complication that they are generally used with functions, and specifically frequently used with anonymous lambdas, producing unaesthetic and often unclear delaborations such as

<⇑>fun x => x → -- Is this `extend' extract` with extract wrapped in a lambda, or `extract <| extend' id `?

Of course, the syntax is well defined and with a little thought you can, for example, exclude extract <| extend' id on type grounds, but I'd rather not have to do that -- I'd rather just have the delaborator automatically parenthesize lambdas so the above becomes the unambiguous <⇑>(fun x => x →).

Is there a way I can do this by fiddling with options/attributes/maybe notation3 which apparently automatically creates delaborators? Or will I have to write my own delab again?

[Kyle Miller]

In the pretty printing pipeline, delaborators are not supposed to be responsible for inserting parentheses, and instead it's the parenthesizers.

There are very few examples parenthesizers, and I've never written one before, but here's one possibility: modify the fun parenthesizer to always insert parentheses around it:

prefix:max (name := extendStx) "<⇑>" => id

open Lean PrettyPrinter.Parenthesizer Syntax.MonadTraverser in
@[parenthesizer Lean.Parser.Term.fun] def funParens : Lean.PrettyPrinter.Parenthesizer := do
  let stx ← getCur
  if stx.getKind != ``Lean.Parser.Term.paren then
    let stx ← `(($(⟨stx⟩)))
    let stx := stx.raw.setInfo (SourceInfo.fromRef stx)
    setCur stx

#check <⇑> fun x => x + 1
-- <⇑>(fun x ↦ x + 1) : ℕ → ℕ

That leads to more parentheses than necessary, but maybe it's ok for you?

Edit: I wrote this wrong. It doesn't go and parenthesize its contents.

[Kyle Miller]

Maybe rather than trying to figure out parenthesizers, it's easiest here to write a delaborator (via an app_unexpander) and insert the parentheses.

def Extend {α : Type} : α → α := id

prefix:max (name := extendStx) "<⇑>" => Extend

@[app_unexpander Extend]
def Extend.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $f) => `(<⇑> ($f))
  | _ => throw ()

#check <⇑> fun x => x + 2
-- <⇑>(fun x ↦ x + 2) : ℕ → ℕ

[Robert Maxton]

So, I'm trying to figure out parenthesizers after all, but I can't get the debug tools to respond. With the above notation, I can write myself a nice little stable of unit tests, but...

    set_option trace.PrettyPrinter.parenthesize true
    #check wα =>> f
    #check wα =>> f ∘ mf
    #check wα =>> f →
    #check wα =>> f2 → <$> wβ
    #check wα =>> f2 <*> wβ
    #check wf <*> wα
    #check wα =>> →
    #check wα =>> (· + 1 →)
    #check hf (· + 1 →)
    #check (· ∘ ·) (·) (const _ ·)
    #check <⇑> fun x => x + 1
    set_option trace.PrettyPrinter.parenthesize false

... none of these actually print any additional messages. And I did check stderr, too.

[Robert Maxton]

As a side note, to my mild dismay, it seems the thing I'm trying to 'fix' is in fact an intentional design decision. From Parenthesizer.lean:

Note that in case 2, it is also sufficient to parenthesize a parent node as long as the offending parser is still to
the right of that node. For example, imagine the tree structure of (f fun x => x) y without parentheses. We need to
insert some parentheses between x and y since the lambda body is parsed with precedence 0, while the identifier
parser for y has precedence maxPrec. But we need to parenthesize the $ node anyway since the precedence of its
RHS (0) again is smaller than that of y. So it's better to only parenthesize the outer node than ending up with
(f $ (fun x => x)) y.

My issue is apparently entirely down to my disagreement with this design decision -- I would prefer all anonymous lambdas to be parenthesized unconditionally, even when not required by precedence rules. In contrast, I don't see the need for the outer parentheses around f .... Function application is already left-associating anyway and must be in order for currying to be natural: f (fun x => x) y must be interpreted as (f (fun x => x)) y if f is to have type ('a -> 'a) -> ('b -> ('c)).

[Robert Maxton]

Kyle Miller said:

In the pretty printing pipeline, delaborators are not supposed to be responsible for inserting parentheses, and instead it's the parenthesizers.

There are very few examples parenthesizers, and I've never written one before, but here's one possibility: modify the fun parenthesizer to always insert parentheses around it:

prefix:max (name := extendStx) "<⇑>" => id

open Lean PrettyPrinter.Parenthesizer Syntax.MonadTraverser in
@[parenthesizer Lean.Parser.Term.fun] def funParens : Lean.PrettyPrinter.Parenthesizer := do
  let stx ← getCur
  if stx.getKind != ``Lean.Parser.Term.paren then
    let stx ← `(($(⟨stx⟩)))
    let stx := stx.raw.setInfo (SourceInfo.fromRef stx)
    setCur stx

#check <⇑> fun x => x + 1
-- <⇑>(fun x ↦ x + 1) : ℕ → ℕ

That leads to more parentheses than necessary, but maybe it's ok for you?

Edit: I wrote this wrong. It doesn't go and parenthesize its contents.

So, I started from this and started debugging. Here's what I've got:

  open Lean PrettyPrinter.Parenthesizer Syntax.MonadTraverser in
  @[parenthesizer Lean.Parser.Term.fun]
  def funParens : Lean.PrettyPrinter.Parenthesizer := do
    let stx ← getCur
    let parent := (←get).stxTrav.parents.back
    dbg_trace "before: {stx}"
    dbg_trace "children : {format stx.getArgs}"
    -- dbg_trace "parents: {parents.back}"
    if parent.getKind != ``Lean.Parser.Term.paren then
      let stx ← `(($(⟨stx⟩)))
      -- dbg_trace "after: {stx}"
      let stx := stx.raw.setInfo (SourceInfo.fromRef stx)
      setCur stx
    visitArgs do
      match (←getCur).getKind with
      | `Term.basicFun => parenthesizerForKind `Lean.Parser.Term.basicFun
      | stx@_ => visitToken

This almost works -- but, as I think you also ran into in your edit/PS, it doesn't recurse properly, it breaks parenthesization inside its children. I tried term.parenthesizer 0 as well, but that didn't seem to work either. Any ideas?

[Robert Maxton]

-- oh, I just needed to replace `Term.basicFun with the full `Lean.Parser.Term.basicFun.

[Robert Maxton]

Thanks for the help!

[Robert Maxton]

Spoke a little too soon, that version also doesn't recurse properly all the time but I didn't notice in my test cases. Here's a working edition, for posterity:

  open Lean PrettyPrinter.Parenthesizer Syntax.MonadTraverser in
  @[parenthesizer Lean.Parser.Term.fun]
  def funParens : Lean.PrettyPrinter.Parenthesizer := do
    let idx ← getIdx
    visitArgs do
      match (←getCur).getKind with
      | `Lean.Parser.Term.basicFun =>
          parenthesizerForKind `Lean.Parser.Term.basicFun
      | stx@_ =>
          visitToken
    -- After visiting the arguments, by the traversal invariant we are now
    -- one node to the *left* of the original node, unless we were already
    -- at the leftmost child.
    unless idx == 0 do goRight
    let stx ← getCur
    setCur stx
    let parent? := (←get).stxTrav.parents.back?
    let stx ← getCur
    let isParen := stx.getKind == ``Lean.Parser.Term.paren
    let st ← get
    let stx ←
      if let some parent := parent? then
        if !(isParen || parent.getKind == ``Lean.Parser.Term.paren) then do
          let stx' ← `(($(⟨stx⟩)))
          pure <| stx'.raw.setInfo (SourceInfo.fromRef stx)
        else
          pure stx
      else
        pure stx
    setCur stx
    goLeft
    -- after parenthesization, this syntax now has max precedence (atomic); adjust state accordingly
    modify (fun st => { st with contPrec := Parser.maxPrec, trailPrec := none })