Add SANY parser backend - #255

Closed

ahelwer wants to merge 85 commits into

tlaplus:mainfrom

ahelwer:sany-slice

Commits on Feb 26, 2026

Added parser backend CLI parameter
ahelwer
committed
1375a4c
Use SANY parse backend when indicated
ahelwer
committed
4f0dae4
Stubbed out SANY parse architecture
ahelwer
committed
2973c8f
Download tla2tools.jar during build
ahelwer
committed
f58b5d3
Call SANY XML Exporter and capture XML output
ahelwer
committed
408dc8e
Integrate SANY XML processing code
ahelwer
committed
7425938
Write some tests to explore prototype
ahelwer
committed
fb1aff0
Reorganized SANY code into its own module
ahelwer
committed
04ab246
Started conversion code
ahelwer
committed
ff84fb0
Translation cont'd
ahelwer
committed
d08e567
Translations runnable in test
ahelwer
committed
06f4fc0
Fix deadlocked SANY call
ahelwer
committed
9067e4d
Use maps instead of lists
ahelwer
committed
64b557d
Variable conversion supported
ahelwer
committed
cbbf735
Basic operator definition conversion supported
ahelwer
committed
886da6a
Convert many expressions
ahelwer
committed
36a0d03
Converted CHOOSE
ahelwer
committed
194f2db
Quantification conversion begin
ahelwer
committed
905e482
Quantification conversion complete
ahelwer
committed
ea19f36
Theorem name conversion
ahelwer
committed
86c46bb
Added comments
ahelwer
committed
22fc0fc
Proof conversion started
ahelwer
committed
92ca26b
Basic proof conversion complete
ahelwer
committed
45ce219
Simplified XML representation
ahelwer
committed
3728b62
Improved XML parsing
ahelwer
committed
b6611a5
Start elaboration process
ahelwer
committed
bfcb8c1
XML parsing: added data subtypes
ahelwer
committed
25c8396
Figuring out propertiesto attach to proof steps
ahelwer
committed
c0e4f2d
Parsed proof step names
ahelwer
committed
be84a11
Extract proof level from step names
ahelwer
committed
9f47fe1
Finish attaching proof name metadata
ahelwer
committed
4dc60f2
Propagate assumption/discovery of proof levels up and down tree
ahelwer
committed
1a1a17d
Flatten module
ahelwer
committed
9cf2c07
Now stuck on proof expansion
ahelwer
committed
fff604e
Proof expansion progress
ahelwer
committed
c2fd073
Translating Examples specs
ahelwer
committed
1bb3840
Fix theorem node translation
ahelwer
committed
a178534
Parse instance units
ahelwer
committed
1a19ad3
Translate recursive functions
ahelwer
committed
7a50609
Translate functions, ITE, and case
ahelwer
committed
e38625e
Translate INSTANCE substitutions
ahelwer
committed
60db57e
Translated CONSTANTS
ahelwer
committed
e57318f
Translated set filter
ahelwer
committed
f581aaa
Translated record sets
ahelwer
committed
3afc66f
Translated record constructor
ahelwer
committed
83203f7
Translated cartesian product
ahelwer
committed
7110ebb
Translated EXCEPT
ahelwer
committed
8f287e4
Translate fairness
ahelwer
committed
0ff4bea
Parse assume/prove and new symbol nodes
ahelwer
committed
935712a
Parsed use-or-hide
ahelwer
committed
02622c1
Converted use-or-hide
ahelwer
committed
a551164
XML parsing improved for BoundSymbol, OpDeclNode, UserDefinedOpNode
ahelwer
committed
4892ec6
Convert CASE proof step
ahelwer
committed
45e4b4f
Convert PICK proof step
ahelwer
committed
c1f19e2
Parse XML for all expression types
ahelwer
committed
35ec791
Convert PICK and TAKE proof steps properly
ahelwer
committed
dba8932
Convert CASE OTHER
ahelwer
committed
4161e7c
Convert all examples specs
ahelwer
committed
e7d6e2a
Enumerate SANY's built-in operators
ahelwer
committed
486974a
Support using community modules & apalache jars when parsing
ahelwer
committed
c4a9361
Upstream SANY DecimalNode fixes
ahelwer
committed
e41a76d
Upstream SANY LOCAL changes
ahelwer
committed
17306b5
Upstream SANY proof level changes
ahelwer
committed
35841fc
Upstream SANY EXTENDS addition
ahelwer
committed
c0004eb
Handle subexpressions (or rather don't)
ahelwer
committed
5b1167e
Convert HAVE proof steps
ahelwer
committed
77e66ed

Commits on Feb 27, 2026

Parse M!op type references
ahelwer
committed
34ab24e
Added location info for debugging ref resolve failures
ahelwer
committed
0590454
Convert DEFINE INSTANCE proof steps
ahelwer
committed
2145d71

Commits on Feb 28, 2026

Use TLAPM standard modules
ahelwer
committed
a4427b0
Improve error reporting
ahelwer
committed
30a68e6

Commits on Mar 2, 2026

Fixed proof step order bug
ahelwer
committed
9892d23
Removed unnecessary utility functions in xml
ahelwer
committed
68b7b70
Translated ASSUME/PROVE hypotheses
ahelwer
committed
bd4a5f8
Fully convert label nodes
ahelwer
committed
4e89248

Commits on Mar 12, 2026

Convert LAMBDA
ahelwer
committed
8c5ee32

Commits on Mar 13, 2026

Fix sany_tests, start work on semantic test escalation
ahelwer
committed
4e7e2f2

Commits on Mar 16, 2026

Semantic test framework
ahelwer
committed
38f024b

Commits on Mar 20, 2026

Adding semantic tests
ahelwer
committed
4d3647d

Commits on Mar 21, 2026

Promote s-expression conversion code from test to library
ahelwer
committed
f850406

Commits on Mar 24, 2026

Order unit-level definitions by position in file
ahelwer
committed
4a009d7

Commits on Mar 25, 2026

Fixed conversion of 0-arity builtins
ahelwer
committed
b1830f6
Validated basic theorem translation
ahelwer
committed
ae1597d

Commits on Mar 28, 2026

Tests for some proof types
ahelwer
committed
a975b11
Removed AddTwo
ahelwer
committed
8c94cae