From 68ef3e40bc3f00fcaea3ff9bef4a9bdbe68bfb5d Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 17 Apr 2015 15:29:35 +0200
Subject: [PATCH] code refactoring
---
.../java/de/tla2b/analysis/BOperation.java | 12 ++-
.../analysis/InstanceTransformation.java | 1 -
.../java/de/tla2b/analysis/SpecAnalyser.java | 76 +++++++++----------
.../java/de/tla2b/analysis/TypeChecker.java | 11 +--
.../de/tla2b/output/ASTPrettyPrinter.java | 2 -
.../tla2b/translation/BDefinitionsFinder.java | 1 -
src/main/java/de/tla2b/types/TLAType.java | 2 -
.../java/de/tla2b/types/TupleOrFunction.java | 12 +--
src/main/java/de/tla2bAst/BAstCreator.java | 12 +--
.../de/tla2bAst/ExpressionTranslator.java | 1 -
.../expression/ModuleAndExpressionTest.java | 3 +-
.../java/de/tla2b/util/TestTypeChecker.java | 1 -
src/test/java/de/tla2b/util/TestUtil.java | 13 +++-
13 files changed, 59 insertions(+), 88 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index fec96cc..f27b3a2 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -185,8 +185,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
if (node instanceof OpApplNode) {
OpApplNode opApplNode = (OpApplNode) node;
if (opApplNode.getOperator().getKind() == BuiltInKind) {
- switch (getOpCode(opApplNode.getOperator().getName())) {
- case OPCODE_eq: {
+
+ if (OPCODE_eq == getOpCode(opApplNode.getOperator()
+ .getName())) {
ExprOrOpArgNode arg1 = opApplNode.getArgs()[0];
try {
OpApplNode arg11 = (OpApplNode) arg1;
@@ -204,12 +205,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
} catch (ClassCastException e) {
-
}
-
- }
- default:
}
+
}
}
}
@@ -263,7 +261,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
beforeAfterPredicates.add(node);
return;
}
- //beforeAfterPredicates.add(node);
+ // beforeAfterPredicates.add(node);
}
private void evalParams() {
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index 3e578c4..c8987c0 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -14,7 +14,6 @@ import tla2sany.semantic.Context;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.InstanceNode;
import tla2sany.semantic.LetInNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.NumeralNode;
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index eebb4d1..7e1a3ab 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -20,7 +20,6 @@ import de.tla2b.global.TranslationGlobals;
import de.tla2b.translation.BDefinitionsFinder;
import de.tla2b.translation.OperationsFinder;
import de.tla2b.translation.UsedDefinitionsFinder;
-import de.tla2b.types.IType;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
@@ -43,8 +42,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
private OpDefNode expressionOpdefNode;
private Hashtable<String, SymbolNode> namingHashTable = new Hashtable<String, SymbolNode>();
-
-
+
private final ModuleNode moduleNode;
private ExprNode nextExpr;
@@ -87,18 +85,16 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
return specAnalyser;
}
-
-
-
- public static SpecAnalyser createSpecAnalyserForTlaExpression(ModuleNode m){
+
+ public static SpecAnalyser createSpecAnalyserForTlaExpression(ModuleNode m) {
SpecAnalyser specAnalyser = new SpecAnalyser(m);
-
- specAnalyser.expressionOpdefNode = m.getOpDefs()[m.getOpDefs().length-1];
+
+ specAnalyser.expressionOpdefNode = m.getOpDefs()[m.getOpDefs().length - 1];
specAnalyser.usedDefinitions.add(specAnalyser.expressionOpdefNode);
specAnalyser.bDefinitionsSet.add(specAnalyser.expressionOpdefNode);
return specAnalyser;
}
-
+
public static SpecAnalyser createSpecAnalyser(ModuleNode m) {
SpecAnalyser specAnalyser = new SpecAnalyser(m);
Hashtable<String, OpDefNode> definitions = new Hashtable<String, OpDefNode>();
@@ -109,7 +105,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
specAnalyser.spec = definitions.get("Spec");
specAnalyser.init = definitions.get("Init");
specAnalyser.next = definitions.get("Next");
- if(definitions.containsKey("Inv")){
+ if (definitions.containsKey("Inv")) {
specAnalyser.invariants.add(definitions.get("Inv"));
}
// TODO are constant in the right order
@@ -132,27 +128,27 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
for (OpDefNode inv : new ArrayList<OpDefNode>(invariants)) {
try {
OpApplNode opApplNode = (OpApplNode) inv.getBody();
-
+
OpDefNode opDefNode = (OpDefNode) opApplNode.getOperator();
-
- if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())){
+
+ if (opDefNode.getKind() == UserDefinedOpKind
+ && !BBuiltInOPs.contains(opDefNode.getName())) {
int i = invariants.indexOf(inv);
invariants.set(i, opDefNode);
- }
+ }
} catch (ClassCastException e) {
}
}
-
-
+
OperationsFinder operationsFinder = new OperationsFinder(this);
bOperations = operationsFinder.getBOperations();
-
+
UsedDefinitionsFinder definitionFinder = new UsedDefinitionsFinder(this);
this.usedDefinitions = definitionFinder.getUsedDefinitions();
-
+
BDefinitionsFinder bDefinitionFinder = new BDefinitionsFinder(this);
this.bDefinitionsSet = bDefinitionFinder.getBDefinitionsSet();
- //usedDefinitions.addAll(bDefinitionsSet);
+ // usedDefinitions.addAll(bDefinitionsSet);
// test whether there is a init predicate if there is a variable
if (moduleNode.getVariableDecls().length > 0 && inits == null) {
@@ -170,9 +166,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
}
findRecursiveConstructs();
-
-
-
+
for (OpDeclNode var : moduleNode.getVariableDecls()) {
namingHashTable.put(var.getName().toString(), var);
}
@@ -182,7 +176,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
for (OpDefNode def : usedDefinitions) {
namingHashTable.put(def.getName().toString(), def);
}
-
+
}
private void evalInit() {
@@ -263,12 +257,12 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
Set<OpDefNode> set = new HashSet<OpDefNode>(usedDefinitions);
for (OpDefNode def : set) {
if (def.getInRecursive()) {
- throw new NotImplementedException("Recursive definitions are currently not supported.");
-// bDefinitionsSet.remove(def);
-// RecursiveDefinition rd = new RecursiveDefinition(def);
-// recursiveDefinitions.add(rd);
- } else
- if (def.getBody() instanceof OpApplNode) {
+ throw new NotImplementedException(
+ "Recursive definitions are currently not supported.");
+ // bDefinitionsSet.remove(def);
+ // RecursiveDefinition rd = new RecursiveDefinition(def);
+ // recursiveDefinitions.add(rd);
+ } else if (def.getBody() instanceof OpApplNode) {
OpApplNode o = (OpApplNode) def.getBody();
switch (getOpCode(o.getOperator().getName())) {
case OPCODE_rfs: { // recursive Function
@@ -297,7 +291,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
public Hashtable<OpDefNode, FormalParamNode[]> getLetParams() {
- return letParams;
+ return new Hashtable<OpDefNode, FormalParamNode[]>(letParams);
}
public ArrayList<String> getDefinitionMacros() {
@@ -320,24 +314,24 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
return this.moduleNode;
}
- public ConfigfileEvaluator getConfigFileEvaluator(){
+ public ConfigfileEvaluator getConfigFileEvaluator() {
return configFileEvaluator;
}
-
- public ArrayList<OpDefNode> getInvariants(){
+
+ public ArrayList<OpDefNode> getInvariants() {
return invariants;
}
-
- public OpDefNode getInitDef(){
+
+ public OpDefNode getInitDef() {
return init;
}
-
- public OpDefNode getExpressionOpdefNode(){
+
+ public OpDefNode getExpressionOpdefNode() {
return expressionOpdefNode;
}
-
- public SymbolNode getSymbolNodeByName(String name){
+
+ public SymbolNode getSymbolNodeByName(String name) {
return namingHashTable.get(name);
}
-
+
}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 48653e2..0132e66 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -45,7 +45,7 @@ import tlc2.tool.BuiltInOPs;
public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TranslationGlobals {
- private final int TEMP_TYPE_ID = 6;
+ private static final int TEMP_TYPE_ID = 6;
private int paramId;
private ArrayList<ExprNode> inits;
@@ -461,14 +461,15 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
TLAType found = ((TLAType) def.getToolObject(TYPE_ID));
- if (found == null){
+ if (found == null) {
found = new UntypedType();
- // throw new RuntimeException(def.getName() + " has no type yet!");
+ // throw new RuntimeException(def.getName() +
+ // " has no type yet!");
}
- if(n.getArgs().length != 0){
+ if (n.getArgs().length != 0) {
found = found.cloneTLAType();
}
-
+
try {
found = found.unify(expected);
} catch (UnificationException e) {
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index 1f89973..829da96 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -13,14 +13,12 @@ import de.be4.classicalb.core.parser.node.AConjunctPredicate;
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.AFirstProjectionExpression;
import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
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.ASecondProjectionExpression;
import de.be4.classicalb.core.parser.node.ASelectSubstitution;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index 4ffc606..93351e8 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -12,7 +12,6 @@ import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.types.IType;
public class BDefinitionsFinder extends AbstractASTVisitor implements
ASTConstants, ToolGlobals, TranslationGlobals {
diff --git a/src/main/java/de/tla2b/types/TLAType.java b/src/main/java/de/tla2b/types/TLAType.java
index 6ea3bde..e403352 100644
--- a/src/main/java/de/tla2b/types/TLAType.java
+++ b/src/main/java/de/tla2b/types/TLAType.java
@@ -2,8 +2,6 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
-import de.tla2b.output.TypeVisitorInterface;
-
public abstract class TLAType implements IType {
private int kind;
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index 07be646..f120eb7 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -204,7 +204,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
public TLAType cloneTLAType() {
TupleOrFunction res = new TupleOrFunction();
for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
- res.types.put(new Integer(entry.getKey().intValue()), entry
+ res.types.put(Integer.valueOf(entry.getKey().intValue()), entry
.getValue().cloneTLAType());
}
return res;
@@ -390,14 +390,4 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
return true;
}
-
- private static boolean allTyped(List<TLAType> typeList) {
- for (int i = 0; i < typeList.size(); i++) {
- if (typeList.get(i).isUntyped()) {
- return false;
- }
- }
- return true;
- }
-
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index f906e99..969fa29 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -94,7 +94,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1]
.getBody();
- System.out.println(expressionIsAPredicate(expr));
if (expressionIsAPredicate(expr)) {
APredicateParseUnit predicateParseUnit = new APredicateParseUnit();
predicateParseUnit.setPredicate(visitExprNodePredicate(expr));
@@ -832,7 +831,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
switch (n.getOperator().getKind()) {
case VariableDeclKind:
case ConstantDeclKind:
- case FormalParamKind: { // TODO
+ case FormalParamKind: {
return new AEqualPredicate(createIdentifierNode(n.getOperator()),
new ABooleanTrueExpression());
}
@@ -1503,7 +1502,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
case OPCODE_fc: // Represents [x \in S |-> e].
case OPCODE_rfs: {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- // ExprNode[] bounds = n.getBdedQuantBounds(); TODO
List<PExpression> idList = new ArrayList<PExpression>();
for (int i = 0; i < params.length; i++) {
for (int j = 0; j < params[i].length; j++) {
@@ -1511,9 +1509,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
idList.add(createIdentifierNode(p));
}
}
-
boolean[] isTuple = n.isBdedQuantATuple();
-
ALambdaExpression lambda = new ALambdaExpression();
List<PExpression> idList2 = new ArrayList<PExpression>();
for (int i = 0; i < params.length; i++) {
@@ -2137,12 +2133,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return list;
}
- private List<PExpression> createIdentifierList(SymbolNode symbolNode) {
- ArrayList<PExpression> list = new ArrayList<PExpression>();
- list.add(createIdentifierNode(getName(symbolNode)));
- return list;
- }
-
private PPredicate visitBuiltInKindPredicate(OpApplNode n) {
switch (getOpCode(n.getOperator().getName())) {
case OPCODE_land: // \land
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index c4da22f..ea33cfb 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -137,7 +137,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
+ "\n" + expr + "\n";
throw new ExpressionTranslationException(message);
}
-
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);
diff --git a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
index 449e378..69e312a 100644
--- a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
@@ -7,11 +7,12 @@ import org.junit.Test;
import de.tla2b.exceptions.TypeErrorException;
public class ModuleAndExpressionTest {
+
@Test
public void testCon() throws Exception {
String module = "---- MODULE Testing ----\n" + "CONSTANTS k \n"
+ "ASSUME k = 4" + "===============";
- compareExprIncludingModel("bool(k = 1)", "k = 1", module);
+ compareExprIncludingModel("k = 1", "k = 1", module);
}
@Test(expected = TypeErrorException.class)
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index 7ecc05c..2dd2c11 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -10,7 +10,6 @@ import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.TLAType;
-import de.tla2b.types.TupleOrFunction;
import de.tla2bAst.Translator;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.ModuleNode;
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 4850e78..a11a4dd 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);
@@ -72,11 +72,16 @@ public class TestUtil {
}
public static void compareExprIncludingModel(String bExpr, String tlaExpr,
- String moduleString) throws TLA2BException {
+ String moduleString) throws TLA2BException, BException {
Translator trans = new Translator(moduleString, null);
trans.translate();
- Start result = trans.translateExpression(tlaExpr);
- // TODO
+ Start resultNode = trans.translateExpression(tlaExpr);
+ Renamer renamer = new Renamer(resultNode);
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
+ resultNode.apply(aP);
+ String bAstString = getAstStringofBExpressionString(bExpr);
+ String result = getAstStringofBExpressionString(aP.getResultString());
+ assertEquals(bAstString, result);
}
public static void compare(String bMachine, String tlaModule)
--
GitLab