From 6ad55775ec721383ce5f6e24716126a1d4727580 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 3 Jan 2025 12:39:15 +0100
Subject: [PATCH] minor simplifications
---
src/main/java/de/tla2b/analysis/PredicateVsExpression.java | 4 ----
src/main/java/de/tla2b/analysis/SymbolRenamer.java | 7 ++++---
src/main/java/de/tla2b/analysis/TypeChecker.java | 4 ++--
src/main/java/de/tla2b/config/TLCValueNode.java | 3 +--
4 files changed, 7 insertions(+), 11 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index a6cf364..ea0c647 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -65,10 +65,6 @@ public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
OpApplNode pair = (OpApplNode) opApplNode.getArgs()[0];
return visitSemanticNode(pair.getArgs()[1]);
}
-
- default: {
- return DefinitionType.EXPRESSION;
- }
}
} else if (kind == UserDefinedOpKind) {
return visitUserdefinedOp(opApplNode);
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index 92bd5ce..bb42ae8 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -1,7 +1,6 @@
package de.tla2b.analysis;
import de.tla2b.global.BBuiltInOPs;
-import de.tla2b.global.TranslationGlobals;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
@@ -10,7 +9,9 @@ import java.util.HashSet;
import java.util.Map;
import java.util.Set;
-public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals {
+import static de.tla2b.global.TranslationGlobals.NEW_NAME;
+
+public class SymbolRenamer extends BuiltInOPs {
private final static Set<String> KEYWORDS = new HashSet<>();
@@ -286,7 +287,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals {
if (BBUILTIN_OPERATOR.containsKey(newName)) {
// a B built-in operator is defined outside a standard module
- if (!STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
+ if (!BBuiltInOPs.isBBuiltInOp(def)) {
return incName(BBUILTIN_OPERATOR.get(newName));
}
}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 8edc28d..010a1ca 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -89,8 +89,8 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
if (!bConstList.contains(con))
continue;
- TLAType defType = (TLAType) entry.getValue().getToolObject(TYPE_ID);
- TLAType conType = (TLAType) con.getToolObject(TYPE_ID);
+ TLAType defType = getType(entry.getValue());
+ TLAType conType = getType(con);
try {
setType(con, defType.unify(conType));
} catch (UnificationException e) {
diff --git a/src/main/java/de/tla2b/config/TLCValueNode.java b/src/main/java/de/tla2b/config/TLCValueNode.java
index 3a5515c..5be9018 100644
--- a/src/main/java/de/tla2b/config/TLCValueNode.java
+++ b/src/main/java/de/tla2b/config/TLCValueNode.java
@@ -1,13 +1,12 @@
package de.tla2b.config;
-import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.TLAType;
import tla2sany.semantic.AbortException;
import tla2sany.semantic.NumeralNode;
import tla2sany.st.TreeNode;
import tlc2.value.impl.Value;
-public class TLCValueNode extends NumeralNode implements TranslationGlobals {
+public class TLCValueNode extends NumeralNode {
private final Value value;
private final TLAType type;
--
GitLab