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

replace setType calls by setTypeAndFollowers

the behaviour of setType changed: is now without followers
parent 07fd0df4
No related branches found
No related tags found
No related merge requests found
Pipeline #148681 passed
...@@ -69,18 +69,18 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo ...@@ -69,18 +69,18 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
public void start() throws TLA2BException { public void start() throws TLA2BException {
for (OpDeclNode con : moduleNode.getConstantDecls()) { for (OpDeclNode con : moduleNode.getConstantDecls()) {
if (constantAssignments != null && constantAssignments.containsKey(con)) { if (constantAssignments != null && constantAssignments.containsKey(con)) {
setType(con, constantAssignments.get(con).getType()); setTypeAndFollowers(con, constantAssignments.get(con).getType());
} else { } else {
// if constant already has a type: keep type; otherwise add an untyped type // if constant already has a type: keep type; otherwise add an untyped type
if (con.getToolObject(TYPE_ID) == null) if (getType(con) == null)
setType(con, new UntypedType()); setTypeAndFollowers(con, new UntypedType());
} }
} }
for (OpDeclNode var : moduleNode.getVariableDecls()) { for (OpDeclNode var : moduleNode.getVariableDecls()) {
// if variable already has a type: keep type; otherwise add an untyped type // if variable already has a type: keep type; otherwise add an untyped type
if (var.getToolObject(TYPE_ID) == null) if (getType(var) == null)
setType(var, new UntypedType()); setTypeAndFollowers(var, new UntypedType());
} }
evalDefinitions(moduleNode.getOpDefs()); evalDefinitions(moduleNode.getOpDefs());
...@@ -175,13 +175,13 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo ...@@ -175,13 +175,13 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
throw new TLA2BFrontEndException(String.format("TLA2B do not support 2nd-order operators: '%s'%n %s ", throw new TLA2BFrontEndException(String.format("TLA2B do not support 2nd-order operators: '%s'%n %s ",
def.getName(), def.getLocation())); def.getName(), def.getLocation()));
} }
setType(p, new UntypedType(), paramId); setTypeAndFollowers(p, new UntypedType(), paramId);
} }
UntypedType u = new UntypedType(); UntypedType u = new UntypedType();
// TODO: check this // TODO: check this
// def.setToolObject(TYPE_ID, u); // def.setToolObject(TYPE_ID, u);
// u.addFollower(def); // u.addFollower(def);
setType(def, visitExprNode(def.getBody(), u)); setTypeAndFollowers(def, visitExprNode(def.getBody(), u));
} }
private void evalAssumptions(AssumeNode[] assumptions) throws TLA2BException { private void evalAssumptions(AssumeNode[] assumptions) throws TLA2BException {
...@@ -875,7 +875,7 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo ...@@ -875,7 +875,7 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
for (FormalParamNode param : n.getUnbdedQuantSymbols()) { for (FormalParamNode param : n.getUnbdedQuantSymbols()) {
TLAType paramType = new UntypedType(); TLAType paramType = new UntypedType();
symbolNodeList.add(param); symbolNodeList.add(param);
setType(param, paramType); setTypeAndFollowers(param, paramType);
list.add(paramType); list.add(paramType);
} }
TLAType found; TLAType found;
...@@ -884,17 +884,9 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo ...@@ -884,17 +884,9 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
} else { } else {
found = new TupleType(list); found = new TupleType(list);
} }
try { found = unifyAndSetTypeWithFollowers(found, expected, n.getOperator().getName().toString(), n);
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(
String.format("Expected %s, found %s at 'CHOOSE',%n%s", expected, found, n.getLocation()));
}
setType(n, found);
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance()); visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
return found;
return getType(n);
} }
case OPCODE_bc: { // CHOOSE x \in S: P case OPCODE_bc: { // CHOOSE x \in S: P
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment