diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 48626c94fe8494a27793e46764c7407a8294e0b6..9502ab7495bda11a843b5ee3840aa0e76aed7a1c 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -111,7 +111,6 @@ public class Translator {
}
public void translate() {
-
UnsupportedConstructsFinder unsupportedConstructsFinder = new UnsupportedConstructsFinder(start);
unsupportedConstructsFinder.find();
@@ -123,7 +122,15 @@ public class Translator {
// TODO move set comprehension optimizer behind the type checker
SetComprehensionOptimizer.optimizeSetComprehensions(start);
- MachineContext machineContext = new MachineContext(machineName, start, ltlFormula, constantsSetup);
+ MachineContext machineContext = new MachineContext(machineName, start);
+ if (ltlFormula != null) {
+ machineContext.addLTLFromula(this.ltlFormula);
+ }
+ if (this.constantsSetup != null) {
+ machineContext.setConstantSetupPredicate(constantsSetup);
+ }
+ machineContext.analyseMachine();
+
this.machineName = machineContext.getMachineName();
if (machineContext.machineContainsOperations()) {
TLC4BGlobals.setPrintCoverage(true);
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 74c1eceef27618b8fd2e2ba6762afe891a342d55..102c2c6d1f2530841b90a39f272f783a168a4a00 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -75,30 +75,24 @@ import de.tlc4b.ltl.LTLFormulaVisitor;
public class MachineContext extends DepthFirstAdapter {
private String machineName;
- private PMachineHeader header;
private final Start start;
- private final Hashtable<String, MachineContext> machineContextsTable;
+
private final ArrayList<LTLFormulaVisitor> ltlVisitors;
- private final PPredicate constantsSetup;
+ private PPredicate constantsSetupPredicate;
+ private boolean hasConstants = false;
- private boolean constantSetupInTraceFile = false;
- // machine identifier
private final LinkedHashMap<String, Node> machineSetParameter;
private final LinkedHashMap<String, Node> machineScalarParameter;
-
private final LinkedHashMap<String, Node> deferredSets;
private final LinkedHashMap<String, Node> enumeratedSets;
private final LinkedHashMap<String, Node> enumValues;
-
- private LinkedHashMap<String, Node> constants;
- private final LinkedHashMap<String, Node> bMachineConstants;
-
private final LinkedHashMap<String, Node> variables;
+ private final LinkedHashMap<String, Node> constants;
private final LinkedHashMap<String, Node> definitions;
private final LinkedHashMap<String, Node> operations;
private final LinkedHashMap<String, AIdentifierExpression> seenMachines;
- // machine clauses
+ private PMachineHeader header;
private AAbstractMachineParseUnit abstractMachineParseUnit;
private AConstraintsMachineClause constraintMachineClause;
private ASeesMachineClause seesMachineClause;
@@ -108,26 +102,18 @@ public class MachineContext extends DepthFirstAdapter {
private AInvariantMachineClause invariantMachineClause;
private AInitialisationMachineClause initialisationMachineClause;
private AOperationsMachineClause operationMachineClause;
- private AAssertionsMachineClause assertionMachineClause;
+ private AAssertionsMachineClause assertiondMachineClause;
private ArrayList<LinkedHashMap<String, Node>> contextTable;
protected final Hashtable<Node, Node> referencesTable;
- public MachineContext(String machineName, Start start, String ltlFormula, PPredicate constantsSetup) {
+ public MachineContext(final String machineName, final Start start) {
this.start = start;
this.machineName = machineName;
- this.constantsSetup = constantsSetup;
this.referencesTable = new Hashtable<Node, Node>();
this.ltlVisitors = new ArrayList<LTLFormulaVisitor>();
- LTLFormulaVisitor ltlVisitor = null;
- if (null != ltlFormula) {
- ltlVisitor = new LTLFormulaVisitor("ltl", this);
- ltlVisitor.parseLTLString(ltlFormula);
- this.ltlVisitors.add(ltlVisitor);
- }
-
this.machineSetParameter = new LinkedHashMap<String, Node>();
this.machineScalarParameter = new LinkedHashMap<String, Node>();
@@ -135,28 +121,34 @@ public class MachineContext extends DepthFirstAdapter {
this.enumeratedSets = new LinkedHashMap<String, Node>();
this.enumValues = new LinkedHashMap<String, Node>();
this.constants = new LinkedHashMap<String, Node>();
- this.bMachineConstants = new LinkedHashMap<String, Node>();
this.variables = new LinkedHashMap<String, Node>();
this.definitions = new LinkedHashMap<String, Node>();
this.operations = new LinkedHashMap<String, Node>();
this.seenMachines = new LinkedHashMap<String, AIdentifierExpression>();
+ }
- this.machineContextsTable = new Hashtable<String, MachineContext>();
- start.apply(this);
-
+ public void analyseMachine() {
+ this.start.apply(this);
+ checkConstantsSetup();
checkLTLFormulas();
+ }
- checkConstantsSetup();
+ public void addLTLFromula(final String ltlFormula) {
+ LTLFormulaVisitor ltlVisitor = new LTLFormulaVisitor("ltl", this);
+ ltlVisitor.parseLTLString(ltlFormula);
+ this.ltlVisitors.add(ltlVisitor);
+ }
+
+ public void setConstantSetupPredicate(final PPredicate constantsSetup) {
+ this.constantsSetupPredicate = constantsSetup;
}
private void checkConstantsSetup() {
- if (constantsSetup == null) {
+ if (constantsSetupPredicate == null) {
return;
}
-
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
-
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
contextTable.add(s.getDeferredSets());
@@ -165,8 +157,7 @@ public class MachineContext extends DepthFirstAdapter {
contextTable.add(s.getConstants());
contextTable.add(s.getDefinitions());
}
- constantsSetup.apply(this);
-
+ constantsSetupPredicate.apply(this);
}
private void checkLTLFormulas() {
@@ -174,17 +165,17 @@ public class MachineContext extends DepthFirstAdapter {
ltlVisitors.get(0).start();
return;
}
- ArrayList<LTLFormulaVisitor> notSupportedLTLFormulas = new ArrayList<LTLFormulaVisitor>();
+ ArrayList<LTLFormulaVisitor> formulasNotSupportedByTLC = new ArrayList<LTLFormulaVisitor>();
for (int i = 0; i < ltlVisitors.size(); i++) {
LTLFormulaVisitor visitor = ltlVisitors.get(i);
try {
visitor.start();
} catch (ScopeException e) {
MP.println("Warning: LTL formula '" + visitor.getName() + "' cannot be checked by TLC.");
- notSupportedLTLFormulas.add(visitor);
+ formulasNotSupportedByTLC.add(visitor);
}
}
- ltlVisitors.removeAll(notSupportedLTLFormulas);
+ ltlVisitors.removeAll(formulasNotSupportedByTLC);
}
public void checkLTLBPredicate(LTLBPredicate ltlbPredicate) {
@@ -310,7 +301,7 @@ public class MachineContext extends DepthFirstAdapter {
*/
copy.removeAll(definitionsToRemove);
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
contextTable.add(s.getDeferredSets());
@@ -442,20 +433,19 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- constantSetupInTraceFile = true;
+ hasConstants = true;
List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression c = (AIdentifierExpression) e;
String name = Utils.getIdentifierAsString(c.getIdentifier());
exist(c.getIdentifier());
constants.put(name, c);
- bMachineConstants.put(name, c);
}
}
@Override
public void caseAAbstractConstantsMachineClause(AAbstractConstantsMachineClause node) {
- constantSetupInTraceFile = true;
+ hasConstants = true;
List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression c = (AIdentifierExpression) e;
@@ -523,15 +513,8 @@ public class MachineContext extends DepthFirstAdapter {
throw new ScopeException("Unkown Identifier: '" + name + "' at position: " + node.getStartPos());
}
- private ArrayList<MachineContext> lookupExtendedMachines() {
+ private ArrayList<MachineContext> lookupReferencedMachines() {
ArrayList<MachineContext> list = new ArrayList<MachineContext>();
- for (Entry<String, AIdentifierExpression> entry : seenMachines.entrySet()) {
- String s = entry.getKey();
- AIdentifierExpression value = entry.getValue();
- if (value.getIdentifier().size() == 1) {
- list.add(machineContextsTable.get(s));
- }
- }
list.add(this);
return list;
}
@@ -551,14 +534,13 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
this.propertiesMachineClause = node;
- constantSetupInTraceFile = true;
+ hasConstants = true;
/**
* check identifier scope in properties clauses
*/
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
-
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
contextTable.add(s.getDeferredSets());
@@ -567,7 +549,6 @@ public class MachineContext extends DepthFirstAdapter {
contextTable.add(s.getConstants());
contextTable.add(s.getDefinitions());
}
-
if (node.getPredicates() != null) {
node.getPredicates().apply(this);
}
@@ -579,7 +560,7 @@ public class MachineContext extends DepthFirstAdapter {
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
this.contextTable.add(s.getSetParamter());
@@ -596,10 +577,10 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAAssertionsMachineClause(AAssertionsMachineClause node) {
- this.assertionMachineClause = node;
+ this.assertiondMachineClause = node;
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
this.contextTable.add(s.getSetParamter());
@@ -624,7 +605,7 @@ public class MachineContext extends DepthFirstAdapter {
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
@@ -646,7 +627,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAOperationsMachineClause(AOperationsMachineClause node) {
this.operationMachineClause = node;
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
this.contextTable.add(s.getSetParamter());
@@ -937,16 +918,12 @@ public class MachineContext extends DepthFirstAdapter {
return header;
}
- public Start getTree() {
+ public Start getStartNode() {
return start;
}
public LinkedHashMap<String, Node> getSetParamter() {
- return machineSetParameter;
- }
-
- public LinkedHashMap<String, Node> getScalarParameter() {
- return machineScalarParameter;
+ return new LinkedHashMap<>(machineSetParameter);
}
public ArrayList<Node> getConstantArrayList() {
@@ -957,36 +934,40 @@ public class MachineContext extends DepthFirstAdapter {
return list;
}
+ public LinkedHashMap<String, Node> getScalarParameter() {
+ return new LinkedHashMap<>(machineScalarParameter);
+ }
+
public LinkedHashMap<String, Node> getConstants() {
return constants;
}
public LinkedHashMap<String, Node> getDefinitions() {
- return definitions;
+ return new LinkedHashMap<>(definitions);
}
public LinkedHashMap<String, Node> getVariables() {
- return variables;
+ return new LinkedHashMap<>(variables);
}
public LinkedHashMap<String, Node> getOperations() {
- return operations;
+ return new LinkedHashMap<>(operations);
}
public LinkedHashMap<String, Node> getDeferredSets() {
- return deferredSets;
+ return new LinkedHashMap<>(deferredSets);
}
public LinkedHashMap<String, Node> getEnumeratedSets() {
- return enumeratedSets;
+ return new LinkedHashMap<>(enumeratedSets);
}
public LinkedHashMap<String, Node> getEnumValues() {
- return enumValues;
+ return new LinkedHashMap<>(enumValues);
}
public LinkedHashMap<String, AIdentifierExpression> getSeenMachines() {
- return seenMachines;
+ return new LinkedHashMap<>(seenMachines);
}
protected Hashtable<Node, Node> getReferences() {
@@ -1005,10 +986,6 @@ public class MachineContext extends DepthFirstAdapter {
return ltlVisitors;
}
- /*
- * machine clauses getter
- */
-
public AAbstractMachineParseUnit getAbstractMachineParseUnit() {
return abstractMachineParseUnit;
}
@@ -1030,7 +1007,7 @@ public class MachineContext extends DepthFirstAdapter {
}
public AAssertionsMachineClause getAssertionMachineClause() {
- return assertionMachineClause;
+ return assertiondMachineClause;
}
public void setPropertiesMachineClaus(APropertiesMachineClause propertiesMachineClause) {
@@ -1062,15 +1039,11 @@ public class MachineContext extends DepthFirstAdapter {
}
public PPredicate getConstantsSetup() {
- return constantsSetup;
- }
-
- public boolean constantSetupInTraceFile() {
- return constantSetupInTraceFile;
+ return constantsSetupPredicate;
}
- public LinkedHashMap<String, Node> getBMachineConstants() {
- return bMachineConstants;
+ public boolean hasConstants() {
+ return hasConstants;
}
}
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index b2c0c5d03509d888d069f2ab5e414ae3135c3e18..864e506ee3bdb55cdf626275d8d9806f6c7bcec4 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -111,7 +111,7 @@ public class Renamer extends DepthFirstAdapter {
evalDefinitions();
- machineContext.getTree().apply(this);
+ machineContext.getStartNode().apply(this);
}
private void evalEnumValues() {
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index 256b4ea1a43388c378e9f9b85e345d3868d9c865..d9919c7acc51fa75bc77012532e28f61783a9e91 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -19,7 +19,7 @@ import de.tlc4b.btypes.ITypechecker;
import de.tlc4b.btypes.IntegerOrSetOfPairType;
import de.tlc4b.btypes.IntegerOrSetType;
import de.tlc4b.btypes.IntegerType;
-import de.tlc4b.btypes.ModelValueType;
+import de.tlc4b.btypes.EnumeratedSetElement;
import de.tlc4b.btypes.PairType;
import de.tlc4b.btypes.SetType;
import de.tlc4b.btypes.StringType;
@@ -40,31 +40,21 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
private final Hashtable<Node, Node> referenceTable;
private final MachineContext machineContext;
- public Typechecker(MachineContext machineContext,
- Hashtable<String, MachineContext> contextTable,
- Hashtable<String, Typechecker> typecheckerTable) {
- this.machineContext = machineContext;
- this.types = new Hashtable<Node, BType>();
- this.referenceTable = machineContext.getReferences();
- }
-
public Typechecker(MachineContext context) {
this.types = new Hashtable<Node, BType>();
this.referenceTable = context.getReferences();
this.machineContext = context;
- context.getTree().apply(this);
- checkLTLFormulas();
+ context.getStartNode().apply(this);
checkConstantsSetup();
-
+ checkLTLFormulas();
}
private void checkLTLFormulas() {
ArrayList<LTLFormulaVisitor> visitors = machineContext.getLTLFormulas();
for (int i = 0; i < visitors.size(); i++) {
LTLFormulaVisitor visitor = visitors.get(i);
- Collection<AIdentifierExpression> parameter = visitor
- .getParameter();
+ Collection<AIdentifierExpression> parameter = visitor.getParameter();
for (AIdentifierExpression param : parameter) {
setType(param, new UntypedType());
}
@@ -81,14 +71,11 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
if (p != null) {
setType(p, BoolType.getInstance());
p.apply(this);
- for (Entry<String, Node> entry : machineContext.getConstants()
- .entrySet()) {
+ for (Entry<String, Node> entry : machineContext.getConstants().entrySet()) {
String c = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
- throw new TypeErrorException(
- "Can not infer type of constant '" + c + "': "
- + getType(n));
+ throw new TypeErrorException("Can not infer type of constant '" + c + "': " + getType(n));
}
}
}
@@ -107,8 +94,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
}
- public void updateType(Node node, AbstractHasFollowers oldType,
- BType newType) {
+ public void updateType(Node node, AbstractHasFollowers oldType, BType newType) {
oldType.deleteFollower(node);
this.types.put(node, newType);
if (newType instanceof AbstractHasFollowers) {
@@ -119,8 +105,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public BType getType(Node node) {
BType res = types.get(node);
if (res == null) {
- new TypeErrorException("Node '" + node + "' has not type.\n"
- + node.getStartPos());
+ new TypeErrorException("Node '" + node + "' has no type.\n" + node.getStartPos());
}
return res;
}
@@ -134,8 +119,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getHeader().apply(this);
}
{
- List<PMachineClause> copy = new ArrayList<PMachineClause>(
- node.getMachineClauses());
+ List<PMachineClause> copy = new ArrayList<PMachineClause>(node.getMachineClauses());
for (PMachineClause e : copy) {
e.apply(this);
}
@@ -148,15 +132,14 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAMachineHeader(AMachineHeader node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
AIdentifierExpression p = (AIdentifierExpression) e;
String name = Utils.getIdentifierAsString(p.getIdentifier());
if (Character.isUpperCase(name.charAt(0))) {
- ModelValueType m = new ModelValueType(name);
+ EnumeratedSetElement m = new EnumeratedSetElement(name);
setType(p, new SetType(m));
} else {
UntypedType u = new UntypedType();
@@ -175,11 +158,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAEnumeratedSetSet(AEnumeratedSetSet node) {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getIdentifier());
+ List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
String setName = Utils.getIdentifierAsString(copy);
- SetType set = new SetType(new ModelValueType(setName));
+ SetType set = new SetType(new EnumeratedSetElement(setName));
setType(node, set);
List<PExpression> copy2 = new ArrayList<PExpression>(node.getElements());
for (PExpression e : copy2) {
@@ -189,16 +171,14 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseADeferredSetSet(ADeferredSetSet node) {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getIdentifier());
+ List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
String name = Utils.getIdentifierAsString(copy);
- setType(node, new SetType(new ModelValueType(name)));
+ setType(node, new SetType(new EnumeratedSetElement(name)));
}
@Override
public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -207,10 +187,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAAbstractConstantsMachineClause(
- AAbstractConstantsMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseAAbstractConstantsMachineClause(AAbstractConstantsMachineClause node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -220,8 +198,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAVariablesMachineClause(AVariablesMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -230,10 +207,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAConcreteVariablesMachineClause(
- AConcreteVariablesMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -247,8 +222,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
- List<PDefinition> copy = new ArrayList<PDefinition>(
- node.getDefinitions());
+ List<PDefinition> copy = new ArrayList<PDefinition>(node.getDefinitions());
for (PDefinition e : copy) {
setType(e, new UntypedType());
}
@@ -260,10 +234,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
// d(a) == 1
- public void caseAExpressionDefinitionDefinition(
- AExpressionDefinitionDefinition node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ public void caseAExpressionDefinitionDefinition(AExpressionDefinitionDefinition node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
UntypedType u = new UntypedType();
setType(e, u);
@@ -274,11 +246,9 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
// d(a) == 1 = 1
- public void caseAPredicateDefinitionDefinition(
- APredicateDefinitionDefinition node) {
+ public void caseAPredicateDefinitionDefinition(APredicateDefinitionDefinition node) {
setType(node, BoolType.getInstance());
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
setType(e, new UntypedType());
}
@@ -296,13 +266,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected + "', found '"
- + found + "' at definition call\n");
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "' at definition call\n");
}
- LinkedList<PExpression> params = ((AExpressionDefinitionDefinition) originalDef)
- .getParameters();
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ LinkedList<PExpression> params = ((AExpressionDefinitionDefinition) originalDef).getParameters();
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (int i = 0; i < params.size(); i++) {
BType type = getType(params.get(i));
setType(copy.get(i), type);
@@ -319,13 +286,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected + "', found '"
- + found + "' at definition call\n");
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "' at definition call\n");
}
- LinkedList<PExpression> params = ((APredicateDefinitionDefinition) originalDef)
- .getParameters();
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ LinkedList<PExpression> params = ((APredicateDefinitionDefinition) originalDef).getParameters();
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (int i = 0; i < params.size(); i++) {
setType(copy.get(i), getType(params.get(i)));
copy.get(i).apply(this);
@@ -342,13 +306,11 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
}
- for (Entry<String, Node> entry : machineContext.getScalarParameter()
- .entrySet()) {
+ for (Entry<String, Node> entry : machineContext.getScalarParameter().entrySet()) {
String name = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
- throw new TypeErrorException(
- "Can not infer type of parameter '" + name + "'");
+ throw new TypeErrorException("Can not infer type of parameter '" + name + "'");
}
}
}
@@ -359,13 +321,11 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
}
- for (Entry<String, Node> entry : machineContext.getConstants()
- .entrySet()) {
+ for (Entry<String, Node> entry : machineContext.getConstants().entrySet()) {
String c = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
- throw new TypeErrorException("Can not infer type of constant '"
- + c + "': " + getType(n));
+ throw new TypeErrorException("Can not infer type of constant '" + c + "': " + getType(n));
}
}
}
@@ -374,13 +334,11 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseAInvariantMachineClause(AInvariantMachineClause node) {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
- for (Entry<String, Node> entry : machineContext.getVariables()
- .entrySet()) {
+ for (Entry<String, Node> entry : machineContext.getVariables().entrySet()) {
String c = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
- throw new TypeErrorException("Can not infer type of variable '"
- + c + "'");
+ throw new TypeErrorException("Can not infer type of variable '" + c + "'");
}
}
}
@@ -395,8 +353,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAInitialisationMachineClause(
- AInitialisationMachineClause node) {
+ public void caseAInitialisationMachineClause(AInitialisationMachineClause node) {
if (node.getSubstitutions() != null) {
node.getSubstitutions().apply(this);
}
@@ -405,8 +362,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAOperation(AOperation node) {
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getReturnValues());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getReturnValues());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -415,8 +371,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -434,23 +389,22 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
- Node originalIdentifier = referenceTable.get(node);
+
BType expected = getType(node);
if (expected == null) {
- System.out.println("Not implemented in Typechecker:"
- + node.parent().getClass());
+ System.out.println("Not implemented in Typechecker:" + node.parent().getClass());
throw new RuntimeException(node + " Pos: " + node.getStartPos());
}
- BType found = getType(originalIdentifier);
+ Node identifierDeclarationNode = referenceTable.get(node);
+ BType found = getType(identifierDeclarationNode);
String name = Utils.getIdentifierAsString(node.getIdentifier());
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + found + "' at identifier " + name + "\n"
- + node.getStartPos());
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + found + "' at identifier " + name
+ + "\n" + node.getStartPos());
}
}
@@ -459,8 +413,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + getType(node)
- + "', found BOOL at '=' \n" + node.getStartPos());
+ throw new TypeErrorException("Expected '" + getType(node) + "', found BOOL at '=' \n" + node.getStartPos());
}
UntypedType x = new UntypedType();
@@ -475,8 +428,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + getType(node)
- + "', found BOOL at '=' \n" + node.getClass());
+ throw new TypeErrorException("Expected '" + getType(node) + "', found BOOL at '=' \n" + node.getClass());
}
UntypedType x = new UntypedType();
@@ -491,12 +443,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + getType(node)
- + "', found BOOL at 'For All' \n");
+ throw new TypeErrorException("Expected '" + getType(node) + "', found BOOL at 'For All' \n");
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -511,12 +461,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + getType(node)
- + "', found BOOL at 'Exists' \n");
+ throw new TypeErrorException("Expected '" + getType(node) + "', found BOOL at 'Exists' \n");
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -550,8 +498,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getCondition(), BoolType.getInstance());
node.getCondition().apply(this);
node.getThen().apply(this);
- List<PSubstitution> copy = new ArrayList<PSubstitution>(
- node.getWhenSubstitutions());
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(node.getWhenSubstitutions());
for (PSubstitution e : copy) {
e.apply(this);
}
@@ -572,8 +519,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getCondition(), BoolType.getInstance());
node.getCondition().apply(this);
node.getThen().apply(this);
- List<PSubstitution> copy = new ArrayList<PSubstitution>(
- node.getElsifSubstitutions());
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(node.getElsifSubstitutions());
for (PSubstitution e : copy) {
e.apply(this);
}
@@ -591,10 +537,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAAssignSubstitution(AAssignSubstitution node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getLhsExpression());
- List<PExpression> copy2 = new ArrayList<PExpression>(
- node.getRhsExpressions());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getLhsExpression());
+ List<PExpression> copy2 = new ArrayList<PExpression>(node.getRhsExpressions());
for (int i = 0; i < copy.size(); i++) {
PExpression left = copy.get(i);
@@ -617,10 +561,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseABecomesElementOfSubstitution(
- ABecomesElementOfSubstitution node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseABecomesElementOfSubstitution(ABecomesElementOfSubstitution node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
SetType set = new SetType(new UntypedType());
setType(node.getSet(), set);
@@ -635,8 +577,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAAnySubstitution(AAnySubstitution node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -648,8 +589,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseALetSubstitution(ALetSubstitution node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -668,9 +608,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in '" + node.getLiteral().getText()
- + "'");
+ throw new TypeErrorException(
+ "Excepted '" + getType(node) + "' , found 'INTEGER' in '" + node.getLiteral().getText() + "'");
}
}
@@ -680,8 +619,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'INTEGER'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'INTEGER'");
}
}
@@ -691,8 +629,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'NATURAL'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'NATURAL'");
}
}
@@ -702,8 +639,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'NATURAL1'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'NATURAL1'");
}
}
@@ -713,8 +649,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'INT'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'INT'");
}
}
@@ -724,8 +659,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'NAT'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'NAT'");
}
}
@@ -735,8 +669,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'NAT1'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'NAT1'");
}
}
@@ -745,8 +678,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in '-'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in '-'");
}
}
@@ -756,8 +688,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' at interval operator");
+ throw new TypeErrorException(
+ "Excepted '" + getType(node) + "' , found 'POW(INTEGER)' at interval operator");
}
setType(node.getLeftBorder(), IntegerType.getInstance());
@@ -781,8 +713,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' > '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' > '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -795,8 +726,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' < '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' < '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -809,8 +739,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' >= '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' >= '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -823,8 +752,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' <= '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' <= '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -837,8 +765,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' min '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' min '");
}
setType(node.getExpression(), new SetType(IntegerType.getInstance()));
node.getExpression().apply(this);
@@ -849,8 +776,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' min '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' min '");
}
setType(node.getExpression(), new SetType(IntegerType.getInstance()));
node.getExpression().apply(this);
@@ -861,8 +787,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' + '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' + '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -871,8 +796,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAMinusOrSetSubtractExpression(
- AMinusOrSetSubtractExpression node) {
+ public void caseAMinusOrSetSubtractExpression(AMinusOrSetSubtractExpression node) {
BType expected = getType(node);
BType found = new IntegerOrSetType();
@@ -888,17 +812,15 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAMultOrCartExpression(AMultOrCartExpression node) {
BType expected = getType(node);
- IntegerOrSetOfPairType found = new IntegerOrSetOfPairType(
- node.getStartPos(), node.getEndPos());
+ IntegerOrSetOfPairType found = new IntegerOrSetOfPairType(node.getStartPos(), node.getEndPos());
// setType(node.getLeft(), found.getFirst());
// setType(node.getRight(), found.getSecond());
BType result = null;
try {
result = expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "' at " + node.getClass().getSimpleName() + "\n "
- + node.getStartPos());
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "' at "
+ + node.getClass().getSimpleName() + "\n " + node.getStartPos());
}
//
// BType res2 = getType(node);
@@ -909,10 +831,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
//
if (result instanceof IntegerOrSetOfPairType) {
- setType(node.getLeft(),
- ((IntegerOrSetOfPairType) result).getFirst());
- setType(node.getRight(),
- ((IntegerOrSetOfPairType) result).getSecond());
+ setType(node.getLeft(), ((IntegerOrSetOfPairType) result).getFirst());
+ setType(node.getRight(), ((IntegerOrSetOfPairType) result).getSecond());
} else if (result instanceof IntegerType) {
setType(node.getLeft(), result);
setType(node.getRight(), result);
@@ -934,8 +854,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' / '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' / '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -948,8 +867,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' ** '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' ** '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -962,8 +880,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' mod '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' mod '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -973,15 +890,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseASuccessorExpression(ASuccessorExpression node) {
- FunctionType found = new FunctionType(IntegerType.getInstance(),
- IntegerType.getInstance());
+ FunctionType found = new FunctionType(IntegerType.getInstance(), IntegerType.getInstance());
unify(getType(node), found, node);
}
@Override
public void caseAPredecessorExpression(APredecessorExpression node) {
- FunctionType found = new FunctionType(IntegerType.getInstance(),
- IntegerType.getInstance());
+ FunctionType found = new FunctionType(IntegerType.getInstance(), IntegerType.getInstance());
unify(getType(node), found, node);
}
@@ -991,12 +906,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + "INTEGER" + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + "INTEGER" + "'");
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -1015,12 +928,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + "INTEGER" + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + "INTEGER" + "'");
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -1042,8 +953,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in 'TRUE'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in 'TRUE'");
}
}
@@ -1052,8 +962,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in 'FALSE'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in 'FALSE'");
}
}
@@ -1063,8 +972,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(BoolType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(BOOL)' in 'BOOL'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(BOOL)' in 'BOOL'");
}
}
@@ -1073,8 +981,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in 'bool(...)'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in 'bool(...)'");
}
setType(node.getPredicate(), BoolType.getInstance());
node.getPredicate().apply(this);
@@ -1089,8 +996,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' & '." + node.getStartPos());
+ throw new TypeErrorException(
+ "Excepted '" + getType(node) + "' , found 'BOOL' in ' & '." + node.getStartPos());
}
setType(node.getLeft(), BoolType.getInstance());
setType(node.getRight(), BoolType.getInstance());
@@ -1103,8 +1010,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' or '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' or '");
}
setType(node.getLeft(), BoolType.getInstance());
setType(node.getRight(), BoolType.getInstance());
@@ -1117,8 +1023,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' => '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' => '");
}
setType(node.getLeft(), BoolType.getInstance());
setType(node.getRight(), BoolType.getInstance());
@@ -1132,8 +1037,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
System.out.println(node.parent().getClass());
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' <=> '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' <=> '");
}
setType(node.getLeft(), BoolType.getInstance());
setType(node.getRight(), BoolType.getInstance());
@@ -1146,8 +1050,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' not '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' not '");
}
setType(node.getPredicate(), BoolType.getInstance());
node.getPredicate().apply(this);
@@ -1176,8 +1079,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(e, u);
}
BType expected = getType(node);
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getExpressions());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getExpressions());
for (PExpression e : copy) {
e.apply(this);
}
@@ -1224,7 +1126,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
private boolean compareElementsOfList(ArrayList<Node> list) {
- if(list.size() == 1){
+ if (list.size() == 1) {
return true;
}
try {
@@ -1241,11 +1143,9 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
} else if (list.get(0) instanceof AIdentifierExpression) {
HashSet<Node> set = new HashSet<Node>();
for (int i = 0; i < list.size(); i++) {
- AIdentifierExpression id = (AIdentifierExpression) list
- .get(i);
+ AIdentifierExpression id = (AIdentifierExpression) list.get(i);
Node enumValue = machineContext.getReferences().get(id);
- if (!machineContext.getEnumValues()
- .containsValue(enumValue)) {
+ if (!machineContext.getEnumValues().containsValue(enumValue)) {
return false;
}
set.add(enumValue);
@@ -1262,8 +1162,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAComprehensionSetExpression(AComprehensionSetExpression node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
ArrayList<BType> typesList = new ArrayList<BType>();
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
@@ -1277,8 +1176,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found " + found + "'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found " + found + "'");
}
setType(node.getPredicates(), BoolType.getInstance());
@@ -1287,10 +1185,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAEventBComprehensionSetExpression(
- AEventBComprehensionSetExpression node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseAEventBComprehensionSetExpression(AEventBComprehensionSetExpression node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -1328,8 +1224,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found = found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'POW(POW(_A))' in 'POW'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'POW(POW(_A))' in 'POW'");
}
setType(expr, found.getSubtype());
@@ -1363,8 +1258,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found = found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
setType(left, found);
setType(right, found);
@@ -1395,8 +1289,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
setType(node.getExpression(), new UntypedType());
@@ -1435,8 +1328,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'BOOL'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'BOOL'");
}
SetType set = new SetType(new UntypedType());
@@ -1453,8 +1345,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'BOOL'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'BOOL'");
}
SetType set = new SetType(new UntypedType());
@@ -1472,8 +1363,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'BOOL'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'BOOL'");
}
SetType set = new SetType(new UntypedType());
@@ -1491,8 +1381,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'BOOL'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'BOOL'");
}
SetType set = new SetType(new UntypedType());
@@ -1515,14 +1404,12 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + found + "'");
}
}
@Override
- public void caseAGeneralIntersectionExpression(
- AGeneralIntersectionExpression node) {
+ public void caseAGeneralIntersectionExpression(AGeneralIntersectionExpression node) {
SetType set = new SetType(new SetType(new UntypedType()));
setType(node.getExpression(), set);
node.getExpression().apply(this);
@@ -1532,16 +1419,14 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + found + "'");
}
}
@Override
public void caseAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
BType expected = getType(node);
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -1557,17 +1442,14 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@Override
- public void caseAQuantifiedIntersectionExpression(
- AQuantifiedIntersectionExpression node) {
+ public void caseAQuantifiedIntersectionExpression(AQuantifiedIntersectionExpression node) {
BType expected = getType(node);
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -1583,8 +1465,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -1594,8 +1475,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseALambdaExpression(ALambdaExpression node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -1621,15 +1501,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@Override
public void caseAFunctionExpression(AFunctionExpression node) {
- FunctionType func = new FunctionType(new UntypedType(),
- new UntypedType());
+ FunctionType func = new FunctionType(new UntypedType(), new UntypedType());
setType(node.getIdentifier(), func);
node.getIdentifier().apply(this);
@@ -1648,12 +1526,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
rangeFound.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + rangeFound + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + rangeFound + "'");
}
- ArrayList<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ ArrayList<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
setType(e, new UntypedType());
e.apply(this);
@@ -1668,8 +1544,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
domainFound.unify(p, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + domainFound
- + "' , found '" + makePair(foundList) + "'");
+ throw new TypeErrorException("Excepted '" + domainFound + "' , found '" + makePair(foundList) + "'");
}
}
@@ -1691,8 +1566,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
domainFound.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + domainFound + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + domainFound + "'");
}
}
@@ -1714,8 +1588,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
rangeFound.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + rangeFound + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + rangeFound + "'");
}
}
@@ -1771,8 +1644,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAPartialSurjectionExpression(
- APartialSurjectionExpression node) {
+ public void caseAPartialSurjectionExpression(APartialSurjectionExpression node) {
// evalFunction(node, node.getLeft(), node.getRight());
BType dom = new UntypedType();
BType ran = new UntypedType();
@@ -1818,8 +1690,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -1848,8 +1719,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -1868,8 +1738,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -1890,8 +1759,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseADomainRestrictionExpression(
- ADomainRestrictionExpression node) {
+ public void caseADomainRestrictionExpression(ADomainRestrictionExpression node) {
UntypedType u = new UntypedType();
SetType setType = new SetType(u);
FunctionType f = new FunctionType(u, new UntypedType());
@@ -1906,8 +1774,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseADomainSubtractionExpression(
- ADomainSubtractionExpression node) {
+ public void caseADomainSubtractionExpression(ADomainSubtractionExpression node) {
UntypedType u = new UntypedType();
SetType setType = new SetType(u);
FunctionType f = new FunctionType(u, new UntypedType());
@@ -2008,8 +1875,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
node.getLeft().apply(this);
@@ -2026,8 +1892,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
BType right = new SetType(new PairType(v, w));
setType(node.getLeft(), left);
setType(node.getRight(), right);
- BType found = new SetType(new PairType(new PairType(t, v),
- new PairType(u, w)));
+ BType found = new SetType(new PairType(new PairType(t, v), new PairType(u, w)));
BType expected = getType(node);
unify(expected, found, node);
@@ -2137,8 +2002,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseATransRelationExpression(ATransRelationExpression node) {
UntypedType t = new UntypedType();
UntypedType u = new UntypedType();
- setType(node.getExpression(), new SetType(new PairType(t,
- new SetType(u))));
+ setType(node.getExpression(), new SetType(new PairType(t, new SetType(u))));
BType found = new SetType(new PairType(t, u));
BType expected = getType(node);
unify(expected, found, node);
@@ -2149,22 +2013,19 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "' at " + node.getClass().getSimpleName() + "\n "
- + node.getStartPos() + ":" + node.getEndPos());
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "' at "
+ + node.getClass().getSimpleName() + "\n " + node.getStartPos() + ":" + node.getEndPos());
}
}
@Override
public void caseAEmptySequenceExpression(AEmptySequenceExpression node) {
BType expected = getType(node);
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -2176,8 +2037,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseASeqExpression(ASeqExpression node) {
UntypedType t = new UntypedType();
setType(node.getExpression(), new SetType(t));
- BType found = new SetType(
- new FunctionType(IntegerType.getInstance(), t));
+ BType found = new SetType(new FunctionType(IntegerType.getInstance(), t));
BType expected = getType(node);
unify(expected, found, node);
node.getExpression().apply(this);
@@ -2185,8 +2045,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseASizeExpression(ASizeExpression node) {
- setType(node.getExpression(),
- new FunctionType(IntegerType.getInstance(), new UntypedType()));
+ setType(node.getExpression(), new FunctionType(IntegerType.getInstance(), new UntypedType()));
BType found = IntegerType.getInstance();
BType expected = getType(node);
unify(expected, found, node);
@@ -2195,8 +2054,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAConcatExpression(AConcatExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
setType(node.getLeft(), found);
setType(node.getRight(), found);
BType expected = getType(node);
@@ -2220,8 +2078,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAFirstExpression(AFirstExpression node) {
BType found = new UntypedType();
- setType(node.getExpression(),
- new FunctionType(IntegerType.getInstance(), found));
+ setType(node.getExpression(), new FunctionType(IntegerType.getInstance(), found));
BType expected = getType(node);
unify(expected, found, node);
node.getExpression().apply(this);
@@ -2229,8 +2086,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseATailExpression(ATailExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
setType(node.getExpression(), found);
BType expected = getType(node);
unify(expected, found, node);
@@ -2244,8 +2100,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
private void evalSetOfSequences(Node node, Node expr) {
UntypedType t = new UntypedType();
setType(expr, new SetType(t));
- BType found = new SetType(
- new FunctionType(IntegerType.getInstance(), t));
+ BType found = new SetType(new FunctionType(IntegerType.getInstance(), t));
BType expected = getType(node);
unify(expected, found, node);
expr.apply(this);
@@ -2281,8 +2136,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseALastExpression(ALastExpression node) {
BType found = new UntypedType();
- setType(node.getExpression(),
- new FunctionType(IntegerType.getInstance(), found));
+ setType(node.getExpression(), new FunctionType(IntegerType.getInstance(), found));
BType expected = getType(node);
unify(expected, found, node);
node.getExpression().apply(this);
@@ -2295,8 +2149,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseARevExpression(ARevExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
setType(node.getExpression(), found);
BType expected = getType(node);
unify(expected, found, node);
@@ -2305,8 +2158,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAFrontExpression(AFrontExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
setType(node.getExpression(), found);
BType expected = getType(node);
unify(expected, found, node);
@@ -2316,10 +2168,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAGeneralConcatExpression(AGeneralConcatExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
- setType(node.getExpression(),
- new FunctionType(IntegerType.getInstance(), found));
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
+ setType(node.getExpression(), new FunctionType(IntegerType.getInstance(), found));
// BType found = new SetType(new PairType(IntegerType.getInstance(),
// new UntypedType()));
@@ -2356,16 +2206,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseASequenceExtensionExpression(
- ASequenceExtensionExpression node) {
+ public void caseASequenceExtensionExpression(ASequenceExtensionExpression node) {
BType expected = getType(node);
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
try {
found = found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
BType subtype;
if (found instanceof FunctionType) {
@@ -2377,8 +2224,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
for (PExpression e : node.getExpression()) {
setType(e, subtype);
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getExpression());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getExpression());
for (PExpression e : copy) {
e.apply(this);
}
@@ -2407,8 +2253,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
unify(expected, found, node);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -2422,14 +2267,12 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getRecord().apply(this);
- BType found = ((StructType) getType(node.getRecord()))
- .getType(fieldName);
+ BType found = ((StructType) getType(node.getRecord())).getType(fieldName);
BType expected = getType(node);
try {
unify(expected, found, node);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -2456,8 +2299,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -2470,8 +2312,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
StringType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found " + StringType.getInstance() + "'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found " + StringType.getInstance() + "'");
}
}
@@ -2481,8 +2322,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found " + found + "'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found " + found + "'");
}
}
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index ab416a1cf00c472861f77a8474b96fc308ae5ba1..aecdcbb166eed4af5d196ab6c0dabffc5ac65b99 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -583,7 +583,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
+ UtilMethods.getPositionAsString(e));
}
- tree = conType.createSyntaxTreeNode(typechecker);
+ tree = conType.createASTNode(typechecker);
} else {
tree = (PExpression) restrictedList.get(0);
for (int i = 1; i < restrictedList.size(); i++) {
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
index db63b09f68eafafc39d3cf1eee91341cca77392e..eb7a3a40950a4b7eeca71af60a0d64b75af8cdd1 100644
--- a/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
@@ -49,7 +49,7 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
public AssignedVariablesFinder(MachineContext machineContext) {
this.assignedVariablesTable = new Hashtable<Node, HashSet<Node>>();
this.machineContext = machineContext;
- machineContext.getTree().apply(this);
+ machineContext.getStartNode().apply(this);
}
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
index 3713b6730830c3ac506fe2cdac34daa5e572b8d5..fe08cb904fe3567060755ad992bd19d0455f3860 100644
--- a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
@@ -87,7 +87,7 @@ public class UnchangedVariablesFinder extends DepthFirstAdapter {
this.unchangedVariablesTable = new Hashtable<Node, HashSet<Node>>();
this.unchangedVariablesNull = new Hashtable<Node, HashSet<Node>>();
- c.getTree().apply(this);
+ c.getStartNode().apply(this);
}
@Override
diff --git a/src/main/java/de/tlc4b/btypes/BType.java b/src/main/java/de/tlc4b/btypes/BType.java
index ed800fc80ac70ff2dd520b63200660c317d72091..b90b379def0affef19c9d9292e50f26ff792a954 100644
--- a/src/main/java/de/tlc4b/btypes/BType.java
+++ b/src/main/java/de/tlc4b/btypes/BType.java
@@ -3,11 +3,10 @@ package de.tlc4b.btypes;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tlc4b.analysis.Typechecker;
-public interface BType extends ITypeConstants{
+public interface BType {
public BType unify(BType other, ITypechecker typechecker);
public boolean isUntyped();
public boolean compare(BType other);
- public String getTlaType();
public boolean containsInfiniteType();
- public PExpression createSyntaxTreeNode(Typechecker typechecker);
+ public PExpression createASTNode(Typechecker typechecker);
}
diff --git a/src/main/java/de/tlc4b/btypes/BoolType.java b/src/main/java/de/tlc4b/btypes/BoolType.java
index ef7bb6b657758fb6e2137b8091ed07b03c0a0166..e2937dd21edcc337e4291864282c59b2f141afdd 100644
--- a/src/main/java/de/tlc4b/btypes/BoolType.java
+++ b/src/main/java/de/tlc4b/btypes/BoolType.java
@@ -43,15 +43,11 @@ public class BoolType implements BType {
return false;
}
- public String getTlaType() {
- return "BOOLEAN";
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
ABoolSetExpression node = new ABoolSetExpression();
typechecker.setType(node, new SetType(this));
return node;
diff --git a/src/main/java/de/tlc4b/btypes/ModelValueType.java b/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
similarity index 73%
rename from src/main/java/de/tlc4b/btypes/ModelValueType.java
rename to src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
index 4017d4869850ae40cb3f7375dd5079c3ac28303e..41728d814aca42662b85218cc336c75ed9051ab6 100644
--- a/src/main/java/de/tlc4b/btypes/ModelValueType.java
+++ b/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
@@ -8,10 +8,10 @@ import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.exceptions.UnificationException;
-public class ModelValueType implements BType {
+public class EnumeratedSetElement implements BType {
private String name;
- public ModelValueType(String name) {
+ public EnumeratedSetElement(String name) {
this.name = name;
}
@@ -23,8 +23,8 @@ public class ModelValueType implements BType {
if (!this.compare(other)) {
throw new UnificationException();
}
- if (other instanceof ModelValueType) {
- if (((ModelValueType) other).getName().equals(this.name)) {
+ if (other instanceof EnumeratedSetElement) {
+ if (((EnumeratedSetElement) other).getName().equals(this.name)) {
return this;
} else {
throw new UnificationException();
@@ -49,23 +49,19 @@ public class ModelValueType implements BType {
public boolean compare(BType other) {
if (other instanceof UntypedType)
return true;
- if (other instanceof ModelValueType) {
- if (((ModelValueType) other).getName().equals(this.name)) {
+ if (other instanceof EnumeratedSetElement) {
+ if (((EnumeratedSetElement) other).getName().equals(this.name)) {
return true;
}
}
return false;
}
- public String getTlaType() {
- return name;
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
TIdentifierLiteral literal = new TIdentifierLiteral(name);
ArrayList<TIdentifierLiteral> idList = new ArrayList<TIdentifierLiteral>();
idList.add(literal);
diff --git a/src/main/java/de/tlc4b/btypes/FunctionType.java b/src/main/java/de/tlc4b/btypes/FunctionType.java
index 64e4348a3033f8b6756cb60df2a6de4f1ca3cfbb..5687f1b866010fe55c81381951f806eab4bb014e 100644
--- a/src/main/java/de/tlc4b/btypes/FunctionType.java
+++ b/src/main/java/de/tlc4b/btypes/FunctionType.java
@@ -81,6 +81,7 @@ public class FunctionType extends AbstractHasFollowers {
setRange(newType);
}
+ @Override
public boolean compare(BType other) {
if (other instanceof UntypedType)
return true;
@@ -119,19 +120,17 @@ public class FunctionType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return "[" + domain.getTlaType() + " -> " + range.getTlaType() + "]";
- }
-
+ @Override
public boolean containsInfiniteType() {
return this.domain.containsInfiniteType()
|| this.range.containsInfiniteType();
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ @Override
+ public PExpression createASTNode(Typechecker typechecker) {
APartialFunctionExpression node = new APartialFunctionExpression(
- domain.createSyntaxTreeNode(typechecker),
- range.createSyntaxTreeNode(typechecker));
+ domain.createASTNode(typechecker),
+ range.createASTNode(typechecker));
typechecker.setType(node, new SetType(this));
return node;
diff --git a/src/main/java/de/tlc4b/btypes/ITypeConstants.java b/src/main/java/de/tlc4b/btypes/ITypeConstants.java
deleted file mode 100644
index 70822584085caea3fa9a3e3a28a7ad5d353238d2..0000000000000000000000000000000000000000
--- a/src/main/java/de/tlc4b/btypes/ITypeConstants.java
+++ /dev/null
@@ -1,6 +0,0 @@
-package de.tlc4b.btypes;
-
-public interface ITypeConstants {
-
- public final String INTEGER = "INTEGER";
-}
diff --git a/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
index fa78770ce6da81e330332f0248e65b3cda50caab..d0d929bd7a2cac9a3785c4152a11b5171c7d8bb2 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
@@ -219,15 +219,11 @@ public class IntegerOrSetOfPairType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return null;
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
return null;
}
diff --git a/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java b/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
index 82857bb780d299ebac98ae4592cd855a5c6fe75c..7d52dfae8b2d30cf1212699b26677083d4de14bf 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
@@ -34,7 +34,6 @@ public class IntegerOrSetType extends AbstractHasFollowers {
}
public boolean isUntyped() {
- // TODO proof
return true;
}
@@ -55,15 +54,11 @@ public class IntegerOrSetType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return null;
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
return null;
}
}
diff --git a/src/main/java/de/tlc4b/btypes/IntegerType.java b/src/main/java/de/tlc4b/btypes/IntegerType.java
index fe3d951815adfc758caae5cbe6fbfc61940dd498..b6ce01fbb768fedda77c485731ebd910b4ee0f33 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerType.java
@@ -40,11 +40,6 @@ public class IntegerType implements BType {
return "INTEGER";
}
- public String getTlaType() {
- return TLC4BGlobals.getMIN_INT() + ".." + TLC4BGlobals.getMAX_INT();
- }
-
-
public boolean isUntyped() {
return false;
@@ -63,7 +58,7 @@ public class IntegerType implements BType {
return true;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
AIntegerSetExpression node = new AIntegerSetExpression();
typechecker.setType(node, new SetType(this));
return node;
diff --git a/src/main/java/de/tlc4b/btypes/PairType.java b/src/main/java/de/tlc4b/btypes/PairType.java
index 1e9057d795f94a60bc53bcfc644ab172325fbdcd..fe7e270a4b0dce4cd300a93ea6c7b9b6d5f51773 100644
--- a/src/main/java/de/tlc4b/btypes/PairType.java
+++ b/src/main/java/de/tlc4b/btypes/PairType.java
@@ -120,24 +120,15 @@ public class PairType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- String res = first.getTlaType() + " \\times ";
- if (second instanceof PairType) {
- res += "(" + second.getTlaType() + ")";
- } else
- res += second.getTlaType();
- return res;
- }
-
public boolean containsInfiniteType() {
return this.first.containsInfiniteType()
|| this.second.containsInfiniteType();
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
ACartesianProductExpression node = new ACartesianProductExpression(
- first.createSyntaxTreeNode(typechecker),
- second.createSyntaxTreeNode(typechecker));
+ first.createASTNode(typechecker),
+ second.createASTNode(typechecker));
typechecker.setType(node, new SetType(this));
return node;
}
diff --git a/src/main/java/de/tlc4b/btypes/SetType.java b/src/main/java/de/tlc4b/btypes/SetType.java
index 8137156d58a149a3e9ffdb4e8dc2abf17f865cb8..8edfe6889efbcb5bc2301932cfce8aacbee9cd31 100644
--- a/src/main/java/de/tlc4b/btypes/SetType.java
+++ b/src/main/java/de/tlc4b/btypes/SetType.java
@@ -34,8 +34,7 @@ public class SetType extends AbstractHasFollowers {
}
if (other instanceof SetType) {
((SetType) other).setFollowersTo(this, typechecker);
- this.subtype = this.subtype.unify(((SetType) other).subtype,
- typechecker);
+ this.subtype = this.subtype.unify(((SetType) other).subtype, typechecker);
return this;
}
@@ -56,12 +55,12 @@ public class SetType extends AbstractHasFollowers {
@Override
public String toString() {
- if(this.equals(subtype)){
+ if (this.equals(subtype)) {
return "POW(recursive call)";
- }else{
+ } else {
return "POW(" + subtype + ")";
}
-
+
}
public boolean isUntyped() {
@@ -75,8 +74,7 @@ public class SetType extends AbstractHasFollowers {
if (other instanceof UntypedType)
return true;
- if (other instanceof IntegerOrSetType
- || other instanceof IntegerOrSetOfPairType) {
+ if (other instanceof IntegerOrSetType || other instanceof IntegerOrSetOfPairType) {
return true;
} else if (other instanceof FunctionType) {
return other.compare(this);
@@ -86,7 +84,7 @@ public class SetType extends AbstractHasFollowers {
@Override
public boolean contains(BType other) {
- if(this.equals(subtype)){
+ if (this.equals(subtype)) {
return true;
}
if (this.subtype.equals(other)) {
@@ -98,16 +96,12 @@ public class SetType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return "SUBSET(" + subtype.getTlaType() + ")";
- }
-
public boolean containsInfiniteType() {
return this.subtype.containsInfiniteType();
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
- APowSubsetExpression node = new APowSubsetExpression(subtype.createSyntaxTreeNode(typechecker));
+ public PExpression createASTNode(Typechecker typechecker) {
+ APowSubsetExpression node = new APowSubsetExpression(subtype.createASTNode(typechecker));
typechecker.setType(node, this);
return node;
}
diff --git a/src/main/java/de/tlc4b/btypes/StringType.java b/src/main/java/de/tlc4b/btypes/StringType.java
index 4771569a3cee584c1ccc28c389332284e18e903c..b4599467f9e19f5a588c74934667dab5a8a4462a 100644
--- a/src/main/java/de/tlc4b/btypes/StringType.java
+++ b/src/main/java/de/tlc4b/btypes/StringType.java
@@ -48,15 +48,11 @@ public class StringType implements BType {
return false;
}
- public String getTlaType() {
- return "STRING";
- }
-
public boolean containsInfiniteType() {
return true;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
AStringSetExpression node = new AStringSetExpression();
typechecker.setType(node, new SetType(this));
return node;
diff --git a/src/main/java/de/tlc4b/btypes/StructType.java b/src/main/java/de/tlc4b/btypes/StructType.java
index 30fc041ebadd20f5f09438086dcdd02712de9164..e2e4345bea039c43fe0714881c57d39f092f9574 100644
--- a/src/main/java/de/tlc4b/btypes/StructType.java
+++ b/src/main/java/de/tlc4b/btypes/StructType.java
@@ -188,28 +188,6 @@ public class StructType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- StringBuffer res = new StringBuffer();
- res.append("[");
- Iterator<Entry<String, BType>> iterator = types.entrySet().iterator();
- if (!iterator.hasNext()) {
- res.append("...");
- } else {
- while (iterator.hasNext()) {
- Entry<String, BType> next = iterator.next();
- String fieldName = next.getKey();
- BType type = next.getValue();
- res.append(fieldName);
- res.append(":");
- res.append(type);
- if (iterator.hasNext())
- res.append(",");
- }
- }
- res.append("]");
- return res.toString();
- }
-
public boolean containsInfiniteType() {
Iterator<BType> iterator = this.types.values().iterator();
while (iterator.hasNext()) {
@@ -219,7 +197,7 @@ public class StructType extends AbstractHasFollowers {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
ArrayList<PRecEntry> list = new ArrayList<PRecEntry>();
Set<Entry<String, BType>> entrySet = this.types.entrySet();
@@ -231,7 +209,7 @@ public class StructType extends AbstractHasFollowers {
idList.add(literal);
AIdentifierExpression id = new AIdentifierExpression(idList);
ARecEntry recEntry = new ARecEntry(id,
- type.createSyntaxTreeNode(typechecker));
+ type.createASTNode(typechecker));
list.add(recEntry);
}
AStructExpression node = new AStructExpression(list);
diff --git a/src/main/java/de/tlc4b/btypes/UntypedType.java b/src/main/java/de/tlc4b/btypes/UntypedType.java
index a24e490ea03324e96f48a9cecd2d88b7c6adc80f..2d1eee0ce0f77b006f666a19e3d49a38c9ae64b3 100644
--- a/src/main/java/de/tlc4b/btypes/UntypedType.java
+++ b/src/main/java/de/tlc4b/btypes/UntypedType.java
@@ -3,7 +3,6 @@ package de.tlc4b.btypes;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tlc4b.analysis.Typechecker;
-
public class UntypedType extends AbstractHasFollowers {
public BType unify(BType other, ITypechecker typechecker) {
@@ -24,21 +23,12 @@ public class UntypedType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return this.toString();
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
return null;
}
-
-// @Override
-// public String toString(){
-// return "UNTYPED: Followers: "+ this.printFollower();
-// }
}
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
index 51ecca716c453f1afc12c848e53195b293f76a5d..4ce9715c29df46688d92a230dd709ca04718c974 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
@@ -70,23 +70,21 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
public void parseDefinition(AExpressionDefinitionDefinition def) {
if (!(def.getRhs() instanceof AStringExpression)) {
- throw new LTLParseException(
- "Error: LTL formula is not in a string representation.");
+ throw new LTLParseException("Error: LTL formula is not in a string representation.");
}
AStringExpression stringNode = (AStringExpression) def.getRhs();
this.ltlFormula = stringNode.getContent().getText();
try {
- this.ltlFormulaStart = parse(ltlFormula);
+ this.ltlFormulaStart = parseLTLFormula(ltlFormula);
} catch (Exception e) {
- String line = "Parsing definition " + name + " (line "
- + def.getStartPos().getLine() + "):\n";
- throw new LTLParseException(line + e.getMessage());
+ String message = "Parsing definition " + name + " (line " + def.getStartPos().getLine() + "):\n";
+ throw new LTLParseException(message + e.getMessage());
}
}
- public void parseLTLString(String ltlString) {
+ public void parseLTLString(final String ltlString) {
try {
- this.ltlFormulaStart = parse(ltlString);
+ this.ltlFormulaStart = parseLTLFormula(ltlString);
} catch (Exception e) {
throw new LTLParseException(e.getMessage());
}
@@ -108,8 +106,7 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
return ltlNodeToBNodeTable;
}
- public de.be4.classicalb.core.parser.node.Node getBAst(
- de.be4.ltl.core.parser.node.Node unparsedLtl) {
+ public de.be4.classicalb.core.parser.node.Node getBAst(de.be4.ltl.core.parser.node.Node unparsedLtl) {
return ltlNodeToBNodeTable.get(unparsedLtl);
}
@@ -125,14 +122,12 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
return ltlFormulaStart;
}
- public void printLTLFormula(TLAPrinter tlaPrinter,
- TypeRestrictor typeRestrictor) {
+ public void printLTLFormula(TLAPrinter tlaPrinter, TypeRestrictor typeRestrictor) {
// LTLFormulaPrinter ltlFormulaPrinter =
new LTLFormulaPrinter(tlaPrinter, this, typeRestrictor);
}
- public static Start parse(String ltlFormula) throws ParserException,
- LexerException, IOException {
+ public static Start parseLTLFormula(String ltlFormula) throws ParserException, LexerException, IOException {
StringReader reader = new StringReader(ltlFormula);
PushbackReader r = new PushbackReader(reader);
Lexer l = new LtlLexer(r);
@@ -144,13 +139,11 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
@Override
public void caseAUnparsedLtl(AUnparsedLtl node) {
- de.be4.classicalb.core.parser.node.Start start = parseBPredicate(node
- .getPredicate().getText());
+ de.be4.classicalb.core.parser.node.Start start = parseBPredicate(node.getPredicate().getText());
ltlNodeToBNodeTable.put(node, start);
- LTLBPredicate ltlBPredicate = new LTLBPredicate(getUnifiedContext(),
- start);
+ LTLBPredicate ltlBPredicate = new LTLBPredicate(getUnifiedContext(), start);
this.bPredicates.add(ltlBPredicate);
machineContext.checkLTLBPredicate(ltlBPredicate);
@@ -171,19 +164,17 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
@Override
public void caseAExistsLtl(AExistsLtl node) {
- handleQuantification(node, node.getExistsIdentifier().getText(), node
- .getPredicate().getText(), node.getLtl());
+ handleQuantification(node, node.getExistsIdentifier().getText(), node.getPredicate().getText(), node.getLtl());
}
@Override
public void caseAForallLtl(AForallLtl node) {
- handleQuantification(node, node.getForallIdentifier().getText(), node
- .getPredicate().getText(), node.getLtl());
+ handleQuantification(node, node.getForallIdentifier().getText(), node.getPredicate().getText(), node.getLtl());
}
- private void handleQuantification(de.be4.ltl.core.parser.node.Node node,
- String parameterName, String bPredicateString, PLtl ltl) {
+ private void handleQuantification(de.be4.ltl.core.parser.node.Node node, String parameterName,
+ String bPredicateString, PLtl ltl) {
// create an identifier (b ast node) for the parameter of the
// quantification
List<TIdentifierLiteral> list = new ArrayList<TIdentifierLiteral>();
@@ -204,8 +195,7 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
// collect all identifiers which can be used in the bPredicate and
// verify the bPredicate
- LTLBPredicate ltlBPredicate = new LTLBPredicate(getUnifiedContext(),
- start);
+ LTLBPredicate ltlBPredicate = new LTLBPredicate(getUnifiedContext(), start);
this.bPredicates.add(ltlBPredicate);
machineContext.checkLTLBPredicate(ltlBPredicate);
@@ -250,68 +240,56 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
}
public void inAUntilLtl(AUntilLtl node) {
- throw new ScopeException(
- "The 'until' operator is not supported by TLC.");
+ throw new ScopeException("The 'until' operator is not supported.");
}
public void inAWeakuntilLtl(AWeakuntilLtl node) {
- throw new ScopeException(
- "The 'weak until' operator is not supported by TLC.");
+ throw new ScopeException("The 'weak until' operator is not supported.");
}
public void inAReleaseLtl(AReleaseLtl node) {
- throw new ScopeException(
- "The 'release' operator is not supported by TLC.");
+ throw new ScopeException("The 'release' operator is not supported.");
}
public void inASinceLtl(ASinceLtl node) {
- throw new ScopeException(
- "The 'since' operator is not supported by TLC.");
+ throw new ScopeException("The 'since' operator is not supported.");
}
public void inATriggerLtl(ATriggerLtl node) {
- throw new ScopeException(
- "The 'trigger' operator is not supported by TLC.");
+ throw new ScopeException("The 'trigger' operator is not supported.");
}
public void inAHistoricallyLtl(AHistoricallyLtl node) {
- throw new ScopeException(
- "The 'history' operator is not supported by TLC.");
+ throw new ScopeException("The 'history' operator is not supported.");
}
public void inAOnceLtl(AOnceLtl node) {
- throw new ScopeException("The 'once' operator is not supported by TLC.");
+ throw new ScopeException("The 'once' operator is not supported.");
}
public void inAYesterdayLtl(AYesterdayLtl node) {
- throw new ScopeException(
- "The 'yesterday' operator is not supported by TLC.");
+ throw new ScopeException("The 'yesterday' operator is not supported.");
}
@Override
public void caseAActionLtl(AActionLtl node) {
- throw new ScopeException(
- "The '[...]' operator is not supported by TLC.");
- }
-
- @Override
- public void caseAAndLtl(AAndLtl node)
- {
- inAAndLtl(node);
- if(node.getLeft() != null)
- {
- node.getLeft().apply(this);
- }
- if(node.getRight() != null)
- {
- node.getRight().apply(this);
- System.out.println(node.getRight().getClass());
- }
- outAAndLtl(node);
- }
-
- protected MachineContext getMachineContext(){
- return this.machineContext;
- }
-
+ throw new ScopeException("The '[...]' operator is not supported.");
+ }
+
+ @Override
+ public void caseAAndLtl(AAndLtl node) {
+ inAAndLtl(node);
+ if (node.getLeft() != null) {
+ node.getLeft().apply(this);
+ }
+ if (node.getRight() != null) {
+ node.getRight().apply(this);
+ }
+ outAAndLtl(node);
+ }
+
+ public MachineContext getMachineContext() {
+ return this.machineContext;
+ }
+
}
diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
index 97c016efb8a6f8a49f768a7a23568b2812266de0..80bbdddcafb5edc70bee8fb374e65a0380b4d3f7 100644
--- a/src/main/java/de/tlc4b/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -74,7 +74,7 @@ public class Generator extends DepthFirstAdapter {
evalInvariant();
evalOperations();
evalGoal();
- machineContext.getTree().apply(this);
+ machineContext.getStartNode().apply(this);
evalSpec();
}
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index 318f46338995903d95962fa36e3a38be947dea9f..8b9584664ec600025075019c221711ea5116260a 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -53,7 +53,7 @@ public class TLCOutputInfo {
this.constants = machineContext.getConstants().keySet();
this.hasInit = tlaModule.getInitPredicates().size() > 0;
- if (machineContext.constantSetupInTraceFile()) {
+ if (machineContext.hasConstants()) {
this.constantSetup = true;
}
diff --git a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
index 484487a14e15278f3dba4958cacaf8ec436a0929..3e3a300383f75a56996cb8e4f8913f55f41b380b 100644
--- a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
+++ b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
@@ -25,30 +25,27 @@ public class TestTypechecker {
Start start = parser.parse(machine, false);
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
- //System.out.println(ast2String2.toString());
- MachineContext c = new MachineContext(null, start, null, null);
+ // System.out.println(ast2String2.toString());
+ MachineContext c = new MachineContext(null, start);
+ c.analyseMachine();
Typechecker t = new Typechecker(c);
for (String name : c.getSetParamter().keySet()) {
- parameters.put(name,
- t.getType(c.getSetParamter().get(name)));
+ parameters.put(name, t.getType(c.getSetParamter().get(name)));
}
-
+
for (String name : c.getScalarParameter().keySet()) {
- parameters.put(name,
- t.getType(c.getScalarParameter().get(name)));
+ parameters.put(name, t.getType(c.getScalarParameter().get(name)));
}
for (String name : c.getConstants().keySet()) {
constants.put(name, t.getType(c.getConstants().get(name)));
}
-
+
for (String name : c.getVariables().keySet()) {
variables.put(name, t.getType(c.getVariables().get(name)));
}
-
}
-
-
+
}