add some tests for reals

src/test/java/de/tla2b/expression/SimpleExpressionTest.java

 package de.tla2b.expression;
 
+import org.junit.Ignore;
 import org.junit.Test;
 
 import static de.tla2b.util.TestUtil.compareExpr;
@@ -26,6 +27,13 @@ public class SimpleExpressionTest {
 		compareExpr("-1 : INTEGER", "-1 \\in Int");
 	}
 
+	// FIXME: real_set(none) vs identifier(none,'Real')
+	@Ignore
+	@Test
+	public void testModulReals() throws Exception {
+		compareExpr("1 : REAL", "1 \\in Real");
+	}
+
 	@Test
 	public void testExist() throws Exception {
 		compareExpr("#a.(a : {1} & 2 > 1)", "\\E a \\in {1}: 2 > 1");

src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java

@@ -27,7 +27,7 @@ public class TestModuleNaturals {
 		TestTypeChecker t = TestUtil.typeCheckString(module);
 		assertEquals("BOOL", t.getConstantType("k"));
 		assertEquals("INTEGER", t.getConstantType("k2"));
-		assertEquals("INTEGER", t.getConstantType("k2"));
+		assertEquals("INTEGER", t.getConstantType("k3"));
 	}
 
 	@Test(expected = TypeErrorException.class)

src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java

+package de.tla2b.typechecking.standardmodules;
+
+import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.exceptions.TypeErrorException;
+import de.tla2b.util.TestTypeChecker;
+import de.tla2b.util.TestUtil;
+import org.junit.Ignore;
+import org.junit.Test;
+
+import static org.junit.Assert.assertEquals;
+
+
+public class TestModuleReals {
+
+	/*
+	 * Real
+	 */
+	@Test
+	public void unifyReal() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Reals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = Real \n" + "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("POW(REAL)", t.getConstantType("k"));
+	}
+
+	@Test(expected = TypeErrorException.class)
+	public void unifyErrorReal() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Reals \n"
+				+ "ASSUME TRUE \\in Real \n"
+				+ "=================================";
+
+		TestUtil.typeCheckString(module);
+	}
+
+	// FIXME: support:
+	@Ignore
+	/*
+	 * unary minus: -x
+	 */
+	@Test
+	public void unifyUnaryMinusReal() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Reals \n"
+				+ "CONSTANTS k, k2 \n"
+				+ "ASSUME k = -k2 \n" + "=================================";
+
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("REAL", t.getConstantType("k"));
+		assertEquals("REAL", t.getConstantType("k2"));
+	}
+
+	@Test(expected = TypeErrorException.class)
+	public void unifyErrorUnaryMinusReal() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Reals \n"
+				+ "ASSUME TRUE = -1.0 \n"
+				+ "=================================";
+		TestUtil.typeCheckString(module);
+	}
+
+	@Test(expected = TypeErrorException.class)
+	public void testRelationalOperatorsException1() throws
+		TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Reals \n"
+			+ "CONSTANTS k, k2 \n"
+			+ "ASSUME 1.0 = (2 > 1) \n" + "=================================";
+		TestUtil.typeCheckString(module);
+	}
+
+	@Test(expected = TypeErrorException.class)
+	public void testRelationalOperatorsException2() throws
+		TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Reals \n"
+			+ "CONSTANTS k, k2 \n"
+			+ "ASSUME 1.0 = (2.0 > 1) \n" + "=================================";
+		TestUtil.typeCheckString(module);
+	}
+
+	@Test(expected = TypeErrorException.class)
+	public void testRelationalOperatorsException3() throws
+		TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Reals \n"
+			+ "CONSTANTS k, k2 \n"
+			+ "ASSUME 1.0 = (2.0 > 1.0) \n" + "=================================";
+		TestUtil.typeCheckString(module);
+	}
+
+	@Test
+	public void testArithmeticOperators() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Naturals \n"
+			+ "ASSUME 2.0 = 1.0 + 1.0 \n"
+			+ "=================================";
+		TestUtil.typeCheckString(module);
+	}
+
+	@Test(expected = TypeErrorException.class)
+	public void testArithmeticOperatorsException1() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Naturals \n"
+			+ "ASSUME TRUE = 1.0 + 1.0 \n"
+			+ "=================================";
+		TestUtil.typeCheckString(module);
+	}
+
+	@Test(expected = TypeErrorException.class)
+	public void testArithmeticOperatorsException2() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Naturals \n"
+			+ "ASSUME 2.0 = 1.0 + 1 \n"
+			+ "=================================";
+		TestUtil.typeCheckString(module);
+	}
+
+	@Test(expected = TypeErrorException.class)
+	public void testArithmeticOperatorsException3() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Naturals \n"
+			+ "ASSUME 2 = 1.0 + 1.0 \n"
+			+ "=================================";
+		TestUtil.typeCheckString(module);
+	}
+
+	/*
+	 * Interval operator: x .. y
+	 */
+
+	@Test(expected = TypeErrorException.class)
+	public void testDotDotReal() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Naturals \n"
+			+ "CONSTANTS k \n"
+			+ "ASSUME k = 1.0 .. 3.0 \n"
+			+ "=================================";
+		TestUtil.typeCheckString(module);
+	}
+}