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

improve readability of some expression creations

parent b4dacadb
No related branches found
No related tags found
No related merge requests found
...@@ -24,6 +24,7 @@ import tlc2.value.impl.*; ...@@ -24,6 +24,7 @@ import tlc2.value.impl.*;
import java.util.*; import java.util.*;
import java.util.Map.Entry; import java.util.Map.Entry;
import java.util.stream.Collectors;
public class BAstCreator extends BuiltInOPs public class BAstCreator extends BuiltInOPs
implements TranslationGlobals, ASTConstants, BBuildIns, ValueConstants { implements TranslationGlobals, ASTConstants, BBuildIns, ValueConstants {
...@@ -1501,7 +1502,6 @@ public class BAstCreator extends BuiltInOPs ...@@ -1501,7 +1502,6 @@ public class BAstCreator extends BuiltInOPs
OpApplNode pair = (OpApplNode) arg; OpApplNode pair = (OpApplNode) arg;
StringNode stringNode = (StringNode) pair.getArgs()[0]; StringNode stringNode = (StringNode) pair.getArgs()[0];
pairTable.put(stringNode.getRep().toString(), visitExprOrOpArgNodeExpression(pair.getArgs()[1])); pairTable.put(stringNode.getRep().toString(), visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
} }
List<PRecEntry> recList = new ArrayList<>(); List<PRecEntry> recList = new ArrayList<>();
if (struct.isExtensible()) { if (struct.isExtensible()) {
...@@ -1539,7 +1539,7 @@ public class BAstCreator extends BuiltInOPs ...@@ -1539,7 +1539,7 @@ public class BAstCreator extends BuiltInOPs
case OPCODE_rc: { // [h_1 |-> 1, h_2 |-> 2] case OPCODE_rc: { // [h_1 |-> 1, h_2 |-> 2]
StructType struct = (StructType) n.getToolObject(TYPE_ID); StructType struct = (StructType) n.getToolObject(TYPE_ID);
if (struct.isExtensible()) { if (struct.isExtensible()) {
Hashtable<String, PExpression> pairTable = new Hashtable<>(); Map<String, PExpression> pairTable = new HashMap<>();
ExprOrOpArgNode[] args = n.getArgs(); ExprOrOpArgNode[] args = n.getArgs();
for (ExprOrOpArgNode arg : args) { for (ExprOrOpArgNode arg : args) {
OpApplNode pair = (OpApplNode) arg; OpApplNode pair = (OpApplNode) arg;
...@@ -1547,8 +1547,7 @@ public class BAstCreator extends BuiltInOPs ...@@ -1547,8 +1547,7 @@ public class BAstCreator extends BuiltInOPs
pairTable.put(stringNode.getRep().toString(), visitExprOrOpArgNodeExpression(pair.getArgs()[1])); pairTable.put(stringNode.getRep().toString(), visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
} }
List<PRecEntry> recList = new ArrayList<>(); List<PRecEntry> recList = new ArrayList<>();
for (int i = 0; i < struct.getFields().size(); i++) { for (String fieldName : struct.getFields()) {
String fieldName = struct.getFields().get(i);
ARecEntry rec = new ARecEntry(); ARecEntry rec = new ARecEntry();
rec.setIdentifier(new TIdentifierLiteral(fieldName)); rec.setIdentifier(new TIdentifierLiteral(fieldName));
if (pairTable.containsKey(fieldName)) { if (pairTable.containsKey(fieldName)) {
...@@ -1572,8 +1571,7 @@ public class BAstCreator extends BuiltInOPs ...@@ -1572,8 +1571,7 @@ public class BAstCreator extends BuiltInOPs
pairTable.put(stringNode.getRep().toString(), visitExprOrOpArgNodeExpression(pair.getArgs()[1])); pairTable.put(stringNode.getRep().toString(), visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
} }
List<PRecEntry> recList = new ArrayList<>(); List<PRecEntry> recList = new ArrayList<>();
for (int i = 0; i < struct.getFields().size(); i++) { for (String fieldName : struct.getFields()) {
String fieldName = struct.getFields().get(i);
ARecEntry rec = new ARecEntry(); ARecEntry rec = new ARecEntry();
rec.setIdentifier(new TIdentifierLiteral(fieldName)); rec.setIdentifier(new TIdentifierLiteral(fieldName));
if (pairTable.containsKey(fieldName)) { if (pairTable.containsKey(fieldName)) {
...@@ -1616,11 +1614,11 @@ public class BAstCreator extends BuiltInOPs ...@@ -1616,11 +1614,11 @@ public class BAstCreator extends BuiltInOPs
} }
case OPCODE_ite: { // IF THEN ELSE case OPCODE_ite: { // IF THEN ELSE
List<PExpression> Elsifs = new ArrayList<>(); return new AIfThenElseExpression(
AIfThenElseExpression ifthenElse = new AIfThenElseExpression(visitExprOrOpArgNodePredicate(n.getArgs()[0]), visitExprOrOpArgNodePredicate(n.getArgs()[0]),
visitExprOrOpArgNodeExpression(n.getArgs()[1]), Elsifs, visitExprOrOpArgNodeExpression(n.getArgs()[1]),
new ArrayList<>(),
visitExprOrOpArgNodeExpression(n.getArgs()[2])); visitExprOrOpArgNodeExpression(n.getArgs()[2]));
return ifthenElse;
// ALambdaExpression lambda1 = new ALambdaExpression(); // ALambdaExpression lambda1 = new ALambdaExpression();
// lambda1.setIdentifiers(createIdentifierList("t_")); // lambda1.setIdentifiers(createIdentifierList("t_"));
...@@ -1701,8 +1699,7 @@ public class BAstCreator extends BuiltInOPs ...@@ -1701,8 +1699,7 @@ public class BAstCreator extends BuiltInOPs
} }
} }
case OPCODE_seq: // ! case OPCODE_seq: { // !
{
return visitExprOrOpArgNodeExpression(n.getArgs()[0]); return visitExprOrOpArgNodeExpression(n.getArgs()[0]);
} }
...@@ -1716,31 +1713,40 @@ public class BAstCreator extends BuiltInOPs ...@@ -1716,31 +1713,40 @@ public class BAstCreator extends BuiltInOPs
case OPCODE_bf: { // \A x \in S : P case OPCODE_bf: { // \A x \in S : P
FormalParamNode[][] params = n.getBdedQuantSymbolLists(); FormalParamNode[][] params = n.getBdedQuantSymbolLists();
ArrayList<PExpression> list = new ArrayList<>(); List<PExpression> list = new ArrayList<>();
for (FormalParamNode[] param : params) { for (FormalParamNode[] param : params) {
for (FormalParamNode formalParamNode : param) { for (FormalParamNode formalParamNode : param) {
list.add(createIdentifierNode(formalParamNode)); list.add(createIdentifierNode(formalParamNode));
} }
} }
AImplicationPredicate implication = new AImplicationPredicate(); return new AConvertBoolExpression(
implication.setLeft(visitBoundsOfLocalVariables(n)); new AForallPredicate(
implication.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0])); list,
return new AConvertBoolExpression(new AForallPredicate(list, implication)); new AImplicationPredicate(
visitBoundsOfLocalVariables(n),
visitExprOrOpArgNodePredicate(n.getArgs()[0])
)
)
);
} }
case OPCODE_be: { // \E x \in S : P case OPCODE_be: { // \E x \in S : P
FormalParamNode[][] params = n.getBdedQuantSymbolLists(); FormalParamNode[][] params = n.getBdedQuantSymbolLists();
ArrayList<PExpression> list = new ArrayList<>(); List<PExpression> list = new ArrayList<>();
for (FormalParamNode[] param : params) { for (FormalParamNode[] param : params) {
for (FormalParamNode formalParamNode : param) { for (FormalParamNode formalParamNode : param) {
list.add(createIdentifierNode(formalParamNode)); list.add(createIdentifierNode(formalParamNode));
} }
} }
AConjunctPredicate conjunction = new AConjunctPredicate(); return new AConvertBoolExpression(
conjunction.setLeft(visitBoundsOfLocalVariables(n)); new AExistsPredicate(
conjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0])); list,
AExistsPredicate exists = new AExistsPredicate(list, conjunction); new AConjunctPredicate(
return new AConvertBoolExpression(exists); visitBoundsOfLocalVariables(n),
visitExprOrOpArgNodePredicate(n.getArgs()[0])
)
)
);
} }
} }
...@@ -1806,7 +1812,6 @@ public class BAstCreator extends BuiltInOPs ...@@ -1806,7 +1812,6 @@ public class BAstCreator extends BuiltInOPs
private PExpression createProjectionFunction(PExpression pair, int field, TLAType t) { private PExpression createProjectionFunction(PExpression pair, int field, TLAType t) {
TupleType tuple = (TupleType) t; TupleType tuple = (TupleType) t;
int size = tuple.getTypes().size();
AFunctionExpression returnFunc = new AFunctionExpression(); AFunctionExpression returnFunc = new AFunctionExpression();
int index; int index;
...@@ -1818,35 +1823,33 @@ public class BAstCreator extends BuiltInOPs ...@@ -1818,35 +1823,33 @@ public class BAstCreator extends BuiltInOPs
)); ));
} else { } else {
index = field; index = field;
ASecondProjectionExpression second = new ASecondProjectionExpression(); List<TLAType> typeList = new ArrayList<>();
ArrayList<TLAType> typeList = new ArrayList<>();
for (int i = 0; i < field - 1; i++) { for (int i = 0; i < field - 1; i++) {
typeList.add(tuple.getTypes().get(i)); typeList.add(tuple.getTypes().get(i));
} }
second.setExp1(createNestedCouple(typeList)); // we could use AEventBSecondProjectionV2Expression here (which would be much easier),
second.setExp2(tuple.getTypes().get(field - 1).getBNode()); // but this is only supported by ProB (?)
returnFunc.setIdentifier(second); returnFunc.setIdentifier(new ASecondProjectionExpression(
createNestedCouple(typeList),
tuple.getTypes().get(field - 1).getBNode()
));
} }
AFunctionExpression func = returnFunc; AFunctionExpression func = returnFunc;
for (int i = index; i < size; i++) { for (int i = index; i < tuple.getTypes().size(); i++) {
AFunctionExpression newfunc = new AFunctionExpression(); AFunctionExpression newfunc = new AFunctionExpression();
AFirstProjectionExpression first = new AFirstProjectionExpression(); List<TLAType> typeList = new ArrayList<>();
ArrayList<TLAType> typeList = new ArrayList<>();
for (int j = 0; j < i; j++) { for (int j = 0; j < i; j++) {
typeList.add(tuple.getTypes().get(j)); typeList.add(tuple.getTypes().get(j));
} }
first.setExp1(createNestedCouple(typeList)); newfunc.setIdentifier(new AFirstProjectionExpression(
first.setExp2(tuple.getTypes().get(i).getBNode()); createNestedCouple(typeList),
newfunc.setIdentifier(first); tuple.getTypes().get(i).getBNode()
));
ArrayList<PExpression> list = new ArrayList<>(); func.setParameters(Collections.singletonList(newfunc));
list.add(newfunc);
func.setParameters(list);
func = newfunc; func = newfunc;
} }
ArrayList<PExpression> list = new ArrayList<>(); func.setParameters(Collections.singletonList(pair));
list.add(pair);
func.setParameters(list);
return returnFunc; return returnFunc;
} }
...@@ -1874,39 +1877,26 @@ public class BAstCreator extends BuiltInOPs ...@@ -1874,39 +1877,26 @@ public class BAstCreator extends BuiltInOPs
} }
private PExpression createUnboundedChoose(OpApplNode n) { private PExpression createUnboundedChoose(OpApplNode n) {
ADefinitionExpression defCall = new ADefinitionExpression(); return new ADefinitionExpression(
defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE")); new TIdentifierLiteral("CHOOSE"),
AComprehensionSetExpression comprehension = new AComprehensionSetExpression(); Collections.singletonList(new AComprehensionSetExpression(
List<PExpression> paramList = new ArrayList<>(); Arrays.stream(n.getUnbdedQuantSymbols()).map(this::createIdentifierNode).collect(Collectors.toList()),
for (FormalParamNode param : n.getUnbdedQuantSymbols()) { visitExprOrOpArgNodePredicate(n.getArgs()[0])
paramList.add(createIdentifierNode(param)); ))
} );
comprehension.setIdentifiers(paramList);
comprehension.setPredicates(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
List<PExpression> list = new ArrayList<>();
list.add(comprehension);
defCall.setParameters(list);
return defCall;
} }
private PExpression createBoundedChoose(OpApplNode n) { private PExpression createBoundedChoose(OpApplNode n) {
ADefinitionExpression defCall = new ADefinitionExpression(); return new ADefinitionExpression(
defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE")); new TIdentifierLiteral("CHOOSE"),
AComprehensionSetExpression comprehension = new AComprehensionSetExpression(); Collections.singletonList(new AComprehensionSetExpression(
List<PExpression> paramList = new ArrayList<>(); Arrays.stream(n.getBdedQuantSymbolLists()[0]).map(this::createIdentifierNode).collect(Collectors.toList()),
for (FormalParamNode param : n.getBdedQuantSymbolLists()[0]) { new AConjunctPredicate(
paramList.add(createIdentifierNode(param)); visitBoundsOfLocalVariables(n),
} visitExprOrOpArgNodePredicate(n.getArgs()[0])
comprehension.setIdentifiers(paramList); )
PPredicate typingPredicate = visitBoundsOfLocalVariables(n); ))
AConjunctPredicate conj = new AConjunctPredicate(); );
conj.setLeft(typingPredicate);
conj.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
comprehension.setPredicates(conj);
List<PExpression> list = new ArrayList<>();
list.add(comprehension);
defCall.setParameters(list);
return defCall;
} }
private PExpression createCaseNode(OpApplNode n) { private PExpression createCaseNode(OpApplNode n) {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment