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

simplify TestTypeChecker

parent f8da3be6
Branches
Tags
No related merge requests found
......@@ -4,83 +4,72 @@ import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.TLAType;
import de.tla2bAst.Translator;
import tla2sany.semantic.*;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SemanticNode;
import java.util.Hashtable;
import java.util.HashMap;
import java.util.Map;
public class TestTypeChecker implements TranslationGlobals {
public final int toolId = 5;
private final Hashtable<String, TLAType> constants;
private final Hashtable<String, TLAType> variables;
private final Hashtable<String, DefCon> definitions;
private final Map<String, TLAType> constants = new HashMap<>();
private final Map<String, TLAType> variables = new HashMap<>();
private final Map<String, TLAType> definitionTypes = new HashMap<>();
private final Map<String, Map<String, TLAType>> definitionParamTypes = new HashMap<>();
public ModuleNode moduleNode;
public TestTypeChecker() {
constants = new Hashtable<>();
variables = new Hashtable<>();
definitions = new Hashtable<>();
}
public void startTest(String moduleString, String configString)
throws TLA2BException {
public void startTest(String moduleString, String configString) throws TLA2BException {
Translator translator = new Translator(moduleString, configString);
translator.translate();
moduleNode = translator.getModuleNode();
init();
}
public void start(String moduleFileName)
throws TLA2BException {
public void start(String moduleFileName) throws TLA2BException {
Translator translator = new Translator(moduleFileName);
translator.translate();
moduleNode = translator.getModuleNode();
init();
}
private TLAType getBType(SemanticNode node) {
TLAType type = (TLAType) node.getToolObject(toolId);
return type;
return (TLAType) node.getToolObject(toolId);
}
private void init() {
for (int i = 0; i < moduleNode.getConstantDecls().length; i++) {
OpDeclNode con = moduleNode.getConstantDecls()[i];
constants.put(con.getName().toString(),
getBType(con));
constants.put(con.getName().toString(), getBType(con));
}
for (int i = 0; i < moduleNode.getVariableDecls().length; i++) {
OpDeclNode var = moduleNode.getVariableDecls()[i];
variables.put(var.getName().toString(),
getBType(var));
variables.put(var.getName().toString(), getBType(var));
}
for (int i = 0; i < moduleNode.getOpDefs().length; i++) {
OpDefNode def = moduleNode.getOpDefs()[i];
DefCon defCon = new DefCon(getBType(def));
if (defCon.getType() == null)
continue;
if (STANDARD_MODULES.contains(def
.getOriginallyDefinedInModuleNode().getName().toString())
|| STANDARD_MODULES.contains(def.getSource()
.getOriginallyDefinedInModuleNode().getName()
.toString())) {
TLAType defType = getBType(def);
if (defType == null
|| STANDARD_MODULES.contains(def.getOriginallyDefinedInModuleNode().getName().toString())
|| STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
continue;
}
Map<String, TLAType> params = new HashMap<>();
for (int j = 0; j < def.getParams().length; j++) {
FormalParamNode p = def.getParams()[j];
defCon.parameters.put(p.getName().toString(),
getBType(p));
params.put(p.getName().toString(), getBType(p));
}
definitions.put(def.getName().toString(), defCon);
definitionTypes.put(def.getName().toString(), defType);
definitionParamTypes.put(def.getName().toString(), params);
}
}
public String getConstantType(String conName) {
return constants.get(conName).toString();
}
......@@ -90,32 +79,10 @@ public class TestTypeChecker implements TranslationGlobals {
}
public String getDefinitionType(String defName) {
return definitions.get(defName).getType().toString();
return definitionTypes.get(defName).toString();
}
public String getDefinitionParamType(String defName, String paramName) {
return definitions.get(defName).getParams().get(paramName).toString();
}
public static class DefCon {
private final Hashtable<String, TLAType> parameters;
private TLAType type;
private DefCon(TLAType t) {
parameters = new Hashtable<>();
type = t;
}
public Hashtable<String, TLAType> getParams() {
return parameters;
}
public TLAType getType() {
return type;
}
public void setType(TLAType type) {
this.type = type;
}
return definitionParamTypes.get(defName).get(paramName).toString();
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment