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

simplify and improve position printing

- use ClassicalPositionPrinter for print of position informations in TlaTypePrinter
- get rid of PrologPrinter by using RecursiveMachineLoader.printAsProlog with TlaTypePrinter
parent 7e3b2e8c
No related branches found
No related tags found
No related merge requests found
Pipeline #144582 failed
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();
}
}
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");
}
}
......@@ -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;
}
......
......@@ -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;
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment