Macro

Lean.Macro 型の項は、マクロの内部実装を表現しています。一般のプログラミング言語においてマクロとは構文を構文に変換することを指す言葉で、必ずしも特定の型や項に対応する概念ではありませんが、Lean の m : Macro は、Syntax → MacroM Syntax という関数型そのものです。

open Lean in

example : Macro = (Syntax → MacroM Syntax) := by rfl

Syntax 型が Lean の構文木をダイレクトに表していたように、Macro 型は Lean のマクロをダイレクトに表しています。

Macro 型とマクロの関係

Macro 型からマクロ

項 m : Macro を使ってマクロを定義するには、以下のように [macro] 属性を付与します。

open Lean

/-- `zeroLit` という構文の定義 -/
syntax (name := zeroLitStx) "zeroLit" : term

/-- `zeroLit` という構文を展開するマクロ -/
@[macro zeroLitStx]
def expandZeroLit : Macro := fun stx =>
  match stx with
  | `(term| zeroLit) => `(term| 0)
  | _ => Macro.throwUnsupported

-- マクロ展開されるので、0 に等しいという結果になる
#guard zeroLit = 0

マクロから Macro 型

実際にマクロを定義する際は、notation コマンドや macro コマンド、macro_rules コマンドなどを使用するでしょう。こういったコマンドでマクロを定義したとき、それが裏で Macro 型の項を生成していることを確かめることができます。特定のコマンドの実行後に新たに生成された識別子の名前をリストアップすることができる、whatsnew コマンドを使えば可能です。

import Mathlib.Util.WhatsNew
import Batteries.Data.String.Matcher

open Lean Elab Command

/-- コマンドの実行結果のメッセージに特定の文字列が含まれるかどうか検証するコマンド -/
syntax (docComment)? "#contain_msg" "in" command : command

elab_rules : command
  | `(command| #contain_msg in $_cmd:command) => do
    logInfo "success: nothing is expected"

  | `(command| $doc:docComment #contain_msg in $cmd:command) => do
    -- ドキュメントコメントに書かれた文字列を取得する
    let expected := String.trim (← getDocStringText doc)
    if expected.isEmpty then
      logInfo "success: nothing is expected"
      return

    -- 与えられたコマンドを実行する
    withReader ({ · with snap? := none }) do
      elabCommandTopLevel cmd

    -- コマンドの実行結果のメッセージを取得する
    let msgs := (← get).messages.toList
    let msgStrs := (← msgs.mapM (·.data.toString))
      |>.map (·.replace "\"" "")

    -- コマンドの実行結果のメッセージに expected が含まれるか検証する
    for msgStr in msgStrs do
      unless String.containsSubstr msgStr expected do
        logError "error: output string does not contain the expected string"

-- `macro_rules` コマンドの `whatsnew` コマンドによる出力の中に、`Macro` 型の項が含まれている
/-- def _aux_LeanByExample_Type_Macro_WhatsNew___macroRules_ident_1 : Macro := -/
#contain_msg in whatsnew in
  macro_rules
  | `(zeroLit) => `(1)

使用例

オセロのゲーム盤

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 boardStx]
def expandBoard : Macro := fun stx => do
  match stx with
  | `(term| board $rows:row*) =>
    let rows ← (rows : TSyntaxArray `row).mapM expandRow
    `(term| #[ $[$rows],* ])
  | _ => throwUnsupported

#check board
  - - - -
  - ● ○ -
  - ○ ● -
  - - - -

指数表記マクロ

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

import Mathlib.Tactic

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

マクロ展開を確認する方法

マクロがどのように展開されているか確かめるには、次で示すように Macro.expandMacro? 関数が利用できます。また、pp.macroStack オプションを使うという方法もあります。

section
  open Lean

  /-- `#expand` の入力に渡すための構文カテゴリ -/
  syntax macro_stx := command <|> tactic <|> term

  /-- マクロを展開するコマンド -/
  elab "#expand " "(" stx:macro_stx ")" : command => do
    let t : Syntax :=
      match stx.raw with
      | .node _ _ #[t] => t
      | _ => stx.raw
    match ← Elab.liftMacroM <| Macro.expandMacro? t with
    | none => logInfo m!"Not a macro"
    | some t => logInfo m!"{t}"
end

/- info: notation:50 lhs✝:51 " LXOR " rhs✝:51 => lxor lhs✝ rhs✝ -/
#expand (infix:50 " LXOR " => lxor)