Display the given message if a is shared, that is, RC(a) > 1
12.2. 引用计数
Lean 使用 引用计数进行内存管理。 每个分配的对象都会维护有多少其他对象引用它的计数。 添加新引用时，计数会增加；删除引用时，计数会递减。 当引用计数达到零时，该对象将不再可访问，并且无法参与程序的进一步执行。 它被释放，并且它对其他对象的所有引用都被删除，这可能会触发进一步的释放。
引用计数提供了许多好处：
- 内存的重用
如果一个对象的引用计数在分配另一个相同大小的对象时降至零，则原始对象的内存可以安全地重新用于新对象。 因此，当要遍历的数据结构只有一个引用时，许多常见的数据结构遍历（例如
List.map）不需要分配内存。- 机会性就地更新
基本类型（例如 strings 和 arrays）可以提供复制共享数据但就地修改非共享数据的操作。 只要它们保留对正在修改的值的唯一引用，对这些基本类型的许多操作都会修改它而不是复制它。 这可以带来显着的性能优势。 精心编写的
Array代码避免了不可变数据结构的性能开销，同时保持纯函数提供的推理简易性。- 可预测性
引用计数会在可预测的时间递减。 因此，引用计数对象可用于管理其他资源，例如文件句柄。 在 Lean 中，
Handle不需要显式关闭，因为当它不再可访问时会立即关闭。- 更简单 FFI
作为回收未使用内存的一部分，不需要重新定位使用引用计数管理的对象。 这极大地简化了与用其他语言（例如 C）编写的代码的交互。
引用计数的传统缺点包括由于更新引用计数而导致的性能开销以及无法识别和释放循环数据。 通过基于“借用”的分析可以最小化前一个缺点，该分析允许省略许多引用计数更新。 然而，多线程代码需要在线程之间同步引用计数更新，这也会带来很大的开销。 为了减少这种开销，Lean 值被分为可从多个线程访问的值和不可访问的值。 单线程引用计数的更新速度比多线程引用计数快得多，并且许多值只能在单个线程上访问。 这些技术共同大大降低了引用计数的性能开销。 由于 Lean 的可验证片段无法创建循环数据，因此 Lean 运行时没有检测它的技术。 Ullrich and de Moura (2019)Sebastian Ullrich and Leonardo de Moura, 2019. “Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming”. In Proceedings of the 31st Symposium on Implementation and Application of Functional Languages (IFL 2019). 提供有关引用计数在 Lean 中实现的更多详细信息。
12.2.1. 观察独特性
确保数组和字符串被唯一引用是在 Lean 中编写快速代码的关键。
原语 dbgTraceIfShared 可用于检查数据结构是否存在别名。
调用时，它返回其参数不变，如果参数的引用计数大于 1，则打印提供的跟踪消息。
由于 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 实现方式的具体情况，将 dbgTraceIfShared 与 Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it.
* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
Users can define `MonadEval` instances to extend the list of supported monads.
The `#eval` command gracefully degrades in capability depending on what is imported.
Importing the `Lean.Elab.Command` module provides full capabilities.
Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
since the presence of `sorry` can lead to runtime instability and crashes.
This check can be overridden with the `#eval! e` command.
Options:
* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
when there is no other way to print the result.
See also: `#reduce e` for evaluation by term reduction.
#eval 一起使用可能会产生误导。
相反，它应该在显式编译和运行的代码中使用。
Observing Uniqueness
该程序读取用户输入的一行，并在用空格替换其第一个字符后打印它。
如果字符串不共享并且字符都包含在 Unicode 的 7 位 ASCII 子集中，则替换字符串中的字符将使用就地更新。
dbgTraceIfShared 调用不执行任何操作，表明该字符串确实会就地更新而不是复制。
def process (str : String) (h : str.startPos ≠ str.endPos) : IO Unit := do
IO.println ((dbgTraceIfShared "String update" str).startPos.set ' ' h)
def main : IO Unit := do
let line := (← (← IO.getStdin).getLine).trimAscii.copy
if h : line.startPos ≠ line.endPos then
process line h
使用此输入运行时：
stdinHere is input.程序发出：
stdout ere is input.具有空的 标准错误 输出：
stderr<empty>
该版本的程序保留了对原始字符串的引用，这需要将调用中的字符串复制到 String.set。
这一事实在其 标准错误 输出中可见。
def process (str : String) (h : str.startPos ≠ str.endPos) : IO Unit := do
IO.println ((dbgTraceIfShared "String update" str).startPos.set ' ' h)
def main : IO Unit := do
let line := (← (← IO.getStdin).getLine).trimAscii.copy
if h : line.startPos ≠ line.endPos then
process line h
IO.println "Original input:"
IO.println line
使用此输入运行时：
stdinHere is input.程序发出：
stdout ere is input.Original input:Here is input.
在其 标准错误 中，传递给 dbgTraceIfShared 的消息是可见的。
stderrshared RC String update12.2.2. 编译器IR
编译器选项 trace.compiler.ir.result 可用于检查函数的编译器中间表示 (IR)。
在此中间表示中，引用计数、分配和重用是明确的：
-
isShared运算符检查引用计数是否为1。 -
ctor_n分配类型的第n个构造函数。 -
proj_n从构造函数值中检索nth 字段。 -
setx[n]改变x中构造函数的nth 字段。 -
retx返回x中的值。
引用计数操作的细节可能取决于优化过程（例如内联）的结果。 虽然绝大多数 Lean 代码不需要这种关注来实现良好的性能，但在编写性能关键型代码时，了解如何诊断独特的引用问题可能非常重要。
option
trace.compiler.ir.result
Default value: false
enable/disable tracing for the given module and submodules
Reference Counts in IR
编译器 IR 可用于观察引用计数何时递增，这有助于诊断预期值具有唯一传入引用但实际上是共享的情况。
这里，process和process'各自以一个字符串作为参数，并用String.set修改它，返回一对字符串。
process 返回常量字符串作为该对的第二个元素，而 process' 返回原始字符串。
set_option trace.compiler.ir.result true
def process (str : String) : String × String :=
(str.set 0 ' ', "")
def process' (str : String) : String × String:=
(str.set 0 ' ', str)
process 的 IR 不包含 inc 或 dec 指令。
如果传入的字符串 x_1 是唯一引用，那么当传递给 String.set 时它仍然是唯一引用，然后可以使用就地修改：
另一方面，process' 的 IR 在调用 String.set 之前递增字符串的引用计数。
因此，修改后的字符串 x_4 是一个副本，无论对 x_1 的原始引用是否唯一：
Memory Reuse in IR
函数 discardElems 是 List.map 的简化版本，它将列表中的每个元素替换为 ()。
检查其中间表示表明，当其引用唯一时，它将重用列表的内存。
set_option trace.compiler.ir.result true
def discardElems : List α → List Unit
| [] => []
| x :: xs => () :: discardElems xs
这会发出以下 IR：
在 IR 中，List.cons 情况显式检查参数值是否共享（即其引用计数是否大于 1）。
如果引用是唯一的，则丢弃的列表元素 x_5 的引用计数将递减，并重用构造函数值。
如果共享，则在 x_11 中为结果分配一个新的 List.cons。