Default value: true
Use the legacy do elaborator instead of the new, extensible implementation.
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 版本 4.29.0 中引入了可扩展的 Lean.Parser.Term.do : termdo 表示法；在此版本之前，它是不可扩展的。
可扩展 Lean.Parser.Term.do : termdo精化器由选项 backward.do.legacy 控制：
option
backward.do.legacy
当 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 : doElem`break` exits the surrounding `for` loop. break 和 Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue）、通过 Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return 转义的方式以及可变变量集等信息。
Lean.Parser.Term.do : termdo-elements 的精化与术语非常相似。
首先，如果所讨论的语法是 宏，则它会被扩展。
重复此操作，直到宏展开的结果不再是宏。
接下来，查询内部表以查找与 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 语法类别的一部分。
Multi-Way 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))
它可以像任何其他术语一样使用：
#eval
let sign : Int → String := fun n =>
if
| n < 0 => "neg"
| n = 0 => "zero"
| else => "pos"
(sign (-2), sign 0, sign 5)
通过将该宏放在 doElem 语法类别中并用 doSeq 而不是 Term 替换多路 Lean.Parser.Term.doIf : doElemif 的每个臂，可以将该宏改编为 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块的一部分，以实现早期返回和可变变量的目的。
在这些情况下，可能需要定义精化器。
Freezing Mutable Variables with a Macro
在 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
y := 2 * x
return y
此外，早期的 Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return 退出内部 Lean.Parser.Term.do : termdo，而不是周围的 Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return，正如预期返回 Unit（在本例中为宇宙多态 PUnit）这一事实所表明的那样：
#eval Id.run do
let mut x : Nat := 0
x := x + 1
let mut y := 0
freeze x in
return x
return y
23.7.3. 精化
Lean.Parser.Term.do : termdo 元素的精化出现在 DoElabM 单子中。
此 monad 是 TermElabM 的包装器，它提供一个额外的 reader 值：Lean.Parser.Term.do : termdo-精化上下文。
精化器还收到一个附加参数：精化continuation 的描述。
延续代表 Lean.Parser.Term.do : termdo 块中当前元素之后的剩余部分；它包括一个 DoElabM 操作（将详细说明块的其余部分）和名称，该术语将通过该名称来引用当前精化步骤的结果。
与将详细术语返回到周围精化上下文的术语精化器不同，Lean.Parser.Term.do : termdo 元素精化器调用提供的延续来安排 Lean.Parser.Term.do : termdo 块其余部分的精化。
structure
Constructor
Lean.Elab.Do.Context.mk
Fields
monadInfo : Elab.Do.MonadInfo
Inferred and cached information about the monad.
mutVars : Array Ident
The mutable variables in declaration order.
mutVarDefs : Std.HashMap Name FVarId
Maps mutable variable names to their initial FVarIds.
doBlockResultType : Expr
The expected type of the current do block.
This can be different from earlyReturnType in for loop do blocks, for example.
contInfo : Elab.Do.ContInfoRef
Information about return, break and continue continuations.
deadCode : Elab.Do.CodeLiveness
Whether the current do element is dead code. elabDoElem will emit a warning if not .alive.
ops : Elab.Do.DoOpsRef
structure
Constructor
Lean.Elab.Do.MonadInfo.mk
Fields
m : Expr
The inferred type of the monad of type Type u → Type v.
u : Level
The u in m : Type u → Type v.
v : Level
The v in m : Type u → Type v.
cachedPUnit : Expr
The cached PUnit expression.
cachedPUnitUnit : Expr
The cached PUnit.unit expression.
inductive type
Whether a code block is alive or dead.
Constructors
Lean.Elab.Do.CodeLiveness.deadSyntactically : Elab.Do.CodeLiveness
We inferred the code is semantically dead and don't need to elaborate it at all.
Lean.Elab.Do.CodeLiveness.deadSemantically : Elab.Do.CodeLiveness
We inferred the code is semantically dead, but we need to elaborate it to produce a program.
Lean.Elab.Do.CodeLiveness.alive : Elab.Do.CodeLiveness
The code is alive. (Or it is dead, but we failed to prove it so.)
为了避免实现中的循环，Context.contInfo和Context.ops字段是构造后填充的引用。
使用ContInfoRef.toContInfo和DoOpsRef.toDoOps恢复底层数据：
opaque
structure
Information about a success, return, break or continue continuation that will be filled in
after the code using it has been elaborated.
Constructor
Lean.Elab.Do.ContInfo.mk
Fields
returnCont : Elab.Do.ReturnCont
breakCont : Option (Elab.Do.DoElabM Expr)
continueCont : Option (Elab.Do.DoElabM Expr)
opaque
structure
Pluggable builders for the pure / bind applications emitted by the do elaborator.
Constructor
Lean.Elab.Do.DoOps.mk
Fields
mkPureApp : Expr → Expr → Elab.Do.DoElabM Expr
Build pure (α:=α) e : m α.
mkBindApp : Expr → Expr → Expr → Expr → Elab.Do.DoElabM Expr
Build bind (α:=α) (β:=β) e k : m β.
isPureApp? : Expr → Option Expr
If e is syntactically a pure … application, return the pure value; otherwise none.
Used by DoElemCont.mkBindUnlessPure to contract e >>= pure to e and
pure e >>= k to let x := e; k x.
splitMonadApp? : Expr → Elab.TermElabM (Option (Elab.Do.MonadInfo × Expr))
Match a monad application m α, returning MonadInfo for m and α.
mkMonadApp : Expr → Elab.Do.DoElabM Expr
Construct m α from α.
精化器使用 doElem_elab 属性与语法类型相关联。
它们的类型应为 DoElab。
除了精化器之外，通过精化器实现的每个自定义 Lean.Parser.Term.do : termdo 元素还必须提供 控制信息。
def
The type of elaborators for do block elements.
It is elabTerm `(do $e; $rest) = elabDoElem e dec, where elabDoElem e · is the elaborator for
do element e, and dec is the DoElemCont describing the elaboration of the rest of the block
rest.
attributeDo Element Elaborators
attr ::= ... | doElem_elab
Registers a do element elaborator for the given syntax node kind.
A do element elaborator should have type DoElab (which is
Lean.Syntax → DoElemCont → DoElabM Expr), i.e. should take syntax of the given syntax node kind
and a DoElemCont as parameters and produce an expression.
When elaborating a do block do e; rest, the elaborator for e is invoked with the syntax of e
and the DoElemCont representing rest.
The elab_rules and elab commands should usually be preferred over using this attribute
directly.
此外，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。
opaque
Lean.Elab.Do.elabDoElem (stx : TSyntax `doElem) (cont : Elab.Do.DoElemCont) (catchExPostpone : Bool := true) : Elab.Do.DoElabM ExprLean.Elab.Do.elabDoElem (stx : TSyntax `doElem) (cont : Elab.Do.DoElemCont) (catchExPostpone : Bool := true) : Elab.Do.DoElabM Expr
opaque
Lean.Elab.Do.elabDoSeq (doSeq : TSyntax `Lean.Parser.Term.doSeq) (cont : Elab.Do.DoElemCont) (catchExPostpone : Bool := true) : Elab.Do.DoElabM ExprLean.Elab.Do.elabDoSeq (doSeq : TSyntax `Lean.Parser.Term.doSeq) (cont : Elab.Do.DoElemCont) (catchExPostpone : Bool := true) : Elab.Do.DoElabM Expr
opaque
Lean.Elab.Do.elabDoElems1 (doElems : Array (TSyntax `doElem)) (cont : Elab.Do.DoElemCont) (catchExPostpone : Bool := true) : Elab.Do.DoElabM ExprLean.Elab.Do.elabDoElems1 (doElems : Array (TSyntax `doElem)) (cont : Elab.Do.DoElemCont) (catchExPostpone : Bool := true) : Elab.Do.DoElabM Expr
23.7.3.1. 单子操作
精化框架提供了几个帮助器，可以更方便、更高效地构建当前 monad 及其操作的应用程序。
def
Constructs m α from α.
def
The expression Bind.bind (α:=α) (β:=β) e k.
23.7.3.2. 延续
Lean.Parser.Term.do : termdo-精化延续由等待当前元素的结果的精化器以及元数据（例如该结果预期具有的类型）组成。
structure
Elaboration of a do block do $e; $rest, results in a call
elabTerm `(do $e; $rest) = elabDoElem e dec, where elabDoElem e · is the elaborator for do
element e, and dec is the DoElemCont describing the elaboration of the rest of the block
rest.
If the semantics of e resumes its continuation rest, its elaborator must bind its result to
resultName, ensure that it has type resultType and then elaborate rest using dec.
Clearly, for term elements e : m α, the result has type α.
More subtly, for binding elements let x := e or let x ← e, the result has type PUnit and is
unrelated to the type of the bound variable x.
Examples:
-
returndrops the continuation;return x; pure ()elaborates topure x. -
let x ← e; rest xelaborates toe >>= fun x => rest x. -
let x := 3; let y ← (let x ← e); rest xelaborates tolet x := 3; e >>= fun x_1 => let y := (); rest x, which is immediately zeta-reduced tolet x := 3; e >>= fun x_1 => rest x. -
one; twoelaborates toone >>= fun (_ : PUnit) => two; it is an error ifonedoes not have typePUnit.
Constructor
Lean.Elab.Do.DoElemCont.mk
Fields
resultName : Name
The name of the monadic result variable.
resultType : Expr
The type of the monadic result.
k : Elab.Do.DoElabM Expr
The continuation to elaborate the rest of the block. It assumes that the result of the do
block is bound to resultName with the correct type (that is, resultType, potentially refined
by a dependent match).
kind : Elab.Do.DoElemContKind
inductive type
Whether the continuation of a do element is duplicable and if so whether it is just pure r for
the result variable r. Saying nonDuplicable is always safe; duplicable allows for more
optimizations.
Constructors
许多精化器要求延续期望其结果具有特定类型。
例如，如果精化器不返回结果，则生成 Unit 是很常见的。
在早期阶段检查类型可以产生更好的错误消息：
def
def
Lean.Elab.Do.DoElemCont.ensureUnitAt (dec : Elab.Do.DoElemCont) (ref : Syntax) : Elab.Do.DoElabM Elab.Do.DoElemContLean.Elab.Do.DoElemCont.ensureUnitAt (dec : Elab.Do.DoElemCont) (ref : Syntax) : Elab.Do.DoElabM Elab.Do.DoElemCont
Given a continuation dec and a reference ref, returns a continuation derived from dec with result type PUnit.
If dec already has result type PUnit, simply returns dec. Otherwise, an error is logged and a
new continuation is returned that calls dec with sorry as a result. The error is reported at ref.
def
Lean.Elab.Do.DoElemCont.ensureHasTypeAt (dec : Elab.Do.DoElemCont) (ref : Syntax) (elementType : Expr) : Elab.Do.DoElabM Elab.Do.DoElemContLean.Elab.Do.DoElemCont.ensureHasTypeAt (dec : Elab.Do.DoElemCont) (ref : Syntax) (elementType : Expr) : Elab.Do.DoElabM Elab.Do.DoElemCont
Given a continuation dec, a reference ref, and an element result type elementType, returns a
continuation derived from dec with result type elementType.
If dec already has result type elementType, simply returns dec.
Otherwise, an error is logged and a new continuation is returned that calls dec with sorry as a
result. The error is reported at ref.
调用延续包括向其提供当前 Lean.Parser.Term.do : termdo 元素的结果。
可以通过三种主要方法来实现此目的。
DoElemCont.continueWithUnit 确保延续需要 Unit，然后调用它。
DoElemCont.elabAsSyntacticallyDeadCode 在断言代码不可访问的上下文中调用延续，通常会导致延续不生成任何代码，并且如果存在代码也会警告用户。
DoElemCont.mkBindUnlessPure 负责将 Lean.Parser.Term.do : termdo 表示法标准脱糖到 bind 的应用程序中；它用于在详细精化由单子类型项组成的 Lean.Parser.Term.do : termdo 元素后调用延续，并且它包含一个优化，用 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定替换 pure 周围的 bind。
def
Return let $k.resultName : PUnit := PUnit.unit; $(← k.k), ensuring that the result type of k.k
is PUnit and then immediately zeta-reduce the let.
def
Lean.Elab.Do.DoElemCont.elabAsSyntacticallyDeadCode (dec : Elab.Do.DoElemCont) : Elab.Do.DoElabM UnitLean.Elab.Do.DoElemCont.elabAsSyntacticallyDeadCode (dec : Elab.Do.DoElemCont) : Elab.Do.DoElabM Unit
Elaborate the DoElemCont with the deadCode flag set to deadSyntactically to emit warnings.
def
Lean.Elab.Do.DoElemCont.mkBindUnlessPure (dec : Elab.Do.DoElemCont) (e : Expr) : Elab.Do.DoElabM ExprLean.Elab.Do.DoElemCont.mkBindUnlessPure (dec : Elab.Do.DoElemCont) (e : Expr) : Elab.Do.DoElabM Expr
Invoking Continuations
内置语法 Lean.Parser.Term.InternalSyntax.doSkipInternal syntax used in the `if` and `unless` elaborators. Behaves like `pure PUnit.unit` but
uses `()` if possible and gives better error messages.
skip 的一个版本（相当于 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 ()：
#eval show Option Unit from do nothing
Elaborating do-elements with elab_rules
doNothing : doElemnothing 的替代版本（相当于内置语法 Lean.Parser.Term.InternalSyntax.doSkipInternal syntax used in the `if` and `unless` elaborators. Behaves like `pure PUnit.unit` but
uses `()` if possible and gives better error messages.
skip）可以使用 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 ()：
#eval show Option Unit from do nothing
由于精化器显式调用其延续，而不是简单地返回值，因此它可以控制精化的上下文。
特别是，它可以使用 withReader 修改上下文，并且可以多次调用延续以支持具有分支的控制结构。
为了防止代码大小爆炸，延续会跟踪它们是否可以在 DoElemCont.kind 中多次详细说明。
如果延续可以被多次调用，则为 duplicable，否则为 nonduplicable。
可以使用 DoElemCont.withDuplicableCont 将不可重复的延续转换为可重复的延续。
def
Lean.Elab.Do.DoElemCont.withDuplicableCont (nondupDec : Elab.Do.DoElemCont) (callerInfo : Elab.Do.ControlInfo) (caller : Elab.Do.DoElemCont → Elab.Do.DoElabM Expr) : Elab.Do.DoElabM ExprLean.Elab.Do.DoElemCont.withDuplicableCont (nondupDec : Elab.Do.DoElemCont) (callerInfo : Elab.Do.ControlInfo) (caller : Elab.Do.DoElemCont → Elab.Do.DoElabM Expr) : Elab.Do.DoElabM Expr
Call caller with a duplicable proxy of dec.
When the proxy is elaborated more than once, a join point is introduced so that dec is only
elaborated once to fill in the RHS of this join point.
This is useful for control-flow constructs like if and match, where multiple tail-called
branches share the continuation.
无法访问的代码不需要详细说明。
当 Lean.Parser.Term.do : termdo 元素的精化器检测到延续的精化的结果不可访问时，它可以直接返回其结果项，而不是将其传递给精化延续。
它应该产生一个术语来证明放弃该程序是合理的，例如调用 False.elim。
在返回该术语之前，它应该在延续上调用 DoElemCont.elabAsSyntacticallyDeadCode，这会警告用户延续将详细说明的代码无法访问。
Unreachable Code
当提供 False 的证明时，运算符 doAbsurd : doElemabsurd 将代码标记为不可访问，这表明当前本地上下文在逻辑上不一致。
如果通过了证明，则使用它；否则，它会尝试一些自动化。
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 }
精化器首先提取证明语法，如果未提供则回退到默认值。
然后，它将证明精化为错误的证明。
如果成功，它会使用 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 子句：
#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 := ⊢ ∀ (x : Nat), x ∈ xs → x % 2 = 1
All goals completed! 🐙
#eval show Id Nat from do
for h : n in 0...5 do
let k := n * 2
if h' : k ∈ xs then
absurd by All goals completed! 🐙
return k
pure 100
但是，它确实运行成功：
23.7.3.3. 控制流：return、break 和 continue
Lean.Parser.Term.do : termdo 表示法支持三个非本地跳转指令： Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return，提前终止整个 Lean.Parser.Term.do : termdo 块； Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break，提前终止循环； Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue，提前终止循环的单次迭代。
Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return 始终是允许的，而 Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break 和 Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue 仅在循环体内有效。
在精化期间，这三个跳转中的每一个都由一个延续表示。
def
def
def
这三个延续是使用帮助程序 enterLoopBody 安装在上下文中的。
def
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 α
Prepare the context for elaborating the body of a loop.
This includes setting the return continuation, break continuation, continue continuation, as
well as the changed result type of the do block in the loop body.
Single-Iteration Loop
单次迭代循环 doOnce : doElemonce 执行一次其主体，跳至 Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break 或 Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue 上的循环末尾：
syntax (name := doOnce) "once " doSeq : doElem
它的控制信息基于身体的控制信息。
doOnce : doElemonce 永远不会中断或继续自身，因为它在其主体中处理 Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break 和 Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue；因此，它将 breaks 和 continues 设置为 false。
numRegularExits 是控制可以到达 doOnce : doElemonce 之后的代码的次数。
主体的正常下降、Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break 和 Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue 都将控制权转移到循环末尾，因此控制最多留下 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 : doElem`break` exits the surrounding `for` loop. break 和 Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue 延续关联起来。
由于精心设计的主体可以从多个位置到达该延续，因此精化器计算了这些用途。
主体的控制信息并不指示 Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break 和 Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue 可以被调用多少次，因此它们近似为每个出口，安全地确保如果使用其中任何一个，则延续将被复制。
总的近似使用计数被传递到 DoElemCont.withDuplicableCont，当使用计数大于 1 时，它会共享延续而不是在每次使用时重复它，从而避免代码爆炸。
它直接从主体计算此计数，因为控制信息处理程序报告的值最多为 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 : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return 终止整个 Lean.Parser.Term.do : termdo 块：
#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 元件必须提供准确的控制信息。不正确的控制信息可能会导致错误的代码生成。
attributeDo Element Control Information
attr ::= ... | doElem_control_info
Registers a ControlInfo inference handler for the given doElem syntax node kind.
A handler should have type ControlInfoHandler (i.e. TSyntax \doElem → TermElabM ControlInfo). For pure handlers, usefun stx => return ControlInfo.pure`.
def
A handler for inferring ControlInfo from a doElem syntax. Register with @[doElem_control_info parserName].
如果 Lean.Parser.Term.do : termdo 元素既不重新分配变量也不导致提前返回或终止，则处理程序可以返回 ControlInfo.pure。
如果它表示没有常规退出且没有其他控制效果的代码，则处理程序可以返回 ControlInfo.empty；否则，将 ControlInfo.numRegularExits 设置为 0，将 ControlInfo.noFallthrough 设置为 true，同时记录任何早期返回、重新分配或循环终止。
structure
Represents information about what control effects a do block has.
The fields split by flavor:
-
breaks,continues,returnsEarly, andreassignsare syntactic:true/non-empty iff the corresponding construct appears anywhere in the source text of the block, independent of whether it is semantically reachable. Downstream elaborators must assume every such syntactic effect may occur, because the elaborator visits every doElem (only top-levelreturn/break/continueshort-circuit viaelabAsSyntacticallyDeadCode). -
numRegularExitsis also syntactic: the number of times the block wires the enclosing continuation into its elaborated expression.withDuplicableContreads it as a join-point duplication trigger (> 1). -
noFallthrough = trueasserts that the next doElem in the enclosing sequence is semantically irrelevant (control never falls through to it).noFallthrough = falsemakes no such assertion. The dead-code warning fires on the next element when this istrue.
Invariant: numRegularExits = 0 → noFallthrough. The converse does not hold.
Constructor
Lean.Elab.Do.ControlInfo.mk
Fields
breaks : Bool
The do block syntactically contains a break.
continues : Bool
The do block syntactically contains a continue.
returnsEarly : Bool
The do block syntactically contains an early return.
numRegularExits : Nat
The number of times the block wires the enclosing continuation into its elaborated expression.
Consumed by withDuplicableCont to decide whether to introduce a join point (> 1).
noFallthrough : Bool
reassigns : NameSet
The variables that are syntactically reassigned somewhere in the do block.
def
def
The identity of ControlInfo.alternative: a ControlInfo describing a block with no branches
at all (so no regular exits and the next element is trivially unreachable).
如果 Lean.Parser.Term.do : termdo 元素本身包含其他 Lean.Parser.Term.do : termdo 元素，则它可以使用组合器 ControlInfo.sequence 和 ControlInfo.alternative 来组合来自其子元素的控制信息。
ControlInfo.sequence 用于顺序步骤，ControlInfo.alternative 用于合并控制流分支。
def
def
一般来说，控制信息应使用inferControlInfoElem或inferControlInfoSeq计算。
def
def
Lean.Elab.Do.inferControlInfoSeq (doSeq : TSyntax `Lean.Parser.Term.doSeq) : Elab.TermElabM Elab.Do.ControlInfoLean.Elab.Do.inferControlInfoSeq (doSeq : TSyntax `Lean.Parser.Term.doSeq) : Elab.TermElabM Elab.Do.ControlInfo
在某些高级情况下，可能需要 Lean.Elab.Do.InferControlInfo 中的功能之一：
opaque
opaque
Lean.Elab.Do.InferControlInfo.ofSeq (stx : TSyntax `Lean.Parser.Term.doSeq) : Elab.TermElabM Elab.Do.ControlInfoLean.Elab.Do.InferControlInfo.ofSeq (stx : TSyntax `Lean.Parser.Term.doSeq) : Elab.TermElabM Elab.Do.ControlInfo
opaque
Lean.Elab.Do.InferControlInfo.ofOptionSeq (stx? : Option (TSyntax `Lean.Parser.Term.doSeq)) : Elab.TermElabM Elab.Do.ControlInfoLean.Elab.Do.InferControlInfo.ofOptionSeq (stx? : Option (TSyntax `Lean.Parser.Term.doSeq)) : Elab.TermElabM Elab.Do.ControlInfo
opaque
opaque
Lean.Elab.Do.InferControlInfo.ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [`Lean.Parser.Term.doIdDecl, `Lean.Parser.Term.doPatDecl]) : Elab.TermElabM Elab.Do.ControlInfoLean.Elab.Do.InferControlInfo.ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [`Lean.Parser.Term.doIdDecl, `Lean.Parser.Term.doPatDecl]) : Elab.TermElabM Elab.Do.ControlInfo
23.7.3.5. 可变变量
上下文的一个重要部分是可用于正在详细说明的 Lean.Parser.Term.do : termdo 元素的一组可变变量。
这在两个字段中可用：mutVars 提供最初绑定变量的标识符，而 mutVarDefs 将它们的名称映射到表示它们的局部变量。
由于卫生，mutVars中的标识符包含宏范围；在构建面向用户的错误消息之前，应使用 Name.simpMacroScopes 删除这些内容。
每个可变变量对应至少一个详细变量 (Expr.fvar)。
这些详细变量存在于跟踪其用户可见名称的本地上下文中。
突变是通过影子 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定实现的，并且 Lean.Parser.Term.do : termdo 块中的后续步骤在上下文中详细说明，其中该影子 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 是变量的用户可见名称的绑定。
使用标准精化帮助程序 Lean.Meta.getFVarFromUserName 和 Lean.Meta.getLocalDeclFromUserName 检索与用户名关联的局部变量，并使用 TSyntax.getId 将 Ident 转换为可查找的用户名。
当使用 Lean.Parser.Term.doLet : doElemlet mut 建立可变变量时，将创建一个 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定来表示它，并且初始变量的绑定标识符和 Expr.fvar 将添加到在延续周围使用的上下文，该延续在 withReader 下调用以添加新变量。
建立 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定后，使用 declareMutVar 注册一个可变变量或一组可变变量。
def
Register the given name as that of a mut variable.
def
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 α
Register the given names as that of mut variables.
要确保标识符引用可变变量，请使用 throwUnlessMutVarDeclared：
def
Throw an error if the given name is not a declared mut variable.
def
Throw an error if the given names are not declared mut variables.
Tracing Mutable Variables
新语法 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 : Ident) => do
let nameLit := x.getId.simpMacroScopes.toString
`(term| s!"{$(quote nameLit)} = {repr $x}")
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
跟踪计算斐波那契数的循环会显示所有中间状态：
#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
可变变量的内置精化器负责许多微妙的细节，例如将可变变量的每个生成的 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定注册为别名，以便 IDE 可以提供适当的反馈。
如果可能的话，最好通过宏或通过在适当的语法上调用 elabDoElem 来重用这些内置的精化器。
Mutating Variables
运算符 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 := 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 后，所有可变变量都已重置为其类型的默认值：
#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}"
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 块的一部分，就像异常处理语法一样。
这是使用 ControlLifter 完成的，它围绕 Lean.Parser.Term.do : termdo 元素的内部序列和函数本身生成合适的包装器代码。
共有三个步骤：
-
内部序列的
ControlLifter是使用ControlLifter.ofCont根据其控制信息和当前元素的延续创建的。 -
内部序列使用
ControlLifter.lift进行详细说明，它为内部精化器提供生成包装代码的合适延续。 -
精化器不调用原始延续，而是调用
ControlLifter.restoreCont生成的延续，这会向结果添加合适的解包代码。
提升代码类似于 Lean 的内置 monad 变压器 的实现。
例如，如果内部 Lean.Parser.Term.do : termdo 序列改变一个变量，则包装和解包代码会安排该变量传递给提升的代码并以元组形式返回，就像 StateT 一样。
如果内部 Lean.Parser.Term.do : termdo 序列可能引发异常，则提升版本类似于 ExceptT 的使用。
structure
Constructor
Lean.Elab.Do.ControlLifter.mk
Fields
origCont : Elab.Do.DoElemCont
returnBase? : Option Elab.Do.ControlStack
breakBase? : Option Elab.Do.ControlStack
continueBase? : Option Elab.Do.ControlStack
pureBase : Elab.Do.ControlStack
pureDeadCode : Elab.Do.CodeLiveness
liftedDoBlockResultType : Expr
def
Lean.Elab.Do.ControlLifter.ofCont (info : Elab.Do.ControlInfo) (dec : Elab.Do.DoElemCont) : Elab.Do.DoElabM Elab.Do.ControlLifterLean.Elab.Do.ControlLifter.ofCont (info : Elab.Do.ControlInfo) (dec : Elab.Do.DoElemCont) : Elab.Do.DoElabM Elab.Do.ControlLifter
def
Lean.Elab.Do.ControlLifter.lift (l : Elab.Do.ControlLifter) (elabElem : Elab.Do.DoElemCont → Elab.Do.DoElabM Expr) : Elab.Do.DoElabM ExprLean.Elab.Do.ControlLifter.lift (l : Elab.Do.ControlLifter) (elabElem : Elab.Do.DoElemCont → Elab.Do.DoElabM Expr) : Elab.Do.DoElabM Expr
This function is like MonadControl.liftWith fun runInBase => elabElem (runInBase pure).
All continuations should be thought of as wrapped in runInBase, so that their effects are embedded
in the terminal stM m (t m) result type. This wrapping will be realized by
ControlStack.synthesizeConts, after we know what the transformer stack t looks like.
What t looks like depends on whether reassignments, early return, break and continue are
used, considering all the use sites of ControlLifter.lift.
def
Lean.Elab.Do.ControlLifter.restoreCont (l : Elab.Do.ControlLifter) : Elab.Do.DoElabM Elab.Do.DoElemContLean.Elab.Do.ControlLifter.restoreCont (l : Elab.Do.ControlLifter) : Elab.Do.DoElabM Elab.Do.DoElemCont
Syntax for 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 术语，这些术语本身不包含括号或方括号之外的 Lean.Parser.Term.do : termdo。
由于此新语法包含一系列 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 的应用程序，特别注意确保函数参数是在 monad 的正确宇宙中使用非依赖函数类型来详细说明的（在 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 ← ControlLifter.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
#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
-- Mutates an outer variable
total := total + (← read)
if (← read) > 1000 then
-- Early return from the outer block
return 999
return total
Locally Violating Invariants
当需要维护可变变量的某些不变量时，使用子类型通常是最方便的。
然而，子类型有一个缺点，即必须始终维持不变式；它不能在本地被破坏并重新建立。
虽然可以使用第二个可变变量来实现此目的，但这会使代码变得混乱并且容易出错。
通过对 Lean.Parser.Term.do : termdo 表示法的适当扩展，可以方便地局部破坏和重新建立不变量。
第一步是建立此操作的语法。
openMutPure : doElemopen mut 将“打开”子类型，将所包含的数据从嵌套块中谓词的限制中释放出来。
区块完成后，用户必须证明或检查不变量是否成立；将 Lean.Parser.Term.do : termdo 块放置在 openMutPure : doEleminvariant 部分中表示要执行动态检查。
第二个语法定义具有明确的高优先级以避免歧义，这确保只要存在 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 : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ``` The *anaphoric let* `let := v` defines a variable called `this`.let绑定内部值，将Lean.Parser.Term.let : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ``` The *anaphoric let* `let := v` defines a variable called `this`.let绑定变量建立为别名并安排其可变。 -
它通过调用所提供的精化器的延续来详细说明主体，该延续“关闭”子类型，重新建立不变量。
def openMutBody (x : Ident) (seq : TSyntax ``doSeq)
(mkClose : (p outerTy : Expr) → (base : FVarId) → DoElabM Expr) :
DoElabM Expr := do
-- Ensure that it is mutable
throwUnlessMutVarDeclared x
-- Ensure that it is a subtype
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}`"
-- Get the value from the subtype
let base := outerDecl.fvarId
let init ← mkAppM ``Subtype.val #[outerDecl.toExpr]
-- Let-bind and continue
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 : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定变量与源代码中的标识符之间的连接，从而启用悬停时的类型信息等功能。
pushInfoLeaf 与 Info.ofFVarAliasInfo 组合将 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定变量注册为现有绑定的别名。
关闭纯版本包括引入新的 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定、对可变变量进行遮蔽和别名，以及更新的值和证明。
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。
它和其他可变变量都可以重新分配：
#eval show Id (Pos × Nat) from do
let mut other := 100
let mut x : Pos := ⟨10, other:Nat := 100⊢ 0 < 10 All goals completed! 🐙⟩
open mut x do
x := x * 2
other := other + x
x := x + 1
invariant other✝: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 All goals completed! 🐙
return (x, other)
同样，内部块可以来自外部 Lean.Parser.Term.do : termdo 块的 Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return：
#eval show Id (Nat × Nat) from do
let mut other := 100
let mut x : Pos := ⟨10, other:Nat := 100⊢ 0 < 10 All goals completed! 🐙⟩
open mut x do
x := x * 2
other := other + x
if other > 0 then return (0, other)
x := x + 1
invariant other✝: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 All goals completed! 🐙
return (x.val, other)
对于无法证明返回值满足谓词的情况，检查它是否满足仍然有用。
单子变体的精化器期望返回 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
#eval trySub3 ⟨10, ⊢ 0 < 10 All goals completed! 🐙⟩
#eval trySub3 ⟨3, ⊢ 0 < 3 All goals completed! 🐙⟩