ch extra3

Author: subfish-zhou

lean/extra/03_pretty-printing.lean

@@ -1,48 +1,28 @@
-/- # Extra: Pretty Printing
-The pretty printer is what Lean uses to present terms that have been
-elaborated to the user. This is done by converting the `Expr`s back into
-`Syntax` and then even higher level pretty printing datastructures. This means
-Lean does not actually recall the `Syntax` it used to create some `Expr`:
-there has to be code that tells it how to do that.
-In the big picture, the pretty printer consists of three parts run in the
-order they are listed in:
-
-- the **[delaborator](https://github.com/leanprover/lean4/tree/master/src/Lean/PrettyPrinter/Delaborator)**
-  this will be our main interest since we can easily extend it with our own code.
-  Its job is to turn `Expr` back into `Syntax`.
-- the **[parenthesizer](https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Parenthesizer.lean)**
-  responsible for adding parenthesis into the `Syntax` tree, where it thinks they would be useful
-- the **[formatter](https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Formatter.lean)**
-  responsible for turning the parenthesized `Syntax` tree into a `Format` object that contains
-  more pretty printing information like explicit whitespaces
-
-## Delaboration
-As its name suggests, the delaborator is in a sense the opposite of the
-elaborator. The job of the delaborator is to take an `Expr` produced by
-the elaborator and turn it back into a `Syntax` which, if elaborated,
-should produce an `Expr` that behaves equally to the input one.
-
-Delaborators have the type `Lean.PrettyPrinter.Delaborator.Delab`. This
-is an alias for `DelabM Syntax`, where `DelabM` is the delaboration monad.
-All of this machinery is defined [here](https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Delaborator/Basic.lean).
-`DelabM` provides us with quite a lot of options you can look up in the documentation
-(TODO: Docs link). We will merely highlight the most relevant parts here.
-
-- It has a `MonadQuotation` instance which allows us to declare `Syntax` objects
-  using the familiar quotation syntax.
-- It can run `MetaM` code.
-- It has a `MonadExcept` instance for throwing errors.
-- It can interact with `pp` options using functions like `whenPPOption`.
-- You can obtain the current subexpression using `SubExpr.getExpr`. There is
-  also an entire API defined around this concept in the `SubExpr` module.
-
-### Making our own
-Like so many things in metaprogramming the elaborator is based on an attribute,
-in this case the `delab` one. `delab` expects a `Name` as an argument,
-this name has to start with the name of an `Expr` constructor, most commonly
-`const` or `app`. This constructor name is then followed by the name of the
-constant we want to delaborate. For example, if we want to delaborate a function
-`foo` in a special way we would use `app.foo`. Let's see this in action:
+/- # 额外内容：美观打印
+Lean 的美观打印器用于向用户呈现已繁饰的术语。这是通过将 `Expr` 转换回 `Syntax`，然后再转换为更高级的美观打印数据结构来完成的。这意味着 Lean 实际上不会记住它用来创建某些 `Expr` 的 `Syntax`：必须有代码告诉它如何执行此操作。
+
+从宏观角度来看，美观打印器由三个部分组成，按列出的顺序运行：
+
+- **[反繁饰器](https://github.com/leanprover/lean4/tree/master/src/Lean/PrettyPrinter/Delaborator)**
+  这是我们主要感兴趣的部分，因为我们可以轻松地用自己的代码扩展它。它的任务是将 `Expr` 转换回 `Syntax`。
+- **[括号添加器](https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Parenthesizer.lean)**
+  负责在 `Syntax` 树中添加括号，它认为在某些地方括号会有帮助。
+- **[格式化器](https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Formatter.lean)**
+  负责将加了括号的 `Syntax` 树转换为包含更多美观打印信息（如显式空格）的 `Format` 对象。
+
+## 反繁饰
+顾名思义，反繁饰器在某种意义上是繁饰器的反面。反繁饰器的任务是将由繁饰器生成的 `Expr` 转换回 `Syntax`，如果再次繁饰，应该生成一个与输入行为相同的 `Expr`。
+
+反繁饰器的类型是 `Lean.PrettyPrinter.Delaborator.Delab`。这是 `DelabM Syntax` 的别名，其中 `DelabM` 是反繁饰 monad。所有这些机制都定义在[这里](https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Delaborator/Basic.lean)。`DelabM` 为我们提供了很多选项，您可以在文档中查看（TODO：文档链接）。这里我们只强调最相关的部分。
+
+- 它有一个 `MonadQuotation` 实例，允许我们使用熟悉的引用语法声明 `Syntax` 对象。
+- 它可以运行 `MetaM` 代码。
+- 它有一个 `MonadExcept` 实例用于抛出错误。
+- 它可以使用 `whenPPOption` 等函数与 `pp` 选项交互。
+- 您可以使用 `SubExpr.getExpr` 获取当前的子表达式。`SubExpr` 模块中还围绕这个概念定义了整个 API。
+
+### 创建我们自己的反繁饰器
+像元编程中的许多事情一样，反繁饰器基于属性，在这种情况下是 `delab` 属性。`delab` 期望以 `Name` 作为参数，这个名称必须以 `Expr` 构造函数的名称开头，最常见的是 `const` 或 `app`。此构造函数名称后面跟着我们想要反繁饰的常量名称。例如，如果我们想以特殊方式反繁饰函数 `foo`，我们将使用 `app.foo`。让我们来看一下实际操作：
 -/
 
 import Lean
@@ -56,12 +36,10 @@ def delabFoo : Delab := do
   `(1)
 
 #check foo -- 1 : Nat → Nat
-#check foo 13 -- 1 : Nat, full applications are also pretty printed this way
+#check foo 13 -- 1 : Nat, 整个应用同样被这样打印出来了
 
 /-!
-This is obviously not a good delaborator since reelaborating this `Syntax`
-will not yield the same `Expr`. Like with many other metaprogramming
-attributes we can also overload delaborators:
+这显然不是一个好的反繁饰器，因为重新繁饰此 `Syntax` 不会产生相同的 `Expr`。像许多其他元编程属性一样，我们也可以重载反繁饰器：
 -/
 
 @[delab app.foo]
@@ -71,65 +49,48 @@ def delabfoo2 : Delab := do
 #check foo -- 2 : Nat → Nat
 
 /-!
-The mechanism for figuring out which one to use is the same as well. The
-delaborators are tried in order, in reverse order of registering, until one
-does not throw an error, indicating that it "feels unresponsible for the `Expr`".
-In the case of delaborators, this is done using `failure`:
+确定使用哪个反繁饰器的机制也是相同的。反繁饰器按照注册的相反顺序依次尝试，直到其中一个没有抛出错误，表明它「不对这个 `Expr` 负责」。在反繁饰器的情况下，这是通过使用 `failure` 来完成的：
 -/
 
 @[delab app.foo]
 def delabfoo3 : Delab := do
   failure
   `(3)
 
-#check foo -- 2 : Nat → Nat, still 2 since 3 failed
+#check foo -- 2 : Nat → Nat, 还是 2 因为 3 失败了
 
 /-!
-In order to write a proper delaborator for `foo`, we will have to use some
-slightly more advanced machinery though:
+为了为 `foo` 编写一个合适的反繁饰器，我们将不得不使用一些稍微高级一点的机制：
 -/
 
 @[delab app.foo]
 def delabfooFinal : Delab := do
   let e ← getExpr
-  guard $ e.isAppOfArity' `foo 1 -- only delab full applications this way
+  guard $ e.isAppOfArity' `foo 1 -- 只能像这样反繁饰整个应用
   let fn := mkIdent `fooSpecial
   let arg ← withAppArg delab
   `($fn $arg)
 
 #check foo 42 -- fooSpecial 42 : Nat
-#check foo -- 2 : Nat → Nat, still 2 since 3 failed
+#check foo -- 2 : Nat → Nat, 还是 2 因为 3 失败了
 
 /-!
-Can you extend `delabFooFinal` to also account for non full applications?
-
-## Unexpanders
-While delaborators are obviously quite powerful it is quite often not necessary
-to use them. If you look in the Lean compiler for `@[delab` or rather `@[builtin_delab`
-(a special version of the `delab` attribute for compiler use, we don't care about it),
-you will see there are quite few occurrences of it. This is because the majority
-of pretty printing is in fact done by so called unexpanders. Unlike delaborators
-they are of type `Lean.PrettyPrinter.Unexpander` which in turn is an alias for
-`Syntax → Lean.PrettyPrinter.UnexpandM Syntax`. As you can see, they are
-`Syntax` to `Syntax` translations, quite similar to macros, except that they
-are supposed to be the inverse of macros. The `UnexpandM` monad is quite a lot
-weaker than `DelabM` but it still has:
-
-- `MonadQuotation` for syntax quotations
-- The ability to throw errors, although not very informative ones: `throw ()`
-  is the only valid one
-
-Unexpanders are always specific to applications of one constant. They are registered
-using the `app_unexpander` attribute, followed by the name of said constant. The unexpander
-is passed the entire application of the constant after the `Expr` has been delaborated,
-without implicit arguments. Let's see this in action:
+你能扩展 `delabFooFinal` 来处理非完整应用的情况吗？
+
+## 反扩展器
+虽然反繁饰器非常强大，但很多情况下并不需要使用它们。如果你查看 Lean 编译器中的 `@[delab` 或 `@[builtin_delab`（编译器使用的 `delab` 属性的特殊版本，我们对此不关心），你会发现它们的出现次数很少。这是因为大多数美观打印实际上是由所谓的反扩展器完成的。与反繁饰器不同，反扩展器的类型是 `Lean.PrettyPrinter.Unexpander`，这实际上是 `Syntax → Lean.PrettyPrinter.UnexpandM Syntax` 的别名。正如你所看到的，它们是 `Syntax` 到 `Syntax` 的转换，类似于宏，区别在于它们应该是宏的逆向操作。`UnexpandM` monad 比 `DelabM` 弱得多，但它仍然具有：
+
+- 支持语法引用的 `MonadQuotation`
+- 能够抛出错误，尽管错误信息并不十分详细：`throw ()` 是唯一有效的错误
+
+反扩展器始终针对一个常量的应用进行。它们通过 `app_unexpander` 属性注册，后面跟着该常量的名称。反扩展器在 `Expr` 经过反繁饰后被传递整个常量应用，而不包含隐式参数。让我们看看这个过程如何操作：
 -/
 
 def myid {α : Type} (x : α) := x
 
 @[app_unexpander myid]
 def unexpMyId : Unexpander
-  -- hygiene disabled so we can actually return `id` without macro scopes etc.
+  -- 禁用语法卫生，这样我们实际上可以返回 `id`，而不涉及宏范围等。
   | `(myid $arg) => set_option hygiene false in `(id $arg)
   | `(myid) => pure $ mkIdent `id
   | _ => throw ()
@@ -138,15 +99,10 @@ def unexpMyId : Unexpander
 #check myid -- id : ?m.3870 → ?m.3870
 
 /-!
-For a few nice examples of unexpanders you can take a look at
-[NotationExtra](https://github.com/leanprover/lean4/blob/master/src/Init/NotationExtra.lean)
-
-### Mini project
-As per usual, we will tackle a little mini project at the end of the chapter.
-This time we build our own unexpander for a mini programming language.
-Note that many ways to define syntax already have generation of the required
-pretty printer code built-in, e.g. `infix`, and `notation` (however not `macro_rules`).
-So, for easy syntax, you will never have to do this yourself.
+关于一些反扩展器的不错示例，你可以查看 [NotationExtra](https://github.com/leanprover/lean4/blob/master/src/Init/NotationExtra.lean)
+
+### 项目示例
+像往常一样，我们将在本章末进行一个迷你项目。这次我们将为一个迷你编程语言构建自己的反扩展器。请注意，许多定义语法的方法已经内置了生成所需的漂亮打印代码，例如 `infix` 和 `notation`（但不包括 `macro_rules`）。因此，对于简单的语法，你不需要自己手动编写这些代码。
 -/
 
 declare_syntax_cat lang
@@ -180,8 +136,7 @@ instance : Coe Ident (TSyntax `lang) where
 ]
 
 /-!
-As you can see, the pretty printing output right now is rather ugly to look at.
-We can do better with an unexpander:
+正如你所见，目前的漂亮打印输出相当难看。我们可以通过使用反扩展器来改进它：
 -/
 
 @[app_unexpander LangExpr.numConst]
@@ -218,7 +173,5 @@ def unexpandLet : Unexpander
 ]
 
 /-!
-That's much better! As always, we encourage you to extend the language yourself
-with things like parenthesized expressions, more data values, quotations for
-`term` or whatever else comes to your mind.
+这样就好多了！一如既往，我们鼓励你自己扩展语言，比如添加带括号的表达式、更多的数据值、对 `term` 的引用，或其他你能想到的内容。
 -/

lean/main/04_metam.lean

@@ -294,7 +294,7 @@ def myAssumption (mvarId : MVarId) : MetaM Bool := do
 
 ### 元变量深度
 
-元变量深度也是一个较为小众的特性，但有时会派上用场。每个元变量都有一个*深度*（一个自然数），并且 `MetavarContext` 也有一个相应的深度。Lean 只有在元变量的深度等于当前 `MetavarContext` 的深度时才会为其赋值。新创建的元变量继承 `MetavarContext` 的深度，因此默认情况下，每个元变量都是可赋值的。
+元变量深度也是一个较为小众的特性，但有时会派上用场。每个元变量都有一个**深度**（一个自然数），并且 `MetavarContext` 也有一个相应的深度。Lean 只有在元变量的深度等于当前 `MetavarContext` 的深度时才会为其赋值。新创建的元变量继承 `MetavarContext` 的深度，因此默认情况下，每个元变量都是可赋值的。
 
 这种机制在某些策略需要一些临时元变量，并且需要确保其他非临时元变量不会被赋值时会很有用。为了实现这一点，策略可以按照以下步骤进行：
 
@@ -305,57 +305,21 @@ def myAssumption (mvarId : MVarId) : MetaM Bool := do
 
 这种模式封装在 `Lean.Meta.withNewMCtxDepth` 中。
 
-### Metavariable Depth
+## 计算
 
-Metavariable depth is also a niche feature, but one that is occasionally useful.
-Any metavariable has a *depth* (a natural number), and a `MetavarContext` has a
-corresponding depth as well. Lean only assigns a metavariable if its depth is
-equal to the depth of the current `MetavarContext`. Newly created metavariables
-inherit the `MetavarContext`'s depth, so by default every metavariable is
-assignable.
+计算是依值类型理论的核心概念。项 `2`、`Nat.succ 1` 和 `1 + 1` 在计算出相同值的意义上是等价的。我们称它们为**定义等价**。从元编程的角度来看，问题在于定义等价的项可能由完全不同的表达式表示，但我们的用户通常期望适用于 `2` 的策略也适用于 `1 + 1`。因此，当我们编写策略时，必须做额外的工作，以确保定义等价的项得到类似的处理。
 
-This setup can be used when a tactic needs some temporary metavariables and also
-needs to make sure that other, non-temporary metavariables will not be assigned.
-To ensure this, the tactic proceeds as follows:
+### 完全标准化
 
-1. Save the current `MetavarContext`.
-2. Increase the depth of the `MetavarContext`.
-3. Perform whatever computation is necessary, possibly creating and assigning
-   metavariables. Newly created metavariables are at the current depth of the
-   `MetavarContext` and so can be assigned. Old metavariables are at a lower
-   depth, so cannot be assigned.
-4. Restore the saved `MetavarContext`, thereby erasing all the temporary
-   metavariables and resetting the `MetavarContext` depth.
+我们能对计算做的最简单的事情就是将项标准化。对于某些数字类型的例外情况，类型为 `T` 的项 `t` 的标准式是 `T` 构造函数的应用序列。例如，列表的标准式是 `List.cons` 和 `List.nil` 的应用序列。
 
-This pattern is encapsulated in `Lean.Meta.withNewMCtxDepth`.
-
-
-## Computation
-
-Computation is a core concept of dependent type theory. The terms `2`, `Nat.succ
-1` and `1 + 1` are all "the same" in the sense that they compute the same value.
-We call them *definitionally equal*. The problem with this, from a
-metaprogramming perspective, is that definitionally equal terms may be
-represented by entirely different expressions, but our users would usually
-expect that a tactic which works for `2` also works for `1 + 1`. So when we
-write our tactics, we must do additional work to ensure that definitionally
-equal terms are treated similarly.
-
-### Full Normalisation
-
-The simplest thing we can do with computation is to bring a term into normal
-form. With some exceptions for numeric types, the normal form of a term `t` of
-type `T` is a sequence of applications of `T`'s constructors. E.g. the normal
-form of a list is a sequence of applications of `List.cons` and `List.nil`.
-
-The function that normalises a term (i.e. brings it into normal form) is
-`Lean.Meta.reduce` with type signature
+将项标准化（即将其带入标准式）的函数是 `Lean.Meta.reduce`，其类型签名为：
 
 ```lean
 reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr
 ```
 
-We can use it like this:
+我们可以这样使用它：
 -/
 
 def someNumber : Nat := (· + 2) $ 3
@@ -367,18 +331,11 @@ def someNumber : Nat := (· + 2) $ 3
 -- Lean.Expr.lit (Lean.Literal.natVal 5)
 
 /-!
-Incidentally, this shows that the normal form of a term of type `Nat` is not
-always an application of the constructors of `Nat`; it can also be a literal.
-Also note that `#eval` can be used not only to evaluate a term, but also to
-execute a `MetaM` program.
-
-The optional arguments of `reduce` allow us to skip certain parts of an
-expression. E.g. `reduce e (explicitOnly := true)` does not normalise any
-implicit arguments in the expression `e`. This yields better performance: since
-normal forms can be very big, it may be a good idea to skip parts of an
-expression that the user is not going to see anyway.
-
-The `#reduce` command is essentially an application of `reduce`:
+顺便说一下，这表明类型为 `Nat` 的项的标准式并不总是 `Nat` 构造函数的应用，它也可以是一个字面量。此外，注意 `#eval` 不仅可以用于计算项，还可以用于执行 `MetaM` 程序。
+
+`reduce` 的可选填参数允许我们跳过表达式的某些部分。例如，`reduce e (explicitOnly := true)` 不会归一化表达式 `e` 中的任何隐式参数。这可以带来更好的性能：由于标准式可能非常庞大，跳过用户无须看到的表达式部分可能是个好主意。
+
+`#reduce` 命令本质上就是 `reduce` 的一个应用：
 -/
 
 #reduce someNumber

lean/main/10_cheat-sheet.lean

@@ -57,7 +57,7 @@ let goal_type ← goal.getType
 * 抛出错误信息：`Lean.Meta.throwTacticEx name mvar message_data`
   其中，`name : Lean.Name` 是策略名，`mvar` 包含错误信息
 
-  用法：`Lean.Meta.throwTacticEx `tac goal (m!"unable to find matching hypothesis of type ({goal_type})")`
+  用法：`Lean.Meta.throwTacticEx` tac goal (m!"unable to find matching hypothesis of type ({goal_type})")`
   其中，`m!` 格式化用于构建 `MessageData`，以便更好地打印项。
 
 TODO: Add?