Parsing TLA⁺ Syntax

TLA⁺ is a large, complicated, and ambiguous language that takes a huge amount of work to parse correctly & completely. This is assisted by a comprehensive test corpus exercising the language's nooks & crannies, but here we will make life easy on ourselves. This tutorial only uses a minimal subset of TLA⁺ syntax, just enough to handle the classic DieHard spec. While that may seem limiting, this tutorial tries to focus on the difficult & interesting parts of parsing the language instead of more mundane drudgework like handling all hundred-some user-definable operator symbols. You are encouraged to extend this minimal core as you wish; language tooling is best developed incrementally! Slowly filling in the details of this rough language sketch has a satisfying meditative aspect.

Here is what our minimal language subset includes:

• The ---- MODULE Name ---- header and ==== footer
• Named parameterized operator definitions like op == ... and op(x, y, z) == ...
• Comments, both single-line like \* comment text and nestable multi-line like (* comment text *)
• Declaration of VARIABLES
• The ENABLED prefix operator
• Finite set literals, like {1, 2, 3, 4, 5}
• Some infix operators: \in, .., =, #, +, -, <, /\, and \/
• The variable-priming suffix operator
• Vertically-aligned conjunction & disjunction lists
• The IF/THEN/ELSE construct
• Natural numbers like 0, 5, 10, etc.
• Boolean values TRUE and FALSE

Notably, the following will not be covered in this tutorial:

• PlusCal
• Declaring CONSTANTS
• Nesting modules or importing other modules through EXTENDS or INSTANCE
• Set map & set filter syntax, like {e \in S : P(e)}
• Universal & existential quantification, like \E e \in S : P(e)
• The CHOOSE operator
• Functions, like [x \in Nat |-> 2*x] or the function EXCEPT syntax
• Sequences, like <<1, 2, 3, 4, 5>>
• The LET/IN construct
• Temporal- or action-level operators like [], <>, [A]_v, or WF_v(A)
• Higher-order operator parameters like op(F(_), x) == ...
• The TLA⁺ proof language

As outlined above, you are free to add these missing features (or others) as you wish.