Skip to content
Snippets Groups Projects
Commit 49a7214a authored by dgelessus's avatar dgelessus
Browse files

Rename STANDARD_MODULES enum to more usual spelling

parent bb6cbc91
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+ 109
− 109
View file @ 49a7214a
......@@ -104,27 +104,27 @@ import de.tlc4b.btypes.SetType;
import de.tlc4b.tla.TLAModule;
public class UsedStandardModules extends DepthFirstAdapter {
private enum STANDARD_MODULES {
private enum StandardModule {
Naturals, Integers, FiniteSets, Sequences, TLC, BBuiltIns, Relations, FunctionsAsRelations, Functions, SequencesExtended, SequencesAsRelations, ExternalFunctions, Foo
}
private final static ArrayList<STANDARD_MODULES> modules = new ArrayList<>();
private final static ArrayList<StandardModule> modules = new ArrayList<>();
static {
modules.add(STANDARD_MODULES.Naturals);
modules.add(STANDARD_MODULES.Integers);
modules.add(STANDARD_MODULES.FiniteSets);
modules.add(STANDARD_MODULES.Sequences);
modules.add(STANDARD_MODULES.TLC);
modules.add(STANDARD_MODULES.BBuiltIns);
modules.add(STANDARD_MODULES.Relations);
modules.add(STANDARD_MODULES.Functions);
modules.add(STANDARD_MODULES.FunctionsAsRelations);
modules.add(STANDARD_MODULES.SequencesExtended);
modules.add(STANDARD_MODULES.SequencesAsRelations);
modules.add(STANDARD_MODULES.ExternalFunctions);
}
private final Set<STANDARD_MODULES> extendedStandardModules;
modules.add(StandardModule.Naturals);
modules.add(StandardModule.Integers);
modules.add(StandardModule.FiniteSets);
modules.add(StandardModule.Sequences);
modules.add(StandardModule.TLC);
modules.add(StandardModule.BBuiltIns);
modules.add(StandardModule.Relations);
modules.add(StandardModule.Functions);
modules.add(StandardModule.FunctionsAsRelations);
modules.add(StandardModule.SequencesExtended);
modules.add(StandardModule.SequencesAsRelations);
modules.add(StandardModule.ExternalFunctions);
}
private final Set<StandardModule> extendedStandardModules;
private final Typechecker typechecker;
public UsedStandardModules(Start start, Typechecker typechecker,
......@@ -133,7 +133,7 @@ public class UsedStandardModules extends DepthFirstAdapter {
this.typechecker = typechecker;
if (TLC4BGlobals.useSymmetry()) {
extendedStandardModules.add(STANDARD_MODULES.TLC);
extendedStandardModules.add(StandardModule.TLC);
}
List<PDefinition> definitions = tlaModule.getAllDefinitions();
......@@ -150,66 +150,66 @@ public class UsedStandardModules extends DepthFirstAdapter {
}
public List<String> getExtendedModules() {
ArrayList<STANDARD_MODULES> list = new ArrayList<>(extendedStandardModules);
if (list.contains(STANDARD_MODULES.Integers)) {
list.remove(STANDARD_MODULES.Naturals);
ArrayList<StandardModule> list = new ArrayList<>(extendedStandardModules);
if (list.contains(StandardModule.Integers)) {
list.remove(StandardModule.Naturals);
}
list.sort((s1, s2) -> {
Integer i1 = modules.indexOf(s1);
Integer i2 = modules.indexOf(s2);
return i1.compareTo(i2);
});
return list.stream().map(STANDARD_MODULES::name).collect(Collectors.toList());
return list.stream().map(StandardModule::name).collect(Collectors.toList());
}
public Set<String> getStandardModulesToBeCreated() {
// dependencies of standard modules
HashSet<STANDARD_MODULES> res = new HashSet<>();
for (STANDARD_MODULES module : extendedStandardModules) {
HashSet<StandardModule> res = new HashSet<>();
for (StandardModule module : extendedStandardModules) {
switch (module) {
case ExternalFunctions:
res.add(STANDARD_MODULES.ExternalFunctions);
res.add(StandardModule.ExternalFunctions);
break;
case FunctionsAsRelations:
res.add(STANDARD_MODULES.FunctionsAsRelations);
res.add(STANDARD_MODULES.Functions);
res.add(StandardModule.FunctionsAsRelations);
res.add(StandardModule.Functions);
break;
case SequencesAsRelations:
res.add(STANDARD_MODULES.SequencesAsRelations);
res.add(STANDARD_MODULES.Relations);
res.add(STANDARD_MODULES.FunctionsAsRelations);
res.add(STANDARD_MODULES.Functions);
res.add(StandardModule.SequencesAsRelations);
res.add(StandardModule.Relations);
res.add(StandardModule.FunctionsAsRelations);
res.add(StandardModule.Functions);
break;
case BBuiltIns:
res.add(STANDARD_MODULES.BBuiltIns);
res.add(StandardModule.BBuiltIns);
break;
case Functions:
res.add(STANDARD_MODULES.Functions);
res.add(StandardModule.Functions);
break;
case Relations:
res.add(STANDARD_MODULES.Relations);
res.add(StandardModule.Relations);
break;
case Sequences:
break;
case SequencesExtended:
res.add(STANDARD_MODULES.SequencesExtended);
res.add(StandardModule.SequencesExtended);
break;
default:
break;
}
}
return res.stream().map(STANDARD_MODULES::name).collect(Collectors.toSet());
return res.stream().map(StandardModule::name).collect(Collectors.toSet());
}
@Override
public void inAExpressionDefinitionDefinition(AExpressionDefinitionDefinition node) {
if (TLC4BGlobals.isForceTLCToEvalConstants()) {
extendedStandardModules.add(STANDARD_MODULES.TLC);
extendedStandardModules.add(StandardModule.TLC);
}
String name = node.getName().getText().trim();
if (StandardModules.isKeywordInModuleExternalFunctions(name)) {
extendedStandardModules.add(STANDARD_MODULES.ExternalFunctions);
extendedStandardModules.add(StandardModule.ExternalFunctions);
}
}
......@@ -217,7 +217,7 @@ public class UsedStandardModules extends DepthFirstAdapter {
public void inADefinitionPredicate(ADefinitionPredicate node) {
String name = node.getDefLiteral().getText().trim();
if (StandardModules.isKeywordInModuleExternalFunctions(name)) {
extendedStandardModules.add(STANDARD_MODULES.ExternalFunctions);
extendedStandardModules.add(StandardModule.ExternalFunctions);
}
}
......@@ -227,46 +227,46 @@ public class UsedStandardModules extends DepthFirstAdapter {
@Override
public void caseANaturalSetExpression(ANaturalSetExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
@Override
public void caseANatural1SetExpression(ANatural1SetExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
@Override
public void caseANatSetExpression(ANatSetExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
@Override
public void caseANat1SetExpression(ANat1SetExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
public void inALessEqualPredicate(ALessEqualPredicate node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
public void inALessPredicate(ALessPredicate node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
public void inAGreaterEqualPredicate(AGreaterEqualPredicate node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
public void inAGreaterPredicate(AGreaterPredicate node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
public void inAAddExpression(AAddExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
public void inAIntervalExpression(AIntervalExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
......@@ -274,16 +274,16 @@ public class UsedStandardModules extends DepthFirstAdapter {
AMinusOrSetSubtractExpression node) {
BType t = typechecker.getType(node);
if (t instanceof IntegerType) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
}
}
public void inAMultOrCartExpression(AMultOrCartExpression node) {
BType t = typechecker.getType(node);
if (t instanceof IntegerType) {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
extendedStandardModules.add(StandardModule.Naturals);
} else {
// usedStandardModules.add(STANDARD_MODULES.RelationsNew);
// usedStandardModules.add(StandardModule.RelationsNew);
}
}
......@@ -292,26 +292,26 @@ public class UsedStandardModules extends DepthFirstAdapter {
*/
public void inAIntSetExpression(AIntSetExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Integers);
extendedStandardModules.add(StandardModule.Integers);
}
public void inAIntegerSetExpression(AIntegerSetExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Integers);
extendedStandardModules.add(StandardModule.Integers);
}
public void inAUnaryMinusExpression(AUnaryMinusExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Integers);
extendedStandardModules.add(StandardModule.Integers);
}
public void inAMinIntExpression(AMinIntExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Integers);
extendedStandardModules.add(StandardModule.Integers);
}
/**
* FiniteSets
*/
public void inACardExpression(ACardExpression node) {
extendedStandardModules.add(STANDARD_MODULES.FiniteSets);
extendedStandardModules.add(StandardModule.FiniteSets);
}
/**
......@@ -319,73 +319,73 @@ public class UsedStandardModules extends DepthFirstAdapter {
*/
public void inAPowerOfExpression(APowerOfExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAMinExpression(AMinExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAMaxExpression(AMaxExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAModuloExpression(AModuloExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inADivExpression(ADivExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAGeneralSumExpression(AGeneralSumExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAGeneralProductExpression(AGeneralProductExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inASuccessorExpression(ASuccessorExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAPredecessorExpression(APredecessorExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAPow1SubsetExpression(APow1SubsetExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAFinSubsetExpression(AFinSubsetExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAFin1SubsetExpression(AFin1SubsetExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inANotSubsetPredicate(ANotSubsetPredicate node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inANotSubsetStrictPredicate(ANotSubsetStrictPredicate node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAGeneralIntersectionExpression(
AGeneralIntersectionExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAQuantifiedIntersectionExpression(
AQuantifiedIntersectionExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
extendedStandardModules.add(StandardModule.BBuiltIns);
}
public void inAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
// usedStandardModules.add(STANDARD_MODULES.BBuiltIns);
// usedStandardModules.add(StandardModule.BBuiltIns);
}
/**
......@@ -394,9 +394,9 @@ public class UsedStandardModules extends DepthFirstAdapter {
private void setOfFunctions(Node node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof FunctionType) {
extendedStandardModules.add(STANDARD_MODULES.Functions);
extendedStandardModules.add(StandardModule.Functions);
} else {
extendedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
extendedStandardModules.add(StandardModule.FunctionsAsRelations);
}
}
......@@ -445,7 +445,7 @@ public class UsedStandardModules extends DepthFirstAdapter {
}
BType type = typechecker.getType(node.getIdentifier());
if (type instanceof SetType) {
extendedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
extendedStandardModules.add(StandardModule.FunctionsAsRelations);
}
}
......@@ -453,7 +453,7 @@ public class UsedStandardModules extends DepthFirstAdapter {
public void inATotalFunctionExpression(ATotalFunctionExpression node) {
SetType type = (SetType) typechecker.getType(node);
if (type.getSubtype() instanceof SetType) {
extendedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
extendedStandardModules.add(StandardModule.FunctionsAsRelations);
}
}
......@@ -464,27 +464,27 @@ public class UsedStandardModules extends DepthFirstAdapter {
private void evalFunctionOrRelation(Node node) {
BType t = typechecker.getType(node);
if (t instanceof FunctionType) {
extendedStandardModules.add(STANDARD_MODULES.Functions);
extendedStandardModules.add(StandardModule.Functions);
} else {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
}
public void inARelationsExpression(ARelationsExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inADomainExpression(ADomainExpression node) {
BType t = typechecker.getType(node.getExpression());
if (!(t instanceof FunctionType)) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
}
public void inASetExtensionExpression(ASetExtensionExpression node) {
BType t = typechecker.getType(node);
if (t instanceof FunctionType) {
extendedStandardModules.add(STANDARD_MODULES.TLC);
extendedStandardModules.add(StandardModule.TLC);
}
}
......@@ -531,52 +531,52 @@ public class UsedStandardModules extends DepthFirstAdapter {
BType type = typechecker.getType(((AFunctionExpression) e)
.getIdentifier());
if (type instanceof SetType) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
} else {
extendedStandardModules.add(STANDARD_MODULES.Functions);
extendedStandardModules.add(StandardModule.Functions);
}
}
}
}
public void inADirectProductExpression(ADirectProductExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inAParallelProductExpression(AParallelProductExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inACompositionExpression(ACompositionExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inAFirstProjectionExpression(AFirstProjectionExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inASecondProjectionExpression(ASecondProjectionExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inAIterationExpression(AIterationExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inAClosureExpression(AClosureExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inAReflexiveClosureExpression(AReflexiveClosureExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inATransFunctionExpression(ATransFunctionExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
public void inATransRelationExpression(ATransRelationExpression node) {
extendedStandardModules.add(STANDARD_MODULES.Relations);
extendedStandardModules.add(StandardModule.Relations);
}
/**
......@@ -586,9 +586,9 @@ public class UsedStandardModules extends DepthFirstAdapter {
public void inASeqExpression(ASeqExpression node) {
SetType type = (SetType) typechecker.getType(node);
if (type.getSubtype() instanceof FunctionType) {
extendedStandardModules.add(STANDARD_MODULES.Sequences);
extendedStandardModules.add(StandardModule.Sequences);
} else {
extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
extendedStandardModules.add(StandardModule.SequencesAsRelations);
}
}
......@@ -603,9 +603,9 @@ public class UsedStandardModules extends DepthFirstAdapter {
private void evalSequenceOrRelation(Node node) {
BType type = typechecker.getType(node);
if (type instanceof FunctionType) {
extendedStandardModules.add(STANDARD_MODULES.Sequences);
extendedStandardModules.add(StandardModule.Sequences);
} else {
extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
extendedStandardModules.add(StandardModule.SequencesAsRelations);
}
}
......@@ -624,36 +624,36 @@ public class UsedStandardModules extends DepthFirstAdapter {
private void evalSequenceExtendedOrRelation(Node node) {
BType type = typechecker.getType(node);
if (type instanceof FunctionType) {
extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
extendedStandardModules.add(StandardModule.SequencesExtended);
} else {
extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
extendedStandardModules.add(StandardModule.SequencesAsRelations);
}
}
public void inAIseqExpression(AIseqExpression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof FunctionType) {
extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
extendedStandardModules.add(StandardModule.SequencesExtended);
} else {
extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
extendedStandardModules.add(StandardModule.SequencesAsRelations);
}
}
public void inASeq1Expression(ASeq1Expression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof FunctionType) {
extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
extendedStandardModules.add(StandardModule.SequencesExtended);
} else {
extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
extendedStandardModules.add(StandardModule.SequencesAsRelations);
}
}
public void inAIseq1Expression(AIseq1Expression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof FunctionType) {
extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
extendedStandardModules.add(StandardModule.SequencesExtended);
} else {
extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
extendedStandardModules.add(StandardModule.SequencesAsRelations);
}
}
......@@ -672,9 +672,9 @@ public class UsedStandardModules extends DepthFirstAdapter {
public void inAPermExpression(APermExpression node) {
SetType set = (SetType) typechecker.getType(node);
if (set.getSubtype() instanceof SetType) {
extendedStandardModules.add(STANDARD_MODULES.SequencesAsRelations);
extendedStandardModules.add(StandardModule.SequencesAsRelations);
} else {
extendedStandardModules.add(STANDARD_MODULES.SequencesExtended);
extendedStandardModules.add(StandardModule.SequencesExtended);
}
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment