Differences

This shows you the differences between two versions of the page.

--- creating:syntax [2025/03/24 20:11] – Defined subset of TLA⁺ to be parsed ahelwer
+++ creating:syntax [2025/04/06 23:20] (current) – Deleting page ahelwer
@@ Line 1: / Line 1: @@
-====== 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 [[https://github.com/tlaplus/rfcs/tree/2a772d9dd11acec5d7dedf30abfab91a49de48b8/language_standard/tests/tlaplus_syntax|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 [[https://github.com/tlaplus/Examples/blob/37236893f14527b4fc9f3963891eb2316c3de62e/specifications/DieHard/DieHard.tla|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.