Skip to content
Snippets Groups Projects
Commit a3b3fb00 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

clarify purpose of expression translate methods

parent 7cc91f59
No related branches found
No related tags found
No related merge requests found
...@@ -321,7 +321,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns, ...@@ -321,7 +321,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
} catch (UnificationException e) { } catch (UnificationException e) {
throw new TypeErrorException(String.format("Expected %s, found %s at constant '%s',%n%s", expected, c, throw new TypeErrorException(String.format("Expected %s, found %s at constant '%s',%n%s", expected, c,
con.getName(), n.getLocation()) con.getName(), n.getLocation())
); );
} }
} }
......
...@@ -126,9 +126,8 @@ public class ExpressionTranslator implements SyntaxTreeConstants { ...@@ -126,9 +126,8 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
return this.expressionStart; return this.expressionStart;
} }
public Start translate() { public Start translateWithoutModel() {
SpecAnalyser specAnalyser = SpecAnalyser SpecAnalyser specAnalyser = SpecAnalyser.createSpecAnalyserForTlaExpression(moduleNode);
.createSpecAnalyserForTlaExpression(moduleNode);
TypeChecker tc = new TypeChecker(moduleNode, specAnalyser); TypeChecker tc = new TypeChecker(moduleNode, specAnalyser);
try { try {
tc.start(); tc.start();
......
...@@ -321,17 +321,16 @@ public class Translator implements TranslationGlobals { ...@@ -321,17 +321,16 @@ public class Translator implements TranslationGlobals {
return rml; return rml;
} }
public Start translateExpression(String tlaExpression) throws TLA2BException { public Start translateExpressionIncludingModel(String tlaExpression) throws TLA2BException {
ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression, this); ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression, this);
expressionTranslator.parse(); expressionTranslator.parse();
return expressionTranslator.translateIncludingModel(); return expressionTranslator.translateIncludingModel();
} }
public static Start translateTlaExpression(String tlaExpression) { public static Start translateExpressionWithoutModel(String tlaExpression) {
ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression); ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression);
expressionTranslator.parse(); expressionTranslator.parse();
expressionTranslator.translate(); return expressionTranslator.translateWithoutModel();
return expressionTranslator.getBExpressionParseUnit();
} }
public Definitions getBDefinitions() { public Definitions getBDefinitions() {
......
...@@ -67,7 +67,7 @@ public class TestUtil { ...@@ -67,7 +67,7 @@ public class TestUtil {
public static void compareExpr(String bExpr, String tlaExpr) throws BCompoundException { public static void compareExpr(String bExpr, String tlaExpr) throws BCompoundException {
ToolIO.setMode(ToolIO.TOOL); ToolIO.setMode(ToolIO.TOOL);
ToolIO.reset(); ToolIO.reset();
Start resultNode = Translator.translateTlaExpression(tlaExpr); Start resultNode = Translator.translateExpressionWithoutModel(tlaExpr);
PrettyPrinter pp = new PrettyPrinter(); PrettyPrinter pp = new PrettyPrinter();
pp.setRenaming(new SuffixIdentifierRenaming()); pp.setRenaming(new SuffixIdentifierRenaming());
resultNode.apply(pp); resultNode.apply(pp);
...@@ -80,7 +80,7 @@ public class TestUtil { ...@@ -80,7 +80,7 @@ public class TestUtil {
public static void compareExprIncludingModel(String bExpr, String tlaExpr, String moduleString) throws BCompoundException, TLA2BException { public static void compareExprIncludingModel(String bExpr, String tlaExpr, String moduleString) throws BCompoundException, TLA2BException {
Translator trans = new Translator(moduleString, null); Translator trans = new Translator(moduleString, null);
trans.translate(); trans.translate();
Start resultNode = trans.translateExpression(tlaExpr); Start resultNode = trans.translateExpressionIncludingModel(tlaExpr);
PrettyPrinter pp = new PrettyPrinter(); PrettyPrinter pp = new PrettyPrinter();
pp.setRenaming(new SuffixIdentifierRenaming()); pp.setRenaming(new SuffixIdentifierRenaming());
resultNode.apply(pp); resultNode.apply(pp);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment