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/19 19:27] – Added link to table of contents ahelwercreating:evaluation [2025/06/19 16:31] (current) – LEFT_BRACE interpretation splits out Object value = ahelwer
Line 65: Line 65:
 ==== Evaluating Unary Operators ==== ==== Evaluating Unary Operators ====
  
-Our first real difference is in the ''visitUnaryExpr()'' method.+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. Recall that since our ''Expr.Unary'' type represents both prefix and suffix operators, we don't call its parameter ''right'' as in the book.
-Here's how we define the negative prefix operator, casting the parameter to an ''int'' instead of a ''double'' (highlighted lines differ from 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 switch statement handling all possible unary operators
-<code java [highlight_lines_extra="3,7"]>+<code java>
   @Override   @Override
   public Object visitUnaryExpr(Expr.Unary expr) {   public Object visitUnaryExpr(Expr.Unary expr) {
-    Object operand = evaluate(expr.expr); 
- 
     switch (expr.operator.type) {     switch (expr.operator.type) {
-      case MINUS: +      case PRIME{
-        return -(int)operand; +
-    }+
  
-    // Unreachable. +      } case ENABLED: { 
-    return null;+ 
 +      } case NOT: { 
 + 
 +      } case MINUS: { 
 + 
 +      } default: { 
 +        // Unreachable. 
 +        return null; 
 +      } 
 +    }
   }   }
 +</code>
 +
 +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="2,3"]>
 +      } case MINUS: {
 +        Object operand = evaluate(expr.expr);
 +        return -(int)operand;
 +      } default: {
 </code> </code>
  
Line 90: Line 103:
  
 Our logical-not prefix operator is denoted by the ''NOT'' token type instead of ''BANG'' as in Lox. 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, since TLA⁺ is quite strict: only Boolean values can be given to Boolean operators! +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 the ''visitUnaryExpr()'' method: +Add this code to ''visitUnaryExpr()'':
 <code java [highlight_lines_extra="2,3"]> <code java [highlight_lines_extra="2,3"]>
-    switch (expr.operator.type+      } case NOT: { 
-      case NOT:+        Object operand = evaluate(expr.expr);
         return !(boolean)operand;         return !(boolean)operand;
-      case MINUS:+      case MINUS: {
 </code> </code>
  
 We still have two more unary operators to define: ''ENABLED'', and the prime operator. 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. Both are trivial in this domain but will become much more complicated later on.
-For constant expressions, ''ENABLED'' is true if and only if the expression itself is true+For constant expressions, ''ENABLED'' is always false and prime is just whatever the inner expression evaluates to
-Add the highlighted code to the ''visitUnaryExpr()'' method: +Add the highlighted code to ''visitUnaryExpr()'': 
- +<code java [highlight_lines_extra="2,4"]> 
-<code java [highlight_lines_extra="2,3"]> +      case PRIME{ 
-    switch (expr.operator.type) { +        return evaluate(expr.expr); 
-      case ENABLED+      case ENABLED: { 
-        return (boolean)operand+        return false
-      case NOT: +      case NOT{
-</code> +
- +
-Priming a constant expression has no effect on the value of that expression, so just return the operand's value: +
- +
-<code java [highlight_lines_extra="2,3"]> +
-    switch (expr.operator.type) { +
-      case PRIME: +
-        return operand+
-      case ENABLED:+
 </code> </code>
  
Line 124: Line 127:
  
 Unlike Lox, addition in TLA⁺ is only defined between two numbers (at least in its standard ''Integers'' module definition). 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: +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"]> <code java [highlight_lines_extra="8,9,10,11,12,13,14"]>
   @Override   @Override
Line 193: Line 195:
 We use ''Set<Object>'', so our sets can hold any value you can imagine including nested sets. 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! 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!
- 
-The only binary operators remaining are logical ''AND'' & ''OR'', and they differ in a subtle but important way. 
-We actually want ''AND'' to implement //short-circuit evaluation//, so an expression like ''FALSE /\ TRUE'' evaluates to ''false'' without even looking at the right hand operand. 
-Add the highlighted lines near the top of the ''visitBinaryExpr()'' method: 
- 
-<code java [highlight_lines_extra="3,4,5,6,7,8,9,10"]> 
-  public Object visitBinaryExpr(Expr.Binary expr) { 
-    Object left = evaluate(expr.left); 
-    switch (expr.operator.type) { 
-      case AND: 
-        if (!(boolean)left) return false; 
-        Object right = evaluate(expr.right); 
-        return (boolean)right; 
-      default: 
-        break; 
-    } 
- 
-</code> 
- 
-In an odd contrast, our ''OR'' binary operator is //not// short-circuited. 
-We add it in with the rest of the operators in ''visitBinaryExpr()'': 
- 
-<code java [highlight_lines_extra="3,4"]> 
-    Object right = evaluate(expr.right); 
-    switch (expr.operator.type) { 
-      case OR: 
-        return (boolean)left || (boolean)right; 
-      case DOT_DOT: 
-</code> 
- 
-Why are these different? 
-It has to do with how they are used in TLA⁺ formulas. 
-Actions are usually defined as a conjunction of expressions serving as guards, where later expressions could result in a runtime error if evaluated in some cases. 
-For example, consider a variable ''x'' that can either be a sentinel value ''None'' or a set. 
-People often write expressions like ''x /= None /\ 1 \in x''. 
-It would be a runtime error to evaluate ''1 \in x'' if ''x = None''. 
-It is thus useful to use conjunction as a guard stopping expression interpretation if the first operand is not true. 
-In contrast, disjunction is used in TLA⁺ to express nondeterminism and so both branches of the disjunct need to be evaluated to see whether their expressions satisfy alternative next states. 
-You can read [[https://groups.google.com/g/tlaplus/c/U6tOJ4dsjVM/m/1zXWHrZbBwAJ|this]] thread on the TLA⁺ mailing list for more information. 
  
 ==== Evaluating Other Operators ==== ==== Evaluating Other Operators ====
Line 265: Line 228:
         Set<Object> set = new HashSet<Object>();         Set<Object> set = new HashSet<Object>();
         for (Expr parameter : expr.parameters) {         for (Expr parameter : expr.parameters) {
-          set.add(evaluate(parameter));+          Object value = evaluate(parameter)
 +          set.add(value);
         }         }
         return set;         return set;
Line 279: Line 243:
 In [[https://craftinginterpreters.com/evaluating-expressions.html#runtime-errors|section 7.3]] we add some error detection & reporting to our interpreter code. In [[https://craftinginterpreters.com/evaluating-expressions.html#runtime-errors|section 7.3]] we add some error detection & reporting to our interpreter code.
  
-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:+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):
  
 <code java [highlight_lines_extra="2,8"]> <code java [highlight_lines_extra="2,8"]>
Line 311: Line 275:
 </code> </code>
  
-We also need some helpers for boolean operator parameters since TLA⁺ is more strict about that; add these to the ''Interpreter'' class:+We also need a helper for booleans since TLA⁺ is more strict about them than Lox; add this to the ''Interpreter'' class:
  
 <code java> <code java>
Line 317: Line 281:
     if (operand instanceof Boolean) return;     if (operand instanceof Boolean) return;
     throw new RuntimeError(operator, "Operand must be a boolean.");     throw new RuntimeError(operator, "Operand must be a boolean.");
-  } 
- 
-  private void checkBooleanOperands(Token operator, Object left, Object right) { 
-    if (left instanceof Boolean && right instanceof Boolean) return; 
-    throw new RuntimeError(operator, "Operands must be booleans."); 
   }   }
 </code> </code>
Line 336: Line 295:
 Now add these checks to our interpreter code. Now add these checks to our interpreter code.
 Here's negative: Here's negative:
-<code java [highlight_lines_extra="2"]> +<code java [highlight_lines_extra="3"]> 
-      case MINUS:+      case MINUS: 
 +        Object operand = evaluate(expr.expr);
         checkNumberOperand(expr.operator, operand);         checkNumberOperand(expr.operator, operand);
         return -(int)operand;         return -(int)operand;
 +      } default: {
 </code> </code>
 Logical not: Logical not:
-<code java [highlight_lines_extra="2"]> +<code java [highlight_lines_extra="3"]> 
-      case NOT:+      case NOT: 
 +        Object operand = evaluate(expr.expr);
         checkBooleanOperand(expr.operator, operand);         checkBooleanOperand(expr.operator, operand);
         return !(boolean)operand;         return !(boolean)operand;
-</code> +      } case MINUS{
-Enabled: +
-<code java [highlight_lines_extra="2"]> +
-      case ENABLED: +
-        checkBooleanOperand(expr.operator, operand); +
-        return (boolean)operand;+
 </code> </code>
 Subtraction: Subtraction:
Line 382: Line 339:
         checkSetOperand(expr.operator, right);         checkSetOperand(expr.operator, right);
         return ((Set<?>)right).contains(left);         return ((Set<?>)right).contains(left);
-</code> 
-Disjunction: 
-<code java [highlight_lines_extra="2"]> 
-      case OR: 
-        checkBooleanOperands(expr.operator, left, right); 
-        return (boolean)left || (boolean)right; 
-</code> 
-Conjunction: 
-<code java [highlight_lines_extra="2,5"]> 
-      case AND: 
-        checkBooleanOperand(expr.operator, left); 
-        if (!(boolean)left) return false; 
-        Object right = evaluate(expr.right); 
-        checkBooleanOperand(expr.operator, right); 
-        return (boolean)right; 
 </code> </code>
 Finally, ''IF''/''THEN''/''ELSE'': Finally, ''IF''/''THEN''/''ELSE'':
Line 487: Line 429:
 </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/4-evaluation|this repo directory]]. +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: [[https://docs.tlapl.us/creating:statements|Handle TLA⁺ Statements]]!+Next tutorial: [[creating:statements|Handle TLA⁺ Statements]]!
  
 ====== Challenges ====== ====== Challenges ======
Line 497: Line 439:
   - 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.   - 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:expressions|< Previous Page]] | [[https://docs.tlapl.us/creating:start#table_of_contents|Table of Contents]] | [[https://docs.tlapl.us/creating:statements|Next Page >]]+[[creating:expressions|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:statements|Next Page >]]
  
  • creating/evaluation.1745090856.txt.gz
  • Last modified: 2025/04/19 19:27
  • by ahelwer