pattern-matching `match`

Stream: metaprogramming / tactics

[Jon Eugster]

What's wrong with the following syntax pattern matching and how would I match syntax of the form fun x => match x with ...?

import Lean
-- import Mathlib

open Lean PrettyPrinter.Delaborator Parser

/-- Delaborator for functions on products like `α × β → γ`. -/
@[delab lam]
def delabMy : Lean.PrettyPrinter.Delaborator.Delab :=
  whenPPOption getPPNotation do
  let stx ← delabLam
  match stx with
    | `(fun $x ↦ match $x with | ($m, $n) => $body) => -- Error
      `(fun ($m, $n) ↦ $body)
    | _ => pure stx

example : True := by
  let myAdd : Nat × Nat → Nat := fun (m, n) ↦ m + n
  /-
  myAdd : ℕ × ℕ → ℕ × ℤ := fun x ↦ match x with | (m, n) => ↑m + ↑n
  ⊢ False
  -/
  trivial

[Jon Eugster]

My solution now is the following, which feels very messy:

import Lean

open Lean PrettyPrinter.Delaborator

/-- Delaborator for functions on products like `α × β → γ`. -/
@[delab lam]
def delabLamTuple : Lean.PrettyPrinter.Delaborator.Delab :=
  -- TODO: add the right options from Lean.PrettyPrinter.Delaborator.Options
  -- here, so that `set_option pp.XXX` has de desired effect.
  whenPPOption getPPNotation do
  let stx ← delabLam
  match stx with
  | `(fun $x ↦ $body) =>
    -- TODO: I expected the following syntax pattern match to work:
    -- | `(fun $x ↦ match $x with | ($m, $n) => $body) => `(fun ($m, $n) ↦ $body)
    -- What follows now is a tedious manual match through the entire syntax tree
    -- which is quite error-prone.

    -- We extract the following variables: "match `x₁` with | (`m`, `n`) => `body₁`"
    match body.raw with
    | .node _ ``Lean.Parser.Term.match #[_, _, _,
        (.node _ `null #[.node _ ``Lean.Parser.Term.matchDiscr #[_, x₁]]), _, alts₀] =>
      if x == x₁ then
        match alts₀ with
        | (.node _ ``Lean.Parser.Term.matchAlts #[(.node _ `null #[
            (.node _ ``Lean.Parser.Term.matchAlt #[_, alts₁, _, body₁])])]) =>
          match alts₁ with
          | .node _ `null #[(.node _ `null #[
              (.node _ `Lean.Parser.Term.tuple #[_,
                (.node _ `null #[m, _, (.node _ `null #[n])]), _])])] =>
            let body₁ : TSyntax `term := ⟨body₁⟩
            let m : TSyntax `term := ⟨m⟩
            let n : TSyntax `term := ⟨n⟩
            `(fun ($m, $n) ↦ $body₁)
          | _ => pure stx
        | _ => pure stx
      else pure stx
    | _ => pure stx
  | _ => pure stx

example : True := by
  let myAdd : Nat × Nat → Nat := fun (m, n) ↦ m + n
  trivial

[Kyle Miller]

It's one of these issues where you need to be explicit about the antiquotes (use the full form with the syntax name $x:ident rather than the abbreviated form $x).

@[delab lam]
def delabMy : Lean.PrettyPrinter.Delaborator.Delab :=
  whenPPOption getPPNotation do
  let stx ← delabLam
  match stx with
    | `(fun $x:ident ↦ match $x':ident with | ($m, $n) => $body) =>
      guard <| x == x'
      `(fun ($m, $n) ↦ $body)
    | _ => pure stx

[Kyle Miller]

I'm also trying to fix a bug: using $x in both places doesn't do an equality check, but rather it's two different patterns.

I'm not completely sure that checking equality with x == x' is completely correct, but it seems to work here for reasons I don't understand (I'd have to look into the core delaborator code). If that doesn't work in general, you could do x.getId == x'.getId, which should be ok since the delaborator handles shadowing.

[Jon Eugster]

Thank you Kyle :D