其他便利功能

嵌套活动

feline 中的很多函数都表现出一种重复模式，其中 IO 操作的结果被赋予一个名称，然后立即且仅使用一次。例如，在 dump 中：

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

该模式出现在 stdout 中：

    let stdout ← IO.getStdout
    stdout.write buf

同样，fileStream 包含以下片段

  let fileExists ← filename.pathExists
  if not fileExists then

当 Lean 编译 do 块时，由括号下方的左箭头组成的表达式会被提升到最近的封闭 do 中，并且其结果会被绑定到一个唯一的名称。这个唯一名称替换了原始的表达式。这意味着 dump 也可以写成如下形式：

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    (← IO.getStdout).write buf
    dump stream

此版本的 dump 避免了引入仅使用一次的名称，这可以极大地简化程序。 Lean 从嵌套表达式上下文中提升的 IO 活动称为 嵌套活动（Nested Action） 。

fileStream 也可以用相同的技巧来简化：

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  if not (← filename.pathExists) then
    (← IO.getStderr).putStrLn s!"File not found: {filename}"
    pure none
  else
    let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

在这种情况下，局部名称 handle 也可以使用嵌套操作来消除，但由此产生的表达式会长而复杂。尽管使用嵌套操作通常是一种良好的代码风格，但有时对中间结果进行命名仍然很有帮助。

但需要记住的是，嵌套操作只是对包围在 do 块中的 IO 活动的一种简短记法。执行它们所涉及的副作用仍然会以相同的顺序发生，并且副作用的执行不会与表达式的求值交替进行。举个可能令人困惑的例子，请考虑以下辅助定义，它们在向世界宣布它们已被执行后才返回数据：

def getNumA : IO Nat := do
  (← IO.getStdout).putStrLn "A"
  pure 5

def getNumB : IO Nat := do
  (← IO.getStdout).putStrLn "B"
  pure 7

这些定义旨在表达更复杂的 IO 代码，这些代码可能用于验证用户输入、读取数据库或打开文件。

一个「当数字 A 为 5 时打印 0，否则打印数字 B」的程序可以写成如下形式：

def test : IO Unit := do
  let a : Nat := if (← getNumA) == 5 then 0 else (← getNumB)
  (← IO.getStdout).putStrLn s!"The answer is {a}"

不过，此程序可能具有比预期更多的副作用（例如提示用户输入或读取数据库）。 getNumA 的定义明确指出它将始终返回 5，因此程序不应读取数字 B。然而，运行此程序会产生以下输出：

A
B
The answer is 0

getNumB 被执行是因为 test 等价于以下定义：

def test : IO Unit := do
  let x ← getNumA
  let y ← getNumB
  let a : Nat := if x == 5 then 0 else y
  (← IO.getStdout).putStrLn s!"The answer is {a}"

这是因为嵌套活动会被提升到最近的包含 do 块的规则。if 的分支没有被隐式地包装在 do 块中，因为 if 本身不是 do 块中的语句，语句是定义 a 的 let。事实上，它们不能以这种方式包装，因为条件表达式的类型是 Nat，而非 IO Nat。

Lean 的 #eval 命令可用于执行 IO 活动，而不仅仅是对它们进行求值。通常，向 Lean 文件添加 #eval 命令会让 Lean 求值提供的表达式，然后将结果值转换为字符串，并在工具提示和信息窗口中提供该字符串。#eval 不会因为 IO 活动无法转换为字符串而失败，而是执行它们，并执行它们的副作用。如果执行结果是 Unit 值 ()，则不显示结果字符串，但如果它是可以转换为字符串的类型，则 Lean 会显示结果值。

这意味着，给定 countdown 和 runActions,

#eval runActions (countdown 3)

会显示

3
2
1
Blast off!

这是运行 IO 活动产生的输出，而不是活动本身的不透明表示。换句话说，对于 IO 活动，#eval 既 求值（Evaluate） 提供的表达式，又 执行（Execute） 结果活动值。

使用 #eval 快速测试 IO 动作比编译和运行整个程序方便得多，只是有一些限制。例如，从标准输入读取只会返回空输入。此外，每当 Lean 需要更新它提供给用户的诊断信息时， IO 动作都会重新执行，这可能会在难以预料的时间发生。例如，读取和写入文件的动作可能会在不合适的时间执行。

Lean 函数式编程

其他便利功能

嵌套活动

`do` 的灵活布局

用 `#eval` 运行 `IO` 活动

Lean 函数式编程

其他便利功能

嵌套活动

do 的灵活布局

用 #eval 运行 IO 活动

`do` 的灵活布局

用 `#eval` 运行 `IO` 活动