From ad0a223af4b720e3c416009ea3b6bc4c6eafc596 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 26 Apr 2024 19:19:41 +0200
Subject: [PATCH] add some tests for reals

---
 .../expression/SimpleExpressionTest.java      |   8 +
 .../standardmodules/TestModuleNaturals.java   |   2 +-
 .../standardmodules/TestModuleReals.java      | 143 ++++++++++++++++++
 3 files changed, 152 insertions(+), 1 deletion(-)
 create mode 100644 src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java

diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
index 391b8cd..91b392a 100644
--- a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
@@ -1,5 +1,6 @@
 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");
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
index 505bb32..7269878 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
+++ b/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)
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
new file mode 100644
index 0000000..928def9
--- /dev/null
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
@@ -0,0 +1,143 @@
+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);
+	}
+}
-- 
GitLab