14.5. マクロ（Macros）🔗

14.5.1. 健全性（Hygiene）🔗

マクロが 健全である （hygienic）であるとは、その展開によって識別子のキャプチャが生じないようなマクロを指します。 識別子のキャプチャ （identifier capture）とは、識別子がソースコード内で発生するスコープ以外の束縛位置を参照してしまうことです。識別子のキャプチャには2つのタイプがあります：

• マクロ展開で束縛子が導入される場合、マクロのパラメータである識別子はその名前が一致すると導入された束縛子を参照してしまう可能性があります。

• マクロ展開が名前を参照することを意図している場合において、その名前がローカルに束縛されているか、新しいグローバル名として導入されているコンテキストにおいてマクロが使用されると、間違った名前を参照してしまう可能性があります。

1つ目の変数キャプチャは、マクロによって導入されるすべての束縛子が新しく生成されたもので、かつグローバルで一意な名前を使用することで、2つ目は定数の参照に常に完全修飾名を使用することでそれぞれ回避できます。1つ目の対策での新しい名前は、再帰的なマクロでの変数キャプチャを回避するためにマクロの呼び出しのたびに生成する必要があります。これらのテクニックはエラーを起こしやすいです。変数キャプチャの問題は、名前の選択の一致に依存するためテストが難しく、これらのテクニックを一貫して適用すると読みづらいコードになります。

Lean は自動的な健全性の機構を持ちます：ほとんどすべての場合において、マクロは自動的に健全です。導入された束縛子によるキャプチャは、マクロによって導入された識別子を マクロスコープ （macro scope）で注釈することで回避できます。マクロスコープはマクロ展開のそれぞれの呼び出しごとに一意に識別されます。束縛子と識別子の使用が同じマクロスコープを持つ場合、それらはマクロ展開の同じステップで導入されたものであり、お互いを参照する必要があります。同様に、マクロによって生成されたコードでのグローバル名の使用は、それが展開されたコンテキストではローカルの束縛子によってキャプチャされません。なぜなら、そのグローバル名の使用位置には束縛子の出現には存在しないマクロスコープがあるからです。新しく導入されたグローバル名によるキャプチャは、潜在的なグローバル名参照に対してマクロの本体で生成されるコードで quotation 時に一致するグローバル名のセットをアノテーションすることで防がれます。潜在的な参照による注釈された識別子は 事前解決された識別子 （pre-resolved identifier）と呼ばれ、 Syntax.ident コンストラクタの Syntax.Preresolved フィールドは潜在的な参照先を格納するために使用されます。エラボレーションの際に、識別子が事前解決されたグローバル名に関連付けられている場合、他のグローバル名は有効な参照対象として考慮されません。

生成された構文へのマクロスコープと事前解決された識別子の導入は quotation の間に行われます。quotation 以外の方法で構文を構築するマクロであっても、他の何らかの方法で健全性を確保する必要があります。Lean の健全性アルゴリズムの詳細については Ullrich and de Moura (2020)Sebastian Ullrich and Leonardo de Moura, 2020. “Beyond notations: Hygienic macro expansion for theorem proving languages”. In Proceedings of the International Joint Conference on Automated Reasoning. and Ullrich (2023)Sebastian Ullrich, 2023. An Extensible Theorem Proving Frontend. Dr. Ing. dissertation, Karlsruhe Institute of Technology を参照してください。

14.5.2. マクロモナド（The Macro Monad）🔗

マクロモナド MacroM は健全性を実装し、エラーを報告するのに十分な機能を有しています。マクロ展開には環境を直接変更したり、単一化を実行したり現在のローカルコンテキストを調べたり、ある特定のコンテキストのみで意味を持つようなことはできません。これにより、Lean 全体で同じマクロ機構を使用することができ、マクロは エラボレータ よりもはるかに書きやすくなります。

Lean.MacroM (α : Type) : Type

Lean.Macro.expandMacro? (stx : Lean.Syntax)
    : Lean.MacroM (Option Lean.Syntax)

Lean.Macro.trace (clsName : Lean.Name)
    (msg : String) : Lean.MacroM Unit

Lean.Macro.throwUnsupported {α : Type}
    : Lean.MacroM α

Lean.Macro.Exception.unsupportedSyntax
    : Lean.Macro.Exception

Lean.Macro.throwError {α : Type} (msg : String)
    : Lean.MacroM α

Lean.Macro.throwErrorAt {α : Type}
    (ref : Lean.Syntax) (msg : String)
    : Lean.MacroM α

Lean.Macro.withFreshMacroScope {α : Type}
    (x : Lean.MacroM α) : Lean.MacroM α

Lean.Macro.addMacroScope (n : Lean.Name)
    : Lean.MacroM Lean.Name

Lean.Macro.hasDecl (declName : Lean.Name)
    : Lean.MacroM Bool

Lean.Macro.getCurrNamespace
    : Lean.MacroM Lean.Name

Lean.Macro.resolveNamespace (n : Lean.Name)
    : Lean.MacroM (List Lean.Name)

Lean.Macro.resolveGlobalName (n : Lean.Name)
    : Lean.MacroM
      (List (Lean.Name × List String))

14.5.3. Quotation🔗

Quotation は Syntax 型のデータとして表現するためにコードをマークします。quote されたコードはパースされますが、エラボレートはされません。つまり構文的に正しくなければなりませんが、意味を為している必要はありません。quotation はコードをプログラム的に生成することをとても簡単にします：Lean のパーサが生成する node 値の特定の入れ子をリバースエンジニアリングするのではなく、パーサを直接呼び出して生成することができます。これはまた、文法のリファクタリングが、ユーザから見える具体的な構文に影響を与えることなくパースされた木の内部を変更する可能性がある場合により堅牢です。Lean の quotation は ​`( と ) で囲まれます。

quote される構文カテゴリやパーサは、その名前を先頭のバックティックと括弧の後に置き、その後に縦棒（|）を置くことで示すことができます。特殊なケースとして、tactic という名前はタクティクやタクティクの列をパースするために使用することができます。構文カテゴリやパーサが提供されていない場合、Lean は quotation を項と空でない一連のコマンドの両方としてパースしようとします。項の quotation はコマンドの quotation よりも優先順位が高いため、あいまいな場合は項として解釈されます；これはコマンド列の quotation であることを明示することで上書きできます。

application type mismatch
  cmd1.raw
argument
  cmd1
has type
  TSyntax `command : Type
but is expected to have type
  TSyntax `term : Type

term ::=
      Syntax quotation for terms. `(term)
    | `(command+)
    | `(tactic|tactic)
    | `(tactic|tactic;*)
    | `(p : identp:ident|Parse a p : identp here )

quotation は Syntax 型ではなく、 m Syntax 型を持ったモナドアクションです。 健全性の節 で説明されているように、 マクロスコープ と事前解決された識別子を追加することで hygiene を実装しているため、quotation はモナドです。使用する特定のモナドは quotation の暗黙のパラメータであり、 MonadQuotation 型クラスのインスタンスを持つ任意のモナドが適しています。 MonadQuotation は MonadRef を継承しており、マクロ展開またはエラボレータが現在処理している構文のソース位置にアクセスすることができます。 MonadQuotation はさらに識別子に マクロスコープ を追加し、サブタスクに新しいマクロスコープを使用する機能を含んでいます。quotation をサポートするモナドは、 MacroM ・ TermElabM ・ CommandElabM ・ TacticM です。

antiquot ::=
      $ident(:ident)?
    | $(term)(:ident)?

ex1 {m : Type → Type} [Monad m] [MonadQuotation m] (e : TSyntax `term) : m (TSyntax `term)

ex2 {m : Type → Type} [Monad m] [MonadQuotation m] (e : TSyntax `num) : m (TSyntax `term)

def ex2 (e) := show m _ from `(2 + expected '`(tactic|' or no space before spliced term$ e:num)

<example>:1:35: expected '`(tactic|' or no space before spliced term

def ex2 (e) := show m _ from `(2 + $e expected ')':num)

<example>:1:38: expected ')'

def f : {m : Type → Type} → [inst : Monad m] → [inst : Lean.MonadQuotation m] → Lean.Term → Nat → m Syntax :=
fun {m} [Monad m] [Lean.MonadQuotation m] x n => do
  let info ← Lean.MonadRef.mkInfoFromRefPos
  let scp ← Lean.getCurrMacroScope
  let mainModule ← Lean.getMainModule
  pure
      {
          raw :=
            Syntax.node2 info `Lean.Parser.Term.fun (Syntax.atom info "fun")
              (Syntax.node4 info `Lean.Parser.Term.basicFun
                (Syntax.node1 info `null (Syntax.ident info "k".toSubstring' (Lean.addMacroScope mainModule `k scp) []))
                (Syntax.node info `null #[]) (Syntax.atom info "=>")
                (Syntax.node3 info `«term_+_»
                  (Syntax.node3 info `«term_+_» x.raw (Syntax.atom info "+") (Lean.quote `term (n + 2)).raw)
                  (Syntax.atom info "+")
                  (Syntax.ident info "k".toSubstring' (Lean.addMacroScope mainModule `k scp) []))) }.raw

ex1 {m : Type → Type} [Monad m] [MonadQuotation m] (xs : Syntax.TSepArray `term ",") : m (TSyntax `term)

ex2 {m : Type → Type} [Monad m] [MonadQuotation m] (xs : Array (TSyntax `term)) : m (TSyntax `term)

#[0, 1, 2, 3]

[1, 2, 3]

mkStx {m : Type → Type} [Monad m] [MonadQuotation m] (e : Option (TSyntax `term)) : m Term

⟨| 5 |⟩

⟨| |⟩

antiquot ::= ...
    | atom%$ident

14.5.4. 構文のマッチ（Matching Syntax）🔗

quasiquotation はテンプレートにマッチする構文を認識するためのパターンマッチで使用することができます。項として使用される quotation の中の antiquotation が通常の非 quote 式として扱われる領域であるのと同じように、パターンの中の antiquotation の領域は通常の Lean のパターンとして扱われます。quote パターンは他のパターンとは異なる方法でコンパイルされるため、1つの Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match 式の中に quote パターン以外のパターンを混在させることはできません。通常の quotation と同様に、quote パターンはまず Lean のパーサによって処理されます。そしてパーサの出力はマッチするかどうかを判断するコードにコンパイルされます。構文マッチは、マッチする構文が Lean のパーサによって quotation を経由・または直接ユーザコードで生成されたものであると仮定し、いくつかのチェックを省略するためにこれを使用します。例えば、ある位置に特定のキーワード以外が存在しない場合、そのチェックは省略されます。

構文は以下の場合に quote パターンにマッチします：

アトム

キーワードアトム（ termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false. if や Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match など）は token. の後にアトムが続く、子を1つだけ持つノードとなります。多くの場合、文法は単一のキーワードしか許さないため、特定のアトムの値をチェックする必要はなく、チェックは行われません。マッチする語の構文がチェックを必要とする場合は、ノードの種別を比較します。

文字列や数値リテラルなどのリテラルは、その文字列表現によって比較されます。パターン ​`(0x15) と quotation ​`(21) はマッチしません。

ノード

マッチするパターンと値の両方が Syntax.node を表す場合、両方が同じ構文種別・同じ数の子を持ち、それぞれの子のパターンが対応する子の値にマッチする時にマッチします。

識別子

パターンとマッチする値の両方が識別子の場合、そのリテラル Name の値はマクロスコープで等しいかどうか比較されます。同じように「見える」識別子はマッチし、それらが同じ束縛子を参照しているかどうかは問題になりません。この設計上の選択により、名前を参照で比較できるコンパイル時の環境に対してアクセスできないコンテキストでも quote パターンマッチを使用できるようになります。

quotation のパターンマッチはパーサが出力するノードの種別に基づいて行われるため、同じように見える quotation でも構文カテゴリが異なるとマッチしないことがあります。疑わしい場合は、quotation に構文カテゴリを含めると良いでしょう。

14.5.5. マクロの定義（Defining Macros）🔗

マクロを定義するには主に2つの方法があります： Lean.Parser.Command.macro_rules : commandmacro_rules コマンドと Lean.Parser.Command.macro : commandmacro コマンドです。 Lean.Parser.Command.macro_rules : commandmacro_rules コマンドは既存の構文にマクロを関連付けますが、 Lean.Parser.Command.macro : commandmacro コマンドは新しい構文とそれを既存の構文に変換するマクロを同時に定義します。 Lean.Parser.Command.macro : commandmacro コマンドは Lean.Parser.Command.notation : commandnotation を一般化したものと見なすことができます。これは単純に置換するのではなく、プログラム的に生成された展開を許可するものです。

command ::= ...
    | A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment?
      (@[attrInstance,*])?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind macro_rules ((kind := ident))?
        (| Syntax quotation for terms. `((p : identp:ident|)?Suitable syntax for p : identp ) => term)*

none

none

some 4

(3, 4)

(6, 4)

(42, 42)

(0, 0)

elaboration function for 'arbitrary!' has not been implemented
  arbitrary! Nat

42

command ::= ...
    | A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment?
      (@[attrInstance,*])?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind macro(:prec)? ((name := ident))? ((priority := prio))? macroArg* : ident =>
        macroRhs

macroArg ::=
    stx

macroArg ::= ...
    | ident:stx

attr ::= ...
    | macro ident

["hello", "hello", "hello"]