From 1c64c81fef8c5f93e768d2d0211a81638fc6db0b Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Sat, 27 Apr 2024 09:51:20 +0200
Subject: [PATCH] =?UTF-8?q?don=E2=80=99t=20rewrite=20real=20division=20ope?=
=?UTF-8?q?ration=20into=20definition?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/main/java/de/tla2b/analysis/SymbolRenamer.java | 1 +
src/main/java/de/tla2b/analysis/TypeChecker.java | 13 +++++++++++++
src/main/java/de/tla2b/global/BBuildIns.java | 3 +++
src/main/java/de/tla2b/global/BBuiltInOPs.java | 1 +
src/main/java/de/tla2bAst/BAstCreator.java | 9 +++++++++
.../de/tla2b/expression/SimpleExpressionTest.java | 5 +++++
.../standardmodules/TestModuleReals.java | 11 +++++++++++
7 files changed, 43 insertions(+)
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index 49a2f80..56ed582 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -110,6 +110,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
BBUILTIN_OPERATOR.put("\\geq", "geq");
BBUILTIN_OPERATOR.put("%", "modulo");
BBUILTIN_OPERATOR.put("\\div", "div");
+ BBUILTIN_OPERATOR.put("/", "realdiv");
BBUILTIN_OPERATOR.put("..", "dot2");
}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index f51225d..3b48ec8 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -1229,6 +1229,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return type;
}
+ case B_OPCODE_realdiv: { // /
+ try {
+ RealType.getInstance().unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format("Expected %s, found REAL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
+ }
+ for (int i = 0; i < n.getArgs().length; i++) {
+ visitExprOrOpArgNode(n.getArgs()[i], RealType.getInstance());
+ }
+ return RealType.getInstance();
+ }
+
case B_OPCODE_dotdot: // ..
{
try {
diff --git a/src/main/java/de/tla2b/global/BBuildIns.java b/src/main/java/de/tla2b/global/BBuildIns.java
index af2ca6c..a36e425 100644
--- a/src/main/java/de/tla2b/global/BBuildIns.java
+++ b/src/main/java/de/tla2b/global/BBuildIns.java
@@ -12,6 +12,8 @@ public interface BBuildIns {
.uniqueStringOf("*");
UniqueString OP_div = UniqueString
.uniqueStringOf("\\div");
+ UniqueString OP_realdiv = UniqueString
+ .uniqueStringOf("/");
UniqueString OP_mod = UniqueString.uniqueStringOf("%");
UniqueString OP_exp = UniqueString.uniqueStringOf("^");
@@ -133,4 +135,5 @@ public interface BBuildIns {
int B_OPCODE_assert = B_OPCODE_rel_inverse + 1;
int B_OPCODE_real = B_OPCODE_assert + 1;
+ int B_OPCODE_realdiv = B_OPCODE_real + 1;
}
diff --git a/src/main/java/de/tla2b/global/BBuiltInOPs.java b/src/main/java/de/tla2b/global/BBuiltInOPs.java
index d1c1d33..3fdbfd3 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -13,6 +13,7 @@ public class BBuiltInOPs implements BBuildIns{
B_Opcode_Table.put(OP_minus, B_OPCODE_minus);
B_Opcode_Table.put(OP_times, B_OPCODE_times);
B_Opcode_Table.put(OP_div, B_OPCODE_div);
+ B_Opcode_Table.put(OP_realdiv, B_OPCODE_realdiv);
B_Opcode_Table.put(OP_mod, B_OPCODE_mod);
B_Opcode_Table.put(OP_exp, B_OPCODE_exp);
B_Opcode_Table.put(OP_uminus, B_OPCODE_uminus);
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index dfe0e4a..4031739 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -1020,6 +1020,15 @@ public class BAstCreator extends BuiltInOPs
returnNode = aFlooredDivExpression;
break;
+ case B_OPCODE_realdiv: // /
+ ADivExpression aDivExpression = new ADivExpression(
+ visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
+ visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
+
+ setPosition(aDivExpression, opApplNode);
+ returnNode = aDivExpression;
+ break;
+
case B_OPCODE_dotdot: // ..
returnNode = new AIntervalExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
index 7f45538..ac8f716 100644
--- a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
@@ -32,6 +32,11 @@ public class SimpleExpressionTest {
compareExpr("1.0 : REAL", "1.0 \\in Real");
}
+ @Test
+ public void testRealDivisionExpression() throws Exception {
+ compareExpr("1.0 / 2.0", "1.0 / 2.0");
+ }
+
@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/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
index f154d7e..7926e6a 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
@@ -133,6 +133,17 @@ public class TestModuleReals {
TestUtil.typeCheckString(module);
}
+ @Test
+ public void testRealDivision() throws TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Reals \n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = 1.0 / 1.0 \n"
+ + "=================================";
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("REAL", t.getConstantType("k"));
+ }
+
/*
* Interval operator: x .. y
*/
--
GitLab