Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
| creating:evaluation [2025/04/19 19:45] – Use internal wiki links ahelwer | creating: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 '' | + | Our first real difference |
| Recall that since our '' | Recall that since our '' | ||
| - | Here's how we define | + | We also don't pre-emptively evaluate |
| - | + | The method is structured as a switch statement handling all possible unary operators: | |
| - | <code java [highlight_lines_extra=" | + | <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; | + | |
| - | } | + | |
| - | | + | } case ENABLED: { |
| - | return null; | + | |
| + | } case NOT: { | ||
| + | |||
| + | } case MINUS: { | ||
| + | |||
| + | } default: { | ||
| + | | ||
| + | return null; | ||
| + | } | ||
| + | } | ||
| } | } | ||
| + | </ | ||
| + | |||
| + | Here's how we define the negative prefix operator; while the book casts the operand to a '' | ||
| + | <code java [highlight_lines_extra=" | ||
| + | } case MINUS: { | ||
| + | Object operand = evaluate(expr.expr); | ||
| + | return -(int)operand; | ||
| + | } default: { | ||
| </ | </ | ||
| Line 90: | Line 103: | ||
| Our logical-not prefix operator is denoted by the '' | Our logical-not prefix operator is denoted by the '' | ||
| - | We also have no use for the '' | + | We also have no use for the '' |
| - | Add this code to the '' | + | Add this code to '' |
| <code java [highlight_lines_extra=" | <code java [highlight_lines_extra=" | ||
| - | switch | + | } case NOT: { |
| - | case NOT: | + | Object operand = evaluate(expr.expr); |
| return !(boolean)operand; | return !(boolean)operand; | ||
| - | case MINUS: | + | |
| </ | </ | ||
| We still have two more unary operators to define: '' | We still have two more unary operators to define: '' | ||
| 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, | + | For constant expressions, |
| - | Add the highlighted code to the '' | + | Add the highlighted code to '' |
| - | + | <code java [highlight_lines_extra=" | |
| - | <code java [highlight_lines_extra=" | + | case PRIME: { |
| - | switch (expr.operator.type) { | + | return |
| - | case ENABLED: | + | |
| - | return (boolean)operand; | + | return |
| - | case NOT: | + | |
| - | </ | + | |
| - | + | ||
| - | Priming a constant expression has no effect on the value of that expression, so just return the operand' | + | |
| - | + | ||
| - | <code java [highlight_lines_extra=" | + | |
| - | switch (expr.operator.type) | + | |
| - | case PRIME: | + | |
| - | return | + | |
| - | case ENABLED: | + | |
| </ | </ | ||
| Line 124: | Line 127: | ||
| Unlike Lox, addition in TLA⁺ is only defined between two numbers (at least in its standard '' | Unlike Lox, addition in TLA⁺ is only defined between two numbers (at least in its standard '' | ||
| - | Here's how we define our basic binary arithmetic & comparison operators; add a '' | + | Here's how we define our basic binary arithmetic & comparison operators; add a '' |
| <code java [highlight_lines_extra=" | <code java [highlight_lines_extra=" | ||
| @Override | @Override | ||
| Line 193: | Line 195: | ||
| We use '' | We use '' | ||
| 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 '' | ||
| - | We actually want '' | ||
| - | Add the highlighted lines near the top of the '' | ||
| - | |||
| - | <code java [highlight_lines_extra=" | ||
| - | 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; | ||
| - | } | ||
| - | |||
| - | </ | ||
| - | |||
| - | In an odd contrast, our '' | ||
| - | We add it in with the rest of the operators in '' | ||
| - | |||
| - | <code java [highlight_lines_extra=" | ||
| - | Object right = evaluate(expr.right); | ||
| - | switch (expr.operator.type) { | ||
| - | case OR: | ||
| - | return (boolean)left || (boolean)right; | ||
| - | case DOT_DOT: | ||
| - | </ | ||
| - | |||
| - | 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 '' | ||
| - | People often write expressions like '' | ||
| - | It would be a runtime error to evaluate '' | ||
| - | 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:// | ||
| ==== Evaluating Other Operators ==== | ==== Evaluating Other Operators ==== | ||
| Line 265: | Line 228: | ||
| Set< | Set< | ||
| for (Expr parameter : expr.parameters) { | for (Expr parameter : expr.parameters) { | ||
| - | | + | |
| + | set.add(value); | ||
| } | } | ||
| return set; | return set; | ||
| Line 279: | Line 243: | ||
| In [[https:// | In [[https:// | ||
| - | Here's our variant of the '' | + | Here's our variant of the '' |
| <code java [highlight_lines_extra=" | <code java [highlight_lines_extra=" | ||
| Line 311: | Line 275: | ||
| </ | </ | ||
| - | We also need some helpers | + | We also need a helper |
| <code java> | <code java> | ||
| Line 317: | Line 281: | ||
| if (operand instanceof Boolean) return; | if (operand instanceof Boolean) return; | ||
| throw new RuntimeError(operator, | throw new RuntimeError(operator, | ||
| - | } | ||
| - | |||
| - | private void checkBooleanOperands(Token operator, Object left, Object right) { | ||
| - | if (left instanceof Boolean && right instanceof Boolean) return; | ||
| - | throw new RuntimeError(operator, | ||
| } | } | ||
| </ | </ | ||
| 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=" | + | <code java [highlight_lines_extra=" |
| - | case MINUS: | + | |
| + | Object operand = evaluate(expr.expr); | ||
| checkNumberOperand(expr.operator, | checkNumberOperand(expr.operator, | ||
| return -(int)operand; | return -(int)operand; | ||
| + | } default: { | ||
| </ | </ | ||
| Logical not: | Logical not: | ||
| - | <code java [highlight_lines_extra=" | + | <code java [highlight_lines_extra=" |
| - | case NOT: | + | |
| + | Object operand = evaluate(expr.expr); | ||
| checkBooleanOperand(expr.operator, | checkBooleanOperand(expr.operator, | ||
| return !(boolean)operand; | return !(boolean)operand; | ||
| - | </ | + | } case MINUS: { |
| - | Enabled: | + | |
| - | <code java [highlight_lines_extra=" | + | |
| - | | + | |
| - | checkBooleanOperand(expr.operator, | + | |
| - | return (boolean)operand; | + | |
| </ | </ | ||
| Subtraction: | Subtraction: | ||
| Line 382: | Line 339: | ||
| checkSetOperand(expr.operator, | checkSetOperand(expr.operator, | ||
| return ((Set<?> | return ((Set<?> | ||
| - | </ | ||
| - | Disjunction: | ||
| - | <code java [highlight_lines_extra=" | ||
| - | case OR: | ||
| - | checkBooleanOperands(expr.operator, | ||
| - | return (boolean)left || (boolean)right; | ||
| - | </ | ||
| - | Conjunction: | ||
| - | <code java [highlight_lines_extra=" | ||
| - | case AND: | ||
| - | checkBooleanOperand(expr.operator, | ||
| - | if (!(boolean)left) return false; | ||
| - | Object right = evaluate(expr.right); | ||
| - | checkBooleanOperand(expr.operator, | ||
| - | return (boolean)right; | ||
| </ | </ | ||
| Finally, '' | Finally, '' | ||
| Line 487: | Line 429: | ||
| </ | </ | ||
| - | If you got out of sync, you can find a snapshot of the expected state of the code in [[https:// | + | If you got out of sync, you can find a snapshot of the expected state of the code in [[https:// |
| Next tutorial: [[creating: | Next tutorial: [[creating: | ||