in base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java [1660:1771]
public TypecheckingResult visitNew(Concrete.NewExpression expr, Expression expectedType) {
if (expr.getExpression() instanceof Concrete.ClassExtExpression classExt) {
Concrete.Expression baseClassExpr = classExt.getBaseClassExpression();
if (baseClassExpr instanceof Concrete.AppExpression) {
baseClassExpr = ((Concrete.AppExpression) baseClassExpr).getFunction();
}
if (baseClassExpr instanceof Concrete.ReferenceExpression && ((Concrete.ReferenceExpression) baseClassExpr).getReferent() instanceof MetaReferable && ((MetaReferable) ((Concrete.ReferenceExpression) baseClassExpr).getReferent()).getDefinition() == null) {
return makeNew(checkMeta((Concrete.ReferenceExpression) baseClassExpr, classExt.getBaseClassExpression() instanceof Concrete.AppExpression ? ((Concrete.AppExpression) classExt.getBaseClassExpression()).getArguments() : Collections.emptyList(), classExt.getCoclauses(), null), expr, expectedType, Collections.emptySet());
}
}
TypecheckingResult exprResult = null;
Set<ClassField> pseudoImplemented = Collections.emptySet();
Concrete.Expression classExpr = desugarClassApp(expr.getExpression() instanceof Concrete.ClassExtExpression ? ((Concrete.ClassExtExpression) expr.getExpression()).getBaseClassExpression() : expr.getExpression(), !(expr.getExpression() instanceof Concrete.ClassExtExpression), Collections.emptySet());
boolean isClassExtOrRef = classExpr instanceof Concrete.ClassExtExpression || classExpr instanceof Concrete.ReferenceExpression;
if (expr.getExpression() instanceof Concrete.ClassExtExpression) {
if (classExpr instanceof Concrete.ClassExtExpression) {
((Concrete.ClassExtExpression) classExpr).getStatements().addAll(((Concrete.ClassExtExpression) expr.getExpression()).getStatements());
} else {
classExpr = expr.getExpression();
}
}
if (isClassExtOrRef) {
Expression unfoldedType = expectedType == null ? null : TypeConstructorExpression.unfoldType(expectedType);
Concrete.Expression baseExpr = classExpr instanceof Concrete.ClassExtExpression ? ((Concrete.ClassExtExpression) classExpr).getBaseClassExpression() : classExpr;
Definition actualDef = unfoldedType instanceof ClassCallExpression && baseExpr instanceof Concrete.ReferenceExpression && ((Concrete.ReferenceExpression) baseExpr).getReferent() instanceof TCDefReferable ? ((TCDefReferable) ((Concrete.ReferenceExpression) baseExpr).getReferent()).getTypechecked() : null;
if (baseExpr instanceof Concrete.HoleExpression || actualDef instanceof ClassDefinition) {
ClassCallExpression actualClassCall = null;
if (baseExpr instanceof Concrete.HoleExpression && !(unfoldedType instanceof ClassCallExpression)) {
errorReporter.report(new TypecheckingError("Cannot infer an expression", baseExpr));
return null;
}
ClassCallExpression expectedClassCall = (ClassCallExpression) unfoldedType;
if (baseExpr instanceof Concrete.ReferenceExpression baseRefExpr) {
ClassDefinition actualClass = (ClassDefinition) actualDef;
boolean ok = actualClass.isSubClassOf(expectedClassCall.getDefinition());
if (ok && (actualDef != expectedClassCall.getDefinition() || baseRefExpr.getPLevels() != null || baseRefExpr.getHLevels() != null)) {
boolean fieldsOK = true;
for (ClassField implField : expectedClassCall.getImplementedHere().keySet()) {
if (actualClass.isImplemented(implField)) {
fieldsOK = false;
break;
}
}
Levels levels = typecheckLevels(actualDef, baseRefExpr, actualDef.generateInferVars(myEquations, expr), false);
actualClassCall = new ClassCallExpression(actualClass, levels, new LinkedHashMap<>(), expectedClassCall.getSort(), actualDef.getUniverseKind());
// It's probably better to use CMP.LE here, but then we need to check that copied implementations fit into their types with new levels.
if (!actualClass.castLevels(expectedClassCall.getDefinition(), levels).compare(expectedClassCall.getLevels(), CMP.EQ, myEquations, expr)) {
errorReporter.report(new TypeMismatchWithSubexprError(new CompareVisitor.Result(actualClassCall, expectedClassCall, actualClassCall, expectedClassCall, actualClassCall.getLevels(), expectedClassCall.getLevels()), expr));
fieldsOK = false;
}
if (fieldsOK) {
copyImplementationsFrom(actualClassCall, expectedClassCall, expr);
}
}
if (!ok) {
errorReporter.report(new TypeMismatchError(unfoldedType, baseExpr, baseExpr));
return null;
}
}
if (actualClassCall != null) {
expectedClassCall = actualClassCall;
expectedClassCall.updateHasUniverses();
}
pseudoImplemented = new HashSet<>();
exprResult = typecheckClassExt(classExpr instanceof Concrete.ClassExtExpression ? ((Concrete.ClassExtExpression) classExpr).getStatements() : Collections.emptyList(), null, expectedClassCall, pseudoImplemented, classExpr, true);
if (exprResult == null) {
return null;
}
}
}
Expression renewExpr = null;
if (exprResult == null) {
Concrete.Expression baseClassExpr;
List<Concrete.ClassFieldImpl> classFieldImpls;
if (classExpr instanceof Concrete.ClassExtExpression) {
baseClassExpr = ((Concrete.ClassExtExpression) classExpr).getBaseClassExpression();
classFieldImpls = ((Concrete.ClassExtExpression) classExpr).getStatements();
} else {
baseClassExpr = classExpr;
classFieldImpls = Collections.emptyList();
}
TypecheckingResult typeCheckedBaseClass = baseClassExpr instanceof Concrete.ReferenceExpression && ((Concrete.ReferenceExpression) baseClassExpr).getReferent() == Prelude.DEP_ARRAY.getRef()
? tResultToResult(null, visitReference((Concrete.ReferenceExpression) baseClassExpr, true), baseClassExpr)
: baseClassExpr instanceof Concrete.ReferenceExpression
? visitReference((Concrete.ReferenceExpression) baseClassExpr, null, false)
: baseClassExpr instanceof Concrete.AppExpression
? visitApp((Concrete.AppExpression) baseClassExpr, null, false)
: checkExpr(baseClassExpr, null);
if (typeCheckedBaseClass == null) {
return null;
}
ClassCallExpression classCall = TypeConstructorExpression.unfoldType(typeCheckedBaseClass.expression).cast(ClassCallExpression.class);
if (classCall == null) {
classCall = TypeConstructorExpression.unfoldType(typeCheckedBaseClass.type).cast(ClassCallExpression.class);
if (classCall == null) {
errorReporter.report(new TypecheckingError("Expected a class or a class instance", baseClassExpr));
return null;
}
renewExpr = typeCheckedBaseClass.expression;
}
exprResult = typecheckClassExt(classFieldImpls, null, renewExpr, classCall, null, baseClassExpr, true);
}
return makeNew(exprResult, expr, expectedType, pseudoImplemented);
}