ch 5 & 6 & 8 & part of 4

lean/extra/01_options.lean

@@ -1,66 +1,56 @@
 /-
-# Extra: Options
-Options are a way to communicate some special configuration to both
-your meta programs and the Lean compiler itself. Basically it's just
-a [`KVMap`](https://github.com/leanprover/lean4/blob/master/src/Lean/Data/KVMap.lean)
-which is a simple map from `Name` to a `Lean.DataValue`. Right now there
-are 6 kinds of data values:
+# 额外内容：选项
+
+选项（Option）是一种向元程序和 Lean 编译器传达一些特殊配置的方法。基本上它只是一个 [`KVMap`](https://github.com/leanprover/lean4/blob/master/src/Lean/Data/KVMap.lean)，这是一个从 `Name` 到 `Lean.DataValue` 的简单映射。目前有 6 种数据值：
 - `String`
 - `Bool`
 - `Name`
 - `Nat`
 - `Int`
 - `Syntax`
 
-Setting an option to tell the Lean compiler to do something different
-with your program is quite simple with the `set_option` command:
+通过 `set_option` 命令设置一个选项，告诉 Lean 编译器对程序做一些不同的处理是非常简单的：
 -/
 
 import Lean
 open Lean
 
 #check 1 + 1 -- 1 + 1 : Nat
 
-set_option pp.explicit true -- No custom syntax in pretty printing
+set_option pp.explicit true -- 在美观打印中不使用通常的语法
 
 #check 1 + 1 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) 1 1 : Nat
 
 set_option pp.explicit false
 
 /-!
-You can furthermore limit an option value to just the next command or term:
+你还可以将选项值限制为仅适用于下一个命令或表达式：
 -/
 
 set_option pp.explicit true in
 #check 1 + 1 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) 1 1 : Nat
 
 #check 1 + 1 -- 1 + 1 : Nat
 
-#check set_option trace.Meta.synthInstance true in 1 + 1 -- the trace of the type class synthesis for `OfNat` and `HAdd`
+#check set_option trace.Meta.synthInstance true in 1 + 1 -- 显示类型类合成 `OfNat` 和 `HAdd` 的途径
 
 /-!
-If you want to know which options are available out of the Box right now
-you can simply write out the `set_option` command and move your cursor
-to where the name is written, it should give you a list of them as auto
-completion suggestions. The most useful group of options when you are
-debugging some meta thing is the `trace.` one.
-
-## Options in meta programming
-Now that we know how to set options, let's take a look at how a meta program
-can get access to them. The most common way to do this is via the `MonadOptions`
-type class, an extension to `Monad` that provides a function `getOptions : m Options`.
-As of now, it is implemented by:
+如果你想知道目前有哪些选项可用，你可以直接码出 `set_option` 空一格然后编辑器会自动弹出代码建议。在调试某些元程序时，最有用的一类选项是 `trace.`。
+
+## 元编程中的选项
+现在我们已经知道如何设置选项了，接下来我们来看一下元程序如何访问这些选项。最常见的方法是通过 `MonadOptions` 类型类，这个类扩展了 `Monad`，提供了一个函数 `getOptions : m Options`。目前，它在以下类型中得到了实现：
 - `CoreM`
 - `CommandElabM`
 - `LevelElabM`
-- all monads to which you can lift operations of one of the above (e.g. `MetaM` from `CoreM`)
+- 所有可以提升上述某个类型操作的 monad（例如 `MetaM` 是从 `CoreM` 提升的）
 
-Once we have an `Options` object, we can query the information via `Options.get`.
-To show this, let's write a command that prints the value of `pp.explicit`.
+一旦我们有了 `Options` 对象，我们就可以通过 `Options.get` 查询相关信息。
+为了演示这一点，让我们编写一个命令来打印 `pp.explicit` 的值。
 -/
+
 elab "#getPPExplicit" : command => do
   let opts ← getOptions
-  -- defValue = default value
+  -- defValue = default value 默认值
   logInfo s!"pp.explicit : {opts.get pp.explicit.name pp.explicit.defValue}"
 
 #getPPExplicit -- pp.explicit : false
@@ -69,12 +59,10 @@ set_option pp.explicit true in
 #getPPExplicit -- pp.explicit : true
 
 /-!
-Note that the real implementation of getting `pp.explicit`, `Lean.getPPExplicit`,
-uses whether `pp.all` is set as a default value instead.
+注意到，获取 `pp.explicit` 的实际实现 `Lean.getPPExplicit` 使用了 `pp.all` 是否被设置作为默认值。
 
-## Making our own
-Declaring our own option is quite easy as well. The Lean compiler provides
-a macro `register_option` for this. Let's see it in action:
+## 自定义选项
+声明我们自己的选项也非常简单。Lean 编译器提供了一个宏 `register_option` 来实现这一功能。让我们来看一下它的用法：
 -/
 
 register_option book.myGreeting : String := {
@@ -84,6 +72,5 @@ register_option book.myGreeting : String := {
 }
 
 /-!
-However, we cannot just use an option that we just declared in the same file
-it was declared in because of initialization restrictions.
+然而，我们不能在声明选项的同一个文件中直接使用它，因为有初始化的限制。
 -/

lean/main/01_intro.lean

@@ -14,37 +14,38 @@
 
 本书试着为DSL和策略建立足够的上下文来使你理解它们。章节依赖关系如下：
 
-* 「证明策略」建立在「宏」和「繁饰」之上
-* 「DSL」建立在「繁饰」之上
-* 「宏」建立在「句法」之上
-* 「繁饰」建立在「句法」和「MetaM」之上
-* 「MetaM」建立在「表达式」之上
+* 「表达式」=>「MetaM」
+* 「语法」=>「宏」
+* 「语法」+「MetaM」=>「繁饰」=>「DSL」
+* 「宏」+「繁饰」=>「证明策略」
 
 证明策略一章之后是包括关键概念和功能概述的备忘录。那之后，是一些章节的额外内容，展示了 Lean 4 元编程的其他应用。大多数章节的末尾都有习题，书的最后是习题答案。
 
 本章的其余部分将简要介绍什么是元编程，并提供一些小示例开胃菜。
 
 注意：代码片段不是自包含的。它们应该从每章的开头开始，以增量方式运行/读取。
 
+> 译注：本书一律将Syntax译为语法，Grammar译为文法。
+
 ## 「元」是什么?
 
-当我们用Python、C、Java或Scala等大多数编程语言编写代码时，通常遵循预定义的句法，否则编译器或解释器将无法理解代码。在Lean中，这些预定义句法是定义归纳类型、实现函数、证明定理等。然后，编译器必须解析代码，构建一个AST（抽象句法树），并将其句法节点阐释为语言内核可以处理的项。我们说编译器执行的这些活动是在**元**层面中完成的，这是本书的内容。我们还说，句法的常见用法是在**对象**层面中完成的。
+当我们用Python、C、Java或Scala等大多数编程语言编写代码时，通常遵循预定义的语法，否则编译器或解释器将无法理解代码。在Lean中，这些预定义语法是定义归纳类型、实现函数、证明定理等。然后，编译器必须解析代码，构建一个AST（抽象语法树），并将其语法节点阐释为语言内核可以处理的项。我们说编译器执行的这些活动是在**元**层面中完成的，这是本书的内容。我们还说，语法的常见用法是在**对象**层面中完成的。
 
 在大多数系统中，元层面活动是用与我们当前用来编写代码的语言不同的语言完成的。在Isabelle中，元层面语言是ML和Scala。在Coq中，它是OCaml。在Agda中，是Haskell。在 Lean 4 中，元代码主要是用 Lean 本身编写的，还有一些用C++编写的组件。
 
-Lean 的一个很酷且方便的地方是，它允许我们用日常在对象层面写 Lean 的方式自定义句法节点，并实现元层面例程。例如，可以编写记号来实例化某种类型的项，并在同一个文件中立即使用它！这个概念通常被称为[**反射**](https://zh.wikipedia.org/wiki/%E5%8F%8D%E5%B0%84%E5%BC%8F%E7%BC%96%E7%A8%8B)。我们可以说，在Lean中，元层面被「反射」到对象层面。
+Lean 的一个很酷且方便的地方是，它允许我们用日常在对象层面写 Lean 的方式自定义语法节点，并实现元层面例程。例如，可以编写记号来实例化某种类型的项，并在同一个文件中立即使用它！这个概念通常被称为[**反射**](https://zh.wikipedia.org/wiki/%E5%8F%8D%E5%B0%84%E5%BC%8F%E7%BC%96%E7%A8%8B)。我们可以说，在Lean中，元层面被「反射」到对象层面。
 
 用Ruby、Python或Javascript等语言做元编程的方式可能是使用预定义的元编程方法来即时定义一些东西。例如，在Ruby中你可以使用 `Class.new` 和 `define_method` 用于在程序执行时即时定义一个新类及其新方法（其中包含新代码！）。
 
 在Lean中，我们通常不需要「即时地」定义新的命令或策略，但是在Lean元编程中能做类似的事，并且同样直接，例如，你可以使用简单的一行 `elab "#help" : command => do ...normal Lean code...`。
 
-然而，在Lean中，我们经常想要直接操作Lean的CST（具体句法树，Lean的 `Syntax` 类型）和Lean的AST（抽象句法树，Lean的 `Expr` 类型），而不是使用「正常的Lean代码」，特别是当我们编写证明策略（Tactic）时。因此，Lean元编程更难掌握。本书的大部分内容都是为了研究这些类型以及我们如何操作它们。
+然而，在Lean中，我们经常想要直接操作Lean的CST（具体语法树，Lean的 `Syntax` 类型）和Lean的AST（抽象语法树，Lean的 `Expr` 类型），而不是使用「正常的Lean代码」，特别是当我们编写证明策略（Tactic）时。因此，Lean元编程更难掌握。本书的大部分内容都是为了研究这些类型以及我们如何操作它们。
 
 ## 元编程示例
 
 下面这些例子仅作为展示。如果您现在不了解细节，请不要担心。
 
-### 引入符号（定义新句法）
+### 引入符号（定义新语法）
 
 通常，人们希望引入新的符号，例如更适合数学（的某分支）的符号。例如，在数学中，人们会将给一个自然数加 `2` 的函数写为 `x : Nat ↦ x + 2` 或简单地写为 `x ↦ x + 2` ，如果可以推断出定义域是自然数。相应的 Lean 定义 `fun x : Nat => x + 2` 和 `fun x => x + 2` 使用 `=>`，这在数学中表示**蕴涵**，因此可能会让一些人感到困惑。
 -/
@@ -92,7 +93,7 @@ elab "#assertType " termStx:term " : " typeStx:term : command =>
 
 /-!
 
-`elab` 启动 `command` 句法的定义。当被编译器解析时，它将触发接下来的计算。
+`elab` 启动 `command` 语法的定义。当被编译器解析时，它将触发接下来的计算。
 
 此时，代码应该在单子 `CommandElabM` 中运行。然后我们使用 `liftTermElabM` 来访问单子 `TermElabM`，这使我们能够使用 `elabType` 和 `elabTermEnsuringType` 从语法节点 `typeStx` 和 `termStx` 构建表达式。
 
@@ -102,9 +103,9 @@ elab "#assertType " termStx:term " : " typeStx:term : command =>
 
 如果到现在为止没有抛出任何错误，则繁饰成功，我们可以使用 `logInfo` 输出 success 。相反，如果捕获到某些错误，则我们使用 `throwError` 并显示相应的消息。
 
-### 构建它的DSL和句法
+### 构建它的DSL和语法
 
-让我们解析一个经典语法，即带有加法、乘法、自然数和变量的算术表达式的语法。我们将定义一个 AST（抽象语法树）来编码表达式的数据，并使用运算符 `+` 和 `*` 来表示构建算术 AST。以下是我们将要解析的 AST：
+让我们解析一个经典文法，即带有加法、乘法、自然数和变量的算术表达式的文法。我们将定义一个 AST（抽象语法树）来编码表达式的数据，并使用运算符 `+` 和 `*` 来表示构建算术 AST。以下是我们将要解析的 AST：
 -/
 
 inductive Arith : Type where
@@ -114,7 +115,7 @@ inductive Arith : Type where
   | var : String → Arith        -- 变量
 
 /-!
-现在我们声明一个句法类别（declare syntax category）来描述我们将要解析的语法。我们通过为 `+` 句法赋予比 `*` 句法更低的优先级权重来控制 `+` 和 `*` 的优先级，这表明乘法比加法绑定得更紧密（数字越高，绑定越紧密）。
+现在我们声明一个语法类别（declare syntax category）来描述我们将要解析的文法。我们通过为 `+` 语法赋予比 `*` 语法更低的优先级权重来控制 `+` 和 `*` 的优先级，这表明乘法比加法绑定得更紧密（数字越高，绑定越紧密）。
 -/
 
 declare_syntax_cat arith

lean/main/02_overview.lean

@@ -7,7 +7,7 @@
 
 ## 与编译器的连接
 
-Lean 中的元编程密切关系到编译步骤 -- 解析、句法分析、转换和代码生成。
+Lean 中的元编程密切关系到编译步骤 -- 解析、语法分析、转换和代码生成。
 
 > Lean 4 是用 Lean 本身重新实现的 Lean 定理证明器。新的编译器生成 C 代码，用户现在可以在 Lean 中实现高效的证明自动化，将其编译为高效的 C 代码，并将其作为插件加载。在 Lean 4 中，用户只需导入 Lean 包即可访问用于实现 Lean 的所有内部数据结构。
 >
@@ -23,17 +23,17 @@ Lean 编译过程可以总结为下图：
 
 因此，编译器看到一串 Lean 代码，例如 `"let a := 2"`，然后展开以下过程：
 
-1. **应用相关句法规则** (`"let a := 2"` ➤ `Syntax`)
+1. **应用相关语法规则** (`"let a := 2"` ➤ `Syntax`)
 
-在解析步骤中，Lean 尝试将一串 Lean 代码与声明的**句法规则**之一进行匹配，以便将该字符串转换为 `Syntax` 对象。**句法规则**基本上是美化的正则表达式 -- 当您编写与某个**句法规则**的正则表达式匹配的 Lean 字符串时，该规则将用于处理后续步骤。
+在解析步骤中，Lean 尝试将一串 Lean 代码与声明的**语法规则**之一进行匹配，以便将该字符串转换为 `Syntax` 对象。**语法规则**基本上是美化的正则表达式 -- 当您编写与某个**语法规则**的正则表达式匹配的 Lean 字符串时，该规则将用于处理后续步骤。
 
 2. **循环应用所有宏** (`Syntax` ➤ `Syntax`)
 
 在繁饰步骤中，每个**宏**只是将现有的 `Syntax` 对象转换为某个新的 `Syntax` 对象。然后，新的 `Syntax` 以类似的方式处理（重复步骤 1 和 2），直到没有更多**宏**可应用。
 
 3. **应用单个 elab** (`Syntax` ➤ `Expr`)
 
-最后，是时候为你的句法注入意义了 -- Lean 通过 `name` 参数找到与相应**句法规则**匹配的 **elab**（**句法规则**、**宏** 和 **elabs** 都有此参数，并且它们必须匹配）。新发现的 **elab** 返回特定的 `Expr` 对象。
+最后，是时候为你的语法注入意义了 -- Lean 通过 `name` 参数找到与相应**语法规则**匹配的 **elab**（**语法规则**、**宏** 和 **elabs** 都有此参数，并且它们必须匹配）。新发现的 **elab** 返回特定的 `Expr` 对象。
 
 这样就完成了繁饰步骤。​​
 
@@ -69,9 +69,9 @@ Lean 编译过程可以总结为下图：
 
 在上图中，您可以看到 `notation`、`prefix`、`infix` 和 `postfix` -- 所有这些都是 `syntax` 和 `@[macro xxx] def ourMacro` 的组合，就像 `macro` 一样。这些命令与 `macro` 不同，因为您只能用它们定义特定形式的语法。
 
-所有这些命令都在 Lean 和 Mathlib 源代码中广泛使用，最好记住。然而，它们中的大多数都是语法糖，您可以通过研究以下 3 个低级命令的行为来了解它们的行为：`syntax`（**句法规则**）、`@[macro xxx] def ourMacro`（**宏**）和 `@[command_elab xxx] def ourElab`（**elab**，繁饰 elaborate 的简写）。
+所有这些命令都在 Lean 和 Mathlib 源代码中广泛使用，最好记住。然而，它们中的大多数都是语法糖，您可以通过研究以下 3 个低级命令的行为来了解它们的行为：`syntax`（**语法规则**）、`@[macro xxx] def ourMacro`（**宏**）和 `@[command_elab xxx] def ourElab`（**elab**，繁饰 elaborate 的简写）。
 
-举一个更具体的例子，假设我们正在实现一个 `#help` 命令，也可以写成 `#h`。然后我们可以按如下方式编写我们的**句法规则**、**宏**和**elab**：
+举一个更具体的例子，假设我们正在实现一个 `#help` 命令，也可以写成 `#h`。然后我们可以按如下方式编写我们的**语法规则**、**宏**和**elab**：
 
 <p align="center">
 <img width="900px" src="https://github.com/lakesare/lean4-metaprogramming-book/assets/7578559/adc1284f-3c0a-441d-91b8-7d87b6035688"/>
@@ -83,7 +83,7 @@ Lean 编译过程可以总结为下图：
 
 如果我们写 `#help "#explode"`，Lean 将遵循 `syntax (name := default_h)` ➤ `@[command_elab default_h] def helpElab` 路径。
 
-请注意，**句法规则**、**宏** 和 **elab** 之间的匹配是通过 `name` 参数完成的。如果我们使用 `macro_rules` 或其他语法糖，Lean 将自行找出适当的 `name` 参数。
+请注意，**语法规则**、**宏** 和 **elab** 之间的匹配是通过 `name` 参数完成的。如果我们使用 `macro_rules` 或其他语法糖，Lean 将自行找出适当的 `name` 参数。
 
 如果我们定义的不是命令，我们可以写 `: term`、`: tactic` 或任何其他语法类别来替换 `: command`。
 elab 函数也可以是不同的类型，例如用于实现 `#help` 的 `CommandElab` 还有 `TermElab` 和 `Tactic`:
@@ -94,7 +94,7 @@ elab 函数也可以是不同的类型，例如用于实现 `#help` 的 `Command
 
 这对应于我们对 Lean 中的项、命令和策略的直观理解 -- 项在执行时返回特定值，命令修改环境或打印某些内容，策略修改证明状态。
 
-## 执行顺序：句法规则、宏、elab
+## 执行顺序：语法规则、宏、elab
 
 上面是这三个基本命令的执行流程，现在明确地阐述一下。执行顺序遵循以下伪代码模板：`syntax (macro; syntax)* elab`。