Unexpander can't match expression with nested parentheses

Stream: lean4

[Chris Wong]

Hi all, I ran into a problem that I've minimized here:

import Mathlib

open Lean
open Lean.PrettyPrinter

def Board := Array (Option (Option Bool))

def Board.mk (array : Array (Option (Option Bool))) : Board := array

declare_syntax_cat cell
syntax "- " : cell
syntax "# " : cell
syntax "I " : cell

syntax "board " cell* : term

open Lean.Macro in
macro_rules
  | `(term| board $cells:cell*) => do
    let cells := ← cells.mapM fun
      | `(cell| -) => ``(none)
      | `(cell| #) => ``(some none)
      | `(cell| I) => ``(some (some true))
      | _ => throwUnsupported
    ``(Board.mk #[ $[$cells],* ])

@[app_unexpander Board.mk]
def unexpandBoard : Unexpander
  | `($_boardMk #[$cells,*]) => do
    let cells := ← (cells : TSyntaxArray `term).mapM fun
      | `(none) => `(cell| -)
      | `(some none) => `(cell| #)
      | `(some (some true)) => `(cell| I)
      | _ => throw ()
    `(board $cells*)
  | _ => throw ()

def board1 : Board := board - #

def board2 : Board := board - # I

#print board1
#print board2

board1 pretty-prints successfully, but board2 doesn't, and it seems like the difference is that the latter has a nested constructor.

Any ideas why this happens?

Context: I'm formalizing Tetris, and as part of that, I'm making a DSL for constructing game boards. Here's the unminimized code.

[Kyle Miller]

Unexpanders get run before parenthesization, so you can't have parentheses in your match patterns.

A way to work around this limitation is to nest matches

[Kyle Miller]

@[app_unexpander Board.mk]
def unexpandBoard : Unexpander
  | `($_boardMk #[$cells,*]) => do
    let cells := ← (cells : TSyntaxArray `term).mapM fun
      | `(none) => `(cell| -)
      | `(some none) => `(cell| #)
      | `(some $v) =>
        match v with
        | `(some true) => `(cell| I)
        | _ => throw ()
      | _ => throw ()
    `(board $cells*)
  | _ => throw ()

[Chris Wong]

Thanks Kyle, that makes sense!

[Chris Wong]

I wonder if it's worth calling this out in the Metaprogramming in Lean book.

[Kyle Miller]

Maybe match could also have some widget to make this more convenient, like

    | stripParens `(some (some true)) => `(cell| I)

[Chris Wong]

Chris Wong said:

I wonder if it's worth calling this out in the Metaprogramming in Lean book.

https://github.com/leanprover-community/lean4-metaprogramming-book/pull/162