From 16150aa7d0c9bc12954b5139d53c7bb485e1fa06 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Mon, 13 Jan 2025 09:56:08 +0100
Subject: [PATCH] add ignored test for nested Real definitions
---
.../standardmodules/TestModuleNaturals.java | 13 +++++++++++++
.../standardmodules/TestModuleReals.java | 17 ++++++++++++++++-
2 files changed, 29 insertions(+), 1 deletion(-)
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
index 6fa6a8b..0d134ea 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
@@ -115,4 +115,17 @@ public class TestModuleNaturals {
TestUtil.typeCheckString(module);
}
+ @Test
+ public void testNestedDefinitions() throws Exception {
+ String module = "---- MODULE Testing ----\n"
+ + "EXTENDS Naturals \n"
+ + "InnerDef(b) == b*5 \n"
+ + "HelpDef(a,b) == a+b \n"
+ + "Init == 1 = HelpDef(1,1) \n"
+ + "===============";
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("INTEGER", t.getDefinitionType("HelpDef"));
+ assertEquals("INTEGER", t.getDefinitionType("InnerDef"));
+ }
+
}
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
index 4ba3f0e..8b4cf34 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
@@ -4,11 +4,11 @@ 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 {
/*
@@ -172,4 +172,19 @@ public class TestModuleReals {
+ "=================================";
TestUtil.typeCheckString(module);
}
+
+ @Ignore
+ @Test
+ public void testNestedDefinitions() throws Exception {
+ // FIXME: this fails because the default type is Int and we first type everything as Int
+ String module = "---- MODULE Testing ----\n"
+ + "EXTENDS Reals \n"
+ + "InnerDef(b) == b*5.0 \n"
+ + "HelpDef(a,b) == a+InnerDef(b) \n"
+ + "Init == 1.0 = HelpDef(1.0,1.0) \n"
+ + "===============";
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("REAL", t.getDefinitionType("HelpDef"));
+ assertEquals("REAL", t.getDefinitionType("InnerDef"));
+ }
}
--
GitLab