TLAUC: TLA⁺ Unicode 转换器

迈出这一步！从

S^+ == {e \in S : e > 0}
Infinitesimal == \A x \in Real^+: \E y \in Real^+: y < x

迁移到

S⁺ ≜ {e ∈ S : e > 0}
Infinitesimal ≜ ∀ x ∈ ℝ⁺: ∃ y ∈ ℝ⁺: y < x

此软件包将任何 ASCII TLA⁺ 文件的所有符号转换为它们的 Unicode 等效符号，或者将任何 Unicode TLA⁺ 文件的所有符号转换为它们的 ASCII 等效符号。它包含两个 crate：一个库，公开此功能（底层使用 tree-sitter-tlaplus），以及一个命令行包装器。

使用此工具来

• 创建一个看起来很棒、易于阅读的规范副本，同时仍然可以编辑并且可以通过源代码控制有意义地跟踪
• 使用 tlaplus-nvim-plugin 在 Unicode 中自信地编写规范，然后将它们的 ASCII 等效物输出到临时文件以供 SANY 和 TLC 使用
• 将现有的 ASCII 规范转换为 Unicode 并使用它们与像 tla-web 这样的 Unicode 感知工具

请注意，GitHub 本身使用 tree-sitter-tlaplus 语法进行高亮显示，因此它支持如这里高亮显示的代码片段所示的 Unicode TLA⁺。如果您想在源代码控制中检查 Unicode 规范，并在 CI 流程中运行非 Unicode 感知工具如 TLC，您可以通过添加使用此工具将 Unicode 规范转换为 TLC 支持的格式的步骤来做到这一点。

符号映射可以在 ./resources/tla-unicode.csv 文件中找到，该文件来自 tlaplus-standard 仓库。该 crate 还提供了对这些映射的程序访问。为了获得最佳的 TLA⁺ Unicode 体验，您需要一个等宽字体来渲染所有这些符号。

安装 & 使用

此 crate 包含一个库及其命令行包装器。

要获取命令行工具，可以直接从 发布版 下载，或使用 cargo 安装。

1. 安装 rust: https://rust-lang.net.cn/tools/install
2. 运行以下命令以安装 tlauc：
3. 确保 cargo 安装目录 已添加到您的路径中

从命令行开始，按照以下步骤将 TLA⁺ 文件从 ASCII 转换为 Unicode：

tlauc Ascii.tla

就地从 Unicode 转换为 ASCII

tlauc Unicode.tla --ascii

若要将输出保存到单独的文件而不是覆盖输入，请使用 --output 或 -o 参数和一个文件路径。在转换过程中执行了几个安全检查，例如输入规范是否正确解析以及输出规范是否与输入规范具有相同的解析树。您可以使用 --force 或 -f 标志来覆盖这些安全检查。

如果存在解析错误，它们的位置将以最佳尝试列表的形式输出行号。不幸的是，tree-sitter 目前没有提供更高级的解析错误报告。

要使用库，请将 tlauc 包 添加到项目的依赖项中，然后按照以下方式使用它：

use tlauc::{rewrite, Mode};

fn main() {
    let input = r#"---- MODULE TotalOrder ----
EXTENDS Reals

Reflexive(S) == \A a \in S : a <= a
Transitive(S) == \A a, b, c \in S : (a <= b /\ b <= c) => (a <= c)
Antisymmetric(S) == \A a, b \in S : (a <= b /\ a >= b) => (a = b)
Total(S) == \A a, b \in S : a <= b \/ a >= b
IsTotallyOrdered(S) ==
    /\ Reflexive(S)
    /\ Transitive(S)
    /\ Antisymmetric(S)
    /\ Rotal(S)
THEOREM RealsTotallyOrdered == IsTotallyOrdered(Real)
===="#;
    println!("{}", rewrite(input, &Mode::AsciiToUnicode, false).unwrap());
}

这将输出：

---- MODULE TotalOrder ----
EXTENDS Reals

Reflexive(S) ≜ ∀ a ∈ S : a ≤ a
Transitive(S) ≜ ∀ a, b, c ∈ S : (a ≤ b ∧ b ≤ c) ⇒ (a ≤ c)
Antisymmetric(S) ≜ ∀ a, b ∈ S : (a ≤ b ∧ a ≥ b) ⇒ (a = b)
Total(S) ≜ ∀ a, b ∈ S : a ≤ b ∨ a ≥ b
IsTotallyOrdered(S) ≜
    ∧ Reflexive(S)
    ∧ Transitive(S)
    ∧ Antisymmetric(S)
    ∧ Total(S)
THEOREM RealsTotallyOrdered ≜ IsTotallyOrdered(ℝ)
====

错误处理和读取/写入文件的细节留给用户，但您可以查看命令行包装器的示例。

按照以下方式访问 Unicode 映射列表：

use tlauc::{SymbolMapping, get_unicode_mappings};

fn main() {
    let mappings: Vec<SymbolMapping> = get_unicode_mappings();
    println!("{:#?}", mappings);
}

构建 & 测试

1. 安装 Rust：https://rust-lang.net.cn/tools/install
2. 使用 --recurse-submodules 参数克隆存储库
3. 运行 cargo build
4. 运行 cargo test

详细信息

TLA⁺ 通常有多个 ASCII 符号表示相同的操作符（例如，<=、=< 和 \leq）；这些都将映射到相同的 Unicode 符号（≤），并且在映射回 ASCII 时将使用分号分隔的 CSV 单元格中的第一个 ASCII 符号（<=）。

这个程序不仅仅是一个简单的搜索和替换的原因是，对于某些 TLA⁺ 构造（特别是连接和析取列表，以下简称 jlists），空白空间和列对齐很重要。

def == /\ A
       /\ \/ B
          \/ C
       /\ D

如果我们天真地将每个 ASCII 符号替换为其 Unicode 等效符号，我们最终会得到：

def ≜ ∧ A
       ∧ ∨ B
          ∨ C
       ∧ D

我们看到 jlists 都失去了对齐。这不太可能改变表达式的逻辑值，但仍然是不希望的。因此，我们需要分析解析树以找到所有 jlists，并确保我们的修改保持其项的对齐。为此，我们使用 tree-sitter-tlaplus，它正确地解析这些构造。上述（正确对齐）代码片段的 tree-sitter 解析树如下：

(operator_definition (identifier) (def_eq)
  (conj_list
    (conj_item (bullet_conj) (identifier_ref))
    (conj_item
      (bullet_conj)
      (disj_list
        (disj_item (bullet_disj) (identifier_ref))
        (disj_item (bullet_disj) (identifier_ref))
      )
    )
    (conj_item (bullet_conj) (identifier_ref))
  )
)

出于安全起见，程序会检查确保转换后的 TLA⁺ 文件与原始文件具有完全相同的解析树。它也不会转换包含任何解析错误的输入文件。这两个检查都可以通过使用 --force 命令行参数（也在库中公开）来绕过。

算法

高级转换算法如下

1. 对于输入文件的每一行，创建两个向量：一个 jlist 向量和一个符号向量。

2. 解析输入文件，使用tree-sitter查询来识别所有jlist的位置和作用域。对于每一行，将开始于该行的任何jlist的详细信息推入jlist向量中，并按从左到右的顺序排序。

3. 使用tree-sitter查询来识别所有需要替换的符号的位置。按行对符号位置进行排序，然后将它们推入行的符号向量中，并按从左到右的顺序排序。

4. 对于每一行，迭代地从符号向量中弹出顶部元素并在文本中替换它。如果该行右侧没有从该符号开始的jlist，则不需要进一步操作；否则

   1. 对于该行上从替换符号右侧开始的每个jlist，迭代通过所有后续的项目符号行，添加或删除空格以修复对齐。更新那些行上的jlist和符号栈中实体的位置。
   2. 对于每个修复了对齐的jlist项目符号，检查该行上是否还有其他jlist开始；递归地使用相同的过程修复它们的对齐，直到没有更多的jlist需要修复。

5. 迭代通过所有行后，过程完成；解析转换后的树并与原始树进行比较。它们应该是相同的。

复杂性

与宽度可变的UTF-8编码文本一样，必须注意区分符号（以下简称“码点”）的字节索引与其字符索引。我们很久以前就告别了“纯文本 = ASCII = 字符是1字节”的世界。现在，“字符”实际上是一个码点（一个任意大的数，用于在国际Unicode标准中标识一个符号），它可以是1字节（所有与ASCII等效的码点仍然保持，以实现无缝的向后兼容性），也可以是2字节、3字节、4字节等。从根本上说，这意味着给定一个字节索引，你无法知道码点的字符索引（这里也称为其“显示”索引），除非从你所在行的开头读取并计算你遇到的码点数量。这种复杂性对于本项目来说尤其令人关注，该项目涉及大量的文本对齐、移动、插入Unicode符号和索引运算。Rust的类型系统在这里非常有帮助；不是像usize或i8这样的原始类型来存储索引或偏移量，而是定义了多种包装类型，以在类型检查级别强制执行索引运算的安全性。你只能对相同类型的值进行加法或比较，并且从一种类型转换为另一种类型需要从被索引的文本行的开头读取。虽然这会增加一些文字说明，但它极大地简化了保持字符索引和字节索引分离以及推理何时适合使用每个索引的难度。对于可能的（但不太可能）未来的工作，还有更多的复杂性可以通过修饰码点找到，其中多个码点组合形成一个“图形群”（在ASCII世界中我们会认为是“字符”）；例如，图形群é可以直接写成码点U+00E9，也可以写成码点U+0301 U+0065，其中U+0301是应用于U+0065的修饰符（“组合变音符号”），而U+0065是我们熟悉的ASCII等效码e。这个程序不处理图形群，并且（错误地但方便地）假设一个码点 = 一个显示字符。这只有在有人使用修饰符在注释中预置对齐敏感的语法（见下文）时才会成为问题，这是一个如此小众的使用案例，因此出于简单起见，将不会在此处理。

对于实际的语法处理，最棘手的边缘情况如下

op == /\ A
      /\ B
      => C

当使用简单算法从ASCII转换为Unicode时，这会导致

op ≜ ∧ A
     ∧ B
      ⇒ C

因此，将 (A ∧ B) ⇒ C 改变为 A ∧ (B ⇒ C)，这绝对是一个不同的逻辑表达式。处理这种边缘情况的方法是查找内嵌操作符节点，这些节点是jlist节点的父节点，其中jlist是左手表达式。幸亏这可以通过tree-sitter查询轻松完成 (bound_infix_op lhs: [(conj_list) (disj_list)]) @capture。然后，记录操作符符号相对于jlist列的列偏移，并在尽可能多的移动jlist时保持它。在从Unicode转换为ASCII时，也存在这种边缘情况。

op ≜ ∧ A
     ∧ B
      = C
     ∧ D
      = E

这会转换成

op == /\ A
      /\ B
      = C
      /\ D
      = E

所以 (A ∧ (B = C)) ∧ (D = E) 被改写为 ((A ∧ B) = C) ∧ D) = E。这个方向通过tree-sitter查询检测难度很大，因为 B = C 可以是一个任意长和复杂的表达式，最终会溢出到额外的行上。由于这种情况在野外发生的可能性很小，直到大量TLA⁺规范首先以Unicode编写，因此程序目前没有处理这种情况（见问题 https://github.com/tlaplus-community/tlauc/issues/1）。

另一个边缘情况涉及到在jlist项之前（通常是空的）空间中的块注释

op == /\ A
(***) /\ B
(***) /\ C

如果以这种方式存在一个或多个注释，它们将作为如何将jlist左移的硬约束。这使得jlist左移从简单的贪婪算法转变为更类似于约束满足问题，特别是当涉及嵌套jlist或与上面提到的内嵌操作符边缘情况结合时，形成一个棘手的边缘情况。

op == /\ A
(***) /\ \/ B
(******) \/ C
(***) => D

注意，注释可以包含任意Unicode符号，因此必须小心使用字符索引而不是字节索引进行列对齐（参见上面的Unicode困难讨论）。当然，这意味着在非Unicode感知工具中，jlists将无法对齐；但这用户的担忧；此工具不会修改注释文本。实际上，似乎只假定一个代码点=一个显示字符；根据图形簇对齐会增加不必要的复杂性，这对于一个非常利基用例来说是不必要的。

在野外尚未观察到块注释的边缘情况，因此尚未得到支持；见问题 https://github.com/tlaplus-community/tlauc/issues/2。

现有技术

Ron Pressler 在2017年初进行了大量工作，试图将Unicode支持添加到SANY和TLA⁺工具箱，包括在用户输入时用Unicode替换ASCII符号。他还用Java编写了类似的Unicode转换工具 a similar Unicode conversion tool，面临着许多关于jlist对齐的相同挑战。不幸的是，这些工作都没有上游。