From d62656caad11dec43f34f51cdef52e55b95285bd Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Thu, 2 Jan 2025 10:28:33 +0100
Subject: [PATCH] add Infinity definition from Reals module
---
src/main/java/de/tla2b/global/BBuildIns.java | 2 ++
src/main/java/de/tla2b/global/BBuiltInOPs.java | 1 +
2 files changed, 3 insertions(+)
diff --git a/src/main/java/de/tla2b/global/BBuildIns.java b/src/main/java/de/tla2b/global/BBuildIns.java
index bce2f60..970ee03 100644
--- a/src/main/java/de/tla2b/global/BBuildIns.java
+++ b/src/main/java/de/tla2b/global/BBuildIns.java
@@ -18,6 +18,7 @@ public interface BBuildIns extends ToolGlobals {
UniqueString OP_nat = UniqueString.uniqueStringOf("Nat");
UniqueString OP_int = UniqueString.uniqueStringOf("Int");
UniqueString OP_real = UniqueString.uniqueStringOf("Real");
+ UniqueString OP_infinity = UniqueString.uniqueStringOf("Infinity");
UniqueString OP_bool = UniqueString.uniqueStringOf("BOOLEAN");
UniqueString OP_true = UniqueString.uniqueStringOf("TRUE");
UniqueString OP_false = UniqueString.uniqueStringOf("FALSE");
@@ -98,4 +99,5 @@ public interface BBuildIns extends ToolGlobals {
int B_OPCODE_real = B_OPCODE_assert + 1;
int B_OPCODE_realdiv = B_OPCODE_assert + 2;
+ int B_OPCODE_infinity = B_OPCODE_assert + 3;
}
diff --git a/src/main/java/de/tla2b/global/BBuiltInOPs.java b/src/main/java/de/tla2b/global/BBuiltInOPs.java
index 163e30f..9d17f8e 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -29,6 +29,7 @@ public class BBuiltInOPs implements BBuildIns {
B_Opcodes.put(OP_nat, B_OPCODE_nat);
B_Opcodes.put(OP_int, B_OPCODE_int);
B_Opcodes.put(OP_real, B_OPCODE_real);
+ B_Opcodes.put(OP_infinity, B_OPCODE_infinity);
B_Opcodes.put(OP_string, B_OPCODE_string);
B_Opcodes.put(OP_finite, B_OPCODE_finite);
--
GitLab