From f464fa63b21884a0732d181ac1246b41b41b3063 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 27 Sep 2024 18:39:16 +0200
Subject: [PATCH] cleanup InstanceTransformation, SymbolSorter and
SymbolRenamer
---
.../analysis/InstanceTransformation.java | 101 +++++++----------
.../java/de/tla2b/analysis/SymbolRenamer.java | 102 ++++++++----------
.../java/de/tla2b/analysis/SymbolSorter.java | 14 +--
.../de/tla2bAst/ExpressionTranslator.java | 19 ++--
src/main/java/de/tla2bAst/Translator.java | 22 ++--
5 files changed, 99 insertions(+), 159 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index a11ae97..b5dccfa 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -9,29 +9,27 @@ import java.util.Hashtable;
public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
- final OpDefNode[] defs;
- final Hashtable<String, OpDefNode> defsHash;
+ private final OpDefNode[] defs;
+ private final Hashtable<String, OpDefNode> defsHash;
private final int substitutionId = 11;
+ private InstanceTransformation(ModuleNode moduleNode) {
+ this.defs = moduleNode.getOpDefs();
+ this.defsHash = SymbolSorter.getDefsHashTable(defs);
+ }
- public InstanceTransformation(ModuleNode moduleNode) {
- defs = moduleNode.getOpDefs();
- defsHash = new Hashtable<>();
- for (OpDefNode def : defs) {
- defsHash.put(def.getName().toString(), def);
- }
+ public static void run(ModuleNode moduleNode) {
+ new InstanceTransformation(moduleNode).start();
}
- public void start() {
+ private void start() {
for (OpDefNode def : defs) {
- if (def.getSource() != def
- && !BBuiltInOPs.contains(def.getSource().getName())) {
+ if (def.getSource() != def && !BBuiltInOPs.contains(def.getSource().getName())) {
// instance
String defName = def.getName().toString();
if (def.getBody() instanceof SubstInNode) {
- String prefix = defName.substring(0,
- defName.lastIndexOf('!') + 1);
+ String prefix = defName.substring(0, defName.lastIndexOf('!') + 1);
def.setParams(generateNewParams(def.getParams()));
ExprNode body;
try {
@@ -45,17 +43,15 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
}
- private ExprOrOpArgNode generateNewExprOrOpArgNode(ExprOrOpArgNode n,
- String prefix) throws AbortException {
+ private ExprOrOpArgNode generateNewExprOrOpArgNode(ExprOrOpArgNode n, String prefix) throws AbortException {
if (n instanceof ExprNode) {
return generateNewExprNode((ExprNode) n, prefix);
} else {
- throw new RuntimeException("OpArgNode not implemented jet");
+ throw new RuntimeException("OpArgNode not implemented yet");
}
}
- private ExprNode generateNewExprNode(ExprNode n, String prefix)
- throws AbortException {
+ private ExprNode generateNewExprNode(ExprNode n, String prefix) throws AbortException {
switch (n.getKind()) {
case OpApplKind: {
return generateNewOpApplNode((OpApplNode) n, prefix);
@@ -93,11 +89,9 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
case AtNodeKind: { // @
AtNode old = (AtNode) n;
OpApplNode oldExcept = old.getExceptRef();
- OpApplNode newExcept = (OpApplNode) oldExcept
- .getToolObject(substitutionId);
+ OpApplNode newExcept = (OpApplNode) oldExcept.getToolObject(substitutionId);
OpApplNode oldComponent = old.getExceptComponentRef();
- OpApplNode newComponent = (OpApplNode) oldComponent
- .getToolObject(substitutionId);
+ OpApplNode newComponent = (OpApplNode) oldComponent.getToolObject(substitutionId);
return new AtNode(newExcept, newComponent);
}
@@ -107,8 +101,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
Context cc = oldLetNode.context;
for (int i = 0; i < oldLetNode.getLets().length; i++) {
OpDefNode let = oldLetNode.getLets()[i];
- UniqueString newName = UniqueString.uniqueStringOf(prefix
- + let.getName().toString());
+ UniqueString newName = UniqueString.uniqueStringOf(prefix + let.getName().toString());
OpDefNode newLet = new OpDefNode(newName, let.getKind(),
generateNewParams(let.getParams()), let.isLocal(),
generateNewExprNode(let.getBody(), prefix),
@@ -119,23 +112,19 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
cc.addSymbolToContext(newName, newLet);
}
- LetInNode newLetNode = new LetInNode(oldLetNode.getTreeNode(),
+ return new LetInNode(oldLetNode.getTreeNode(),
newLets, null, generateNewExprNode(oldLetNode.getBody(),
prefix), cc);
- return newLetNode;
}
-
}
throw new RuntimeException();
}
- private ExprNode generateNewOpApplNode(OpApplNode n, String prefix)
- throws AbortException {
+ private ExprNode generateNewOpApplNode(OpApplNode n, String prefix) throws AbortException {
switch (n.getOperator().getKind()) {
case VariableDeclKind:
case ConstantDeclKind: {
- ExprOrOpArgNode e = (ExprOrOpArgNode) n.getOperator()
- .getToolObject(substitutionId);
+ ExprOrOpArgNode e = (ExprOrOpArgNode) n.getOperator().getToolObject(substitutionId);
if (e != null) {
if (e instanceof ExprNode) {
// TODO newprefix, witout last prefix
@@ -143,8 +132,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
} else {
OpArgNode opArg = (OpArgNode) e;
while (opArg.getOp().getToolObject(substitutionId) != null) {
- opArg = (OpArgNode) opArg.getOp().getToolObject(
- substitutionId);
+ opArg = (OpArgNode) opArg.getOp().getToolObject(substitutionId);
}
return new OpApplNode(opArg.getOp(), generateNewArgs(
n.getArgs(), prefix), n.getTreeNode(), null);
@@ -161,8 +149,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
if (f == null) {
throw new RuntimeException();
}
- return new OpApplNode(f, generateNewArgs(n.getArgs(), prefix),
- n.getTreeNode(), null);
+ return new OpApplNode(f, generateNewArgs(n.getArgs(), prefix), n.getTreeNode(), null);
}
case BuiltInKind: {
@@ -171,17 +158,14 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
case UserDefinedOpKind: {
// in case of a call of a LetInNode
- OpDefNode letOp = (OpDefNode) n.getOperator().getToolObject(
- substitutionId);
+ OpDefNode letOp = (OpDefNode) n.getOperator().getToolObject(substitutionId);
if (letOp != null) {
- return new OpApplNode(letOp, generateNewArgs(n.getArgs(),
- prefix), n.getTreeNode(), null);
+ return new OpApplNode(letOp, generateNewArgs(n.getArgs(), prefix), n.getTreeNode(), null);
}
// in case of a call of BBuiltInOp e.g. +, -
if (BBuiltInOPs.contains(n.getOperator().getName())) {
- return new OpApplNode(n.getOperator(), generateNewArgs(
- n.getArgs(), prefix), n.stn, null);
+ return new OpApplNode(n.getOperator(), generateNewArgs(n.getArgs(), prefix), n.stn, null);
}
// normal userdefined Operator
@@ -190,28 +174,23 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
if (op == null) {
throw new RuntimeException();
}
- return new OpApplNode(op, generateNewArgs(n.getArgs(),
- prefix), n.getTreeNode(), null);
+ return new OpApplNode(op, generateNewArgs(n.getArgs(), prefix), n.getTreeNode(), null);
}
}
- throw new RuntimeException("OpApplkind not implemented jet");
+ throw new RuntimeException("OpApplkind not implemented yet");
}
- private ExprNode generateNewBuiltInNode(OpApplNode n, String prefix)
- throws AbortException {
+ private ExprNode generateNewBuiltInNode(OpApplNode n, String prefix) throws AbortException {
switch (getOpCode(n.getOperator().getName())) {
-
case OPCODE_exc: { // Except
- OpApplNode newNode = new OpApplNode(n.getOperator().getName(),
- null, n.getTreeNode(), null);
+ OpApplNode newNode = new OpApplNode(n.getOperator().getName(), null, n.getTreeNode(), null);
n.setToolObject(substitutionId, newNode); // needed for @ node
ExprOrOpArgNode[] newArgs = new ExprOrOpArgNode[n.getArgs().length];
newArgs[0] = generateNewExprOrOpArgNode(n.getArgs()[0], prefix);
for (int i = 1; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
- OpApplNode newPair = new OpApplNode(pair.getOperator()
- .getName(), null, pair.getTreeNode(), null);
+ OpApplNode newPair = new OpApplNode(pair.getOperator().getName(), null, pair.getTreeNode(), null);
// needed for @ node: we have to set a reference from the old
// pair to the new pair
// before evaluation the arguments which may be contains a @
@@ -233,10 +212,9 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
f.getTreeNode(), null, null);
f.setToolObject(substitutionId, newSymbols[i]);
}
- OpApplNode newNode = new OpApplNode(n.getOperator().getName(),
+ return new OpApplNode(n.getOperator().getName(),
newSymbols, generateNewArgs(n.getArgs(), prefix), null,
null, null, n.getTreeNode(), null);
- return newNode;
}
case OPCODE_rfs:
@@ -255,8 +233,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
FormalParamNode[] temp = new FormalParamNode[oldParams[i].length];
for (int j = 0; j < oldParams[i].length; j++) {
FormalParamNode f = oldParams[i][j];
- temp[j] = new FormalParamNode(f.getName(), f.getArity(),
- f.getTreeNode(), null, null);
+ temp[j] = new FormalParamNode(f.getName(), f.getArity(), f.getTreeNode(), null, null);
// set reference the old param to the new
f.setToolObject(substitutionId, temp[j]);
}
@@ -266,25 +243,20 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
// new ranges
ExprNode[] ranges = new ExprNode[n.getBdedQuantBounds().length];
for (int i = 0; i < n.getBdedQuantBounds().length; i++) {
- ranges[i] = generateNewExprNode(n.getBdedQuantBounds()[i],
- prefix);
+ ranges[i] = generateNewExprNode(n.getBdedQuantBounds()[i], prefix);
}
- OpApplNode newNode = new OpApplNode(n.getOperator().getName(),
+ return new OpApplNode(n.getOperator().getName(),
null, generateNewArgs(n.getArgs(), prefix), newParams,
n.isBdedQuantATuple(), ranges, n.getTreeNode(), null);
- return newNode;
}
default: { // =
- OpApplNode newNode = new OpApplNode(n.getOperator(),
- generateNewArgs(n.getArgs(), prefix), n.getTreeNode(), null);
- return newNode;
+ return new OpApplNode(n.getOperator(), generateNewArgs(n.getArgs(), prefix), n.getTreeNode(), null);
}
}
}
- private ExprOrOpArgNode[] generateNewArgs(ExprOrOpArgNode[] args,
- String prefix) throws AbortException {
+ private ExprOrOpArgNode[] generateNewArgs(ExprOrOpArgNode[] args, String prefix) throws AbortException {
ExprOrOpArgNode[] res = new ExprOrOpArgNode[args.length];
for (int i = 0; i < args.length; i++) {
res[i] = generateNewExprOrOpArgNode(args[i], prefix);
@@ -304,5 +276,4 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
return newParams;
}
-
}
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index 22c13bc..8d1c8e8 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -1,6 +1,5 @@
package de.tla2b.analysis;
-
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import tla2sany.semantic.*;
@@ -10,8 +9,7 @@ import java.util.HashSet;
import java.util.Hashtable;
import java.util.Set;
-public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
- ASTConstants {
+public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, ASTConstants {
private final static Set<String> KEYWORDS = new HashSet<>();
@@ -114,56 +112,57 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
private final Set<String> globalNames = new HashSet<>();
private final Hashtable<OpDefNode, Set<String>> usedNamesTable = new Hashtable<>();
- public SymbolRenamer(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
+ private SymbolRenamer(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
this.usedDefinitions = specAnalyser.getUsedDefinitions();
}
- public SymbolRenamer(ModuleNode moduleNode) {
+ private SymbolRenamer(ModuleNode moduleNode) {
this.moduleNode = moduleNode;
- usedDefinitions = new HashSet<>();
+ this.usedDefinitions = new HashSet<>();
OpDefNode[] defs = moduleNode.getOpDefs();
- usedDefinitions.add(defs[defs.length - 1]);
+ this.usedDefinitions.add(defs[defs.length - 1]);
+ }
+
+ public static void run(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
+ new SymbolRenamer(moduleNode, specAnalyser).start();
}
- public void start() {
+ public static void run(ModuleNode moduleNode) {
+ new SymbolRenamer(moduleNode).start();
+ }
+
+ private void start() {
// Variables
- for (int i = 0; i < moduleNode.getVariableDecls().length; i++) {
- OpDeclNode v = moduleNode.getVariableDecls()[i];
- String newName = incName(v.getName().toString());
+ for (OpDeclNode node : moduleNode.getVariableDecls()) {
+ String newName = incName(node.getName().toString());
globalNames.add(newName);
- v.setToolObject(NEW_NAME, newName);
+ node.setToolObject(NEW_NAME, newName);
}
// constants
- for (int i = 0; i < moduleNode.getConstantDecls().length; i++) {
- OpDeclNode c = moduleNode.getConstantDecls()[i];
- String newName = incName(c.getName().toString());
+ for(OpDeclNode node : moduleNode.getConstantDecls()) {
+ String newName = incName(node.getName().toString());
globalNames.add(newName);
- c.setToolObject(NEW_NAME, newName);
+ node.setToolObject(NEW_NAME, newName);
}
- for (int i = 0; i < moduleNode.getOpDefs().length; i++) {
- OpDefNode def = moduleNode.getOpDefs()[i];
- String newName = getOperatorName(def);
+ for(OpDefNode node : moduleNode.getOpDefs()) {
+ String newName = getOperatorName(node);
globalNames.add(newName);
- def.setToolObject(NEW_NAME, newName);
- usedNamesTable.put(def, new HashSet<>());
+ node.setToolObject(NEW_NAME, newName);
+ usedNamesTable.put(node, new HashSet<>());
}
- for (int i = 0; i < moduleNode.getAssumptions().length; i++) {
- AssumeNode assumeNode = moduleNode.getAssumptions()[i];
- visitNode(assumeNode.getAssume(), new HashSet<>());
+ for(AssumeNode node : moduleNode.getAssumptions()) {
+ visitNode(node.getAssume(), new HashSet<>());
}
for (int i = moduleNode.getOpDefs().length - 1; i >= 0; i--) {
OpDefNode def = moduleNode.getOpDefs()[i];
Set<String> usedNames = usedNamesTable.get(def);
- for (int j = 0; j < def.getParams().length; j++) {
- FormalParamNode p = def.getParams()[j];
- String paramName = p.getName().toString();
- String newParamName = incName(paramName);
- p.setToolObject(NEW_NAME, newParamName);
+ for (FormalParamNode node : def.getParams()) {
+ node.setToolObject(NEW_NAME, incName(node.getName().toString()));
//Parameter of different definitions calling each other can have the same name
//usedNames.add(newParamName);
}
@@ -176,13 +175,11 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
// System.out.println(n.toString(1)+ " "+ n.getKind());
switch (n.getKind()) {
-
case LetInKind: {
LetInNode letInNode = (LetInNode) n;
OpDefNode[] defs = letInNode.getLets();
- // Initialize all local definitions (get a new name, get an empty
- // list)
+ // Initialize all local definitions (get a new name, get an empty list)
for (OpDefNode def : defs) {
String newName = getOperatorName(def);
globalNames.add(newName);
@@ -197,11 +194,8 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
for (int i = defs.length - 1; i >= 0; i--) {
OpDefNode def = defs[i];
Set<String> usedNamesOfDef = usedNamesTable.get(def);
- for (int j = 0; j < def.getParams().length; j++) {
- FormalParamNode p = def.getParams()[j];
- String paramName = p.getName().toString();
- String newParamName = incName(paramName);
- p.setToolObject(NEW_NAME, newParamName);
+ for (FormalParamNode node : def.getParams()) {
+ node.setToolObject(NEW_NAME, incName(node.getName().toString()));
//usedNamesOfDef.add(newParamName);
}
visitNode(def.getBody(), usedNamesOfDef);
@@ -212,7 +206,6 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
case OpApplKind: {
OpApplNode opApplNode = (OpApplNode) n;
switch (opApplNode.getOperator().getKind()) {
-
case BuiltInKind: {
visitBuiltinNode(opApplNode, usedNames);
return;
@@ -228,24 +221,23 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
usedNamesTable.get(def).addAll(usedNames);
}
-
- for (int i = 0; i < n.getChildren().length; i++) {
- visitNode(opApplNode.getArgs()[i], usedNames);
+ for (SemanticNode node : n.getChildren()) {
+ visitNode(node, usedNames);
}
return;
}
}
- for (int i = 0; i < opApplNode.getArgs().length; i++) {
- visitNode(opApplNode.getArgs()[i], usedNames);
+ for (ExprOrOpArgNode node : opApplNode.getArgs()) {
+ visitNode(node, usedNames);
}
return;
}
}
if (n.getChildren() != null) {
- for (int i = 0; i < n.getChildren().length; i++) {
- visitNode(n.getChildren()[i], usedNames);
+ for (SemanticNode node : n.getChildren()) {
+ visitNode(node, usedNames);
}
}
}
@@ -266,28 +258,25 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
Set<String> newUsedNames = new HashSet<>(usedNames);
for (FormalParamNode[] formalParamNodes : params) {
for (FormalParamNode param : formalParamNodes) {
- String paramName = param.getName().toString();
- String newName = incName(paramName, usedNames);
+ String newName = incName(param.getName().toString(), usedNames);
param.setToolObject(NEW_NAME, newName);
newUsedNames.add(newName);
}
}
- for (int i = 0; i < opApplNode.getBdedQuantBounds().length; i++) {
- visitNode(opApplNode.getBdedQuantBounds()[i], usedNames);
+ for (ExprNode node : opApplNode.getBdedQuantBounds()) {
+ visitNode(node, usedNames);
}
visitNode(opApplNode.getArgs()[0], newUsedNames);
-
return;
}
default:
- for (int i = 0; i < opApplNode.getArgs().length; i++) {
- if (opApplNode.getArgs()[i] != null) {
- visitNode(opApplNode.getArgs()[i], usedNames);
+ for (ExprOrOpArgNode node : opApplNode.getArgs()) {
+ if (node != null) {
+ visitNode(node, usedNames);
}
}
-
}
}
@@ -295,9 +284,8 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
String newName = def.getName().toString();
if (BBUILTIN_OPERATOR.containsKey(newName)) {
- // a B built-in operator is defined outside of a standard module
- if (!STANDARD_MODULES.contains(def.getSource()
- .getOriginallyDefinedInModuleNode().getName().toString())) {
+ // a B built-in operator is defined outside a standard module
+ if (!STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
return incName(BBUILTIN_OPERATOR.get(newName));
}
}
diff --git a/src/main/java/de/tla2b/analysis/SymbolSorter.java b/src/main/java/de/tla2b/analysis/SymbolSorter.java
index 34b4616..b457ac9 100644
--- a/src/main/java/de/tla2b/analysis/SymbolSorter.java
+++ b/src/main/java/de/tla2b/analysis/SymbolSorter.java
@@ -9,19 +9,14 @@ import java.util.Comparator;
import java.util.Hashtable;
public class SymbolSorter {
- private final ModuleNode moduleNode;
- public SymbolSorter(ModuleNode moduleNode) {
- this.moduleNode = moduleNode;
- }
-
- public void sort() {
+ public static void sort(ModuleNode moduleNode) {
// sort constants
- Arrays.sort(moduleNode.getConstantDecls(), new OpDeclNodeComparator());
+ sortDeclNodes(moduleNode.getConstantDecls());
// sort variables
- Arrays.sort(moduleNode.getVariableDecls(), new OpDeclNodeComparator());
+ sortDeclNodes(moduleNode.getVariableDecls());
// sort definitions
- Arrays.sort(moduleNode.getOpDefs(), new OpDefNodeComparator());
+ sortOpDefNodes(moduleNode.getOpDefs());
}
public static void sortDeclNodes(OpDeclNode[] opDeclNodes) {
@@ -47,7 +42,6 @@ public class SymbolSorter {
}
return definitions;
}
-
}
class OpDeclNodeComparator implements Comparator<OpDeclNode> {
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index 64233b1..35f6460 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -132,8 +132,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
String message = "****TypeError****\n" + e.getLocalizedMessage() + "\n" + expr + "\n";
throw new ExpressionTranslationException(message);
}
- SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
- symRenamer.start();
+ SymbolRenamer.run(moduleNode, specAnalyser);
BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);
this.expressionStart = bASTCreator.expressionStart;
@@ -150,8 +149,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
+ "\n" + expr + "\n";
throw new ExpressionTranslationException(message);
}
- SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
- symRenamer.start();
+ SymbolRenamer.run(moduleNode, specAnalyser);
BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);
this.expressionStart = bASTCreator.expressionStart;
@@ -165,19 +163,16 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
SANY.frontEndMain(spec, moduleName, ToolIO.out);
} catch (FrontEndException e) {
// Error in Frontend, should never happen
- throw new de.tla2b.exceptions.FrontEndException(
- "Frontend error! This should never happen.", spec);
+ throw new de.tla2b.exceptions.FrontEndException("Frontend error! This should never happen.", spec);
}
if (spec.parseErrors.isFailure()) {
- String message = module + "\n\n" + spec.parseErrors;
- message += allMessagesToString(ToolIO.getAllMessages());
+ String message = module + "\n\n" + spec.parseErrors + allMessagesToString(ToolIO.getAllMessages());
throw new de.tla2b.exceptions.FrontEndException(message, spec);
}
if (spec.semanticErrors.isFailure()) {
- String message = module + "\n\n" + spec.semanticErrors;
- message += allMessagesToString(ToolIO.getAllMessages());
+ String message = module + "\n\n" + spec.semanticErrors + allMessagesToString(ToolIO.getAllMessages());
throw new de.tla2b.exceptions.FrontEndException(message, spec);
}
@@ -185,9 +180,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
ModuleNode n = spec.getExternalModuleTable().rootModule;
if (spec.getInitErrors().isFailure()) {
System.err.println(spec.getInitErrors());
- throw new de.tla2b.exceptions.FrontEndException(
-
- allMessagesToString(ToolIO.getAllMessages()), spec);
+ throw new de.tla2b.exceptions.FrontEndException(allMessagesToString(ToolIO.getAllMessages()), spec);
}
if (n == null) { // Parse Error
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 09032dd..187cfc6 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -198,16 +198,11 @@ public class Translator implements TranslationGlobals {
}
public Start translate() throws TLA2BException {
- InstanceTransformation trans = new InstanceTransformation(moduleNode);
- trans.start();
-
- SymbolSorter symbolSorter = new SymbolSorter(moduleNode);
- symbolSorter.sort();
- PredicateVsExpression predicateVsExpression = new PredicateVsExpression(moduleNode);
+ InstanceTransformation.run(moduleNode);
+ SymbolSorter.sort(moduleNode);
ConfigfileEvaluator conEval = null;
if (modelConfig != null) {
-
conEval = new ConfigfileEvaluator(modelConfig, moduleNode);
conEval.start();
@@ -220,13 +215,12 @@ public class Translator implements TranslationGlobals {
specAnalyser.start();
typechecker = new TypeChecker(moduleNode, conEval, specAnalyser);
typechecker.start();
- SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
- symRenamer.start();
- UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(moduleNode, specAnalyser);
- RecursiveFunctionHandler recursiveFunctionHandler = new RecursiveFunctionHandler(specAnalyser);
- BMacroHandler bMacroHandler = new BMacroHandler(specAnalyser, conEval);
- bAstCreator = new BAstCreator(moduleNode, conEval, specAnalyser, usedExternalFunctions, predicateVsExpression,
- bMacroHandler, recursiveFunctionHandler);
+ SymbolRenamer.run(moduleNode, specAnalyser);
+ bAstCreator = new BAstCreator(moduleNode, conEval, specAnalyser,
+ new UsedExternalFunctions(moduleNode, specAnalyser),
+ new PredicateVsExpression(moduleNode),
+ new BMacroHandler(specAnalyser, conEval),
+ new RecursiveFunctionHandler(specAnalyser));
this.BAst = bAstCreator.getStartNode();
this.typeTable = bAstCreator.getTypeTable();
--
GitLab