TOML🔗

Lake.Toml 常用于配置文件。Lean 4 提供了一个用于处理 Lake.Toml 的模块。本章介绍如何在 Lean 中创建、操作和持久化 Lake.Toml 数据。

在 Lean 中处理 TOML 需要理解两个主要类型：

• Table：本质上是一个从键到值的映射（字典）。当你解析一个 TOML 字符串时，得到的是一个 Table。

• Value：这是一个归纳类型，可以是字符串、整数、布尔值、数组或另一个表。

  • 为什么 Value 很重要：Table 把键映射到值，但这些值可以是任意类型（先是字符串，再是数字，然后是嵌套表）。在 Lean 中，一个映射的所有值必须是同一种类型。Value 充当统一的封装类型，让我们能在同一个 Table 中存放不同类型的数据。

• Syntax 与 .missing：Lean 中大多数 TOML 类型都携带一个 Lean.Syntax 对象。它用于追踪值在源文件中的确切位置，以便提供更好的错误报告。

  • 为什么 .missing 很重要：当我们以编程方式（而非从文件）创建 TOML 值时，没有可指向的“源代码行”。我们使用 Lean.Syntax.missing（或简写 .missing）来满足类型系统的要求，而不必提供一个虚构的源位置。

处理 Lake.Toml 不像处理 Json 那样直接，但接下来的各节会提供有效处理 TOML 数据所需的工具。

配方：

1. 解析 TOML
2. 访问与修改 TOML
3. 嵌套 TOML 与表数组
4. 读写 TOML 文件
5. JSON 与 TOML 互转
6. 处理 lakefile.toml