23.5.1. 卫生🔗

如果宏的扩展无法导致标识符捕获，则该宏为 hygienic。 标识符捕获是指标识符最终引用了源代码中该标识符出现的范围之外的绑定位点。 标识符捕获有两种类型：

• 如果宏的扩展引入了绑定器，那么作为宏参数的标识符最终可能会引用引入的绑定器（如果它们的名称恰好匹配）。

• 如果宏的扩展旨在引用一个名称，但该宏在本地绑定该名称或引入了新的全局名称的上下文中使用，则它最终可能会引用错误的名称。

第一种变量捕获可以通过确保宏引入的每个绑定都使用新生成的全局唯一名称来避免，而第二种变量捕获可以通过始终使用完全限定名称来引用常量来避免。 每次调用宏时都必须再次生成新名称，以避免递归宏中的变量捕获。 这些技术很容易出错。 变量捕获问题很难测试，因为它们依赖于名称选择的巧合，并且一致地应用这些技术会产生嘈杂的代码。

Lean 具有自动卫生功能：几乎在所有情况下，宏都会自动卫生。 通过使用 macroscopes 对宏引入的标识符进行注释，可以避免引入的绑定捕获，该标识符唯一标识宏展开的每次调用。 如果标识符的绑定和使用具有相同的宏范围，则它们是通过宏展开的同一步骤引入的，并且应该相互引用。 同样，宏生成的代码中全局名称的使用不会被扩展上下文中的本地绑定捕获，因为这些使用站点具有绑定出现中不存在的宏范围。 通过使用在宏主体中生成的代码中在引用时匹配的一组全局名称来注释潜在的全局名称引用，可以防止新引入的全局名称的捕获。 用潜在引用对象注释的标识符称为 预解析标识符，并且 Syntax.ident 构造函数上的 Syntax.Preresolved 字段用于存储潜在引用对象。 在精化期间，如果标识符具有与其关联的预解析全局名称，则其他全局名称不会被视为有效的引用目标。

宏作用域和预解析标识符的引入发生在 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。

23.5.2. 宏观单子🔗

宏单子 MacroM 足够强大，可以实现卫生和报告错误。 宏展开无法直接修改环境、执行统一、检查当前本地上下文或执行任何仅在特定上下文中有意义的其他操作。 这允许在整个 Lean 中使用相同的宏机制，并且它使宏的编写比 elaborators 容易得多。

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. 引述🔗

Quotation 标记用于表示为 Syntax 类型数据的代码。 引用的代码已被解析，但未详细说明 - 虽然它在语法上必须正确，但不一定有意义。 引用使得以编程方式生成代码变得更加容易：无需对 Lean 解析器将生成的 node 值的特定嵌套进行逆向工程，而是可以直接调用解析器来创建它们。 这在面对可能改变解析树的内部结构而不影响用户可见的具体语法的语法重构时也更加稳健。 Lean 中的报价被 `( and ) 包围。

被引用的语法类别或解析器可以通过将其名称放在左反引号和括号后面，后跟竖线（|）来指示。 作为特殊情况，名称 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 ::=
      Syntax quotation for terms. `(term)
    | `(command+)
    | `(tactic|tactic)
    | `(tactic|tactic;*)
    | `(p : identp:ident|Parse a p : identp here )

引用不是类型 Syntax，而是类型为 m Syntax 的单子操作。 引用是一元的，因为它通过添加 宏范围 和预解析标识符来实现 卫生，如 卫生部分 中所述。 要使用的特定 monad 是引用的隐式参数，任何具有 MonadQuotation 类型类实例的 monad 都适用。 MonadQuotation 扩展了 MonadRef，这使引用能够访问宏扩展器或精化器当前正在处理的语法的源位置。 MonadQuotation 还包括将 宏范围 添加到标识符并为子任务使用新的宏范围的功能。 支持报价的 Monad 包括 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|' or no space before spliced term $ e:num)

<example>:1:34-1:36: unexpected token '$'; expected '`(tactic|' 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 : 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 表达式中的非引号模式混合。 与普通引用一样，引用模式首先由 Lean 的解析器处理。 然后解析器的输出被编译成代码来确定是否存在匹配。 语法匹配假定匹配的语法是由 Lean 的解析器通过引用或直接在用户代码中生成的，并使用它来省略一些检查。 例如，如果在给定位置中只能出现特定关键字，则可以省略该检查。

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

原子

关键字原子（例如 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. 后跟原子的单例节点。 在许多情况下，没有必要检查特定的原子值，因为语法只允许单个关键字，并且不会执行任何检查。 如果匹配的术语的语法需要检查，则比较节点类型。

文字（例如字符串或数字文字）通过其底层字符串表示形式进行比较。 模式 `(0x15) and the quotation `(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 ::= ...
    | 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.

At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
`plainDocComment` to always treat the contents as plain text.

A plain text doc comment 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.
A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
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! (List 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.

At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
`plainDocComment` to always treat the contents as plain text.

A plain text doc comment 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.
A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
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"]