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:27] – Added link to table of contents 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: [[https:// | + | Next tutorial: [[creating: |
====== Challenges ====== | ====== Challenges ====== | ||
Line 497: | Line 439: | ||
- TLC requires set elements to all be of the same type. Trying to construct the set '' | - TLC requires set elements to all be of the same type. Trying to construct the set '' | ||
- | [[https:// | + | [[creating: |