MacroM

MacroM は、マクロ展開のための主要なモナドです。マクロ衛生を実現するために必要な状態を保持しています。

使用例

オセロのゲーム盤

Macro 型の関数および MacroM モナドに包まれた関数を使用して、オセロのゲーム盤を表現する構文を定義することができます。

import Lean

/-- 盤面の１セルの状態 -/
inductive Cell where
  /-- 空のセル -/
  | empty
  /-- 黒のセル -/
  | black
  /-- 白のセル -/
  | white
deriving Inhabited, Repr, BEq

/-- 盤面の１セルを表す構文カテゴリ -/
declare_syntax_cat cell

/-- 盤面の何も置かれていない箇所 -/
syntax "-" : cell
/-- 盤面の黒のセル -/
syntax "●" : cell
/-- 盤面の白のセル -/
syntax "○" : cell

open Lean Macro

/-- cellの構文展開 -/
def expandCell (stx : TSyntax `cell) : MacroM (TSyntax `term) := do
  match stx with
  | `(cell| -) => `(Cell.empty)
  | `(cell| ○) => `(Cell.white)
  | `(cell| ●) => `(Cell.black)
  | _ => throwUnsupported

open Parser TSyntax

syntax row := withPosition((lineEq cell)*)
syntax (name := boardStx) "board" withoutPosition(sepByIndentSemicolon(row)) : term

/-- rowの構文展開 -/
def expandRow (stx : TSyntax `row) : MacroM (TSyntax `term) := do
  match stx with
  | `(row| $cells:cell*) => do
    let cells ← cells.mapM expandCell
    `(term| #[ $[$cells],* ])
  | _ => throwUnsupported

macro_rules
  | `(term| board $rows:row*) => do
    let rows ← (rows : TSyntaxArray `row).mapM expandRow
    `(term| #[ $[$rows],* ])

#guard
  let actual := board
    - - - -
    - ● ○ -
    - ○ ● -
    - - - -
  let expected : Array (Array Cell) := #[
    #[Cell.empty, Cell.empty, Cell.empty, Cell.empty],
    #[Cell.empty, Cell.black, Cell.white, Cell.empty],
    #[Cell.empty, Cell.white, Cell.black, Cell.empty],
    #[Cell.empty, Cell.empty, Cell.empty, Cell.empty]
  ]
  actual == expected

指数表記マクロ

a¹、a²、a³ のような指数表記をマクロで定義することもできます。以下の例では、aⁿ のような構文を定義しています。

open Lean Macro Parser

/-- 指数表記 -/
declare_syntax_cat exp
syntax "⁰" : exp
syntax "¹" : exp
syntax "²" : exp
syntax "³" : exp
syntax "⁴" : exp
syntax "⁵" : exp
syntax "⁶" : exp
syntax "⁷" : exp
syntax "⁸" : exp
syntax "⁹" : exp

-- ホワイトスペースなしで`exp`が１つ以上連続したときにマッチ
syntax term (noWs exp)+ : term
syntax term "⁻"(noWs exp)+ : term

-- `Inv`のために用意されている`⁻¹`という構文を上書きする
syntax term "⁻¹"(noWs exp)+ : term

def expToNat (stx : TSyntax `exp) : Nat :=
  match stx with
  | `(exp|⁰) => 0
  | `(exp|¹) => 1
  | `(exp|²) => 2
  | `(exp|³) => 3
  | `(exp|⁴) => 4
  | `(exp|⁵) => 5
  | `(exp|⁶) => 6
  | `(exp|⁷) => 7
  | `(exp|⁸) => 8
  | `(exp|⁹) => 9
  | _ => 0 -- 無効な構文の場合は0を返す

def expToSyntax (exp : Array (TSyntax `exp)) (litPrefix := 0) : MacroM (TSyntax `term) := do
  let digits := exp.map expToNat
  let exp := digits.foldl (fun acc x => 10 * acc + x) litPrefix
  return quote exp

macro_rules
  | `($lhs $[$exp]*) => do
    let stx ← expToSyntax exp
    `($lhs ^ $stx)
  | `($lhs ⁻$[$exp]*) => do
    let stx ← expToSyntax exp
    `($lhs ^ (Int.neg $stx))
  | `($lhs ⁻¹$[$exp]*) => do
    let stx ← expToSyntax exp (litPrefix := 1)
    `($lhs ^ (Int.neg $stx))

#guard (2 : Int)⁰ = 1
#guard 2³ = 8
#guard (2 : Rat)⁻¹⁰ = (1 : Rat) / 1024

ラベル付き木の項表示

ラベル付き木に対する項表示の構文をマクロで定義することができます。

variable {α : Type}

/-- ラベル付き木 -/
inductive Tree (α : Type) where
  | empty
  | node (v : α) (children : List (Tree α))
deriving BEq

/-- 葉(子を持たないノード) -/
def Tree.leaf (v : α) : Tree α := Tree.node v []

open Lean Macro

/-- ラベル付き木のための構文 -/
declare_syntax_cat tree

/-- `φ`が`tree`構文であるならば、`[tree| φ]`はラベル付き木を表す -/
syntax "[tree| " tree "]" : term

/-- 木のラベル。ラベルとしては、数値リテラル・文字列リテラル・文字リテラルを許可する -/
syntax tree_label := num <|> str <|> char

/-- 基底ケース: `[tree| 42]`などは正しい構文 -/
syntax tree_label : tree

/-- 再帰ステップ -/
syntax tree_label " * " "(" sepBy(tree, " + ") ")" : tree

-- 構文のテスト
#check_failure [tree| 42]
#check_failure [tree| 42 * (13 + 22 + 14)]

/-- `tree_label`に属する構文を`term`に変換する -/
def expandTreeLabel (stx : TSyntax `tree_label) : MacroM (TSyntax `term) :=
  match stx with
  | `(tree_label| $num:num) => `(term| $num)
  | `(tree_label| $str:str) => `(term| $str)
  | `(tree_label| $char:char) => `(term| $char)
  | _ => throwUnsupported

/-- 再帰的に`tree`構文を`term`に変換する -/
partial def expandTree (stx : TSyntax `tree) : MacroM (TSyntax `term) := do
  match stx with
  | `(tree| $label:tree_label) =>
    let v ← expandTreeLabel label
    `(term| Tree.leaf $v)
  | `(tree| $label:tree_label * ( $children+* )) =>
    let v ← expandTreeLabel label
    let children ← children.getElems.mapM expandTree
    `(term| Tree.node $v [ $children,* ])
  | _ => throwUnsupported

macro_rules
  | `([tree| $tree_stx:tree]) => expandTree tree_stx

-- マクロ展開のテスト
#guard
  let actual := [tree| 42]
  let expected := Tree.leaf 42
  actual == expected

#guard
  let actual := [tree| "foo" * ("a" + "b" + "c")]
  let expected := Tree.node "foo" [Tree.leaf "a", Tree.leaf "b", Tree.leaf "c"]
  actual == expected