diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java index 969fa2903cd71014879d8a1e14bb1911807930e6..50c5db07d705761342e449d4fb7bd5e40857ae96 100644 --- a/src/main/java/de/tla2bAst/BAstCreator.java +++ b/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,24 +944,36 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, new ABooleanTrueExpression()); } - List<PExpression> params = new ArrayList<PExpression>(); - for (int i = 0; i < n.getArgs().length; i++) { - params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i])); - } + 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])); + } - if (predicateVsExpression.getDefinitionType(def) == DefinitionType.EXPRESSION) { - ADefinitionExpression defCall = new ADefinitionExpression(); - defCall.setDefLiteral(new TIdentifierLiteral(getName(def))); - defCall.setParameters(params); - return new AEqualPredicate(defCall, new ABooleanTrueExpression()); + if (predicateVsExpression.getDefinitionType(def) == DefinitionType.EXPRESSION) { + ADefinitionExpression defCall = new ADefinitionExpression(); + defCall.setDefLiteral(new TIdentifierLiteral(getName(def))); + defCall.setParameters(params); + return new AEqualPredicate(defCall, + new ABooleanTrueExpression()); - } else { - ADefinitionPredicate defCall = new ADefinitionPredicate(); - defCall.setDefLiteral(new TDefLiteralPredicate(getName(def))); + } else { + ADefinitionPredicate defCall = new ADefinitionPredicate(); + defCall.setDefLiteral(new TDefLiteralPredicate(getName(def))); - defCall.setParameters(params); - return defCall; + 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) { diff --git a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java index f57db27b211a273e7ed565699818078b24d50456..c1722d8c3542ed254119a517f773fd25b3721eda 100644 --- a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java +++ b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java @@ -20,6 +20,17 @@ public class ComplexExpressionTest { public void testLetIn() throws Exception { 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 { diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java index a11a4dd11a0f2870c3fe8254f1e9caf024e1817a..7e2af8f3e9d1011273ed4f4d12eeca960951a5c4 100644 --- a/src/test/java/de/tla2b/util/TestUtil.java +++ b/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);