23.5.1. 卫生性🔗

如果一个宏的展开不会导致标识符捕获，那么该宏就是卫生的。 标识符捕获是指标识符最终指向的绑定位置并非源代码中该标识符出现处作用域内的绑定位置。 标识符捕获有两类：

• 如果宏的展开引入了绑定器，那么宏参数中的标识符可能会因名称恰好相同而最终指向这些新引入的绑定器。

• 如果宏的展开意图引用某个名称，但宏所用的上下文在局部绑定了该名称，或其中新引入了同名全局名称，那么它最终可能引用错误的名称。

第一类变量捕获可通过确保宏引入的每个绑定都使用新生成且全局唯一的名称来避免；第二类则可通过始终使用完全限定名称引用常量来避免。 每次调用宏时都必须重新生成新名称，以免递归宏中发生变量捕获。 这些技巧容易出错。 变量捕获问题很难测试，因为它依赖名称选择上的巧合；而始终贯彻这些技巧又会产生冗杂代码。

Lean 具有自动卫生机制：在几乎所有情况下，宏都会自动保持卫生。 通过给宏引入的标识符标注宏作用域来避免新引入绑定造成的捕获；宏作用域能唯一标识每次宏展开调用。 如果标识符的绑定处和使用处具有相同的宏作用域，那么它们由同一步宏展开引入，应当相互指代。 同理，宏生成代码中的全局名称使用处不会被展开上下文中的局部绑定捕获，因为这些使用处带有绑定出现处所没有的宏作用域。 为防止新引入的全局名称造成捕获，宏体生成代码中的潜在全局名称引用会被标注上引用时所有匹配全局名称的集合。 带有潜在指称对象标注的标识符称为预解析标识符；Syntax.ident 构造器上的 Syntax.Preresolved 字段用于存储这些潜在指称对象。 精译期间，如果一个标识符关联了预解析的全局名称，那么其他全局名称不会被视为有效的引用目标。

在生成语法中引入宏作用域和预解析标识符发生于引用期间。 不通过引用来构造语法的宏也应以其他方式确保卫生性。 有关 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.

23.5.2. 宏单子🔗

宏单子 MacroM 的能力足以实现卫生性并报告错误。 宏展开不能直接修改环境、执行合一、检查当前局部上下文，也不能进行任何只在某个特定上下文中才有意义的操作。 因此，同一套宏机制可以贯穿 Lean 使用，也使宏比精译器更容易编写。

Lean.MacroM (α : Type) : Type
Lean.MacroM (α : Type) : Type

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

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

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

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

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

Lean.Macro.throwErrorAt {α : Type} (ref : Lean.Syntax) (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.withFreshMacroScope {α : Type}
  (x : Lean.MacroM α) : Lean.MacroM α

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

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

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

Lean.Macro.resolveNamespace (n : Lean.Name) :
  Lean.MacroM (List 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))
Lean.Macro.resolveGlobalName
  (n : Lean.Name) :
  Lean.MacroM
    (List (Lean.Name × List String))

23.5.3. 引用🔗

引用把代码标记为以 Syntax 类型的数据表示。 被引用的代码会被解析，但不会被精译——它必须在语法上正确，却不必有意义。 引用让以编程方式生成代码容易得多：无需逆向推导 Lean 解析器会产生的 node 值的具体嵌套结构，而可以直接调用解析器来创建它们。 这种方式面对语法重构也更稳健；重构可能改变解析树的内部结构，却不影响用户可见的具体语法。 Lean 中的引用由 `( 和 ) 包围。

可以在开头的反引号和左括号之后写出被引用的语法类别或解析器名称，再跟一条竖线（|）。 作为特例，名称 tactic 可用于解析策略或策略序列。 若未提供语法类别或解析器，Lean 会同时尝试把引用解析为项和非空命令序列。 项引用的优先级高于命令引用，因此有歧义时会选择项解释；显式指明引用的是命令序列可覆盖这一选择。

Application type mismatch: The argument
  cmd1
has type
  TSyntax `command
but is expected to have type
  TSyntax `term
in the application
  cmd1.raw

term ::=
      `(term)
    | `(command+)
    | `(tactic|tactic)
    | `(tactic|tactic;*)
    | `(p : identp:ident|在此解析一个 p : identp )

引用的类型不是 Syntax，而是类型为 m Syntax 的单子动作。 引用之所以是单子的，是因为它会如卫生性一节所述，通过添加宏作用域和预解析标识符来实现卫生性。 要使用的具体单子是引用的隐式参数；只要某单子具有 MonadQuotation 类型类的实例，就可以使用。 MonadQuotation 扩展了 MonadRef，后者使引用能够访问宏展开器或精译器当前正在处理的语法的源位置。MonadQuotation 还提供了向标识符添加宏作用域以及为子任务使用新宏作用域的能力。 支持引用的单子包括 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 +unexpected token '$'; expected '`(tactic|', 'do' or no space before spliced term $ e:num)

<example>:1:34-1:36: unexpected token '$'; expected '`(tactic|', 'do' or no space before spliced term

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

<example>:1:37-1:39: unexpected token ':'; expected ')'

def f : {m : Type → Type} → [Monad m] → [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 quotCtx ← Lean.MonadQuotation.getContext
  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".toRawSubstring' (Lean.addMacroScope quotCtx `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".toRawSubstring' (Lean.addMacroScope quotCtx `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 Term) : m Term

⟨| 5 |⟩

⟨| |⟩

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

23.5.4. 匹配语法🔗

准引用可以用于模式匹配，以识别符合某个模板的语法。 正如用作项的引用中的反引用区域会被当作普通未引用表达式处理，模式中的反引用区域也会被当作普通 Lean 模式处理。 引用模式的编译方式不同于其他模式，因此不能在同一个 Lean.Parser.Term.match : termmatch 表达式中与非引用模式混用。 与普通引用一样，引用模式首先由 Lean 的解析器处理。 随后，解析器输出会被编译成判断是否匹配的代码。 语法匹配假定被匹配语法由 Lean 解析器产生——无论是通过引用还是直接来自用户代码——并利用这一点省略某些检查。 例如，如果某个位置只能出现特定关键字，就可以省略检查。

在以下情况下，语法与引用模式匹配：

原子

关键字原子（如 termIfThenElse : term`if c then t else e` 是 `ite c t e`（即“如果—那么—否则”）的记法；它根据 `c` 是否为真返回 `t` 或 `e`。 显式参数 `c : Prop` 本身没有计算内容；另有一个由实例合成得到的 `[Decidable c]` 参数，真正决定如何把 `c` 求值为真或假。 写成 `if h : c then t else e` 时表示依赖式条件 `dite`，此时 `t` 和 `e` 可以使用 `c` 为真或假的事实。 标识符中的记法约定：建议将 `if c then t else e` 写作 `ite`，并分别用 `left`、`right` 指代 `t`、`e`。if 或 Lean.Parser.Term.match : termmatch）会产生单例节点，其种类是以 token. 开头、后接该原子。 在许多情况下，无需检查具体原子值，因为语法只允许一个关键字，此时不会执行检查。 如果被匹配项的语法要求该检查，就会比较节点种类。

字面量（如字符串或数值字面量）按其底层字符串表示比较。 模式 `(0x15) 与引用 `(21) 不匹配。

节点

如果模式和被匹配值都表示 Syntax.node，则当二者语法种类相同、子节点数相同，且每个子模式都匹配对应子值时，匹配成功。

标识符

如果模式和被匹配值都是标识符，则比较其字面 Name 值在忽略宏作用域后的相等性。 “看起来”相同的标识符会匹配，它们是否指向同一绑定并不重要。 这一设计使引用模式匹配可用于无法访问编译期环境、因而无法按引用比较名称的上下文。

由于引用模式匹配基于解析器发出的节点种类，外观相同的引用如果来自不同语法类别，也可能不匹配。 拿不准时，在引用中写明语法类别会有所帮助。

语法模式匹配所绑定的变量具有 TSyntax k 类型，其中 k 描述可能的语法种类。 重复中的变量具有 TSyntaxArray k 类型；如果重复以字符串 sep 分隔，则类型为 TSepArray k sep。 有类型语法一节会更详细地介绍 TSyntax。

["2; true", "2; false", "4; true", "4; false"]

23.5.5. 定义宏🔗

定义宏主要有两种方式：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 ::= ...
    | docComment?
      (@[attrInstance,*])?
      `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。attrKind macro_rules ((kind := ident))?
        (| `((p : identp:ident|)?适合 p : identp 的语法 ) => term)*

none

none

some 4

(3, 4)

(6, 4)

(42, 42)

(0, 0)

elaboration function for `arbitrary!` has not been implemented
  arbitrary! (List Nat)

#[42]

command ::= ...
    | docComment?
      (@[attrInstance,*])?
      `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。attrKind macro(:prec)? ((name := ident))? ((priority := prio))? macroArg* : ident =>
        macroRhs

macroArg ::=
    stx

macroArg ::= ...
    | ident:stx

attr ::= ...
    | macro ident

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