creating:evaluation

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
creating:evaluation [2025/04/17 15:34] – Split evaluation tutorial into its own page ahelwercreating:evaluation [2025/06/19 16:31] (current) – LEFT_BRACE interpretation splits out Object value = ahelwer
Line 1: Line 1:
-======= Handling Constant TLA⁺ Expressions =======+======= Evaluating Constant TLA⁺ Expressions =======
  
-This tutorial page covers the next two chapters in //Crafting Interpreters//: +Now that we can parse expressions, let's evaluate them! 
-  - [[https://craftinginterpreters.com/representing-code.html|Chapter 5: Representing Code]] +Here we follow the material in [[https://craftinginterpreters.com/evaluating-expressions.html|Chapter 7]] of //Crafting Interpreters//. 
-  - [[https://craftinginterpreters.com/parsing-expressions.html|Chapter 6: Parsing Expressions]]+It's an exciting chapter, so let's jump in.
  
-Same as the book, we //could// build a parser for our entire minimal TLA⁺ language subset before moving on to interpreting it, but that would be boring! +====== Section 7.1: Representing Values ======
-Instead we focus on a simple vertical slice of the language: expressions. +
-And not just any expressions, constant expressions - expressions that do not contain variables or identifiers that we would have to resolve. +
-Just primitive literal values stuck together, not too much more advanced than a simple calculator app. +
-This will give us a skeleton on which to hang the rest of the language.+
  
-Each section in this tutorial corresponds to one or more sections of //Crafting Interpreters// (henceforth referred to as "the book"). +In [[https://craftinginterpreters.com/evaluating-expressions.html#representing-values|section 7.1]] we define a mapping from language values to internal Java values. 
-First read the section of the book, then read the corresponding commentary & modifications given by this tutorial.+Our mapping for TLA⁺ is fairly similar to Lox, although we use ''Integer'' instead of ''Double'' for number values and also have a set type. 
 +TLA⁺ thankfully lacks ''nil'' types.
  
-====== Chapter 5: Representing Code ======+^ TLA⁺ type      ^ Java representation       ^ 
 +| Any TLA⁺ value | ''Object''                | 
 +| Boolean        | ''Boolean''               | 
 +| number         | ''Integer''               | 
 +| set            | ''java.util.Set<Object>'' |
  
-[[https://craftinginterpreters.com/representing-code.html|Chapter 5]] focuses more on concepts than code, so this section will not have many TLA⁺-specific modifications. +Java does a huge amount of work for us with the capabilities of the ''Object'' type, as we'll see.
-However, since this tutorial is intended to be self-contained code-wise, all necessary code is reproduced.+
  
-===== Section 5.1: Context-Free Grammars =====+====== Section 7.2: Representing Values ======
  
-Everything before [[https://craftinginterpreters.com/representing-code.html#a-grammar-for-lox-expressions|Section 5.1.3: A Grammar for Lox expressions]] applies equally to TLA⁺. +[[https://craftinginterpreters.com/evaluating-expressions.html#evaluating-expressions|Section 7.2]] is where we start laying down interpreter code. 
-The ambiguous first-draft grammar for Lox expressions can be adapted to TLA⁺: +Create a new file ''Interpreter.java'' with the highlighted lines changed or added compared with the book:
-<code eiffel> +
-expression     → literal +
-               | unary +
-               | binary +
-               | ternary +
-               | variadic +
-               | grouping ;+
  
-literal        → NUMBER | "TRUE" | "FALSE" ; +<code java [highlight_lines_extra="1,3,4"]> 
-grouping       → "(" expression ")" ; +package tla;
-unary          → (( "ENABLED" | "-" ) expression ) | ( expression "'" ) ; +
-binary         → expression operator expression ; +
-ternary        → "IF" expression "THEN" expression "ELSE" expression; +
-variadic       → "{" ( expression ( "," expression )* )? "}" +
-operator       → "=" | "+" | "-" | ".." | "/\" | "\/" | "<"  | "\in" ; +
-</code> +
-There are a few interesting differences. +
-The ''unary'' rule now captures both prefix //and// suffix operators, which both only accept a single parameter. +
-The ''ternary'' rule matches the ''IF''/''THEN''/''ELSE'' operator, with the three parameters being the predicate, the true branch, and the false branch. +
-The operators are changed to the set of operators defined in our TLA⁺ implementation. +
-These are all the expressions we can use without introducing the concept of identifiers referring to something else.+
  
-There is also the ''variadic'' rule matching finite set literals like ''{1, 2, 3}'' or the empty set ''{}''. +import java.util.Set; 
-This one is so named because it's where we'll put operators accepting varying numbers of parameters. +import java.util.HashSet;
-It's kind of weird to think of the finite set literal ''{1, 2, 3}'' as an operator, but it is! +
-The only difference between ''{1, 2, 3}'' and an operator like ''constructSet(1, 2, 3)'' is syntactic sugar. +
-This is the perspective of a language implementer. +
-Later on we will extend the definition of ''variadic'' to include vertically-aligned conjunction & disjunction lists.+
  
-===== Section 5.2: Implementing Syntax Trees =====+class Interpreter implements Expr.Visitor<Object> { 
 +} 
 +</code>
  
-While some programmers might have an aversion to generating code, the approach taken in the book is actually very convenient - as you will discover if you take some time to prototype & play around with different class representations of the parse tree! +If your IDE supports it, get it to automatically add all necessary stub methods to implement the ''Expr.Visitor<Object>'' interface; we'll be filling these in, defining the interpretation of every expression type!
-In [[https://craftinginterpreters.com/representing-code.html#metaprogramming-the-trees|Section 5.2.2: Metaprogramming the trees]], the main differences in the ''GenerateAst'' class reflect our modification of the Lox grammar in the previous section:+
  
-<code java [highlight_lines_extra="19,20,21"]> +Let's start with defining the value of literals. 
-package tool;+Our code is completely unchanged from the book; add this ''visitLiteralExpr()'' method in the ''Interpreter'' class:
  
-import java.io.IOException; +<code java> 
-import java.io.PrintWriter; +  @Override 
-import java.util.Arrays; +  public Object visitLiteralExpr(Expr.Literal expr) { 
-import java.util.List; +    return expr.value;
- +
-public class GenerateAst { +
-  public static void main(String[] args) throws IOException { +
-    if (args.length != 1) { +
-      System.err.println("Usage: generate_ast <output directory>"); +
-      System.exit(64); +
-    } +
-    String outputDir = args[0]; +
-    defineAst(outputDir, "Expr", Arrays.asList( +
-      "Binary   : Expr left, Token operator, Expr right", +
-      "Grouping : Expr expression", +
-      "Literal  : Object value", +
-      "Unary    : Token operator, Expr expr", +
-      "Ternary  : Token operator, Expr first, Expr second, Expr third", +
-      "Variadic : Token operator, List<Expr> parameters" +
-    ));+
   }   }
-} 
 </code> </code>
  
-In the ''defineAst'' function, we only need to modify the output code so that it uses the package ''.tla'' instead of ''.lox''; add this after the ''main'' method of ''GenerateAst'':+Our code for evaluating grouping (parentheses) is similarly unchanged from the book:
  
-<code java [highlight_lines_extra="7"]> +<code java> 
-  private static void defineAst( +  @Override 
-      String outputDir, String baseName, List<String> types) +  public Object visitGroupingExpr(Expr.Grouping expr) { 
-      throws IOException { +    return evaluate(expr.expression);
-    String path = outputDir + "/" + baseName + ".java"; +
-    PrintWriter writer = new PrintWriter(path, "UTF-8"); +
- +
-    writer.println("package tla;"); +
-    writer.println(); +
-    writer.println("import java.util.List;"); +
-    writer.println(); +
-    writer.println("abstract class " + baseName + " {"); +
- +
- +
-    // The AST classes. +
-    for (String type : types) { +
-      String className = type.split(":")[0].trim(); +
-      String fields = type.split(":")[1].trim(); +
-      defineType(writer, baseName, className, fields); +
-    } +
-    writer.println("}"); +
-    writer.close();+
   }   }
 </code> </code>
  
-Finally, the ''defineType'' method - added after the ''defineAst'' method - is unchanged:+This uses the ''evaluate()'' helper method; add it to the ''Interpreter'' class:
  
 <code java> <code java>
-  private static void defineType( +  private Object evaluate(Expr expr) { 
-      PrintWriter writer, String baseName, +    return expr.accept(this);
-      String className, String fieldList) { +
-    writer.println("  static class " + className + " extends " + +
-        baseName + " {"); +
- +
-    // Constructor. +
-    writer.println("    " + className + "(" + fieldList + ") {"); +
- +
-    // Store parameters in fields. +
-    String[] fields = fieldList.split(", "); +
-    for (String field : fields) { +
-      String name = field.split(" ")[1]; +
-      writer.println("      this." + name + " = " + name + ";"); +
-    } +
- +
-    writer.println("    }"); +
- +
-    // Fields. +
-    writer.println(); +
-    for (String field : fields) { +
-      writer.println("    final " + field + ";"); +
-    } +
- +
-    writer.println("  }");+
   }   }
 </code> </code>
  
 +==== Evaluating Unary Operators ====
  
-===== Section 5.3: Working with Trees =====+Our first real difference from the book is in the ''visitUnaryExpr()'' method. 
 +Recall that since our ''Expr.Unary'' type represents both prefix and suffix operators, we don't call its parameter ''right'' as in the book. 
 +We also don't pre-emptively evaluate the inner expression at the top of the method; this is important for when we later fully implement the prime and enabled operators. 
 +The method is structured as a switch statement handling all possible unary operators: 
 +<code java> 
 +  @Override 
 +  public Object visitUnaryExpr(Expr.Unary expr) { 
 +    switch (expr.operator.type) { 
 +      case PRIME: {
  
-[[https://craftinginterpreters.com/representing-code.html#working-with-trees|Section 5.3]] introduces the Visitor pattern. +      } case ENABLED: {
-No TLA⁺-specific differences are necessary when modifying ''GenerateAst'' to support it. +
-Insert this line in ''defineAst()'': +
-<code java [highlight_lines_extra="3"]> +
-    writer.println("abstract class " + baseName + " {");+
  
-    defineVisitor(writer, baseName, types);+      } case NOT: {
  
-    // The AST classes. +      } case MINUS: {
-</code>+
  
-This calls the ''defineVisitor'' function which writes the visitor interface, defined as follows: +      } default: { 
-<code java> +        // Unreachable. 
-  private static void defineVisitor( +        return null; 
-      PrintWriter writer, String baseName, List<String> types) { +      }
-    writer.println("  interface Visitor<R> {"); +
- +
-    for (String type : types) { +
-      String typeName = type.split(":")[0].trim(); +
-      writer.println("    R visit" + typeName + baseName + "(" + +
-          typeName + " " + baseName.toLowerCase() + ");");+
     }     }
- 
-    writer.println("  }"); 
   }   }
 </code> </code>
  
-Again insert some lines in ''defineAst()'' to create the abstract ''accept'' method: +Here's how we define the negative prefix operator; while the book casts the operand to a ''double'', here we cast it to an ''int'': 
-<code java [highlight_lines_extra="4,5,6"]> +<code java [highlight_lines_extra="2,3"]> 
-      defineType(writer, baseName, className, fields); +      } case MINUS: { 
-    } +        Object operand = evaluate(expr.expr); 
- +        return -(int)operand; 
-    // The base accept() method. +      } default: {
-    writer.println(); +
-    writer.println("  abstract <R> R accept(Visitor<R> visitor);"); +
- +
-    writer.println("}");+
 </code> </code>
  
-Finally, insert some lines in ''defineType'' to add a types-specific ''accept'' method in each output class: +Note that the negative prefix operator is not actually a built-in operator of TLA⁺. 
-<code java [highlight_lines_extra="3,4,5,6,7,8,9"]> +It is defined in the ''Integers'' standard module, and TLA⁺ users need to import that module to access it. 
-    writer.println("    }"); +However, because our minimal TLA⁺ language subset lacks module importing, for convenience we just define some common arithmetic operators as built-in. 
- +You can find more information about the built-in TLA⁺ operators in chapter 16 of //[[https://lamport.azurewebsites.net/tla/book.html|Specifying Systems]]// by Leslie Lamport, or [[https://github.com/tlaplus/tlaplus/blob/13e5a39b5368a6da4906b8ed1c2c1114d2e7de15/tlatools/org.lamport.tlatools/src/tla2sany/semantic/BuiltInOperators.java#L80-L153|this SANY source file]].
-    // Visitor pattern. +
-    writer.println(); +
-    writer.println("    @Override"); +
-    writer.println("    <R> R accept(Visitor<R> visitor) {"); +
-    writer.println("      return visitor.visit" + +
-        className + baseName + "(this);"); +
-    writer.println("    }");+
  
-    // Fields.+Our logical-not prefix operator is denoted by the ''NOT'' token type instead of ''BANG'' as in Lox. 
 +We also have no use for the ''isTruthy()'' helper method from the book, since TLA⁺ is quite strict: only Boolean values can be given to Boolean operators! 
 +Add this code to ''visitUnaryExpr()'': 
 +<code java [highlight_lines_extra="2,3"]> 
 +      } case NOT: { 
 +        Object operand = evaluate(expr.expr); 
 +        return !(boolean)operand; 
 +      } case MINUS: {
 </code> </code>
-Our generated syntax tree node types now support the visitor pattern! 
  
-===== Section 5.4: A (Not Very) Pretty Printer ===== +We still have two more unary operators to define: ''ENABLED'', and the prime operator. 
- +Both are trivial in this domain but will become much more complicated later on. 
-[[https://craftinginterpreters.com/representing-code.html#a-not-very-pretty-printer|Section 5.4]] provides an implementation of a visitor called ''AstPrinter'' that prints out the parse tree. +For constant expressions, ''ENABLED'' is always false and prime is just whatever the inner expression evaluates to. 
-There are a few TLA⁺-specific modifications, starting of course with the package name: +Add the highlighted code to ''visitUnaryExpr()'': 
- +<code java [highlight_lines_extra="2,4"]> 
-<code java [highlight_lines_extra="1"]> +      case PRIME: { 
-package tla; +        return evaluate(expr.expr); 
- +      } case ENABLED: { 
-class AstPrinter implements Expr.Visitor<String> { +        return false; 
-  String print(Expr expr) { +      } case NOT: {
-    return expr.accept(this); +
-  } +
-}+
 </code> </code>
  
-We also have some modifications and additions to the ''visit'' methods of the ''AstPrinter'' class, again reflecting our modified TLA⁺-specific grammar:+==== Evaluating Binary Operators ====
  
-<code java [highlight_lines_extra="20,23,24,25,26,27,29,30,31,32"]>+Unlike Lox, addition in TLA⁺ is only defined between two numbers (at least in its standard ''Integers'' module definition). 
 +Here's how we define our basic binary arithmetic & comparison operators; add a ''visitBinaryExpr()'' method in the ''Interpreter'' class (highlighted code differs from the book): 
 +<code java [highlight_lines_extra="8,9,10,11,12,13,14"]>
   @Override   @Override
-  public String visitBinaryExpr(Expr.Binary expr) { +  public Object visitBinaryExpr(Expr.Binary expr) { 
-    return parenthesize(expr.operator.lexeme, +    Object left = evaluate(expr.left); 
-                        expr.left, expr.right); +    Object right = evaluate(expr.right);
-  }+
  
-  @Override +    switch (expr.operator.type) { 
-  public String visitGroupingExpr(Expr.Grouping expr) { +      case MINUS: 
-    return parenthesize("group", expr.expression); +        return (int)left - (int)right; 
-  }+      case PLUS: 
 +        return (int)left + (int)right; 
 +      case LESS_THAN: 
 +        return (int)left < (int)right; 
 +      case EQUAL: 
 +        return left.equals(right); 
 +    }
  
-  @Override +    // Unreachable. 
-  public String visitLiteralExpr(Expr.Literal expr) { +    return null;
-    if (expr.value == null) return "nil"; +
-    return expr.value.toString(); +
-  } +
- +
-  @Override +
-  public String visitUnaryExpr(Expr.Unary expr) { +
-    return parenthesize(expr.operator.lexeme, expr.expr); +
-  } +
- +
-  @Override +
-  public string visitTernaryExpr(Expr.Ternary expr) { +
-    return parenthesize(expr.operator.lexeme, expr.first, +
-                        expr.second, expr.third); +
-  } +
- +
-  @Override +
-  public string visitVariadicExpr(Expr.Variadic expr) { +
-    return parenthesize(expr.operator.lexeme, +
-                        expr.parameters.toArray(Expr[]::new));+
   }   }
 </code> </code>
  
-The ''parenthesize'' method is unchanged from the book and should be inserted after the ''visit'' methods:+Note that since we don't have to worry about ''null'' values, we don't need the ''isEqual()'' helper method from the book and can use Java's ''Object.equals()'' method directly. 
 +However, this actually gives us different equality semantics from TLC. 
 +In TLC, evaluating things like ''123 = TRUE'' results in a runtime error instead of evaluating to ''false'' as will be the case here. 
 +In the interest of simplicity we are fine with keeping these looser semantics. 
 +See the challenges at the end of this tutorial page if you're interested in more closely matching the semantics of TLC.
  
-<code java> +Let's take our first foray into sets by defining the set membership operator in ''visitBinaryExpr()'':
-  private String parenthesize(String name, Expr... exprs) { +
-    StringBuilder builder = new StringBuilder();+
  
-    builder.append("(").append(name); +<code java [highlight_lines_extra="2,3"]> 
-    for (Expr expr : exprs) { +    switch (expr.operator.type) { 
-      builder.append(" "); +      case IN: 
-      builder.append(expr.accept(this)); +        return ((Set<?>)right).contains(left); 
-    } +      case MINUS:
-    builder.append(")"); +
- +
-    return builder.toString(); +
-  }+
 </code> </code>
  
-It isn't necessary to define a ''main'' method in the ''AstPrinter'' class, but if you'd like to try it out you are free to copy the one given in the book.+The question mark is some unusual Java syntax you probably haven't seen before, called a [[https://docs.oracle.com/javase/tutorial/java/generics/wildcards.html|wildcard]]. 
 +It has to do with //covariance//, which you can read about at the end of the chapter in the book. 
 +Think of it as casting the right operand to //some kind// of set, so we can access the ''Set.contains()'' method. 
 +It is tempting to cast it to ''Set<Object>'' (as we only ever create ''Set<Object>'' instances) but this produces a compiler warning.
  
-====== Chapter 6: Parsing Expressions ======+Similar to equality, we get looser semantics here than with TLC. 
 +TLC will emit a runtime error when evaluating the expression ''TRUE \in {1, 2, 3}'', while our interpreter will simple evaluate it to ''false''. 
 +Again this is acceptable.
  
-In [[https://craftinginterpreters.com/parsing-expressions.html|Chapter 6]], we finally build a parse tree out of our tokens!+Now for something more complicated. 
 +Here's the set construction helper operator ''..'', also defined in ''visitBinaryExpr()''; this constructs a set containing all numbers between the left and right parameters, inclusive:
  
-===== Section 6.1: Ambiguity and the Parsing Game ===== +<code java [highlight_lines_extra="2,3,4,5,6,7,8,9,10,11"]> 
- +    switch (expr.operator.type) { 
-First, as in [[https://craftinginterpreters.com/parsing-expressions.html#ambiguity-and-the-parsing-game|section 6.1 of the book]], we have to disambiguate our grammar. +      case DOT_DOT: 
-The way that precedence works in TLA⁺ is different from Lox, and indeed different from most other languages! +        Set<Object> set = new HashSet<Object>(); 
-One side-quote from this section of the book reads: +        int lower = (int)left; 
- +        int higher = (int)right; 
->While not common these days, some languages specify that certain pairs of operators have no relative precedence. That makes it a syntax error to mix those operators in an expression without using explicit grouping. +        if (lower <= higher) { 
- +          for (int i = lower; i <= higher; i++) { 
->Likewise, some operators are *non-associative*. That means it’s an error to use that operator more than once in a sequence. For example, Perl’s range operator isn’t associative, so a .. b is OK, but a .. b .. c is an error. +            set.add(i); 
- +          } 
-TLA⁺ has both of these features! +        } 
-Instead of operators occupying a slot in some hierarchy of precedence, each operator has a precedence //range//. +        return set; 
-When the precedence ranges of two operators overlap it is a parse error. +      case IN:
-For example, the ''ENABLED'' prefix operator has precedence range 4-15, and the prime operator has precedence range 15-15; thus, the following expression has a precedence conflict and should not parse: +
-<code> +
-ENABLED x'+
 </code> </code>
-Users must add parentheses to indicate their desired grouping in the expression. 
-Similarly, some operators like ''='' are not associative so ''a = b = c'' should be a parse error. 
-Both of these factors combine to make our operator parsing code quite a bit different from that given in the book. 
-Worry not, it can still be made terse and understandable! 
  
-===== Section 6.2: Recursive Descent Parsing =====+So expressions like ''1 .. 3'' produce the set ''{1, 2, 3}'' while ''3 .. 2'' produces the empty set ''{}''. 
 +We use ''Set<Object>'', so our sets can hold any value you can imagine including nested sets. 
 +It's incredible how much we get for free here; Java sets even implement value-based de-duplication and equality comparison for us for arbitrarily-nested sets!
  
-[[https://craftinginterpreters.com/parsing-expressions.html#recursive-descent-parsing|Section 6.2]] is where we start writing our parser in the recursive descent style. +==== Evaluating Other Operators ====
-Recursive descent can seem a bit magical even if you're used to reasoning about recursive functions! +
-Unfortunately TLA⁺ requires us to push this magic even further. +
-We'll take it step by step.+
  
-We start with the same basic ''Parser.java'' file as in the book, renaming ''lox'' to ''tla'' in the package name as usual. +Our ''IF''/''THEN''/''ELSE'' and set constructor operators are all that remain. 
-We also add an import for ''ArrayList'', which we will later make use of when parsing variadic operators:+Add this ''visitTernaryExpr()'' method to the ''Interpreter'' class:
  
-<code java [highlight_lines_extra="1,4,6"]> +<code java> 
-package tla; +  @Override 
- +  public Object visitTernaryExpr(Ternary expr) { 
-import java.util.List; +    switch (expr.operator.type) { 
-import java.util.ArrayList; +      case IF: 
- +        Object conditional = evaluate(expr.first); 
-import static tla.TokenType.*; +        return (boolean)conditional ? 
- +            evaluate(expr.second) : evaluate(expr.third); 
-class Parser { +      default: 
-  private final List<Token> tokens; +        // Unreachable. 
-  private int current = 0; +        return null; 
- +    }
-  Parser(List<Token> tokens) { +
-    this.tokens = tokens;+
   }   }
-} 
 </code> </code>
  
-Now we hit our first major difference. +''IF''/''THEN''/''ELSE'' has a straightforward translation to Java's ''?''/'':'' mixfix operator. 
-In Lox, precedence is given by a small hierarchy of named rules like ''equality'', ''comparison'', ''term'', etc. +Note our definition is also short-circuiting. 
-TLA⁺ is more complicated than that. + 
-The full language has around 100 operators spanning precedences 1 to 15! +Finally, here's how we define the set construction operator; add this ''visitVariadicExpr()'' method in the ''Interpreter'' class:
-If we wanted to match the book's style we'd have to write a tower of recursive functions like: +
-<code java> +
-private Expr operatorExpressionPrec1() { ... } +
-private Expr operatorExpressionPrec2() { ... } +
-private Expr operatorExpressionPrec3() { ... } +
-... +
-private Expr operatorExpressionPrec15() { ... } +
-</code> +
-where each ''operatorExpressionPrecN()'' function parses all the prefix, infix, and postfix operators of precedence ''N'', and calls ''operatorExpressionPrecN+1()''. +
-Life is too short for this. +
-Instead, we'll adopt a technique alluded to in the text: +
->If you wanted to do some clever Java 8, you could create a helper method for parsing a left-associative series of binary operators given a list of token types, and an operand method handle to simplify this redundant code.+
  
-Here's the skeleton of our operator parsing function; the trick is to make the precedence a parameter to the function instead of a component of the name. 
-Add this code after the ''Parser()'' constructor: 
 <code java> <code java>
-  private Expr expression() { +  @Override 
-    return operatorExpression(1); +  public Object visitVariadicExpr(Expr.Variadic expr) { 
-  } +    switch (expr.operator.type) { 
- +      case LEFT_BRACE: 
-  private Expr operatorExpression(int prec) { +        Set<Object> set = new HashSet<Object>(); 
-    if (prec == 16) return primary(); +        for (Expr parameter : expr.parameters) { 
- +          Object value = evaluate(parameter); 
-    Expr expr = operatorExpression(prec + 1); +          set.add(value); 
- +        } 
-    return expr;+        return set; 
 +      default: 
 +        // Unreachable. 
 +        return null; 
 +    }
   }   }
 </code> </code>
  
-Before filling out ''operatorExpression()'', we'll add the helper methods; these form an incredibly well-designed parsing API and are unchanged from the book:+====== Section 7.3: Runtime Errors ======
  
-<code java> +In [[https://craftinginterpreters.com/evaluating-expressions.html#runtime-errors|section 7.3]] we add some error detection & reporting to our interpreter code.
-  private boolean match(TokenType... types) { +
-    for (TokenType type : types) { +
-      if (check(type)) { +
-        advance(); +
-        return true; +
-      } +
-    }+
  
-    return false; +Here's our variant of the ''checkNumberOperand()'' and ''checkNumberOperands()'' methods given in the book, using ''Integer'' instead of ''Double''; put these in the ''Interpreter'' class (highlighted code differs from the book):
-  }+
  
-  private boolean check(TokenType type) { +<code java [highlight_lines_extra="2,8"]> 
-    if (isAtEnd()) return false; +  private void checkNumberOperand(Token operator, Object operand) { 
-    return peek().type == type;+    if (operand instanceof Integer) return; 
 +    throw new RuntimeError(operator, "Operand must be a number.");
   }   }
  
-  private Token advance() { +  private void checkNumberOperands(Token operator, 
-    if (!isAtEnd()) current++; +                                   Object left, Object right) { 
-    return previous(); +    if (left instanceof Integer && right instanceof Integer) return;
-  } +
- +
-  private boolean isAtEnd() { +
-    return peek().type == EOF; +
-  } +
- +
-  private Token peek() { +
-    return tokens.get(current); +
-  }+
  
-  private Token previous() { +    throw new RuntimeError(operator, "Operands must be numbers.");
-    return tokens.get(current - 1);+
   }   }
 </code> </code>
  
-Now we have to define a table of operators with their details. +Create a new ''RuntimeError.java'' file. 
-For this, create a new file ''Operator.java'' containing a class recording operator fix type, token type, associativity, and precedence range:+Contents are identical to that give in the book except for the package name:
  
-<code java>+<code java [highlight_lines_extra="1"]>
 package tla; package tla;
  
-enum Fix { +class RuntimeError extends RuntimeException { 
-  PREFIX, INFIX, POSTFIX +  final Token token;
-}+
  
-class Operator { +  RuntimeError(Token token, String message) { 
-  final Fix fix; +    super(message);
-  final TokenType token; +
-  final boolean assoc; +
-  final int lowPrec; +
-  final int highPrec; +
- +
-  public Operator(Fix fix, TokenType token, boolean assoc, +
-                  int lowPrec, int highPrec) { +
-    this.fix = fix;+
     this.token = token;     this.token = token;
-    this.assoc = assoc; 
-    this.lowPrec = lowPrec; 
-    this.highPrec = highPrec; 
   }   }
 } }
 </code> </code>
  
-For convenience, import the ''Fix'' enum values in ''Parser.java'' so they can be referenced directly: +We also need a helper for booleans since TLA⁺ is more strict about them than Lox; add this to the ''Interpreter'' class:
- +
-<code java [highlight_lines_extra="7"]> +
-package tla; +
- +
-import java.util.List; +
-import java.util.ArrayList; +
- +
-import static tla.TokenType.*; +
-import static tla.Fix.*; +
- +
-class Parser { +
-</code> +
- +
- +
-You can find operator attributes on page 271 of //[[https://lamport.azurewebsites.net/tla/book.html|Specifying Systems]]// by Leslie Lamport, or [[https://github.com/tlaplus/tlaplus/blob/13e5a39b5368a6da4906b8ed1c2c1114d2e7de15/tlatools/org.lamport.tlatools/src/tla2sany/parser/Operators.java#L130-L234|this TLA⁺ tools source file]]. +
-We use a small subset of these operators. +
-Record their attributes in a table in ''Parser.java'', below ''operatorExpression()'':+
  
 <code java> <code java>
-  private static final Operator[] operators = new Operator[] { +  private void checkBooleanOperand(Token operator, Object operand) { 
-    new Operator(PREFIX,  NOT,        true,   4,  4 ), +    if (operand instanceof Boolean) return; 
-    new Operator(PREFIX,  ENABLED,    false,  4,  15), +    throw new RuntimeError(operator, "Operand must be a boolean."); 
-    new Operator(PREFIX,  MINUS,      true,   12, 12), +  }
-    new Operator(INFIX,   AND,        true,   3,  3 ), +
-    new Operator(INFIX,   OR,         true,   3,  3 ), +
-    new Operator(INFIX,   IN,         false,  5,  5 ), +
-    new Operator(INFIX,   EQUAL,      false,  5,  5 ), +
-    new Operator(INFIX,   LESS_THAN,  false,  5,  5 ), +
-    new Operator(INFIX,   DOT_DOT,    false,  9,  9 ), +
-    new Operator(INFIX,   PLUS,       true,   10, 10), +
-    new Operator(INFIX,   MINUS,      true,   11, 11), +
-    new Operator(POSTFIX, PRIME,      false,  15, 15), +
-  };+
 </code> </code>
  
-Here's something a bit odd. +Finally, we need a helper for checking whether an operand is a set:
-In TLA⁺, the infix minus operator (subtraction) has higher precedence at 11-11 than the infix plus operator (addition) at 10-10! +
-In grade school you probably learned acronyms like PEMDAS or BEDMAS to remember the order of operations in arithmetic. +
-Really, you learned parsing rules! +
-Now when writing our own parsing algorithm we come to understand that the order of these operations is not inscribed in the bedrock of mathematical truth but instead is a simple convention of mathematical notation. +
-TLA⁺ subverts this by parsing the expression ''a + b - c'' as ''a + (b - c)'' instead of the PEMDAS-style ''(a + b) - c''. +
-While this design decision is unusual, it is [[https://groups.google.com/g/tlaplus/c/Bt1fl8GvizE/m/ohYTfQWiCgAJ|unlikely to cause any problems]].+
  
-We need one more helper method before we can start working on ''operatorExpression()'': a superpowered ''match()'' method specific to operators, which will try to match any operators of a given fix type & (low) precedence. 
-Add this code above ''match()'': 
 <code java> <code java>
-  private Operator matchOp(Fix fix, int prec) { +  private void checkSetOperand(Token operator, Object operand) { 
-    for (Operator op : operators) { +    if (operand instanceof Set<?>) return; 
-      if (op.fix == fix && op.lowPrec == prec) { +    throw new RuntimeError(operator, "Operand must be a set.");
-        if (match(op.token)) return op; +
-      } +
-    } +
- +
-    return null;+
   }   }
 </code> </code>
  
-Okay, we're all set for the main event! +Now add these checks to our interpreter code. 
-Here is how we modify ''operatorExpression()'' to parse infix operators. +Here's negative: 
-You can see a strong resemblance to the infix operator parsing code given in the book (new lines highlighted): +<code java [highlight_lines_extra="3"]> 
-<code java [highlight_lines_extra="4,7,8,9,10,11"]> +      } case MINUS: { 
-  private Expr operatorExpression(int prec) { +        Object operand = evaluate(expr.expr); 
-    if (prec == 16) return primary(); +        checkNumberOperand(expr.operator, operand); 
- +        return -(int)operand; 
-    Operator op; +      } default: {
- +
-    Expr expr = operatorExpression(prec + 1); +
-    while ((op = matchOp(INFIX, prec)) != null) { +
-      Token operator = previous(); +
-      Expr right = operatorExpression(op.highPrec + 1); +
-      expr = new Expr.Binary(expr, operator, right); +
-    } +
- +
-    return expr; +
-  }+
 </code> </code>
- +Logical not: 
-We use Java's combined conditional-assignment atop the ''while'' loop to make our code more terse, both checking whether any operators were matched and getting details of the matched operator if so. +<code java [highlight_lines_extra="3"]> 
-The interior of the ''while'' loop is largely identical to infix parsing logic from the book, except for when we recurse to a higher precedence level: in the book the code recurses one level above the matched operator's precedence, but here we go one level above the //upper bound// of the matched operator's precedence. +      } case NOT: { 
-It takes a bit of thinking to understand why this works for parsing expressions according to the precedence rules we want, but it does. +        Object operand = evaluate(expr.expr); 
-Take a minute to ponder it. +        checkBooleanOperand(expr.operator, operand); 
-If you still don't get it, wait until we have a fully-functional expression parser then play around with this line to see how it changes the behavior. +        return !(boolean)operand; 
- +      } case MINUS: {
-Our code implements precedence ranges, but assumes all infix operators are associative. +
-We need to modify the loop to return immediately if the infix operator is not associative: +
-<code java [highlight_lines_extra="5"]> +
-    while ((op = matchOp(INFIX, prec)) != null) { +
-      Token operator = previous(); +
-      Expr right = operatorExpression(op.highPrec + 1); +
-      expr = new Expr.Binary(expr, operator, right); +
-      if (!op.assoc) return expr; +
-    }+
 </code> </code>
- +Subtraction: 
-And that's how we parse infix operators! +<code java [highlight_lines_extra="2"]> 
-That was the most complicated case, so let's move on to prefix operators. +      case MINUS: 
-Again our code resembles the prefix operator parsing logic given in the book. +        checkNumberOperands(expr.operator, left, right); 
-Add this snippet near the top of ''operatorExpression()'': +        return (int)left - (int)right;
- +
-<code java [highlight_lines_extra="5,6,7,8,9,10"]> +
-  private Expr operatorExpression(int prec) { +
-    if (prec == 16) return primary(); +
- +
-    Operator op; +
-    if ((op = matchOp(PREFIX, prec)) != null) { +
-      Token opToken = previous(); +
-      Expr expr = operatorExpression( +
-                    op.assoc ? op.lowPrec : op.highPrec + 1); +
-      return new Expr.Unary(opToken, expr); +
-    } +
- +
-    Expr expr = operatorExpression(prec + 1);+
 </code> </code>
- +Addition: 
-Of note is the expression ''op.assoc ? op.lowPrec : op.highPrec + 1'' controlling the precedence level at which we recurse. +<code java [highlight_lines_extra="2"]> 
-To understand this expression, it is helpful to consider an example. +      case PLUS: 
-The negative prefix operator ''-1'' is associative, so we should be able to parse the expression ''--1'' as ''-(-1)''. +        checkNumberOperands(expr.operator, left, right); 
-In order to do that after consuming the first ''-'' we have to recurse into ''operatorExpression()'' //at the same precedence level//. +        return (int)left + (int)right;
-Then we will consume the second ''-'', then again recurse and ultimately consume ''1'' in our yet-to-be-defined ''primary'' method. +
-In contrast, the prefix operator ''ENABLED'' is not associative and has range 4-15. +
-In that case we want to reject the expression ''ENABLED ENABLED TRUE'', so we recurse at a level higher than ''ENABLED'''s upper precedence bound. +
-Thus the second ''ENABLED'' will not be matched and we will report a parse error using methods defined in chapter section 6.3. +
- +
-All that remains is to parse postfix operators. +
-These are not covered in the book, but they pretty much resemble infix operators without matching an expression on the right-hand side of the operator. +
-Add the highlighted code below the ''INFIX'' logic in ''operatorExpression()'': +
- +
-<code java [highlight_lines_extra="3,4,5,6,7"]> +
-    } +
- +
-    while ((op = matchOp(POSTFIX, prec)) != null) { +
-      Token opToken = previous(); +
-      expr = new Expr.Unary(opToken, expr); +
-      if (!op.assoc) break; +
-    } +
- +
-    return expr +
-  }+
 </code> </code>
- +Less than: 
-And that completes our operator parsing logic! +<code java [highlight_lines_extra="2"]> 
-All that remains is our ''primary()'' method. +      case LESS_THAN: 
-It is fairly similar to that given in the book, with some omissions since our minimal TLA⁺ subset does not contain strings or null values. +        checkNumberOperands(expr.operator, left, right); 
-Add this code after ''operatorExpression()'': +        return (int)left < (int)right;
- +
-<code java> +
-  private Expr primary() { +
-    if (match(FALSE)) return new Expr.Literal(false); +
-    if (match(TRUE)) return new Expr.Literal(true); +
- +
-    if (match(NUMBER)) { +
-      return new Expr.Literal(previous().literal); +
-    } +
- +
-    if (match(LEFT_PAREN)) { +
-      Expr expr = expression(); +
-      consume(RIGHT_PAREN, "Expect ')' after expression."); +
-      return new Expr.Grouping(expr); +
-    } +
-  }+
 </code> </code>
- +The ''..'' range set constructor: 
-We have two final additions to ''primary()'', the ''IF''/''THEN''/''ELSE'' operator and the set construction operator. +<code java [highlight_lines_extra="2"]> 
-Here's how we parse ''IF''/''THEN''/''ELSE''; add the highlighted code to the bottom of ''primary()'': +      case DOT_DOT: 
- +        checkNumberOperands(expr.operator, left, right); 
-<code java [highlight_lines_extra="4,5,6,7,8,9,10,11,12"]> +        Set<Object> set = new HashSet<Object>(); 
-      return new Expr.Grouping(expr); +</code> 
-    } +Set membership: 
- +<code java [highlight_lines_extra="2"]> 
-    if (match(IF)) { +      case IN: 
-      Token operator = previous(); +        checkSetOperand(expr.operator, right); 
-      Expr condition = expression(); +        return ((Set<?>)right).contains(left); 
-      consume(THEN, "'THEN' required after 'IF' expression."); +</code> 
-      Expr yes = expression(); +Finally, ''IF''/''THEN''/''ELSE'': 
-      consume(ELSE, "'ELSE' required after 'THEN' expression."); +<code java [highlight_lines_extra="3"]> 
-      Expr no = expression(); +      case IF: 
-      return new Expr.Ternary(operator, condition, yes, no); +        Object conditional = evaluate(expr.first); 
-    } +        checkBooleanOperand(expr.operator, conditional); 
-  }+        return (boolean)conditional ? 
 +            evaluate(expr.second) : evaluate(expr.third);
 </code> </code>
  
-And here's how we parse the set construction operator. +====== Section 7.4: Hooking Up the Interpreter ======
-Again add the highlighted code to the bottom of ''primary()'':+
  
-<code java [highlight_lines_extra="4,5,6,7,8,9,10,11,12,13,14"]> +We're very close! 
-      return new Expr.Ternary(operator, condition, yes, no); +In [[https://craftinginterpreters.com/evaluating-expressions.html#hooking-up-the-interpreter|section 7.4]] we put in the finishing touches to get to a real running TLA⁺ REPL! 
-    } +First, add this public ''interpret()'' method to the ''Interpreter'' class; highlighted line shows a difference from the book: 
- +<code java [highlight_lines_extra="6"]> 
-    if (match(LEFT_BRACE)) { +  void interpret(Expr expression) {  
-      Token operator = previous(); +    try { 
-      List<Expr> elements = new ArrayList<Expr>(); +      Object value = evaluate(expression); 
-      if (RIGHT_BRACE != peek().type) { +      System.out.println(stringify(value)); 
-        do { +    } catch (RuntimeError error) { 
-          elements.add(expression()); +      TlaPlus.runtimeError(error);
-        } while (match(COMMA)); +
-      } +
-      consume(RIGHT_BRACE, "'}' is required to terminate finite set literal."); +
-      return new Expr.Variadic(operator, elements);+
     }     }
   }   }
 </code> </code>
  
-This will handle expressions like ''{1,2,3}'' and (crucially) ''{}''. +In contrast to the book, our ''stringify()'' method is very simple; add this to the ''Interpreter'' class:
- +
-The ''consume()'' operator is defined in the next section, along with error reporting generally. +
- +
-===== Section 6.3: Syntax Errors ===== +
- +
-We don't need to modify most of the error reporting code given in [[https://craftinginterpreters.com/parsing-expressions.html#syntax-errors|Section 6.3]]. +
-Here it is; add the ''consume()'' method after ''match()'' in the ''Parser'' class:+
  
 <code java> <code java>
-  private Token consume(TokenType type, String message) { +  private String stringify(Object object) { 
-    if (check(type)) return advance(); +    return object.toString();
- +
-    throw error(peek(), message);+
   }   }
 </code> </code>
  
-Then add the ''error()'' method after ''previous()'':+Add a ''runtimeError()'' method to your main ''TlaPlus'' class after ''error()'':
  
 <code java> <code java>
-  private ParseError error(Token token, String message) { +  static void runtimeError(RuntimeError error) { 
-    Lox.error(token, message); +    System.err.println(error.getMessage() + 
-    return new ParseError();+        "\n[line " + error.token.line + "]"); 
 +    hadRuntimeError = true;
   }   }
 </code> </code>
  
-In the ''TlaPlus'' class, add the ''error()'' method after ''report()'': +Then add a static ''hadRuntimeError'' field to the ''TlaPlus'' class:
- +
-<code java> +
-  static void error(Token token, String message) { +
-    if (token.type == TokenType.EOF) { +
-      report(token.line, " at end", message); +
-    } else { +
-      report(token.line, " at '" + token.lexeme + "'", message); +
-    } +
-  } +
-</code> +
- +
-Add the ''ParseError'' class definition at the top of the ''Parser'' class:+
  
 <code java [highlight_lines_extra="2"]> <code java [highlight_lines_extra="2"]>
-class Parser { +  static boolean hadError = false; 
-  private static class ParseError extends RuntimeException {}+  static boolean hadRuntimeError = false;
  
-  private final List<Token> tokens;+  public static void main(String[] args) throws IOException {
 </code> </code>
  
-One piece of code we //do// need to modify is the ''synchronization()'' method. +And exit from the ''runFile()'' method with a particular error code if a runtime error occurs:
-TLA⁺ doesn't have statements separated by semicolons, so our best choice of synchronization point is the ''EQUAL_EQUAL'' symbol denoting an operator definition; add this in the ''Parser'' class after ''error()'':+
  
-<code java> +<code java [highlight_lines_extra="5"]> 
-  private void synchronize() { +    run(new String(bytes, StandardCharsets.UTF_8));
-    advance();+
  
-    while(!isAtEnd()) { +    // Indicate an error in the exit code. 
-      if (previous().type == EQUAL_EQUAL) return; +    if (hadError) System.exit(65); 
- +    if (hadRuntimeError) System.exit(70);
-      advance(); +
-    }+
   }   }
 </code> </code>
  
-Fully-featured TLA⁺ parsers generally look ahead to identify the start of a new operator definition (not trivial!) and insert a synthetic zero-width token for the parser to consume. +Finally, create a static ''Interpreter'' instance at the top of the ''TlaPlus'' class:
-For an example, see SANY's very complicated ''[[https://github.com/tlaplus/tlaplus/blob/13e5a39b5368a6da4906b8ed1c2c1114d2e7de15/tlatools/org.lamport.tlatools/javacc/tla%2B.jj#L229-L392|belchDEF()]]'' method. +
-We won't be doing that here, but it's a good technique to know about; looking ahead then inserting synthetic tokens to disambiguate syntax is a common method when parsing complicated & ambiguous languages like TLA⁺.+
  
-===== Section 6.4: Wiring up the Parser =====+<code java [highlight_lines_extra="2"]> 
 +public class TlaPlus { 
 +  private static final Interpreter interpreter = new Interpreter(); 
 +  static boolean hadError = false; 
 +</code>
  
-In [[https://craftinginterpreters.com/parsing-expressions.html#wiring-up-the-parser|section 6.4]] we finally arrive at the point where you can parse TLA⁺ expressions in your REPL. +Then finish it off by actually interpreting the expression given by the user; add this in the ''run()'' method in the ''TlaPlus'' class:
-In the ''run()'' method of the ''TlaPlus'' class, delete the code printing out the scanned tokens (or not, it can be informative to keep around) and replace it with this: +
- +
-<code java [highlight_lines_extra="3,4,6,7,9"]> +
-    List<Token> tokens = scanner.scanTokens(); +
- +
-    Parser parser = new Parser(tokens); +
-    Expr expression = parser.parse();+
  
 +<code java [highlight_lines_extra="4"]>
     // Stop if there was a syntax error.     // Stop if there was a syntax error.
     if (hadError) return;     if (hadError) return;
  
-    System.out.println(new AstPrinter().print(expression));+    interpreter.interpret(expression);
   }   }
 </code> </code>
  
-Fire up the interpreter and parse a TLA⁺ expression!+Voila! 
 +Your program will now interpret any constant TLA⁺ expression you provide it! 
 +Try it out:
 <code> <code>
-> {1 + 2, IF TRUE THEN 3 ELSE 4, {}} +> {0 .. 2, IF TRUE THEN 1 ELSE 2, {}} 
-({ (+ 1 2) (IF true 3 4) ({))+[[], 1, [0, 1, 2]]
 </code> </code>
-If you got out of sync, you can find a snapshot of the expected state of the code in [[https://github.com/tlaplus-community/tlaplus-creator/tree/main/3-expressions|this repo directory]]. + 
-Next tutorial: [[https://docs.tlapl.us/creating:statements|Evaluating Constant TLA⁺ Expressions]]!+If you got out of sync, you can find a snapshot of the expected state of the code in [[https://github.com/tlaplus/devkit/tree/main/4-evaluation|this repo directory]]. 
 +Next tutorial: [[creating:statements|Handle TLA⁺ Statements]]!
  
 ====== Challenges ====== ====== Challenges ======
  
 Here are some optional challenges to flesh out your TLA⁺ interpreter, roughly ranked from simplest to most difficult. Here are some optional challenges to flesh out your TLA⁺ interpreter, roughly ranked from simplest to most difficult.
 +You should save a copy of your code before attempting these.
 +  - TLC evaluates cross-type equality comparison as a runtime error. For example, ''123 = TRUE'' evaluates to ''false'' in our interpreter but will throw an exception in TLC. Modify your interpreter to match the behavior of TLC.
 +  - TLC requires set elements to all be of the same type. Trying to construct the set ''{1, 2, TRUE}'' results in a TLC runtime error. Similarly, TLC only allows nested sets if //all// elements are similarly nested and of the same type: ''{1, {2}}'' is not allowed. Modify your interpreter to match the behavior of TLC. Use the TLC REPL to check which set constructions are allowed or disallowed. Checking whether an element of the wrong type is part of a set using the ''\in'' operator also should result in a runtime error.
  
-[[https://docs.tlapl.us/creating:scanning|< Previous Page]] | [[https://docs.tlapl.us/creating:evaluation|Next Page >]]+[[creating:expressions|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:statements|Next Page >]]
  
  • creating/evaluation.1744904072.txt.gz
  • Last modified: 2025/04/17 15:34
  • by ahelwer