Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
creating:operators [2025/05/21 19:45] – Slightly changed title ahelwer | creating:operators [2025/06/13 21:25] (current) – Removed PrintStream parameter from Interpreter constructor ahelwer | ||
---|---|---|---|
Line 101: | Line 101: | ||
In [[https:// | In [[https:// | ||
+ | First, add some imports to the top of '' | ||
+ | <code java [highlight_lines_extra=" | ||
+ | import java.util.Set; | ||
+ | import java.util.HashSet; | ||
+ | import java.util.ArrayList; | ||
+ | import java.util.List; | ||
+ | import java.util.Map; | ||
+ | import java.util.HashMap; | ||
+ | </ | ||
- | First let's implement | + | Implement |
<code java> | <code java> | ||
@Override | @Override | ||
Line 232: | Line 241: | ||
We've already implemented all our native TLA⁺ functions in the // | We've already implemented all our native TLA⁺ functions in the // | ||
Due to the '' | Due to the '' | ||
- | <code java [highlight_lines_extra=" | + | <code java [highlight_lines_extra=" |
class Interpreter implements Expr.Visitor< | class Interpreter implements Expr.Visitor< | ||
| | ||
final Environment globals; | final Environment globals; | ||
private Environment environment; | private Environment environment; | ||
- | private final PrintStream out; | ||
- | public Interpreter(PrintStream out, boolean replMode) { | + | public Interpreter(boolean replMode) { |
this.globals = new Environment(replMode); | this.globals = new Environment(replMode); | ||
this.environment = this.globals; | this.environment = this.globals; | ||
- | this.out = out; | ||
} | } | ||
</ | </ | ||
Line 431: | Line 438: | ||
return null; | return null; | ||
} | } | ||
+ | </ | ||
+ | |||
+ | Additional TLA⁺-specific validation is necessary here. | ||
+ | While we allow redefining operators // | ||
+ | So, if an operator of name '' | ||
+ | We should also disallow operator definitions with duplicate parameter names like '' | ||
+ | Define a new helper for this near the bottom of the '' | ||
+ | <code java> | ||
+ | private void checkNotDefined(List< | ||
+ | for (Token name : names) { | ||
+ | if (environment.isDefined(name)) { | ||
+ | throw new RuntimeError(name, | ||
+ | } | ||
+ | } | ||
+ | |||
+ | for (int i = 0; i < names.size() - 1; i++) { | ||
+ | for (int j = i + 1; j < names.size(); | ||
+ | if (names.get(i).lexeme.equals(names.get(j).lexeme)) { | ||
+ | throw new RuntimeError(names.get(i), | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | </ | ||
+ | |||
+ | This helper requires a new method in the '' | ||
+ | <code java> | ||
+ | boolean isDefined(Token name) { | ||
+ | return values.containsKey(name.lexeme) | ||
+ | || (enclosing != null && enclosing.isDefined(name)); | ||
+ | } | ||
+ | </ | ||
+ | |||
+ | Add a '' | ||
+ | <code java [highlight_lines_extra=" | ||
+ | public Void visitOpDefStmt(Stmt.OpDef stmt) { | ||
+ | checkNotDefined(stmt.params); | ||
+ | for (Token param : stmt.params) { | ||
+ | if (param.lexeme.equals(stmt.name.lexeme)) { | ||
+ | throw new RuntimeError(param, | ||
+ | } | ||
+ | } | ||
+ | |||
+ | TlaOperator op = new TlaOperator(stmt); | ||
</ | </ | ||
And that takes care of operators! | And that takes care of operators! | ||
Now to handle functions. | Now to handle functions. | ||
- | We still need to implement our '' | + | We still need to implement our '' |
+ | Similar | ||
+ | We also ensure the function parameter names are not shadowing an existing identifier: | ||
<code java> | <code java> | ||
@Override | @Override | ||
public Object visitQuantFnExpr(Expr.QuantFn expr) { | public Object visitQuantFnExpr(Expr.QuantFn expr) { | ||
+ | checkNotDefined(expr.params); | ||
Object set = evaluate(expr.set); | Object set = evaluate(expr.set); | ||
checkSetOperand(expr.op, | checkSetOperand(expr.op, | ||
Line 524: | Line 578: | ||
Object junctResult = executeBlock(expr.body, | Object junctResult = executeBlock(expr.body, | ||
checkBooleanOperand(expr.op, | checkBooleanOperand(expr.op, | ||
- | result |= (Boolean)junctResult; | + | result |= (boolean)junctResult; |
} | } | ||
return result; | return result; |