Using the Delaborator

Stream: lean4

[Siddharth Bhat]

I'm trying to get a toy example of the delaborator working. As I understand it, it's supposed to allow me to control how terms are printed out, ideally performing "macro contraction", allowing one to pretty-print macro-expanded terms. Towards this end, I'm trying to get the i x macro which expands to MLIRTy.int x to delaborate into i x. Here's some code I have so far:

  import Lean.Parser
  import Init.Data.List
  import Lean.PrettyPrinter.Delaborator
  import Lean.Syntax

  open Lean.Parser
  open Lean.Meta
  open Std
  open Lean.Syntax
  open Lean.PrettyPrinter.Delaborator

  declare_syntax_cat mlir_type
  syntax ident numLit : mlir_type

  inductive MLIRTy : Type where
  | int : Int -> MLIRTy

  syntax "[mlir_type|" mlir_type "]": term

  macro_rules
    | `([mlir_type| i $x:numLit ]) => `(MLIRTy.int $x)

  def tyfoo : MLIRTy := [mlir_type| i 42]

  @[delab MLIRTy]
  def foo : Delab := do
    let ctx ← read
    let mut fields : Lean.Syntax ← `(i 1337)
    pure fields

  #print foo -- I expected: i 1337
/-  MLIRTy.int 42 -/ -- not what I expect.

I don't know if (1) my assumption about what the delaborator does is incorrect, or (2) I'm using the delaborator incorrectly?

[Siddharth Bhat]

Ah, it seems one can use appUnexpander to do what I need. I'll read how this relates to Delab now..

  import Lean.Parser
  import Init.Data.List
  import Lean.PrettyPrinter.Delaborator
  import Lean.Syntax

  open Lean.Parser
  open Lean.Meta
  open Std
  open Lean.Syntax
  open Lean.PrettyPrinter.Delaborator
  open Lean PrettyPrinter

  declare_syntax_cat mlir_type
  syntax ident numLit : mlir_type

  inductive MLIRTy : Type where
  | int : Int -> MLIRTy

  syntax "[mlir_type|" mlir_type "]": term

  macro_rules
    | `([mlir_type| i $x:numLit ]) => `(MLIRTy.int $x)

  @[appUnexpander MLIRTy.int]
  def baz : Unexpander
   | `($(_)) => `(i 32)

def x : MLIRTy := MLIRTy.int 32
#print x -- i✝ 32