in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [2674:3264]
private void typecheckClass(Concrete.ClassDefinition def, ClassDefinition typedDef) {
if (myNewDef) {
typedDef.clear();
typedDef.setUniverseKind(UniverseKind.WITH_UNIVERSES);
typedDef.setParametersOriginalDefinitions(def.getParametersOriginalDefinitions());
typedDef.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
boolean classOk = true;
fixClassElements(typedDef, def, def.getElements());
// Set level fields
{
findLevelsParentsInClass(typedDef, def);
List<LevelVariable> levelParams = typecheckLevelParameters(def);
if (myNewDef) {
typedDef.setLevelParameters(levelParams);
}
}
List<LocalInstance> localInstances = new ArrayList<>();
boolean hasClassifyingField = false;
if (!def.isRecord() && !def.withoutClassifying()) {
if (def.getClassifyingField() != null) {
hasClassifyingField = true;
} else {
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
if (superClass.getClassifyingField() != null) {
hasClassifyingField = true;
break;
}
}
}
}
// Typecheck class parameters
{
Concrete.Expression previousType = null;
ClassField previousField = null;
for (Concrete.ClassElement element : def.getElements()) {
if (element instanceof Concrete.ClassField field) {
if (!field.getData().isParameterField()) {
continue;
}
if (previousType == field.getResultType()) {
if (myNewDef && previousField != null) {
ClassField newField = addField(field.getData(), typedDef, previousField.getType(), previousField.getTypeLevel());
newField.setStatus(previousField.status());
newField.setUniverseKind(previousField.getUniverseKind());
newField.setNumberOfParameters(previousField.getNumberOfParameters());
if (field.isCoerce()) {
newField.setHideable(true);
}
}
} else {
previousType = field.getResultType();
previousField = typecheckClassField(field, typedDef, localInstances, hasClassifyingField, def);
}
}
}
}
// Process super classes
for (Concrete.ReferenceExpression aSuperClass : def.getSuperClasses()) {
ClassDefinition superClass = typechecker.referableToDefinition(aSuperClass.getReferent(), ClassDefinition.class, "Expected a class", aSuperClass);
if (superClass == null) {
continue;
}
if (superClass == Prelude.DEP_ARRAY) {
errorReporter.report(new TypecheckingError("Array cannot be extended", aSuperClass));
continue;
}
if (myNewDef) {
typedDef.addSuperClass(superClass);
}
}
Levels idLevels = typedDef.makeIdLevels();
// Set super class levels
{
Map<ClassDefinition, Levels> superLevels = new HashMap<>();
int i = 0;
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
superLevels.put(superClass, typechecker.typecheckLevels(superClass, def.getSuperClasses().get(i++), null, false));
}
if (!superLevels.isEmpty()) {
LevelEquationsSolver levelSolver = typechecker.getEquations().makeLevelEquationsSolver();
LevelSubstitution subst = levelSolver.solveLevels();
if (myNewDef && !subst.isEmpty()) {
for (Map.Entry<ClassDefinition, Levels> entry : superLevels.entrySet()) {
entry.setValue(entry.getValue().subst(subst));
}
}
}
i = 0;
for (ClassDefinition currentClass : typedDef.getSuperClasses()) {
Concrete.ReferenceExpression aSuperClass = def.getSuperClasses().get(i++);
Levels currentLevels = superLevels.get(currentClass);
if (currentLevels == null) {
for (Map.Entry<ClassDefinition, Levels> entry : currentClass.getSuperLevels().entrySet()) {
Levels levels = entry.getValue();
Levels superClassLevels = superLevels.get(currentClass);
if (superClassLevels != null) levels = levels.subst(superClassLevels.makeSubstitution(currentClass));
Levels oldLevels = superLevels.putIfAbsent(entry.getKey(), levels);
if (oldLevels != null && !oldLevels.equals(levels)) {
errorReporter.report(new SuperLevelsMismatchError(entry.getKey(), oldLevels, levels, aSuperClass));
}
}
} else {
new DFS<ClassDefinition, Void>() {
@Override
protected Void forDependencies(ClassDefinition unit) {
if (unit != currentClass) {
Levels newLevels = currentClass.castLevels(unit, currentLevels);
Levels oldLevels = superLevels.putIfAbsent(unit, newLevels);
if (oldLevels != null && !oldLevels.equals(newLevels)) {
errorReporter.report(new SuperLevelsMismatchError(unit, oldLevels, newLevels, aSuperClass));
}
}
for (ClassDefinition superClass : unit.getSuperClasses()) {
visit(superClass);
}
return null;
}
}.visit(currentClass);
}
}
i = 0;
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
if (superLevels.get(superClass) != null) continue;
for (Map.Entry<ClassDefinition, Levels> entry : superLevels.entrySet()) {
Levels oldLevels = superLevels.get(entry.getKey());
if (oldLevels != null && !superClass.getSuperLevels().containsKey(entry.getKey()) && superClass.isSubClassOf(entry.getKey())) {
Levels levels = entry.getKey().makeIdLevels();
Levels superClassLevels = superLevels.get(superClass);
if (superClassLevels != null) levels = levels.subst(superClassLevels.makeSubstitution(superClass));
if (!oldLevels.equals(levels)) {
errorReporter.report(new SuperLevelsMismatchError(entry.getKey(), oldLevels, levels, def.getSuperClasses().get(i)));
}
}
}
i++;
}
for (Iterator<Map.Entry<ClassDefinition, Levels>> iterator = superLevels.entrySet().iterator(); iterator.hasNext(); ) {
Map.Entry<ClassDefinition, Levels> entry = iterator.next();
Levels levels = entry.getValue();
if (levels.compare(idLevels, CMP.EQ, DummyEquations.getInstance(), null)) {
iterator.remove();
}
}
if (myNewDef && !superLevels.isEmpty()) {
typedDef.setSuperLevels(superLevels);
}
}
// Copy data from super classes
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
typedDef.addFields(superClass.getNotImplementedFields());
}
Concrete.SourceNode alreadyImplementedSourceNode = null;
List<FieldReferable> alreadyImplementFields = new ArrayList<>();
for (Concrete.ReferenceExpression aSuperClass : def.getSuperClasses()) {
Definition superClassDef = aSuperClass.getReferent() instanceof TCDefReferable ? ((TCDefReferable) aSuperClass.getReferent()).getTypechecked() : null;
if (superClassDef instanceof ClassDefinition superClass) {
for (Map.Entry<ClassField, AbsExpression> entry : superClass.getImplemented()) {
Levels levels = typedDef.getSuperLevels().get(superClass);
if (!implementField(entry.getKey(), entry.getValue().subst(new ExprSubstitution(), levels == null ? idLevels.makeSubstitution(superClass) : levels.makeSubstitution(superClass)), typedDef, alreadyImplementFields)) {
classOk = false;
alreadyImplementedSourceNode = aSuperClass;
}
}
}
}
Set<ClassField> allFields = typedDef.getAllFields();
// Check for cycles in implementations from super classes
boolean checkImplementations = true;
FieldDFS dfs = new FieldDFS(typedDef);
for (ClassField field : allFields) {
List<ClassField> cycle = dfs.findCycle(field);
if (cycle != null) {
errorReporter.report(new FieldCycleError(cycle, def));
checkImplementations = false;
break;
}
}
// Set overridden fields from super classes
if (!typedDef.getSuperClasses().isEmpty()) {
// Collect overridden fields
Set<ClassField> overriddenHere = new HashSet<>();
for (Concrete.ClassElement element : def.getElements()) {
if (element instanceof Concrete.OverriddenField) {
ClassField field = typechecker.referableToClassField(((Concrete.OverriddenField) element).getOverriddenField(), null);
if (field != null) {
overriddenHere.add(field);
}
}
}
for (ClassField field : allFields) {
ClassDefinition originalSuperClass = null;
PiExpression type = null;
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
PiExpression superType = superClass.getOverriddenType(field);
if (superType != null) {
if (type == null) {
originalSuperClass = superClass;
TypedSingleDependentLink thisParam = new TypedSingleDependentLink(false, "this", new ClassCallExpression(typedDef, idLevels), true);
type = new PiExpression(superType.getResultSort(), thisParam, superType.applyExpression(new ReferenceExpression(thisParam)));
} else if (!overriddenHere.contains(field)) {
if (!CompareVisitor.compare(DummyEquations.getInstance(), CMP.EQ, type.getCodomain(), superType.applyExpression(new ReferenceExpression(type.getParameters())), Type.OMEGA, def)) {
if (!type.getCodomain().reportIfError(errorReporter, def) && !superType.getCodomain().reportIfError(errorReporter, def)) {
errorReporter.report(new TypecheckingError("The types of the field '" + field.getName() + "' differ in super classes '" + originalSuperClass.getName() + "' and '" + superClass.getName() + "'", def));
}
originalSuperClass = typedDef;
type = new PiExpression(type.getResultSort(), type.getParameters(), new ErrorExpression());
break;
}
}
}
}
if (type != null) {
typedDef.overrideField(field, type, originalSuperClass);
}
}
for (var entry : typedDef.getOverriddenFields()) {
if (!overriddenHere.contains(entry.getKey())) {
overrideField(entry.getKey(), entry.getValue().proj1, typedDef, def, entry.getValue().proj2);
}
}
}
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
addFieldInstances(superClass, localInstances);
}
// Process fields and implementations
Set<ClassField> implementedHere = new HashSet<>();
for (Concrete.ClassElement element : def.getElements()) {
if (element instanceof Concrete.CoClauseFunctionReference) {
continue;
}
if (element instanceof Concrete.ClassField field) {
if (!field.getData().isParameterField()) {
typecheckClassField(field, typedDef, localInstances, hasClassifyingField, def);
}
} else if (element instanceof Concrete.ClassFieldImpl classFieldImpl) {
ClassField field = typechecker.referableToClassField(classFieldImpl.getImplementedField(), classFieldImpl);
if (field == null || !typedDef.containsField(field)) {
if (field != null) {
errorReporter.report(new IncorrectImplementationError(field, typedDef, classFieldImpl));
}
classOk = false;
continue;
}
if (!classFieldImpl.isDefault()) {
boolean isFieldAlreadyImplemented;
if (myNewDef) {
isFieldAlreadyImplemented = typedDef.isImplemented(field);
} else if (implementedHere.contains(field)) {
isFieldAlreadyImplemented = true;
} else {
isFieldAlreadyImplemented = false;
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
if (superClass.isImplemented(field)) {
isFieldAlreadyImplemented = true;
break;
}
}
}
if (isFieldAlreadyImplemented) {
classOk = false;
alreadyImplementFields.add(field.getReferable());
alreadyImplementedSourceNode = classFieldImpl;
} else {
implementedHere.add(field);
}
if (isFieldAlreadyImplemented || !checkImplementations) {
continue;
}
}
typedDef.updateSort();
TypedSingleDependentLink thisBinding = new TypedSingleDependentLink(false, "this", new ClassCallExpression(typedDef, idLevels), true);
Concrete.LamExpression lamImpl = (Concrete.LamExpression) classFieldImpl.implementation;
TypecheckingResult result;
if (lamImpl != null) {
typechecker.addBinding(lamImpl.getParameters().get(0).getReferableList().get(0), thisBinding);
LocalInstancePool localInstancePool = new LocalInstancePool(typechecker);
addLocalInstances(localInstances, thisBinding, typedDef, !typedDef.isRecord() && typedDef.getClassifyingField() == null, localInstancePool);
GlobalInstancePool instancePool = typechecker.getInstancePool().copy(typechecker);
instancePool.setInstancePool(localInstancePool);
typechecker.setInstancePool(instancePool);
if (field.isProperty()) {
CheckTypeVisitor.setCaseLevel(lamImpl.body, -1, true);
} else if (field.getResultTypeLevel() >= -1) {
CheckTypeVisitor.setCaseLevel(lamImpl.body, field.getResultTypeLevel(), false);
}
Levels superLevels = typedDef.getSuperLevels().get(field.getParentClass());
Expression type = typedDef.getFieldType(field, superLevels == null ? idLevels.makeSubstitution(field) : superLevels.makeSubstitution(field), new ReferenceExpression(thisBinding));
result = typechecker.finalCheckExpr(CheckTypeVisitor.addImplicitLamParams(lamImpl.body, type), type);
} else {
result = null;
}
if (result == null) {
classOk = false;
}
typechecker.getContext().clear();
if (result != null && !classFieldImpl.isDefault()) {
List<ClassField> cycle = dfs.checkDependencies(field, FieldsCollector.getFields(result.expression, thisBinding, typedDef.getAllFields()));
if (cycle != null) {
errorReporter.report(new FieldCycleError(cycle, def));
checkImplementations = false;
}
}
if (myNewDef) {
boolean ok = true;
if (result != null && classFieldImpl.isDefault()) {
Set<ClassField> dependencies = FieldsCollector.getFields(result.expression, thisBinding, typedDef.getAllFields());
if (dependencies.contains(field)) {
errorReporter.report(new TypecheckingError("The implementation depends on the field itself", classFieldImpl));
ok = false;
} else {
typedDef.addDefaultImplDependencies(field, dependencies);
}
}
if (ok) {
AbsExpression abs = new AbsExpression(thisBinding, checkImplementations && result != null ? result.expression : new ErrorExpression());
if (classFieldImpl.isDefault()) {
typedDef.addDefault(field, abs, false);
} else {
typedDef.implementField(field, abs);
}
}
}
} else if (element instanceof Concrete.OverriddenField) {
ClassField field = typecheckClassField((Concrete.OverriddenField) element, typedDef, localInstances, hasClassifyingField, def);
if (field == null) {
classOk = false;
}
} else {
throw new IllegalStateException();
}
}
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
for (Map.Entry<ClassField, Set<ClassField>> entry : superClass.getDefaultDependencies().entrySet()) {
Set<ClassField> dependencies = entry.getValue();
if (!typedDef.getDefaults().isEmpty()) {
Set<ClassField> newDependencies = new HashSet<>();
for (ClassField dependency : dependencies) {
if (typedDef.getDefault(dependency) == null) {
newDependencies.add(dependency);
}
}
if (newDependencies.size() != dependencies.size()) {
dependencies = newDependencies;
}
}
typedDef.addDefaultDependencies(entry.getKey(), dependencies);
}
Set<ClassField> added = new HashSet<>();
for (Map.Entry<ClassField, Pair<AbsExpression, Boolean>> entry : superClass.getDefaults()) {
Levels levels = typedDef.getSuperLevels().get(superClass);
if (typedDef.addDefaultIfAbsent(entry.getKey(), entry.getValue().proj1.subst(new ExprSubstitution(), levels == null ? idLevels.makeSubstitution(superClass) : levels.makeSubstitution(superClass)), entry.getValue().proj2)) {
added.add(entry.getKey());
}
}
for (Map.Entry<ClassField, Set<ClassField>> entry : superClass.getDefaultImplDependencies().entrySet()) {
if (added.contains(entry.getKey())) {
typedDef.addDefaultImplDependencies(entry.getKey(), entry.getValue());
}
}
}
MapDFS<ClassField> fieldDFS = new MapDFS<>(typedDef.getDefaultDependencies());
fieldDFS.visit(typedDef.getImplementedFields());
for (ClassField field : fieldDFS.getVisited()) {
typedDef.removeDefault(field);
}
// Set fields covariance
allFields = typedDef.getAllFields();
Set<ClassField> covariantFields = new HashSet<>(allFields);
ParametersCovarianceChecker checker = new ParametersCovarianceChecker(covariantFields);
for (ClassField field : allFields) {
checker.check(field.getType().getCodomain());
if (covariantFields.isEmpty()) {
break;
}
}
for (ClassField field : covariantFields) {
typedDef.addCovariantField(field);
}
// Process classifying field
if (!def.isRecord()) {
ClassField classifyingField = null;
if (!def.isForcedClassifyingField() && !typedDef.getSuperClasses().isEmpty()) {
Set<ClassDefinition> visited = new HashSet<>();
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
classifyingField = findClassifyingField(superClass, typedDef, visited);
if (classifyingField != null) {
break;
}
}
}
if (classifyingField == null && def.getClassifyingField() != null) {
Definition definition = def.getClassifyingField().getTypechecked();
if (definition instanceof ClassField && ((ClassField) definition).getParentClass().equals(typedDef)) {
classifyingField = (ClassField) definition;
} else {
errorReporter.report(new TypecheckingError("Internal error: coercing field must be a field belonging to the class", def));
}
}
if (def.withoutClassifying()) {
if (classifyingField == null) {
errorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.NO_CLASSIFYING_IGNORED, def));
} else {
classifyingField = null;
}
}
if (myNewDef) {
typedDef.setClassifyingField(classifyingField);
if (classifyingField != null) {
if (classifyingField.getParentClass() == typedDef) {
classifyingField.setHideable(true);
classifyingField.setType(classifyingField.getType().normalize(NormalizationMode.WHNF));
}
typedDef.getCoerceData().addCoercingField(classifyingField, null, null);
}
}
} else {
if (myNewDef) {
typedDef.setRecord();
}
}
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
for (Map.Entry<CoerceData.Key, List<Definition>> entry : superClass.getCoerceData().getMapTo()) {
if (entry.getValue().size() == 1 && entry.getValue().get(0) instanceof ClassField) {
typedDef.getCoerceData().addCoercingField((ClassField) entry.getValue().get(0), null, null);
}
}
}
// Copy coerce functions from super classes
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
for (Map.Entry<CoerceData.Key, List<Definition>> entry : superClass.getCoerceData().getMapTo()) {
typedDef.getCoerceData().putCoerceTo(entry.getKey(), entry.getValue());
}
}
if (!alreadyImplementFields.isEmpty()) {
errorReporter.report(new FieldsImplementationError(true, def.getData(), alreadyImplementFields, alreadyImplementFields.size() > 1 ? def : alreadyImplementedSourceNode));
}
if (myNewDef) {
if (!typedDef.getOverriddenFields().isEmpty()) {
Set<ClassField> superFields = new LinkedHashSet<>();
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
superFields.addAll(superClass.getNotImplementedFields());
}
for (ClassField field : superFields) {
if (field.isProperty() || typedDef.isImplemented(field) || typedDef.isOverridden(field)) {
continue;
}
TypedSingleDependentLink thisParam = new TypedSingleDependentLink(false, "this", new ClassCallExpression(typedDef, idLevels), true);
Expression type = field.getResultTypeFor(typedDef).subst(field.getThisParameter(), new ReferenceExpression(thisParam));
Type newType = type.accept(new MinimizeLevelVisitor(), null);
if (newType != null && newType != type) {
typedDef.overrideField(field, new PiExpression(thisParam.getType().getSortOfType().max(newType.getSortOfType()), thisParam, newType.getExpr()), typedDef);
}
}
}
typedDef.setStatus(!classOk ? Definition.TypeCheckingStatus.HAS_ERRORS : typechecker.getStatus());
typedDef.updateSort();
UniverseKind baseUniverseKind = UniverseKind.NO_UNIVERSES;
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
baseUniverseKind = baseUniverseKind.max(superClass.getBaseUniverseKind());
if (baseUniverseKind == UniverseKind.WITH_UNIVERSES) {
break;
}
}
if (baseUniverseKind != UniverseKind.WITH_UNIVERSES) {
UniverseInParametersChecker checker1 = new UniverseInParametersChecker(def.getRecursiveDefinitions());
for (ClassField field : allFields) {
baseUniverseKind = baseUniverseKind.max(checker1.getUniverseKind(field.getResultTypeFor(typedDef)));
if (baseUniverseKind == UniverseKind.WITH_UNIVERSES) {
break;
}
if (checker1.isOmega()) {
typedDef.addOmegaField(field);
}
}
if (baseUniverseKind != UniverseKind.NO_UNIVERSES) {
typedDef.getOmegaFields().clear();
}
}
typedDef.setBaseUniverseKind(baseUniverseKind);
UniverseKind universeKind = baseUniverseKind;
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
universeKind = universeKind.max(superClass.getUniverseKind());
if (universeKind == UniverseKind.WITH_UNIVERSES) {
break;
}
}
if (universeKind != UniverseKind.WITH_UNIVERSES) {
for (ClassField field : typedDef.getNotImplementedFields()) {
if (field.getUniverseKind().ordinal() > universeKind.ordinal()) {
universeKind = field.getUniverseKind();
if (universeKind == UniverseKind.WITH_UNIVERSES) {
break;
}
}
}
}
typedDef.setUniverseKind(universeKind);
for (ClassField field : typedDef.getPersonalFields()) {
field.getType().getParameters().setType(new ClassCallExpression(typedDef, idLevels));
}
Set<ClassField> goodFields = new HashSet<>(typedDef.getPersonalFields());
GoodThisParametersVisitor visitor = new GoodThisParametersVisitor(goodFields);
for (ClassDefinition superClass : typedDef.getSuperClasses()) {
goodFields.addAll(superClass.getGoodThisFields());
}
for (ClassField field : typedDef.getPersonalFields()) {
field.getType().getCodomain().accept(visitor, null);
}
for (Concrete.ClassElement element : def.getElements()) {
if (element instanceof Concrete.ClassFieldImpl) {
ClassField field = typechecker.referableToClassField(((Concrete.ClassFieldImpl) element).getImplementedField(), null);
if (field != null) {
AbsExpression impl = typedDef.getImplementation(field);
if (impl != null) {
impl.getExpression().accept(visitor, null);
}
}
} else if (element instanceof Concrete.OverriddenField) {
ClassField field = typechecker.referableToClassField(((Concrete.OverriddenField) element).getOverriddenField(), null);
if (field != null) {
field.getType().getCodomain().accept(visitor, null);
}
}
}
typedDef.setGoodThisFields(visitor.getGoodFields());
Set<ClassField> typeClassFields = new HashSet<>();
for (Concrete.ClassElement element : def.getElements()) {
if (element instanceof Concrete.ClassField && ((Concrete.ClassField) element).getData().isParameterField()) {
Concrete.Expression resultType = ((Concrete.ClassField) element).getResultType();
if (resultType instanceof Concrete.PiExpression) {
resultType = ((Concrete.PiExpression) resultType).getCodomain();
}
if (isTypeClassRef(resultType)) {
ClassField field = typechecker.referableToClassField(((Concrete.ClassField) element).getData(), null);
if (field != null) {
typeClassFields.add(field);
}
}
}
}
if (!typeClassFields.isEmpty()) {
typedDef.setTypeClassFields(typeClassFields);
}
def.setTypechecked();
}
}