Improve performance of operators

 1. wrap them in a LET so arguments are not evaluated multiple times

 2. add special translation for some TLA standard operators

src/main/java/de/tla2bAst/BAstCreator.java

@@ -26,6 +26,7 @@ import tlc2.value.impl.*;
 import java.util.*;
 import java.util.Map.Entry;
 import java.util.stream.Collectors;
+import java.util.stream.IntStream;
 
 import static de.be4.classicalb.core.parser.util.ASTBuilder.*;
 import static de.tla2b.analysis.TypeChecker.getType;
@@ -182,24 +183,87 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
 				.map(bDefinitions::getDefinition).collect(Collectors.toList()); // add external functions
 		for (OpDefNode opDefNode : bDefs) {
 			List<PExpression> params = Arrays.stream(opDefNode.getParams())
-					.map(this::createIdentifierFromNode).collect(Collectors.toList());
-			// TLAType type = getType(OpDefNode);
-			// if (opDefNode.level == 2 || type instanceof BoolType) {
+				                           .map(this::createIdentifierFromNode)
+				                           .collect(Collectors.toList());
 			PDefinition definition;
 			if (predicateVsExpression.getDefinitionType(opDefNode) == DefinitionType.PREDICATE) {
+				PPredicate pred = null;
+				// special predicate definitions
+
+				if (pred == null) {
+					pred = visitExprNodePredicate(opDefNode.getBody());
+					if (!params.isEmpty()) {
+						// wrap in let to force single evaluation of all params
+						List<PExpression> paramsCopy = params;
+						List<PExpression> defParams = Arrays.stream(opDefNode.getParams())
+							                              .map(p -> createPositionedNode(createIdentifier("p__" + getName(p)), p))
+							                              .collect(Collectors.toList());
+						params = defParams;
+						List<PPredicate> conjuncts = IntStream.range(0, paramsCopy.size())
+							                             .mapToObj(i -> {
+								                             PExpression param = paramsCopy.get(i);
+								                             PExpression defParam = defParams.get(i);
+								                             return new AEqualPredicate(param.clone(), defParam.clone());
+							                             })
+							                             .collect(Collectors.toList());
+						pred = new ALetPredicatePredicate(paramsCopy, createConjunction(conjuncts), pred);
+					}
+					DebugUtils.printVeryVerboseMsg("Creating Predicate DEFINITION " + getName(opDefNode));
+				} else {
+					DebugUtils.printVeryVerboseMsg("Creating Predicate DEFINITION " + getName(opDefNode) + " (optimized)");
+				}
 				definition = new APredicateDefinitionDefinition(
 					new TDefLiteralPredicate(getName(opDefNode)),
 					params,
-						visitExprNodePredicate(opDefNode.getBody())
+					pred
 				);
-				DebugUtils.printVeryVerboseMsg("Creating Predicate DEFINITION " + getName(opDefNode));
 			} else {
+				PExpression expr = null;
+
+				// special expression definitions
+				if (opDefNode.isStandardModule()) {
+					List<PExpression> paramAccess = Arrays.stream(opDefNode.getParams())
+						                                .map(this::createIdentifierFromNodeWithoutPos)
+						                                .collect(Collectors.toList());
+					switch (getName(opDefNode)) {
+						case ":>": {
+							expr = createPositionedNode(createSetOfPExpression(createNestedCouple(Arrays.asList(paramAccess.get(0), paramAccess.get(1)))), opDefNode.getBody());
+							break;
+						}
+						case "@@": {
+							expr = createPositionedNode(new AOverwriteExpression(paramAccess.get(1), paramAccess.get(0)), opDefNode.getBody());
+							break;
+						}
+					}
+				}
+
+				if (expr == null) {
+					expr = visitExprNodeExpression(opDefNode.getBody());
+					if (!params.isEmpty()) {
+						// wrap in let to force single evaluation of all params
+						List<PExpression> paramsCopy = params;
+						List<PExpression> defParams = Arrays.stream(opDefNode.getParams())
+							         .map(p -> createPositionedNode(createIdentifier("p__" + getName(p)), p))
+							         .collect(Collectors.toList());
+						params = defParams;
+						List<PPredicate> conjuncts = IntStream.range(0, paramsCopy.size())
+							                             .mapToObj(i -> {
+								                             PExpression param = paramsCopy.get(i);
+															 PExpression defParam = defParams.get(i);
+								                             return new AEqualPredicate(param.clone(), defParam.clone());
+							                             })
+							                             .collect(Collectors.toList());
+						expr = new ALetExpressionExpression(paramsCopy, createConjunction(conjuncts), expr);
+					}
+					DebugUtils.printVeryVerboseMsg("Creating Expression DEFINITION " + getName(opDefNode));
+				} else {
+					DebugUtils.printVeryVerboseMsg("Creating Expression DEFINITION " + getName(opDefNode) + " (optimized)");
+				}
 				definition = new AExpressionDefinitionDefinition(
 					new TIdentifierLiteral(getName(opDefNode)),
 					params,
-						visitExprNodeExpression(opDefNode.getBody())
+					expr
 				);
-				DebugUtils.printVeryVerboseMsg("Creating Expression DEFINITION " + getName(opDefNode));
 			}
 			PDefinition def = createPositionedNode(definition, opDefNode);
 			bDefinitions.addDefinition(def);
@@ -1640,14 +1704,18 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
 
 	// HELPER METHODS
 
-	public AIdentifierExpression createIdentifierFromNode(SymbolNode symbolNode) {
+	public AIdentifierExpression createIdentifierFromNodeWithoutPos(SymbolNode symbolNode) {
 		if (bMacroHandler.containsSymbolNode(symbolNode)) {
-			return createPositionedNode(createIdentifier(bMacroHandler.getNewName(symbolNode)), symbolNode);
+			return createIdentifier(bMacroHandler.getNewName(symbolNode));
 		} else {
-			return createPositionedNode(createIdentifier(symbolNode.getName().toString()), symbolNode);
+			return createIdentifier(symbolNode.getName().toString());
 		}
 	}
 
+	public AIdentifierExpression createIdentifierFromNode(SymbolNode symbolNode) {
+		return createPositionedNode(createIdentifierFromNodeWithoutPos(symbolNode), symbolNode);
+	}
+
 	private List<PExpression> createListOfParameters(FormalParamNode[][] params) {
 		List<PExpression> list = new ArrayList<>();
 		for (FormalParamNode[] formalParamNodes : params) {

src/test/java/de/tla2b/prettyprintb/MacroTest.java

@@ -15,7 +15,7 @@ public class MacroTest {
 			+ "=================================";
 
 		final String expected = "MACHINE Testing\n"
-			+ "DEFINITIONS def(y) == !(x_1).(x_1 : {1} => y = 3); "
+			+ "DEFINITIONS def(p__y) == LET y BE y=p__y IN !(x_1).(x_1 : {1} => y = 3) END; "
 			+ "PROPERTIES #(x).(x : {3} & def(x)) \n" + "END";
 		compare(expected, module);
 	}
@@ -29,7 +29,7 @@ public class MacroTest {
 			+ "=================================";
 
 		final String expected = "MACHINE Testing\n"
-			+ "DEFINITIONS def(y) == !(x_1).(x_1 : {1} => y = 3); "
+			+ "DEFINITIONS def(p__y) == LET y BE y=p__y IN !(x_1).(x_1 : {1} => y = 3) END; "
 			+ "PROPERTIES #(x).(x : {2} & def(x+1)) \n" + "END";
 		compare(expected, module);
 	}
@@ -44,8 +44,8 @@ public class MacroTest {
 			+ "=================================";
 
 		final String expected = "MACHINE Testing\n"
-			+ "DEFINITIONS foo(a) == a; \n"
-			+ "def(y) == !(x_1).(x_1 : {1} => y = 3) \n"
+			+ "DEFINITIONS foo(p__a) == LET a BE a=p__a IN a END; \n"
+			+ "def(p__y) == LET y BE y=p__y IN !(x_1).(x_1 : {1} => y = 3) END\n"
 			+ "PROPERTIES #(x).(x : {2} & foo(bool(def(x))) = TRUE) \n" + "END";
 		compare(expected, module);
 	}
@@ -61,7 +61,7 @@ public class MacroTest {
 
 		final String expected = "MACHINE Testing\n"
 			+ "DEFINITIONS \n"
-			+ "def(y) == !(x_1).(x_1 : {1} => y = 3); \n"
+			+ "def(p__y) == LET y BE y=p__y IN !(x_1).(x_1 : {1} => y = 3) END; \n"
 			+ "foo == #(x).(x : {2} & def(x)); \n"
 			+ "PROPERTIES foo \n" + "END";
 		compare(expected, module);
@@ -78,8 +78,8 @@ public class MacroTest {
 
 		final String expected = "MACHINE Testing\n"
 			+ "DEFINITIONS \n"
-			+ "def(y) == !(x_1).(x_1 : {1} => y = 3); \n"
-			+ "foo(x) == def(x); \n"
+			+ "def(p__y) == LET y BE y=p__y IN !(x_1).(x_1 : {1} => y = 3) END; \n"
+			+ "foo(p__x) == LET x BE x=p__x IN def(x) END; \n"
 			+ "PROPERTIES #(x).(x : {2} & foo(x)) \n" + "END";
 		compare(expected, module);
 	}
@@ -95,7 +95,7 @@ public class MacroTest {
 
 		final String expected = "MACHINE Testing\n"
 			+ "DEFINITIONS \n"
-			+ "def(y) == !(x_1).(x_1 : {1} => y = 3); \n"
+			+ "def(p__y) == LET y BE y=p__y IN !(x_1).(x_1 : {1} => y = 3) END; \n"
 			+ "CONSTANTS x\n"
 			+ "PROPERTIES x : INTEGER & (x = 3 &  def(x)) \n" + "END";
 		compare(expected, module);

src/test/java/de/tla2b/prettyprintb/MiscellaneousConstructsTest.java

@@ -200,7 +200,7 @@ public class MiscellaneousConstructsTest {
 			+ "=================================";
 
 		final String expected = "MACHINE Testing\n"
-			+ "DEFINITIONS RelParFuncEleOf(S,T) == {f|f:POW(S*T) & card(UNION(x).(x:f|{@prj1(x)}))=card(f)};"
+			+ "DEFINITIONS RelParFuncEleOf(p__S,p__T) == LET S,T BE S=p__S & T=p__T IN {f|f:POW(S*T) & card(UNION(x).(x:f|{@prj1(x)}))=card(f)} END;"
 			+ "CONSTANTS k \n"
 			+ "PROPERTIES k : POW(INTEGER*BOOL) & k : RelParFuncEleOf(INTEGER,BOOL) \n"
 			+ "END";

src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java

@@ -26,7 +26,7 @@ public class SimpleModulesTest {
 			+ "=================================";
 
 		final String expected = "MACHINE Testing\n"
-			+ "DEFINITIONS add(a,b) == a + b \n"
+			+ "DEFINITIONS add(p__a,p__b) == LET a,b BE a=p__a & b=p__b IN a + b END\n"
 			+ "PROPERTIES add(1,3) = 4\n"
 			+ "END";
 		compare(expected, module);

src/test/resources/prettyprint/RelParFuncEleOf/RelParFuncEleOf.mch

 MACHINE RelParFuncEleOf
 DEFINITIONS
-RelParFuncEleOf(S, T) == {f|f:POW(S*T) & card(UNION(x).(x:f|{@prj1((@prj1(x), @prj2(x)))}))=card(f)}
+RelParFuncEleOf(p__S, p__T) == LET S,T BE S=p__S & T=p__T IN {f|f:POW(S*T) & card(UNION(x).(x:f|{@prj1((@prj1(x), @prj2(x)))}))=card(f)} END
 CONSTANTS k
 PROPERTIES k:POW(INTEGER*BOOL) & k:RelParFuncEleOf(INTEGER, BOOL)
 END