From 89f1e7e0341445acb6dd0d638f207528396782ae Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 9 May 2014 15:38:51 +0200
Subject: [PATCH] implemented expression translator
---
.../java/de/tla2b/analysis/SpecAnalyser.java | 11 +-
.../AbstractExpressionPrinter.java | 3 +-
.../{pprint => old}/BMachinePrinter.java | 3 +-
.../de/tla2b/{pprint => old}/DContext.java | 2 +-
.../de/tla2b/{pprint => old}/ExprReturn.java | 2 +-
.../{pprint => old}/ExpressionPrinter.java | 3 +-
.../ExpressionTranslatorOld.java} | 10 +-
.../de/tla2b/{translation => old}/TLA2B.java | 4 +-
.../{translation => old}/Tla2BTranslator.java | 2 +-
.../de/tla2b/output/ASTPrettyPrinter.java | 8 +-
.../de/tla2b/translation/BMacroHandler.java | 19 +-
src/main/java/de/tla2bAst/BAstCreator.java | 44 ++-
.../de/tla2bAst/ExpressionTranslator.java | 317 ++++++++++++++++++
src/main/java/de/tla2bAst/Translator.java | 15 +-
.../expression/SimpleExpressionTest.java | 39 +++
.../expression/TestComplexExpression.java | 71 ++++
.../java/de/tla2b/expression/TestError.java | 27 ++
.../de/tla2b/expression/TestKeywords.java | 37 ++
.../de/tla2b/expression/TestSequences.java | 28 ++
.../java/de/tla2b/util/TestTypeChecker.java | 2 +-
src/test/java/de/tla2b/util/TestUtil.java | 34 +-
.../resources/regression/Club/Club_tla.mch | 2 +-
22 files changed, 626 insertions(+), 57 deletions(-)
rename src/main/java/de/tla2b/{pprint => old}/AbstractExpressionPrinter.java (96%)
rename src/main/java/de/tla2b/{pprint => old}/BMachinePrinter.java (96%)
rename src/main/java/de/tla2b/{pprint => old}/DContext.java (85%)
rename src/main/java/de/tla2b/{pprint => old}/ExprReturn.java (91%)
rename src/main/java/de/tla2b/{pprint => old}/ExpressionPrinter.java (96%)
rename src/main/java/de/tla2b/{translation/ExpressionTranslator.java => old/ExpressionTranslatorOld.java} (94%)
rename src/main/java/de/tla2b/{translation => old}/TLA2B.java (94%)
rename src/main/java/de/tla2b/{translation => old}/Tla2BTranslator.java (95%)
create mode 100644 src/main/java/de/tla2bAst/ExpressionTranslator.java
create mode 100644 src/test/java/de/tla2b/expression/SimpleExpressionTest.java
create mode 100644 src/test/java/de/tla2b/expression/TestComplexExpression.java
create mode 100644 src/test/java/de/tla2b/expression/TestError.java
create mode 100644 src/test/java/de/tla2b/expression/TestKeywords.java
create mode 100644 src/test/java/de/tla2b/expression/TestSequences.java
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index c7fec44..ff2ca24 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -83,7 +83,16 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
return specAnalyser;
}
-
+
+
+ public static SpecAnalyser createSpecAnalyserForTlaExpression(ModuleNode m){
+ SpecAnalyser specAnalyser = new SpecAnalyser(m);
+ OpDefNode expr = m.getOpDefs()[m.getOpDefs().length-1];
+ specAnalyser.usedDefinitions.add(expr);
+ specAnalyser.bDefinitionsSet.add(expr);
+ return specAnalyser;
+ }
+
public static SpecAnalyser createSpecAnalyser(ModuleNode m) {
SpecAnalyser specAnalyser = new SpecAnalyser(m);
Hashtable<String, OpDefNode> definitions = new Hashtable<String, OpDefNode>();
diff --git a/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java b/src/main/java/de/tla2b/old/AbstractExpressionPrinter.java
similarity index 96%
rename from src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java
rename to src/main/java/de/tla2b/old/AbstractExpressionPrinter.java
index 1504c6b..d1f11c5 100644
--- a/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java
+++ b/src/main/java/de/tla2b/old/AbstractExpressionPrinter.java
@@ -2,7 +2,7 @@
* @author Dominik Hansen <Dominik.Hansen at hhu.de>
**/
-package de.tla2b.pprint;
+package de.tla2b.old;
import java.util.ArrayList;
import java.util.Hashtable;
@@ -20,7 +20,6 @@ import de.tla2b.types.SetType;
import de.tla2b.types.StructType;
import de.tla2b.types.TLAType;
import de.tla2b.types.TupleType;
-
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AtNode;
import tla2sany.semantic.ExprNode;
diff --git a/src/main/java/de/tla2b/pprint/BMachinePrinter.java b/src/main/java/de/tla2b/old/BMachinePrinter.java
similarity index 96%
rename from src/main/java/de/tla2b/pprint/BMachinePrinter.java
rename to src/main/java/de/tla2b/old/BMachinePrinter.java
index 147ec15..9e435a7 100644
--- a/src/main/java/de/tla2b/pprint/BMachinePrinter.java
+++ b/src/main/java/de/tla2b/old/BMachinePrinter.java
@@ -2,7 +2,7 @@
* @author Dominik Hansen <Dominik.Hansen at hhu.de>
**/
-package de.tla2b.pprint;
+package de.tla2b.old;
import java.util.ArrayList;
import java.util.Hashtable;
@@ -19,7 +19,6 @@ import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.EnumType;
import de.tla2b.types.SetType;
import de.tla2b.types.TLAType;
-
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.FormalParamNode;
diff --git a/src/main/java/de/tla2b/pprint/DContext.java b/src/main/java/de/tla2b/old/DContext.java
similarity index 85%
rename from src/main/java/de/tla2b/pprint/DContext.java
rename to src/main/java/de/tla2b/old/DContext.java
index 988026e..3f2b8b3 100644
--- a/src/main/java/de/tla2b/pprint/DContext.java
+++ b/src/main/java/de/tla2b/old/DContext.java
@@ -2,7 +2,7 @@
* @author Dominik Hansen <Dominik.Hansen at hhu.de>
**/
-package de.tla2b.pprint;
+package de.tla2b.old;
public class DContext {
public StringBuilder indent;
diff --git a/src/main/java/de/tla2b/pprint/ExprReturn.java b/src/main/java/de/tla2b/old/ExprReturn.java
similarity index 91%
rename from src/main/java/de/tla2b/pprint/ExprReturn.java
rename to src/main/java/de/tla2b/old/ExprReturn.java
index dfe31fd..e54d6d3 100644
--- a/src/main/java/de/tla2b/pprint/ExprReturn.java
+++ b/src/main/java/de/tla2b/old/ExprReturn.java
@@ -1,4 +1,4 @@
-package de.tla2b.pprint;
+package de.tla2b.old;
public class ExprReturn {
public StringBuilder out= new StringBuilder();
diff --git a/src/main/java/de/tla2b/pprint/ExpressionPrinter.java b/src/main/java/de/tla2b/old/ExpressionPrinter.java
similarity index 96%
rename from src/main/java/de/tla2b/pprint/ExpressionPrinter.java
rename to src/main/java/de/tla2b/old/ExpressionPrinter.java
index bb2e432..a0b3444 100644
--- a/src/main/java/de/tla2b/pprint/ExpressionPrinter.java
+++ b/src/main/java/de/tla2b/old/ExpressionPrinter.java
@@ -2,14 +2,13 @@
* @author Dominik Hansen <Dominik.Hansen at hhu.de>
**/
-package de.tla2b.pprint;
+package de.tla2b.old;
import java.util.Hashtable;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.types.TLAType;
-
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.ModuleNode;
diff --git a/src/main/java/de/tla2b/translation/ExpressionTranslator.java b/src/main/java/de/tla2b/old/ExpressionTranslatorOld.java
similarity index 94%
rename from src/main/java/de/tla2b/translation/ExpressionTranslator.java
rename to src/main/java/de/tla2b/old/ExpressionTranslatorOld.java
index beffd41..2a545f3 100644
--- a/src/main/java/de/tla2b/translation/ExpressionTranslator.java
+++ b/src/main/java/de/tla2b/old/ExpressionTranslatorOld.java
@@ -2,7 +2,7 @@
* @author Dominik Hansen <Dominik.Hansen at hhu.de>
**/
-package de.tla2b.translation;
+package de.tla2b.old;
import java.io.File;
import java.io.FileWriter;
@@ -16,8 +16,6 @@ import de.tla2b.analysis.TypeChecker;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TLA2BIOException;
import de.tla2b.exceptions.TypeErrorException;
-import de.tla2b.pprint.ExpressionPrinter;
-
import tla2sany.drivers.FrontEndException;
import tla2sany.drivers.InitException;
import tla2sany.drivers.SANY;
@@ -29,7 +27,7 @@ import tla2sany.st.SyntaxTreeConstants;
import tla2sany.st.TreeNode;
import util.ToolIO;
-public class ExpressionTranslator implements SyntaxTreeConstants {
+public class ExpressionTranslatorOld implements SyntaxTreeConstants {
private String TLAExpression;
private ArrayList<String> variables;
private ArrayList<String> noVariables;
@@ -39,7 +37,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
throws TLA2BException {
ToolIO.reset();
ToolIO.setMode(ToolIO.TOOL);
- ExpressionTranslator et = new ExpressionTranslator(tlaExpression);
+ ExpressionTranslatorOld et = new ExpressionTranslatorOld(tlaExpression);
try {
et.start();
} catch (RuntimeException e) {
@@ -49,7 +47,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
return et.BExpression.toString();
}
- public ExpressionTranslator(String TLAExpression) {
+ public ExpressionTranslatorOld(String TLAExpression) {
this.TLAExpression = TLAExpression;
this.variables = new ArrayList<String>();
this.noVariables = new ArrayList<String>();
diff --git a/src/main/java/de/tla2b/translation/TLA2B.java b/src/main/java/de/tla2b/old/TLA2B.java
similarity index 94%
rename from src/main/java/de/tla2b/translation/TLA2B.java
rename to src/main/java/de/tla2b/old/TLA2B.java
index 0875681..af6a755 100644
--- a/src/main/java/de/tla2b/translation/TLA2B.java
+++ b/src/main/java/de/tla2b/old/TLA2B.java
@@ -2,7 +2,7 @@
* @author Dominik Hansen <Dominik.Hansen at hhu.de>
**/
-package de.tla2b.translation;
+package de.tla2b.old;
import java.io.BufferedReader;
import java.io.File;
@@ -249,7 +249,7 @@ public class TLA2B implements TranslationGlobals {
} catch (IOException e) {
e.printStackTrace();
}
- ExpressionTranslator et = new ExpressionTranslator(expr);
+ ExpressionTranslatorOld et = new ExpressionTranslatorOld(expr);
try {
et.start();
} catch (TLA2BException e) {
diff --git a/src/main/java/de/tla2b/translation/Tla2BTranslator.java b/src/main/java/de/tla2b/old/Tla2BTranslator.java
similarity index 95%
rename from src/main/java/de/tla2b/translation/Tla2BTranslator.java
rename to src/main/java/de/tla2b/old/Tla2BTranslator.java
index 92c97f2..4bad7d4 100644
--- a/src/main/java/de/tla2b/translation/Tla2BTranslator.java
+++ b/src/main/java/de/tla2b/old/Tla2BTranslator.java
@@ -1,4 +1,4 @@
-package de.tla2b.translation;
+package de.tla2b.old;
import java.io.File;
import java.io.FileWriter;
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index f36db50..9c8902b 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -9,17 +9,16 @@ import de.be4.classicalb.core.parser.analysis.ExtendedDFAdapter;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
-import de.be4.classicalb.core.parser.node.ABlockSubstitution;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.AExpressionParseUnit;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.ALambdaExpression;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
import de.be4.classicalb.core.parser.node.ASelectSubstitution;
-import de.be4.classicalb.core.parser.node.ASkipSubstitution;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PMachineClause;
@@ -178,7 +177,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
putSymbol("ABoolSetExpression", "BOOL");
putSymbol("AStringSetExpression", "STRING");
putSymbol("ASkipSubstitution", "skip");
-
+
putPreEnd("APowSubsetExpression", "POW(", ")");
putPreEnd("AConvertBoolExpression", "bool(", ")");
putPreEnd("ADomainExpression", "dom(", ")");
@@ -196,8 +195,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
putPreEnd("ABlockSubstitution", "BEGIN ", " END");
// TODO other substitutions
-
-
+
put("ASetExtensionExpression", null, "{", ", ", "}", null, null);
put("AStructExpression", "struct", "(", ", ", ")", null, null);
put("ARecExpression", "rec", "(", ", ", ")", null, null);
diff --git a/src/main/java/de/tla2b/translation/BMacroHandler.java b/src/main/java/de/tla2b/translation/BMacroHandler.java
index 04237df..a6c3cc1 100644
--- a/src/main/java/de/tla2b/translation/BMacroHandler.java
+++ b/src/main/java/de/tla2b/translation/BMacroHandler.java
@@ -20,12 +20,14 @@ import de.tla2b.config.ConfigfileEvaluator;
public class BMacroHandler extends AbstractASTVisitor {
+ private final Hashtable<FormalParamNode, String> renamingTable = new Hashtable<FormalParamNode, String>();
+
public BMacroHandler(SpecAnalyser specAnalyser, ConfigfileEvaluator conEval) {
ModuleNode moduleNode = specAnalyser.getModuleNode();
ArrayList<OpDefNode> bDefs = new ArrayList<OpDefNode>();
for (int i = 0; i < moduleNode.getOpDefs().length; i++) {
OpDefNode def = moduleNode.getOpDefs()[i];
- if(specAnalyser.getUsedDefinitions().contains(def)){
+ if (specAnalyser.getUsedDefinitions().contains(def)) {
if (conEval != null
&& conEval.getConstantOverrideTable()
.containsValue(def)) {
@@ -42,6 +44,9 @@ public class BMacroHandler extends AbstractASTVisitor {
visitAssumptions(moduleNode.getAssumptions());
}
+ public BMacroHandler() {
+ }
+
private HashSet<FormalParamNode> definitionParameters;
private HashSet<FormalParamNode> localVariables;
private final Hashtable<FormalParamNode, Set<FormalParamNode>> parameterContext = new Hashtable<FormalParamNode, Set<FormalParamNode>>();
@@ -72,7 +77,6 @@ public class BMacroHandler extends AbstractASTVisitor {
localVariables = null;
}
-
@Override
public void visitBuiltInNode(OpApplNode n) {
@@ -115,7 +119,6 @@ public class BMacroHandler extends AbstractASTVisitor {
}
}
-
private Set<String> getStringSet(Set<FormalParamNode> set) {
HashSet<String> stringSet = new HashSet<String>();
@@ -156,8 +159,6 @@ public class BMacroHandler extends AbstractASTVisitor {
}
}
- Hashtable<FormalParamNode, String> renamingTable = new Hashtable<FormalParamNode, String>();
-
@Override
public void visitFormalParamNode(OpApplNode n) {
FormalParamNode param = (FormalParamNode) n.getOperator();
@@ -168,7 +169,6 @@ public class BMacroHandler extends AbstractASTVisitor {
hasSymbolAValidName(n);
}
-
public void visitConstantNode(OpApplNode n) {
hasSymbolAValidName(n);
}
@@ -176,8 +176,8 @@ public class BMacroHandler extends AbstractASTVisitor {
public void visitVariableNode(OpApplNode n) {
hasSymbolAValidName(n);
}
-
- private void hasSymbolAValidName(OpApplNode n){
+
+ private void hasSymbolAValidName(OpApplNode n) {
SymbolNode symbol = n.getOperator();
String symbolName = symbol.getName().toString();
if (illegalParams != null) {
@@ -190,8 +190,7 @@ public class BMacroHandler extends AbstractASTVisitor {
}
}
}
-
-
+
Set<String> globalNames = new HashSet<String>();
private Boolean existingName(String name) {
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 730c6d3..cd10aed 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -57,6 +57,7 @@ import de.be4.classicalb.core.parser.node.AEqualPredicate;
import de.be4.classicalb.core.parser.node.AEquivalencePredicate;
import de.be4.classicalb.core.parser.node.AExistsPredicate;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.AExpressionParseUnit;
import de.be4.classicalb.core.parser.node.AFinSubsetExpression;
import de.be4.classicalb.core.parser.node.AFirstExpression;
import de.be4.classicalb.core.parser.node.AForallPredicate;
@@ -128,7 +129,6 @@ import de.be4.classicalb.core.parser.node.TStringLiteral;
import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.PredicateVsExpression;
import de.tla2b.analysis.RecursiveDefinition;
-import de.tla2b.analysis.RecursiveFunktion;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.analysis.UsedExternalFunctions;
import de.tla2b.analysis.PredicateVsExpression.DefinitionType;
@@ -159,13 +159,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private final BMacroHandler bMacroHandler;
private final RecursiveFunctionHandler recursiveFunctionHandler;
-
-
- final HashSet<OpDefNode> allTLADefinitions;
- List<OpDeclNode> bConstants;
+ private List<OpDeclNode> bConstants;
private ModuleNode moduleNode;
- private final UsedExternalFunctions usedExternalFunctions;
+ private UsedExternalFunctions usedExternalFunctions;
private Definitions bDefinitions = new Definitions();
@@ -178,6 +175,22 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return bDefinitions;
}
+ public Start expressionStart;
+
+ public BAstCreator(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
+ this.moduleNode = moduleNode;
+ this.specAnalyser = specAnalyser;
+ this.bMacroHandler = new BMacroHandler();
+ this.predicateVsExpression = new PredicateVsExpression(moduleNode);
+ this.recursiveFunctionHandler = new RecursiveFunctionHandler(specAnalyser);
+
+ ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1]
+ .getBody();
+ AExpressionParseUnit expressionParseUnit = new AExpressionParseUnit();
+ expressionParseUnit.setExpression(visitExprNodeExpression(expr));
+ expressionStart = new Start(expressionParseUnit, new EOF());
+ }
+
public BAstCreator(ModuleNode moduleNode, ConfigfileEvaluator conEval,
SpecAnalyser specAnalyser,
UsedExternalFunctions usedExternalFunctions,
@@ -192,8 +205,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
this.usedExternalFunctions = usedExternalFunctions;
- this.allTLADefinitions = new HashSet<OpDefNode>(
- Arrays.asList(moduleNode.getOpDefs()));
if (conEval != null) {
this.bConstants = conEval.getbConstantList();
@@ -920,7 +931,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
- if (allTLADefinitions.contains(def)) {
+ 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]));
@@ -1706,6 +1717,21 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
implication));
}
+ case OPCODE_be: { // \E x \in S : P
+ FormalParamNode[][] params = n.getBdedQuantSymbolLists();
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 0; i < params.length; i++) {
+ for (int j = 0; j < params[i].length; j++) {
+ list.add(createIdentifierNode(params[i][j]));
+ }
+ }
+ AConjunctPredicate conjunction = new AConjunctPredicate();
+ conjunction.setLeft(visitBounded(n));
+ conjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
+ AExistsPredicate exists = new AExistsPredicate(list, conjunction);
+ return new AConvertBoolExpression(exists);
+ }
+
}
throw new RuntimeException(n.getOperator().getName().toString());
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
new file mode 100644
index 0000000..a75e2ab
--- /dev/null
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -0,0 +1,317 @@
+package de.tla2bAst;
+
+import java.io.File;
+import java.io.FileWriter;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.Set;
+
+import tla2sany.drivers.FrontEndException;
+import tla2sany.drivers.InitException;
+import tla2sany.drivers.SANY;
+import tla2sany.modanalyzer.ParseUnit;
+import tla2sany.modanalyzer.SpecObj;
+import tla2sany.parser.ParseException;
+import tla2sany.semantic.ModuleNode;
+import tla2sany.st.SyntaxTreeConstants;
+import tla2sany.st.TreeNode;
+import util.ToolIO;
+import de.be4.classicalb.core.parser.node.AExpressionParseUnit;
+import de.be4.classicalb.core.parser.node.Start;
+import de.tla2b.analysis.SpecAnalyser;
+import de.tla2b.analysis.SymbolRenamer;
+import de.tla2b.analysis.TypeChecker;
+import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.old.Tla2BTranslator;
+
+public class ExpressionTranslator implements SyntaxTreeConstants{
+
+ private final String tlaExpression;
+ private final ArrayList<String> variables = new ArrayList<String>();
+ private final ArrayList<String> noVariables = new ArrayList<String>();
+ private Start expressionStart;
+
+ public Start getBExpressionParseUnit(){
+ return expressionStart;
+ }
+
+
+ public ExpressionTranslator(String tlaExpression) {
+ this.tlaExpression = tlaExpression;
+ }
+
+ public void start(){
+ String dir = System.getProperty("java.io.tmpdir");
+ ToolIO.setUserDir(dir);
+
+ File tempFile = null;
+ String moduleName = null;
+ String module = null;
+ try {
+ tempFile = File.createTempFile("Testing", ".tla");
+
+ moduleName = tempFile.getName().substring(0,
+ tempFile.getName().indexOf("."));
+
+ module = "----MODULE " + moduleName + " ----\n"
+ + "Expression == " + tlaExpression + "\n====";
+
+ FileWriter fw = new FileWriter(tempFile);
+ fw.write(module);
+ fw.close();
+ } catch (IOException e) {
+ throw new RuntimeException("Can not create file "
+ + tempFile.getName() + " in directory '" + dir + "'");
+ }
+
+ SpecObj spec = parseModuleWithoutSemanticAnalyse(moduleName, module);
+ evalVariables(spec, moduleName);
+
+ StringBuilder sb = new StringBuilder();
+ sb.append("----MODULE " + moduleName + " ----\n");
+ sb.append("EXTENDS Naturals, Integers, Sequences, FiniteSets \n");
+ if (variables.size() > 0) {
+ sb.append("VARIABLES ");
+ for (int i = 0; i < variables.size(); i++) {
+ if (i != 0) {
+ sb.append(", ");
+ }
+ sb.append(variables.get(i));
+ }
+ sb.append("\n");
+ }
+ sb.append("Expression");
+ sb.append(" == ");
+ sb.append(tlaExpression);
+ sb.append("\n====================");
+
+
+ try {
+ FileWriter fw = new FileWriter(tempFile);
+ fw.write(sb.toString());
+ fw.close();
+ tempFile.deleteOnExit();
+ } catch (IOException e) {
+ e.printStackTrace();
+ throw new RuntimeException(e.getMessage());
+ }
+ ToolIO.reset();
+ expressionStart = translate(moduleName, sb.toString());
+ }
+
+
+ private static Start translate(String moduleName, String expr) {
+ ModuleNode moduleNode = null;
+ try {
+ moduleNode = parseModule(moduleName, expr);
+ } catch (de.tla2b.exceptions.FrontEndException e) {
+ throw new RuntimeException(e.getLocalizedMessage());
+ }
+
+ SpecAnalyser specAnalyser = SpecAnalyser.createSpecAnalyserForTlaExpression(moduleNode);
+ TypeChecker tc = new TypeChecker(moduleNode);
+ try {
+ tc.start();
+ } catch (TLA2BException e) {
+ //String[] m = ToolIO.getAllMessages();
+ String message = "****TypeError****\n"
+ + e.getLocalizedMessage() + "\n" + expr + "\n";
+ // System.out.println(message);
+ throw new RuntimeException(message);
+ }
+
+ SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
+ symRenamer.start();
+ BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);
+
+ return bASTCreator.expressionStart;
+ }
+
+ public static ModuleNode parseModule(String moduleName, String module)
+ throws de.tla2b.exceptions.FrontEndException {
+ SpecObj spec = new SpecObj(moduleName, null);
+ try {
+ SANY.frontEndMain(spec, moduleName, ToolIO.out);
+ } catch (FrontEndException e) {
+ // Error in Frontend, should never happens
+ return null;
+ }
+
+ if (spec.parseErrors.isFailure()) {
+ //String[] m = ToolIO.getAllMessages();
+ String message = module + "\n\n"
+ + spec.parseErrors;
+ // System.out.println(spec.parseErrors);
+ message += Tla2BTranslator.allMessagesToString(ToolIO
+ .getAllMessages());
+ throw new de.tla2b.exceptions.FrontEndException(message, spec);
+ }
+
+ if (spec.semanticErrors.isFailure()) {
+ //String[] m = ToolIO.getAllMessages();
+ String message = module + "\n\n" + spec.semanticErrors;
+ message += Tla2BTranslator.allMessagesToString(ToolIO
+ .getAllMessages());
+ throw new de.tla2b.exceptions.FrontEndException(message, spec);
+ }
+
+ // RootModule
+ ModuleNode n = spec.getExternalModuleTable().rootModule;
+ if (spec.getInitErrors().isFailure()) {
+ System.err.println(spec.getInitErrors());
+ throw new de.tla2b.exceptions.FrontEndException(
+ Tla2BTranslator
+ .allMessagesToString(ToolIO.getAllMessages()),
+ spec);
+ }
+
+ if (n == null) { // Parse Error
+ // System.out.println("Rootmodule null");
+ throw new de.tla2b.exceptions.FrontEndException(
+ Tla2BTranslator
+ .allMessagesToString(ToolIO.getAllMessages()),
+ spec);
+ }
+ return n;
+ }
+
+
+ /**
+ * @param moduleFileName
+ * @throws de.tla2b.exceptions.FrontEndException
+ */
+ private SpecObj parseModuleWithoutSemanticAnalyse(String moduleFileName, String module)
+ {
+ SpecObj spec = new SpecObj(moduleFileName, null);
+
+ try {
+ SANY.frontEndInitialize(spec, ToolIO.out);
+ SANY.frontEndParse(spec, ToolIO.out);
+
+ } catch (InitException e1) {
+ System.out.println(e1);
+ } catch (ParseException e1) {
+ System.out.println(e1);
+ }
+
+ if (spec.parseErrors.isFailure()) {
+ String message = module + "\n\n";
+ message += Tla2BTranslator.allMessagesToString(ToolIO
+ .getAllMessages());
+ //throw new de.tla2b.exceptions.FrontEndException(message, spec);
+ throw new RuntimeException(message);
+ }
+ return spec;
+ }
+
+
+
+ /**
+ * @param spec
+ * @return
+ */
+ private void evalVariables(SpecObj spec, String moduleName) {
+ ParseUnit p = (ParseUnit) spec.parseUnitContext.get(moduleName);
+ TreeNode n_module = p.getParseTree();
+ TreeNode n_body = n_module.heirs()[2];
+ TreeNode n_operatorDefintion = n_body.heirs()[0];
+ TreeNode expr = n_operatorDefintion.heirs()[2];
+ searchVarInSyntaxTree(expr);
+
+ for (int i = 0; i < noVariables.size(); i++) {
+ variables.remove(noVariables.get(i));
+ }
+
+ }
+
+ private final static Set<String> KEYWORDS = new HashSet<String>();
+ static {
+ KEYWORDS.add("BOOLEAN");
+ KEYWORDS.add("TRUE");
+ KEYWORDS.add("FALSE");
+ KEYWORDS.add("Nat");
+ KEYWORDS.add("Int");
+ KEYWORDS.add("Cardinality");
+ KEYWORDS.add("IsFiniteSet");
+ KEYWORDS.add("Append");
+ KEYWORDS.add("Head");
+ KEYWORDS.add("Tail");
+ KEYWORDS.add("Len");
+ KEYWORDS.add("Seq");
+ KEYWORDS.add("SubSeq");
+ KEYWORDS.add("SelectSeq");
+ KEYWORDS.add("MinOfSet");
+ KEYWORDS.add("MaxOfSet");
+ KEYWORDS.add("SetProduct");
+ KEYWORDS.add("SetSummation");
+ KEYWORDS.add("PermutedSequences");
+ KEYWORDS.add("@");
+
+ }
+
+ /**
+ *
+ */
+ private void searchVarInSyntaxTree(TreeNode treeNode) {
+ // System.out.println(treeNode.getKind() + " " + treeNode.getImage());
+ switch (treeNode.getKind()) {
+ case N_GeneralId: {
+ String con = treeNode.heirs()[1].getImage();
+ if (!variables.contains(con) && !KEYWORDS.contains(con)) {
+ variables.add(con);
+ }
+ break;
+ }
+ case N_IdentLHS: { // left side of a definition
+ TreeNode[] children = treeNode.heirs();
+ noVariables.add(children[0].getImage());
+ break;
+ }
+ case N_IdentDecl: { // parameter of a LET definition
+ // e.g. x in LET foo(x) == e
+ noVariables.add(treeNode.heirs()[0].getImage());
+ break;
+ }
+ case N_FunctionDefinition: {
+ // the first child is the function name
+ noVariables.add(treeNode.heirs()[0].getImage());
+ break;
+ }
+ case N_UnboundQuant: {
+ TreeNode[] children = treeNode.heirs();
+ for (int i = 1; i < children.length - 2; i = i + 2) {
+ // System.out.println(children[i].getImage());
+ }
+ searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
+ break;
+ }
+ case N_QuantBound: {
+ TreeNode[] children = treeNode.heirs();
+ for (int i = 0; i < children.length - 2; i = i + 2) {
+ String boundedVar = children[i].getImage();
+ if (!noVariables.contains(boundedVar)) {
+ noVariables.add(boundedVar);
+ }
+ }
+ searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
+ break;
+ }
+ case N_SubsetOf: { // { x \in S : e }
+ TreeNode[] children = treeNode.heirs();
+ String boundedVar = children[1].getImage(); // x
+ if (!noVariables.contains(boundedVar)) {
+ noVariables.add(boundedVar);
+ }
+ searchVarInSyntaxTree(treeNode.heirs()[3]); // S
+ searchVarInSyntaxTree(treeNode.heirs()[5]); // e
+ break;
+ }
+
+ }
+
+ for (int i = 0; i < treeNode.heirs().length; i++) {
+ searchVarInSyntaxTree(treeNode.heirs()[i]);
+ }
+ }
+}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 83aeb92..1d40375 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -23,7 +23,7 @@ import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.output.ASTPrettyPrinter;
-import de.tla2b.pprint.BMachinePrinter;
+import de.tla2b.output.Renamer;
import de.tla2b.translation.BMacroHandler;
import de.tla2b.translation.RecursiveFunctionHandler;
import de.tla2b.util.FileUtils;
@@ -199,13 +199,9 @@ public class Translator implements TranslationGlobals {
TypeChecker typechecker = new TypeChecker(moduleNode, conEval,
specAnalyser);
typechecker.start();
- // specAnalyser.evalIfThenElse();
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
- // BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
- // specAnalyser);
- // bMachineString = p.start().toString();
UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(
moduleNode, specAnalyser);
RecursiveFunctionHandler recursiveFunctionHandler = new RecursiveFunctionHandler(
@@ -253,7 +249,8 @@ public class Translator implements TranslationGlobals {
System.exit(-1);
}
- ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ Renamer renamer = new Renamer(BAst);
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(renamer);
BAst.apply(aP);
StringBuilder result = aP.getResultAsStringbuilder();
result.insert(0, "/*@ generated by TLA2B " + VERSION + " " + new Date()
@@ -275,6 +272,12 @@ public class Translator implements TranslationGlobals {
}
+ public static Start translateTlaExpression(String tlaExpression){
+ ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression);
+ expressionTranslator.start();
+ return expressionTranslator.getBExpressionParseUnit();
+ }
+
public Definitions getBDefinitions() {
return bDefinitions;
diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
new file mode 100644
index 0000000..4afcbc7
--- /dev/null
+++ b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
@@ -0,0 +1,39 @@
+/**
+ * @author Dominik Hansen <Dominik.Hansen at hhu.de>
+ **/
+
+package de.tla2b.expression;
+
+import org.junit.Test;
+
+import static de.tla2b.util.TestUtil.compareExpr;
+
+public class SimpleExpressionTest {
+
+ @Test
+ public void testSimpleExpr() throws Exception {
+ compareExpr("1 + 2", "1 + 2");
+ }
+
+ @Test
+ public void testModulIntegers() throws Exception {
+ compareExpr("bool(-1 : INTEGER)", "-1 \\in Int");
+ }
+
+ @Test
+ public void testExist() throws Exception {
+ compareExpr("bool(#a.(a : {1} & 2 > 1))", "\\E a \\in {1}: 2 > 1");
+ }
+
+ @Test
+ public void testIfThenElse() throws Exception {
+ compareExpr(
+ "(%t_.( t_ = 0 & 1 = 1 | 1 )\\/%t_.( t_ = 0 & not(1 = 1) | 2 ))(0)",
+ "IF 1 = 1 THEN 1 ELSE 2");
+ }
+
+ @Test
+ public void testTRUE() throws Exception {
+ compareExpr("TRUE", "TRUE");
+ }
+}
diff --git a/src/test/java/de/tla2b/expression/TestComplexExpression.java b/src/test/java/de/tla2b/expression/TestComplexExpression.java
new file mode 100644
index 0000000..deb92d0
--- /dev/null
+++ b/src/test/java/de/tla2b/expression/TestComplexExpression.java
@@ -0,0 +1,71 @@
+/**
+ * @author Dominik Hansen <Dominik.Hansen at hhu.de>
+ **/
+
+package de.tla2b.expression;
+
+import org.junit.Test;
+
+import static de.tla2b.util.TestUtil.compareExpr;
+
+public class TestComplexExpression {
+
+ @Test
+ public void testExcept() throws Exception {
+ compareExpr("bool(a = %u.(u : {3, 4, 5}| u + 1) & x = a <+ {3 |-> 1})",
+ "a = [u \\in {3,4,5}|-> u + 1] /\\ x = [a EXCEPT ![3] = 1]");
+ }
+
+ @Test
+ public void testLetIn() throws Exception {
+ compareExpr("1 + 1", "LET foo == 1 IN foo + foo");
+ }
+
+ @Test
+ public void testLetDefWithArgs() throws Exception {
+ compareExpr("2 * 4", "LET foo(x,y) == x * y IN foo(2,4) ");
+ }
+
+ @Test
+ public void testLetTwoDefs() throws Exception {
+ compareExpr("1 + 2", "LET foo == 1 bar == 2 IN foo + bar ");
+ }
+
+ @Test
+ public void testPrime() throws Exception {
+ compareExpr("bool(x_n = 1)", "x' = 1");
+ }
+
+ @Test
+ public void testFunction() throws Exception {
+ compareExpr("%n.(n : {1}| 1)(1)", "LET f[n \\in {1}] == 1 IN f[1]");
+ }
+
+ @Test
+ public void testQuantifier() throws Exception {
+ compareExpr(
+ "bool(#x,z,y.(x : NATURAL & z : NATURAL & y : NATURAL & x = y))",
+ "\\E x,z \\in Nat, y \\in Nat: x = y");
+ }
+
+ @Test
+ public void testFunctions() throws Exception {
+ compareExpr("(%x.(x : 1 .. 10| x * x) <+ {3 |-> 6})(3)", "LET"
+ + " f[x \\in 1..10] == x*x\n" + " h == [f EXCEPT ![3] = 6]\n"
+ + "IN h[3]");
+ }
+
+ @Test
+ public void testRecord() throws Exception {
+ compareExpr("rec(a:rec(a:1, b:TRUE)'a + rec(a:1, b:TRUE)'a, b:rec(a:1, b:TRUE)'b)",
+ "[[a|->1, b |->TRUE] EXCEPT !.a= @+@]");
+ }
+
+ @Test
+ public void testRecord2() throws Exception {
+ compareExpr("bool(r = rec(a:rec(x:1, y:TRUE), b:1) & r2 = rec(a:2, b:r'b))",
+ "r = [a |-> [x|->1,y|->TRUE], b |-> 1] "
+ + "/\\ r2 = [r EXCEPT !.a.x = 2]");
+ }
+
+}
diff --git a/src/test/java/de/tla2b/expression/TestError.java b/src/test/java/de/tla2b/expression/TestError.java
new file mode 100644
index 0000000..a63773f
--- /dev/null
+++ b/src/test/java/de/tla2b/expression/TestError.java
@@ -0,0 +1,27 @@
+/**
+ * @author Dominik Hansen <Dominik.Hansen at hhu.de>
+ **/
+
+package de.tla2b.expression;
+
+import static de.tla2b.util.TestUtil.compareExpr;
+
+import org.junit.Test;
+
+public class TestError {
+
+ @Test(expected = Exception.class)
+ public void testParseError() throws Exception {
+ compareExpr(null, "a =");
+ }
+
+ @Test(expected = Exception.class)
+ public void testSemanticError() throws Exception {
+ compareExpr(null, "a(1)");
+ }
+
+ @Test(expected = Exception.class)
+ public void testTypeError() throws Exception {
+ compareExpr(null, "1 = TRUE");
+ }
+}
diff --git a/src/test/java/de/tla2b/expression/TestKeywords.java b/src/test/java/de/tla2b/expression/TestKeywords.java
new file mode 100644
index 0000000..db85231
--- /dev/null
+++ b/src/test/java/de/tla2b/expression/TestKeywords.java
@@ -0,0 +1,37 @@
+/**
+ * @author Dominik Hansen <Dominik.Hansen at hhu.de>
+ **/
+
+package de.tla2b.expression;
+
+import org.junit.Test;
+
+import static de.tla2b.util.TestUtil.compareExpr;
+
+public class TestKeywords {
+
+ @Test
+ public void testTRUE() throws Exception {
+ compareExpr("TRUE", "TRUE");
+ }
+
+ @Test
+ public void testNat() throws Exception {
+ compareExpr("NATURAL", "Nat");
+ }
+
+ @Test
+ public void testExcept() throws Exception {
+ compareExpr("bool(x = a <+ {1 |-> 1})", "x = [a EXCEPT ![1] = 1]");
+ }
+
+ @Test
+ public void testCardinality() throws Exception {
+ compareExpr("card({1, 2, 3})", "Cardinality({1,2,3})");
+ }
+
+ @Test
+ public void testDom() throws Exception {
+ compareExpr("bool(dom_1 = 1)", "dom = 1");
+ }
+}
diff --git a/src/test/java/de/tla2b/expression/TestSequences.java b/src/test/java/de/tla2b/expression/TestSequences.java
new file mode 100644
index 0000000..9fabeec
--- /dev/null
+++ b/src/test/java/de/tla2b/expression/TestSequences.java
@@ -0,0 +1,28 @@
+/**
+ * @author Dominik Hansen <Dominik.Hansen at hhu.de>
+ **/
+
+package de.tla2b.expression;
+
+import static de.tla2b.util.TestUtil.compareExpr;
+
+import org.junit.Test;
+
+public class TestSequences {
+
+ @Test
+ public void testAppend() throws Exception {
+ compareExpr("[1] <- 2", "Append(<<1>>, 2)");
+ }
+
+ @Test
+ public void testHead() throws Exception {
+ compareExpr("first([1, 2, 3])", "Head(<<1,2,3>>)");
+ }
+
+ @Test
+ public void testTail() throws Exception {
+ compareExpr("tail([1, 2, 3])", "Tail(<<1,2,3>>)");
+ }
+
+}
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index cbe0d5e..9c30e3a 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -9,7 +9,7 @@ import java.util.Hashtable;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.translation.Tla2BTranslator;
+import de.tla2b.old.Tla2BTranslator;
import de.tla2b.types.TLAType;
import de.tla2bAst.Translator;
import tla2sany.semantic.FormalParamNode;
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 4d9e0d0..2314805 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -17,9 +17,9 @@ import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.old.Tla2BTranslator;
import de.tla2b.output.ASTPrettyPrinter;
import de.tla2b.output.Renamer;
-import de.tla2b.translation.Tla2BTranslator;
import de.tla2bAst.Translator;
import tla2sany.semantic.AbortException;
import util.ToolIO;
@@ -38,12 +38,6 @@ public class TestUtil {
public static void runModule(String tlaFile) throws Exception{
Translator t = new Translator(tlaFile);
Start start = t.translate();
- //String printResult = getAstStringofBMachineString(t.getBMachineString());
- //System.out.println(printResult);
- //System.out.println(getTreeAsString(start));
- //BParser.printASTasProlog(System.out, new BParser(), new File("./test.mch"), resultNode, false, true, null);
-
-
System.out.println("-------------------");
ASTPrettyPrinter aP = new ASTPrettyPrinter();
@@ -66,6 +60,21 @@ public class TestUtil {
//System.out.println(t.getBDefinitions().getDefinitionNames());
}
+ public static void compareExpr(String bExpr, String tlaExpr) throws BException{
+ ToolIO.setMode(ToolIO.TOOL);
+ ToolIO.reset();
+ Start resultNode = Translator.translateTlaExpression(tlaExpr);
+ Renamer renamer = new Renamer(resultNode);
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(renamer);
+ resultNode.apply(aP);
+ System.out.println(aP.getResultString());
+ String bAstString = getAstStringofBExpressionString(bExpr);
+ String result = getAstStringofBExpressionString(aP.getResultString());
+ //String tlaAstString = getTreeAsString(resultNode);
+ assertEquals(bAstString, result);
+ }
+
+
public static void compare(String bMachine, String tlaModule) throws BException, TLA2BException{
ToolIO.setMode(ToolIO.TOOL);
String expected = getAstStringofBMachineString(bMachine);
@@ -214,5 +223,16 @@ public class TestUtil {
return string;
}
+ public static String getAstStringofBExpressionString(final String expr)
+ throws BException {
+ final BParser parser = new BParser("testcase");
+ final Start startNode = parser.parse("#FORMULA " + expr, false);
+
+ final Ast2String ast2String = new Ast2String();
+ startNode.apply(ast2String);
+ final String string = ast2String.toString();
+ return string;
+ }
+
}
diff --git a/src/test/resources/regression/Club/Club_tla.mch b/src/test/resources/regression/Club/Club_tla.mch
index 91c6f69..9c82d40 100644
--- a/src/test/resources/regression/Club/Club_tla.mch
+++ b/src/test/resources/regression/Club/Club_tla.mch
@@ -1,4 +1,4 @@
-/*@ generated by TLA2B 1.0.7 Fri May 09 12:45:00 CEST 2014 */
+/*@ generated by TLA2B 1.0.7 Fri May 09 15:38:02 CEST 2014 */
MACHINE Club
SETS ENUM1 = {n1, n2, n3}
ABSTRACT_CONSTANTS capacity, NAME, total
--
GitLab