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/14 21:41] – function & operator call syntax parsing 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 15: Line 15:
 Functions have not yet been defined in any form, but will be later in this tutorial. Functions have not yet been defined in any form, but will be later in this tutorial.
  
-====== Section 10.1: Operator Calls ======+====== Section 10.1: Function Calls ======
  
 [[https://craftinginterpreters.com/functions.html#function-calls|Section 10.1]] takes us through adding calling syntax to the parser. [[https://craftinginterpreters.com/functions.html#function-calls|Section 10.1]] takes us through adding calling syntax to the parser.
Line 97: Line 97:
  
 This ''do''/''while'' loop is very similar to our existing set literal parsing code for handling comma-separated expressions, so it should be familiar to you. This ''do''/''while'' loop is very similar to our existing set literal parsing code for handling comma-separated expressions, so it should be familiar to you.
 +
 +===== Subsection 10.1.2: Interpreting function calls =====
 +
 +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>
 +
 +Implement the ''Interpreter'' class visitor method for ''Expr.FnApply'':
 +<code java>
 +  @Override
 +  public Object visitFnApplyExpr(Expr.FnApply expr) {
 +    Object callee = evaluate(expr.fn);
 +    Object argument = evaluate(expr.argument);
 +    Map<?, ?> function = (Map<?, ?>)callee;
 +
 +    return function.get(argument);
 +  }
 +</code>
 +
 +Now we can apply functions, although we can't yet define them.
 +Next up is operators.
 +Here we completely rewrite our ''visitVariableExpr()'' method in the ''Interpreter'' class to resemble the ''visitCallExpr()'' method from the book:
 +<code java>
 +  @Override
 +  public Object visitVariableExpr(Expr.Variable expr) {
 +    Object callee = environment.get(expr.name);
 +
 +    List<Object> arguments = new ArrayList<>();
 +    for (Expr argument : expr.arguments) {
 +      arguments.add(evaluate(argument));
 +    }
 +
 +    TlaCallable operator = (TlaCallable)callee;
 +    return operator.call(this, arguments);
 +  }
 +</code>
 +
 +We write our own version of the ''LoxCallable'' interface from the book, which we'll call ''TlaCallable'':
 +<code java>
 +package tla;
 +
 +import java.util.List;
 +
 +interface TlaCallable {
 +  Object call(Interpreter interpreter, List<Object> arguments);
 +}
 +</code>
 +We can now call operators, although cannot yet define operators to call!
 +
 +===== Subsection 10.1.3: Call type errors =====
 +
 +In ''visitFnApply()'', we should validate that our ''callee'' is actually a function:
 +<code java [highlight_lines_extra="4"]>
 +  @Override
 +  public Object visitFnApplyExpr(Expr.FnApply expr) {
 +    Object callee = evaluate(expr.fn);
 +    checkFunctionOperand(expr.bracket, callee);
 +    Object argument = evaluate(expr.argument);
 +    Map<?, ?> function = (Map<?, ?>)callee;
 +</code>
 +This requires another validation helper, ''checkFunctionOperand()''.
 +Put it down with the rest of the validation helpers:
 +<code java>
 +  private void checkFunctionOperand(Token operator, Object operand) {
 +    if (operand instanceof Map<?,?>) return;
 +    throw new RuntimeError(operator, "Operand must be a function.");
 +  }
 +</code>
 +
 +We should also check that the function is actually defined on the given argument, and provide a useful error message if not:
 +<code java [highlight_lines_extra="3,4,5,6,7"]>
 +    Object argument = evaluate(expr.argument);
 +    Map<?, ?> function = (Map<?, ?>)callee;
 +    if (!function.containsKey(argument)) {
 +      throw new RuntimeError(expr.bracket,
 +          "Cannot apply function to element outside domain: "
 +          + argument.toString());
 +    }
 +
 +    return function.get(argument);
 +  }
 +</code>
 +
 +In ''visitVariableExpr()'', similar to the book we need to check whether ''callee'' is an instance of ''TlaCallable''.
 +However, unlike the book this is not an error!
 +It is simply an identifier bound to a concrete value in the current ''environment'', and we should immediately return that value:
 +<code java [highlight_lines_extra="5,6,7"]>
 +  @Override
 +  public Object visitVariableExpr(Expr.Variable expr) {
 +    Object callee = environment.get(expr.name);
 +
 +    if (!(callee instanceof TlaCallable)) {
 +      return callee;
 +    }
 +
 +    List<Object> arguments = new ArrayList<>();
 +</code>
 +This duality of identifiers either being operators to be evaluated or already-bound values is a bit confusing at times, but we can handle it.
 +If the user tries to provide arguments to one of these concrete values then we should raise an error:
 +<code java [highlight_lines_extra="2,3,4,5"]>
 +    if (!(callee instanceof TlaCallable)) {
 +      if (!expr.arguments.isEmpty()) {
 +        throw new RuntimeError(expr.name,
 +            "Cannot give arguments to non-operator identifier.");
 +      }
 +
 +      return callee;
 +    }
 +</code>
 +
 +===== Subsection 10.1.4: Checking arity =====
 +
 +If ''callee'' //is// an operator, we need to [[https://craftinginterpreters.com/functions.html#checking-arity|check arity]] - that the number of arguments provided is as expected:
 +<code java [highlight_lines_extra="2,3,4,5,6"]>
 +    TlaCallable operator = (TlaCallable)callee;
 +    if (arguments.size() != operator.arity()) {
 +      throw new RuntimeError(expr.name, "Expected " +
 +          operator.arity() + " arguments but got " +
 +          arguments.size() + ".");
 +    }
 +
 +    return operator.call(this, arguments);
 +</code>
 +Which requires adding a new method to the ''TlaCallable'' interface:
 +<code java [highlight_lines_extra="2"]>
 +interface TlaCallable {
 +  int arity();
 +  Object call(Interpreter interpreter, List<Object> arguments);
 +</code>
 +
 +For functions, we don't need to check arity because the single-argument restriction is enforced at the parser level.
 +
 +====== Section 10.2: Native Functions ======
 +
 +In [[https://craftinginterpreters.com/functions.html#native-functions|Section 10.2]] we learn how to implement primitive/native functions.
 +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):
 +<code java [highlight_lines_extra="3,7,8"]>
 +class Interpreter implements Expr.Visitor<Object>,
 +                             Stmt.Visitor<Void> {
 +  final Environment globals;
 +  private Environment environment;
 +
 +  public Interpreter(boolean replMode) {
 +    this.globals = new Environment(replMode);
 +    this.environment = this.globals;
 +  }
 +</code>
 +
 +Note that the ''globals'' field has package visibility, not class visibility.
 +The use of this field will become clear when implementing the ''TlaCallable.call()'' interface method.
 +
 +====== Section 10.3: Function Declarations ======
 +
 +We can call functions & operators, now let's [[https://craftinginterpreters.com/functions.html#function-declarations|define them]]!
 +Operators take less work so they come first.
 +In the ''Parser'' class, we have our existing ''isAtOpDefStart()'' and ''operatorDefinition()'' methods which we will now extend to accept parameters.
 +We want to parse operator definitions like ''op(x, y, z) == expr'' and also ''op == expr''.
 +''op() == expr'' is invalid syntax in TLA⁺.
 +We will use the now-familiar ''do''/''while'' method of consuming one or more comma-separated values.
 +Recall that ''isAtOpDefStart()'' is a lookahead method to determine whether the upcoming token sequence is an operator definition, while ''operatorDefinition()'' actually parses that same token sequence into an AST node.
 +<code java [highlight_lines_extra="3,4,5,6,7,8"]>
 +  private boolean isAtOpDefStart() {
 +    if (!match(IDENTIFIER)) return false;
 +    if (match(LEFT_PAREN)) {
 +      do {
 +        if (!match(IDENTIFIER)) return false;
 +      } while (match(COMMA));
 +      if (!match(RIGHT_PAREN)) return false;
 +    }
 +
 +    return match(EQUAL_EQUAL);
 +  }
 +</code>
 +<code java [highlight_lines_extra="3,4,5,6,7,8,9,12"]>
 +  private Stmt operatorDefinition() {
 +    Token name = consume(IDENTIFIER, "Name required for operator definition.");
 +    List<Token> params = new ArrayList<>();
 +    if (match(LEFT_PAREN)) {
 +      do {
 +        params.add(consume(IDENTIFIER, "Identifier required as operator parameter."));
 +      } while (match(COMMA));
 +      consume(RIGHT_PAREN, "')' required to terminate operator parameters.");
 +    }
 +
 +    consume(EQUAL_EQUAL, "'==' required for operator definition.");
 +    return new Stmt.OpDef(name, params, expression());
 +  }
 +</code>
 +
 +Our changes to ''operatorDefinition()'' require modifying the definition of ''Stmt.OpDef'' in the ''GenerateAst'' class to accept parameters:
 +<code java [highlight_lines_extra="3"]>
 +    defineAst(outputDir, "Stmt", Arrays.asList(
 +      "Print    : Expr expression",
 +      "OpDef    : Token name, List<Token> params, Expr body"
 +    ));
 +</code>
 +
 +We can now parse operators with parameters!
 +On to functions.
 +This requires defining a new expression type in the ''GenerateAST'' class:
 +<code java [highlight_lines_extra="3"]>
 +    defineAst(outputDir, "Expr", Arrays.asList(
 +      "Binary   : Expr left, Token operator, Expr right",
 +      "QuantFn  : Token op, List<Token> params, Expr set, Expr body",
 +      "FnApply  : Expr fn, Token bracket, Expr argument",
 +</code>
 +
 +This looks a bit abstract.
 +What does ''QuantFn'' mean?
 +And why do we allow multiple parameters when our functions only take one?
 +This is because we'll be bundling multiple closely-related language constructs into this single AST node type: function constructors, universal quantifiers, and existential quantifiers.
 +
 +In TLA⁺, functions are constructed with the ''|->'' operator.
 +So you can write ''[x \in 0 .. 2 |-> x + 1]'' to define a function mapping the values 0, 1, and 2 to 1, 2, and 3 respectively.
 +TLA⁺ also has very useful universal & existential quantification syntax.
 +You can write ''\A x \in 0 .. 2 : x < 3'' to assert that all elements of the set ''{0, 1, 2}'' are less than three, or ''\E x, y  \in 0 .. 2 : x + y = 4'' to assert that there are two elements of the set ''{0, 1, 2}'' that together sum to four.
 +We can see the commonality between these; they all have:
 +  - A token identifying the operator (''|->'', ''\A'', or ''\E'')
 +  - A set to draw elements from (''0 .. 2'')
 +  - Some number of identifiers to which to bind values from the set (''x'', ''y'')
 +  - An expression body in which the identifiers can be used
 +So we can contain all of them in the ''QuantFn'' expression node, which means something like "quantifier function".
 +
 +Here's how we parse the function constructor syntax.
 +Add this to the ''primary()'' method in the ''Parser'' class, below the finite set literal code:
 +<code java>
 +    if (match(LEFT_BRACKET)) {
 +      List<Token> params = new ArrayList<>();
 +      params.add(consume(IDENTIFIER, "Identifier required in function constructor."));
 +      consume(IN, "'\\in' required in function constructor.");
 +      Expr set = expression();
 +      Token op = consume(ALL_MAP_TO, "'|->' required in function constructor.");
 +      Expr expr = expression();
 +      consume(RIGHT_BRACKET, "']' required to conclude function constructor.");
 +      return new Expr.QuantFn(op, params, set, expr);
 +    }
 +</code>
 +While the ''Expr.QuantFn'' constructor accepts a list of parameters, we only parse one.
 +
 +The parser code for universal & existential quantification looks similar, but we allow multiple parameters; put this in ''primary()'' just below the function constructor parsing logic:
 +<code java>
 +    if (match(FOR_ALL, EXISTS)) {
 +      Token op = previous();
 +      List<Token> params = new ArrayList<>();
 +      do {
 +        params.add(consume(IDENTIFIER, "Identifier required in quantifier."));
 +      } while (match(COMMA));
 +      consume(IN, "'\\in' required in quantifier.");
 +      Expr set = expression();
 +      consume(COLON, "':' required in quantifier.");
 +      Expr expr = expression();
 +      return new Expr.QuantFn(op, params, set, expr);
 +    }
 +</code>
 +
 +And that concludes function parsing!
 +We can now define both operators and functions with parameters; on to evaluation.
 +
 +====== Section 10.4: Function Objects ======
 +
 +In [[https://craftinginterpreters.com/functions.html#function-objects|Section 10.4]] we write a class implementing the ''TlaCallable'' interface and hook our function & operator definitions up in the interpreter.
 +Create a new file called ''TlaOperator.java'':
 +<code java>
 +package tla;
 +
 +import java.util.List;
 +
 +class TlaOperator implements TlaCallable {
 +  private final Stmt.OpDef declaration;
 +  TlaOperator(Stmt.OpDef declaration) {
 +    this.declaration = declaration;
 +  }
 +}
 +</code>
 +
 +The implementation of the ''call()'' method is exactly as defined in the book:
 +<code java>
 +  @Override
 +  public Object call(Interpreter interpreter,
 +                     List<Object> arguments) {
 +    Environment environment = new Environment(interpreter.globals);
 +    for (int i = 0; i < declaration.params.size(); i++) {
 +      environment.define(declaration.params.get(i).lexeme,
 +          arguments.get(i));
 +    }
 +
 +    interpreter.executeBlock(declaration.body, environment);
 +    return null;
 +  }
 +</code>
 +Here we see the usage of ''interpreter.globals''; we define the argument values within a new ''Environment'' instance, but the parent of that ''Environment'' is the root global instance instead of the current instance.
 +This is so nested operator calls do not propagate their argument values to the nested callee.
 +
 +This method calls a nonexistent ''executeBlock()'' method which we will define in ''Interpreter'':
 +<code java>
 +  Object executeBlock(Expr expr, Environment environment) {
 +    Environment previous = this.environment;
 +    try {
 +      this.environment = environment;
 +      return evaluate(expr);
 +    } finally {
 +      this.environment = previous;
 +    }
 +  }
 +</code>
 +In the book, ''executeBlock()'' was defined back in [[https://craftinginterpreters.com/statements-and-state.html#block-syntax-and-semantics|Chapter 8]] and looked quite a bit different.
 +Since TLA⁺ is not an imperative language with code blocks in the traditional sense, we define ''executeBlock()'' over expressions instead of lists of statements.
 +Wrapping the evaluation in a ''try''/''finally'' ensures that if a runtime exception is thrown our environment is not left in an invalid state.
 +
 +Back in ''TlaOperator'', we still need to implement the ''arity()'' interface method:
 +<code java>
 +  @Override
 +  public int arity() {
 +    return declaration.params.size();
 +  }
 +</code>
 +
 +For ease of use we'll also override ''toString()'':
 +<code java>
 +  @Override
 +  public String toString() {
 +    return "<fn " + declaration.name.lexeme + ">";
 +  }
 +</code>
 +
 +There is only one more thing to do and then parameterized operators will be fully functional (operational?): modify ''visitOpDefStmt()'' in ''Interpreter'' so that it defines new ''TlaOperator'' instances instead of evaluating the statement body directly:
 +<code java [highlight_lines_extra="3,4"]>
 +  @Override
 +  public Void visitOpDefStmt(Stmt.OpDef stmt) {
 +    TlaOperator op = new TlaOperator(stmt);
 +    environment.define(stmt.name, op);
 +    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>
 +
 +And that takes care of operators!
 +Now to handle functions.
 +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>
 +  @Override
 +  public Object visitQuantFnExpr(Expr.QuantFn expr) {
 +    checkNotDefined(expr.params);
 +    Object set = evaluate(expr.set);
 +    checkSetOperand(expr.op, set);
 +    switch (expr.op.type) {
 +      case ALL_MAP_TO: {
 +
 +      } case FOR_ALL: {
 +
 +      } case EXISTS: {
 +
 +      } default: {
 +        // Unreachable.
 +        return null;
 +      }
 +    }
 +  }
 +</code>
 +
 +Thinking about it, the code to implement these operators is fairly tricky.
 +We want to generate a series of bindings of set elements to identifiers.
 +Let's fill out the ''FOR_ALL'' case to get a sense of how we want this to look; note that like our conjunction implementation in the previous chapter, universal quantification is short-circuiting and returns false as soon as it encounters a counterexample to the body predicate:
 +<code java [highlight_lines_extra="2,3,4,5,6,7"]>
 +      } case FOR_ALL: {
 +        for (Environment binding : bindings) {
 +          Object result = executeBlock(expr.body, binding);
 +          checkBooleanOperand(expr.op, result);
 +          if (!(Boolean)result) return false;
 +        }
 +        return true;
 +      } case EXISTS: {
 +</code>
 +This is nice, concise code.
 +We iterate over a series of bindings - in the form of ''Environment'' instances - which enumerate all possible bindings of set values to identifiers.
 +But what is ''bindings''?
 +This is one of the more algorithmically tricky parts of this entire tutorial series, but it is also very fun!
 +We are going to encapsulate the binding generation logic in a new class file, ''BindingGenerator.java'', where the class implements both the ''Iterator<Environment>'' and ''Iterable<Environment>'' standard Java interfaces:
 +<code java>
 +package tla;
 +
 +import java.util.ArrayList;
 +import java.util.Iterator;
 +import java.util.List;
 +import java.util.Set;
 +
 +class BindingGenerator implements Iterator<Environment>,
 +                                  Iterable<Environment> {
 +  private final List<Token> vars;
 +  private final List<Object> set;
 +  private final Environment parent;
 +
 +  BindingGenerator(List<Token> vars, Set<?> set, Environment parent) {
 +    this.vars = vars;
 +    this.set = new ArrayList<>(set);
 +    this.parent = parent;
 +  }
 +
 +  @Override
 +  public Iterator<Environment> iterator() {
 +    return this;
 +  }
 +}
 +</code>
 +Implementing the ''Iterator<>'' and ''Iterable<>'' interfaces allows us to treat ''BindingGenerator'' instances as things that can be iterated over in Java's nice [[https://docs.oracle.com/javase/8/docs/technotes/guides/language/foreach.html|for-each loop]] syntax.
 +So that's what ''bindings'' is!
 +A ''BindingGenerator'' instance!
 +
 +Before getting too far into the weeds with the ''BindingGenerator'' iterator algorithm, let's just assume it works and fill out the rest of ''visitQuantFnExpr()''.
 +Construct a ''BindingGenerator'' instance atop the ''switch'' statement:
 +<code java [highlight_lines_extra="4"]>
 +  public Object visitQuantFnExpr(Expr.QuantFn expr) {
 +    Object set = evaluate(expr.set);
 +    checkSetOperand(expr.op, set);
 +    BindingGenerator bindings = new BindingGenerator(expr.params, (Set<?>)set, environment);
 +    switch (expr.op.type) {
 +</code>
 +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>
 +op(x) == \A y \in 0 .. 2 : y < x 
 +</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):
 +<code java [highlight_lines_extra="2,3,4,5,6,7,8"]>
 +      } case EXISTS: {
 +        boolean result = false;
 +        for (Environment binding : bindings) {
 +          Object junctResult = executeBlock(expr.body, binding);
 +          checkBooleanOperand(expr.op, junctResult);
 +          result |= (boolean)junctResult;
 +        }
 +        return result;
 +      } default: {
 +</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:
 +<code java [highlight_lines_extra="2,3,4,5,6,7"]>
 +      case ALL_MAP_TO: {
 +        Token param = expr.params.get(0);
 +        Map<Object, Object> function = new HashMap<>();
 +        for (Environment binding : bindings) {
 +          function.put(binding.get(param), executeBlock(expr.body, binding));
 +        }
 +        return function;
 +      } case FOR_ALL: {
 +</code>
 +
 +====== Set Enumeration ======
 +
 +Now that we've finished all that, let's get to the real difficult part: implementing an enumeration algorithm in ''BindingGenerator''.
 +A moment of consideration is in order.
 +If you had to bind a set of variables to every combination of values from a set, how would you do it?
 +To computer scientists, the connection between enumerating every possible combination of values and incrementing numbers in an arbitrary base is readily made.
 +For example, imagine you had a set of three values ''{a, b, c}'' that you wanted to bind to two identifiers ''x'' and ''y''.
 +This is isomorphic to iterating through all possible values of a two-digit number in base three.
 +The number of digits corresponds to the number of variables to bind, and the base corresponds to the number of elements in the set.
 +
 +This is confusing, but we will walk through it step by step.
 +First we must assign an arbitrary order to the set so we can map single digits in base three to an element of the set:
 +^ Digit ^ Element ^
 +| 0     | a       |
 +| 1     | b       |
 +| 2     | c       |
 +
 +Using that mapping, here's a table showing how counting up through all two-digit base three numbers decomposes into binding all possible combinations of values to ''x'' and ''y'':
 +^ Number (base 3) ^ As set elements ^ x (0th-significant digit) ^ y (1st-significant digit) ^
 +| 00              | aa              | a                         | a                         |
 +| 01              | ab              | b                         | a                         |
 +| 02              | ac              | c                         | a                         |
 +| 10              | ba              | a                         | b                         |
 +| 11              | bb              | b                         | b                         |
 +| 12              | bc              | c                         | b                         |
 +| 20              | ca              | a                         | c                         |
 +| 21              | cb              | b                         | c                         |
 +| 22              | cc              | c                         | c                         |
 +
 +As you can see, we generated every possible binding of ''{a, b, c}'' to ''x'' and ''y''!
 +Each identifier is assigned a particular digit in the number, and their value in a binding is given by that digit's value in the enumeration.
 +
 +We're almost there, but not quite; Java doesn't have the built-in ability to iterate through numbers in a particular base.
 +We will need to increment a regular ''int'' counter and //convert// it into the desired base, then extract the value of each digit.
 +Actually the well-known [[https://en.wikipedia.org/wiki/Positional_notation#Base_conversion|base conversion]] algorithm lets us do both at once!
 +It is quite elegant; given a number ''n'' and a desired base ''b'', the value of the least-significant digit can be found by calculating ''n % b'' (''%'' meaning mod, giving the division remainder).
 +Then, assign ''n' = n / b'' (using integer division, so throw away the remainder) and repeat for as many digits as desired.
 +Confused? Here's how it looks as a table for converting the enumeration value 6 to a binding from our previous base 3 example:
 +^ Iteration ^ ''n'' ^ ''n % 3'' ^ ''n / 3'' ^
 +| 0         | 6     | 0         | 2         |
 +| 1         | 2     | 2         | 0         |
 +
 +Note that the value of ''n / 3'' always becomes the value of ''n'' in the next row.
 +Reading the ''n % 3'' column from bottom to top we see "20", which is 6 in base 3.
 +Consulting our tables, we see "20" should map to ''ca''.
 +''x'' gets the 0th (least significant) digit, so it should get ''a''.
 +''y'' gets the 1st-significant digit, so it should get ''c''.
 +
 +The iteration number actually corresponds to digit significance.
 +So, in iteration 0, ''x'' should get the value of the ''n % 3'' column, which we see is 0 and thus ''a'' as expected.
 +In iteration 1, ''y'' should get the value of the ''n % 3'' column, which we see is 2 and thus ''c'' as expected.
 +If this is still too abstract, try some other values to convince yourself that our algorithm successfully calculates the binding!
 +
 +Now to implement it.
 +First, add another field to the ''BindingGenerator'' class:
 +<code java [highlight_lines_extra="6"]>
 +class BindingGenerator implements Iterator<Environment>,
 +                                  Iterable<Environment> {
 +  private final List<Token> vars;
 +  private final List<Object> set;
 +  private final Environment parent;
 +  private int enumerationIndex = 0;
 +</code>
 +
 +Then, implement ''hasNext()''.
 +This is required by the ''Iterator<>'' interface and returns true if there are additional un-enumerated combinations.
 +In our case, we test that ''enumerationIndex'' is strictly less than the number of elements in the set raised to the power of the number of identifiers.
 +For ''n'' digits in base ''b'', there are ''bⁿ'' possible values to iterate through.
 +<code java>
 +  @Override
 +  public boolean hasNext() {
 +    return enumerationIndex < Math.pow(set.size(), vars.size());
 +  }
 +</code>
 +
 +Now for the main event.
 +Here's the strikingly simple code implementing the change-of-base algorithm in the ''next()'' method required by the ''Iterator<>'' interface:
 +<code java>
 +  @Override
 +  public Environment next() {
 +    int current = enumerationIndex++;
 +    Environment bindings = new Environment(parent);
 +    for (Token var : vars) {
 +      bindings.define(var, set.get(current % set.size()));
 +      current /= set.size();
 +    }
 +
 +    return bindings;
 +  }
 +</code>
 +
 +Note that ''enumerationIndex++'' retrieves the current value of ''enumerationIndex'' to store in ''current'' and then increments the value of ''enumerationIndex'' itself.
 +A nice little terse code trick.
 +
 +And we're done!
 +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]].
 +On to the next chapter: [[creating:actions|Variables, States, and Actions]]!
 +
 +====== Challenges ======
 +
 +  - In the full TLA⁺ language, quantified functions can be even more complicated; for example, you can write ''\A x, y \in 0 .. 2, z \in 0 .. 5 : P(x, y, z)''. Modify the definition of ''Expr.QuantFn'' and your parsing code to handle this syntax.
 +  - Modify the change-of-base algorithm to handle enumerating multiple sets of varying cardinality, as required to interpret the expressions parsed in the first challenge.
 +  - Our enumeration algorithm is a "depth-first" enumeration: all elements of one set will be enumerated before enumerating a second element of any of the other sets. Come up with an enumeration algorithm that enumerates sets in breadth-first order instead, so the enumeration progresses evenly for each set.
 +  - Often, sets in TLA⁺ models are very large. Instead of immediately evaluating sets constructed with the ''..'' infix operator and holding them in memory, write a class that lazily generates set elements as requested. Integrate this lazy evaluation with the breadth-first binding enumeration from the previous challenge.
 +
 +[[creating:jlists|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:actions|Next Page >]]
  
  • creating/operators.1747258900.txt.gz
  • Last modified: 2025/05/14 21:41
  • by ahelwer