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/05/21 19:38] – Improved change-of-base explanation ahelwercreating:operators [2025/06/13 21:25] (current) – Removed PrintStream parameter from Interpreter constructor ahelwer
Line 1: Line 1:
-======= Operators & Parameters =======+======= Functions, Operators, and Parameters =======
  
 We now rejoin //Crafting Interpreters// for [[https://craftinginterpreters.com/functions.html|Chapter 10]]. We now rejoin //Crafting Interpreters// for [[https://craftinginterpreters.com/functions.html|Chapter 10]].
Line 101: Line 101:
  
 In [[https://craftinginterpreters.com/functions.html#interpreting-function-calls|this section]] we learn how to interpret our shiny new call syntax. In [[https://craftinginterpreters.com/functions.html#interpreting-function-calls|this section]] we learn how to interpret our shiny new call syntax.
 +First, add some imports to the top of ''Interpreter.java'':
 +<code java [highlight_lines_extra="3,5,6"]>
 +import java.util.Set;
 +import java.util.HashSet;
 +import java.util.ArrayList;
 +import java.util.List;
 +import java.util.Map;
 +import java.util.HashMap;
 +</code>
  
-First let's implement the ''Interpreter'' class visitor method for ''Expr.FnApply'':+Implement the ''Interpreter'' class visitor method for ''Expr.FnApply'':
 <code java> <code java>
   @Override   @Override
Line 232: 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 431: Line 438:
     return null;     return null;
   }   }
 +</code>
 +
 +Additional TLA⁺-specific validation is necessary here.
 +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.
 +We should also disallow operator definitions with duplicate parameter names like ''op(x, x) == ...''.
 +Define a new helper for this near the bottom of the ''Interpreter'' class:
 +<code java>
 +  private void checkNotDefined(List<Token> names) {
 +    for (Token name : names) {
 +      if (environment.isDefined(name)) {
 +        throw new RuntimeError(name, "Identifier already in use.");
 +      }
 +    }
 +
 +    for (int i = 0; i < names.size() - 1; i++) {
 +      for (int j = i + 1; j < names.size(); j++) {
 +        if (names.get(i).lexeme.equals(names.get(j).lexeme)) {
 +          throw new RuntimeError(names.get(i), "Identifier used twice in same list.");
 +        }
 +      }
 +    }
 +  }
 +</code>
 +
 +This helper requires a new method in the ''Environment'' class:
 +<code java>
 +  boolean isDefined(Token name) {
 +    return values.containsKey(name.lexeme)
 +        || (enclosing != null && enclosing.isDefined(name));
 +  }
 +</code>
 +
 +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"]>
 +  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, "Identifier already in use.");
 +      }
 +    }
 +
 +    TlaOperator op = new TlaOperator(stmt);
 </code> </code>
  
 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 ''visitQuantFnExpr()'' method in the ''Interpreter''; similar to other operator evaluation methods like ''visitBinaryExpr()'' we evaluate what we can (here, the set to be quantified over) then branch on the operator type:+We still need to implement our ''visitQuantFnExpr()'' method in the ''Interpreter'' class. 
 +Similar to other operator evaluation methods like ''visitBinaryExpr()'' we evaluate what we can (here, the set to be quantified over) then branch on the operator type. 
 +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, set);     checkSetOperand(expr.op, set);
Line 524: Line 578:
           Object junctResult = executeBlock(expr.body, binding);           Object junctResult = executeBlock(expr.body, binding);
           checkBooleanOperand(expr.op, junctResult);           checkBooleanOperand(expr.op, junctResult);
-          result |= (Boolean)junctResult;+          result |= (boolean)junctResult;
         }         }
         return result;         return result;
Line 638: Line 692:
 You can now run your interpreter and enjoy the full power of functions & operators with parameters, along with the new universal & existential quantification expressions! You can now run your interpreter and enjoy the full power of functions & operators with parameters, along with the new universal & existential quantification expressions!
 See the current expected state of your source code [[https://github.com/tlaplus/devkit/tree/main/7-operators|here]]. See the current expected state of your source code [[https://github.com/tlaplus/devkit/tree/main/7-operators|here]].
-On to the next chapter: [[creating:actions|Variables & Actions]]!+On to the next chapter: [[creating:actions|Variables, States, and Actions]]!
  
 ====== Challenges ====== ====== Challenges ======
  • creating/operators.1747856322.txt.gz
  • Last modified: 2025/05/21 19:38
  • by ahelwer