diff --git a/src/main/java/de/tla2b/output/PrologPrinter.java b/src/main/java/de/tla2b/output/PrologPrinter.java
deleted file mode 100644
index b26fd25780d4cc4b641535303bd7ef3f1dec262f..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/output/PrologPrinter.java
+++ /dev/null
@@ -1,89 +0,0 @@
-package de.tla2b.output;
-
-import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
-import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
-import de.be4.classicalb.core.parser.node.Node;
-import de.be4.classicalb.core.parser.node.Start;
-import de.hhu.stups.sablecc.patch.PositionedNode;
-import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.output.PrologTermOutput;
-import de.tla2b.types.TLAType;
-
-import java.io.File;
-import java.io.IOException;
-import java.io.PrintWriter;
-import java.util.*;
-
-public class PrologPrinter {
- final RecursiveMachineLoader rml;
- final BParser bParser;
- final String moduleName;
-
- //private final Map<String, SourcePositions> positions = new HashMap<String, SourcePositions>();
- private HashSet<PositionedNode> positions;
- private final List<File> files = new ArrayList<>();
- private final Hashtable<Node, TLAType> typeTable;
-
- public PrologPrinter(RecursiveMachineLoader rml, BParser bParser,
- File mainFile, String moduleName, Hashtable<Node, TLAType> typeTable) {
- this.rml = rml;
- this.bParser = bParser;
- this.moduleName = moduleName;
- this.typeTable = typeTable;
- files.add(mainFile);
- }
-
- public void setPositions(HashSet<PositionedNode> sourcePositions) {
- positions = sourcePositions;
- }
-
- public void printAsProlog(final PrintWriter out, final boolean useIndention) {
- final IPrologTermOutput pout = new PrologTermOutput(out, useIndention);
- printAsProlog(pout);
- }
-
- public void printAsProlog(final IPrologTermOutput pout) {
- // final ClassicalPositionPrinter pprinter = new
- // ClassicalPositionPrinter(
- // rml.getNodeIdMapping());
-
- final TlaTypePrinter pprinter = new TlaTypePrinter(
- rml.getNodeIdMapping(), typeTable);
- pprinter.setSourcePositions(positions);
-
- final ASTProlog prolog = new ASTProlog(pout, pprinter);
-
- // parser version
- pout.openTerm("parser_version");
- pout.printAtom(BParser.getGitSha());
- pout.closeTerm();
- pout.fullstop();
-
- // machine
- pout.openTerm("classical_b");
- pout.printAtom(moduleName);
- pout.openList();
- for (final File file : files) {
- try {
- pout.printAtom(file.getCanonicalPath());
- } catch (IOException e) {
- pout.printAtom(file.getPath());
- }
- }
- pout.closeList();
- pout.closeTerm();
- pout.fullstop();
- for (final Map.Entry<String, Start> entry : rml.getParsedMachines()
- .entrySet()) {
- pout.openTerm("machine");
- //final SourcePositions src = positions.get(entry.getKey());
- //pprinter.setSourcePositions(src);
- entry.getValue().apply(prolog);
- pout.closeTerm();
- pout.fullstop();
- }
-
- pout.flush();
- }
-}
diff --git a/src/main/java/de/tla2b/output/TlaTypePrinter.java b/src/main/java/de/tla2b/output/TlaTypePrinter.java
index afc200b22b1c8511e2fa55328c1a95422b07634c..1092ed7bd6d4d7120f6ea3565d6f49a2947af814 100644
--- a/src/main/java/de/tla2b/output/TlaTypePrinter.java
+++ b/src/main/java/de/tla2b/output/TlaTypePrinter.java
@@ -1,76 +1,49 @@
package de.tla2b.output;
+import de.be4.classicalb.core.parser.analysis.prolog.ClassicalPositionPrinter;
import de.be4.classicalb.core.parser.analysis.prolog.INodeIds;
-import de.be4.classicalb.core.parser.analysis.prolog.PositionPrinter;
import de.be4.classicalb.core.parser.node.Node;
-import de.hhu.stups.sablecc.patch.PositionedNode;
import de.prob.prolog.output.IPrologTermOutput;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.types.*;
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Hashtable;
+import java.util.List;
+import java.util.Map;
-public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
- private IPrologTermOutput pout;
-
- // to look up the identifier of each node
- public final INodeIds nodeIds;
-
- private final Hashtable<Node, TLAType> typeTable;
-
- private HashSet<PositionedNode> positions;
+public class TlaTypePrinter extends ClassicalPositionPrinter implements TypeVisitorInterface {
- public TlaTypePrinter(INodeIds nodeIds,
- Hashtable<Node, TLAType> typeTable) {
- this.nodeIds = nodeIds;
- this.typeTable = typeTable;
- }
+ private IPrologTermOutput pout;
+ private final Map<Node, TLAType> types;
- public void setSourcePositions(final HashSet<PositionedNode> positions) {
- this.positions = positions;
+ public TlaTypePrinter(INodeIds nodeIds, Map<Node, TLAType> types) {
+ super(nodeIds);
+ super.setPrintSourcePositions(true, true);
+ this.types = types;
}
public void printPosition(final Node node) {
- TLAType type = typeTable.get(node);
+ TLAType type = types.get(node);
if (type != null) {
pout.openTerm("info");
}
- final Integer id = nodeIds.lookup(node);
- if (positions != null && positions.contains(node)) {
- pout.openTerm("pos", true);
- pout.printNumber(id == null ? -1 : id);
- pout.printNumber(nodeIds.lookupFileNumber(node));
- pout.printNumber(node.getStartPos().getLine());
- pout.printNumber(node.getStartPos().getPos());
- pout.printNumber(node.getEndPos().getLine());
- pout.printNumber(node.getEndPos().getPos());
- pout.closeTerm();
- } else {
- if (id == null) {
- pout.printAtom("none");
- } else {
- pout.printNumber(id);
- }
- }
+ super.printPosition(node);
+
if (type != null) {
pout.openTerm("tla_type");
type.apply(this);
pout.closeTerm();
-
pout.closeTerm();
}
}
public void setPrologTermOutput(final IPrologTermOutput pout) {
+ super.setPrologTermOutput(pout);
this.pout = pout;
}
public void caseIntegerType(IntType t) {
pout.printAtom("integer");
-
}
public void caseBoolType(BoolType t) {
@@ -122,7 +95,7 @@ public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
public void caseStructType(StructType type) {
pout.openTerm("record");
pout.openList();
- ArrayList<String> fields = type.getFields();
+ List<String> fields = type.getFields();
for (String field : fields) {
if (type.isExtensible()) {
pout.openTerm("opt");
@@ -150,5 +123,4 @@ public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
public void caseUntyped(UntypedType type) {
throw new NotImplementedException("should not happen");
}
-
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 0786aade5da7253dadcb53d844d07dc17bca39c7..2378f2439f5f8351fa64b3ef8cc64ac9fe015ecb 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -43,8 +43,8 @@ public class BAstCreator extends BuiltInOPs
private final Definitions bDefinitions = new Definitions();
private Start start;
- private final Hashtable<Node, TLAType> typeTable = new Hashtable<>();
- private final HashSet<PositionedNode> sourcePosition = new HashSet<>();
+ private final Map<Node, TLAType> types = new HashMap<>();
+ private final Set<PositionedNode> sourcePosition = new HashSet<>();
private final NodeFileNumbers nodeFileNumbers = new NodeFileNumbers();
private final List<String> filesOrderedById = new ArrayList<>();
private List<String> toplevelUnchangedVariableNames = new ArrayList<>();
@@ -334,7 +334,7 @@ public class BAstCreator extends BuiltInOPs
new AIdentifierExpression(createTIdentifierLiteral(getName(opDeclNode))), opDeclNode);
list.add(id);
TLAType type = (TLAType) opDeclNode.getToolObject(TYPE_ID);
- typeTable.put(id, type);
+ types.put(id, type);
}
AVariablesMachineClause varClause = new AVariablesMachineClause(list);
machineClauseList.add(varClause);
@@ -350,14 +350,14 @@ public class BAstCreator extends BuiltInOPs
recDef.getOpDefNode());
constantsList.add(id);
TLAType type = (TLAType) recDef.getOpDefNode().getToolObject(TYPE_ID);
- typeTable.put(id, type);
+ types.put(id, type);
}
for (OpDefNode recFunc : specAnalyser.getRecursiveFunctions()) {
AIdentifierExpression id = new AIdentifierExpression(createTIdentifierLiteral(getName(recFunc)));
constantsList.add(id);
TLAType type = (TLAType) recFunc.getToolObject(TYPE_ID);
- typeTable.put(id, type);
+ types.put(id, type);
}
if (!constantsList.isEmpty()) {
@@ -381,7 +381,7 @@ public class BAstCreator extends BuiltInOPs
new AIdentifierExpression(createTIdentifierLiteral(getName(opDeclNode))), opDeclNode);
constantsList.add(id);
TLAType type = (TLAType) opDeclNode.getToolObject(TYPE_ID);
- typeTable.put(id, type);
+ types.put(id, type);
}
if (!constantsList.isEmpty()) {
AConstantsMachineClause constantsClause = new AConstantsMachineClause(constantsList);
@@ -2362,11 +2362,11 @@ public class BAstCreator extends BuiltInOPs
return bDefinitions;
}
- public Hashtable<Node, TLAType> getTypeTable() {
- return this.typeTable;
+ public Map<Node, TLAType> getTypes() {
+ return this.types;
}
- public HashSet<PositionedNode> getSourcePositions() {
+ public Set<PositionedNode> getSourcePositions() {
return this.sourcePosition;
}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 79c2d965f1e7357372772d389f8ec16c061658ca..474f18e1cf6da6bf9c9082772cfd14a896d071a5 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -9,13 +9,15 @@ 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.hhu.stups.sablecc.patch.PositionedNode;
+import de.prob.prolog.output.PrologTermOutput;
import de.tla2b.analysis.*;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ModuleOverrider;
import de.tla2b.exceptions.TLA2BFrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.output.PrologPrinter;
+import de.tla2b.output.TlaTypePrinter;
import de.tla2b.translation.BMacroHandler;
import de.tla2b.translation.RecursiveFunctionHandler;
import de.tla2b.types.TLAType;
@@ -30,14 +32,14 @@ import util.ToolIO;
import java.io.*;
import java.nio.charset.StandardCharsets;
import java.nio.file.Files;
-import java.util.Hashtable;
+import java.util.Map;
public class Translator implements TranslationGlobals {
private String moduleFileName;
private File moduleFile;
private File configFile;
private Start BAst;
- private Hashtable<Node, TLAType> typeTable;
+ private Map<Node, TLAType> types;
private Definitions bDefinitions;
@@ -203,7 +205,7 @@ public class Translator implements TranslationGlobals {
new BMacroHandler(specAnalyser, conEval),
new RecursiveFunctionHandler(specAnalyser));
- this.typeTable = bAstCreator.getTypeTable();
+ this.types = bAstCreator.getTypes();
this.bDefinitions = bAstCreator.getBDefinitions();
return this.BAst = bAstCreator.getStartNode();
}
@@ -226,12 +228,8 @@ public class Translator implements TranslationGlobals {
bParser.getDefinitions().addDefinitions(getBDefinitions());
final RecursiveMachineLoader rml = parseAllMachines(getBAST(), getModuleFile(), bParser);
- String moduleName = FileUtils.removeExtension(moduleFile.getName());
- PrologPrinter prologPrinter = new PrologPrinter(rml, bParser, moduleFile, moduleName, typeTable);
- prologPrinter.setPositions(bAstCreator.getSourcePositions());
-
PrintWriter outWriter = new PrintWriter(probFile, "UTF-8");
- prologPrinter.printAsProlog(outWriter, false);
+ rml.printAsProlog(new PrologTermOutput(outWriter, false));
outWriter.close();
System.out.println(probFile.getAbsolutePath() + " created.");
@@ -288,10 +286,11 @@ public class Translator implements TranslationGlobals {
}
- public static RecursiveMachineLoader parseAllMachines(final Start ast, final File f, final BParser bparser)
- throws BCompoundException {
final RecursiveMachineLoader rml = new RecursiveMachineLoader(f.getParent(), bparser.getContentProvider());
+ public RecursiveMachineLoader parseAllMachines(final Start ast, final File f, final BParser bparser) throws BCompoundException {
rml.loadAllMachines(f, ast, bparser.getDefinitions());
+ // this is required for correct positions in ProB2(-UI) when rml.printAsProlog is called
+ rml.setPositionPrinter(new TlaTypePrinter(rml.getNodeIdMapping(), bAstCreator.getTypes()));
return rml;
}
@@ -341,8 +340,8 @@ public class Translator implements TranslationGlobals {
return moduleFile;
}
- public Hashtable<Node, TLAType> getTypeTable() {
- return this.typeTable;
+ public Map<Node, TLAType> getTypes() {
+ return this.types;
}
}