Skip to content
Snippets Groups Projects
Commit 5eee515d authored by Jan Gruteser's avatar Jan Gruteser
Browse files

replace some tables

parent feba1821
Branches
Tags
No related merge requests found
Pipeline #148347 passed
...@@ -5,11 +5,12 @@ import de.tla2b.global.TranslationGlobals; ...@@ -5,11 +5,12 @@ import de.tla2b.global.TranslationGlobals;
import tla2sany.semantic.*; import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs; import tlc2.tool.BuiltInOPs;
import java.util.HashMap;
import java.util.HashSet; import java.util.HashSet;
import java.util.Hashtable; import java.util.Map;
import java.util.Set; import java.util.Set;
public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, ASTConstants { public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals {
private final static Set<String> KEYWORDS = new HashSet<>(); private final static Set<String> KEYWORDS = new HashSet<>();
...@@ -66,7 +67,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, AST ...@@ -66,7 +67,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, AST
KEYWORDS.add("OPERATIONS"); KEYWORDS.add("OPERATIONS");
} }
private final static Hashtable<String, String> INFIX_OPERATOR = new Hashtable<>(); private final static Map<String, String> INFIX_OPERATOR = new HashMap<>();
static { static {
INFIX_OPERATOR.put("!!", "exclamationmark2"); INFIX_OPERATOR.put("!!", "exclamationmark2");
...@@ -89,7 +90,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, AST ...@@ -89,7 +90,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, AST
INFIX_OPERATOR.put("...", "dot3"); INFIX_OPERATOR.put("...", "dot3");
} }
private final static Hashtable<String, String> BBUILTIN_OPERATOR = new Hashtable<>(); private final static Map<String, String> BBUILTIN_OPERATOR = new HashMap<>();
static { static {
BBUILTIN_OPERATOR.put("+", "plus"); BBUILTIN_OPERATOR.put("+", "plus");
...@@ -110,7 +111,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, AST ...@@ -110,7 +111,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, AST
private final Set<OpDefNode> usedDefinitions; private final Set<OpDefNode> usedDefinitions;
private final Set<String> globalNames = new HashSet<>(); private final Set<String> globalNames = new HashSet<>();
private final Hashtable<OpDefNode, Set<String>> usedNamesTable = new Hashtable<>(); private final Map<OpDefNode, Set<String>> usedNamesTable = new HashMap<>();
private SymbolRenamer(ModuleNode moduleNode, SpecAnalyser specAnalyser) { private SymbolRenamer(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode; this.moduleNode = moduleNode;
......
...@@ -6,62 +6,61 @@ import java.util.HashMap; ...@@ -6,62 +6,61 @@ import java.util.HashMap;
import java.util.Map; import java.util.Map;
public class BBuiltInOPs implements BBuildIns { public class BBuiltInOPs implements BBuildIns {
private static final Map<UniqueString, Integer> B_Opcode_Table; private static final Map<UniqueString, Integer> B_Opcodes = new HashMap<>();
static { static {
B_Opcode_Table = new HashMap<>(); B_Opcodes.put(OP_dotdot, B_OPCODE_dotdot);
B_Opcode_Table.put(OP_dotdot, B_OPCODE_dotdot); B_Opcodes.put(OP_plus, B_OPCODE_plus);
B_Opcode_Table.put(OP_plus, B_OPCODE_plus); B_Opcodes.put(OP_minus, B_OPCODE_minus);
B_Opcode_Table.put(OP_minus, B_OPCODE_minus); B_Opcodes.put(OP_times, B_OPCODE_times);
B_Opcode_Table.put(OP_times, B_OPCODE_times); B_Opcodes.put(OP_div, B_OPCODE_div);
B_Opcode_Table.put(OP_div, B_OPCODE_div); B_Opcodes.put(OP_realdiv, B_OPCODE_realdiv);
B_Opcode_Table.put(OP_realdiv, B_OPCODE_realdiv); B_Opcodes.put(OP_mod, B_OPCODE_mod);
B_Opcode_Table.put(OP_mod, B_OPCODE_mod); B_Opcodes.put(OP_exp, B_OPCODE_exp);
B_Opcode_Table.put(OP_exp, B_OPCODE_exp); B_Opcodes.put(OP_uminus, B_OPCODE_uminus);
B_Opcode_Table.put(OP_uminus, B_OPCODE_uminus);
B_Opcode_Table.put(OP_lt, B_OPCODE_lt); B_Opcodes.put(OP_lt, B_OPCODE_lt);
B_Opcode_Table.put(OP_leq, B_OPCODE_leq); B_Opcodes.put(OP_leq, B_OPCODE_leq);
B_Opcode_Table.put(OP_gt, B_OPCODE_gt); B_Opcodes.put(OP_gt, B_OPCODE_gt);
B_Opcode_Table.put(OP_geq, B_OPCODE_geq); B_Opcodes.put(OP_geq, B_OPCODE_geq);
B_Opcode_Table.put(OP_bool, B_OPCODE_bool); B_Opcodes.put(OP_bool, B_OPCODE_bool);
B_Opcode_Table.put(OP_true, B_OPCODE_true); B_Opcodes.put(OP_true, B_OPCODE_true);
B_Opcode_Table.put(OP_false, B_OPCODE_false); B_Opcodes.put(OP_false, B_OPCODE_false);
B_Opcode_Table.put(OP_nat, B_OPCODE_nat); B_Opcodes.put(OP_nat, B_OPCODE_nat);
B_Opcode_Table.put(OP_int, B_OPCODE_int); B_Opcodes.put(OP_int, B_OPCODE_int);
B_Opcode_Table.put(OP_real, B_OPCODE_real); B_Opcodes.put(OP_real, B_OPCODE_real);
B_Opcode_Table.put(OP_string, B_OPCODE_string); B_Opcodes.put(OP_string, B_OPCODE_string);
B_Opcode_Table.put(OP_finite, B_OPCODE_finite); B_Opcodes.put(OP_finite, B_OPCODE_finite);
B_Opcode_Table.put(OP_card, B_OPCODE_card); B_Opcodes.put(OP_card, B_OPCODE_card);
B_Opcode_Table.put(OP_len, B_OPCODE_len); B_Opcodes.put(OP_len, B_OPCODE_len);
B_Opcode_Table.put(OP_append, B_OPCODE_append); B_Opcodes.put(OP_append, B_OPCODE_append);
B_Opcode_Table.put(OP_seq, B_OPCODE_seq); B_Opcodes.put(OP_seq, B_OPCODE_seq);
B_Opcode_Table.put(OP_head, B_OPCODE_head); B_Opcodes.put(OP_head, B_OPCODE_head);
B_Opcode_Table.put(OP_tail, B_OPCODE_tail); B_Opcodes.put(OP_tail, B_OPCODE_tail);
B_Opcode_Table.put(OP_subseq, B_OPCODE_subseq); B_Opcodes.put(OP_subseq, B_OPCODE_subseq);
B_Opcode_Table.put(OP_conc, B_OPCODE_conc); B_Opcodes.put(OP_conc, B_OPCODE_conc);
B_Opcode_Table.put(OP_min, B_OPCODE_min); B_Opcodes.put(OP_min, B_OPCODE_min);
B_Opcode_Table.put(OP_max, B_OPCODE_max); B_Opcodes.put(OP_max, B_OPCODE_max);
B_Opcode_Table.put(OP_setprod, B_OPCODE_setprod); B_Opcodes.put(OP_setprod, B_OPCODE_setprod);
B_Opcode_Table.put(OP_setsum, B_OPCODE_setsum); B_Opcodes.put(OP_setsum, B_OPCODE_setsum);
B_Opcode_Table.put(OP_permseq, B_OPCODE_permseq); B_Opcodes.put(OP_permseq, B_OPCODE_permseq);
B_Opcode_Table.put(OP_pow1, B_OPCODE_pow1); B_Opcodes.put(OP_pow1, B_OPCODE_pow1);
//relations //relations
B_Opcode_Table.put(OP_rel_inverse, B_OPCODE_rel_inverse); B_Opcodes.put(OP_rel_inverse, B_OPCODE_rel_inverse);
B_Opcode_Table.put(OP_assert, B_OPCODE_assert); B_Opcodes.put(OP_assert, B_OPCODE_assert);
} }
public static boolean contains(UniqueString s) { public static boolean contains(UniqueString s) {
return B_Opcode_Table.containsKey(s); return B_Opcodes.containsKey(s);
} }
public static int getOpcode(UniqueString s) { public static int getOpcode(UniqueString s) {
return B_Opcode_Table.get(s); return B_Opcodes.get(s);
} }
} }
...@@ -12,7 +12,7 @@ import java.util.HashSet; ...@@ -12,7 +12,7 @@ import java.util.HashSet;
import java.util.Set; import java.util.Set;
public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals { public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<>(); private final Set<OpDefNode> bDefinitionsSet = new HashSet<>();
public BDefinitionsFinder(SpecAnalyser specAnalyser) { public BDefinitionsFinder(SpecAnalyser specAnalyser) {
if (specAnalyser.getConfigFileEvaluator() != null) { if (specAnalyser.getConfigFileEvaluator() != null) {
...@@ -50,7 +50,7 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstan ...@@ -50,7 +50,7 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstan
} }
} }
HashSet<OpDefNode> temp = new HashSet<>(bDefinitionsSet); Set<OpDefNode> temp = new HashSet<>(bDefinitionsSet);
for (OpDefNode opDefNode : temp) { for (OpDefNode opDefNode : temp) {
visitExprNode(opDefNode.getBody()); visitExprNode(opDefNode.getBody());
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment