creating:operators

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:operators [2025/06/06 17:39] – Add variable shadowing error checking ahelwercreating:operators [2025/06/19 14:50] (current) – ALL_MAP_TO interpretation splits out Object value = ahelwer
Line 109: Line 109:
 import java.util.Map; import java.util.Map;
 import java.util.HashMap; import java.util.HashMap;
-import java.io.PrintStream; 
 </code> </code>
  
Line 242: Line 241:
 We've already implemented all our native TLA⁺ functions in the //[[creating:evaluation|Evaluating Constant TLA⁺ Expressions]]// chapter, but we will follow along to add a crucial field to the ''Interpreter'' class: a global environment. We've already implemented all our native TLA⁺ functions in the //[[creating:evaluation|Evaluating Constant TLA⁺ Expressions]]// chapter, but we will follow along to add a crucial field to the ''Interpreter'' class: a global environment.
 Due to the ''replMode'' parameter we have to put the initialization logic in the constructor (new code highlighted): Due to the ''replMode'' parameter we have to put the initialization logic in the constructor (new code highlighted):
-<code java [highlight_lines_extra="3,8,9"]>+<code java [highlight_lines_extra="3,7,8"]>
 class Interpreter implements Expr.Visitor<Object>, class Interpreter implements Expr.Visitor<Object>,
                              Stmt.Visitor<Void> {                              Stmt.Visitor<Void> {
   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; 
   }   }
 </code> </code>
Line 300: Line 297:
 <code java [highlight_lines_extra="3"]> <code java [highlight_lines_extra="3"]>
     defineAst(outputDir, "Stmt", Arrays.asList(     defineAst(outputDir, "Stmt", Arrays.asList(
-      "Print    : Expr expression",+      "Print    : Token location, Expr expression",
       "OpDef    : Token name, List<Token> params, Expr body"       "OpDef    : Token name, List<Token> params, Expr body"
     ));     ));
Line 307: Line 304:
 We can now parse operators with parameters! We can now parse operators with parameters!
 On to functions. On to functions.
-This requires defining a new expression type in the ''GenerateAST'' class:+This requires defining a new expression type in the ''GenerateAst'' class:
 <code java [highlight_lines_extra="3"]> <code java [highlight_lines_extra="3"]>
     defineAst(outputDir, "Expr", Arrays.asList(     defineAst(outputDir, "Expr", Arrays.asList(
Line 444: Line 441:
  
 Additional TLA⁺-specific validation is necessary here. Additional TLA⁺-specific validation is necessary here.
-TLA⁺ does not allow shadowing existing identifiers with operator parameter names.+While we allow redefining operators //themselves// in REPL mode, TLA⁺ does not allow shadowing existing operator names with operator parameter names.
 So, if an operator of name ''x'' exists, and the user tries to define a new operator ''op(x) == ...'', we should raise a runtime error. So, if an operator of name ''x'' exists, and the user tries to define a new operator ''op(x) == ...'', we should raise a runtime error.
 We should also disallow operator definitions with duplicate parameter names like ''op(x, x) == ...''. We should also disallow operator definitions with duplicate parameter names like ''op(x, x) == ...''.
Line 452: Line 449:
     for (Token name : names) {     for (Token name : names) {
       if (environment.isDefined(name)) {       if (environment.isDefined(name)) {
-        throw new RuntimeError(name, "Identifier is already in use.");+        throw new RuntimeError(name, "Identifier already in use.");
       }       }
     }     }
Line 459: Line 456:
       for (int j = i + 1; j < names.size(); j++) {       for (int j = i + 1; j < names.size(); j++) {
         if (names.get(i).lexeme.equals(names.get(j).lexeme)) {         if (names.get(i).lexeme.equals(names.get(j).lexeme)) {
-          throw new RuntimeError(names.get(i), "Identifier is used twice in same list.");+          throw new RuntimeError(names.get(i), "Identifier used twice in same list.");
         }         }
       }       }
Line 474: Line 471:
 </code> </code>
  
-Add a call to ''checkNotDefined()'' to ''visitOpDefStmt()'', along with another check that the user is not trying to define an operator like ''x(x) == ...'':+Add a ''checkNotDefined()'' call to ''visitOpDefStmt()'', along with another check that the user is not trying to define an operator like ''x(x) == ...'':
 <code java [highlight_lines_extra="2,3,4,5,6,7"]> <code java [highlight_lines_extra="2,3,4,5,6,7"]>
   public Void visitOpDefStmt(Stmt.OpDef stmt) {   public Void visitOpDefStmt(Stmt.OpDef stmt) {
Line 480: Line 477:
     for (Token param : stmt.params) {     for (Token param : stmt.params) {
       if (param.lexeme.equals(stmt.name.lexeme)) {       if (param.lexeme.equals(stmt.name.lexeme)) {
-        throw new RuntimeError(param, "Identifier is already in use.");+        throw new RuntimeError(param, "Identifier already in use.");
       }       }
     }     }
Line 572: Line 569:
 One important thing to note is that unlike in ''TlaOperator'', we give ''BindingGenerator'' the //current// environment instead of the root global environment; this is because if we are evaluating an ''Expr.QuantFn'' instance inside an operator, the body expression should be able to access definitions from the operator's environment, like: One important thing to note is that unlike in ''TlaOperator'', we give ''BindingGenerator'' the //current// environment instead of the root global environment; this is because if we are evaluating an ''Expr.QuantFn'' instance inside an operator, the body expression should be able to access definitions from the operator's environment, like:
 <code haskell> <code haskell>
-op(x) == \A y \in 0 .. 2 : y < x +op(x) == \A y \in 0 .. 2 : y < x
 </code> </code>
 Here's how we implement the ''EXISTS'' case; unlike universal quantification, existential quantification is not short-circuiting in TLA⁺ (for reasons that will become clear in the next chapter): Here's how we implement the ''EXISTS'' case; unlike universal quantification, existential quantification is not short-circuiting in TLA⁺ (for reasons that will become clear in the next chapter):
Line 587: Line 584:
 </code> </code>
 Finally, here's how we implement the ''ALL_MAP_TO'' case; we want to construct a ''Map<Object, Object>'' instance recording each value the single parameter is mapped to: Finally, here's how we implement the ''ALL_MAP_TO'' case; we want to construct a ''Map<Object, Object>'' instance recording each value the single parameter is mapped to:
-<code java [highlight_lines_extra="2,3,4,5,6,7"]>+<code java [highlight_lines_extra="2,3,4,5,6,7,8"]>
       case ALL_MAP_TO: {       case ALL_MAP_TO: {
         Token param = expr.params.get(0);         Token param = expr.params.get(0);
         Map<Object, Object> function = new HashMap<>();         Map<Object, Object> function = new HashMap<>();
         for (Environment binding : bindings) {         for (Environment binding : bindings) {
-          function.put(binding.get(param), executeBlock(expr.body, binding));+          Object value = executeBlock(expr.body, binding); 
 +          function.put(binding.get(param), value);
         }         }
         return function;         return function;
  • creating/operators.1749231573.txt.gz
  • Last modified: 2025/06/06 17:39
  • by ahelwer