operators without parameters have a fixed type

src/main/java/de/tla2b/analysis/TypeChecker.java

@@ -9,6 +9,7 @@ import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.Iterator;
 import java.util.LinkedList;
+import java.util.List;
 import java.util.Set;
 import java.util.Map.Entry;
 
@@ -332,7 +333,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						exprNode.getLocation()));
 			}
 
-
 		}
 
 		case LetInKind: {
@@ -365,6 +365,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 		}
 	}
 
+	private TLAType getType(OpApplNode n) {
+		return (TLAType) n.getToolObject(TYPE_ID);
+	}
 
 	/**
 	 * @param n
@@ -458,10 +461,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			}
 
 			TLAType found = ((TLAType) def.getToolObject(TYPE_ID));
-			if (found == null)
+			if (found == null){
 				found = new UntypedType();
 			// throw new RuntimeException(def.getName() + " has no type yet!");
+			}
+			if(n.getArgs().length != 0){
 				found = found.cloneTLAType();
+			}
+			
 			try {
 				found = found.unify(expected);
 			} catch (UnificationException e) {
@@ -867,8 +874,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 					n.getArgs()[0].setToolObject(TYPE_ID, res);
 					tupleNodeList.add(n.getArgs()[0]);
 					if (res instanceof AbstractHasFollowers) {
-						((AbstractHasFollowers) res).addFollower(n
-								.getArgs()[0]);
+						((AbstractHasFollowers) res)
+								.addFollower(n.getArgs()[0]);
 					}
 					TLAType found = (TLAType) n.getToolObject(TYPE_ID);
 					try {
@@ -1069,14 +1076,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 		}
 
 		case OPCODE_uc: {
-			TLAType found = new UntypedType();
-			FormalParamNode x = n.getUnbdedQuantSymbols()[0];
-			symbolNodeList.add(x);
-			x.setToolObject(TYPE_ID, found);
-			((AbstractHasFollowers) found).addFollower(x);
-			visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
-
-			found = (TLAType) x.getToolObject(TYPE_ID);
+			List<TLAType> list = new ArrayList<TLAType>();
+			for (FormalParamNode param : n.getUnbdedQuantSymbols()) {
+				TLAType paramType = new UntypedType();
+				symbolNodeList.add(param);
+				setType(param, paramType);
+				list.add(paramType);
+			}
+			TLAType found = null;
+			if (list.size() == 1) {
+				found = list.get(0);
+			} else {
+				found = new TupleType(list);
+			}
 			try {
 				found = found.unify(expected);
 			} catch (UnificationException e) {
@@ -1084,20 +1096,15 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						"Expected %s, found %s at 'CHOOSE',%n%s", expected,
 						found, n.getLocation()));
 			}
-			return found;
-		}
+			setType(n, found);
+			visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
+
+			return getType(n);
 
-		case OPCODE_bc: { // CHOOSE x \in S: P
-			if (n.isBdedQuantATuple()[0]) {
-				throw new TypeErrorException(
-						"A tuple as parameter within the set constructor is not permitted.\n"
-								+ n.getLocation());
 		}
-			ExprNode[] bounds = n.getBdedQuantBounds();
-			SetType S = (SetType) visitExprNode(bounds[0], new SetType(
-					new UntypedType()));
-			TLAType found = S.getSubType();
 
+		case OPCODE_bc: { // CHOOSE x \in S: P
+			TLAType found = evalBoundedVariables(n);
 			try {
 				found = found.unify(expected);
 			} catch (UnificationException e) {
@@ -1105,12 +1112,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						"Expected %s, found %s at 'CHOOSE',%n%s", expected,
 						found, n.getLocation()));
 			}
-			FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
-			symbolNodeList.add(x);
-			x.setToolObject(TYPE_ID, found);
-			if (found instanceof AbstractHasFollowers) {
-				((AbstractHasFollowers) found).addFollower(x);
-			}
 			visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
 			return found;
 		}
@@ -1205,8 +1206,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 		return domType;
 	}
 
-	
-	
 	/**
 	 * @param n
 	 * @param expected

src/main/java/de/tla2bAst/BAstCreator.java

@@ -2020,8 +2020,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		ADefinitionExpression defCall = new ADefinitionExpression();
 		defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
 		AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
-		FormalParamNode x = n.getUnbdedQuantSymbols()[0];
-		comprehension.setIdentifiers(createIdentifierList(getName(x)));
+		List<PExpression> paramList = new ArrayList<PExpression>();
+		for (FormalParamNode param : n.getUnbdedQuantSymbols()) {
+			paramList.add(createIdentifierNode(param));
+		}
+		comprehension.setIdentifiers(paramList);
 		comprehension
 				.setPredicates(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
 		List<PExpression> list = new ArrayList<PExpression>();
@@ -2034,14 +2037,14 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		ADefinitionExpression defCall = new ADefinitionExpression();
 		defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
 		AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
-		FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
-		comprehension.setIdentifiers(createIdentifierList(x));
-		AMemberPredicate member = new AMemberPredicate();
-		member.setLeft(createIdentifierNode(x));
-		ExprNode in = n.getBdedQuantBounds()[0];
-		member.setRight(visitExprNodeExpression(in));
+		List<PExpression> paramList = new ArrayList<PExpression>();
+		for (FormalParamNode param : n.getBdedQuantSymbolLists()[0]) {
+			paramList.add(createIdentifierNode(param));
+		}
+		comprehension.setIdentifiers(paramList);
+		PPredicate typingPredicate = visitBoundsOfLocalVariables(n);
 		AConjunctPredicate conj = new AConjunctPredicate();
-		conj.setLeft(member);
+		conj.setLeft(typingPredicate);
 		conj.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
 		comprehension.setPredicates(conj);
 		List<PExpression> list = new ArrayList<PExpression>();

src/test/java/de/tla2b/prettyprintb/MiscellaneousConstructsTest.java

@@ -131,6 +131,21 @@ public class MiscellaneousConstructsTest {
 		compare(expected, module);
 	}
 	
+
+	
+	@Test
+	public void testUnBoundedChooseTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME <<1,TRUE>> = CHOOSE <<a,b>> \\in {<<1,TRUE>>}: TRUE \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+				+ "PROPERTIES (1,TRUE) = CHOOSE({a,b | (a,b) : {(1,TRUE)} & TRUE = TRUE}) \n" + "END";
+		compare(expected, module);
+	}
+	
+	
 	@Test
 	public void testBoundedChoosePredicate() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
@@ -142,4 +157,28 @@ public class MiscellaneousConstructsTest {
 				+ "PROPERTIES CHOOSE({x | x : {TRUE} & TRUE = TRUE}) = TRUE \n" + "END";
 		compare(expected, module);
 	}
+	
+	@Test
+	public void testBoundedChooseTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME <<1,TRUE>> = CHOOSE <<a,b>> \\in {<<1,TRUE>>}: TRUE \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+				+ "PROPERTIES (1,TRUE) = CHOOSE({a,b | (a,b) : {(1,TRUE)} & TRUE = TRUE}) \n" + "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testUnboundedChooseTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME <<1,TRUE>> = CHOOSE <<a,b>> : <<a,b>> = <<1,TRUE>>\n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+				+ "PROPERTIES (1,TRUE) = CHOOSE({a,b | (a,b) = (1,TRUE)}) \n" + "END";
+		compare(expected, module);
+	}
 }

src/test/java/de/tla2b/prettyprintb/TupleTest.java

@@ -141,6 +141,23 @@ public class TupleTest {
 		compare(expected, module);
 	}
 	
+	@Ignore
+	@Test
+	public void testAtTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k, k2 \n"
+				+ "ASSUME k =[i \\in Nat |-> <<1, \"s\">>] /\\ k2 = [ k EXCEPT ![22] = <<@[1],\"d\">>] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "CONSTANTS k, k2 \n"
+				+ "PROPERTIES \n"
+				+ "(k : INTEGER +-> INTEGER * STRING & k2 : INTEGER +-> INTEGER * STRING)"
+				+ " & (k = %(i).(i : NATURAL | (1,\"s\")) & k2 = k <+ {(22,( prj1(INTEGER,STRING)(k(22)),\"d\") )}) \n"
+				+ "END";
+		compare(expected, module);
+	}
 	
 	
 }

src/test/java/de/tla2b/typechecking/ExceptTest.java

@@ -122,7 +122,7 @@ public class ExceptTest {
 	}
 	
 	@Test
-	public void testRecordTest() throws Exception {
+	public void testRecordExcept() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
 				+ "EXTENDS Naturals \n"
 				+ "CONSTANTS k\n"
@@ -133,4 +133,18 @@ public class ExceptTest {
 		assertEquals("INTEGER", t.getConstantType("k"));
 	}
 	
+	@Test
+	public void testAtTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k, k2\n"
+				+ "ASSUME k  = [i \\in Nat |-> <<1, \"s\">>] /\\ k2 = [ k EXCEPT ![22] = <<@[1],\"d\">>] \n"
+				+ "=================================";
+
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("POW(INTEGER*(INTEGER*STRING))", t.getConstantType("k"));
+		assertEquals("POW(INTEGER*(INTEGER*STRING))", t.getConstantType("k2"));
+	}
+	
+
 }

src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java

@@ -105,5 +105,45 @@ public class MiscellaneousConstructsTest {
 		assertEquals("BOOL",t.getConstantType("k4"));
 	}
 	
+	@Test
+	public void testBoundedChoose() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = CHOOSE x \\in {1}: TRUE  \n"
+				+ "=================================";
+		TestTypeChecker t =TestUtil.typeCheckString(module);
+		assertEquals("INTEGER",t.getConstantType("k"));
+	}
+	
+	@Test
+	public void testUnboundedChoose() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = CHOOSE x : x = 1  \n"
+				+ "=================================";
+		TestTypeChecker t =TestUtil.typeCheckString(module);
+		assertEquals("INTEGER",t.getConstantType("k"));
+	}
+	
+	@Test
+	public void testUnboundedChooseTuple() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = CHOOSE <<a,b>> : <<a,b>> = <<1,TRUE>>  \n"
+				+ "=================================";
+		TestTypeChecker t =TestUtil.typeCheckString(module);
+		assertEquals("INTEGER*BOOL",t.getConstantType("k"));
+	}
+	
+	@Test
+	public void testBoundedChooseTuple() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = CHOOSE <<a,b>> \\in {<<1,TRUE>>}: TRUE  \n"
+				+ "=================================";
+		TestTypeChecker t =TestUtil.typeCheckString(module);
+		assertEquals("INTEGER*BOOL",t.getConstantType("k"));
+	}
+	
 	
 }

src/test/java/de/tla2b/typechecking/StructTest.java

@@ -6,7 +6,6 @@ package de.tla2b.typechecking;
 
 import static org.junit.Assert.assertEquals;
 
-import org.junit.Ignore;
 import org.junit.Test;
 
 import de.tla2b.exceptions.FrontEndException;