From 70f8ec54ee9521322ba54b8b4f78b5d5ee3bf751 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Mon, 12 May 2014 17:20:22 +0200
Subject: [PATCH] adding the TLA type to the prolog AST.
---
src/main/java/de/tla2b/TLA2B.java | 9 +-
.../java/de/tla2b/analysis/SpecAnalyser.java | 2 +-
.../java/de/tla2b/analysis/TypeChecker.java | 153 ++++++++----------
.../de/tla2b/config/ConfigfileEvaluator.java | 4 +-
.../tla2b/old/AbstractExpressionPrinter.java | 20 +--
.../java/de/tla2b/old/BMachinePrinter.java | 3 +-
.../java/de/tla2b/old/ExpressionPrinter.java | 3 +-
.../java/de/tla2b/output/PrologPrinter.java | 100 ++++++++++++
.../java/de/tla2b/output/TlaTypePrinter.java | 136 ++++++++++++++++
.../de/tla2b/output/TypeVisitorInterface.java | 31 ++++
.../tla2b/translation/BDefinitionsFinder.java | 2 +-
.../tla2b/translation/OperationsFinder.java | 3 +-
.../translation/UsedDefinitionsFinder.java | 3 +-
.../de/tla2b/types/AbstractHasFollowers.java | 4 +-
src/main/java/de/tla2b/types/BoolType.java | 10 +-
src/main/java/de/tla2b/types/EnumType.java | 11 +-
.../java/de/tla2b/types/FunctionType.java | 13 +-
src/main/java/de/tla2b/types/IType.java | 3 +
src/main/java/de/tla2b/types/IntType.java | 12 +-
.../java/de/tla2b/types/ModelValueType.java | 9 +-
src/main/java/de/tla2b/types/PairType.java | 9 +-
src/main/java/de/tla2b/types/SetType.java | 9 +-
src/main/java/de/tla2b/types/StringType.java | 11 +-
...unction.java => StructOrFunctionType.java} | 25 +--
src/main/java/de/tla2b/types/StructType.java | 15 +-
src/main/java/de/tla2b/types/TLAType.java | 2 +-
src/main/java/de/tla2b/types/TupleType.java | 13 +-
.../types/{Untyped.java => UntypedType.java} | 13 +-
src/main/java/de/tla2bAst/BAstCreator.java | 146 ++++-------------
src/main/java/de/tla2bAst/Translator.java | 21 ++-
src/test/resources/regression/Club/Club.prob | 2 +-
31 files changed, 527 insertions(+), 270 deletions(-)
create mode 100644 src/main/java/de/tla2b/output/PrologPrinter.java
create mode 100644 src/main/java/de/tla2b/output/TlaTypePrinter.java
create mode 100644 src/main/java/de/tla2b/output/TypeVisitorInterface.java
rename src/main/java/de/tla2b/types/{StructOrFunction.java => StructOrFunctionType.java} (85%)
rename src/main/java/de/tla2b/types/{Untyped.java => UntypedType.java} (71%)
diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java
index b717d53..cd5b121 100644
--- a/src/main/java/de/tla2b/TLA2B.java
+++ b/src/main/java/de/tla2b/TLA2B.java
@@ -4,19 +4,12 @@
package de.tla2b;
-import java.io.File;
-import java.io.PrintStream;
-import java.io.PrintWriter;
-import de.be4.classicalb.core.parser.BParser;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2bAst.Translator;
-import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
-import de.be4.classicalb.core.parser.exceptions.BException;
-import de.be4.classicalb.core.parser.node.Start;
public class TLA2B implements TranslationGlobals {
private String mainFile;
@@ -69,7 +62,7 @@ public class TLA2B implements TranslationGlobals {
System.err.println(e.getMessage());
System.exit(-1);
}
- translator.createMachineFile();
+ //translator.createMachineFile();
translator.createProbFile();
}
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 1c46459..fbf363c 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -35,7 +35,7 @@ import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
- ToolGlobals, IType, TranslationGlobals {
+ ToolGlobals, TranslationGlobals {
private OpDefNode spec;
private OpDefNode init;
private OpDefNode next;
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index abf389b..3869d37 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -40,8 +40,8 @@ import tla2sany.semantic.StringNode;
import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
-public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
- BBuildIns, TranslationGlobals {
+public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
+ TranslationGlobals {
private final int TEMP_TYPE_ID = 6;
private int paramId;
@@ -55,7 +55,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
private ModuleNode moduleNode;
private ArrayList<OpDeclNode> bConstList;
private SpecAnalyser specAnalyser;
-
+
private Hashtable<OpDeclNode, ValueObj> constantAssignments;
private ConfigfileEvaluator conEval;
@@ -68,7 +68,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
public TypeChecker(ModuleNode moduleNode, ConfigfileEvaluator conEval,
SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
- this.specAnalyser= specAnalyser;
+ this.specAnalyser = specAnalyser;
if (conEval != null) {
this.bConstList = conEval.getbConstantList();
this.constantAssignments = conEval.getConstantAssignments();
@@ -101,11 +101,11 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
&& constantAssignments.containsKey(con)) {
TLAType t = constantAssignments.get(con).getType();
con.setToolObject(TYPE_ID, t);
- if(t instanceof AbstractHasFollowers){
+ if (t instanceof AbstractHasFollowers) {
((AbstractHasFollowers) t).addFollower(con);
}
} else {
- Untyped u = new Untyped();
+ UntypedType u = new UntypedType();
con.setToolObject(TYPE_ID, u);
u.addFollower(con);
}
@@ -114,34 +114,33 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
OpDeclNode[] vars = moduleNode.getVariableDecls();
for (int i = 0; i < vars.length; i++) {
OpDeclNode var = vars[i];
- Untyped u = new Untyped();
+ UntypedType u = new UntypedType();
var.setToolObject(TYPE_ID, u);
u.addFollower(var);
}
evalDefinitions(moduleNode.getOpDefs());
- if(conEval != null){
+ if (conEval != null) {
Iterator<Entry<OpDeclNode, OpDefNode>> iter = conEval
.getConstantOverrideTable().entrySet().iterator();
while (iter.hasNext()) {
Entry<OpDeclNode, OpDefNode> entry = iter.next();
OpDeclNode con = entry.getKey();
- if(!bConstList.contains(con)){
+ if (!bConstList.contains(con)) {
continue;
}
OpDefNode def = entry.getValue();
TLAType defType = (TLAType) def.getToolObject(TYPE_ID);
TLAType conType = (TLAType) con.getToolObject(TYPE_ID);
-
+
try {
TLAType result = defType.unify(conType);
con.setToolObject(TYPE_ID, result);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
"Expected %s, found %s at constant '%s'.", defType,
- conType, con.getName())
- );
+ conType, con.getName()));
}
}
}
@@ -201,7 +200,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
for (int j = 0; j < struct.getFields().size(); j++) {
String fieldName = struct.getFields().get(j);
if (!fieldNames.contains(fieldName)
- && struct.getType(fieldName).getKind() == MODELVALUE) {
+ && struct.getType(fieldName).getKind() == IType.MODELVALUE) {
EnumType e = (EnumType) struct.getType(fieldName);
e.setNoVal();
}
@@ -243,11 +242,11 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
"TLA2B do not support 2nd-order operators: '%s'\n %s ",
def.getName(), def.getLocation()));
}
- Untyped u = new Untyped();
+ UntypedType u = new UntypedType();
p.setToolObject(paramId, u);
u.addFollower(p);
}
- TLAType defType = visitExprNode(def.getBody(), new Untyped());
+ TLAType defType = visitExprNode(def.getBody(), new UntypedType());
def.setToolObject(TYPE_ID, defType);
if (defType instanceof AbstractHasFollowers) {
((AbstractHasFollowers) defType).addFollower(def);
@@ -392,10 +391,10 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
TLAType v = (TLAType) symbolNode.getToolObject(TYPE_ID);
if (v == null) {
SymbolNode var = this.specAnalyser.getSymbolNodeByName(vName);
- if(var != null){
- // symbolNode is variable of an expression, e.g. v + 1
+ if (var != null) {
+ // symbolNode is variable of an expression, e.g. v + 1
v = (TLAType) var.getToolObject(TYPE_ID);
- }else{
+ } else {
throw new RuntimeException(vName + " has no type yet!");
}
}
@@ -445,7 +444,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
TLAType found = ((TLAType) def.getToolObject(TYPE_ID));
if (found == null)
- found = new Untyped();
+ found = new UntypedType();
// throw new RuntimeException(def.getName() + " has no type yet!");
found = found.cloneTLAType();
try {
@@ -463,7 +462,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
FormalParamNode p = params[i];
TLAType pType = ((TLAType) p.getToolObject(TYPE_ID));
if (pType == null) {
- pType = new Untyped();
+ pType = new UntypedType();
// throw new RuntimeException("Parameter " + p.getName()
// + " has no type yet!\n" + p.getLocation());
}
@@ -479,7 +478,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
p.setToolObject(TEMP_TYPE_ID, pType);
}
- if (found.isUntyped() || untyped|| def.getInRecursive() == false) {
+ if (found.isUntyped() || untyped || def.getInRecursive() == false) {
// evaluate the body of the definition again
paramId = TEMP_TYPE_ID;
found = visitExprNode(def.getBody(), found);
@@ -525,7 +524,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
.getOperator().getName(), n.getLocation()));
}
TLAType left = visitExprOrOpArgNode(n.getArgs()[0],
- new de.tla2b.types.Untyped());
+ new de.tla2b.types.UntypedType());
visitExprOrOpArgNode(n.getArgs()[1], left);
return BoolType.getInstance();
}
@@ -578,7 +577,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
**********************************************************************/
case OPCODE_se: // SetEnumeration {..}
{
- SetType found = new SetType(new Untyped());
+ SetType found = new SetType(new UntypedType());
try {
found = found.unify(expected);
} catch (UnificationException e) {
@@ -602,7 +601,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
.getOperator().getName(), n.getLocation()));
}
TLAType element = visitExprOrOpArgNode(n.getArgs()[0],
- new Untyped());
+ new UntypedType());
visitExprOrOpArgNode(n.getArgs()[1], new SetType(element));
return BoolType.getInstance();
@@ -612,7 +611,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case OPCODE_cup: // set union
case OPCODE_cap: // set intersection
{
- SetType found = new SetType(new Untyped());
+ SetType found = new SetType(new UntypedType());
try {
found = found.unify(expected);
} catch (UnificationException e) {
@@ -635,7 +634,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
.getOperator().getName(), n.getLocation()));
}
TLAType left = visitExprOrOpArgNode(n.getArgs()[0], new SetType(
- new Untyped()));
+ new UntypedType()));
visitExprOrOpArgNode(n.getArgs()[1], left);
return BoolType.getInstance();
}
@@ -661,7 +660,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
{
- SetType found = new SetType(new Untyped());
+ SetType found = new SetType(new UntypedType());
try {
found = found.unify(expected);
} catch (UnificationException e) {
@@ -676,7 +675,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case OPCODE_subset: // SUBSET (conforms POW in B)
{
- SetType found = new SetType(new Untyped());
+ SetType found = new SetType(new UntypedType());
try {
found = found.unify(expected);
} catch (UnificationException e) {
@@ -690,7 +689,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case OPCODE_union: // Union - Union{{1},{2}}
{
- SetType found = new SetType(new Untyped());
+ SetType found = new SetType(new UntypedType());
try {
found = found.unify(expected);
} catch (UnificationException e) {
@@ -729,11 +728,12 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case OPCODE_tup: { // $Tuple
ArrayList<TLAType> list = new ArrayList<TLAType>();
for (int i = 0; i < n.getArgs().length; i++) {
- list.add(visitExprOrOpArgNode(n.getArgs()[i], new Untyped()));
+ list.add(visitExprOrOpArgNode(n.getArgs()[i], new UntypedType()));
}
TLAType found = null;
if (list.size() == 0) {
- found = new FunctionType(IntType.getInstance(), new Untyped());
+ found = new FunctionType(IntType.getInstance(),
+ new UntypedType());
} else if (list.size() == 1) {
found = new FunctionType(IntType.getInstance(), list.get(0));
} else {
@@ -766,7 +766,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
recType.addFollower(recFunc);
TLAType domainType = evalBoundedVariables(n);
- FunctionType found = new FunctionType(domainType, new Untyped());
+ FunctionType found = new FunctionType(domainType, new UntypedType());
visitExprOrOpArgNode(n.getArgs()[0], found.getRange());
try {
@@ -792,7 +792,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case OPCODE_fc: // [n \in Nat |-> n+1]
{
TLAType domainType = evalBoundedVariables(n);
- FunctionType found = new FunctionType(domainType, new Untyped());
+ FunctionType found = new FunctionType(domainType, new UntypedType());
visitExprOrOpArgNode(n.getArgs()[0], found.getRange());
try {
@@ -818,12 +818,13 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
OpApplNode domOpAppl = (OpApplNode) dom;
for (int i = 0; i < domOpAppl.getArgs().length; i++) {
TLAType d = visitExprOrOpArgNode(domOpAppl.getArgs()[i],
- new Untyped());
+ new UntypedType());
domList.add(d);
}
domType = new TupleType(domList);
} else {
- domType = visitExprOrOpArgNode(n.getArgs()[1], new Untyped());
+ domType = visitExprOrOpArgNode(n.getArgs()[1],
+ new UntypedType());
}
FunctionType func = new FunctionType(domType, expected);
FunctionType res = (FunctionType) visitExprOrOpArgNode(
@@ -836,7 +837,8 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
***********************************************************************/
case OPCODE_domain: {
- FunctionType func = new FunctionType(new Untyped(), new Untyped());
+ FunctionType func = new FunctionType(new UntypedType(),
+ new UntypedType());
func = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], func);
TLAType res = null;
try {
@@ -854,9 +856,9 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case OPCODE_sof: // [ A -> B]
{
SetType A = (SetType) visitExprOrOpArgNode(n.getArgs()[0],
- new SetType(new Untyped()));
+ new SetType(new UntypedType()));
SetType B = (SetType) visitExprOrOpArgNode(n.getArgs()[1],
- new SetType(new Untyped()));
+ new SetType(new UntypedType()));
SetType found = new SetType(new FunctionType(A.getSubType(),
B.getSubType()));
@@ -886,7 +888,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
ArrayList<TLAType> list = new ArrayList<TLAType>();
for (int i = 0; i < n.getArgs().length; i++) {
SetType t = (SetType) visitExprOrOpArgNode(n.getArgs()[i],
- new SetType(new Untyped()));
+ new SetType(new UntypedType()));
list.add(t.getSubType());
}
@@ -911,7 +913,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
OpApplNode pair = (OpApplNode) n.getArgs()[i];
StringNode field = (StringNode) pair.getArgs()[0];
SetType fieldType = (SetType) visitExprOrOpArgNode(
- pair.getArgs()[1], new SetType(new Untyped()));
+ pair.getArgs()[1], new SetType(new UntypedType()));
struct.add(field.getRep().toString(), fieldType.getSubType());
}
@@ -937,7 +939,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
OpApplNode pair = (OpApplNode) n.getArgs()[i];
StringNode field = (StringNode) pair.getArgs()[0];
TLAType fieldType = visitExprOrOpArgNode(pair.getArgs()[1],
- new Untyped());
+ new UntypedType());
found.add(field.getRep().toString(), fieldType);
}
try {
@@ -1013,15 +1015,15 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
}
- case OPCODE_uc:{
- TLAType found = new Untyped();
+ case OPCODE_uc: {
+ TLAType found = new UntypedType();
FormalParamNode x = n.getUnbdedQuantSymbols()[0];
x.setToolObject(TYPE_ID, found);
if (found instanceof AbstractHasFollowers) {
((AbstractHasFollowers) found).addFollower(x);
}
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
-
+
found = (TLAType) x.getToolObject(TYPE_ID);
try {
found = found.unify(expected);
@@ -1032,7 +1034,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
}
return found;
}
-
+
case OPCODE_bc: { // CHOOSE x \in S: P
if (n.isBdedQuantATuple()[0]) {
throw new TypeErrorException(
@@ -1041,7 +1043,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
}
ExprNode[] bounds = n.getBdedQuantBounds();
SetType S = (SetType) visitExprNode(bounds[0], new SetType(
- new Untyped()));
+ new UntypedType()));
TLAType found = S.getSubType();
try {
@@ -1059,7 +1061,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
return found;
}
-
+
case OPCODE_unchanged: {
return BoolType.getInstance().unify(expected);
}
@@ -1082,7 +1084,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
ExprNode[] bounds = n.getBdedQuantBounds();
for (int i = 0; i < bounds.length; i++) {
SetType boundType = (SetType) visitExprNode(bounds[i], new SetType(
- new Untyped()));
+ new UntypedType()));
TLAType subType = boundType.getSubType();
if (n.isBdedQuantATuple()[i]) {
@@ -1104,7 +1106,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
((AbstractHasFollowers) paramType).addFollower(p);
}
}
- } else if (subType instanceof Untyped) {
+ } else if (subType instanceof UntypedType) {
TupleType tuple = new TupleType(params[i].length);
try {
tuple = (TupleType) tuple.unify(subType);
@@ -1169,7 +1171,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
ExprOrOpArgNode leftside = pair.getArgs()[0];
ExprOrOpArgNode rightside = pair.getArgs()[1];
// stored for @ node
- Untyped untyped = new Untyped();
+ UntypedType untyped = new UntypedType();
rightside.setToolObject(TYPE_ID, untyped);
untyped.addFollower(rightside);
TLAType valueType = visitExprOrOpArgNode(rightside, untyped);
@@ -1184,7 +1186,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
if (first instanceof StringNode) {
String field = ((StringNode) first).getRep().toString();
TLAType res = evalType(list, valueType);
- StructOrFunction s = new StructOrFunction(field, res);
+ StructOrFunctionType s = new StructOrFunctionType(field, res);
try {
t = t.unify(s);
} catch (UnificationException e) {
@@ -1205,12 +1207,12 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
OpApplNode domOpAppl = (OpApplNode) domExpr;
for (int j = 0; j < domOpAppl.getArgs().length; j++) {
TLAType d = visitExprOrOpArgNode(
- domOpAppl.getArgs()[j], new Untyped());
+ domOpAppl.getArgs()[j], new UntypedType());
domList.add(d);
}
domType = new TupleType(domList);
} else {
- domType = visitExprOrOpArgNode(domExpr, new Untyped());
+ domType = visitExprOrOpArgNode(domExpr, new UntypedType());
}
rangeType = evalType(list, valueType);
FunctionType func = new FunctionType(domType, rangeType);
@@ -1242,11 +1244,11 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
if (head instanceof StringNode) {
// record or function of strings
String name = ((StringNode) head).getRep().toString();
- StructOrFunction res = new StructOrFunction(name, evalType(list,
- valueType));
+ StructOrFunctionType res = new StructOrFunctionType(name, evalType(
+ list, valueType));
return res;
}
- TLAType t = visitExprOrOpArgNode(head, new Untyped());
+ TLAType t = visitExprOrOpArgNode(head, new UntypedType());
FunctionType res = new FunctionType(t, evalType(list, valueType));
return res;
}
@@ -1366,7 +1368,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
"Expected %s, found BOOL at 'IsFiniteSet',\n%s",
expected, n.getLocation()));
}
- visitExprOrOpArgNode(n.getArgs()[0], new SetType(new Untyped()));
+ visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
return BoolType.getInstance();
}
@@ -1379,7 +1381,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
"Expected %s, found INTEGER at 'Cardinality',\n%s",
expected, n.getLocation()));
}
- visitExprOrOpArgNode(n.getArgs()[0], new SetType(new Untyped()));
+ visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
return IntType.getInstance();
}
@@ -1389,7 +1391,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case B_OPCODE_seq: { // Seq(S) - set of sequences, S must be a set
SetType S = (SetType) visitExprOrOpArgNode(n.getArgs()[0],
- new SetType(new Untyped()));
+ new SetType(new UntypedType()));
SetType set_of_seq = new SetType(new FunctionType(
IntType.getInstance(), S.getSubType()));
@@ -1412,13 +1414,13 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0],
- new FunctionType(IntType.getInstance(), new Untyped()));
+ new FunctionType(IntType.getInstance(), new UntypedType()));
return IntType.getInstance();
}
case B_OPCODE_conc: { // s \o s2 - concatenation of s and s2
FunctionType found = new FunctionType(IntType.getInstance(),
- new Untyped());
+ new UntypedType());
found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[1], found);
try {
@@ -1434,7 +1436,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case B_OPCODE_append: // Append(s, e)
{
FunctionType found = new FunctionType(IntType.getInstance(),
- new Untyped());
+ new UntypedType());
found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
visitExprOrOpArgNode(n.getArgs()[1], found.getRange());
try {
@@ -1449,7 +1451,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case B_OPCODE_head: { // HEAD(s) - the first element of the sequence
FunctionType func = new FunctionType(IntType.getInstance(),
- new Untyped());
+ new UntypedType());
func = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], func);
TLAType found = func.getRange();
@@ -1465,7 +1467,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case B_OPCODE_tail: { // Tail(s)
FunctionType found = new FunctionType(IntType.getInstance(),
- new Untyped());
+ new UntypedType());
found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
try {
found = found.unify(expected);
@@ -1479,7 +1481,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case B_OPCODE_subseq: { // SubSeq(s,m,n)
FunctionType found = new FunctionType(IntType.getInstance(),
- new Untyped());
+ new UntypedType());
found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
visitExprOrOpArgNode(n.getArgs()[1], IntType.getInstance());
visitExprOrOpArgNode(n.getArgs()[2], IntType.getInstance());
@@ -1518,7 +1520,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case B_OPCODE_permseq: { // PermutedSequences(S)
SetType argType = (SetType) visitExprOrOpArgNode(n.getArgs()[0],
- new SetType(new Untyped()));
+ new SetType(new UntypedType()));
SetType found = new SetType(new FunctionType(IntType.getInstance(),
argType.getSubType()));
try {
@@ -1537,7 +1539,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
case B_OPCODE_pow1: // POW1
{
- SetType set = new SetType(new Untyped());
+ SetType set = new SetType(new UntypedType());
set = (SetType) visitExprOrOpArgNode(n.getArgs()[0], set);
SetType found = new SetType(set);
try {
@@ -1614,21 +1616,4 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
}
}
}
-
- public static TLAType makePair(ArrayList<TLAType> list) {
- if (list.size() == 0)
- throw new RuntimeException("emptylist");
- if (list.size() == 1)
- return list.get(0);
- PairType p = new PairType();
- p.setFirst(list.get(0));
- for (int i = 1; i < list.size(); i++) {
- p.setSecond(list.get(i));
- if (i < list.size() - 1) {
- p = new PairType(p, null);
- }
- }
- return p;
- }
-
}
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index 749d0b1..eb10b36 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -20,7 +20,7 @@ import de.tla2b.types.IntType;
import de.tla2b.types.SetType;
import de.tla2b.types.StringType;
import de.tla2b.types.TLAType;
-import de.tla2b.types.Untyped;
+import de.tla2b.types.UntypedType;
import tla2sany.semantic.InstanceNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
@@ -505,7 +505,7 @@ public class ConfigfileEvaluator {
return IntType.getInstance();
} else if (o.getClass().getName().equals("tlc2.value.SetEnumValue")) {
SetEnumValue set = (SetEnumValue) o;
- SetType t = new SetType(new Untyped());
+ SetType t = new SetType(new UntypedType());
if (set.size() == 0) {
throw new ConfigFileErrorException(
"empty set is not permitted!");
diff --git a/src/main/java/de/tla2b/old/AbstractExpressionPrinter.java b/src/main/java/de/tla2b/old/AbstractExpressionPrinter.java
index d1f11c5..80fdbba 100644
--- a/src/main/java/de/tla2b/old/AbstractExpressionPrinter.java
+++ b/src/main/java/de/tla2b/old/AbstractExpressionPrinter.java
@@ -34,7 +34,7 @@ import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
public abstract class AbstractExpressionPrinter extends BuiltInOPs implements
- ASTConstants, IType, BBuildIns, Priorities, TranslationGlobals {
+ ASTConstants, BBuildIns, Priorities, TranslationGlobals {
// private int substitutionId = 10;
final int NOBOOL = 0;
@@ -235,7 +235,7 @@ public abstract class AbstractExpressionPrinter extends BuiltInOPs implements
}
TLAType defType = (TLAType) n.getToolObject(TYPE_ID);
- if (defType != null && defType.getKind() == BOOL) {
+ if (defType != null && defType.getKind() == IType.BOOL) {
return makeBoolValue(out, expected, P_max);
}
return new ExprReturn(out);
@@ -564,7 +564,7 @@ public abstract class AbstractExpressionPrinter extends BuiltInOPs implements
String oldRecOrFunc = visitExprOrOpArgNode(n.getArgs()[0], d,
NOBOOL).out.toString();
- if (t.getKind() == STRUCT) {
+ if (t.getKind() == IType.STRUCT) {
StructType structType = (StructType) t;
Hashtable<String, String> temp = new Hashtable<String, String>();
@@ -884,7 +884,7 @@ public abstract class AbstractExpressionPrinter extends BuiltInOPs implements
if (head == null) {
return val;
}
- if (type.getKind() == STRUCT) {
+ if (type.getKind() == IType.STRUCT) {
StructType structType = (StructType) type;
String field = ((StringNode) head).getRep().toString();
@@ -945,7 +945,7 @@ public abstract class AbstractExpressionPrinter extends BuiltInOPs implements
protected ExprReturn evalIfThenElse(OpApplNode n, DContext d, int expected) {
TLAType t = (TLAType) n.getToolObject(TYPE_ID);
- if (t.getKind() == BOOL) {
+ if (t.getKind() == IType.BOOL) {
d.indent.append(" ");
ExprReturn iif = visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE);
ExprReturn then = visitExprOrOpArgNode(n.getArgs()[1], d, PREDICATE);
@@ -1367,18 +1367,18 @@ public abstract class AbstractExpressionPrinter extends BuiltInOPs implements
private String getDummy(TLAType type) {
switch (type.getKind()) {
- case INTEGER:
+ case IType.INTEGER:
return "0";
- case STRING:
+ case IType.STRING:
return "\"\"";
- case POW:
+ case IType.POW:
return "{}";
- case BOOL:
+ case IType.BOOL:
return "FALSE";
- case MODELVALUE:
+ case IType.MODELVALUE:
EnumType e = (EnumType) type;
return "noVal" + e.id;
default:
diff --git a/src/main/java/de/tla2b/old/BMachinePrinter.java b/src/main/java/de/tla2b/old/BMachinePrinter.java
index 9e435a7..7fa4473 100644
--- a/src/main/java/de/tla2b/old/BMachinePrinter.java
+++ b/src/main/java/de/tla2b/old/BMachinePrinter.java
@@ -17,6 +17,7 @@ import de.tla2b.config.ValueObj;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.EnumType;
+import de.tla2b.types.IType;
import de.tla2b.types.SetType;
import de.tla2b.types.TLAType;
import tla2sany.semantic.AssumeNode;
@@ -687,7 +688,7 @@ public class BMachinePrinter extends AbstractExpressionPrinter implements
}
TLAType defType = (TLAType) n.getToolObject(TYPE_ID);
- if (defType != null && defType.getKind() == BOOL) {
+ if (defType != null && defType.getKind() == IType.BOOL) {
return makeBoolValue(out, expected, P_max);
}
return new ExprReturn(out);
diff --git a/src/main/java/de/tla2b/old/ExpressionPrinter.java b/src/main/java/de/tla2b/old/ExpressionPrinter.java
index a0b3444..d388259 100644
--- a/src/main/java/de/tla2b/old/ExpressionPrinter.java
+++ b/src/main/java/de/tla2b/old/ExpressionPrinter.java
@@ -8,6 +8,7 @@ package de.tla2b.old;
import java.util.Hashtable;
import de.tla2b.global.BBuiltInOPs;
+import de.tla2b.types.IType;
import de.tla2b.types.TLAType;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
@@ -59,7 +60,7 @@ public class ExpressionPrinter extends AbstractExpressionPrinter {
protected ExprReturn evalIfThenElse(OpApplNode n, DContext d, int expected) {
TLAType t = (TLAType) n.getToolObject(TYPE_ID);
- if (t.getKind() == BOOL) {
+ if (t.getKind() == IType.BOOL) {
d.indent.append(" ");
ExprReturn iif = visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE);
ExprReturn then = visitExprOrOpArgNode(n.getArgs()[1], d, PREDICATE);
diff --git a/src/main/java/de/tla2b/output/PrologPrinter.java b/src/main/java/de/tla2b/output/PrologPrinter.java
new file mode 100644
index 0000000..ba951ae
--- /dev/null
+++ b/src/main/java/de/tla2b/output/PrologPrinter.java
@@ -0,0 +1,100 @@
+package de.tla2b.output;
+
+import java.io.File;
+import java.io.IOException;
+import java.io.PrintWriter;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Hashtable;
+import java.util.List;
+import java.util.Map;
+
+import de.be4.classicalb.core.parser.BParser;
+import de.be4.classicalb.core.parser.analysis.pragma.Pragma;
+import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
+import de.be4.classicalb.core.parser.analysis.prolog.ClassicalPositionPrinter;
+import de.be4.classicalb.core.parser.analysis.prolog.NodeIdAssignment;
+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.SourcePositions;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.output.PrologTermOutput;
+import de.tla2b.types.TLAType;
+
+public class PrologPrinter {
+ RecursiveMachineLoader rml;
+ BParser bParser;
+ String moduleName;
+
+ private final Map<String, SourcePositions> positions = new HashMap<String, SourcePositions>();
+ private final List<File> files = new ArrayList<File>();
+ 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 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);
+
+ final ASTProlog prolog = new ASTProlog(pout, pprinter);
+
+ // parser version
+ pout.openTerm("parser_version");
+ pout.printAtom(BParser.getBuildRevision());
+ 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();
+ }
+
+// if (bParser.getPragmas().size() > 0) {
+// NodeIdAssignment ids = pprinter.nodeIds;
+//
+// List<Pragma> pragmas = bParser.getPragmas();
+// for (Pragma pragma : pragmas) {
+// pragma.printProlog(pout, ids);
+// pout.fullstop();
+// }
+//
+// }
+ pout.flush();
+ }
+}
diff --git a/src/main/java/de/tla2b/output/TlaTypePrinter.java b/src/main/java/de/tla2b/output/TlaTypePrinter.java
new file mode 100644
index 0000000..724cfcb
--- /dev/null
+++ b/src/main/java/de/tla2b/output/TlaTypePrinter.java
@@ -0,0 +1,136 @@
+package de.tla2b.output;
+
+import java.util.ArrayList;
+import java.util.Hashtable;
+
+import de.be4.classicalb.core.parser.analysis.prolog.NodeIdAssignment;
+import de.be4.classicalb.core.parser.analysis.prolog.PositionPrinter;
+import de.be4.classicalb.core.parser.node.Node;
+import de.hhu.stups.sablecc.patch.SourcePositions;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.tla2b.exceptions.NotImplementedException;
+import de.tla2b.types.BoolType;
+import de.tla2b.types.EnumType;
+import de.tla2b.types.FunctionType;
+import de.tla2b.types.IntType;
+import de.tla2b.types.TLAType;
+import de.tla2b.types.ModelValueType;
+import de.tla2b.types.PairType;
+import de.tla2b.types.SetType;
+import de.tla2b.types.StringType;
+import de.tla2b.types.StructOrFunctionType;
+import de.tla2b.types.StructType;
+import de.tla2b.types.TupleType;
+import de.tla2b.types.UntypedType;
+
+public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
+ private IPrologTermOutput pout;
+
+ // to look up the identifier of each node
+ public final NodeIdAssignment nodeIds;
+
+ private final Hashtable<Node, TLAType> typeTable;
+
+ private SourcePositions positions;
+
+ // public TlaTypePrinter(final NodeIdAssignment nodeIds) {
+ // this.nodeIds = nodeIds;
+ // }
+
+ public TlaTypePrinter(NodeIdAssignment nodeIdAssignment,
+ Hashtable<Node, TLAType> typeTable) {
+ this.nodeIds = nodeIdAssignment;
+ this.typeTable = typeTable;
+ }
+
+ public void setSourcePositions(final SourcePositions positions) {
+ this.positions = positions;
+ }
+
+ public void printPosition(final Node node) {
+ pout.openTerm("info");
+ final Integer id = nodeIds.lookup(node);
+ pout.printNumber(id);
+
+ pout.openTerm("tla_type");
+ TLAType type = typeTable.get(node);
+ if (type == null) {
+ pout.printAtom("none");
+ } else {
+ type.apply(this);
+ }
+ pout.closeTerm();
+
+ pout.closeTerm();
+ }
+
+ public void setPrologTermOutput(final IPrologTermOutput pout) {
+ this.pout = pout;
+ }
+
+ public void caseIntegerType(IntType t) {
+ pout.printAtom("integer");
+
+ }
+
+ public void caseBoolType(BoolType t) {
+ pout.printAtom("bool");
+ }
+
+ public void caseEnumType(EnumType type) {
+ pout.printAtom("modelvalue");
+ }
+
+ public void caseFunctionType(FunctionType type) {
+ pout.openTerm("function", true);
+ type.getDomain().apply(this);
+ type.getRange().apply(this);
+ pout.closeTerm();
+ }
+
+ public void caseModelValueType(ModelValueType type) {
+ pout.printAtom("modelvalue");
+ }
+
+ public void casePairType(PairType type) {
+ pout.openTerm("couple", true);
+ type.getFirst().apply(this);
+ type.getSecond().apply(this);
+ pout.closeTerm();
+ }
+
+ public void caseSetType(SetType type) {
+ pout.openTerm("set");
+ type.getSubType().apply(this);
+ pout.closeTerm();
+ }
+
+ public void caseStringType(StringType type) {
+ pout.printAtom("string");
+ }
+
+ public void caseStructOrFunction(StructOrFunctionType type) {
+ throw new NotImplementedException("should not happen");
+ }
+
+ public void caseStructType(StructType type) {
+ pout.openTerm("struct");
+ pout.openList();
+ ArrayList<String> fields = type.getFields();
+ for (String field : fields) {
+ type.getType(field).apply(this);
+ }
+ pout.closeList();
+ pout.closeTerm();
+ }
+
+ public void caseTupleType(TupleType type) {
+ // TODO Auto-generated method stub
+
+ }
+
+ public void caseUntyped(UntypedType type) {
+ throw new NotImplementedException("should not happen");
+ }
+
+}
diff --git a/src/main/java/de/tla2b/output/TypeVisitorInterface.java b/src/main/java/de/tla2b/output/TypeVisitorInterface.java
new file mode 100644
index 0000000..5fbfc91
--- /dev/null
+++ b/src/main/java/de/tla2b/output/TypeVisitorInterface.java
@@ -0,0 +1,31 @@
+package de.tla2b.output;
+
+import de.tla2b.types.BoolType;
+import de.tla2b.types.EnumType;
+import de.tla2b.types.FunctionType;
+import de.tla2b.types.IntType;
+import de.tla2b.types.ModelValueType;
+import de.tla2b.types.PairType;
+import de.tla2b.types.SetType;
+import de.tla2b.types.StringType;
+import de.tla2b.types.StructOrFunctionType;
+import de.tla2b.types.StructType;
+import de.tla2b.types.TupleType;
+import de.tla2b.types.UntypedType;
+
+
+public interface TypeVisitorInterface {
+
+ void caseIntegerType(IntType type);
+ void caseBoolType(BoolType type);
+ void caseEnumType(EnumType type);
+ void caseFunctionType(FunctionType type);
+ void caseModelValueType(ModelValueType type);
+ void casePairType(PairType type);
+ void caseSetType(SetType type);
+ void caseStringType(StringType type);
+ void caseStructOrFunction(StructOrFunctionType type);
+ void caseStructType(StructType type);
+ void caseTupleType(TupleType type);
+ void caseUntyped(UntypedType type);
+}
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index 5272dc7..867822f 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -15,7 +15,7 @@ import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.IType;
public class BDefinitionsFinder extends AbstractASTVisitor implements
- ASTConstants, ToolGlobals, IType, TranslationGlobals {
+ ASTConstants, ToolGlobals, TranslationGlobals {
private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<OpDefNode>();
public BDefinitionsFinder(SpecAnalyser specAnalyser) {
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
index 3051cd2..78f7925 100644
--- a/src/main/java/de/tla2b/translation/OperationsFinder.java
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -15,10 +15,9 @@ import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.types.IType;
public class OperationsFinder extends AbstractASTVisitor implements
- ASTConstants, ToolGlobals, IType, TranslationGlobals {
+ ASTConstants, ToolGlobals, TranslationGlobals {
private final SpecAnalyser specAnalyser;
private String currentName;
diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
index 679a7f9..c5ef8a7 100644
--- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
@@ -12,10 +12,9 @@ import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.types.IType;
public class UsedDefinitionsFinder extends AbstractASTVisitor implements
- ASTConstants, ToolGlobals, IType, TranslationGlobals {
+ ASTConstants, ToolGlobals, TranslationGlobals {
private final HashSet<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
diff --git a/src/main/java/de/tla2b/types/AbstractHasFollowers.java b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
index fc6bc44..b7105c6 100644
--- a/src/main/java/de/tla2b/types/AbstractHasFollowers.java
+++ b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
@@ -74,8 +74,8 @@ public abstract class AbstractHasFollowers extends TLAType {
((FunctionType) follower).update(this, newType);
} else if (follower instanceof StructType) {
((StructType) follower).setNewType(this, newType);
- } else if (follower instanceof StructOrFunction) {
- ((StructOrFunction) follower).setNewType(this, newType);
+ } else if (follower instanceof StructOrFunctionType) {
+ ((StructOrFunctionType) follower).setNewType(this, newType);
} else {
throw new RuntimeException("Unknown follower type: "
+ follower.getClass());
diff --git a/src/main/java/de/tla2b/types/BoolType.java b/src/main/java/de/tla2b/types/BoolType.java
index 013822a..4daed91 100644
--- a/src/main/java/de/tla2b/types/BoolType.java
+++ b/src/main/java/de/tla2b/types/BoolType.java
@@ -3,6 +3,7 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.ABoolSetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
public class BoolType extends TLAType {
@@ -38,8 +39,8 @@ public class BoolType extends TLAType {
public BoolType unify(TLAType o) throws UnificationException {
if (o.getKind() == BOOL) {
return this;
- } else if (o instanceof Untyped) {
- ((Untyped) o).setFollowersTo(this);
+ } else if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
return this;
} else
throw new UnificationException();
@@ -59,4 +60,9 @@ public class BoolType extends TLAType {
public PExpression getBNode() {
return new ABoolSetExpression();
}
+
+ public void apply(TypeVisitorInterface t) {
+ t.caseBoolType(this);
+ }
+
}
\ No newline at end of file
diff --git a/src/main/java/de/tla2b/types/EnumType.java b/src/main/java/de/tla2b/types/EnumType.java
index 3cbe1fb..c0ce831 100644
--- a/src/main/java/de/tla2b/types/EnumType.java
+++ b/src/main/java/de/tla2b/types/EnumType.java
@@ -9,6 +9,7 @@ import java.util.LinkedHashSet;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
@@ -50,8 +51,8 @@ public class EnumType extends AbstractHasFollowers {
@Override
public EnumType unify(TLAType o) throws UnificationException {
- if (o instanceof Untyped) {
- ((Untyped) o).setFollowersTo(this);
+ if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
return this;
}
if (o instanceof EnumType) {
@@ -83,4 +84,10 @@ public class EnumType extends AbstractHasFollowers {
public PExpression getBNode() {
return BAstCreator.createIdentifierNode("ENUM" + id);
}
+
+ public void apply(TypeVisitorInterface t) {
+ t.caseEnumType(this);
+ }
+
+
}
\ No newline at end of file
diff --git a/src/main/java/de/tla2b/types/FunctionType.java b/src/main/java/de/tla2b/types/FunctionType.java
index 06a6d93..ad97f8d 100644
--- a/src/main/java/de/tla2b/types/FunctionType.java
+++ b/src/main/java/de/tla2b/types/FunctionType.java
@@ -3,6 +3,7 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.APartialFunctionExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
public class FunctionType extends AbstractHasFollowers {
private TLAType domain;
@@ -16,8 +17,8 @@ public class FunctionType extends AbstractHasFollowers {
public FunctionType() {
super(FUNCTION);
- this.setDomain(new Untyped());
- this.setRange(new Untyped());
+ this.setDomain(new UntypedType());
+ this.setRange(new UntypedType());
}
@@ -65,8 +66,8 @@ public class FunctionType extends AbstractHasFollowers {
public FunctionType unify(TLAType o) throws UnificationException {
if (!this.compare(o))
throw new UnificationException();
- if (o instanceof Untyped) {
- ((Untyped) o).setFollowersTo(this);
+ if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
return this;
}
if (o instanceof FunctionType) {
@@ -119,4 +120,8 @@ public class FunctionType extends AbstractHasFollowers {
return new APartialFunctionExpression(domain.getBNode(), range.getBNode());
}
+ public void apply(TypeVisitorInterface vistor) {
+ vistor.caseFunctionType(this);
+ }
+
}
diff --git a/src/main/java/de/tla2b/types/IType.java b/src/main/java/de/tla2b/types/IType.java
index 26c84ca..a363a9d 100644
--- a/src/main/java/de/tla2b/types/IType.java
+++ b/src/main/java/de/tla2b/types/IType.java
@@ -1,5 +1,7 @@
package de.tla2b.types;
+import de.tla2b.output.TypeVisitorInterface;
+
public interface IType {
public final int UNTYPED = 0;
public final int INTEGER = 1;
@@ -14,4 +16,5 @@ public interface IType {
public final int FUNCTION = 10;
public final int TUPLE = 11;
+ void apply(TypeVisitorInterface visitor);
}
diff --git a/src/main/java/de/tla2b/types/IntType.java b/src/main/java/de/tla2b/types/IntType.java
index b5fae0f..10bce86 100644
--- a/src/main/java/de/tla2b/types/IntType.java
+++ b/src/main/java/de/tla2b/types/IntType.java
@@ -3,6 +3,7 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.AIntegerSetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
public class IntType extends TLAType {
@@ -38,8 +39,8 @@ public class IntType extends TLAType {
public IntType unify(TLAType o) throws UnificationException {
if (o.getKind() == INTEGER) {
return this;
- } else if (o instanceof Untyped) {
- ((Untyped) o).setFollowersTo(this);
+ } else if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
return this;
} else
throw new UnificationException();
@@ -49,7 +50,7 @@ public class IntType extends TLAType {
public IntType cloneTLAType() {
return this;
}
-
+
@Override
public boolean contains(TLAType o) {
return false;
@@ -59,4 +60,9 @@ public class IntType extends TLAType {
public PExpression getBNode() {
return new AIntegerSetExpression();
}
+
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.caseIntegerType(this);
+ }
+
}
\ No newline at end of file
diff --git a/src/main/java/de/tla2b/types/ModelValueType.java b/src/main/java/de/tla2b/types/ModelValueType.java
index e196cea..86bed4b 100644
--- a/src/main/java/de/tla2b/types/ModelValueType.java
+++ b/src/main/java/de/tla2b/types/ModelValueType.java
@@ -2,6 +2,7 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
public class ModelValueType extends TLAType {
@@ -38,8 +39,8 @@ public class ModelValueType extends TLAType {
public ModelValueType unify(TLAType o) throws UnificationException {
if (o.getKind() == MODELVALUE) {
return this;
- } else if (o instanceof Untyped) {
- ((Untyped) o).setFollowersTo(this);
+ } else if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
return this;
} else
throw new UnificationException();
@@ -60,4 +61,8 @@ public class ModelValueType extends TLAType {
// TODO Auto-generated method stub
return null;
}
+
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.caseModelValueType(this);
+ }
}
\ No newline at end of file
diff --git a/src/main/java/de/tla2b/types/PairType.java b/src/main/java/de/tla2b/types/PairType.java
index 8eaf54a..2b3865a 100644
--- a/src/main/java/de/tla2b/types/PairType.java
+++ b/src/main/java/de/tla2b/types/PairType.java
@@ -4,6 +4,7 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
public class PairType extends AbstractHasFollowers {
@@ -12,8 +13,8 @@ public class PairType extends AbstractHasFollowers {
public PairType() {
super(PAIR);
- setFirst(new Untyped());
- setSecond(new Untyped());
+ setFirst(new UntypedType());
+ setSecond(new UntypedType());
}
public PairType(TLAType f, TLAType s) {
@@ -135,4 +136,8 @@ public class PairType extends AbstractHasFollowers {
return card;
}
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.casePairType(this);
+ }
+
}
diff --git a/src/main/java/de/tla2b/types/SetType.java b/src/main/java/de/tla2b/types/SetType.java
index 636aee8..e6d19ea 100644
--- a/src/main/java/de/tla2b/types/SetType.java
+++ b/src/main/java/de/tla2b/types/SetType.java
@@ -3,6 +3,7 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.APowSubsetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
public class SetType extends AbstractHasFollowers {
private TLAType subType;
@@ -45,7 +46,7 @@ public class SetType extends AbstractHasFollowers {
((AbstractHasFollowers) o).setFollowersTo(this);
}
- if (o instanceof StructOrFunction){
+ if (o instanceof StructOrFunctionType){
return (SetType)o.unify(this);
}
if (o instanceof SetType) {
@@ -67,7 +68,7 @@ public class SetType extends AbstractHasFollowers {
if (o.getKind() == UNTYPED)
return true;
- if (o instanceof StructOrFunction){
+ if (o instanceof StructOrFunctionType){
return o.compare(this);
}
@@ -107,4 +108,8 @@ public class SetType extends AbstractHasFollowers {
return new APowSubsetExpression(this.getSubType().getBNode());
}
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.caseSetType(this);
+ }
+
}
diff --git a/src/main/java/de/tla2b/types/StringType.java b/src/main/java/de/tla2b/types/StringType.java
index e66f900..b32ab64 100644
--- a/src/main/java/de/tla2b/types/StringType.java
+++ b/src/main/java/de/tla2b/types/StringType.java
@@ -7,6 +7,7 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.AStringSetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
public class StringType extends TLAType {
@@ -42,9 +43,9 @@ public class StringType extends TLAType {
public StringType unify(TLAType o) throws UnificationException {
if (o.getKind() == STRING) {
return this;
- } else if (o instanceof Untyped) {
- ((Untyped) o).setFollowersTo(this);
- ((Untyped) o).deleteFollowers();
+ } else if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
+ ((UntypedType) o).deleteFollowers();
return this;
} else
throw new UnificationException();
@@ -64,5 +65,9 @@ public class StringType extends TLAType {
public PExpression getBNode() {
return new AStringSetExpression();
}
+
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.caseStringType(this);
+ }
}
diff --git a/src/main/java/de/tla2b/types/StructOrFunction.java b/src/main/java/de/tla2b/types/StructOrFunctionType.java
similarity index 85%
rename from src/main/java/de/tla2b/types/StructOrFunction.java
rename to src/main/java/de/tla2b/types/StructOrFunctionType.java
index 7f18ef0..493bbde 100644
--- a/src/main/java/de/tla2b/types/StructOrFunction.java
+++ b/src/main/java/de/tla2b/types/StructOrFunctionType.java
@@ -11,19 +11,20 @@ import java.util.Map.Entry;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
-public class StructOrFunction extends AbstractHasFollowers {
+public class StructOrFunctionType extends AbstractHasFollowers {
private LinkedHashMap<String, TLAType> types;
- public StructOrFunction(String name, TLAType type) {
+ public StructOrFunctionType(String name, TLAType type) {
super(STRUCT_OR_FUNCTION);
types = new LinkedHashMap<String, TLAType>();
types.put(name, type);
}
- public StructOrFunction() {
+ public StructOrFunctionType() {
super(STRUCT_OR_FUNCTION);
types = new LinkedHashMap<String, TLAType>();
}
@@ -99,8 +100,8 @@ public class StructOrFunction extends AbstractHasFollowers {
return false;
}
- if (o instanceof StructOrFunction) {
- StructOrFunction s = (StructOrFunction) o;
+ if (o instanceof StructOrFunctionType) {
+ StructOrFunctionType s = (StructOrFunctionType) o;
Iterator<String> thisKeys = types.keySet().iterator();
while (thisKeys.hasNext()) {
@@ -144,7 +145,7 @@ public class StructOrFunction extends AbstractHasFollowers {
@Override
public TLAType cloneTLAType() {
- StructOrFunction res = new StructOrFunction();
+ StructOrFunctionType res = new StructOrFunctionType();
for (String field : types.keySet()) {
res.types.put(field, this.types.get(field));
}
@@ -156,8 +157,8 @@ public class StructOrFunction extends AbstractHasFollowers {
if (!this.compare(o))
throw new UnificationException();
- if (o instanceof Untyped) {
- ((Untyped) o).setFollowersTo(this);
+ if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
return this;
}
@@ -179,8 +180,8 @@ public class StructOrFunction extends AbstractHasFollowers {
}
return o.unify(res);
}
- if (o instanceof StructOrFunction) {
- StructOrFunction other = (StructOrFunction) o;
+ if (o instanceof StructOrFunctionType) {
+ StructOrFunctionType other = (StructOrFunctionType) o;
for (String field : other.types.keySet()) {
TLAType type = other.types.get(field);
if (this.types.containsKey(field)) {
@@ -229,4 +230,8 @@ public class StructOrFunction extends AbstractHasFollowers {
return null;
}
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.caseStructOrFunction(this);
+ }
+
}
diff --git a/src/main/java/de/tla2b/types/StructType.java b/src/main/java/de/tla2b/types/StructType.java
index f7df486..b995c71 100644
--- a/src/main/java/de/tla2b/types/StructType.java
+++ b/src/main/java/de/tla2b/types/StructType.java
@@ -1,6 +1,7 @@
package de.tla2b.types;
import java.util.ArrayList;
+import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.List;
@@ -15,6 +16,7 @@ import de.be4.classicalb.core.parser.node.AStructExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PRecEntry;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
public class StructType extends AbstractHasFollowers {
@@ -85,7 +87,7 @@ public class StructType extends AbstractHasFollowers {
if (o.getKind() == UNTYPED)
return true;
- if (o instanceof StructOrFunction) {
+ if (o instanceof StructOrFunctionType) {
return o.compare(this);
}
if (o instanceof StructType) {
@@ -113,7 +115,7 @@ public class StructType extends AbstractHasFollowers {
if (o instanceof AbstractHasFollowers)
((AbstractHasFollowers) o).setFollowersTo(this);
- if (o instanceof StructOrFunction) {
+ if (o instanceof StructOrFunctionType) {
return (StructType) o.unify(this);
}
@@ -235,4 +237,13 @@ public class StructType extends AbstractHasFollowers {
}
return new AStructExpression(recList);
}
+
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.caseStructType(this);
+ }
+
+ public LinkedHashMap<String, TLAType> getTypeTable(){
+ return this.types;
+ }
+
}
diff --git a/src/main/java/de/tla2b/types/TLAType.java b/src/main/java/de/tla2b/types/TLAType.java
index f6da56a..6ea3bde 100644
--- a/src/main/java/de/tla2b/types/TLAType.java
+++ b/src/main/java/de/tla2b/types/TLAType.java
@@ -2,6 +2,7 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
public abstract class TLAType implements IType {
@@ -40,5 +41,4 @@ public abstract class TLAType implements IType {
public final String printObjectToString() {
return super.toString();
}
-
}
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index 001f3d1..8d03bd3 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -6,6 +6,7 @@ import java.util.List;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
public class TupleType extends AbstractHasFollowers {
private ArrayList<TLAType> types;
@@ -19,7 +20,7 @@ public class TupleType extends AbstractHasFollowers {
super(TUPLE);
ArrayList<TLAType> list = new ArrayList<TLAType>();
for (int i = 0; i < size; i++) {
- list.add(new Untyped());
+ list.add(new UntypedType());
}
setTypes(list);
}
@@ -135,8 +136,8 @@ public class TupleType extends AbstractHasFollowers {
if (!this.compare(o)) {
throw new UnificationException();
}
- if (o instanceof Untyped) {
- ((Untyped) o).setFollowersTo(this);
+ if (o instanceof UntypedType) {
+ ((UntypedType) o).setFollowersTo(this);
return this;
}
if (o instanceof TupleType) {
@@ -162,7 +163,7 @@ public class TupleType extends AbstractHasFollowers {
}
if (o instanceof FunctionType) {
// TODO
- if (compareToAll(new Untyped())) {
+ if (compareToAll(new UntypedType())) {
// Function
TLAType t = types.get(0);
for (int i = 1; i < types.size(); i++) {
@@ -219,4 +220,8 @@ public class TupleType extends AbstractHasFollowers {
return card;
}
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.caseTupleType(this);
+ }
+
}
diff --git a/src/main/java/de/tla2b/types/Untyped.java b/src/main/java/de/tla2b/types/UntypedType.java
similarity index 71%
rename from src/main/java/de/tla2b/types/Untyped.java
rename to src/main/java/de/tla2b/types/UntypedType.java
index 7b7b36d..5f4d74b 100644
--- a/src/main/java/de/tla2b/types/Untyped.java
+++ b/src/main/java/de/tla2b/types/UntypedType.java
@@ -2,10 +2,11 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.output.TypeVisitorInterface;
-public class Untyped extends AbstractHasFollowers {
+public class UntypedType extends AbstractHasFollowers {
- public Untyped() {
+ public UntypedType() {
super(UNTYPED);
}
@@ -43,12 +44,16 @@ public class Untyped extends AbstractHasFollowers {
}
@Override
- public Untyped cloneTLAType() {
- return new Untyped();
+ public UntypedType cloneTLAType() {
+ return new UntypedType();
}
@Override
public PExpression getBNode() {
return null;
}
+
+ public void apply(TypeVisitorInterface visitor) {
+ visitor.caseUntyped(this);
+ }
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 52efad9..6b98ba2 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -24,110 +24,14 @@ import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.StringNode;
import tla2sany.semantic.SymbolNode;
+import tla2tex.TLA;
import tlc2.tool.BuiltInOPs;
import tlc2.value.ModelValue;
import tlc2.value.SetEnumValue;
import tlc2.value.Value;
import tlc2.value.ValueConstants;
import de.be4.classicalb.core.parser.Definitions;
-import de.be4.classicalb.core.parser.node.AAbstractConstantsMachineClause;
-import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
-import de.be4.classicalb.core.parser.node.AAddExpression;
-import de.be4.classicalb.core.parser.node.AAnySubstitution;
-import de.be4.classicalb.core.parser.node.AAssignSubstitution;
-import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
-import de.be4.classicalb.core.parser.node.ABoolSetExpression;
-import de.be4.classicalb.core.parser.node.ABooleanFalseExpression;
-import de.be4.classicalb.core.parser.node.ABooleanTrueExpression;
-import de.be4.classicalb.core.parser.node.ACardExpression;
-import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
-import de.be4.classicalb.core.parser.node.AConcatExpression;
-import de.be4.classicalb.core.parser.node.AConjunctPredicate;
-import de.be4.classicalb.core.parser.node.AConvertBoolExpression;
-import de.be4.classicalb.core.parser.node.ACoupleExpression;
-import de.be4.classicalb.core.parser.node.ADefinitionExpression;
-import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
-import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
-import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
-import de.be4.classicalb.core.parser.node.ADivExpression;
-import de.be4.classicalb.core.parser.node.ADomainExpression;
-import de.be4.classicalb.core.parser.node.AEmptySequenceExpression;
-import de.be4.classicalb.core.parser.node.AEmptySetExpression;
-import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
-import de.be4.classicalb.core.parser.node.AEqualPredicate;
-import de.be4.classicalb.core.parser.node.AEquivalencePredicate;
-import de.be4.classicalb.core.parser.node.AExistsPredicate;
-import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.AExpressionParseUnit;
-import de.be4.classicalb.core.parser.node.AFinSubsetExpression;
-import de.be4.classicalb.core.parser.node.AFirstExpression;
-import de.be4.classicalb.core.parser.node.AForallPredicate;
-import de.be4.classicalb.core.parser.node.AFunctionExpression;
-import de.be4.classicalb.core.parser.node.AGeneralUnionExpression;
-import de.be4.classicalb.core.parser.node.AGreaterEqualPredicate;
-import de.be4.classicalb.core.parser.node.AGreaterPredicate;
-import de.be4.classicalb.core.parser.node.AIdentifierExpression;
-import de.be4.classicalb.core.parser.node.AImplicationPredicate;
-import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
-import de.be4.classicalb.core.parser.node.AInsertTailExpression;
-import de.be4.classicalb.core.parser.node.AIntegerExpression;
-import de.be4.classicalb.core.parser.node.AIntegerSetExpression;
-import de.be4.classicalb.core.parser.node.AIntersectionExpression;
-import de.be4.classicalb.core.parser.node.AIntervalExpression;
-import de.be4.classicalb.core.parser.node.AInvariantMachineClause;
-import de.be4.classicalb.core.parser.node.ALambdaExpression;
-import de.be4.classicalb.core.parser.node.ALessEqualPredicate;
-import de.be4.classicalb.core.parser.node.ALessPredicate;
-import de.be4.classicalb.core.parser.node.AMachineHeader;
-import de.be4.classicalb.core.parser.node.AMachineMachineVariant;
-import de.be4.classicalb.core.parser.node.AMemberPredicate;
-import de.be4.classicalb.core.parser.node.AMinusExpression;
-import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
-import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
-import de.be4.classicalb.core.parser.node.ANaturalSetExpression;
-import de.be4.classicalb.core.parser.node.ANegationPredicate;
-import de.be4.classicalb.core.parser.node.ANotEqualPredicate;
-import de.be4.classicalb.core.parser.node.ANotMemberPredicate;
-import de.be4.classicalb.core.parser.node.AOperation;
-import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
-import de.be4.classicalb.core.parser.node.AOverwriteExpression;
-import de.be4.classicalb.core.parser.node.APowSubsetExpression;
-import de.be4.classicalb.core.parser.node.APowerOfExpression;
-import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
-import de.be4.classicalb.core.parser.node.ARecEntry;
-import de.be4.classicalb.core.parser.node.ARecExpression;
-import de.be4.classicalb.core.parser.node.ARecordFieldExpression;
-import de.be4.classicalb.core.parser.node.ARestrictFrontExpression;
-import de.be4.classicalb.core.parser.node.ARestrictTailExpression;
-import de.be4.classicalb.core.parser.node.ASeqExpression;
-import de.be4.classicalb.core.parser.node.ASequenceExtensionExpression;
-import de.be4.classicalb.core.parser.node.ASetExtensionExpression;
-import de.be4.classicalb.core.parser.node.ASetsMachineClause;
-import de.be4.classicalb.core.parser.node.ASizeExpression;
-import de.be4.classicalb.core.parser.node.AStringExpression;
-import de.be4.classicalb.core.parser.node.AStringSetExpression;
-import de.be4.classicalb.core.parser.node.AStructExpression;
-import de.be4.classicalb.core.parser.node.ASubsetPredicate;
-import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.ATailExpression;
-import de.be4.classicalb.core.parser.node.ATotalFunctionExpression;
-import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
-import de.be4.classicalb.core.parser.node.AUnionExpression;
-import de.be4.classicalb.core.parser.node.AVariablesMachineClause;
-import de.be4.classicalb.core.parser.node.EOF;
-import de.be4.classicalb.core.parser.node.PDefinition;
-import de.be4.classicalb.core.parser.node.PExpression;
-import de.be4.classicalb.core.parser.node.PMachineClause;
-import de.be4.classicalb.core.parser.node.POperation;
-import de.be4.classicalb.core.parser.node.PPredicate;
-import de.be4.classicalb.core.parser.node.PRecEntry;
-import de.be4.classicalb.core.parser.node.PSet;
-import de.be4.classicalb.core.parser.node.Start;
-import de.be4.classicalb.core.parser.node.TDefLiteralPredicate;
-import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
-import de.be4.classicalb.core.parser.node.TIntegerLiteral;
-import de.be4.classicalb.core.parser.node.TStringLiteral;
+import de.be4.classicalb.core.parser.node.*;
import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.PredicateVsExpression;
import de.tla2b.analysis.RecursiveDefinition;
@@ -153,8 +57,8 @@ import de.tla2b.types.TLAType;
import de.tla2b.types.TupleType;
public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
- ASTConstants, IType, BBuildIns, Priorities, ValueConstants {
- Start start;
+ ASTConstants, BBuildIns, Priorities, ValueConstants {
+
List<PMachineClause> machineClauseList;
ConfigfileEvaluator conEval;
SpecAnalyser specAnalyser;
@@ -169,14 +73,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private Definitions bDefinitions = new Definitions();
- public Start getStartNode() {
- return start;
- }
-
- public Definitions getBDefinitions() {
- // used for the recursive machine loader
- return bDefinitions;
- }
+ private Start start;
+ private final Hashtable<Node, TLAType> typeTable = new Hashtable<Node, TLAType>();
public Start expressionStart;
@@ -501,6 +399,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
AIdentifierExpression id = new AIdentifierExpression(
createTIdentifierLiteral(getName(opDeclNode)));
list.add(id);
+ TLAType type = (TLAType) opDeclNode.getToolObject(TYPE_ID);
+ typeTable.put(id, type);
}
AVariablesMachineClause varClause = new AVariablesMachineClause(
list);
@@ -521,6 +421,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
AIdentifierExpression id = new AIdentifierExpression(
createTIdentifierLiteral(getName(opDeclNode)));
constantsList.add(id);
+ TLAType type = (TLAType) opDeclNode.getToolObject(TYPE_ID);
+ typeTable.put(id, type);
}
for (RecursiveDefinition recDef : specAnalyser
@@ -528,12 +430,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
AIdentifierExpression id = new AIdentifierExpression(
createTIdentifierLiteral(getName(recDef.getOpDefNode())));
constantsList.add(id);
+ TLAType type = (TLAType) recDef.getOpDefNode().getToolObject(TYPE_ID);
+ typeTable.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);
}
if (constantsList.size() > 0) {
@@ -541,6 +447,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
constantsList);
machineClauseList.add(abstractConstantsClause);
}
+
+
}
@@ -1421,7 +1329,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
AExistsPredicate exist = new AExistsPredicate();
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- ExprNode[] bounds = n.getBdedQuantBounds();
List<PExpression> idList = new ArrayList<PExpression>();
List<PPredicate> predList = new ArrayList<PPredicate>();
@@ -1593,7 +1500,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
List<PRecEntry> recList = new ArrayList<PRecEntry>();
if (struct.isExtensible()) {
for (int i = 0; i < struct.getFields().size(); i++) {
- String fieldName = struct.getFields().get(i); // name
+ String fieldName = struct.getFields().get(i); // name
AIdentifierExpression field = createIdentifierNode(fieldName);
ARecEntry rec = new ARecEntry();
rec.setIdentifier(field);
@@ -1679,7 +1586,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
rec.setValue(pairTable.get(fieldName));
} else {
// this struct is extensible
- throw new NotImplementedException("Missing case handling extensible structs.");
+ throw new NotImplementedException(
+ "Missing case handling extensible structs.");
}
recList.add(rec);
}
@@ -1760,7 +1668,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
case OPCODE_exc: // Except
{
TLAType type = (TLAType) n.getToolObject(TYPE_ID);
- if (type.getKind() == STRUCT) {
+ if (type.getKind() == IType.STRUCT) {
Hashtable<String, PExpression> temp = new Hashtable<String, PExpression>();
for (int i = 1; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
@@ -2266,4 +2174,18 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
list.add(expr);
return list;
}
+
+ public Start getStartNode() {
+ return start;
+ }
+
+ public Definitions getBDefinitions() {
+ // used for the recursive machine loader
+ return bDefinitions;
+ }
+
+ public Hashtable<Node, TLAType> getTypeTable() {
+ return this.typeTable;
+ }
+
}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 6095017..451acbc 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -9,11 +9,14 @@ import java.io.IOException;
import java.io.PrintWriter;
import java.io.Writer;
import java.util.Date;
+import java.util.HashMap;
+import java.util.Hashtable;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.analysis.InstanceTransformation;
import de.tla2b.analysis.PredicateVsExpression;
@@ -28,9 +31,11 @@ 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;
@@ -43,6 +48,7 @@ public class Translator implements TranslationGlobals {
private File moduleFile;
private File configFile;
private Start BAst;
+ private Hashtable<Node, TLAType> typeTable;
private Definitions bDefinitions;
@@ -216,6 +222,7 @@ public class Translator implements TranslationGlobals {
specAnalyser, usedExternalFunctions, predicateVsExpression,
bMacroHandler, recursiveFunctionHandler);
this.BAst = bAstCreator.getStartNode();
+ this.typeTable = bAstCreator.getTypeTable();
this.bDefinitions = bAstCreator.getBDefinitions();
return BAst;
}
@@ -240,8 +247,15 @@ public class Translator implements TranslationGlobals {
final RecursiveMachineLoader rml = parseAllMachines(getBAST(),
getModuleFile(), bParser);
//rml.printAsProlog(new PrintWriter(System.out), false);
- rml.printAsProlog(new PrintWriter(probFile), false);
+ //rml.printAsProlog(new PrintWriter(probFile), false);
+
+ String moduleName = FileUtils.removeExtention(moduleFile.getName());
+ PrologPrinter prologPrinter = new PrologPrinter(rml, bParser,
+ moduleFile, moduleName, typeTable);
+ prologPrinter.printAsProlog(new PrintWriter(probFile), false);
System.out.println(probFile.getAbsolutePath() + " created.");
+
+ prologPrinter.printAsProlog(new PrintWriter(System.out), false);
} catch (BException e) {
e.printStackTrace();
} catch (FileNotFoundException e) {
@@ -309,7 +323,6 @@ public class Translator implements TranslationGlobals {
final File f, final BParser bparser) throws BException {
final RecursiveMachineLoader rml = new RecursiveMachineLoader(
f.getParent(), bparser.getContentProvider());
-
rml.loadAllMachines(f, ast, null, bparser.getDefinitions(),
bparser.getPragmas());
return rml;
@@ -360,4 +373,8 @@ public class Translator implements TranslationGlobals {
return moduleFile;
}
+ public Hashtable<Node, TLAType> getTypeTable() {
+ return this.typeTable;
+ }
+
}
diff --git a/src/test/resources/regression/Club/Club.prob b/src/test/resources/regression/Club/Club.prob
index 8233cd6..a379719 100644
--- a/src/test/resources/regression/Club/Club.prob
+++ b/src/test/resources/regression/Club/Club.prob
@@ -1,3 +1,3 @@
parser_version('2014-03-12 22:57:52.564').
classical_b('Club',['/Users/hansen/git/tla2bAST/src/test/resources/regression/Club/Club.tla']).
-machine(abstract_machine(1,machine(2),machine_header(3,'Club',[]),[sets(4,[enumerated_set(5,'ENUM1',[identifier(6,n1),identifier(7,n2),identifier(8,n3)])]),abstract_constants(9,[identifier(10,capacity),identifier(11,'NAME'),identifier(12,total)]),properties(13,conjunct(14,conjunct(15,conjunct(16,conjunct(17,conjunct(18,member(19,identifier(20,capacity),integer_set(21)),equal(22,identifier(23,'NAME'),identifier(24,'ENUM1'))),member(25,identifier(26,total),integer_set(27))),conjunct(28,member(29,identifier(30,capacity),natural_set(31)),equal(32,identifier(33,capacity),integer(34,2)))),greater(35,card(36,identifier(37,'NAME')),identifier(38,capacity))),conjunct(39,member(40,identifier(41,total),natural_set(42)),greater(43,identifier(44,total),integer(45,2))))),variables(46,[identifier(47,member),identifier(48,waiting)]),invariant(49,conjunct(50,member(51,identifier(52,member),pow_subset(53,identifier(54,'ENUM1'))),member(55,identifier(56,waiting),pow_subset(57,identifier(58,'ENUM1'))))),initialisation(59,becomes_such(60,[identifier(61,member),identifier(62,waiting)],conjunct(63,equal(64,identifier(65,member),empty_set(66)),equal(67,identifier(68,waiting),empty_set(69))))),operations(70,[operation(71,identifier(71,join_queue),[],[identifier(72,nn)],any(73,[identifier(74,member_n)],conjunct(75,conjunct(76,conjunct(77,conjunct(78,conjunct(79,member(80,identifier(81,nn),identifier(82,'NAME')),not_member(83,identifier(84,nn),identifier(85,member))),not_member(86,identifier(87,nn),identifier(88,waiting))),member(89,identifier(90,member_n),pow_subset(91,identifier(92,'ENUM1')))),less(93,card(94,identifier(95,waiting)),identifier(96,total))),equal(97,identifier(98,member_n),identifier(99,member))),assign(100,[identifier(101,waiting),identifier(102,member)],[union(103,identifier(104,waiting),set_extension(105,[identifier(106,nn)])),identifier(107,member_n)]))),operation(108,identifier(108,join),[],[identifier(109,nn)],select(110,conjunct(111,conjunct(112,conjunct(113,member(114,identifier(115,nn),identifier(116,'NAME')),member(117,identifier(118,nn),identifier(119,waiting))),less(120,card(121,identifier(122,member)),identifier(123,capacity))),less(124,card(125,identifier(126,member)),identifier(127,capacity))),assign(128,[identifier(129,member),identifier(130,waiting)],[union(131,identifier(132,member),set_extension(133,[identifier(134,nn)])),minus_or_set_subtract(135,identifier(136,waiting),set_extension(137,[identifier(138,nn)]))]),[])),operation(139,identifier(139,remove),[],[identifier(140,nn)],any(141,[identifier(142,waiting_n)],conjunct(143,conjunct(144,conjunct(145,member(146,identifier(147,nn),identifier(148,'NAME')),member(149,identifier(150,nn),identifier(151,member))),member(152,identifier(153,waiting_n),pow_subset(154,identifier(155,'ENUM1')))),equal(156,identifier(157,waiting_n),identifier(158,waiting))),assign(159,[identifier(160,member),identifier(161,waiting)],[minus_or_set_subtract(162,identifier(163,member),set_extension(164,[identifier(165,nn)])),identifier(166,waiting_n)])))])])).
+machine(abstract_machine(info(1,tla_type(none)),machine(info(2,tla_type(none))),machine_header(info(3,tla_type(none)),'Club',[]),[sets(info(4,tla_type(none)),[enumerated_set(info(5,tla_type(none)),'ENUM1',[identifier(info(6,tla_type(none)),n1),identifier(info(7,tla_type(none)),n2),identifier(info(8,tla_type(none)),n3)])]),abstract_constants(info(9,tla_type(none)),[identifier(info(10,tla_type(integer)),capacity),identifier(info(11,tla_type(set(modelvalue))),'NAME'),identifier(info(12,tla_type(integer)),total)]),properties(info(13,tla_type(none)),conjunct(info(14,tla_type(none)),conjunct(info(15,tla_type(none)),conjunct(info(16,tla_type(none)),conjunct(info(17,tla_type(none)),conjunct(info(18,tla_type(none)),member(info(19,tla_type(none)),identifier(info(20,tla_type(none)),capacity),integer_set(info(21,tla_type(none)))),equal(info(22,tla_type(none)),identifier(info(23,tla_type(none)),'NAME'),identifier(info(24,tla_type(none)),'ENUM1'))),member(info(25,tla_type(none)),identifier(info(26,tla_type(none)),total),integer_set(info(27,tla_type(none))))),conjunct(info(28,tla_type(none)),member(info(29,tla_type(none)),identifier(info(30,tla_type(none)),capacity),natural_set(info(31,tla_type(none)))),equal(info(32,tla_type(none)),identifier(info(33,tla_type(none)),capacity),integer(info(34,tla_type(none)),2)))),greater(info(35,tla_type(none)),card(info(36,tla_type(none)),identifier(info(37,tla_type(none)),'NAME')),identifier(info(38,tla_type(none)),capacity))),conjunct(info(39,tla_type(none)),member(info(40,tla_type(none)),identifier(info(41,tla_type(none)),total),natural_set(info(42,tla_type(none)))),greater(info(43,tla_type(none)),identifier(info(44,tla_type(none)),total),integer(info(45,tla_type(none)),2))))),variables(info(46,tla_type(none)),[identifier(info(47,tla_type(set(modelvalue))),member),identifier(info(48,tla_type(set(modelvalue))),waiting)]),invariant(info(49,tla_type(none)),conjunct(info(50,tla_type(none)),member(info(51,tla_type(none)),identifier(info(52,tla_type(none)),member),pow_subset(info(53,tla_type(none)),identifier(info(54,tla_type(none)),'ENUM1'))),member(info(55,tla_type(none)),identifier(info(56,tla_type(none)),waiting),pow_subset(info(57,tla_type(none)),identifier(info(58,tla_type(none)),'ENUM1'))))),initialisation(info(59,tla_type(none)),becomes_such(info(60,tla_type(none)),[identifier(info(61,tla_type(none)),member),identifier(info(62,tla_type(none)),waiting)],conjunct(info(63,tla_type(none)),equal(info(64,tla_type(none)),identifier(info(65,tla_type(none)),member),empty_set(info(66,tla_type(none)))),equal(info(67,tla_type(none)),identifier(info(68,tla_type(none)),waiting),empty_set(info(69,tla_type(none))))))),operations(info(70,tla_type(none)),[operation(info(71,tla_type(none)),identifier(info(71,tla_type(none)),join_queue),[],[identifier(info(72,tla_type(none)),nn)],any(info(73,tla_type(none)),[identifier(info(74,tla_type(none)),member_n)],conjunct(info(75,tla_type(none)),conjunct(info(76,tla_type(none)),conjunct(info(77,tla_type(none)),conjunct(info(78,tla_type(none)),conjunct(info(79,tla_type(none)),member(info(80,tla_type(none)),identifier(info(81,tla_type(none)),nn),identifier(info(82,tla_type(none)),'NAME')),not_member(info(83,tla_type(none)),identifier(info(84,tla_type(none)),nn),identifier(info(85,tla_type(none)),member))),not_member(info(86,tla_type(none)),identifier(info(87,tla_type(none)),nn),identifier(info(88,tla_type(none)),waiting))),member(info(89,tla_type(none)),identifier(info(90,tla_type(none)),member_n),pow_subset(info(91,tla_type(none)),identifier(info(92,tla_type(none)),'ENUM1')))),less(info(93,tla_type(none)),card(info(94,tla_type(none)),identifier(info(95,tla_type(none)),waiting)),identifier(info(96,tla_type(none)),total))),equal(info(97,tla_type(none)),identifier(info(98,tla_type(none)),member_n),identifier(info(99,tla_type(none)),member))),assign(info(100,tla_type(none)),[identifier(info(101,tla_type(none)),waiting),identifier(info(102,tla_type(none)),member)],[union(info(103,tla_type(none)),identifier(info(104,tla_type(none)),waiting),set_extension(info(105,tla_type(none)),[identifier(info(106,tla_type(none)),nn)])),identifier(info(107,tla_type(none)),member_n)]))),operation(info(108,tla_type(none)),identifier(info(108,tla_type(none)),join),[],[identifier(info(109,tla_type(none)),nn)],select(info(110,tla_type(none)),conjunct(info(111,tla_type(none)),conjunct(info(112,tla_type(none)),conjunct(info(113,tla_type(none)),member(info(114,tla_type(none)),identifier(info(115,tla_type(none)),nn),identifier(info(116,tla_type(none)),'NAME')),member(info(117,tla_type(none)),identifier(info(118,tla_type(none)),nn),identifier(info(119,tla_type(none)),waiting))),less(info(120,tla_type(none)),card(info(121,tla_type(none)),identifier(info(122,tla_type(none)),member)),identifier(info(123,tla_type(none)),capacity))),less(info(124,tla_type(none)),card(info(125,tla_type(none)),identifier(info(126,tla_type(none)),member)),identifier(info(127,tla_type(none)),capacity))),assign(info(128,tla_type(none)),[identifier(info(129,tla_type(none)),member),identifier(info(130,tla_type(none)),waiting)],[union(info(131,tla_type(none)),identifier(info(132,tla_type(none)),member),set_extension(info(133,tla_type(none)),[identifier(info(134,tla_type(none)),nn)])),minus_or_set_subtract(info(135,tla_type(none)),identifier(info(136,tla_type(none)),waiting),set_extension(info(137,tla_type(none)),[identifier(info(138,tla_type(none)),nn)]))]),[])),operation(info(139,tla_type(none)),identifier(info(139,tla_type(none)),remove),[],[identifier(info(140,tla_type(none)),nn)],any(info(141,tla_type(none)),[identifier(info(142,tla_type(none)),waiting_n)],conjunct(info(143,tla_type(none)),conjunct(info(144,tla_type(none)),conjunct(info(145,tla_type(none)),member(info(146,tla_type(none)),identifier(info(147,tla_type(none)),nn),identifier(info(148,tla_type(none)),'NAME')),member(info(149,tla_type(none)),identifier(info(150,tla_type(none)),nn),identifier(info(151,tla_type(none)),member))),member(info(152,tla_type(none)),identifier(info(153,tla_type(none)),waiting_n),pow_subset(info(154,tla_type(none)),identifier(info(155,tla_type(none)),'ENUM1')))),equal(info(156,tla_type(none)),identifier(info(157,tla_type(none)),waiting_n),identifier(info(158,tla_type(none)),waiting))),assign(info(159,tla_type(none)),[identifier(info(160,tla_type(none)),member),identifier(info(161,tla_type(none)),waiting)],[minus_or_set_subtract(info(162,tla_type(none)),identifier(info(163,tla_type(none)),member),set_extension(info(164,tla_type(none)),[identifier(info(165,tla_type(none)),nn)])),identifier(info(166,tla_type(none)),waiting_n)])))])])).
--
GitLab