diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index 9c8902b2470621e3f45becc008e4009cd8bca684..a0359d0c4d6c1cf8610ec40b77e9818c61d52706 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -12,9 +12,9 @@ import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.AExpressionParseUnit;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.ALambdaExpression;
+import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
@@ -150,7 +150,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
putInfixOperator("AAddExpression", "+", 180, left);
putInfixOperator("AMinusOrSetSubtractExpression", "-", 180, left);
-
+
putInfixOperator("ACartesianProductExpression", "*", 190, left);
putInfixOperator("AMultOrCartExpression", "*", 190, left);
putInfixOperator("ADivExpression", "/", 190, left);
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 80b2bda6c3a8055001dd0cac65c65a5386bdfc3e..a6e7987992785c623d59cf8c8af01d3fac11a89c 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -9,6 +9,7 @@ import java.util.List;
import java.util.Map.Entry;
import java.util.Set;
+import sun.audio.AudioPlayer;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.AtNode;
@@ -24,6 +25,7 @@ import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.StringNode;
import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
+import tlc2.value.ModelValue;
import tlc2.value.SetEnumValue;
import tlc2.value.Value;
import tlc2.value.ValueConstants;
@@ -79,6 +81,7 @@ import de.be4.classicalb.core.parser.node.ALessPredicate;
import de.be4.classicalb.core.parser.node.AMachineHeader;
import de.be4.classicalb.core.parser.node.AMachineMachineVariant;
import de.be4.classicalb.core.parser.node.AMemberPredicate;
+import de.be4.classicalb.core.parser.node.AMinusExpression;
import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
import de.be4.classicalb.core.parser.node.ANaturalSetExpression;
@@ -235,6 +238,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
+
+
private void createSetsClause() {
if (conEval == null || conEval.getEnumerationSet() == null
|| conEval.getEnumerationSet().size() == 0)
@@ -245,6 +250,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
OpDeclNode[] cons = moduleNode.getConstantDecls();
for (int i = 0; i < cons.length; i++) {
TLAType type = (TLAType) cons[i].getToolObject(TYPE_ID);
+
EnumType e = null;
if (type instanceof SetType) {
if (((SetType) type).getSubType() instanceof EnumType) {
@@ -260,7 +266,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
}
-
+
ArrayList<PSet> sets = new ArrayList<PSet>();
for (int i = 0; i < printed.size(); i++) {
AEnumeratedSetSet eSet = new AEnumeratedSetSet();
@@ -693,8 +699,21 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return new AIntegerExpression(new TIntegerLiteral(
tlcValue.toString()));
+ case SETENUMVALUE: {
+ SetEnumValue s = (SetEnumValue) tlcValue;
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 0; i < s.elems.size(); i++) {
+ Value v = s.elems.elementAt(i);
+ ModelValue m = (ModelValue) v;
+ AIdentifierExpression id = createIdentifierNode(m.toString());
+ list.add(id);
+ }
+ return new ASetExtensionExpression(list);
}
+ }
+
+ System.out.println(tlcValue);
throw new RuntimeException();
}
@@ -1174,18 +1193,48 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return new ATailExpression(
visitExprOrOpArgNodeExpression(n.getArgs()[0]));
- case B_OPCODE_subseq: { // SubSeq(s,m,n)
- ARestrictFrontExpression restrictFront = new ARestrictFrontExpression();
- restrictFront
- .setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
- restrictFront
- .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
-
- ARestrictTailExpression restrictTail = new ARestrictTailExpression();
- restrictTail.setLeft(restrictFront);
- restrictTail
- .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
- return restrictTail;
+ case B_OPCODE_subseq: { // SubSeq(s,a,b)
+ //%p.(p : 1..(b-a+1)| s(p+a-1))
+ ALambdaExpression lambda = new ALambdaExpression();
+ lambda.setIdentifiers(createIdentifierList("t_"));
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(createIdentifierNode("t_"));
+ AIntervalExpression interval = new AIntervalExpression();
+ interval.setLeftBorder(new AIntegerExpression(new TIntegerLiteral("1")));
+ AMinusOrSetSubtractExpression minus = new AMinusOrSetSubtractExpression();
+ minus.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
+ minus.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
+ AAddExpression add = new AAddExpression();
+ add.setLeft(minus);
+ add.setRight(new AIntegerExpression(new TIntegerLiteral("1")));
+ interval.setRightBorder(add);
+ member.setRight(interval);
+ lambda.setPredicate(member);
+ AAddExpression add2 = new AAddExpression();
+ add2.setLeft(createIdentifierNode("t_"));
+ add2.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
+ AMinusOrSetSubtractExpression minus2 = new AMinusOrSetSubtractExpression();
+ minus2.setLeft(add2);
+ minus2.setRight(new AIntegerExpression(new TIntegerLiteral("1")));
+ ArrayList<PExpression> params = new ArrayList<PExpression>();
+ params.add(minus2);
+ AFunctionExpression func = new AFunctionExpression();
+ func.setIdentifier(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ func.setParameters(params);
+ lambda.setExpression(func);
+ return lambda;
+
+// ARestrictFrontExpression restrictFront = new ARestrictFrontExpression();
+// restrictFront
+// .setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+// restrictFront
+// .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
+//
+// ARestrictTailExpression restrictTail = new ARestrictTailExpression();
+// restrictTail.setLeft(restrictFront);
+// restrictTail
+// .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
+// return restrictTail;
}
}
diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/SequencesTest.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/SequencesTest.java
index 70094e42e33fe891c82457e087c183172d597e5f..b179ebce34099b111dda4ccfe5ff44d1335151dc 100644
--- a/src/test/java/de/tla2b/prettyprintb/standardmodules/SequencesTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/SequencesTest.java
@@ -86,7 +86,7 @@ public class SequencesTest {
+ "ASSUME SubSeq(<<1,2,3,4,5>>, 2, 3) = <<2,3>> \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "PROPERTIES ([1,2,3,4,5] /|\\ 3) \\|/ 2 = [2,3] \n"
+ + "PROPERTIES %(t_).(t_ : 1 .. (3 - 2) + 1 | [1,2,3,4,5](((t_ + 2) - 1))) = [2,3] \n"
+ "END";
compare(expected, module);
}