Writing a delaborator for WithLp.toLp

Stream: mathlib4

[Etienne Marion]

Hi! In #27270 I turn WithLp into a one field structure with two constructors, one of which being WithLp.toLp. The issue is that when writing WithLp.toLp p x in the code, it gets printed as { ofLp := x } which is not great for readability (and causes the build error in the PR in some testing file). Jireh suggested that we would just need a delaborator to fix the issue. Here comes the tricky part: I have absolutely no idea how meta programming works and find the syntax very obscure. Taking inspiration on the delaborator for the !₂[x, y, ...] notation in Analysis.InnerProductSpace.PiL2 I wrote the following:

import Mathlib

open Lean Meta Elab Term Macro TSyntax PrettyPrinter.Delaborator SubExpr

@[app_delab WithLp.toLp]
def test : Delab :=
  whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 3 do
    -- check that the `WithLp.toLp _` is present
    let p : Term ← withNaryArg 0 <| delab
    let x ← withNaryArg 2 delab
    `(toLp $p $x)

variable (p : ENNReal)

#check WithLp.toLp p (0 : ℝ) -- toLp✝ p 0 : WithLp p ℝ

which kinda works but prints out toLp✝ instead of just toLp. I don't know where to find instructions so I have no idea what to do to solve the issue or if what I wrote is the right way to do it. It looks like the issue comes from the fact that I want to print an existing function. Any help would be greatly appreciated!

[Eric Wieser]

You should use withNaryFun delab to get the toLp part

[Eric Wieser]

Though I think there might be a pp setting to disable constructor notation that could help here

[Eric Wieser]

(and we should probably build this for ULift.up too)

[Etienne Marion]

It looks like

set_option pp.structureInstances false

solves it, but I don't think we want this across all mathlib. Can it be activated only for toLp?

[Etienne Marion]

Ok this seems to work!

import Mathlib

open Lean Meta Elab Term Macro TSyntax PrettyPrinter.Delaborator SubExpr

@[app_delab WithLp.toLp]
def test : Delab :=
  whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 3 do
    let toLp ← withNaryFn delab
    let p ← withNaryArg 0 delab
    let x ← withNaryArg 2 delab
    `($toLp $p $x)

variable (p : ENNReal)

#check WithLp.toLp p (0 : ℝ) -- WithLp.toLp p 0 : WithLp p ℝ

[Etienne Marion]

Yes the error in the testing file is fixed, thanks Eric!

[Eric Wieser]

This also works:

@[app_delab WithLp.toLp]
def test : Delab := delabApp

[Etienne Marion]

lol, well that was easy

[Eric Wieser]

I was going to suggest that you can set the pp.structureInstances option locally in the elaborator then fall back to the default delaborator, then realized that the default delaborator already does the right thing.

[Eric Wieser]

(If you just call delab then Lean goes into a loop and prints an ellipsis)

[Etienne Marion]

So delabApp is the "Default delaborator for applications" (according to the docstring), but here because toLp is a constructor there is a kind of conflict and it's another delaborator which is used?

[Eric Wieser]

Yes, as there are multiple things registered with @[delab app], and they are tried in order

[Eric Wieser]

I guess this is the other way to write it without referring to a handler by name:

@[app_delab WithLp.toLp]
def test : Delab :=
  whenPPOption pp.structureInstances.get do
    withOptions (pp.structureInstances.set · false) do
      delab

though this isn't quite correct as it disables the option for x too.