diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index c090fceb3f44c947ae28b066ed462b86e07f96ca..c78aac7a5c07a68553e3de8280fb3ae58f435e23 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -825,14 +825,40 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
domList.add(d);
}
domType = new TupleType(domList);
+ FunctionType func = new FunctionType(domType, expected);
+ TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
+ return ((FunctionType) res).getRange();
} else {
+ ExprOrOpArgNode arg = n.getArgs()[1];
+ if (arg instanceof NumeralNode) {
+ NumeralNode num = (NumeralNode) arg;
+ UntypedType u = new UntypedType();
+ n.setToolObject(TYPE_ID, u);
+ u.addFollower(n);
+ TupleOrFunction tupleOrFunc = new TupleOrFunction(
+ num.val(), u);
+ TLAType funcOrTuple = visitExprOrOpArgNode(n.getArgs()[0], tupleOrFunc);
+ n.getArgs()[0].setToolObject(TYPE_ID, funcOrTuple);
+ if(funcOrTuple instanceof AbstractHasFollowers){
+ ((AbstractHasFollowers) funcOrTuple).addFollower(n.getArgs()[0]);
+ }
+
+ TLAType found = (TLAType) n.getToolObject(TYPE_ID);
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException("Expected '" + expected
+ + "', found '" + found + "'.\n" + n.getLocation());
+ }
+ return found;
+ }
domType = visitExprOrOpArgNode(n.getArgs()[1],
new UntypedType());
}
-
FunctionType func = new FunctionType(domType, expected);
TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
return ((FunctionType) res).getRange();
+
}
/***********************************************************************
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index d89e24030c51ff9f7f772c3bf4bd32f652d0ca2a..c19d2f6a39b970e494bb466290eb6821e8cac6bc 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -9,15 +9,16 @@ import de.be4.classicalb.core.parser.analysis.ExtendedDFAdapter;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
-import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
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.AFirstProjectionExpression;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.ALambdaExpression;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.ASecondProjectionExpression;
import de.be4.classicalb.core.parser.node.ASelectSubstitution;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -103,8 +104,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
putDeclarationClause("ASetsMachineClause", "SETS", ";");
putDeclarationClause("AAbstractConstantsMachineClause",
"ABSTRACT_CONSTANTS", ",");
- putDeclarationClause("AConstantsMachineClause",
- "CONSTANTS", ",");
+ putDeclarationClause("AConstantsMachineClause", "CONSTANTS", ",");
putDeclarationClause("AVariablesMachineClause", "VARIABLES", ",");
put("AEnumeratedSetSet", null, null, ", ", null, " = {", "}");
@@ -152,7 +152,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);
@@ -213,6 +213,9 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
put("AComprehensionSetExpression", "{", "", ",", "", " | ", "}");
+ put("AFirstProjectionExpression", "prj1(", null, null, null, ", ", ")");
+
+ put("ASecondProjectionExpression", "prj2(", null, null, null, ", ", ")");
}
@Override
diff --git a/src/main/java/de/tla2b/types/AbstractHasFollowers.java b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
index b7105c6f54a7a61c367032c9f5e49c2c345f6d88..2666c759cdd3befacac737353daf9a6d67b98796 100644
--- a/src/main/java/de/tla2b/types/AbstractHasFollowers.java
+++ b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
@@ -76,6 +76,8 @@ public abstract class AbstractHasFollowers extends TLAType {
((StructType) follower).setNewType(this, newType);
} else if (follower instanceof StructOrFunctionType) {
((StructOrFunctionType) follower).setNewType(this, newType);
+ } else if (follower instanceof TupleOrFunction) {
+ ((TupleOrFunction) follower).setNewType(this, newType);
} else {
throw new RuntimeException("Unknown follower type: "
+ follower.getClass());
diff --git a/src/main/java/de/tla2b/types/FunctionType.java b/src/main/java/de/tla2b/types/FunctionType.java
index ad97f8dba17956e06fc2e6e872c23f3b075bc956..bd2656b35f873e15428052bd3f0058c2ec6afa69 100644
--- a/src/main/java/de/tla2b/types/FunctionType.java
+++ b/src/main/java/de/tla2b/types/FunctionType.java
@@ -42,6 +42,9 @@ public class FunctionType extends AbstractHasFollowers {
if(o instanceof TupleType){
return o.compare(this);
}
+ if(o instanceof TupleOrFunction){
+ return o.compare(this);
+ }
return false;
}
@@ -78,6 +81,9 @@ public class FunctionType extends AbstractHasFollowers {
if (o instanceof TupleType){
return (FunctionType) o.unify(this);
}
+ if(o instanceof TupleOrFunction){
+ return (FunctionType) o.unify(this);
+ }
throw new RuntimeException();
}
diff --git a/src/main/java/de/tla2b/types/IType.java b/src/main/java/de/tla2b/types/IType.java
index a363a9daa6dc5eb9d320aed90ac182d64106e1bf..b55529539748af08bba20a63032d1fcac75c8edb 100644
--- a/src/main/java/de/tla2b/types/IType.java
+++ b/src/main/java/de/tla2b/types/IType.java
@@ -15,6 +15,7 @@ public interface IType {
public final int STRUCT_OR_FUNCTION = 9;
public final int FUNCTION = 10;
public final int TUPLE = 11;
+ public final int TUPLE_OR_FUNCTION =12;
void apply(TypeVisitorInterface visitor);
}
diff --git a/src/main/java/de/tla2b/types/SetType.java b/src/main/java/de/tla2b/types/SetType.java
index e6d19ea46538abca75aec462292e882bca1b96a1..4f5780bcc641b43874adce99886f70554baab87d 100644
--- a/src/main/java/de/tla2b/types/SetType.java
+++ b/src/main/java/de/tla2b/types/SetType.java
@@ -68,10 +68,6 @@ public class SetType extends AbstractHasFollowers {
if (o.getKind() == UNTYPED)
return true;
- if (o instanceof StructOrFunctionType){
- return o.compare(this);
- }
-
if (o instanceof SetType) {
SetType p = (SetType) o;
// test sub types compatibility
diff --git a/src/main/java/de/tla2b/types/StructOrFunctionType.java b/src/main/java/de/tla2b/types/StructOrFunctionType.java
index 9b662311900d1f6c62b823e496caa0575acaf070..fc4aea18059a0c65577465890ee993eb8bbba115 100644
--- a/src/main/java/de/tla2b/types/StructOrFunctionType.java
+++ b/src/main/java/de/tla2b/types/StructOrFunctionType.java
@@ -80,25 +80,6 @@ public class StructOrFunctionType extends AbstractHasFollowers {
}
return true;
}
- if (o instanceof SetType) {
- SetType p = (SetType) o;
- TLAType sub = p.getSubType();
- if (sub.getKind() == UNTYPED)
- return true;
-
- if (sub instanceof PairType) {
- PairType pair = (PairType) sub;
- if (pair.getFirst().compare(StringType.getInstance())) {
- for (String key : types.keySet()) {
- if (!pair.getSecond().compare(types.get(key)))
- return false;
- }
- return true;
- } else
- return false;
- } else
- return false;
- }
if (o instanceof StructOrFunctionType) {
StructOrFunctionType s = (StructOrFunctionType) o;
@@ -114,9 +95,7 @@ public class StructOrFunctionType extends AbstractHasFollowers {
}
}
return true;
-
}
-
return false;
}
@@ -135,12 +114,6 @@ public class StructOrFunctionType extends AbstractHasFollowers {
@Override
public boolean isUntyped() {
return true;
- // Iterator<BType> itr = types.values().iterator();
- // while (itr.hasNext()) {
- // if (itr.next().isUntyped())
- // return true;
- // }
- // return false;
}
@Override
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index 0c22efd19f312a081a6dba3cf104b1ccfe654f1e..b93441cfb9b42fecf1539b584b106609808d240b 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -87,11 +87,15 @@ public class TupleType extends AbstractHasFollowers {
return false;
}
}
- if(!compareToAll(range)){
+ if (!compareToAll(range)) {
return false;
}
return true;
}
+ if (o instanceof TupleOrFunction) {
+ return o.compare(this);
+ }
+
return false;
}
@@ -182,6 +186,9 @@ public class TupleType extends AbstractHasFollowers {
}
}
+ if (o instanceof TupleOrFunction) {
+ return o.unify(this);
+ }
throw new RuntimeException();
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index cc6d9f61b55730fa5984ed9efd8502e3cd8ca1fa..e89a5390fd0d67f1a8520b6c098c568e455aab4b 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -1449,24 +1449,33 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
case OPCODE_fa: { // f[1]
- AFunctionExpression func = new AFunctionExpression();
- func.setIdentifier(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
- List<PExpression> paramList = new ArrayList<PExpression>();
-
- ExprOrOpArgNode dom = n.getArgs()[1];
- if (dom instanceof OpApplNode
- && ((OpApplNode) dom).getOperator().getName().toString()
- .equals("$Tuple")) {
- OpApplNode domOpAppl = (OpApplNode) dom;
- for (int i = 0; i < domOpAppl.getArgs().length; i++) {
- paramList.add(visitExprOrOpArgNodeExpression(domOpAppl
- .getArgs()[i]));
- }
+ TLAType t = (TLAType) n.getArgs()[0].getToolObject(TYPE_ID);
+ if (t != null && t instanceof TupleType) {
+ NumeralNode num = (NumeralNode) n.getArgs()[1];
+ int field = num.val();
+ System.out.println(t);
+ return createProjectionFunction(n, field, t);
} else {
- paramList.add(visitExprOrOpArgNodeExpression(dom));
+ AFunctionExpression func = new AFunctionExpression();
+ func.setIdentifier(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ List<PExpression> paramList = new ArrayList<PExpression>();
+
+ ExprOrOpArgNode dom = n.getArgs()[1];
+ if (dom instanceof OpApplNode
+ && ((OpApplNode) dom).getOperator().getName()
+ .toString().equals("$Tuple")) {
+ OpApplNode domOpAppl = (OpApplNode) dom;
+ for (int i = 0; i < domOpAppl.getArgs().length; i++) {
+ paramList.add(visitExprOrOpArgNodeExpression(domOpAppl
+ .getArgs()[i]));
+ }
+ } else {
+ paramList.add(visitExprOrOpArgNodeExpression(dom));
+ }
+ func.setParameters(paramList);
+ return func;
}
- func.setParameters(paramList);
- return func;
+
}
case OPCODE_domain:
@@ -1791,6 +1800,76 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
throw new RuntimeException(n.getOperator().getName().toString());
}
+ private PExpression createProjectionFunction(OpApplNode n, int field,
+ TLAType t) {
+ TupleType tuple = (TupleType) t;
+ int size = tuple.getTypes().size();
+
+ AFunctionExpression returnFunc = new AFunctionExpression();
+ int index;
+ if (field == 1) {
+ index = 2;
+ AFirstProjectionExpression first = new AFirstProjectionExpression();
+ first.setExp1(tuple.getTypes().get(0).getBNode());
+ first.setExp2(tuple.getTypes().get(1).getBNode());
+ returnFunc.setIdentifier(first);
+ }else{
+ index = field;
+ ASecondProjectionExpression second = new ASecondProjectionExpression();
+ ArrayList<TLAType> typeList = new ArrayList<TLAType>();
+ for (int i = 0; i < field - 1; i++) {
+ typeList.add(tuple.getTypes().get(i));
+ }
+ second.setExp1(createNestedCoupleAsBNode(typeList));
+ second.setExp2(tuple.getTypes().get(field - 1).getBNode());
+ returnFunc.setIdentifier(second);
+ }
+ AFunctionExpression func = returnFunc;
+ for (int i = index; i < size; i++) {
+ AFunctionExpression newfunc = new AFunctionExpression();
+ AFirstProjectionExpression first = new AFirstProjectionExpression();
+ ArrayList<TLAType> typeList = new ArrayList<TLAType>();
+ for (int j = 0; j < i; j++) {
+ typeList.add(tuple.getTypes().get(j));
+ }
+ first.setExp1(createNestedCoupleAsBNode(typeList));
+ first.setExp2(tuple.getTypes().get(i).getBNode());
+ newfunc.setIdentifier(first);
+
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ list.add(newfunc);
+ func.setParameters(list);
+ func = newfunc;
+ }
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ list.add(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ func.setParameters(list);
+ return returnFunc;
+ }
+
+ public static PExpression createNestedCoupleAsBNode(List<TLAType> typeList) {
+ if (typeList.size() == 1) {
+ return typeList.get(0).getBNode();
+ }
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (TLAType t : typeList) {
+ list.add(t.getBNode());
+ }
+ AMultOrCartExpression card = new AMultOrCartExpression();
+ card.setLeft(list.get(0));
+ for (int i = 1; i < list.size(); i++) {
+ if (i < list.size() - 1) {
+ AMultOrCartExpression old = card;
+ old.setRight(list.get(i));
+ card = new AMultOrCartExpression();
+ card.setLeft(old);
+ } else {
+ card.setRight(list.get(i));
+ }
+ }
+ return card;
+ }
+
private PExpression createUnboundedChoose(OpApplNode n) {
ADefinitionExpression defCall = new ADefinitionExpression();
defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
diff --git a/src/test/java/de/tla2b/prettyprintb/RecordTest.java b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
index 175057c6967aab781a00af3d1aa157717a910c79..c956984edb449197afe511bd9b18718d8e9c2b00 100644
--- a/src/test/java/de/tla2b/prettyprintb/RecordTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
@@ -127,5 +127,5 @@ public class RecordTest {
+ "END";
compare(expected, module);
}
-
+
}
diff --git a/src/test/java/de/tla2b/prettyprintb/TupleTest.java b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
index d5e7472295f60b9ca7ff5c715315d523fea64542..8894ceaabef46529fb7f6d142f8afed982aff12b 100644
--- a/src/test/java/de/tla2b/prettyprintb/TupleTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
@@ -7,42 +7,112 @@ package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Test;
-
public class TupleTest {
-
+
@Test
public void testTuple() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME <<TRUE,1,TRUE>> /= <<TRUE,2,TRUE>>\n"
+ "=================================";
-
+
final String expected = "MACHINE Testing\n"
+ "PROPERTIES (TRUE,1,TRUE) /= (TRUE,2,TRUE) \n" + "END";
compare(expected, module);
}
-
+
@Test
public void testCartesianProduct() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME <<TRUE,1>> \\in BOOLEAN \\X {1} \n"
+ "=================================";
-
+
final String expected = "MACHINE Testing\n"
+ "PROPERTIES (TRUE,1) : BOOL*{1} \n" + "END";
compare(expected, module);
}
-
+
@Test
public void testCartesianProduct2() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = BOOLEAN \\X ({1} \\X BOOLEAN) \n"
+ "=================================";
-
- final String expected = "MACHINE Testing\n"+ "CONSTANTS k\n"
- + "PROPERTIES k : POW(BOOL * (INTEGER * BOOL)) & k = BOOL*({1}*BOOL) \n" + "END";
+
+ final String expected = "MACHINE Testing\n"
+ + "CONSTANTS k\n"
+ + "PROPERTIES k : POW(BOOL * (INTEGER * BOOL)) & k = BOOL*({1}*BOOL) \n"
+ + "END";
compare(expected, module);
}
-
-
+
+ @Test
+ public void testTupleFunctionCall() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME 1 = <<1,TRUE>>[1] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES 1 = prj1(INTEGER, BOOL)((1,TRUE)) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testTupleFunctionCall2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME TRUE = <<1,TRUE>>[2] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES TRUE = prj2(INTEGER, BOOL)((1,TRUE)) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testTupleFunctionCall3() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME 1 = <<1,TRUE,1>>[3] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES 1 = prj2(INTEGER * BOOL, INTEGER)((1,TRUE,1)) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testTupleFunctionCall4() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME 1 = <<1,TRUE,1>>[1] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES 1 = prj1(INTEGER, BOOL)((prj1(INTEGER * BOOL, INTEGER)((1,TRUE,1)))) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testTupleFunctionCall5() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME 1 = <<1,TRUE,2>>[1] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES 1 = prj1(INTEGER, BOOL)((prj1(INTEGER * BOOL, INTEGER)((1,TRUE,2)))) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testTupleFunctionCall6() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME 1 = <<1,TRUE,2,FALSE>>[1] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES 1 = prj1(INTEGER, BOOL)((prj1(INTEGER * BOOL, INTEGER)((prj1((INTEGER * BOOL) * INTEGER, BOOL)((1,TRUE,2,FALSE)))))) \n"
+ + "END";
+ compare(expected, module);
+ }
+
}
diff --git a/src/test/java/de/tla2b/typechecking/StructTest.java b/src/test/java/de/tla2b/typechecking/StructTest.java
index 360131c61b56ed09d872b47de8ac0243f8bbe42a..ddd967e513aa8510928ec1e3dd253ecd06924f02 100644
--- a/src/test/java/de/tla2b/typechecking/StructTest.java
+++ b/src/test/java/de/tla2b/typechecking/StructTest.java
@@ -6,6 +6,7 @@ package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
+import org.junit.Ignore;
import org.junit.Test;
import de.tla2b.exceptions.FrontEndException;
@@ -13,7 +14,6 @@ import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
-
import util.ToolIO;
public class StructTest {
@@ -274,4 +274,14 @@ public class StructTest {
+ "=================================";
TestUtil.typeCheckString(module);
}
+
+ @Test (expected = TypeErrorException.class)
+ public void testRecord5() throws FrontEndException,
+ TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k, k2 \n"
+ + "ASSUME k = [k EXCEPT !.a = 1] /\\ k ={k2} \n"
+ + "=================================";
+ TestUtil.typeCheckString(module);
+ }
}
diff --git a/src/test/java/de/tla2b/typechecking/TupleTest.java b/src/test/java/de/tla2b/typechecking/TupleTest.java
index 2d4fe86ea1ae41e1de92c74b59e6d62925ca18d6..7ac78dc14b23494b555eb6a87a8c39578e8697d7 100644
--- a/src/test/java/de/tla2b/typechecking/TupleTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleTest.java
@@ -27,7 +27,6 @@ public class TupleTest {
}
- @Ignore
@Test
public void testTupleFunctionCall() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -37,7 +36,19 @@ public class TupleTest {
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("ka", t.getConstantType("k").toString());
+ assertEquals("BOOL", t.getConstantType("k").toString());
+ }
+
+ @Test
+ public void testTupleFunctionCall2() throws FrontEndException, TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = <<1,TRUE,\"str\">>[3] \n"
+ + "=================================";
+
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("STRING", t.getConstantType("k").toString());
}
@Test