Skip to content

Add SANY parser backend#255

Open
ahelwer wants to merge 85 commits intotlaplus:mainfrom
ahelwer:sany-slice
Open

Add SANY parser backend#255
ahelwer wants to merge 85 commits intotlaplus:mainfrom
ahelwer:sany-slice

Conversation

@ahelwer
Copy link
Copy Markdown
Collaborator

@ahelwer ahelwer commented Mar 28, 2026

The big files to look at here are:

  • src/sany/xml.ml: this shells out to SANY and parses its output into a collection of typed datastructures that reflect the XML output format; the XML output format documentation was added in XML Exporter: add comprehensive documentation to schema file tlaplus#1346)
  • src/sany/sany.ml: this takes the datastructures generated by src/sany/xml.ml and converts it into TLAPM's existing parse tree

The rest is test code, and modifications to Tlapm_lib to add entrypoints to the SANY functionality hidden behind a feature flag.

The current status of the work is as follows:

  • All files in the tlaplus/examples repo (and all .tla files in this repo) are parsed with SANY and have the XML output successfully run through the conversion process. Success here means the conversion process doesn't produce exceptions, although recursive operators and anonymous subexpressions are not supported. This test is currently only hardcoded to work on my personal computer since the CI of this repository is broken anyway due to TLAPM library modules depend on community modules #252.
  • A selection of basic proofs are fully checked after being sent through the SANY parse pipeline. Extending this to check every proof in the tlaplus/examples repo likely would not take much more work.
  • Functionality is exposed to compare the S-expressions of the parse trees produced by TLAPM and SANY for differences. There are a couple unbridgeable gaps (like SANY exports VARIABLES x, y as VARIABLE x then VARIABLE y) but after accounting for these comparing the S-expression output is a very nice way to spot differences. S-expression export has not yet been added on the SANY side.
  • There are quite a few nitpick bugs that need to be fixed on the SANY XML Exporter side. I will be documenting those in the near future; a good central issue for now is Feedback & updates to the XML output format from TLAPM work tlaplus#1313 (this is one of those things where the more you look the more you find so I tried to focus on getting this to shippable state instead of getting bogged down in making it perfect on both sides).

Ref #213

Expose ability to use SANY

Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Propagate CLI parameter to Tlapm_lib

Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Added Xmlm library dependency

Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

1 participant