Delaborator for MyList

Stream: general

[Asei Inoue]

In the following code, I define MyList by mimicking the standard List, and also define syntax for list literals.
I would like to improve the readability of the output of the #check and #eval commands.
To do this, I need to implement a delaborator and a Repr instance.
Since it's fine for the outputs of #check and #eval to be the same, I want to unify the implementation as much as possible.
Is it possible to derive the Repr instance from the implementation of the delaborator?

/-- A custom-defined `List` -/
inductive MyList (α : Type) where
  /-- An empty list -/
  | nil
  /-- Add an element to the head of the list -/
  | cons (head : α) (tail : MyList α)
deriving DecidableEq

/-- An empty `MyList` -/
notation:max "m[]" => MyList.nil

/-- Add an element to a `MyList` -/
infixr:70 " ::: " => MyList.cons

/-- Custom list literal syntax. A trailing comma is allowed. -/
syntax "m[" term,*,? "]" : term

macro_rules
  | `(m[ ]) => `(m[])
  | `(m[$x]) => `($x ::: m[])
  | `(m[$x, $xs,*]) => `($x ::: (m[$xs,*]))

-- Since there is no delaborator, the custom syntax is not used in output.
-- We want it to display as `m[1, 2, 3] : MyList Nat`
#check m[1, 2, 3]

-- Since there is no `Repr` instance, the custom syntax is not used in output.
-- We want it to display as `m[1, 2, 3]`
#eval m[1, 2, 3]

[Kyle Miller]

You do not need a Repr instance for #eval. If you have a ToExpr instance plus a delaborator, then #eval will use those to pretty print the result.

[Asei Inoue]

@Kyle Miller Thanks. Can a common implementation be used for both the ToExpr instance and the delaborator?

[Kyle Miller]

No, the ToExpr instance is what enables using the delaborator.

[Aaron Liu]

Here's what a ToExpr instance can look like:

def foldr {α β} (l : MyList α) (init : β) (cons : α → β → β) := match l with
  | .nil => init
  | .cons head tail => cons head (foldr tail init cons)

instance {α} [Lean.ToExpr α] : Lean.ToExpr (MyList α) where
  toExpr l := foldr l (.app (.const ``MyList.nil []) (Lean.ToExpr.toTypeExpr α))
    (fun a acc => .app (.app (.app (.const ``MyList.cons []) (Lean.ToExpr.toTypeExpr α)) (Lean.ToExpr.toExpr a)) acc)
  toTypeExpr := .app (.const ``MyList []) (Lean.ToExpr.toTypeExpr α)

[Kyle Miller]

It can also look like deriving ToExpr

[Aaron Liu]

There's a deriving handler???

[Aaron Liu]

There is a deriving handler!

[Kyle Miller]

import Mathlib.Util.Notation3

/-- A custom-defined `List` -/
inductive MyList (α : Type) where
  /-- An empty list -/
  | nil
  /-- Add an element to the head of the list -/
  | cons (head : α) (tail : MyList α)
  deriving DecidableEq, Lean.ToExpr

-- optional ::: notation
/-- Add an element to a `MyList` -/
infixr:70 " ::: " => MyList.cons

notation3 "m[" (x", "* => foldr (a b => MyList.cons a b) MyList.nil) "]" => x

-- Now both pretty print:

#check m[1, 2, 3]

#eval m[1, 2, 3]

[Asei Inoue]

why you use notation3? notation3 is better than notation?

[Kyle Miller]

notation3 has a number of additional features, features that used to be in the Lean 3 notation command

[Kyle Miller]

Notice that you get a delaborator for this complex notation

[Asei Inoue]

Amazing. But is there a way to unify them without using notation3?

[Kyle Miller]

I personally don't see any reason to avoid notation3.

[Kyle Miller]

(Although the foldr syntax is odd. I had to copy it from the test file!)

[Asei Inoue]

Let me rephrase my question.
In the code below, a delaborator is defined.
Using the output of this delaborator, is it possible to define a ToString or Repr instance?

/-- A custom-defined `List` -/
inductive MyList (α : Type) where
  /-- An empty list -/
  | nil
  /-- Add an element to the head of the list -/
  | cons (head : α) (tail : MyList α)
deriving DecidableEq

/-- An empty `MyList` -/
notation:max "m[]" => MyList.nil

/-- Add an element to a `MyList` -/
infixr:70 " ::: " => MyList.cons

/-- Custom list literal syntax. A trailing comma is allowed. -/
syntax "m[" term,*,? "]" : term

macro_rules
  | `(m[ ]) => `(m[])
  | `(m[$x]) => `($x ::: m[])
  | `(m[$x, $xs,*]) => `($x ::: (m[$xs,*]))

namespace MyList

open Lean PrettyPrinter

@[app_unexpander MyList.cons]
def cons.unexpander : Unexpander := fun stx =>
  match stx with
  | `($(_) $head $tail) =>
    match tail with
    | `(m[]) => `(m[ $head ])
    | `(m[ $xs,* ]) => `(m[ $head, $xs,* ])
    | `(⋯) => `(m[ $head, $tail ])
    | _ => throw ()
  | _ => throw ()

#check (m[] : MyList Nat)
#check m[1, 2, 3]

end MyList