Replace TLAPM parser with SANY

[ahelwer]

As discussed in tlaplus/rfcs#16, the TLAPM parser is to be replaced with SANY. This work has been approved for funding by the TLA⁺ Foundation. The reasons for this replacement are as follows:

1. Reduced maintenance burden, since only one fully-featured parser will need to be maintained
2. The TLAPM parser lacks many semantic checks and does not have a fully-functional level checker
3. The TLAPM parser has many bugs that need to be fixed (although most are minor)

One remaining question is how to handle the interface between TLAPM and SANY, as TLAPM is an OCaml program and SANY is a Java program. Three possibilities exist:

1. From TLAPM, call SANY's XML Exporter program to parse the TLA⁺ input in a separate process, then consume the output XML from OCaml & translate it to TLAPM's existing abstract syntax tree (AST) format; to reduce startup time, SANY will be run as a GraalVM Native Image so it does not need to load the JVM.
2. Compile SANY to a GraalVM Native Image, exposing a C API so SANY can be called directly from C code; then, call this C API from OCaml code in TLAPM.
3. Call SANY from TLAPM OCaml code using some other OCaml/Java interface method; there are a few (1, 2, 3) of these projects floating around but nothing that seems fully-featured & maintained, thus this option is not seriously considered.

Of these options, (1) has been explored to the greatest depth. A prototype parser of SANY's XML output was written back in November 2024. However, at that time @Calvin-L had not yet experimented with compiling SANY to a Graal Native Image, and I was much less familiar with GraalVM generally and its interoperability goals. I have spent some time recently experimenting with exposing a simple C API from Java in Graal.

While it would be nicer to call SANY directly instead of having to parse an intermediate XML AST representation, there does seem to be one substantial drawback: Java code seems limited in the datatypes that can be exposed via Graal Native Image C APIs. My understanding at this time (which might be incorrect) is that the C APIs must return a concretely-defined datatype, not an abstract datatype that can be dynamically casted to an inheriting class. SANY's parse tree node datatype is currently implemented as a fairly deep tree of inheritance; see this by opening the type hierarchy of the SemanticNode class in Eclipse. Thus I believe if we wanted to go this route we would have to write a C API layer inside SANY which somehow simplifies its AST format and makes it concrete. I also don't believe the C API could support variants but might be wrong.

In contrast, XML is very flexible in a way which matches OCaml's type system fairly well, with variants and so forth. We also already have a fairly functional XML parser for this format from past work. Thus while the GraalVM Native Image C API option is compelling and would have substantial benefits for other users who want to consume SANY from non-JVM languages (including web languages!) for expediency the XML option might be the best. What do people think?

Other than this question of how to interface with SANY, the greatest remaining work item is to translate the SANY AST format - however we get it - into TLAPM's existing AST format. We want to leave TLAPM's AST format unchanged as all existing transformations to backend theorem provers are defined over this format.

[lemmy]

+1 for the XML exporter: it has the fewest unknowns and offers the most generic API, making it best for future integration with any ecosystem.

[kape1395]

Some comments adapted from #186, mostly considering the LSP:

• I would like to pass some checksums/modification times for the modules already parsed by the tlapm. This way, it could avoid repeatedly parsing them (the dependencies of a module currently edited). A stateful interaction is probably needed to handle that properly (that would imply grpc or similar, I guess).
• I would like to have a way to parse a document not saved to the disk, e.g., from the stdin or grpc message payload. This is currently used by the tlapm lsp.
• Should we add protobuf and/or grpc or json-rpc interface for the parser instead of parsing the XML? LSP uses JSON-RPC, maybe we should follow that standard? XML only associates with something outdated nowadays.

Also, it is unclear to me what happens to the expression levels when definitions in an expression are expanded. Don't we need to recalculate the levels? E.g., having P(x) == x + x and later its use as P(some'). In a proof step <2>x. P(some') \in S BY DEF P the definition will be expanded to some' + some' \in S. Will the SANY parser's output contain enough information to assign the levels for the latter/expanded expression?

[lemmy]

If parsing and level-checking were fast enough, would there still be a need to track state using checksums or modification times, or is there another requirement that justifies it?

[ahelwer]

E.g., having P(x) == x + x and later its use as P(some'). In a proof step <2>x. P(some') \in S BY DEF P the definition will be expanded to some' + some' \in S. Will the SANY parser's output contain enough information to assign the levels for the latter/expanded expression?

I gave a longer explanation of operator expansion & level-checking here but this case is actually very simple. The level of some operator op(x, y, z) is the maximum of the level of the operator itself and expressions x, y, and z. So in your case of P(x) the level of P is constant and the level of x is action (since it's some'). So the level of P(some') is action.

Of course here we actually encounter an unknown in this project, which is how easy it will be to translate SANY's AST to TLAPM's.

[kape1395]

If parsing and level-checking were fast enough, would there still be a need to track state using checksums or modification times, or is there another requirement that justifies it?

The reason is the performance. The size of the current proof documents is small enough, and re-parsing all would still work for now. But if the stdlib or the community modules were to grow, the amount of parsing would only increase. In my current development (several thousand proof lines), I split the modules into "sections", each "section" as a module extending the preceding "section". While that allowed me to work faster (fewer annotations to exchange with VSCode), the parsing remained the bottleneck. Instead, if only the current buffer (if deps are not modified) were re-parsed, there would be a clear way to cope with an increasing number of theorems in a project.

[kape1395]

So in your case of P(x) the level of P is constant and the level of x is action (since it's some'). So the level of P(some') is action.

But for TLAPS, it is not enough to know P(some') is an action. It also has to know all the levels for sub-expressions in some' + some' \in S, which does not exist in SANY's parse tree (assuming the expressions are not expanded there). Maybe I'm confused here?

[ahelwer]

Why does it need to know that? Is it not enough to know (some' + some') is an action?

[kape1395]

Why does it need to know that? Is it not enough to know (some' + some') is an action?

To my understanding, e.g., some is a definition containing some constant and variable-level sub-expressions. If I deconstruct the formula, the sub-expressions should be considered at a correct level. There are some transformations that check if an expression is constant (src/expr/e_constness.ml). Not sure if variable/action levels are considered separately. Maybe @muenchnerkindl could resolve this confusion :)

[lemmy]

The reason is the performance. The size of the current proof documents is small enough, and re-parsing all would still work for now. But if the stdlib or the community modules were to grow, the amount of parsing would only increase. In my current development (several thousand proof lines), I split the modules into "sections", each "section" as a module extending the preceding "section". While that allowed me to work faster (fewer annotations to exchange with VSCode), the parsing remained the bottleneck. Instead, if only the current buffer (if deps are not modified) were re-parsed, there would be a clear way to cope with an increasing number of theorems in a project.

Incremental parsing and improved handling of parse errors are both features that could—and should—be built into SANY.