From a3b3fb00b5c30570bd3a0a56c1c3c629939e2a7a Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Mon, 23 Sep 2024 17:58:32 +0200
Subject: [PATCH] clarify purpose of expression translate methods
---
src/main/java/de/tla2b/analysis/TypeChecker.java | 1 -
src/main/java/de/tla2bAst/ExpressionTranslator.java | 7 +++----
src/main/java/de/tla2bAst/Translator.java | 7 +++----
src/test/java/de/tla2b/util/TestUtil.java | 4 ++--
4 files changed, 8 insertions(+), 11 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 40c187d..a1d9d4d 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -321,7 +321,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
} catch (UnificationException e) {
throw new TypeErrorException(String.format("Expected %s, found %s at constant '%s',%n%s", expected, c,
con.getName(), n.getLocation())
-
);
}
}
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index 474b8f9..299c571 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -126,15 +126,14 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
return this.expressionStart;
}
- public Start translate() {
- SpecAnalyser specAnalyser = SpecAnalyser
- .createSpecAnalyserForTlaExpression(moduleNode);
+ public Start translateWithoutModel() {
+ SpecAnalyser specAnalyser = SpecAnalyser.createSpecAnalyserForTlaExpression(moduleNode);
TypeChecker tc = new TypeChecker(moduleNode, specAnalyser);
try {
tc.start();
} catch (TLA2BException e) {
String message = "****TypeError****\n" + e.getLocalizedMessage()
- + "\n" + expr + "\n";
+ + "\n" + expr + "\n";
throw new ExpressionTranslationException(message);
}
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index a2937ef..09032dd 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -321,17 +321,16 @@ public class Translator implements TranslationGlobals {
return rml;
}
- public Start translateExpression(String tlaExpression) throws TLA2BException {
+ public Start translateExpressionIncludingModel(String tlaExpression) throws TLA2BException {
ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression, this);
expressionTranslator.parse();
return expressionTranslator.translateIncludingModel();
}
- public static Start translateTlaExpression(String tlaExpression) {
+ public static Start translateExpressionWithoutModel(String tlaExpression) {
ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression);
expressionTranslator.parse();
- expressionTranslator.translate();
- return expressionTranslator.getBExpressionParseUnit();
+ return expressionTranslator.translateWithoutModel();
}
public Definitions getBDefinitions() {
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 81fa3ca..caf9595 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -67,7 +67,7 @@ public class TestUtil {
public static void compareExpr(String bExpr, String tlaExpr) throws BCompoundException {
ToolIO.setMode(ToolIO.TOOL);
ToolIO.reset();
- Start resultNode = Translator.translateTlaExpression(tlaExpr);
+ Start resultNode = Translator.translateExpressionWithoutModel(tlaExpr);
PrettyPrinter pp = new PrettyPrinter();
pp.setRenaming(new SuffixIdentifierRenaming());
resultNode.apply(pp);
@@ -80,7 +80,7 @@ public class TestUtil {
public static void compareExprIncludingModel(String bExpr, String tlaExpr, String moduleString) throws BCompoundException, TLA2BException {
Translator trans = new Translator(moduleString, null);
trans.translate();
- Start resultNode = trans.translateExpression(tlaExpr);
+ Start resultNode = trans.translateExpressionIncludingModel(tlaExpr);
PrettyPrinter pp = new PrettyPrinter();
pp.setRenaming(new SuffixIdentifierRenaming());
resultNode.apply(pp);
--
GitLab