From 7ce92491335fc43865ef736e6055edd6ff2a14b0 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 3 Jan 2025 12:23:52 +0100
Subject: [PATCH] add method for isBBuiltInOp check
---
.../java/de/tla2b/analysis/PredicateVsExpression.java | 5 +----
src/main/java/de/tla2b/analysis/TypeChecker.java | 10 +++-------
src/main/java/de/tla2b/global/BBuiltInOPs.java | 7 +++++++
.../de/tla2b/translation/UsedDefinitionsFinder.java | 6 +-----
src/main/java/de/tla2bAst/BAstCreator.java | 7 +++----
src/main/java/de/tla2bAst/ExpressionTranslator.java | 5 +----
6 files changed, 16 insertions(+), 24 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index 2e4c8fe..a6cf364 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -8,8 +8,6 @@ import tlc2.tool.BuiltInOPs;
import java.util.HashMap;
import java.util.Map;
-import static de.tla2b.global.TranslationGlobals.STANDARD_MODULES;
-
public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
private final Map<OpDefNode, DefinitionType> definitionsTypeMap = new HashMap<>();
@@ -80,8 +78,7 @@ public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
private DefinitionType visitUserdefinedOp(OpApplNode s) {
OpDefNode def = (OpDefNode) s.getOperator();
- if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
+ if (BBuiltInOPs.isBBuiltInOp(def)) {
switch (BBuiltInOPs.getOpcode(def.getName())) {
case B_OPCODE_lt: // <
case B_OPCODE_gt: // >
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index bae579c..8edc28d 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -156,12 +156,9 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
private void evalDefinitions(OpDefNode[] opDefs) throws TLA2BException {
for (OpDefNode def : opDefs) {
// Definition in this module
- String moduleName1 = def.getOriginallyDefinedInModuleNode().getName().toString();
- String moduleName2 = def.getSource().getOriginallyDefinedInModuleNode().getName().toString();
-
- if (STANDARD_MODULES.contains(moduleName1) || STANDARD_MODULES.contains(moduleName2)) {
+ String moduleName = def.getOriginallyDefinedInModuleNode().getName().toString();
+ if (STANDARD_MODULES.contains(moduleName) || BBuiltInOPs.isBBuiltInOp(def))
continue;
- }
if (usedDefinitions.contains(def) || bDefinitions.contains(def))
visitOpDefNode(def);
}
@@ -283,8 +280,7 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
OpDefNode def = (OpDefNode) n.getOperator();
// Definition is a BBuilt-in definition
- String sourceModule = def.getSource().getOriginallyDefinedInModuleNode().getName().toString();
- if (BBuiltInOPs.contains(def.getName()) && STANDARD_MODULES.contains(sourceModule)) {
+ if (BBuiltInOPs.isBBuiltInOp(def)) {
return evalBBuiltIns(n, expected);
}
diff --git a/src/main/java/de/tla2b/global/BBuiltInOPs.java b/src/main/java/de/tla2b/global/BBuiltInOPs.java
index 9d17f8e..60633b2 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -1,10 +1,13 @@
package de.tla2b.global;
+import tla2sany.semantic.OpDefNode;
import util.UniqueString;
import java.util.HashMap;
import java.util.Map;
+import static de.tla2b.global.TranslationGlobals.STANDARD_MODULES;
+
public class BBuiltInOPs implements BBuildIns {
private static final Map<UniqueString, Integer> B_Opcodes = new HashMap<>();
@@ -61,6 +64,10 @@ public class BBuiltInOPs implements BBuildIns {
return B_Opcodes.containsKey(s);
}
+ public static boolean isBBuiltInOp(OpDefNode def) {
+ return contains(def.getName()) && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString());
+ }
+
public static int getOpcode(UniqueString s) {
return B_Opcodes.get(s);
}
diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
index 67b06eb..a101349 100644
--- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
@@ -14,8 +14,6 @@ import java.util.Collection;
import java.util.HashSet;
import java.util.Set;
-import static de.tla2b.global.TranslationGlobals.STANDARD_MODULES;
-
public class UsedDefinitionsFinder extends AbstractASTVisitor {
private final Set<OpDefNode> usedDefinitions = new HashSet<>();
@@ -82,9 +80,7 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor {
OpDefNode def = (OpDefNode) n.getOperator();
ModuleNode moduleNode = def.getSource().getOriginallyDefinedInModuleNode();
- if (moduleNode.getName().toString().equals("TLA2B"))
- return;
- if (BBuiltInOPs.contains(def.getName()) && STANDARD_MODULES.contains(moduleNode.getName().toString()))
+ if (moduleNode.getName().toString().equals("TLA2B") || BBuiltInOPs.isBBuiltInOp(def))
return;
if (usedDefinitions.add(def)) {
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index e4bdced..89be2a9 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -626,8 +626,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
private PPredicate visitUserdefinedOpPredicate(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
- if (BBuiltInOPs.contains(def.getName()) // Operator is a B built-in operator
- && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
+ // Operator is a B built-in operator
+ if (BBuiltInOPs.isBBuiltInOp(def)) {
return visitBBuiltInsPredicate(n);
}
if (specAnalyser.getRecursiveFunctions().contains(def)) {
@@ -666,8 +666,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
private PExpression visitUserdefinedOpExpression(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
// Operator is a B built-in operator
- if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
+ if (BBuiltInOPs.isBBuiltInOp(def)) {
return visitBBuiltInsExpression(n);
}
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index c87b11c..89e8141 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -30,8 +30,6 @@ import java.io.IOException;
import java.util.*;
import java.util.stream.Collectors;
-import static de.tla2b.global.TranslationGlobals.STANDARD_MODULES;
-
public class ExpressionTranslator implements SyntaxTreeConstants {
private final String tlaExpression;
@@ -380,8 +378,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
// nCtx.addSymbolToContext(node.getName(), fromSpec);
// this should be redundant and not necessary:
// TypeChecker.setType(node, TypeChecker.getType(fromSpec));
- } else if (!(BBuiltInOPs.contains(node.getName())
- && STANDARD_MODULES.contains(node.getSource().getOriginallyDefinedInModuleNode().getName().toString()))) {
+ } else if (!BBuiltInOPs.isBBuiltInOp(node)) {
// throw error if def is not included in translation and not a built-in definition
throw new ExpressionTranslationException("Evaluation error:\n"
+ "Definition '" + fromSpec.getName() + "' is not included in the B translation.\n");
--
GitLab