Differences

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

--- creating:syntax [2025/03/27 17:44] – Added starting code snippet 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.
-===== Preparation =====
-Read section I (the first three chapters) of free online textbook //[[https://craftinginterpreters.com/contents.html|Crafting Interpreters]]// by Robert Nystrom.
-We will be closely following the material in this book, modifying it to our uses.
-The first two chapters are a nice introduction and overview of language implementation generally.
-Chapter three specifies a toy language called Lox, to be used as an object of study for the remainder of the book.
-Our minimal TLA⁺ subset has some similarity to Lox with regard to expressions involving integers and booleans, but also differences - you can skip the section on closures (unless you want to implement higher-order operator parameters yourself) and the section on classes.
-What's important is that it's similar enough for all the fundamentals to still apply!
-[[https://craftinginterpreters.com/a-tree-walk-interpreter.html|Section II]] (A Tree-Walk Interpreter) is where we start to merge with and modify the given code.
-Everything up to [[https://craftinginterpreters.com/scanning.html#token-type|section 4.2.1]] can be left unchanged from what's given, although of course it makes sense to change some of the names from "Lox" to "TlaPlus" or similar.
-You should thus have followed along and arrived at the following file ''TlaPlus.java'':
-<code java>
-package com.craftinginterpreters.TlaPlus;
-import java.io.BufferedReader;
-import java.io.IOException;
-import java.io.InputStreamReader;
-import java.nio.charset.Charset;
-import java.nio.file.Files;
-import java.nio.file.Paths;
-import java.util.List;
-public class TlaPlus {
-  public static void main(String[] args) throws IOException {
-    if (args.length > 1) {
-      System.out.println("Usage: jlox [script]");
-      System.exit(64);
-    } else if (args.length == 1) {
-      runFile(args[0]);
-    } else {
-      runPrompt();
-    }
-  }
-  private static void runFile(String path) throws IOException {
-    byte[] bytes = Files.readAllBytes(Paths.get(path));
-    run(new String(bytes, Charset.defaultCharset()));
-  }
-  private static void runPrompt() throws IOException {
-    InputStreamReader input = new InputStreamReader(System.in);
-    BufferedReader reader = new BufferedReader(input);
-    for (;;) {
-      System.out.print("> ");
-      String line = reader.readLine();
-      if (line == null) break;
-      run(line);
-    }
-  }
-  private static void run(String source) {
-    Scanner scanner = new Scanner(source);
-    List<Token> tokens = scanner.scanTokens();
-    // For now, just print the tokens.
-    for (Token token : tokens) {
-      System.out.println(token);
-    }
-  }
-}
-</code>