# tree-sitter-tlaplus
[](https://github.com/tlaplus-community/tree-sitter-tlaplus/actions/workflows/ci.yml)
[](https://www.npmjs.com/package/@tlaplus/tree-sitter-tlaplus)
[](https://crates.io/crates/tree-sitter-tlaplus)
[](https://pypi.org/project/tree-sitter-tlaplus)
## Overview
This is a [tree-sitter](https://tree-sitter.github.io/tree-sitter/) grammar for the formal specification language [TLA⁺](https://en.wikipedia.org/wiki/TLA%2B) and its embedded variant [PlusCal](https://en.wikipedia.org/wiki/PlusCal).
Tree-sitter is an incremental error-tolerant parser generator primarily aimed at language tooling such as highlighting, code folding, symbol finding, and other tasks making use of its fully-featured syntax tree query API.
This grammar is intended to function gracefully while parsing a source file mid-edit, when the syntax isn't fully correct.
It is also fast enough to re-parse the file on every keystroke.
You can take the parser for a spin at https://tlaplus-community.github.io/tree-sitter-tlaplus/
The most important files in this repo are `grammar.js` and `src/scanner.c`.
The former is the source of truth for parser code generation and the latter contains logic for parsing the context-sensitive parts of TLA⁺ like nested proofs and conjunction/disjunction lists.
This grammar is published as a [Rust crate](https://crates.io/crates/tree-sitter-tlaplus), [Node.js package](https://www.npmjs.com/package/@tlaplus/tree-sitter-tlaplus), and [Python package](https://pypi.org/project/tree-sitter-tlaplus).
You can see examples of how to consume these packages [here](test/consumers).
A WASM build is also included in the Node.js package and attached to the releases in this repo.
A blog post detailing the development process of this parser can be found [here](https://ahelwer.ca/post/2023-01-11-tree-sitter-tlaplus/).
This repo is [mirrored on sourcehut](https://git.sr.ht/~ahelwer/tree-sitter-tlaplus).
## Aims & Capabilities
The aim of this project is to facilitate creation of modern user-assistive language tooling for TLA⁺.
To that end, the project provides two main capabilities:
1. Provide an approximately-correct parse tree for TLA⁺ specifications in standardized form, for easy integration with general projects designed to consume the tree-sitter grammars of many languages.
1. Provide a [tree query API](https://tree-sitter.github.io/tree-sitter/using-parsers#pattern-matching-with-queries) for efficiently querying the TLA⁺ parse tree, in addition to an API for arbitrary programmatic exploration of same, with bindings in multiple languages for easy integration with projects specifically targeting TLA⁺.
The correctness criterion of this parser is as follows: if the TLA⁺ specification being parsed constitutes valid TLA⁺ (both syntactically and semantically), the parse tree will be correct.
If the spec is not valid TLA⁺, the parse tree will be approximately correct - perhaps permissively allowing illegal syntax, or interpreting erroneous syntax in strange ways.
This permissive behavior makes it excellent for user-assistive language tooling, but a less-compelling choice as the backbone for an interpreter or model-checker.
Application possibilities include:
* Advanced syntax highlighting
* Syntax-aware code folding
* Lightweight backend for a TLA⁺ [language server](https://microsoft.github.io/language-server-protocol/)
* Writing TLA⁺ specs via dictation using [Cursorless](https://github.com/pokey/cursorless-vscode)
* Semantic analysis of TLA⁺ specs [on GitHub](https://github.com/github/semantic)
* Translation of TLA⁺ operator symbols [into their unicode equivalents](https://github.com/tlaplus-community/tlauc)
## Use & Notable Integrations
There are a number of avenues available for consuming & using the parser in a project of your own; see examples in several different programming languages [here](test/consumers).
Notable projects currently using or integrating this grammar include:
* [nvim-treesitter](https://github.com/nvim-treesitter/nvim-treesitter) for TLA⁺ syntax highlighting & code folding in Neovim
* [tla-web](https://github.com/will62794/tla-web) for a web-based TLA⁺ interpreter and trace explorer
* GitHub for syntax highlighting of TLA⁺ files and snippets
* [tlauc](https://github.com/tlaplus-community/tlauc) for translating between ASCII and Unicode TLA⁺ symbols
As applicable, query files for integrations live in the `integrations` directory.
## Build & Test
Be sure to clone the repo with the `--recurse-submodules` parameter, or run `git submodule update --init --recursive` if you already cloned it without that parameter.
If using nix:
1. Run `nix-shell`
1. Run `tree-sitter test`
Otherwise:
1. Install [node.js and npm](https://docs.npmjs.com/downloading-and-installing-node-js-and-npm)
1. Ensure a C compiler is installed and on your path
1. Run `npm install`
1. Run `npm test`
### Corpus Tests
This test ensures the grammar can parse all modules in the [tlaplus/examples](https://github.com/tlaplus/examples) repo, which is included as a git submodule.
To run:
1. If this is the first time running tree-sitter on your machine, run `npx tree-sitter init-config`
1. For Unix-type OSs, run `./test/run-corpus.sh`; for Windows, run `.\test\run-corpus.ps1`
1. The scripts exit with error code 0 if successful
### Build WASM & Start Playground
If using nix:
1. Run `nix-shell`
1. Run `tree-sitter build-wasm`
1. Start the playground with `tree-sitter playground`
Otherwise:
1. Install [node.js and npm](https://docs.npmjs.com/downloading-and-installing-node-js-and-npm)
1. Install [Emscripten 3.x](https://emscripten.org/)
1. Run `npm install`
1. Run `npx tree-sitter build-wasm`
1. Start the playground with `npx tree-sitter playground`
The playground enables you to easily try out the parser in your browser.
You can use the playground [online](https://tlaplus-community.github.io/tree-sitter-tlaplus/) (serving the latest release) or run it locally by following the directions above.
The playground consists of a pane containing an editable TLA⁺ spec, and another pane containing the parse tree for that spec.
The parse tree is updated in real time as you edit the TLA⁺ spec.
You can click parse tree nodes to highlight the corresponding snippet of TLA⁺, and move the cursor around the spec to show the corresponding parse tree node.
You can click the "log" checkbox and open your browser's development console to see the parser's debug output as it attempts to parse the TLA⁺ spec.
You can also click the "query" checkbox to open a third pane for testing [tree queries](https://tree-sitter.github.io/tree-sitter/using-parsers#pattern-matching-with-queries); for example, enter the following to match all operator names in a capture named `@operator` (indicated by the names becoming highlighted):
```
(operator_definition name: (identifier) @operator)
```
## Fuzzing
You can fuzz the grammar if you're running Linux with a recent version of Clang installed.
Do so as follows:
1. Clone the repo with the `--recurse-submodules` parameter
2. From repo root, run the bash script `test/fuzzing/build-for-fuzzing.sh`
3. From repo root, run `test/fuzzing/out/tree_sitter_tlaplus_fuzzer`
## Contributions
One easy way to contribute is to add your TLA⁺ specifications to the [tlaplus/examples](https://github.com/tlaplus/examples) repo, which this grammar uses as a valuable test corpus!
Pull requests are welcome. If you modify `grammar.js`, make sure you run `npx tree-sitter generate` before committing & pushing.
Generated files are (unfortunately) currently present in the repo but will hopefully be removed in [the future](https://github.com/tree-sitter/tree-sitter/discussions/1243).
Their correspondence is enforced during CI.
Raw data
{
"_id": null,
"home_page": null,
"name": "tree-sitter-tlaplus",
"maintainer": "Andrew Helwer",
"docs_url": null,
"requires_python": ">=3.8",
"maintainer_email": null,
"keywords": "incremental, parsing, tree-sitter, tlaplus",
"author": "Andrew Helwer, Vasiliy Morkovkin",
"author_email": null,
"download_url": null,
"platform": null,
"description": "# tree-sitter-tlaplus\n\n[](https://github.com/tlaplus-community/tree-sitter-tlaplus/actions/workflows/ci.yml)\n[](https://www.npmjs.com/package/@tlaplus/tree-sitter-tlaplus)\n[](https://crates.io/crates/tree-sitter-tlaplus)\n[](https://pypi.org/project/tree-sitter-tlaplus)\n\n## Overview\n\nThis is a [tree-sitter](https://tree-sitter.github.io/tree-sitter/) grammar for the formal specification language [TLA\u207a](https://en.wikipedia.org/wiki/TLA%2B) and its embedded variant [PlusCal](https://en.wikipedia.org/wiki/PlusCal).\nTree-sitter is an incremental error-tolerant parser generator primarily aimed at language tooling such as highlighting, code folding, symbol finding, and other tasks making use of its fully-featured syntax tree query API.\nThis grammar is intended to function gracefully while parsing a source file mid-edit, when the syntax isn't fully correct.\nIt is also fast enough to re-parse the file on every keystroke.\nYou can take the parser for a spin at https://tlaplus-community.github.io/tree-sitter-tlaplus/\n\nThe most important files in this repo are `grammar.js` and `src/scanner.c`.\nThe former is the source of truth for parser code generation and the latter contains logic for parsing the context-sensitive parts of TLA\u207a like nested proofs and conjunction/disjunction lists.\nThis grammar is published as a [Rust crate](https://crates.io/crates/tree-sitter-tlaplus), [Node.js package](https://www.npmjs.com/package/@tlaplus/tree-sitter-tlaplus), and [Python package](https://pypi.org/project/tree-sitter-tlaplus).\nYou can see examples of how to consume these packages [here](test/consumers).\nA WASM build is also included in the Node.js package and attached to the releases in this repo.\n\nA blog post detailing the development process of this parser can be found [here](https://ahelwer.ca/post/2023-01-11-tree-sitter-tlaplus/).\nThis repo is [mirrored on sourcehut](https://git.sr.ht/~ahelwer/tree-sitter-tlaplus).\n\n## Aims & Capabilities\n\nThe aim of this project is to facilitate creation of modern user-assistive language tooling for TLA\u207a.\nTo that end, the project provides two main capabilities:\n1. Provide an approximately-correct parse tree for TLA\u207a specifications in standardized form, for easy integration with general projects designed to consume the tree-sitter grammars of many languages.\n1. Provide a [tree query API](https://tree-sitter.github.io/tree-sitter/using-parsers#pattern-matching-with-queries) for efficiently querying the TLA\u207a parse tree, in addition to an API for arbitrary programmatic exploration of same, with bindings in multiple languages for easy integration with projects specifically targeting TLA\u207a.\n\nThe correctness criterion of this parser is as follows: if the TLA\u207a specification being parsed constitutes valid TLA\u207a (both syntactically and semantically), the parse tree will be correct.\nIf the spec is not valid TLA\u207a, the parse tree will be approximately correct - perhaps permissively allowing illegal syntax, or interpreting erroneous syntax in strange ways.\nThis permissive behavior makes it excellent for user-assistive language tooling, but a less-compelling choice as the backbone for an interpreter or model-checker.\nApplication possibilities include:\n * Advanced syntax highlighting\n * Syntax-aware code folding\n * Lightweight backend for a TLA\u207a [language server](https://microsoft.github.io/language-server-protocol/)\n * Writing TLA\u207a specs via dictation using [Cursorless](https://github.com/pokey/cursorless-vscode)\n * Semantic analysis of TLA\u207a specs [on GitHub](https://github.com/github/semantic)\n * Translation of TLA\u207a operator symbols [into their unicode equivalents](https://github.com/tlaplus-community/tlauc)\n\n## Use & Notable Integrations\n\nThere are a number of avenues available for consuming & using the parser in a project of your own; see examples in several different programming languages [here](test/consumers).\n\nNotable projects currently using or integrating this grammar include:\n * [nvim-treesitter](https://github.com/nvim-treesitter/nvim-treesitter) for TLA\u207a syntax highlighting & code folding in Neovim\n * [tla-web](https://github.com/will62794/tla-web) for a web-based TLA\u207a interpreter and trace explorer\n * GitHub for syntax highlighting of TLA\u207a files and snippets\n * [tlauc](https://github.com/tlaplus-community/tlauc) for translating between ASCII and Unicode TLA\u207a symbols\n\nAs applicable, query files for integrations live in the `integrations` directory.\n\n## Build & Test\n\nBe sure to clone the repo with the `--recurse-submodules` parameter, or run `git submodule update --init --recursive` if you already cloned it without that parameter.\n\nIf using nix:\n1. Run `nix-shell`\n1. Run `tree-sitter test`\n\nOtherwise:\n1. Install [node.js and npm](https://docs.npmjs.com/downloading-and-installing-node-js-and-npm)\n1. Ensure a C compiler is installed and on your path\n1. Run `npm install`\n1. Run `npm test`\n\n### Corpus Tests\n\nThis test ensures the grammar can parse all modules in the [tlaplus/examples](https://github.com/tlaplus/examples) repo, which is included as a git submodule.\nTo run:\n1. If this is the first time running tree-sitter on your machine, run `npx tree-sitter init-config`\n1. For Unix-type OSs, run `./test/run-corpus.sh`; for Windows, run `.\\test\\run-corpus.ps1`\n1. The scripts exit with error code 0 if successful\n\n### Build WASM & Start Playground\n\nIf using nix:\n1. Run `nix-shell`\n1. Run `tree-sitter build-wasm`\n1. Start the playground with `tree-sitter playground`\n\nOtherwise:\n1. Install [node.js and npm](https://docs.npmjs.com/downloading-and-installing-node-js-and-npm)\n1. Install [Emscripten 3.x](https://emscripten.org/)\n1. Run `npm install`\n1. Run `npx tree-sitter build-wasm`\n1. Start the playground with `npx tree-sitter playground`\n\nThe playground enables you to easily try out the parser in your browser.\nYou can use the playground [online](https://tlaplus-community.github.io/tree-sitter-tlaplus/) (serving the latest release) or run it locally by following the directions above.\n\nThe playground consists of a pane containing an editable TLA\u207a spec, and another pane containing the parse tree for that spec.\nThe parse tree is updated in real time as you edit the TLA\u207a spec.\nYou can click parse tree nodes to highlight the corresponding snippet of TLA\u207a, and move the cursor around the spec to show the corresponding parse tree node.\nYou can click the \"log\" checkbox and open your browser's development console to see the parser's debug output as it attempts to parse the TLA\u207a spec.\nYou can also click the \"query\" checkbox to open a third pane for testing [tree queries](https://tree-sitter.github.io/tree-sitter/using-parsers#pattern-matching-with-queries); for example, enter the following to match all operator names in a capture named `@operator` (indicated by the names becoming highlighted):\n```\n(operator_definition name: (identifier) @operator)\n```\n\n## Fuzzing\n\nYou can fuzz the grammar if you're running Linux with a recent version of Clang installed.\nDo so as follows:\n1. Clone the repo with the `--recurse-submodules` parameter\n2. From repo root, run the bash script `test/fuzzing/build-for-fuzzing.sh`\n3. From repo root, run `test/fuzzing/out/tree_sitter_tlaplus_fuzzer`\n\n## Contributions\n\nOne easy way to contribute is to add your TLA\u207a specifications to the [tlaplus/examples](https://github.com/tlaplus/examples) repo, which this grammar uses as a valuable test corpus!\n\nPull requests are welcome. If you modify `grammar.js`, make sure you run `npx tree-sitter generate` before committing & pushing.\nGenerated files are (unfortunately) currently present in the repo but will hopefully be removed in [the future](https://github.com/tree-sitter/tree-sitter/discussions/1243).\nTheir correspondence is enforced during CI.\n\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "A tree-sitter grammar for TLA\u207a and PlusCal",
"version": "1.2.8",
"project_urls": {
"Homepage": "https://github.com/tlaplus-community/tree-sitter-tlaplus",
"Issues": "https://github.com/tlaplus-community/tree-sitter-tlaplus/issues"
},
"split_keywords": [
"incremental",
" parsing",
" tree-sitter",
" tlaplus"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "4f4c167bf2d248acec2bb9b935adec395e1a47ac515f69e07a6ba4ed9fc97724",
"md5": "cfca06a79bfc71dae176d555a0d79bd5",
"sha256": "63859f0f16f573308d6a66bf0701cf8af130e8ca78b894405f39a2e4325a0943"
},
"downloads": -1,
"filename": "tree_sitter_tlaplus-1.2.8-cp38-abi3-macosx_10_9_x86_64.whl",
"has_sig": false,
"md5_digest": "cfca06a79bfc71dae176d555a0d79bd5",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8",
"size": 263098,
"upload_time": "2024-04-18T19:37:13",
"upload_time_iso_8601": "2024-04-18T19:37:13.627615Z",
"url": "https://files.pythonhosted.org/packages/4f/4c/167bf2d248acec2bb9b935adec395e1a47ac515f69e07a6ba4ed9fc97724/tree_sitter_tlaplus-1.2.8-cp38-abi3-macosx_10_9_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "5e2aa1ea09a916ccae1fa890ecc657067baa9cfb0eaaaba77677f3f249c1144a",
"md5": "95e0301207d05a6a45c6e6e3644a89b5",
"sha256": "1058fb82bd4491ed0524addd255a0f2571028d196776e32c55533c9476052986"
},
"downloads": -1,
"filename": "tree_sitter_tlaplus-1.2.8-cp38-abi3-macosx_11_0_arm64.whl",
"has_sig": false,
"md5_digest": "95e0301207d05a6a45c6e6e3644a89b5",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8",
"size": 302464,
"upload_time": "2024-04-18T19:37:15",
"upload_time_iso_8601": "2024-04-18T19:37:15.995523Z",
"url": "https://files.pythonhosted.org/packages/5e/2a/a1ea09a916ccae1fa890ecc657067baa9cfb0eaaaba77677f3f249c1144a/tree_sitter_tlaplus-1.2.8-cp38-abi3-macosx_11_0_arm64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "7f4ae05cdcf20ab4dbdf033ff23557b11557ef615ce7b1a1a0b61ca6e06da0ba",
"md5": "cb3947a5a937ce071ef6107e2fa14215",
"sha256": "6657de5a5cd48c29f243ef5d68717117a036218b57c5467ab42d26975aea60d7"
},
"downloads": -1,
"filename": "tree_sitter_tlaplus-1.2.8-cp38-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.whl",
"has_sig": false,
"md5_digest": "cb3947a5a937ce071ef6107e2fa14215",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8",
"size": 341430,
"upload_time": "2024-04-18T19:37:18",
"upload_time_iso_8601": "2024-04-18T19:37:18.826752Z",
"url": "https://files.pythonhosted.org/packages/7f/4a/e05cdcf20ab4dbdf033ff23557b11557ef615ce7b1a1a0b61ca6e06da0ba/tree_sitter_tlaplus-1.2.8-cp38-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "735b207f73e1cc29f49c561b6230d786e7b78e056901f3f07f6558771ee6cc74",
"md5": "3194cb8d7a26908adf4075a6c1049f0a",
"sha256": "190149191519c2378633fa9b89c880303d8ca1e0490b4e214a33499f9f1a4766"
},
"downloads": -1,
"filename": "tree_sitter_tlaplus-1.2.8-cp38-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl",
"has_sig": false,
"md5_digest": "3194cb8d7a26908adf4075a6c1049f0a",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8",
"size": 315486,
"upload_time": "2024-04-18T19:37:20",
"upload_time_iso_8601": "2024-04-18T19:37:20.688027Z",
"url": "https://files.pythonhosted.org/packages/73/5b/207f73e1cc29f49c561b6230d786e7b78e056901f3f07f6558771ee6cc74/tree_sitter_tlaplus-1.2.8-cp38-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "5d4ba3e7d875ea268d8da86737d00d4c5f4a10c89fba1394d4ed7c87c84098bf",
"md5": "7d93d618f32010d85df7d3b7dcc82ee9",
"sha256": "2f894219d1cef6cff6f31c9695ccb870769fb4371562889100068450a2969bbc"
},
"downloads": -1,
"filename": "tree_sitter_tlaplus-1.2.8-cp38-abi3-musllinux_1_1_aarch64.whl",
"has_sig": false,
"md5_digest": "7d93d618f32010d85df7d3b7dcc82ee9",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8",
"size": 341034,
"upload_time": "2024-04-18T19:37:22",
"upload_time_iso_8601": "2024-04-18T19:37:22.870146Z",
"url": "https://files.pythonhosted.org/packages/5d/4b/a3e7d875ea268d8da86737d00d4c5f4a10c89fba1394d4ed7c87c84098bf/tree_sitter_tlaplus-1.2.8-cp38-abi3-musllinux_1_1_aarch64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "1f849a59aceff3f6a007d44ae337762d42b26a2d9fab627966cd4c13565b9753",
"md5": "0db26ba1cc15406272dfcf38687e6004",
"sha256": "6215464878e1900cf13739df98deac958282e0dfb4e467fb7b1d756090528ea1"
},
"downloads": -1,
"filename": "tree_sitter_tlaplus-1.2.8-cp38-abi3-musllinux_1_1_x86_64.whl",
"has_sig": false,
"md5_digest": "0db26ba1cc15406272dfcf38687e6004",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8",
"size": 315314,
"upload_time": "2024-04-18T19:37:24",
"upload_time_iso_8601": "2024-04-18T19:37:24.945444Z",
"url": "https://files.pythonhosted.org/packages/1f/84/9a59aceff3f6a007d44ae337762d42b26a2d9fab627966cd4c13565b9753/tree_sitter_tlaplus-1.2.8-cp38-abi3-musllinux_1_1_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "7accc20af68460ba8aaad4b59c59716815850aae329ea7edaf4ebfa255b04574",
"md5": "13f7d15a6447d2e32e9c424a0ce67224",
"sha256": "9081872d6ab9af982cb0f58a1d1018d8a7d90934b53a37b4152a8fa8750d34f1"
},
"downloads": -1,
"filename": "tree_sitter_tlaplus-1.2.8-cp38-abi3-win_amd64.whl",
"has_sig": false,
"md5_digest": "13f7d15a6447d2e32e9c424a0ce67224",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8",
"size": 267044,
"upload_time": "2024-04-18T19:37:27",
"upload_time_iso_8601": "2024-04-18T19:37:27.587460Z",
"url": "https://files.pythonhosted.org/packages/7a/cc/c20af68460ba8aaad4b59c59716815850aae329ea7edaf4ebfa255b04574/tree_sitter_tlaplus-1.2.8-cp38-abi3-win_amd64.whl",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-04-18 19:37:13",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "tlaplus-community",
"github_project": "tree-sitter-tlaplus",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "tree-sitter-tlaplus"
}
JSON
