tree-sitter-tlaplus

概述

这是一个为形式规范语言 tree-sitter 的 TLA⁺ 和其嵌入式变体 PlusCal 定制的语法。tree-sitter 是一个增量容错解析器生成器，主要用于语言工具，如高亮、代码折叠、符号查找等，这些工具利用其功能齐全的语法树查询 API。此语法旨在在源文件编辑过程中语法不完全正确时优雅地工作。它也足够快，可以在每个按键时重新解析文件。您可以在 https://tlaplus-community.github.io/tree-sitter-tlaplus/ 上尝试解析器。

此存储库中最重要的文件是 grammar.js 和 src/scanner.c。前者是解析器代码生成的源头，后者包含解析 TLA⁺ 的上下文相关部分（如嵌套证明和合取/析取列表）的逻辑。此语法以 Rust crate、Node.js 包 和 Python 包 的形式发布。您可以在 这里 找到如何使用这些包的示例。Node.js 包中也包含 WASM 构建，并附加到本存储库的版本中。

有关此解析器开发过程的详细博客文章可在 这里 找到。此存储库已在 sourcehut 上镜像。

目标和能力

此项目旨在促进创建现代用户辅助语言工具。为此，该项目提供了两个主要功能

1. 提供一种标准的近似正确的TLA⁺规范语法分析树，以便于与旨在消费多种语言语法分析树的通用项目集成。
2. 除了为TLA⁺语法分析树提供API进行任意程序探索外，还提供了一个树查询API，用于高效地查询TLA⁺语法分析树，并提供多种语言的绑定，以便于与针对TLA⁺专门设计的项目集成。

该解析器的正确性标准如下：如果正在解析的TLA⁺规范构成有效的TLA⁺（在语法和语义上），则语法分析树将是正确的。如果规范不是有效的TLA⁺，则语法分析树将是近似正确的——可能允许非法语法，或者以奇怪的方式解释错误的语法。这种宽松的行为使其非常适合作为辅助语言工具，但作为解释器或模型检查器的核心则不太引人注目。应用可能性包括

• 高级语法高亮显示
• 语法感知代码折叠
• TLA⁺语言服务器的轻量级后端
• 使用Cursorless通过语音输入编写TLA⁺规范
• 在GitHub上对TLA⁺规范进行语义分析（链接）
• 将TLA⁺运算符符号转换为它们的Unicode等效符号

使用和显著集成

您可以在自己的项目中以多种方式使用并消费该解析器；请参阅不同编程语言中的示例（链接）。

目前正在使用或集成此语法的显著项目包括

• nvim-treesitter用于Neovim中的TLA⁺语法高亮和代码折叠
• tla-web用于基于Web的TLA⁺解释器和跟踪探索器
• GitHub用于高亮显示TLA⁺文件和代码片段的语法
• tlauc用于在ASCII和Unicode TLA⁺符号之间进行转换

如有适用，集成查询文件位于integrations目录。

构建和测试

请使用--recurse-submodules参数克隆存储库，或者如果您没有使用该参数克隆它，请运行git submodule update --init --recursive

如果使用nix

1. 运行nix-shell
2. 运行tree-sitter test

否则

1. 安装node.js和npm
2. 确保已安装C编译器并将其添加到您的路径中
3. 运行npm install
4. 运行npm test

语料库测试

此测试确保语法可以解析tlaplus/examples存储库中的所有模块，该存储库作为git子模块包含。要运行

1. 如果您是第一次在您的机器上运行tree-sitter，请运行npx tree-sitter init-config
2. 对于Unix类型的操作系统，请运行./test/run-corpus.sh；对于Windows，请运行.\test\run-corpus.ps1
3. 如果成功，则脚本会以错误代码0退出

构建WASM并启动游乐场

如果使用nix

1. 运行nix-shell
2. 运行 tree-sitter build-wasm
3. 使用 tree-sitter playground 启动沙箱

否则

1. 安装node.js和npm
2. 安装 Emscripten 3.x
3. 运行npm install
4. 运行 npx tree-sitter build-wasm
5. 使用 npx tree-sitter playground 启动沙箱

沙箱允许您在浏览器中轻松尝试解析器。您可以在线上（提供最新版本）或按照上述说明在本地运行沙箱。

沙箱由一个包含可编辑的 TLA⁺ 规范的面板和一个包含该规范解析树的另一个面板组成。解析树会随着您对 TLA⁺ 规范的编辑实时更新。您可以点击解析树节点以突出显示相应的 TLA⁺ 片段，并移动光标在规范中显示相应的解析树节点。您可以通过点击“日志”复选框并打开浏览器的开发者控制台来查看解析器尝试解析 TLA⁺ 规范时的调试输出。您还可以点击“查询”复选框来打开第三个面板以测试树查询；例如，输入以下内容以匹配名为 @operator 的捕获中的所有运算符名称（名称变高亮表示）

(operator_definition name: (identifier) @operator)

模糊测试

如果您正在运行带有最新版本 Clang 的 Linux，您可以模糊测试语法。按照以下步骤操作

1. 使用 --recurse-submodules 参数克隆仓库
2. 从仓库根目录运行 bash 脚本 test/fuzzing/build-for-fuzzing.sh
3. 从仓库根目录运行 test/fuzzing/out/tree_sitter_tlaplus_fuzzer

贡献

一个简单的方法是将您的 TLA⁺ 规范添加到 tlaplus/examples 仓库，该语法将其用作有价值的测试语料库！

欢迎提交拉取请求。如果您修改了 grammar.js，请确保在提交 & 推送之前运行 npx tree-sitter generate。生成的文件目前存在于仓库中，但有望在未来被移除。它们在 CI 期间强制对应。