23.7. 扩展 `do` 记法🔗

宏与精译器可以用来通过新命令和新项扩展 Lean。除此之外，Lean.Parser.Term.do : termdo 记法本身也可以扩展。对 Lean.Parser.Term.do : termdo 记法的扩展会定义新的 Lean.Parser.Term.do : termdo 元素种类。宏会把新的 Lean.Parser.Term.do : termdo 元素翻译成既有的 Lean.Parser.Term.do : termdo 元素，而精译器则能访问更多信息，并在 Lean 的类型论中构造任意项。

本章介绍可用于扩展 Lean.Parser.Term.do : termdo 记法的机制。可扩展的 Lean.Parser.Term.do : termdo 记法是在 Lean 4.29.0 版本中引入的；在此之前，它并不可扩展。可扩展的 Lean.Parser.Term.do : termdo 精译器受选项 backward.do.legacy 控制，其默认值为 false：

选项

backward.do.legacy

默认值：false

使用旧版 do 精译器，而不是新的可扩展实现。

当 backward.do.legacy 为 false 时，可扩展精译器会启用。自定义 Lean.Parser.Term.do : termdo 元素精译器会扩展关于单子语法的小节中描述的脱糖过程。

23.7.1. 精译概览🔗

语法种类 doElem 表示单个 do 元素。由这些元素构成的序列则由语法种类 doSeq 表示，它构成了 Lean.Parser.Term.do : termdo 块的主体。 Lean.Parser.Term.do : termdo 的精译器会对其主体中的 doSeq 调用一个专门的精译框架，依次精译每个 doElem。这个专门框架允许序列中的每个元素修改后续元素的精译方式，也能跟踪诸如外围循环（供 Lean.Parser.Term.doBreak : doElembreak 与 Lean.Parser.Term.doContinue : doElemcontinue 使用）、通过 Lean.Parser.Term.doReturn : doElemreturn 逃离的方式，以及可变变量集合等信息。

Lean.Parser.Term.do : termdo 元素的精译与项的精译非常相似。首先，如果相关语法是一个宏，那么它会被展开。这一过程会反复进行，直到宏展开的结果不再是宏为止。接着，系统会查询一张内部表，找到与该 Lean.Parser.Term.do : termdo 元素语法种类相关联的精译过程。这张表与项精译器表分开维护，因为 Lean.Parser.Term.do : termdo 元素精译器的类型不同。如果某个 Lean.Parser.Term.do : termdo 元素仅由一个项组成，那么 Lean 解析器会把它包裹在语法种类 doExpr 中；它的精译器会调用项精译器，并确保该项具有适合当前 Lean.Parser.Term.do : termdo 块的正确类型。

23.7.2. `do` 记法中的宏🔗

宏展开发生在 Lean.Parser.Term.do : termdo 元素的精译期间。 Lean.Parser.Term.do : termdo 元素宏与项宏或命令宏在本质上并无区别；它们的差别只在于：它们是为 doElem 语法类别中的语法而定义的。

多路 if

作为嵌套 Lean.Parser.Term.doIf : doElemif 项序列的一种替代，这种“多路 Lean.Parser.Term.doIf : doElemif”把每个条件都放在同一语法层级：

syntax (name := multiIfTerm)
  "if " withPosition(
    (colGe atomic("|" (atomic(ident " : "))? term) " => " term)+
    colGe "|" " else " " => " term
  ) : term

它是缩进敏感的。它可以实现为一个递归宏，产出预期的嵌套 Lean.Parser.Term.ifif：

def mkTermIf (h? : Option Ident) (g b e : Term) : MacroM Term :=
  match h? with
  | some h => `(if $h:ident : $g then $b else $e)
  | none => `(if $g then $b else $e)

macro_rules
  | `(if | $[$h?:ident :]? $g:term => $b:term | else => $e:term) =>
      mkTermIf h? g b e
  | `(if | $[$h?:ident :]? $g:term => $b:term
         | $[$h2?:ident :]? $g2:term => $b2:term
         $[| $[$hs?:ident :]? $gs:term => $bs:term]*
         | else => $e:term) => do
      mkTermIf h? g b
        (← `(if | $[$h2?:ident :]? $g2 => $b2
                $[| $[$hs?:ident :]? $gs => $bs]*
                | else => $e))

它可以像任何其他项一样使用：

("neg", "zero", "pos")#eval
  let sign : Int → String := fun n =>
    if
      | n < 0 => "neg"
      | n = 0 => "zero"
      | else => "pos"
  (sign (-2), sign 0, sign 5)

("neg", "zero", "pos")

只要把这个宏放进 doElem 语法类别，并把多路 Lean.Parser.Term.doIf : doElemif 的每个分支从 Term 换成 doSeq，它就可以改造成 Lean.Parser.Term.do : termdo 元素。语法定义几乎完全一样；不过，Lean.Parser.Term.doIf : doElemelse 分支变成可选的了：

syntax (name := multiIf)
  "if " withPosition(
    (colGe atomic("|" (atomic(ident " : "))? term) " => " doSeq)+
    (colGe "|" " else " " => " doSeq)?
  ) : doElem

同样，提供一个辅助函数，把可选的条件假设名称附加到 Lean.Parser.Term.doIf : doElemif 上会很方便：

def mkDoIf (h? : Option Ident) (g : Term) (b : TSyntax ``doSeq)
    (els? : Option (TSyntax ``doSeq)) : MacroM (TSyntax `doElem) :=
  match h? with
  | some h =>
    `(doElem| if $h : $g then $b $[else $els?]?)
  | none =>
    `(doElem| if $g then $b $[else $els?]?)

其递归宏实现也几乎完全一样：

macro_rules
  | `(doElem| if | $[$h?:ident :]? $g:term => $b:doSeq
                   $[| else => $e:doSeq]?) =>
      mkDoIf h? g b e
  | `(doElem| if | $[$h?:ident :]? $g:term => $b:doSeq
                 | $[$h2?:ident :]? $g2:term => $b2:doSeq
                 $[| $[$hs?:ident :]? $gs:term => $bs:doSeq]*
                 $[| else => $e:doSeq]?) => do
      mkDoIf h? g b <| some
        (← `(doSeq| if | $[$h2?:ident :]? $g2 => $b2
                       $[| $[$hs?:ident :]? $gs => $bs]*
                       $[| else => $e]?))

它可以在 Lean.Parser.Term.do : termdo 中使用：

def getEven : IO { n : Nat // n % 2 = 0 ∨ n % 3 = 0} := do
  let n ← (← IO.getStdin).getLine
  let some n := n.toNat?
    | throw <| IO.userError s!"Not a Nat: {n}"
  if
    | h : n % 2 = 0 =>
      IO.println s!"{n} is even."
      return ⟨n, .inl h⟩
    | h : n % 3 = 0 =>
      IO.println s!"{n} is divisible by 3."
      return ⟨n, .inr h⟩
    | else =>
      throw <| IO.userError s!"Invalid input {n}"

在线查看 ↪

23.7.2.1. 局限性🔗

当某个扩展可以实现成宏时，通常最好就这么做。宏维护起来简单得多，而且它们还能自动继承所展开到的目标语法实现中的缺陷修复。不过，宏并不能实现所有可能的扩展：

宏无法访问可变变量集合的信息，也无法覆写它。
宏无法实现那些不能用内建控制结构表达出来的新型控制结构。
宏无法把某个 Lean.Parser.Term.do : termdo 序列放进新的上下文（例如绑定器之下），同时仍然让它在提前返回和可变变量这两方面保持为外围 Lean.Parser.Term.do : termdo 块的一部分。

在这些情况下，就可能需要定义精译器。

用宏冻结可变变量

在 Lean.Parser.Term.do : termdo 块内部，新的 Lean.Parser.Term.doLet : doElemlet 绑定不能遮蔽已有的 Lean.Parser.Term.doLet : doElemlet mut 绑定。不过，许多可变变量在初始化之后其实并不会再被修改。如果能通过去掉它们的可变性来表明这一点，往往会更方便。

目前并不存在一种现成的方式，能把某个可变变量替换成不可变变量，因此这个特性无法通过展开到某个现有 Lean.Parser.Term.do : termdo 元素的宏来实现——因为那样的元素并不能让该变量在后续块中变为不可变。不过，可以把这个操作符设计成通过展开为函数调用来引入一个作用域，在这个作用域里，可变变量是不可变的：

macro "freeze " x:ident " in " body:doSeq : doElem =>
  `(doElem| (fun $x => do $body) $x)

虽然这看起来颇有希望，但这种基于宏的方案有严重缺点。首先，得到的函数体会形成一个新的 Lean.Parser.Term.do : termdo 块。这意味着外围块中的可变变量无法被修改：

#eval Id.run do
  let mut x : Nat := 0
  x := x + 1
  let mut y := 0
  freeze x in
    Variable `y` cannot be mutated. Only variables declared using `let mut` can be mutated.
      If you did not intend to mutate but define `y`, consider using `let y` insteady := 2 * x
  return y

Variable `y` cannot be mutated. Only variables declared using `let mut` can be mutated.
      If you did not intend to mutate but define `y`, consider using `let y` instead

此外，提前出现的 Lean.Parser.Term.doReturn : doElemreturn 只会退出内部的 Lean.Parser.Term.do : termdo，而不是外围那个；其依据是它被期望返回一个 Unit（这里是宇宙多态的 PUnit）：

#eval Id.run do
  let mut x : Nat := 0
  x := x + 1
  let mut y := 0
  freeze x in
    return Type mismatch
  x
has type
  Nat
but is expected to have type
  PUnitx
  return y

Type mismatch
  x
has type
  Nat
but is expected to have type
  PUnit

在线查看 ↪

23.7.3. 精译🔗

Lean.Parser.Term.do : termdo 元素的精译发生在 DoElabM 单子中。这个单子是对 TermElabM 的封装，并额外提供了一个读取器值：Lean.Parser.Term.do : termdo 精译上下文。精译器还会接收一个额外参数：描述精译续延的信息。这个续延表示当前元素之后，整个 Lean.Parser.Term.do : termdo 块剩余的部分；其中既包含一个会精译该块剩余部分的 DoElabM 动作，也包含该项用来引用当前精译步骤结果的名字。与把精译后项返回给外围精译上下文的项精译器不同，Lean.Parser.Term.do : termdo 元素精译器会调用所提供的续延，以安排该 Lean.Parser.Term.do : termdo 块其余部分的精译。

结构体

Lean.Elab.Do.Context : Type
Lean.Elab.Do.Context : Type

do 块精译期间共享的上下文。它缓存单子信息、跟踪可变变量与控制流续延，并保存构造 pure、bind 及单子应用所需的操作。

构造子

Lean.Elab.Do.Context.mk

字段

monadInfo : Elab.Do.MonadInfo

已推断并缓存的单子信息。

mutVars : Array Elab.Do.MutVar

按声明顺序排列的可变变量。它与 mutVarDefs 保持同步；只能通过 declareMutVar / declareMutVars 插入。

mutVarDefs : Std.HashMap Name Elab.Do.MutVar

从可变变量名到其 MutVar 记录的映射；它与 mutVars 保持同步。

doBlockResultType : Expr

当前 do 块的预期类型。例如，在 for 循环的 do 块中，它可能不同于 ReturnCont.resultType。

contInfo : Elab.Do.ContInfoRef

return、break 和 continue 续延的信息引用。

deadCode : Elab.Do.CodeLiveness

当前 do 元素是否为死代码。如果它不是 .alive，elabDoElem 将发出警告。

ops : Elab.Do.DoOpsRef

构造 pure、bind 和单子应用的可插拔操作。

结构体

Lean.Elab.Do.MonadInfo : Type
Lean.Elab.Do.MonadInfo : Type

已推断出的单子及其宇宙层级信息，并缓存相应的 PUnit 表达式。

构造子

Lean.Elab.Do.MonadInfo.mk

字段

m : Expr

已推断出的单子，其类型为 Type u → Type v。

u : Level

m : Type u → Type v 中的 u。

v : Level

m : Type u → Type v 中的 v。

cachedPUnit : Expr

缓存的 PUnit 表达式。

cachedPUnitUnit : Expr

缓存的 PUnit.unit 表达式。

归纳类型

Lean.Elab.Do.CodeLiveness : Type
Lean.Elab.Do.CodeLiveness : Type

代码块是活代码还是死代码。

构造子

Lean.Elab.Do.CodeLiveness.deadSyntactically :
  Elab.Do.CodeLiveness

已推断代码在语法上不可达，因此完全不必精译。

Lean.Elab.Do.CodeLiveness.deadSemantically :
  Elab.Do.CodeLiveness

已推断代码在语义上不可达，但仍须精译以生成程序。

Lean.Elab.Do.CodeLiveness.alive : Elab.Do.CodeLiveness

代码可达，或虽不可达但系统未能证明这一点。

为避免实现中的循环依赖，Context.contInfo 与 Context.ops 字段都是在构造后再填入内容的引用。可以使用 ContInfoRef.toContInfo 与 DoOpsRef.toDoOps 取回底层数据：

不透明定义

Lean.Elab.Do.ContInfoRef.toContInfo (m : Elab.Do.ContInfoRef) :
  Elab.Do.ContInfo
Lean.Elab.Do.ContInfoRef.toContInfo
  (m : Elab.Do.ContInfoRef) :
  Elab.Do.ContInfo

从为打破实现循环依赖而使用的引用中取回控制续延信息。

结构体

Lean.Elab.Do.ContInfo : Type
Lean.Elab.Do.ContInfo : Type

有关成功、return、break 或 continue 续延的信息；使用这些续延的代码精译完毕后，才会填充它们。

构造子

Lean.Elab.Do.ContInfo.mk

字段

returnCont : Elab.Do.ReturnCont

提前 return 所使用的续延。

breakCont : Option (Elab.Do.DoElabM Expr)

当前循环的 break 续延；不在循环中时为 none。

continueCont : Option (Elab.Do.DoElabM Expr)

当前循环的 continue 续延；不在循环中时为 none。

不透明定义

Lean.Elab.Do.DoOpsRef.toDoOps (r : Elab.Do.DoOpsRef) : Elab.Do.DoOps
Lean.Elab.Do.DoOpsRef.toDoOps
  (r : Elab.Do.DoOpsRef) : Elab.Do.DoOps

从为打破实现循环依赖而使用的引用中取回 do 精译操作。

结构体

Lean.Elab.Do.DoOps : Type
Lean.Elab.Do.DoOps : Type

do 精译器所生成的 pure / bind 应用的可插拔构造器。

构造子

Lean.Elab.Do.DoOps.mk

字段

mkPureApp : Expr → Expr → Elab.Do.DoElabM Expr

构造 pure (α:=α) e : m α。

mkBindApp : Expr → Expr → Expr → Expr → Elab.Do.DoElabM Expr

构造 bind (α:=α) (β:=β) e k : m β。

isPureApp? : Expr → Option Expr

如果 e 在语法上是 pure … 应用，则返回纯值；否则返回 none。 DoElemCont.mkBindUnlessPure 用它将 e >>= pure 收缩为 e，并将 pure e >>= k 收缩为 let x := e; k x。

splitMonadApp? : Expr → Elab.TermElabM (Option (Elab.Do.MonadInfo × Expr))

匹配单子应用 m α，返回 m 的 MonadInfo 和 α。

mkMonadApp : Expr → Elab.Do.DoElabM Expr

从结果类型 α 构造 m α。

精译器通过 doElem_elab 属性与语法种类关联。它们应当具有类型 DoElab。除了精译器之外，每个通过精译器实现的自定义 Lean.Parser.Term.do : termdo 元素还必须提供控制信息。

定义

Lean.Elab.Do.DoElab : Type
Lean.Elab.Do.DoElab : Type

do 块元素精译器的类型。

它满足 elabTerm `(do $e; $rest) = elabDoElem e dec，其中 elabDoElem e · 是 do 元素 e 的精译器，而 dec 是描述块中剩余部分 rest 如何精译的 DoElemCont。

属性do 元素精译器

attr ::= ...
    | doElem_elab

为给定的语法结点种类注册一个 do 元素精译器。

do 元素精译器应具有 DoElab 类型（即 Lean.Syntax → DoElemCont → DoElabM Expr）：它应以给定语法结点种类的语法和一个 DoElemCont 为参数，并生成一个表达式。

精译 do 块 do e; rest 时，会以 e 的语法和表示 rest 的 DoElemCont 调用 e 的精译器。

通常应优先使用 elab_rules 和 elab 命令，而不是直接使用此属性。

此外，也可以使用 Lean.Parser.Command.elab_rules : commandelab_rules 来同时定义精译器并把它关联到语法上。正如 elab_rules : term <= ty 会把期望类型绑定到 ty 一样，elab_rules : doElem <= dec 会把续延绑定到 dec。

正如项精译器可以通过调用 elabTerm 等函数，递归地对其子项再次调用精译一样，Lean.Parser.Term.do : termdo 元素精译器也可以精译嵌套的 Lean.Parser.Term.do : termdo 元素或由 Lean.Parser.Term.do : termdo 元素组成的序列。要精译单个 Lean.Parser.Term.do : termdo 元素，请调用 elabDoElem。要精译非空数组中的一组 Lean.Parser.Term.do : termdo 元素，请调用 elabDoElems1。要精译一整个 Lean.Parser.Term.do : termdo 元素序列，请调用 elabDoSeq。

不透明定义

Lean.Elab.Do.elabDoElem (stx : DoElem) (cont : Elab.Do.DoElemCont)
  (catchExPostpone : Bool := true) : Elab.Do.DoElabM Expr
Lean.Elab.Do.elabDoElem (stx : DoElem)
  (cont : Elab.Do.DoElemCont)
  (catchExPostpone : Bool := true) :
  Elab.Do.DoElabM Expr

精译单个 do 元素 stx，并以 cont 表示其余 do 块。它会先处理死代码、宏展开与嵌套动作，再依语法结点种类调用已注册的元素精译器；默认捕获精译延后异常并安排重试。

不透明定义

Lean.Elab.Do.elabDoSeq (doSeq : DoSeq) (cont : Elab.Do.DoElemCont)
  (catchExPostpone : Bool := true) : Elab.Do.DoElabM Expr
Lean.Elab.Do.elabDoSeq (doSeq : DoSeq)
  (cont : Elab.Do.DoElemCont)
  (catchExPostpone : Bool := true) :
  Elab.Do.DoElabM Expr

精译完整的 doSeq，并把结果交给 cont。默认捕获精译延后异常、恢复精译状态，并把整个序列安排为稍后重试。

不透明定义

Lean.Elab.Do.elabDoElems1 (doElems : Array DoElem)
  (cont : Elab.Do.DoElemCont) (catchExPostpone : Bool := true) :
  Elab.Do.DoElabM Expr
Lean.Elab.Do.elabDoElems1
  (doElems : Array DoElem)
  (cont : Elab.Do.DoElemCont)
  (catchExPostpone : Bool := true) :
  Elab.Do.DoElabM Expr

从右向左为非空 do 元素数组构造续延链并精译它；若数组为空则报错。默认让每个元素捕获并处理精译延后异常。

23.7.3.1. 单子操作🔗

精译框架提供了若干辅助函数，让构造当前单子及其操作的应用变得更方便也更高效。

定义

Lean.Elab.Do.mkMonadApp (resultType : Expr) : Elab.Do.DoElabM Expr
Lean.Elab.Do.mkMonadApp
  (resultType : Expr) :
  Elab.Do.DoElabM Expr

从 α 构造 m α。

定义

Lean.Elab.Do.mkPureApp (α e : Expr) : Elab.Do.DoElabM Expr
Lean.Elab.Do.mkPureApp (α e : Expr) :
  Elab.Do.DoElabM Expr

表达式 pure (α:=α) e。

定义

Lean.Elab.Do.mkBindApp (α β e k : Expr) : Elab.Do.DoElabM Expr
Lean.Elab.Do.mkBindApp (α β e k : Expr) :
  Elab.Do.DoElabM Expr

表达式 Bind.bind (α:=α) (β:=β) e k。

定义

Lean.Elab.Do.mkPUnitUnit : Elab.Do.DoElabM Expr
Lean.Elab.Do.mkPUnitUnit :
  Elab.Do.DoElabM Expr

缓存的 PUnit.unit 表达式。

23.7.3.2. 续延🔗

Lean.Parser.Term.do : termdo 精译续延由一个等待当前元素结果的精译器，以及若干元数据（例如该结果期望具有的类型）共同组成。

结构体

Lean.Elab.Do.DoElemCont : Type
Lean.Elab.Do.DoElemCont : Type

精译 do 块 do $e; $rest 会产生调用 elabTerm `(do $e; $rest) = elabDoElem e dec，其中 elabDoElem e · 是 do 元素 e 的精译器，而 dec 是描述块中剩余部分 rest 如何精译的 DoElemCont。

如果 e 的语义会恢复其续延 rest，则它的精译器必须把结果绑定到 resultName，确保结果具有 resultType 类型，然后使用 dec 精译 rest。

显然，对于项元素 e : m α，结果类型是 α。较微妙的是，对于绑定元素 let x := e 或 let x ← e，结果类型是 PUnit，与被绑定变量 x 的类型无关。

示例：

return 丢弃续延；return x; pure () 精译为 pure x。
let x ← e; rest x 精译为 e >>= fun x => rest x。
let x := 3; let y ← (let x ← e); rest x 精译为 let x := 3; e >>= fun x_1 => let y := (); rest x，随后立即进行 ζ 约简，得到 let x := 3; e >>= fun x_1 => rest x。
one; two 精译为 one >>= fun (_ : PUnit) => two；如果 one 的类型不是 PUnit，则会报错。

构造子

Lean.Elab.Do.DoElemCont.mk

字段

resultName : Name

单子结果变量的名字。

resultType : Expr

单子结果的类型。

k : Elab.Do.DoElabM Expr

用于精译块中 rest 的续延。它假定 do 块的结果已经以正确类型绑定到 resultName（即 resultType，但依赖 match 可能会细化该类型）。

kind : Elab.Do.DoElemContKind

是否允许多次生成续延的代码，例如在 match 或 if 的不同分支中生成。

归纳类型

Lean.Elab.Do.DoElemContKind : Type
Lean.Elab.Do.DoElemContKind : Type

do 元素的续延是否可以复制。指定 nonDuplicable 始终安全；duplicable 允许更多优化。

构造子

Lean.Elab.Do.DoElemContKind.nonDuplicable :
  Elab.Do.DoElemContKind

续延不可复制，必要时应通过连接点共享。

Lean.Elab.Do.DoElemContKind.duplicable :
  Elab.Do.DoElemContKind

续延可以安全地在多个控制流分支中精译。

许多精译器都要求续延对其结果期待某个特定类型。例如，精译器在不返回结果时，其结果类型往往应为 Unit。尽早检查这一类型，通常能得到更好的错误信息：

定义

Lean.Elab.Do.DoElemCont.ensureUnit (dec : Elab.Do.DoElemCont) :
  Elab.Do.DoElabM Elab.Do.DoElemCont
Lean.Elab.Do.DoElemCont.ensureUnit
  (dec : Elab.Do.DoElemCont) :
  Elab.Do.DoElabM Elab.Do.DoElemCont

给定续延 dec，返回一个从 dec 派生且结果类型为 PUnit 的续延。如果 dec 的结果类型已经是 PUnit，则直接返回 dec。否则记录错误，并返回一个以 sorry 为结果调用 dec 的新续延。

定义

Lean.Elab.Do.DoElemCont.ensureUnitAt (dec : Elab.Do.DoElemCont)
  (ref : Syntax) : Elab.Do.DoElabM Elab.Do.DoElemCont
Lean.Elab.Do.DoElemCont.ensureUnitAt
  (dec : Elab.Do.DoElemCont)
  (ref : Syntax) :
  Elab.Do.DoElabM Elab.Do.DoElemCont

给定续延 dec 和引用 ref，返回一个从 dec 派生且结果类型为 PUnit 的续延。如果 dec 的结果类型已经是 PUnit，则直接返回 dec。否则记录错误，并返回一个以 sorry 为结果调用 dec 的新续延。错误报告在 ref 处。

定义

Lean.Elab.Do.DoElemCont.ensureHasTypeAt (dec : Elab.Do.DoElemCont)
  (ref : Syntax) (elementType : Expr) :
  Elab.Do.DoElabM Elab.Do.DoElemCont
Lean.Elab.Do.DoElemCont.ensureHasTypeAt
  (dec : Elab.Do.DoElemCont)
  (ref : Syntax) (elementType : Expr) :
  Elab.Do.DoElabM Elab.Do.DoElemCont

给定续延 dec、引用 ref 和元素结果类型 elementType，返回一个从 dec 派生且结果类型为 elementType 的续延。如果 dec 的结果类型已经是 elementType，则直接返回 dec。若二者不定义相等，则记录错误，并返回一个以 sorry 为结果调用 dec 的新续延。错误报告在 ref 处。

调用续延，就是向它提供当前 Lean.Parser.Term.do : termdo 元素的结果。主要有三种方式可以做到这一点。 DoElemCont.continueWithUnit 会确保续延期待的是 Unit，然后再调用它。 DoElemCont.elabAsSyntacticallyDeadCode 会在一个断言代码不可达的上下文中调用续延，这通常会导致续延不生成任何代码；如果那里确实有代码，还会向用户发出警告。 DoElemCont.mkBindUnlessPure 负责把 Lean.Parser.Term.do : termdo 记法标准地脱糖为对 bind 的应用；当某个 Lean.Parser.Term.do : termdo 元素只是一项且该项具有单子类型时，它就用来在精译后调用续延；其中还包含一项优化：会把包裹在 pure 外面的 bind 替换为 Lean.Parser.Term.let : termlet 绑定。

定义

Lean.Elab.Do.DoElemCont.continueWithUnit (dec : Elab.Do.DoElemCont) :
  Elab.Do.DoElabM Expr
Lean.Elab.Do.DoElemCont.continueWithUnit
  (dec : Elab.Do.DoElemCont) :
  Elab.Do.DoElabM Expr

返回 let $k.resultName : PUnit := PUnit.unit; $(← k.k)，并确保 k.k 的结果类型是 PUnit，然后立即对这个 let 进行 ζ 约简。

定义

Lean.Elab.Do.DoElemCont.elabAsSyntacticallyDeadCode
  (dec : Elab.Do.DoElemCont) : Elab.Do.DoElabM Unit
Lean.Elab.Do.DoElemCont.elabAsSyntacticallyDeadCode
  (dec : Elab.Do.DoElemCont) :
  Elab.Do.DoElabM Unit

将 deadCode 标志设为 deadSyntactically 来精译 DoElemCont，以便发出警告。

定义

Lean.Elab.Do.DoElemCont.mkBindUnlessPure (dec : Elab.Do.DoElemCont)
  (e : Expr) : Elab.Do.DoElabM Expr
Lean.Elab.Do.DoElemCont.mkBindUnlessPure
  (dec : Elab.Do.DoElemCont) (e : Expr) :
  Elab.Do.DoElabM Expr

返回 $e >>= fun ($dec.resultName : $dec.resultType) => $(← dec.k)；如果 $(← dec.k) 是 pure $dec.resultName，或 e 是某个 pure 计算，则消去此绑定。

调用续延

一种内建语法 Lean.Parser.Term.InternalSyntax.doSkipskip 的变体——它等价于 pure ()——可以用一个精译器来实现：它立即用 Unit 调用自己的续延。为了得到更好的错误信息，它还会断言该续延期望的结果类型是 Unit。

syntax (name := doNothing) "nothing" : doElem

@[doElem_elab doNothing]
def elabDoNothing : DoElab := fun stx dec => do
  let dec ← dec.ensureUnitAt stx
  dec.continueWithUnit

为了给控制结构生成代码，Lean.Parser.Term.do : termdo 元素精译框架需要知道每个元素可能执行哪些副作用。这些控制信息通过 doElem_control_info 属性注册。由于 doNothing : doElemnothing 既不会修改可变变量，也不会抛出异常、提前终止循环，或做出任何其他动作，因此它的控制信息就是 ControlInfo.pure。

@[doElem_control_info doNothing]
def doNothing.control : ControlInfoHandler := fun _ => do return .pure

它确实等价于 pure ()：

some ()#eval show Option Unit from do nothing

some ()

在线查看 ↪

用 elab_rules 精译 do 元素

作为 doNothing : doElemnothing 的另一种实现版本——它等价于内建语法 Lean.Parser.Term.InternalSyntax.doSkipskip——可以使用 Lean.Parser.Command.elab_rules : commandelab_rules，作为带 doElem_elab 属性的显式精译器的替代方案。

syntax (name := doNothing) "nothing" : doElem

elab_rules : doElem <= dec
  | `(doElem|nothing%$tk) => do
    let dec ← dec.ensureUnitAt tk
    dec.continueWithUnit

@[doElem_control_info doNothing]
def doNothing.control : ControlInfoHandler := fun _ => do return .pure

它等价于 pure ()：

some ()#eval show Option Unit from do nothing

some ()

在线查看 ↪

由于精译器是显式调用其续延，而不是简单返回一个值，因此它可以控制精译的上下文。尤其是，它可以使用 withReader 修改上下文，也可以多次调用续延，以支持带分支的控制结构。为了防止代码大小爆炸，续延会在 DoElemCont.kind 中跟踪自己是否可能被精译多次。如果一个续延可能被多次调用，那么它就是 可复制 的；否则它就是 不可复制 的。不可复制的续延可以通过 DoElemCont.withDuplicableCont 转换成可复制的续延。

定义

Lean.Elab.Do.DoElemCont.withDuplicableCont
  (nondupDec : Elab.Do.DoElemCont) (callerInfo : Elab.Do.ControlInfo)
  (caller : Elab.Do.DoElemCont → Elab.Do.DoElabM Expr) :
  Elab.Do.DoElabM Expr
Lean.Elab.Do.DoElemCont.withDuplicableCont
  (nondupDec : Elab.Do.DoElemCont)
  (callerInfo : Elab.Do.ControlInfo)
  (caller :
    Elab.Do.DoElemCont →
      Elab.Do.DoElabM Expr) :
  Elab.Do.DoElabM Expr

以 dec 的可复制代理调用 caller。当代理被精译多次时，会引入一个连接点，使 dec 只精译一次，以填充该连接点的右侧。

这适用于 if 和 match 等控制流构造：其中多个尾调用分支共享同一续延。

不可达代码无需精译。当某个 Lean.Parser.Term.do : termdo 元素的精译器已经检测到续延精译的结果不可达时，它可以直接返回自己的结果项，而不是把它交给精译续延。它应当构造一个足以证明程序可以在此放弃执行的项，例如对 False.elim 的调用。在返回这个项之前，它应当对续延调用 DoElemCont.elabAsSyntacticallyDeadCode，以警告用户：续延原本会精译的那段代码是不可达的。

不可达代码

操作符 doAbsurd : doElemabsurd 在给出 False 的证明时，会把代码标记为不可达；这说明当前局部上下文在逻辑上是不一致的。如果传入了证明，它就使用该证明；否则，它会尝试一些自动化手段。

syntax (name := doAbsurd) "absurd" (" by " tacticSeq)? : doElem

由于 doAbsurd : doElemabsurd 永远不会返回，而且控制流也不可能越过它继续执行，因此它的控制信息会把 numRegularExits 设为 0，并把 noFallthrough 设为 true：

@[doElem_control_info doAbsurd]
def inferAbsurd : ControlInfoHandler := fun _ =>
  return { numRegularExits := 0, noFallthrough := true }

精译器首先提取证明语法；如果未提供，就回退到默认值。然后，它会把该证明精译为 False 的一个证明。如果成功，它就会用 DoElemCont.elabAsSyntacticallyDeadCode 把剩余的 Lean.Parser.Term.do : termdo 序列标记为死代码，并把 False.elim 作为结果项直接返回，而不是交给续延。 False.elim 会接收该项所期望具有的类型；这个类型通过 Lean.Elab.Do.mkMonadApp 与结果类型共同确定。这里必须使用 Do.Context.doBlockResultType，而不是续延的结果类型，因为效应提升可能已经在局部修改了该类型。

@[doElem_elab doAbsurd]
def elabAbsurd : DoElab := fun stx dec => do
  let `(doElem| absurd $[by $tac?]?) := stx
    | throwUnsupportedSyntax
  let proofStx : Term ←
    if let some tac := tac? then
      `(by $tac)
    else
      `(by first | contradiction | grind)
  let proof ← elabTermEnsuringType proofStx (mkConst ``False)
  dec.elabAsSyntacticallyDeadCode
  let ty ← mkMonadApp (← read).doBlockResultType
  return (← Meta.mkAppOptM ``False.elim #[some ty, some proof])

doAbsurd : doElemabsurd 可以利用嵌套条件分支中积累的信息，断定 Lean.Parser.Term.doIf : doElemelse 子句不可达：

("small", "medium", "large")#eval show Id (String × String × String) from do
  let classify : Nat → String := fun n => Id.run do
    if n < 3 then return "small"
    else if h1 : n < 10 then return "medium"
    else if h2 : n ≥ 10 then return "large"
    else absurd
  return (classify 1, classify 5, classify 99)

由于调用了 DoElemCont.elabAsSyntacticallyDeadCode，位于 doAbsurd : doElemabsurd 之后的步骤会收到死代码警告：

def xs := #[1, 3, 5]
theorem xs_all_odd : ∀ x, x ∈ xs → x % 2 = 1 := by⊢ ∀ (x : Nat), x ∈ xs → x % 2 = 1
  simp [xs]All goals completed! 🐙

100#eval show Id Nat from do
  for h : n in 0...5 do
    let k := n * 2
    if h' : k ∈ xs then
      absurd by grind [xs_all_odd]All goals completed! 🐙
      This `do` element and its control-flow region are dead code. Consider removing it.return k
  pure 100

This `do` element and its control-flow region are dead code. Consider removing it.

不过，它确实可以成功运行：

在线查看 ↪

23.7.3.3. 控制流：`return`、`break` 与 `continue`🔗

Lean.Parser.Term.do : termdo 记法支持三种非局部跳转指令：Lean.Parser.Term.doReturn : doElemreturn 用于提前终止整个 Lean.Parser.Term.do : termdo 块；Lean.Parser.Term.doBreak : doElembreak 用于提前终止循环；Lean.Parser.Term.doContinue : doElemcontinue 用于提前终止循环中的单次迭代。 Lean.Parser.Term.doReturn : doElemreturn 总是允许出现，而 Lean.Parser.Term.doBreak : doElembreak 与 Lean.Parser.Term.doContinue : doElemcontinue 只在循环体内部合法。在精译过程中，这三种跳转都由续延来表示。

定义

Lean.Elab.Do.getReturnCont : Elab.Do.DoElabM Elab.Do.ReturnCont
Lean.Elab.Do.getReturnCont :
  Elab.Do.DoElabM Elab.Do.ReturnCont

从当前 do 精译上下文取得 return 续延。

定义

Lean.Elab.Do.getBreakCont :
  Elab.Do.DoElabM (Option (Elab.Do.DoElabM Expr))
Lean.Elab.Do.getBreakCont :
  Elab.Do.DoElabM
    (Option (Elab.Do.DoElabM Expr))

从当前 do 精译上下文取得 break 续延；不在循环中时返回 none。

定义

Lean.Elab.Do.getContinueCont :
  Elab.Do.DoElabM (Option (Elab.Do.DoElabM Expr))
Lean.Elab.Do.getContinueCont :
  Elab.Do.DoElabM
    (Option (Elab.Do.DoElabM Expr))

从当前 do 精译上下文取得 continue 续延；不在循环中时返回 none。

这三个续延会借助辅助函数 enterLoopBody 安装到上下文中。

定义

Lean.Elab.Do.enterLoopBody {α : Type}
  (breakCont continueCont : Elab.Do.DoElabM Expr)
  (returnCont : Elab.Do.ReturnCont) (body : Elab.Do.DoElabM α) :
  Elab.Do.DoElabM α
Lean.Elab.Do.enterLoopBody {α : Type}
  (breakCont continueCont :
    Elab.Do.DoElabM Expr)
  (returnCont : Elab.Do.ReturnCont)
  (body : Elab.Do.DoElabM α) :
  Elab.Do.DoElabM α

准备好用于精译循环体的上下文。这包括设置返回续延、中断续延、继续续延，以及循环体中 do 块已改变的结果类型。

单次迭代循环

单次迭代循环 doOnce : doElemonce 会执行其主体一次；如果在主体中遇到 Lean.Parser.Term.doBreak : doElembreak 或 Lean.Parser.Term.doContinue : doElemcontinue，就会跳到循环末尾：

syntax (name := doOnce) "once " doSeq : doElem

它的控制信息基于其主体的控制信息。 doOnce : doElemonce 自身永远不会再向外 break 或 continue，因为它会在自己的主体内部处理 Lean.Parser.Term.doBreak : doElembreak 和 Lean.Parser.Term.doContinue : doElemcontinue；因此它会把 breaks 和 continues 设为 false。 numRegularExits 表示控制流到达 doOnce : doElemonce 之后那段代码的次数。主体的正常落空、Lean.Parser.Term.doBreak : doElembreak 和 Lean.Parser.Term.doContinue : doElemcontinue 都会把控制流转移到循环末尾，因此控制流离开一个 doOnce : doElemonce 的次数至多为一次。因此，只要主体能以这些方式中的任意一种退出，numRegularExits 就是 1；否则就是 0，此时还会设置 noFallthrough。

@[doElem_control_info doOnce]
def inferOnce : ControlInfoHandler := fun stx => do
  let `(doElem| once $body) := stx | throwUnsupportedSyntax
  let bodyInfo ← InferControlInfo.ofSeq body
  let exits :=
    bodyInfo.numRegularExits > 0 ||
    bodyInfo.breaks ||
    bodyInfo.continues
  return { bodyInfo with
    breaks := false
    continues := false
    numRegularExits := if exits then 1 else 0
    noFallthrough := !exits
  }

doOnce : doElemonce 的实际精译器使用 enterLoopBody，把该精译器的整体续延与主体内部的 Lean.Parser.Term.doBreak : doElembreak 和 Lean.Parser.Term.doContinue : doElemcontinue 续延关联起来。由于精译后的主体可能从多个位置抵达该续延，精译器会对这些使用进行计数。主体的控制信息并不说明 Lean.Parser.Term.doBreak : doElembreak 与 Lean.Parser.Term.doContinue : doElemcontinue 可能被调用多少次，因此这里把它们都安全地近似为两个出口，以确保只要二者之一被使用，续延就会被复制。近似后的总使用次数会传给 DoElemCont.withDuplicableCont；当使用次数大于一时，它会共享续延而不是在每次使用处都复制它，从而避免代码爆炸。这里直接根据主体计算这个次数，因为控制信息处理器报告的值最多只有 1，并不能反映内部的实际使用次数。

@[doElem_elab doOnce]
def elabOnce : DoElab := fun stx dec => do
  let `(doElem| once $body) := stx | throwUnsupportedSyntax
  let dec ← dec.ensureUnit
  let bodyInfo ← InferControlInfo.ofSeq body
  let numRegularExits :=
    bodyInfo.numRegularExits +
    (if bodyInfo.breaks then 2 else 0) +
    (if bodyInfo.continues then 2 else 0)
  dec.withDuplicableCont { bodyInfo with numRegularExits } fun dec => do
    let returnCont ← getReturnCont
    let exitCont := dec.continueWithUnit
    enterLoopBody exitCont exitCont returnCont do
      elabDoSeq body dec

doOnce : doElemonce 可用于终止某个计算片段，而不会像 Lean.Parser.Term.doReturn : doElemreturn 那样终止整个 Lean.Parser.Term.do : termdo 块：

2#eval show Id Nat from do
  let mut x := 0
  once
    x := x + 2
    if x % 2 = 0 then break
    x := 0
  return x

在线查看 ↪

23.7.3.4. 控制信息🔗

除了精译器之外，自定义 Lean.Parser.Term.do : termdo 元素还必须提供 控制信息。这描述了自定义元素如何与外围控制结构和可变变量交互。控制信息使 Lean 能够生成合适的代码；特别是，它让 DoElemCont.withDuplicableCont 能分析续延将要精译的代码，从而改进生成结果。控制信息之所以与精译器分离，是因为精译器需要在真正精译之前分析子元素的语法，才能知道应当如何组织自己的续延。 自定义 Lean.Parser.Term.do : termdo 元素必须提供准确的控制信息。错误的控制信息可能导致错误的代码生成。

属性do 元素控制信息

attr ::= ...
    | doElem_control_info

为给定的 doElem 语法结点种类注册一个 ControlInfo 推断处理器。

处理器应具有 ControlInfoHandler 类型（即 DoElem → TermElabM ControlInfo）。对于纯处理器，请使用 fun stx => return ControlInfo.pure。

定义

Lean.Elab.Do.ControlInfoHandler : Type
Lean.Elab.Do.ControlInfoHandler : Type

从 doElem 语法推断 ControlInfo 的处理器。用 @[doElem_control_info parserName] 注册。

如果某个 Lean.Parser.Term.do : termdo 元素既不重新赋值变量，也不会提前返回或终止执行，那么处理器可以返回 ControlInfo.pure。如果它表示一段没有常规出口且也没有其他控制效应的代码，那么处理器可以返回 ControlInfo.empty；否则，应把 ControlInfo.numRegularExits 设为 0，把 ControlInfo.noFallthrough 设为 true，同时记录任何提前返回、重新赋值或循环终止行为。

结构体

Lean.Elab.Do.ControlInfo : Type
Lean.Elab.Do.ControlInfo : Type

表示 do 块具有哪些控制效应的信息。

各字段按性质分为：

breaks、continues、returnsEarly 和 reassigns 属于语法层面：当且仅当相应构造出现在块源代码的任意位置时，它们才为 true / 非空，与该构造在语义上是否可达无关。下游精译器必须假定每个这样的语法效应都可能发生，因为精译器会访问每一个 do 元素（只有顶层 return/break/continue 会通过 elabAsSyntacticallyDeadCode 短路）。
numRegularExits 也属于语法层面：它是块在精译所得表达式中接入外围续延的次数。 withDuplicableCont 将它读作连接点复制的触发条件（> 1）。
noFallthrough = true 断言外围序列中的下一个 do 元素在语义上无关（控制绝不会落入其中）。noFallthrough = false 不作任何断言。当此字段为 true 时，会在下一个元素上发出死代码警告。

不变量：numRegularExits = 0 → noFallthrough。其逆命题不成立。

构造子

Lean.Elab.Do.ControlInfo.mk

字段

breaks : Bool

do 块在语法上包含 break。

continues : Bool

do 块在语法上包含 continue。

returnsEarly : Bool

do 块在语法上包含提前 return。

numRegularExits : Nat

块在精译所得表达式中接入外围续延的次数。 withDuplicableCont 用它判断是否引入连接点（> 1）。

noFallthrough : Bool

为 true 时，断言外围序列中的下一个 do 元素在语义上无关（控制绝不会落入其中）。 false 不作任何断言。

reassigns : NameSet

do 块中某处在语法上被重新赋值的变量。

定义

Lean.Elab.Do.ControlInfo.pure : Elab.Do.ControlInfo
Lean.Elab.Do.ControlInfo.pure :
  Elab.Do.ControlInfo

ControlInfo.sequence 的左单位元：描述总会正常落入后续代码、且只有一个常规出口的元素的 ControlInfo。

定义

Lean.Elab.Do.ControlInfo.empty : Elab.Do.ControlInfo
Lean.Elab.Do.ControlInfo.empty :
  Elab.Do.ControlInfo

ControlInfo.alternative 的单位元：描述完全没有任何分支的块的 ControlInfo（因此没有常规出口，且下一个元素显然不可达）。

如果某个 Lean.Parser.Term.do : termdo 元素自身又包含其他 Lean.Parser.Term.do : termdo 元素，那么它可以使用组合子 ControlInfo.sequence 和 ControlInfo.alternative 来合并其子元素的控制信息。 ControlInfo.sequence 用于顺序步骤，ControlInfo.alternative 用于合并控制流分支。

定义

Lean.Elab.Do.ControlInfo.sequence (a b : Elab.Do.ControlInfo) :
  Elab.Do.ControlInfo
Lean.Elab.Do.ControlInfo.sequence
  (a b : Elab.Do.ControlInfo) :
  Elab.Do.ControlInfo

序列 a; b 的 ControlInfo：效应标志取并集，常规出口就是 b 的常规出口，并且当且仅当两部分都能落入后续代码时，该序列才会落入后续代码。

定义

Lean.Elab.Do.ControlInfo.alternative (a b : Elab.Do.ControlInfo) :
  Elab.Do.ControlInfo
Lean.Elab.Do.ControlInfo.alternative
  (a b : Elab.Do.ControlInfo) :
  Elab.Do.ControlInfo

分支 a | b 的 ControlInfo：效应标志取并集，常规出口数相加，并且当且仅当至少一个分支能落入后续代码时，该选择结构才会落入后续代码。

一般来说，应当使用 inferControlInfoElem 或 inferControlInfoSeq 来计算控制信息。

定义

Lean.Elab.Do.inferControlInfoElem (doElem : DoElem) :
  Elab.TermElabM Elab.Do.ControlInfo
Lean.Elab.Do.inferControlInfoElem
  (doElem : DoElem) :
  Elab.TermElabM Elab.Do.ControlInfo

推断单个 do 元素的 ControlInfo。

定义

Lean.Elab.Do.inferControlInfoSeq (doSeq : DoSeq) :
  Elab.TermElabM Elab.Do.ControlInfo
Lean.Elab.Do.inferControlInfoSeq
  (doSeq : DoSeq) :
  Elab.TermElabM Elab.Do.ControlInfo

推断 doSeq 的 ControlInfo。

在某些高级情形下，可能需要使用 Lean.Elab.Do.InferControlInfo 中的某个函数：

不透明定义

Lean.Elab.Do.InferControlInfo.ofElem (stx : DoElem) :
  Elab.TermElabM Elab.Do.ControlInfo
Lean.Elab.Do.InferControlInfo.ofElem
  (stx : DoElem) :
  Elab.TermElabM Elab.Do.ControlInfo

递归推断单个 doElem 的 ControlInfo。它先展开宏，再按内建 do 元素的语法形式分析；对于自定义语法，则依次尝试通过 @[doElem_control_info ...] 注册的处理器。

不透明定义

Lean.Elab.Do.InferControlInfo.ofSeq (stx : DoSeq) :
  Elab.TermElabM Elab.Do.ControlInfo
Lean.Elab.Do.InferControlInfo.ofSeq
  (stx : DoSeq) :
  Elab.TermElabM Elab.Do.ControlInfo

依次推断 doSeq 中每个元素的 ControlInfo，并用 ControlInfo.sequence 按顺序组合它们。

不透明定义

Lean.Elab.Do.InferControlInfo.ofOptionSeq (stx? : Option DoSeq) :
  Elab.TermElabM Elab.Do.ControlInfo
Lean.Elab.Do.InferControlInfo.ofOptionSeq
  (stx? : Option DoSeq) :
  Elab.TermElabM Elab.Do.ControlInfo

如果可选序列是 none，则返回纯 ControlInfo；否则推断其中 doSeq 的控制信息。

不透明定义

Lean.Elab.Do.InferControlInfo.ofLetOrReassign (reassigned : Array Ident)
  (rhs? : Option DoElem)
  (otherwise? body? : Option (TSyntax `Lean.Parser.Term.doSeqIndent)) :
  Elab.TermElabM Elab.Do.ControlInfo
Lean.Elab.Do.InferControlInfo.ofLetOrReassign
  (reassigned : Array Ident)
  (rhs? : Option DoElem)
  (otherwise? body? :
    Option
      (TSyntax
        `Lean.Parser.Term.doSeqIndent)) :
  Elab.TermElabM Elab.Do.ControlInfo

推断 let、模式绑定或重新赋值的控制信息：分别推断可选右侧、模式匹配失败分支与后续主体，将右侧同“主体或失败分支”的选择顺序组合，并记录 reassigned 中所有标识符。

不透明定义

Lean.Elab.Do.InferControlInfo.ofLetOrReassignArrow (reassignment : Bool)
  (decl :
    TSyntax [`Lean.Parser.Term.doIdDecl, `Lean.Parser.Term.doPatDecl]) :
  Elab.TermElabM Elab.Do.ControlInfo
Lean.Elab.Do.InferControlInfo.ofLetOrReassignArrow
  (reassignment : Bool)
  (decl :
    TSyntax
      [`Lean.Parser.Term.doIdDecl,
        `Lean.Parser.Term.doPatDecl]) :
  Elab.TermElabM Elab.Do.ControlInfo

推断使用 ← 的标识符声明或模式声明的控制信息；reassignment 指明该声明是重新赋值而非新绑定，并据此收集被重新赋值的标识符。

23.7.3.5. 可变变量🔗

结构体

Lean.Elab.Do.MutVar : Type
Lean.Elab.Do.MutVar : Type

do 块中由 let mut 声明的可变变量。

构造子

Lean.Elab.Do.MutVar.mk

字段

ident : Ident

let mut 声明中的标识符。

baseId : FVarId

let mut 所产生的初始绑定的 FVarId。

每个可变变量都至少对应一个精译后的变量（Expr.fvar）。这些精译后的变量存在于一个跟踪其用户可见名称的局部上下文中。变量修改通过一个遮蔽性的 Lean.Parser.Term.let : termlet 绑定来实现，随后 Lean.Parser.Term.do : termdo 块中的步骤会在这样一个上下文中被精译：在该上下文里，这个遮蔽性的 Lean.Parser.Term.let : termlet 就是该变量用户可见名称所对应的绑定。使用标准精译辅助函数 Lean.Meta.getFVarFromUserName 和 Lean.Meta.getLocalDeclFromUserName，可以取回与某个用户名关联的局部变量；使用 TSyntax.getId 则可把 Ident 转换成可供查找的用户名。

当某个可变变量通过 Lean.Parser.Term.doLet : doElemlet mut 建立时，会创建一个 Lean.Parser.Term.let : termlet 绑定来表示它，并把初始变量的绑定标识符与 Expr.fvar 加入围绕续延所使用的上下文；这个续延会在 withReader 下被调用，以便加入新变量。在建立该 Lean.Parser.Term.let : termlet 绑定之后，使用 declareMutVar 来注册一个可变变量，或注册它们组成的数组。

定义

Lean.Elab.Do.declareMutVar {α : Type} (x : Ident)
  (k : Elab.Do.DoElabM α) : Elab.Do.DoElabM α
Lean.Elab.Do.declareMutVar {α : Type}
  (x : Ident) (k : Elab.Do.DoElabM α) :
  Elab.Do.DoElabM α

将给定名称注册为一个 mut 变量。

定义

Lean.Elab.Do.declareMutVars {α : Type} (xs : Array Ident)
  (k : Elab.Do.DoElabM α) : Elab.Do.DoElabM α
Lean.Elab.Do.declareMutVars {α : Type}
  (xs : Array Ident)
  (k : Elab.Do.DoElabM α) :
  Elab.Do.DoElabM α

将给定的各个名称注册为 mut 变量。

若要确保某个标识符指向的是可变变量，请使用 throwUnlessMutVarDeclared：

定义

Lean.Elab.Do.throwUnlessMutVarDeclared (x : Ident) :
  Elab.Do.DoElabM Unit
Lean.Elab.Do.throwUnlessMutVarDeclared
  (x : Ident) : Elab.Do.DoElabM Unit

如果给定名称不是已声明的 mut 变量，则抛出错误。

定义

Lean.Elab.Do.throwUnlessMutVarsDeclared (xs : Array Ident) :
  Elab.Do.DoElabM Unit
Lean.Elab.Do.throwUnlessMutVarsDeclared
  (xs : Array Ident) :
  Elab.Do.DoElabM Unit

如果给定的各个名称不是已声明的 mut 变量，则抛出错误。

跟踪可变变量

新语法 dbgMut : doElemdbg_mut 会跟踪所有可变变量的当前值。

syntax (name := dbgMut) "dbg_mut" : doElem

@[doElem_elab dbgMut] def elabDbgMut : DoElab := fun _stx cont => do
  let ctx ← readThe Do.Context
  let parts : Array Term ← ctx.mutVars.mapM fun (x : MutVar) => do
    let nameLit := x.getId.simpMacroScopes.toString
    `(term| s!"{$(quote nameLit)} = {repr $(x.ident)}")
  let msg ← `(term| String.intercalate ", " [$parts,*])
  elabDoElem (← `(doElem| dbg_trace $msg)) cont

dbgMut : doElemdbg_mut 没有任何值得特别记录的控制信息。

@[doElem_control_info dbgMut]
def dbgMut.control : ControlInfoHandler := fun _ => do return .pure

跟踪一个计算 Fibonacci 数的循环，可以显示所有中间状态：

x = 1, y = 1
x = 1, y = 2
x = 2, y = 3
x = 3, y = 5
x = 5, y = 8
#eval show IO Unit from do
  let mut x := 1
  let mut y := 1
  for _ in 0...5 do
    let z := y
    dbg_mut
    y := x + y
    x := z

x = 1, y = 1
x = 1, y = 2
x = 2, y = 3
x = 3, y = 5
x = 5, y = 8

在线查看 ↪

用于可变变量的内建精译器会处理许多细微细节，例如把生成出的每一个可变变量 Lean.Parser.Term.let : termlet 绑定注册为别名，以便 IDE 能提供合适的反馈。只要可能，最好复用这些内建精译器：要么通过宏，要么通过在适当语法上调用 elabDoElem。

修改变量

操作符 doCensor : doElemcensor 会把所有可变变量替换成其类型的 Inhabited 实例所定义的默认值。

syntax (name := doCensor) "censor" : doElem

@[doElem_elab doCensor]
def elabCensor : DoElab := fun stx dec => do
  let vars := (← readThe Do.Context).mutVars
  let dec ← dec.ensureUnitAt stx
  if h : vars.size = 0 then
    logErrorAt stx "There are no mutable variables to censor."
    dec.continueWithUnit
  else
    let assigns ← vars.mapM fun v =>
      `(doElem| $(v.ident):ident := Inhabited.default)
    elabDoElems1 assigns dec

Lean.Parser.Term.do : termdo 精译上下文在控制信息处理器中不可用，因此无法精确返回“所有被修改的可变变量集合”。不过，把所有局部变量的用户名称作为一个过近似是合适的：

@[doElem_control_info doCensor]
def doCensor.control : ControlInfoHandler := fun _ => do
  return { ControlInfo.pure with
      reassigns := (← getLCtx).decls.map (·.map (·.userName))
        |>.foldl (init := .empty) fun
          | names, some n => names.insert n
          | names, none => names
    }

使用 doCensor : doElemcensor 之后，所有可变变量都会被重置为各自类型的默认值：

x: 1, c: m
x: 1, c: f
x: 0, c: A
#eval show IO Unit from do
  let mut x := 0
  let mut c := 'm'
  x := x + 1
  IO.println s!"x: {x}, c: {c}"
  c := 'f'
  IO.println s!"x: {x}, c: {c}"
  censor
  IO.println s!"x: {x}, c: {c}"

x: 1, c: m
x: 1, c: f
x: 0, c: A

在线查看 ↪

23.7.3.6. 效应提升🔗

许多有用的单子运算符都接受一个返回类型位于该单子中的函数，并以某种修改过的方式运行这个函数。例如 withReader、tryCatch 与 IO.FS.withFile。像 tryCatch 这样的函数拥有专门语法，可以让“可能抛出异常的代码”和“处理该异常的代码”都成为外围 Lean.Parser.Term.do : termdo 块的一部分，因此它们也就可以重新赋值可变变量，或提前返回等。这些其他运算符则没有这样的语法。

Lean.Parser.Term.do : termdo 元素精译器可以安排：在精译后表达式中传给这些运算符的那个函数，其函数体仍被当作源 Lean.Parser.Term.do : termdo 块的一部分，就像异常处理语法那样。这借助 EffectForwarder 完成；它会围绕内部的 Lean.Parser.Term.do : termdo 元素序列和函数本身生成合适的包装代码。分三步进行：

根据内部序列的控制信息与当前元素的续延，用 EffectForwarder.ofCont 为该内部序列创建一个 EffectForwarder。
使用 EffectForwarder.lift 精译内部序列；它会向内部精译器提供一个合适的续延，用来生成包装代码。
精译器不会调用原始续延，而是调用由 EffectForwarder.restoreCont 生成的续延；这个续延会为结果添加合适的解包代码。

这些提升代码与 Lean 内建单子变换器的实现很相似。例如，如果内部的 Lean.Parser.Term.do : termdo 序列修改了某个变量，那么包装与解包代码就会像 StateT 那样，安排把该变量传入被提升的代码并以元组形式返回。如果内部的 Lean.Parser.Term.do : termdo 序列可能抛出异常，那么提升后的版本就类似于一次对 ExceptT 的使用。

结构体

Lean.Elab.Do.EffectForwarder : Type
Lean.Elab.Do.EffectForwarder : Type

通过单子变换器栈把非尾位置的可恢复主体嵌入 origCont 的方案。

构造子

Lean.Elab.Do.EffectForwarder.mk

字段

origCont : Elab.Do.DoElemCont

外围 do 块的续延；主体结束后恢复。

returnBase? : Option Elab.Do.ControlStack

安装提前返回处理器处的子栈（如果安装了该处理器）。

breakBase? : Option Elab.Do.ControlStack

安装 break 处理器处的子栈（如果安装了该处理器）。

continueBase? : Option Elab.Do.ControlStack

安装 continue 处理器处的子栈（如果安装了该处理器）。

liftedStack : Elab.Do.ControlStack

位于基础单子之上的完整变换器栈。

liftedDoBlockResultType : Expr

主体的精译类型，即 stM dec.resultType。

定义

Lean.Elab.Do.EffectForwarder.ofCont (info : Elab.Do.ControlInfo)
  (dec : Elab.Do.DoElemCont) : Elab.Do.DoElabM Elab.Do.EffectForwarder
Lean.Elab.Do.EffectForwarder.ofCont
  (info : Elab.Do.ControlInfo)
  (dec : Elab.Do.DoElemCont) :
  Elab.Do.DoElabM Elab.Do.EffectForwarder

为效应由 info 汇总的主体构造提升器方案。

定义

Lean.Elab.Do.EffectForwarder.lift (l : Elab.Do.EffectForwarder)
  (elabElem : Elab.Do.DoElemCont → Elab.Do.DoElabM Expr) :
  Elab.Do.DoElabM Expr
Lean.Elab.Do.EffectForwarder.lift
  (l : Elab.Do.EffectForwarder)
  (elabElem :
    Elab.Do.DoElemCont →
      Elab.Do.DoElabM Expr) :
  Elab.Do.DoElabM Expr

在提升后的栈中精译 elabElem：安装汇入 liftedStack 的 break/continue/return 处理器，并将 do 块的结果类型设为 liftedDoBlockResultType。其语义为 MonadControl.liftWith fun runInBase => elabElem (runInBase pure)。传给 elabElem 的续延会隐式包装在 runInBase 中；一旦通过汇总此提升器所有 lift 调用点上的效应确定了变换器栈 t，随后便由 ControlStack.mkBreak/mkContinue/mkReturn 实现这一包装。

定义

Lean.Elab.Do.EffectForwarder.restoreCont (l : Elab.Do.EffectForwarder) :
  Elab.Do.DoElabM Elab.Do.DoElemCont
Lean.Elab.Do.EffectForwarder.restoreCont
  (l : Elab.Do.EffectForwarder) :
  Elab.Do.DoElabM Elab.Do.DoElemCont

构造一个 DoElemCont，它解包提升后主体的结果，并恢复执行 origCont.k。

withReader 的语法

在 Lean.Parser.Term.do : termdo 块中，doLocally : doElemlocally 允许在修改过的 MonadReader 上下文中运行一段 Lean.Parser.Term.do : termdo 元素序列：

syntax (name := doLocally)
  "locally " ident " => " termBeforeDo " do " doSeq : doElem

termBeforeDo 解析器会匹配那些自身不包含括号或方括号之外的 Lean.Parser.Term.do : termdo 的 Lean 项。由于这个新语法包含一段 Lean.Parser.Term.do : termdo 元素序列，因此它的控制信息必须从这些元素计算出来：

@[doElem_control_info doLocally]
def inferLocally : ControlInfoHandler := fun stx => do
  let `(doElem| locally $_:ident => $_ do $seq) := stx
    | throwUnsupportedSyntax
  InferControlInfo.ofSeq seq

实际的精译器首先会计算主体的控制信息，然后根据该控制信息和原始续延导出一个控制提升器。这个控制提升器可以精译主体；它会向精译器提供自己的续延。构造 withReader 的应用时，使用的是常规项精译技术；其中要特别注意，函数参数必须以适用于该单子的正确宇宙层级上的非依赖函数类型来精译（这个宇宙可在 Context.monadInfo 的 MonadInfo.u 中取得）。最后，还会再次使用控制提升器，为完整精译结果重建一个合适的续延：

@[doElem_elab doLocally] def elabDoLocally : DoElab := fun stx dec => do
  let `(doElem| locally $x:ident => $e do $seq) := stx
    | throwUnsupportedSyntax
  let lifter ← EffectForwarder.ofCont (← inferControlInfoElem stx) dec
  let body ← lifter.lift (elabDoSeq seq)
  let ρ ← Meta.mkFreshExprMVar (mkSort (.succ (← read).monadInfo.u))
  let f ← Term.elabTermEnsuringType (← `(fun $x => $e)) (← mkArrow ρ ρ)
  Term.synthesizeSyntheticMVarsNoPostponing
  let wrapped ← Meta.mkAppM ``MonadWithReaderOf.withReader #[f, body]
  (← lifter.restoreCont).mkBindUnlessPure wrapped

有了这个精译器之后，即便某个值由 ReaderT 提供，也可以在局部覆写它，同时依然允许那些与外围 Lean.Parser.Term.do : termdo 块绑定在一起的效应继续工作：

abbrev App := ReaderT Nat Id

110#eval show Id Nat from do
  Id.run <| (·.run 5) <| show App Nat from do
    let mut total := 0
    total := total + (← read)
    locally r => r + 100 do
      -- 修改外层变量
      total := total + (← read)
      if (← read) > 1000 then
        -- 从外层块提前返回
        return 999
    return total

在线查看 ↪

局部破坏不变式

当某个可变变量需要维持某种不变式时，通常最方便的做法是使用子类型。不过，子类型的缺点在于：这个不变式必须始终成立；你不能在局部打破它，再在稍后重新建立。虽然也可以为此使用第二个可变变量，但那样会让代码变得杂乱且容易出错。借助对 Lean.Parser.Term.do : termdo 记法的适当扩展，就可以很方便地在局部打破并重新建立不变式。

第一步是为这个操作建立语法。 openMutPure : doElemopen mut 会把该子类型“打开”，使其中包含的数据在嵌套块中摆脱谓词约束。当该块结束后，用户必须证明或检查该不变式成立；如果在 openMutPure : doEleminvariant 部分放置一个 Lean.Parser.Term.do : termdo 块，就表示应当执行一次动态检查。第二个语法定义显式给出了高优先权以避免歧义，从而确保只要出现 Lean.Parser.Term.do : termdo 块，就会优先使用它。

syntax (name := openMutPure)
  "open" "mut" ident "do" doSeq "invariant" term : doElem

syntax (name := openMutMon) (priority := high)
  "open" "mut" ident "do" doSeq "invariant" "do" doSeq : doElem

这些操作的控制信息处理器是嵌入其中的 doSeq 语法的函数：

@[doElem_control_info openMutPure, doElem_control_info openMutMon]
def openMutInfo : ControlInfoHandler := fun
  | `(doElem|open mut $x do $steps invariant do $steps') => do
    let info ← inferControlInfoSeq steps
    let info' ← inferControlInfoSeq steps'
    return info.sequence info'
  | `(doElem|open mut $x do $steps invariant $tm:term) =>
    inferControlInfoSeq steps
  | _ => throwUnsupportedSyntax

这个精译器的核心是一个辅助函数，它会做如下几件事：

确保给定名称确实引用了一个子类型变量，并提取其底层类型与谓词。
从该子类型中取出内部值。
用 Lean.Parser.Term.let : termlet 绑定这个内部值，把这个 Lean.Parser.Term.let : termlet 绑定变量建立为别名，并把它安排成可变变量。
用一个会调用“关闭”该子类型、重新建立不变式的精译器的续延来精译主体。

def openMutBody (x : Ident) (seq : TSyntax ``doSeq)
    (mkClose : (p outerTy : Expr) → (base : FVarId) → DoElabM Expr) :
    DoElabM Expr := do
  -- 确保它是可变变量
  throwUnlessMutVarDeclared x
  -- 确保它是子类型
  let outerDecl ← getLocalDeclFromUserName x.getId
  let ty ← whnf outerDecl.type
  let (``Subtype, #[α, p]) := ty.getAppFnArgs
    | throwError "`open mut`: `{x}` is not a subtype, but is a `{ty}`"

  -- 从子类型中取出值
  let base := outerDecl.fvarId
  let init ← mkAppM ``Subtype.val #[outerDecl.toExpr]

  -- 建立 let 绑定并继续
  withLetDecl x.getId α init (nondep := false) fun innerX => do
    addLocalVarInfo x innerX
    pushInfoLeaf <| .ofFVarAliasInfo {
      userName := x.getId, id := innerX.fvarId!, baseId := base
    }
    let bodyCont : DoElemCont := {
      resultName := ← mkFreshUserName `__r, resultType := ← mkPUnit
      k := mkClose p outerDecl.type base
    }
    mkLetFVars #[innerX] (← declareMutVar x do elabDoSeq seq bodyCont)

调用 addLocalVarInfo 会把精译后 Lean.Parser.Term.let : termlet 绑定变量与源码中的标识符之间的联系告知语言服务器，从而支持例如悬停显示类型信息等特性。 pushInfoLeaf 与 Info.ofFVarAliasInfo 联合使用时，会把这个 Lean.Parser.Term.let : termlet 绑定变量注册为已有绑定的别名。

关闭纯版本时，需要引入一个新的 Lean.Parser.Term.let : termlet 绑定，用更新后的值和证明来遮蔽并别名化这个可变变量。

def rebindMut (x : Ident) (outerTy repacked : Expr) (base : FVarId)
    (dec : DoElemCont) : DoElabM Expr :=
  withLetDecl x.getId outerTy repacked (nondep := false) fun newX => do
    addLocalVarInfo x newX
    pushInfoLeaf <| .ofFVarAliasInfo {
      userName := x.getId, id := newX.fvarId!, baseId := base
    }
    mkLetFVars #[newX] (← dec.continueWithUnit)

纯版本的精译器把上述两个部分连接起来：

@[doElem_elab openMutPure]
def elabOpenMutPure : DoElab := fun stx dec => do
  let `(doElem| open mut $x:ident do $seq invariant $prf:term) := stx
    | throwUnsupportedSyntax
  let dec ← dec.ensureUnitAt x
  openMutBody x seq fun p outerTy base => do
    let cur ← getFVarFromUserName x.getId
    let proof ← Term.elabTermEnsuringType prf (mkApp p cur)
    rebindMut x outerTy (← mkAppM ``Subtype.mk #[cur, proof]) base dec

为了演示这个特性的实际效果，考虑非零自然数类型 Pos：

abbrev Pos := { n : Nat // 0 < n }

在 openMutPure : doElemopen 块内部，x 的类型是 Nat。它和其他可变变量都可以被重新赋值：

(21, 120)#eval show Id (Pos × Nat) from do
  let mut other := 100
  let mut x : Pos := ⟨10, byother:Nat := 100⊢ 0 < 10 grindAll goals completed! 🐙⟩
  open mut x do
    x := x * 2
    other := other + x
    x := x + 1
  invariant byother✝:Nat := 100x✝²:Pos := ⟨10, _eval._proof_1⟩x✝¹:Nat := x✝².valx✝:Nat := x✝¹ * 2other:Nat := other✝ + x✝x:Nat := x✝ + 1⊢ (fun n => 0 < n) x grindAll goals completed! 🐙
  return (x, other)

(21, 120)

同样，内部块也可以从外层 Lean.Parser.Term.do : termdo 块中 Lean.Parser.Term.doReturn : doElemreturn：

(0, 120)#eval show Id (Nat × Nat) from do
  let mut other := 100
  let mut x : Pos := ⟨10, byother:Nat := 100⊢ 0 < 10 grindAll goals completed! 🐙⟩
  open mut x do
    x := x * 2
    other := other + x
    if other > 0 then return (0, other)
    x := x + 1
  invariant byother✝:Nat := 100x✝²:Pos := ⟨10, _eval._proof_1⟩x✝¹:Nat := x✝².valx✝:Nat := x✝¹ * 2other:Nat := other✝ + x✝__r✝¹:Unitx:Nat := x✝ + 1⊢ (fun n => 0 < n) x grindAll goals completed! 🐙
  return (x.val, other)

(0, 120)

对于无法证明返回值满足该谓词的情形，检查它是否满足仍然可能很有用。单子版本的精译器期望返回一个经过 PLift 提升的证明：

def closeInvariant {α : Type} {P : α → Prop} [Monad m]
    (val : α) (act : m (PLift (P val))) : m (Subtype P) :=
  return ⟨val, (← act).down⟩

@[doElem_elab openMutMon]
def elabOpenMutMon : DoElab := fun stx dec => do
  let `(doElem| open mut $x:ident do $seq invariant do $invSeq) := stx
    | throwUnsupportedSyntax
  let dec ← dec.ensureUnitAt x
  openMutBody x seq fun _p outerTy base => do
    let cur ← getFVarFromUserName x.getId
    let actionStx ←
      ``(closeInvariant $(← Term.exprToSyntax cur) (do $invSeq))
    let action ← elabTermEnsuringType actionStx (← mkMonadApp outerTy)
    let rn ← mkFreshUserName `__repacked
    let closeCont : DoElemCont := {
      resultName := rn, resultType := outerTy
      k := do
        let d ← getLocalDeclFromUserName rn
        rebindMut x outerTy d.toExpr base dec
    }
    closeCont.mkBindUnlessPure action

现在，运行时检查可以确保该不变式成立；如果不成立，就抛出异常：

def trySub3 (x : Pos) : IO Pos := do
  let mut x := x
  open mut x do
    x := x - 3
  invariant do
    if h : 0 < x then pure ⟨h⟩
    else throw (IO.userError s!"Not positive: x = {x}")
  return x

7#eval trySub3 ⟨10, by⊢ 0 < 10 grindAll goals completed! 🐙⟩

Not positive: x = 0#eval trySub3 ⟨3, by⊢ 0 < 3 grindAll goals completed! 🐙⟩

Not positive: x = 0

在线查看 ↪

23.7. 扩展 do 记法🔗

23.7.1. 精译概览🔗

23.7.2. do 记法中的宏🔗

23.7.2.1. 局限性🔗

23.7.3. 精译🔗

23.7.3.1. 单子操作🔗

23.7.3.2. 续延🔗

23.7.3.3. 控制流：return、break 与 continue🔗

23.7.3.4. 控制信息🔗

23.7.3.5. 可变变量🔗

23.7.3.6. 效应提升🔗

23.7. 扩展 `do` 记法🔗

23.7.2. `do` 记法中的宏🔗

23.7.3.3. 控制流：`return`、`break` 与 `continue`🔗