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

replace unifications and setType in evalExcept

parent a459e590
No related branches found
No related tags found
No related merge requests found
...@@ -790,63 +790,40 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo ...@@ -790,63 +790,40 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
private TLAType evalExcept(OpApplNode n, TLAType expected) throws TLA2BException { private TLAType evalExcept(OpApplNode n, TLAType expected) throws TLA2BException {
TLAType t = visitExprOrOpArgNode(n.getArgs()[0], expected); TLAType t = visitExprOrOpArgNode(n.getArgs()[0], expected);
n.setToolObject(TYPE_ID, t); setTypeAndFollowers(n, t);
if (t instanceof AbstractHasFollowers) {
((AbstractHasFollowers) t).addFollower(n);
}
for (int i = 1; i < n.getArgs().length; i++) { for (int i = 1; i < n.getArgs().length; i++) { // start at 1
OpApplNode pair = (OpApplNode) n.getArgs()[i]; OpApplNode pair = (OpApplNode) n.getArgs()[i];
ExprOrOpArgNode leftside = pair.getArgs()[0];
ExprOrOpArgNode rightside = pair.getArgs()[1];
// stored for @ node // stored for @ node
UntypedType untyped = new UntypedType(); UntypedType untyped = new UntypedType();
rightside.setToolObject(TYPE_ID, untyped); setTypeAndFollowers(pair.getArgs()[1], untyped);
untyped.addFollower(rightside); TLAType valueType = visitExprOrOpArgNode(pair.getArgs()[1], untyped); // right side
TLAType valueType = visitExprOrOpArgNode(rightside, untyped);
OpApplNode seq = (OpApplNode) leftside; OpApplNode seq = (OpApplNode) pair.getArgs()[0]; // left side
LinkedList<ExprOrOpArgNode> list = new LinkedList<>(); LinkedList<ExprOrOpArgNode> list = new LinkedList<>(Arrays.asList(seq.getArgs()));
Collections.addAll(list, seq.getArgs()); ExprOrOpArgNode domExpr = list.poll();
ExprOrOpArgNode first = list.poll();
if (first instanceof StringNode) { if (domExpr instanceof StringNode) {
String field = ((StringNode) first).getRep().toString(); String field = ((StringNode) domExpr).getRep().toString();
TLAType res = evalType(list, valueType); TLAType res = evalType(list, valueType);
StructOrFunctionType s = new StructOrFunctionType(field, res); t = unify(t, new StructOrFunctionType(field, res), pair);
try {
t = t.unify(s);
} catch (UnificationException e) {
throw new TypeErrorException(
String.format("Expected %s, found %s at 'EXCEPT',%n%s", t, s, pair.getLocation()));
}
} else { } else {
// Function // Function
ExprOrOpArgNode domExpr = first;
TLAType domType; TLAType domType;
TLAType rangeType;
if (domExpr instanceof OpApplNode if (domExpr instanceof OpApplNode
&& ((OpApplNode) domExpr).getOperator().getName().toString().equals("$Tuple")) { && ((OpApplNode) domExpr).getOperator().getName().equals("$Tuple")) {
ArrayList<TLAType> domList = new ArrayList<>(); List<TLAType> domList = new ArrayList<>();
OpApplNode domOpAppl = (OpApplNode) domExpr; for (ExprOrOpArgNode arg : ((OpApplNode) domExpr).getArgs()) {
for (int j = 0; j < domOpAppl.getArgs().length; j++) { domList.add(visitExprOrOpArgNode(arg, new UntypedType()));
TLAType d = visitExprOrOpArgNode(domOpAppl.getArgs()[j], new UntypedType());
domList.add(d);
} }
domType = new TupleType(domList); domType = new TupleType(domList);
domExpr.setToolObject(TYPE_ID, domType); // store type setType(domExpr, domType); // store type
} else { } else {
domType = visitExprOrOpArgNode(domExpr, new UntypedType()); domType = visitExprOrOpArgNode(domExpr, new UntypedType());
} }
rangeType = evalType(list, valueType);
FunctionType func = new FunctionType(domType, rangeType); TLAType rangeType = evalType(list, valueType);
try { t = unify(t, new FunctionType(domType, rangeType), pair);
t = t.unify(func);
} catch (UnificationException e) {
throw new TypeErrorException(
String.format("Expected %s, found %s at 'EXCEPT',%n%s", t, func, pair.getLocation()));
}
} }
} }
return t; return t;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment