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/20 20:22] – Change-of-base counting algorithm for set enumeration & binding ahelwercreating:operators [2025/06/19 14:50] (current) – ALL_MAP_TO interpretation splits out Object value = 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 290: 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 297: 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 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 515: 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 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 530: 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;
       } case FOR_ALL: {       } case FOR_ALL: {
 </code> </code>
 +
 +====== Set Enumeration ======
  
 Now that we've finished all that, let's get to the real difficult part: implementing an enumeration algorithm in ''BindingGenerator''. Now that we've finished all that, let's get to the real difficult part: implementing an enumeration algorithm in ''BindingGenerator''.
Line 547: Line 604:
 For example, imagine you had a set of three values ''{a, b, c}'' that you wanted to bind to two identifiers ''x'' and ''y''. 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. This is isomorphic to iterating through all possible values of a two-digit number in base three.
-Confusing? Here's a table illustrating the connection:+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) ^ ^ Number (base 3) ^ As set elements ^ x (0th-significant digit) ^ y (1st-significant digit) ^
 | 00              | aa              | a                         | a                         | | 00              | aa              | a                         | a                         |
Line 559: Line 625:
 | 22              | cc              | c                         | c                         | | 22              | cc              | c                         | c                         |
  
-As you can see, by counting up through all two-digit base-three numbers, we generate every possible binding of ''{a, b, c}'' to ''x'' and ''y''!+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. 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.
-So, for a set ''S'' and list of identifiers ''I'' it suffices to enumerate all ''|I|''-digit numbers of base ''|S|'', where ''| .. |'' means the number of elements in the collection. 
  
 We're almost there, but not quite; Java doesn't have the built-in ability to iterate through numbers in a particular base. 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. 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! 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 ''|S|'', the value of the least-significant digit can be found by calculating ''n % |S|'' (''%'' meaning mod, giving the division remainder). +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 / |S|'' (using integer division) and repeat for as many digits as desired (after some finite number of iterations, the digits all become zero).+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: 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'' ^ ^ Iteration ^ ''n'' ^ ''n % 3'' ^ ''n / 3'' ^
Line 575: Line 640:
 Note that the value of ''n / 3'' always becomes the value of ''n'' in the next row. 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. Reading the ''n % 3'' column from bottom to top we see "20", which is 6 in base 3.
-Now associate each value in the set with a fixed value between ''0'' and ''|S| - 1''. +Consulting our tables, we see "20" should map to ''ca''. 
-In our case, 0 maps to ''a'', 1 maps to ''b'', and 2 maps to ''c''. +''x'' gets the 0th (least significant) digit, so it should get ''a''. 
-The base 3 digit is identified by the iteration value. +''y'' gets the 1st-significant digit, so it should get ''c''.
-The value of ''n % 3'' in the zeroeth iteration gives the 0th-significant digit, from which we derive the value of ''x'' - here, 0 which maps to ''a''. +
-The value of ''n % 3'' in the first iteration gives the 1st-significant digit, from which we derive the value of ''y'' - here, 2 which maps to ''c''. +
-So, enumeration value 6 binds value ''a'' to identifier ''x'' and value ''c'' to identifier ''y''. +
-You should consult the original table and try some other values to convince yourself that our algorithm successfully calculates the binding.+
  
-Now to implement it!+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: First, add another field to the ''BindingGenerator'' class:
 <code java [highlight_lines_extra="6"]> <code java [highlight_lines_extra="6"]>
Line 596: Line 662:
 Then, implement ''hasNext()''. Then, implement ''hasNext()''.
 This is required by the ''Iterator<>'' interface and returns true if there are additional un-enumerated combinations. 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 ''|S|^|I|'':+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> <code java>
   @Override   @Override
Line 619: Line 686:
   }   }
 </code> </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! 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! 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.1747772547.txt.gz
  • Last modified: 2025/05/20 20:22
  • by ahelwer