From 160304cc02f9b3c196938ac24b7f06a484375d82 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 26 Apr 2023 00:00:27 +0200
Subject: [PATCH] Replace ASTPrettyPrinter and Renamer with B parser
PrettyPrinter
---
.../de/tla2b/output/ASTPrettyPrinter.java | 6 ++++
src/main/java/de/tla2b/output/Renamer.java | 7 +++-
src/main/java/de/tla2bAst/Translator.java | 26 +++++++-------
src/test/java/de/tla2b/util/TestUtil.java | 36 ++++++++++---------
src/test/java/testing/ExampleFilesTest.java | 18 +++++-----
5 files changed, 55 insertions(+), 38 deletions(-)
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index 5ad97b0..a2cf80c 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -6,8 +6,13 @@ import java.util.Iterator;
import java.util.List;
import de.be4.classicalb.core.parser.node.*;
+import de.be4.classicalb.core.parser.util.PrettyPrinter;
import de.tla2b.util.ExtendedDFAdapter;
+/**
+ * @deprecated Use {@link PrettyPrinter} from the B parser library instead.
+ */
+@Deprecated
public class ASTPrettyPrinter extends ExtendedDFAdapter {
private final StringBuilder sb = new StringBuilder();
private Renamer renamer;
@@ -726,6 +731,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
}
+@Deprecated
class PrettyPrintNode {
private String begin = "";
private String beginList = "";
diff --git a/src/main/java/de/tla2b/output/Renamer.java b/src/main/java/de/tla2b/output/Renamer.java
index 1e768d7..2f55f7e 100644
--- a/src/main/java/de/tla2b/output/Renamer.java
+++ b/src/main/java/de/tla2b/output/Renamer.java
@@ -4,13 +4,18 @@ import java.util.HashMap;
import java.util.HashSet;
import java.util.Set;
-import de.be4.classicalb.core.parser.util.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.be4.classicalb.core.parser.util.SuffixIdentifierRenaming;
+import de.be4.classicalb.core.parser.util.Utils;
+/**
+ * @deprecated Use {@link SuffixIdentifierRenaming} from the B parser library instead.
+ */
+@Deprecated
public class Renamer extends DepthFirstAdapter {
private final HashMap<Node, String> namesTables;
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index df6ee71..ef24f2d 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -20,6 +20,8 @@ import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.exceptions.PreParseException;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.util.PrettyPrinter;
+import de.be4.classicalb.core.parser.util.SuffixIdentifierRenaming;
import de.tla2b.analysis.InstanceTransformation;
import de.tla2b.analysis.PredicateVsExpression;
import de.tla2b.analysis.SpecAnalyser;
@@ -32,17 +34,18 @@ import de.tla2b.config.ModuleOverrider;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.output.ASTPrettyPrinter;
import de.tla2b.output.PrologPrinter;
-import de.tla2b.output.Renamer;
import de.tla2b.translation.BMacroHandler;
import de.tla2b.translation.RecursiveFunctionHandler;
import de.tla2b.types.TLAType;
import de.tla2b.util.FileUtils;
+
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.ModuleNode;
+
import tlc2.tool.ModelConfig;
+
import util.ToolIO;
public class Translator implements TranslationGlobals {
@@ -100,10 +103,10 @@ public class Translator implements TranslationGlobals {
throws TLA2BException {
Translator translator = new Translator(moduleName, moduleString, configString);
Start bAST = translator.getBAST();
- Renamer renamer = new Renamer(bAST);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(bAST, renamer);
- bAST.apply(aP);
- return aP.getResultString();
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ bAST.apply(pp);
+ return pp.getPrettyPrint();
}
public Translator(String moduleName, String moduleString, String configString) throws TLA2BException {
@@ -317,16 +320,15 @@ public class Translator implements TranslationGlobals {
System.exit(-1);
}
- Renamer renamer = new Renamer(BAst);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(BAst, renamer);
- BAst.apply(aP);
- StringBuilder result = aP.getResultAsStringbuilder();
- result.insert(0, "/*@ generated by TLA2B " + VERSION_NUMBER + " " + new Date() + " */\n");
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ BAst.apply(pp);
+ String result = "/*@ generated by TLA2B " + VERSION_NUMBER + " " + new Date() + " */\n" + pp.getPrettyPrint();
try {
BufferedWriter out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(machineFile), "UTF-8"));
try {
- out.write(result.toString());
+ out.write(result);
} finally {
out.close();
}
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 4007828..4ba66b4 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -5,10 +5,10 @@ import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.util.PrettyPrinter;
+import de.be4.classicalb.core.parser.util.SuffixIdentifierRenaming;
import de.prob.prolog.output.PrologTermStringOutput;
import de.tla2b.exceptions.TLA2BException;
-import de.tla2b.output.ASTPrettyPrinter;
-import de.tla2b.output.Renamer;
import de.tla2bAst.Translator;
import util.FileUtil;
@@ -27,10 +27,12 @@ public class TestUtil {
Translator t = new Translator(tlaFile);
Start start = t.translate();
- ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
- start.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ // FIXME Is it intentional that we don't use SuffixIdentifierRenaming here?
+ start.apply(pp);
+ System.out.println(pp.getPrettyPrint());
final BParser parser = new BParser("testcase");
- final Start ppStart = parser.parse(aP.getResultString(), false);
+ final Start ppStart = parser.parse(pp.getPrettyPrint(), false);
String result = getTreeAsString(start);
String ppResult = getTreeAsString(ppStart);
@@ -43,11 +45,11 @@ public class TestUtil {
ToolIO.setMode(ToolIO.TOOL);
ToolIO.reset();
Start resultNode = Translator.translateTlaExpression(tlaExpr);
- Renamer renamer = new Renamer(resultNode);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
- resultNode.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ resultNode.apply(pp);
String bAstString = getAstStringofBExpressionString(bExpr);
- String result = getAstStringofBExpressionString(aP.getResultString());
+ String result = getAstStringofBExpressionString(pp.getPrettyPrint());
// String tlaAstString = getTreeAsString(resultNode);
assertEquals(bAstString, result);
}
@@ -56,11 +58,11 @@ public class TestUtil {
Translator trans = new Translator(moduleString, null);
trans.translate();
Start resultNode = trans.translateExpression(tlaExpr);
- Renamer renamer = new Renamer(resultNode);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
- resultNode.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ resultNode.apply(pp);
String bAstString = getAstStringofBExpressionString(bExpr);
- String result = getAstStringofBExpressionString(aP.getResultString());
+ String result = getAstStringofBExpressionString(pp.getPrettyPrint());
assertEquals(bAstString, result);
}
@@ -94,11 +96,11 @@ public class TestUtil {
public static void renamerTest(String tlaFile) throws BCompoundException, TLA2BException {
Translator t = new Translator(tlaFile);
Start start = t.translate();
- Renamer renamer = new Renamer(start);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(start, renamer);
- start.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ start.apply(pp);
final BParser parser = new BParser("testcase");
- parser.parse(aP.getResultString(), false);
+ parser.parse(pp.getPrettyPrint(), false);
}
public static TestTypeChecker typeCheckString(String moduleString) throws TLA2BException {
diff --git a/src/test/java/testing/ExampleFilesTest.java b/src/test/java/testing/ExampleFilesTest.java
index 241befa..ad2dfc1 100644
--- a/src/test/java/testing/ExampleFilesTest.java
+++ b/src/test/java/testing/ExampleFilesTest.java
@@ -3,19 +3,20 @@ package testing;
import java.io.File;
import java.util.ArrayList;
-import org.junit.Test;
-import org.junit.runner.RunWith;
-
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.node.Start;
-import de.tla2b.output.ASTPrettyPrinter;
+import de.be4.classicalb.core.parser.util.PrettyPrinter;
import de.tla2b.util.AbstractParseModuleTest;
import de.tla2b.util.FileUtils;
import de.tla2b.util.PolySuite;
-import de.tla2b.util.TestUtil;
import de.tla2b.util.PolySuite.Config;
import de.tla2b.util.PolySuite.Configuration;
+import de.tla2b.util.TestUtil;
import de.tla2bAst.Translator;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
import static org.junit.Assert.assertEquals;
@RunWith(PolySuite.class)
@@ -35,12 +36,13 @@ public class ExampleFilesTest extends AbstractParseModuleTest {
Start start = t.translate();
String resultTree = TestUtil.getTreeAsString(start);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
- start.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ // FIXME Is it intentional that we don't use SuffixIdentifierRenaming here?
+ start.apply(pp);
// parse pretty print result
final BParser parser = new BParser("testcase");
- final Start ppStart = parser.parse(aP.getResultString(), false);
+ final Start ppStart = parser.parse(pp.getPrettyPrint(), false);
String ppTree = TestUtil.getTreeAsString(ppStart);
// comparing result with pretty print
--
GitLab