From adf7aa8c22e51922c663d133bd6531c98f8190a2 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 17 Nov 2024 23:38:49 +0900
Subject: [PATCH] =?UTF-8?q?Macro=20=E5=9E=8B=E3=82=92=E7=B4=B9=E4=BB=8B?=
 =?UTF-8?q?=E3=81=99=E3=82=8B=20Fixes=20#1135?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Type/Macro.lean | 49 +++++++++++++++++++++++++
 booksrc/SUMMARY.md                      |  1 +
 2 files changed, 50 insertions(+)
 create mode 100644 LeanByExample/Reference/Type/Macro.lean

diff --git a/LeanByExample/Reference/Type/Macro.lean b/LeanByExample/Reference/Type/Macro.lean
new file mode 100644
index 00000000..79e8995a
--- /dev/null
+++ b/LeanByExample/Reference/Type/Macro.lean
@@ -0,0 +1,49 @@
+/- # Macro
+
+`Lean.Macro` 型の項は、マクロを表現しています。一般のプログラミング言語においてマクロとは構文を構文に変換することですが、Lean の `m : Macro` は、`Syntax → MacroM Syntax` という型の関数そのものです。
+
+[`Syntax`](./Syntax.md) 型が Lean の構文木をダイレクトに表していたように、`Macro` 型は Lean のマクロをダイレクトに表しています。
+-/
+import Mathlib.Util.WhatsNew
+
+open Lean in
+
+/-- `Macro` とは、おおむね `Syntax` から `Syntax` への関数である -/
+example : Macro = (Syntax → MacroM Syntax) := by rfl
+
+/- ## Macro 型とマクロの関係
+
+### Macro 型からマクロ
+
+項 `m : Macro` を使ってマクロを定義するには、以下のように `[macro]` 属性を使用します。
+-/
+open Lean
+
+/-- `zeroLit` という構文の定義 -/
+syntax (name := zeroLitPar) "zeroLit" : term
+
+/-- `zeroLit` という構文を展開するマクロ -/
+def zeroLitExpand : Macro := fun stx =>
+  -- `stx : Syntax` に対するパターンマッチで関数を定義できる
+  match stx with
+  | `(zeroLit) => `(0)
+  | _ => Macro.throwUnsupported
+
+-- まだマクロとして登録されていないのでエラーになる
+/--
+error: elaboration function for 'zeroLitPar' has not been implemented
+  zeroLit
+-/
+#guard_msgs in #check zeroLit
+
+-- マクロとして登録する
+attribute [macro zeroLitPar] zeroLitExpand
+
+-- マクロ展開されるので、0 に等しいという結果になる
+#guard zeroLit = 0
+
+/- ### macro コマンドから Macro 型
+
+実際に、`macro` コマンドなどでマクロを定義したとき、それが `Macro` 型の項を生成していることを確かめることができます。`whatsnew` コマンドで、特定のコマンドの実行後に新たに生成された識別子の名前をリストアップすることができます。以下の出力の中に `Lean.Macro` 型の項があるはずです。-/
+
+whatsnew in macro "oneLit" : term => `(1)
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index f16391c6..e4130be6 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -104,6 +104,7 @@
   - [Char: Unicode 文字](./Reference/Type/Char.md)
   - [Float: 浮動小数点数](./Reference/Type/Float.md)
   - [List: 連結リスト](./Reference/Type/List.md)
+  - [Macro: マクロ](./Reference/Type/Macro.md)
   - [Prop: 命題全体](./Reference/Type/Prop.md)
   - [String: 文字列](./Reference/Type/String.md)
   - [Syntax: 具象構文木](./Reference/Type/Syntax.md)