fixed bug translating let statements

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

@@ -118,6 +118,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 						.getName());
 				return OperatorTypes.bbuiltInOperatorIsPredicate(opcode);
 			}
+		} else if (expr.getKind() == LetInKind){
+			LetInNode letInNode = (LetInNode) expr;
+			return expressionIsAPredicate(letInNode.getBody());
 		}
 		return false;
 	}
@@ -941,6 +944,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 					new ABooleanTrueExpression());
 		}
 
+		if (Arrays.asList(moduleNode.getOpDefs()).contains(def)) {
 			List<PExpression> params = new ArrayList<PExpression>();
 			for (int i = 0; i < n.getArgs().length; i++) {
 				params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
@@ -950,7 +954,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 				ADefinitionExpression defCall = new ADefinitionExpression();
 				defCall.setDefLiteral(new TIdentifierLiteral(getName(def)));
 				defCall.setParameters(params);
-			return new AEqualPredicate(defCall, new ABooleanTrueExpression());
+				return new AEqualPredicate(defCall,
+						new ABooleanTrueExpression());
 
 			} else {
 				ADefinitionPredicate defCall = new ADefinitionPredicate();
@@ -959,6 +964,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 				defCall.setParameters(params);
 				return defCall;
 			}
+		}else{
+			FormalParamNode[] params = def.getParams();
+			for (int i = 0; i < params.length; i++) {
+				FormalParamNode param = params[i];
+				param.setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
+			}
+			PPredicate result = visitExprNodePredicate(def.getBody());
+			return result;
+		}
+
 	}
 
 	private String getName(SymbolNode def) {

src/test/java/de/tla2b/expression/ComplexExpressionTest.java

@@ -21,6 +21,17 @@ public class ComplexExpressionTest {
 		compareExpr("1 + 1", "LET foo == 1 IN foo + foo");
 	}
 	
+	@Test
+	public void testLetPredicate() throws Exception {
+		compareExpr("1=1 & 1 = 1", "LET foo == 1 = 1 IN foo /\\ foo");
+	}
+	
+	@Test
+	public void testLetParameterPredicate() throws Exception {
+		compareExpr("1=1 & 1 = 2", "LET foo(a,b) == a = b IN foo(1,1) /\\ foo(1,2)");
+	}
+	
+
 	@Test
 	public void testLetDefWithArgs() throws Exception {
 		compareExpr("2 * 4", "LET foo(x,y) == x * y IN foo(2,4) ");

src/test/java/de/tla2b/util/TestUtil.java

@@ -64,7 +64,7 @@ public class TestUtil {
 		Renamer renamer = new Renamer(resultNode);
 		ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
 		resultNode.apply(aP);
-		//System.out.println(aP.getResultString());
+		System.out.println(aP.getResultString());
 		String bAstString = getAstStringofBExpressionString(bExpr);
 		String result = getAstStringofBExpressionString(aP.getResultString());
 		// String tlaAstString = getTreeAsString(resultNode);