TLA+ extension parsing architecture

[younes-io]

Hey everyone,

PR #386 sparked an interesting architectural debate that I think deserves broader discussion. The PR adds a simple "Update vars" command, but the implementation choices reveal deeper questions about the parsing strategy.

Currently, we use multiple parsers:

• SANY (via XMLExporter): "THE" semantic truth
• Regex fallbacks: for unsaved/invalid files
• TextMate grammars: for syntax highlighting
• TLAPS parser: an LSP server, for TLA+ proofs

Question: Should we add tree-sitter to this mix?

For tree-sitter:

• Handles incomplete/malformed code gracefully
• Replaces brittle regexes with proper grammar
• Has TypeScript bindings ready
• Covers 100% of TLA+ syntax

Concerns:

• Yet another parser to maintain
• Any potential inconsistencies with SANY?
• Does it support native VSCode highlighting yet?

The real issue

I think this boils down to a fundamental separation of concerns:

• Semantic parsing => SANY remains "THE" go-to tool
• Syntactic parsing => We need something that works on incomplete code

Many IDE features (variable extraction, code navigation, folding) need syntactic parsing that works even when SANY would fail. Currently we use regex for this, which... works, but isn't ideal.

Questions for Discussion

1. Is adding tree-sitter worth the complexity for better syntactic parsing?
2. Should we wait for SANY to get incremental/recovery parsing capabilities?
3. Are there other approaches we should consider?
4. How important is github.dev compatibility for these architecture decisions? (cf. src/main.browser.ts)
5. Should we wait for this Explore using tree sitter for syntax highlighting microsoft/vscode#210475?

I don't have strong opinions yet. Just wanted to surface this discussion from the PR comments. This decision will impact incoming PRs, I suppose, so it's worth getting alignment.

What do you all think?

[lemmy]

Should we wait for SANY to get incremental/recovery parsing capabilities?

@ahelwer Do you have a rough estimate of how difficult or time-consuming it would be to add recovery parsing to SANY? Incremental parsing is less of a priority—partly because we already have some support for it (TLA+ debugger breakpoint expressions).

[ahelwer]

I would estimate 1-3 months of work to add error recovery to SANY. It depends on whether newer versions of JavaCC support it. If not, will have to hack something together on top of JavaCC. You can advocate to the board for its prioritization after the TLAPM work.

[lemmy]

Is there a technical reason why it has to happen after the TLAPS work?

[ahelwer]

No, only a prioritization reason. The TLAPS work has dragged on long enough and I need to get it finished.

[ahelwer]

As far as technical approach, since JavaCC generates a recursive descent parser, the standard method of doing error recovery in recursive descent is "panic mode"; basically after a parse exception is thrown, read & throw out tokens until you reach the start of the next OpDef(x, y, z) == ... statement, then resume parsing (this is made more difficult in TLA⁺ by definitions also appearing in LET/IN blocks and also some proof constructs but still could be tractable). Then somehow mark the errored/incomplete definition as being as such, and then modify the semantic & level checking code to be tolerant of such malformed definitions.

[lemmy]

How long do you estimate it would take for someone to ramp up and handle the recovery mode work while SANY is being integrated into TLAPS? From your technical description, recover mode doesn't seem to require significant TLA+ expertise.

[ahelwer]

I'm biased (since it's the reason I developed tree-sitter-tlaplus in the first place) but the purpose of tree-sitter as a project is to replace all instances of using regular expressions to parse context-free or context-sensitive languages, a very obvious category error.

With regard to inconsistencies between SANY and tree-sitter-tlaplus, both of them conform to the syntactic test corpus (modulo a few open bugs) so we can be basically assured no user-visible differences exist.

There are other nice features of the tree-sitter API, like being able to run queries for particular syntax subtree forms.

Issue microsoft/vscode#210475 has no movement behind it and will basically never happen. I don't know whether the TextMate grammar can be replaced by using tree-sitter as input to the VS Code semantic highlighting feature, but that is one possibility.

[lemmy]

I'm biased (since it's the reason I developed tree-sitter-tlaplus in the first place) but the purpose of tree-sitter as a project is to replace all instances of using regular expressions to parse context-free or context-sensitive languages, a very obvious category error.

With regard to inconsistencies between SANY and tree-sitter-tlaplus, both of them conform to the syntactic test corpus (modulo a few open bugs) so we can be basically assured no user-visible differences exist.

For a test corpus to demonstrate the absence of user-visible differences, it must be exhaustive. What is the justification for claiming that this test corpus is exhaustive?

[ahelwer]

Absent formal proofs of equivalence, which will never happen, the test corpus is the best guarantee you're going to get. The tests number around 350 IIRC (with each test exercising several things) and every exposed node type is used. Of course there are an infinite number of possible parse inputs so they cannot be said to be exhaustive. The tree-sitter-tlaplus parser is also less restrictive than SANY (for example with operator precedence conflicts) which is good for this sort of language tooling.