From 9af8cc0af9f9812c852d6fecf72ff3f5b9e304c3 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 3 Jan 2025 10:42:01 +0100
Subject: [PATCH] minor simplifications
---
.../translation/RecursiveFunctionHandler.java | 39 +++++++------------
src/main/java/de/tla2bAst/BAstCreator.java | 9 ++---
2 files changed, 18 insertions(+), 30 deletions(-)
diff --git a/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
index d659417..10b80b0 100644
--- a/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
+++ b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
@@ -4,19 +4,16 @@ import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.SpecAnalyser;
import tla2sany.semantic.*;
-import java.util.ArrayList;
-import java.util.Collections;
-import java.util.HashSet;
-import java.util.Hashtable;
+import java.util.*;
public class RecursiveFunctionHandler extends AbstractASTVisitor {
- private ArrayList<FormalParamNode> paramList;
- private ArrayList<FormalParamNode> ignoreParamList;
- private ArrayList<SymbolNode> externParams;
+ private List<FormalParamNode> paramList;
+ private List<FormalParamNode> ignoreParamList;
+ private List<SymbolNode> externParams;
- private final HashSet<OpApplNode> recursiveFunctions = new HashSet<>();
- private final Hashtable<SemanticNode, ArrayList<SymbolNode>> additionalParamsTable = new Hashtable<>();
+ private final Set<OpApplNode> recursiveFunctions = new HashSet<>();
+ private final Map<SemanticNode, List<SymbolNode>> additionalParamsTable = new HashMap<>();
public RecursiveFunctionHandler(SpecAnalyser specAnalyser) {
for (OpDefNode recFunc : specAnalyser.getRecursiveFunctions()) {
@@ -51,7 +48,7 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
externParams.add(n.getOperator());
}
- public ArrayList<SymbolNode> getAdditionalParams(SemanticNode n) {
+ public List<SymbolNode> getAdditionalParams(SemanticNode n) {
return additionalParamsTable.get(n);
}
@@ -69,30 +66,22 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
case OPCODE_bf: // \A x \in S : P
case OPCODE_bc: // CHOOSE x \in S: P
case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
- case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
- {
- FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- HashSet<FormalParamNode> set = new HashSet<>();
- for (FormalParamNode[] param : params) {
+ case OPCODE_soa: { // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
+ Set<FormalParamNode> set = new HashSet<>();
+ for (FormalParamNode[] param : n.getBdedQuantSymbolLists()) {
Collections.addAll(set, param);
}
ignoreParamList.addAll(set);
- ExprNode[] in = n.getBdedQuantBounds();
- for (ExprNode exprNode : in) {
+ for (ExprNode exprNode : n.getBdedQuantBounds()) { // in
visitExprNode(exprNode);
}
- ExprOrOpArgNode[] arguments = n.getArgs();
- for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
- visitExprOrOpArgNode(exprOrOpArgNode);
+ for (ExprOrOpArgNode argument : n.getArgs()) {
+ visitExprOrOpArgNode(argument);
}
return;
}
- default: {
+ default:
super.visitBuiltInNode(n);
- }
-
}
-
}
-
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index ef40219..e4bdced 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -672,11 +672,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
}
if (specAnalyser.getRecursiveFunctions().contains(def)) {
- ArrayList<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(def);
+ List<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(def);
if (!list.isEmpty()) {
AFunctionExpression call = new AFunctionExpression();
call.setIdentifier(createIdentifierNode(def));
- ArrayList<PExpression> params = new ArrayList<>();
+ List<PExpression> params = new ArrayList<>();
for (SymbolNode symbolNode : list) {
params.add(createIdentifierNode(symbolNode));
}
@@ -1241,11 +1241,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
lambda.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
if (recursiveFunctionHandler.isRecursiveFunction(n)) {
-
- ArrayList<SymbolNode> externParams = recursiveFunctionHandler.getAdditionalParams(n);
+ List<SymbolNode> externParams = recursiveFunctionHandler.getAdditionalParams(n);
if (!externParams.isEmpty()) {
ALambdaExpression lambda2 = new ALambdaExpression();
- ArrayList<PExpression> shiftedParams = new ArrayList<>();
+ List<PExpression> shiftedParams = new ArrayList<>();
List<PPredicate> predList2 = new ArrayList<>();
for (SymbolNode p : externParams) {
shiftedParams.add(createIdentifierNode(p));
--
GitLab