From a1f570aa456310be5cc41ef9a7a420fced070463 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Sat, 27 Apr 2024 07:31:04 +0200
Subject: [PATCH] support unary minus for reals
also needs to be simplified
---
.../java/de/tla2b/analysis/TypeChecker.java | 35 ++++++++++++++++---
.../standardmodules/TestModuleReals.java | 16 ++++++---
2 files changed, 41 insertions(+), 10 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 582bd30..f51225d 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -1285,14 +1285,39 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
case B_OPCODE_uminus: // -x
{
- try {
+ // TODO: simplify
+ TLAType type;
+ if (expected instanceof RealType) {
+ try {
+ RealType.getInstance().unify(expected);
+ type = RealType.getInstance();
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
+ String.format("Expected %s, found REAL at '-',%n%s", expected, n.getLocation()));
+ }
+ } else if (expected instanceof IntType) {
+ try {
+ IntType.getInstance().unify(expected);
+ type = IntType.getInstance();
+ } catch (UnificationException e) {
+ throw new TypeErrorException(
+ String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation()));
+ }
+ } else if (expected instanceof UntypedType) {
IntType.getInstance().unify(expected);
- } catch (UnificationException e) {
+ type = IntType.getInstance();
+ try {
+ visitExprOrOpArgNode(n.getArgs()[0], type);
+ } catch (TypeErrorException e) {
+ RealType.getInstance().unify(expected);
+ type = RealType.getInstance();
+ }
+ } else {
throw new TypeErrorException(
- String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation()));
+ String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation()));
}
- visitExprOrOpArgNode(n.getArgs()[0], IntType.getInstance());
- return IntType.getInstance();
+ visitExprOrOpArgNode(n.getArgs()[0], type);
+ return type;
}
/*
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
index 928def9..f154d7e 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
@@ -35,8 +35,6 @@ public class TestModuleReals {
TestUtil.typeCheckString(module);
}
- // FIXME: support:
- @Ignore
/*
* unary minus: -x
*/
@@ -44,12 +42,20 @@ public class TestModuleReals {
public void unifyUnaryMinusReal() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Reals \n"
- + "CONSTANTS k, k2 \n"
- + "ASSUME k = -k2 \n" + "=================================";
+ + "CONSTANTS k \n"
+ + "ASSUME k = -1.0 \n" + "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
assertEquals("REAL", t.getConstantType("k"));
- assertEquals("REAL", t.getConstantType("k2"));
+ }
+
+ @Test(expected = TypeErrorException.class)
+ public void unifyUnaryMinusRealError() throws TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Reals \n"
+ + "ASSUME -1 = -1.0 \n" + "=================================";
+
+ TestTypeChecker t = TestUtil.typeCheckString(module);
}
@Test(expected = TypeErrorException.class)
--
GitLab