From c025f321f0e50fbcc0a81b4c34e5c5452f5c4b98 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 20 Dec 2024 11:59:36 +0100
Subject: [PATCH] improve computation of the value of numeral and decimal nodes

---
 src/main/java/de/tla2bAst/BAstCreator.java | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index cf868dc..796454b 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -523,11 +523,15 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
 			case OpApplKind:
 				return visitOpApplNodeExpression((OpApplNode) exprNode);
 			case NumeralKind: {
-				String number = String.valueOf(((NumeralNode) exprNode).val());
+				NumeralNode node = (NumeralNode) exprNode;
+				String number = String.valueOf(node.useVal() ? node.val() : node.bigVal());
 				return createPositionedNode(new AIntegerExpression(new TIntegerLiteral(number)), exprNode);
 			}
 			case DecimalKind: {
-				return createPositionedNode(new ARealExpression(new TRealLiteral(exprNode.toString())), exprNode);
+				DecimalNode node = (DecimalNode) exprNode;
+				String number = String.valueOf(node.bigVal() == null ? node.mantissa() * Math.pow(10,node.exponent()) : node.bigVal());
+				// the image of BigDecimal should always be with .0, because the node would not have been of DecimalKind otherwise
+				return createPositionedNode(new ARealExpression(new TRealLiteral(number)), exprNode);
 			}
 			case StringKind: {
 				StringNode s = (StringNode) exprNode;
-- 
GitLab