in base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java [1388:1583]
private TypecheckingResult typecheckClassExt(List<? extends Concrete.ClassFieldImpl> classFieldImpls, Expression expectedType, Expression renewExpr, ClassCallExpression classCallExpr, Set<ClassField> pseudoImplemented, Concrete.Expression expr, boolean useDefaults) {
ClassDefinition baseClass = classCallExpr.getDefinition();
Map<ClassField, Expression> fieldSet = new LinkedHashMap<>();
ClassCallExpression resultClassCall = new ClassCallExpression(baseClass, classCallExpr.getLevels(), fieldSet, Sort.PROP, baseClass.getUniverseKind());
copyImplementationsFrom(resultClassCall, classCallExpr, expr);
resultClassCall.updateHasUniverses();
Set<ClassField> defined = new HashSet<>();
List<Pair<Definition,Concrete.ClassFieldImpl>> implementations = new ArrayList<>(classFieldImpls.size());
for (Concrete.ClassFieldImpl classFieldImpl : classFieldImpls) {
Definition definition = referableToDefinition(classFieldImpl.getImplementedField(), classFieldImpl);
if (definition != null) {
boolean ok = true;
if (definition instanceof ClassField classField) {
if (baseClass.containsField(classField)) {
defined.add(classField);
} else {
errorReporter.report(new IncorrectImplementationError(classField, baseClass, classFieldImpl));
ok = false;
}
} else if (definition instanceof ClassDefinition) {
if (baseClass.isSubClassOf((ClassDefinition) definition)) {
defined.addAll(((ClassDefinition) definition).getNotImplementedFields());
defined.addAll(((ClassDefinition) definition).getImplementedFields());
} else {
errorReporter.report(new IncorrectImplementationError((ClassDefinition) definition, baseClass, classFieldImpl));
ok = false;
}
}
if (ok) {
implementations.add(new Pair<>(definition, classFieldImpl));
}
}
}
FieldDFS dfs = new FieldDFS(resultClassCall.getDefinition());
if (renewExpr != null) {
for (ClassField field : baseClass.getNotImplementedFields()) {
if (!defined.contains(field) && !resultClassCall.isImplementedHere(field)) {
Set<ClassField> found = FindDefCallVisitor.findDefinitions(field.getType().getCodomain(), defined);
if (!found.isEmpty()) {
Concrete.SourceNode sourceNode = null;
for (Pair<Definition, Concrete.ClassFieldImpl> implementation : implementations) {
if (implementation.proj1 instanceof ClassField && found.contains(implementation.proj1)) {
sourceNode = implementation.proj2;
break;
}
}
if (sourceNode == null) {
sourceNode = expr;
}
errorReporter.report(new FieldDependencyError(field, found, sourceNode));
return null;
}
fieldSet.put(field, FieldCallExpression.make(field, renewExpr));
}
}
} else if (useDefaults && !baseClass.getDefaults().isEmpty()) {
MapDFS<ClassField> defaultDFS = new MapDFS<>(baseClass.getDefaultDependencies());
defaultDFS.visit(defined);
defaultDFS.visit(resultClassCall.getImplementedHere().keySet());
Set<ClassField> notDefault = defaultDFS.getVisited();
Map<ClassField, AbsExpression> defaults = new HashMap<>();
DFS<ClassField, Boolean> implDfs = new DFS<>() {
@Override
protected Boolean forDependencies(ClassField field) {
if (defined.contains(field) || resultClassCall.isImplemented(field)) return true;
AbsExpression impl = baseClass.getDefault(field);
if (impl == null || notDefault.contains(field)) return false;
Set<ClassField> dependencies = baseClass.getDefaultImplDependencies().get(field);
if (dependencies != null) {
for (ClassField dependency : dependencies) {
Boolean ok = visit(dependency);
if (ok == null || !ok) return false;
}
}
defaults.put(field, impl);
return true;
}
@Override
protected Boolean getVisitedValue(ClassField field, boolean cycle) {
return !cycle && (defined.contains(field) || resultClassCall.isImplemented(field) || defaults.containsKey(field));
}
};
for (ClassField field : baseClass.getNotImplementedFields()) {
implDfs.visit(field);
AbsExpression defaultImpl = defaults.get(field);
if (defaultImpl != null && !notDefault.contains(field)) {
Pair<AbsExpression, Boolean> pair = baseClass.getDefaultPair(field);
checkImplementationCycle(dfs, field, defaultImpl.apply(new ReferenceExpression(resultClassCall.getThisBinding()), resultClassCall.getLevelSubstitution()), pair != null && pair.proj2, resultClassCall, expr);
}
}
}
if (!implementations.isEmpty()) {
if (resultClassCall.getDefinition() == Prelude.DEP_ARRAY && !resultClassCall.getImplementedHere().isEmpty()) {
for (Pair<Definition, Concrete.ClassFieldImpl> pair : implementations) {
if (pair.proj1 instanceof ClassField) {
resultClassCall.getImplementedHere().remove(pair.proj1);
} else if (pair.proj1 instanceof ClassDefinition) {
resultClassCall.getImplementedHere().keySet().removeAll(((ClassDefinition) pair.proj1).getNotImplementedFields());
resultClassCall.getImplementedHere().keySet().removeAll(((ClassDefinition) pair.proj1).getImplementedFields());
}
}
}
Referable thisRef = addBinding(null, resultClassCall.getThisBinding());
myClassCallBindings.add(resultClassCall.getThisBinding());
try {
for (Pair<Definition, Concrete.ClassFieldImpl> pair : implementations) {
if (pair.proj1 instanceof ClassField field) {
TypecheckingResult implResult = typecheckImplementation(field, pair.proj2.implementation, resultClassCall, !(pair.proj2 instanceof Concrete.CoClauseFunctionReference));
if (implResult != null) {
Expression oldImpl = null;
if (!field.isProperty()) {
oldImpl = resultClassCall.getAbsImplementationHere(field);
if (oldImpl == null) {
AbsExpression absImpl = resultClassCall.getDefinition().getImplementation(field);
oldImpl = absImpl == null ? null : absImpl.getExpression().subst(resultClassCall.getLevelSubstitution());
}
}
if (oldImpl != null) {
if (!classCallExpr.isImplemented(field) || !CompareVisitor.compare(myEquations, CMP.EQ, implResult.expression, oldImpl, implResult.type, pair.proj2.implementation)) {
errorReporter.report(new FieldsImplementationError(true, baseClass.getReferable(), Collections.singletonList(field.getReferable()), pair.proj2));
}
} else if (!resultClassCall.isImplemented(field)) {
checkImplementationCycle(dfs, field, implResult.expression, false, resultClassCall, pair.proj2.implementation);
}
} else if (pseudoImplemented != null) {
pseudoImplemented.add(field);
} else if (!resultClassCall.isImplemented(field)) {
fieldSet.put(field, new ErrorExpression());
}
} else if (pair.proj1 instanceof ClassDefinition classDef) {
TypecheckingResult result = pair.proj2.implementation instanceof Concrete.ThisExpression ? checkThisExpression((Concrete.ThisExpression) pair.proj2.implementation, null, null, pair.proj2.implementation, 1) : checkExpr(pair.proj2.implementation, null);
if (result != null) {
Expression type = result.type.normalize(NormalizationMode.WHNF);
ClassCallExpression classCall = type.cast(ClassCallExpression.class);
if (classCall == null) {
if (!type.reportIfError(errorReporter, pair.proj2.implementation) && !type.isInstance(ErrorExpression.class)) {
InferenceVariable var = type instanceof InferenceReferenceExpression ? ((InferenceReferenceExpression) type).getVariable() : null;
errorReporter.report(var != null && !(var instanceof MetaInferenceVariable) ? var.getErrorInfer() : new TypeMismatchError(DocFactory.text("a class"), type, pair.proj2.implementation));
}
} else {
if (!classCall.getDefinition().isSubClassOf(classDef)) {
errorReporter.report(new TypeMismatchError(new ClassCallExpression(classDef, classDef.makeMinLevels()), type, pair.proj2.implementation));
} else {
if (classCall.getDefinition().getUniverseKind() != UniverseKind.NO_UNIVERSES && resultClassCall.getDefinition().getUniverseKind() != UniverseKind.NO_UNIVERSES && !resultClassCall.getLevels(classDef).compare(classCall.getLevels(classDef), CMP.EQ, myEquations, pair.proj2.implementation)) {
errorReporter.report(new TypeMismatchError(new ClassCallExpression(classDef, resultClassCall.getLevels(classDef)), classCall, pair.proj2.implementation));
return null;
}
for (ClassField field : classDef.getNotImplementedFields()) {
Levels fieldLevels = classCall.getLevels(field.getParentClass());
Expression impl = FieldCallExpression.make(field, result.expression).normalize(NormalizationMode.WHNF);
boolean isImplemented = resultClassCall.isImplemented(field);
if (isImplemented && !field.isProperty()) {
if (!CompareVisitor.compare(myEquations, CMP.EQ, impl, resultClassCall.getImplementation(field, new ReferenceExpression(resultClassCall.getThisBinding())), classCall.getDefinition().getFieldType(field, fieldLevels, result.expression), pair.proj2.implementation)) {
errorReporter.report(new FieldsImplementationError(true, baseClass.getReferable(), Collections.singletonList(field.getReferable()), pair.proj2));
}
} else {
if (!isImplemented) {
checkImplementationCycle(dfs, field, impl, false, resultClassCall, pair.proj2.implementation);
PiExpression overridden = baseClass.getOverriddenType(field);
if (overridden != null && classCall.getDefinition().getOverriddenType(field) != overridden) {
Expression actualFieldType = impl.getType();
Expression expectedFieldType = overridden.getCodomain().subst(new ExprSubstitution(overridden.getParameters(), result.expression), classCallExpr.getLevelSubstitution());
if (!CompareVisitor.compare(myEquations, CMP.LE, actualFieldType, expectedFieldType, Type.OMEGA, pair.proj2.implementation)) {
errorReporter.report(new TypeMismatchError("The type of field '" + field.getName() + "' does not match", expectedFieldType, actualFieldType, pair.proj2.implementation));
}
}
}
}
}
resultClassCall.updateHasUniverses();
}
}
}
} else {
errorReporter.report(new WrongReferable("Expected either a field or a class", pair.proj2.getImplementedField(), pair.proj2));
}
}
} finally {
myClassCallBindings.remove(myClassCallBindings.size() - 1);
}
removeBinding(thisRef);
}
resultClassCall.fixOrderOfImplementations();
fixClassExtSort(resultClassCall, expr);
resultClassCall.updateHasUniverses();
return checkResult(expectedType, new TypecheckingResult(resultClassCall, new UniverseExpression(resultClassCall.getSortOfType())), expr);
}