Function that tries to reverse macro expansions as a post-processing step of delaboration.
While less general than an arbitrary delaborator, it can be declared without importing Lean.
Used by the [app_unexpander] attribute.
23.8. 扩展Lean的输出
用新语法扩展Lean，并通过宏和精化器实现新语法，使用户可以更方便地向Lean表达想法。 然而，Lean 是一个交互式 定理证明器：它提供的反馈易于理解也很重要。 语法扩展应该在output 和input 中使用。
有两种主要机制可用于指示 Lean 在其输出中使用语法扩展：
- 解扩展器
解扩展器是 宏 的逆。 宏通过翻译根据旧语法实现新语法，将新功能扩展为预先存在的功能的编码。 与宏一样，unexpanders 将
Syntax翻译为Syntax；与宏不同，它们将编码转换为新的扩展。- 精化器
Delaborators 是 elaborators 的逆。 虽然 elaborators 将
Syntax翻译为核心类型论的Expr，但 delaborators 将Expr翻译为Syntax。
在显示 Expr 之前，首先对其进行细化，然后取消展开。
精化器跟踪其输出源自的原始 Expr 中的位置；该位置在生成的语法 SourceInfo 中进行编码。
正如宏展开自动使用与原始语法位置相对应的合成源信息来注释生成的语法，解扩展机制保留生成的语法与基础 Expr 的关联。
此关联启用 Lean 的交互功能，当结果语法显示在 证明状态 和诊断中时，该功能提供有关结果语法的信息。
23.8.1. 解扩展器
正如宏注册在将 语法种类 映射到宏实现的表中一样，解扩展器也注册在将常量名称映射到解扩展器实现的表中。 Lean 在向用户显示语法之前，会尝试根据此表重写语法中常量的每个应用。 非应用程序的上下文出现被视为具有零参数的应用程序。
反膨胀是从内到外进行的。
在参数被解展开后，解展开器将传递应用程序的语法，并隐藏隐式参数。
如果选项 pp.explicit 是 true 或 pp.notation 是 false，则不使用解扩展器。
解扩展器的类型为 Lean.PrettyPrinter.Unexpander，它是 Syntax → Lean.PrettyPrinter.UnexpandM Syntax 的缩写。
在本节的其余部分中，名称 Unexpander 和 UnexpandM 不合格地使用。
UnexpandM 是一个通过其 MonadQuotation 和 MonadExcept Unit 实例支持报价和失败的 monad。
解展开器应该返回未展开的语法，或者使用 throw () 失败。
如果解展开成功，则生成的语法将再次解展开；如果失败，则尝试下一个解扩展器。
当该语法没有成功的解展开器时，其子节点将被解展开，直到所有解展开的机会都用尽为止。
def
def
通过应用 app_unexpander 属性来注册常量的解扩展器。
自定义运算符 和 符号 自动为其引入的语法创建解展开器。
Custom Unit Type
与 Unit 等效的类型，但具有自己的表示法，可以定义为零字段结构和宏：
structure Solo where
mk ::
syntax "‹" "›" : term
macro_rules
| `(term|‹›) => ``(Solo.mk)
虽然新的符号可用于编写定理陈述，但它不会出现在证明状态中。
例如，当证明Solo类型的所有值都等于‹›时，初始证明状态为：
此证明状态显示使用 结构实例 语法的构造函数。
解扩展器可用于覆盖此选择。
由于 Solo.mk 不能应用于任何参数，因此解展开器可以忽略语法，该语法始终为 `(Solo.mk)。
@[app_unexpander Solo.mk]
def unexpandSolo : Lean.PrettyPrinter.Unexpander
| _ => `(‹›)
有了这个解展开器，证明的初始状态现在用正确的语法呈现：
Unexpansion and Arguments
ListCursor 表示 List 中的位置。
ListCursor.before 包含该位置之前的元素的反向列表，ListCursor.after 包含该位置之后的元素。
structure ListCursor (α) where
before : List α
after : List α
deriving Repr
列表光标可以向左或向右移动：
def ListCursor.left : ListCursor α → Option (ListCursor α)
| ⟨[], _⟩ => none
| ⟨l :: ls, rs⟩ => some ⟨ls, l :: rs⟩
def ListCursor.right : ListCursor α → Option (ListCursor α)
| ⟨_, []⟩ => none
| ⟨ls, r :: rs⟩ => some ⟨r :: ls, rs⟩
它们也可以一直向左或一直向右移动：
def ListCursor.rewind : ListCursor α → ListCursor α
| xs@⟨[], _⟩ => xs
| ⟨l :: ls, rs⟩ => rewind ⟨ls, l :: rs⟩
termination_by xs => xs.before
def ListCursor.fastForward : ListCursor α → ListCursor α
| xs@⟨_, []⟩ => xs
| ⟨ls, r :: rs⟩ => fastForward ⟨r :: ls, rs⟩
termination_by xs => xs.after
但是，需要反转先前元素的列表可能会使列表游标难以理解。
可以为光标指定一个符号，其中标志 (🚩) 标记光标在列表中的位置：
syntax "[" term,* " 🚩 " term,* "]": term
macro_rules
| `([$ls,* 🚩 $rs,*]) =>
``(ListCursor.mk [$[$((ls : Array Lean.Term).reverse)],*] [$rs,*])
在宏中，元素序列的类型为 Syntax.TSepArray `term ","。
Array Lean.Term 的类型注释会引发强制转换，以便可以应用 Array.reverse，并且类似的强制转换会重新插入分隔逗号。
这些强制转换在 类型化语法 部分中进行了描述。
虽然该语法有效，但 Lean 的输出中未使用它：
#check [1, 2, 3 🚩 4, 5]
解扩展器可以解决这个问题。 解展开器依赖于已重写两个列表的列表文字的内置解展开器：
@[app_unexpander ListCursor.mk]
def unexpandListCursor : Lean.PrettyPrinter.Unexpander
| `($_ [$ls,*] [$rs,*]) =>
`([$((ls : Array Lean.Term).reverse),* 🚩 $(rs),*])
| _ => throw ()
#check [1, 2, 3 🚩 4, 5]
#reduce [1, 2, 3 🚩 4, 5].right
#reduce [1, 2, 3 🚩 4, 5].left >>= (·.left)
23.8.2. 精化器
解析器是 Lean.PrettyPrinter.Delaborator.Delab 类型的函数，它是 Lean.PrettyPrinter.Delaborator.DelabM Term 的缩写。
与解展开器不同，解展开器不是作为函数实现的。
这是为了更容易正确实现它们：monad DelabM 跟踪正在详细说明的表达式中的当前位置，以便详细说明机制可以注释生成的语法。
解析器使用 delab 属性注册。
内部表将 Expr（不带命名空间）的构造函数的名称映射到 delaborators。
此外，参考名称 app.c 来查找常量 c 的应用程序的解释器，并参考名称 mdata.k 来查找 Expr.mdata 构造函数的解释器，其元数据。
attributeDelaborator Registration
delab 属性为 Expr 的指示构造函数或元数据键注册一个解析器。
attr ::= ... | delab ident
app_delab 属性在当前 范围 中的 解析 后为指示常量的应用程序注册一个解释器。
attr ::= ...
| `@[app_delab c]` registers a delaborator for applications with head constant `c`.
Such delaborators also apply to the constant `c` itself (known as a "nullary application").
This attribute should be applied to definitions of type `Lean.PrettyPrinter.Delaborator.Delab`.
When defining delaborators for constant applications, one should prefer this attribute over `@[delab app.c]`,
as `@[app_delab c]` first performs name resolution on `c` in the current scope.
monad DelabM 是一个 reader monad，其中包括对 Expr 中当前位置的访问。
递归精化是通过调整读取器单子的跟踪位置来执行的，而不是通过显式地将子表达式传递给另一个函数来执行。
在解析器中处理子表达式的最重要的函数位于命名空间 Lean.PrettyPrinter.Delaborator.SubExp 中：
-
getExpr检索当前表达式进行分析。 -
withAppFn将当前位置调整为应用程序中函数的位置。 -
withAppArg将当前位置调整为应用程序中参数的位置 -
withAppFnArgs将当前表达式分解为非应用程序函数及其参数，重点关注每个函数。 -
withBindingBody下降到函数或函数类型的主体。
可以使用更多函数深入 Expr 的其余构造函数。