in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [3285:3472]
private ClassField typecheckClassField(Concrete.BaseClassField def, ClassDefinition parentClass, List<LocalInstance> localInstances, boolean hasClassifyingField, Concrete.ClassDefinition classDef) {
ClassField typedDef = null;
if (def instanceof Concrete.OverriddenField) {
typedDef = typechecker.referableToClassField(((Concrete.OverriddenField) def).getOverriddenField(), def);
if (typedDef == null) {
return null;
}
if (typedDef.getParentClass() == parentClass || !parentClass.containsField(typedDef)) {
errorReporter.report(new IncorrectImplementationError(typedDef, parentClass, def));
return null;
}
}
boolean isProperty = false;
boolean ok;
PiExpression piType;
try (var ignored = new Utils.RefContextSaver(typechecker.getContext(), typechecker.getLocalExpressionPrettifier())) {
Concrete.Expression codomain;
Levels idLevels = parentClass.makeIdLevels();
TypedSingleDependentLink thisParam = new TypedSingleDependentLink(false, "this", new ClassCallExpression(parentClass, idLevels), true);
if (!def.getParameters().isEmpty()) {
if (def.getParameters().size() == 1) {
codomain = def.getResultType();
} else {
codomain = new Concrete.PiExpression(def.getParameters().get(1).getData(), def.getParameters().subList(1, def.getParameters().size()), def.getResultType());
}
typechecker.addBinding(def.getParameters().get(0).getReferableList().get(0), thisParam);
} else {
typechecker.addBinding(null, thisParam);
errorReporter.report(new TypecheckingError("Internal error: class field must have a function type", def));
codomain = def.getResultType();
}
LocalInstancePool localInstancePool = new LocalInstancePool(typechecker);
addLocalInstances(localInstances, thisParam, parentClass, !parentClass.isRecord() && !hasClassifyingField, localInstancePool);
GlobalInstancePool instancePool = typechecker.getInstancePool().copy(typechecker);
instancePool.setInstancePool(localInstancePool);
typechecker.setInstancePool(instancePool);
ClassFieldKind kind = def instanceof Concrete.ClassField ? ((Concrete.ClassField) def).getKind() : typedDef == null ? ClassFieldKind.ANY : typedDef.isProperty() ? ClassFieldKind.PROPERTY : ClassFieldKind.FIELD;
Type typeResult = typechecker.finalCheckType(codomain, Type.OMEGA, kind == ClassFieldKind.PROPERTY && def.getResultTypeLevel() == null);
ok = typeResult != null;
Expression typeExpr = ok ? typeResult.getExpr() : new ErrorExpression();
piType = new PiExpression(ok ? Sort.STD.max(typeResult.getSortOfType()) : Sort.STD, thisParam, typeExpr);
if (myNewDef && def instanceof Concrete.ClassField) {
typedDef = addField(((Concrete.ClassField) def).getData(), parentClass, piType, null);
}
if (ok && def.getResultTypeLevel() != null) {
var pair = addPiParametersToContext(def.getParameters(), piType);
if (!pair.proj1.hasNext() && pair.proj2 != null) {
Integer level = typecheckResultTypeLevel(def.getResultTypeLevel(), LevelMismatchError.TargetKind.PROPERTY, pair.proj2, null, typedDef, def instanceof Concrete.OverriddenField);
isProperty = level != null && level == -1 && kind != ClassFieldKind.FIELD;
} else {
// Just reports an error
typechecker.getExpressionLevel(pair.proj1, null, null, DummyEquations.getInstance(), def.getResultTypeLevel());
}
} else if (ok && kind != ClassFieldKind.FIELD) {
Sort sort = typeResult.getSortOfType();
if (sort.isProp()) {
isProperty = true;
} else {
DefCallExpression defCall = typeExpr.cast(DefCallExpression.class);
Integer level = defCall == null ? null : defCall.getUseLevel();
if (kind == ClassFieldKind.PROPERTY) {
boolean check = true;
if ((level == null || level != -1) && typechecker.getExtension() != null) {
LevelProver prover = typechecker.getExtension().getLevelProver();
if (prover != null) {
var pair = addPiParametersToContext(def.getParameters(), piType);
Type typeType;
Expression type = pair.proj2;
if (type == null) {
type = typeExpr;
typeType = typeResult;
} else if (type instanceof Type) {
typeType = (Type) type;
} else {
Sort typeSort = type.getSortOfType();
typeType = new TypeExpression(type, typeSort != null ? typeSort : typeResult.getSortOfType());
}
TypecheckingResult result = pair.proj2 == null ? null : typechecker.finalize(TypecheckingResult.fromChecked(prover.prove(null, type, CheckTypeVisitor.getLevelExpression(typeType, -1), -1, def.getResultType(), typechecker)), def.getResultType(), false);
if (result != null) {
Integer level2 = checkResultTypeLevel(result, LevelMismatchError.TargetKind.PROPERTY, type, null, typedDef, false, def);
if (level2 != null && level2 == -1) {
isProperty = true;
}
check = false;
}
}
}
if (check && checkLevel(LevelMismatchError.TargetKind.PROPERTY, level, sort, def)) {
isProperty = true;
}
} else {
if (level != null && level == -1) {
isProperty = true;
}
}
}
}
}
boolean newDef = myNewDef;
if (newDef && typedDef == null) {
throw new IllegalStateException();
}
GoodThisParametersVisitor goodThisParametersVisitor = new GoodThisParametersVisitor(piType.getParameters());
piType.getCodomain().accept(goodThisParametersVisitor, null);
List<Boolean> goodThisParams = goodThisParametersVisitor.getGoodParameters();
if (goodThisParams.isEmpty() || !goodThisParams.get(0)) {
errorReporter.report(new TypecheckingError("The type of the field contains illegal \\this occurrence", def.getParameters().isEmpty() ? def.getResultType() : def.getParameters().get(0)));
ok = false;
if (newDef && def instanceof Concrete.ClassField) {
typedDef.setType(new PiExpression(piType.getResultSort(), piType.getParameters(), new ErrorExpression()));
}
}
if (def instanceof Concrete.OverriddenField) {
if (!CompareVisitor.compare(DummyEquations.getInstance(), CMP.LE, piType.getCodomain(), typedDef.getType().applyExpression(new ReferenceExpression(piType.getParameters())), Type.OMEGA, def)) {
if (!piType.getCodomain().reportIfError(errorReporter, def) && !typedDef.getType().getCodomain().reportIfError(errorReporter, def)) {
errorReporter.report(new TypecheckingError("The type of the overridden field is not compatible with the specified type", def));
}
ok = false;
}
for (ClassDefinition superClass : parentClass.getSuperClasses()) {
if (!ok) {
break;
}
PiExpression superType = superClass.getOverriddenType(typedDef);
if (superType != null && !CompareVisitor.compare(DummyEquations.getInstance(), CMP.LE, piType.getCodomain(), superType.applyExpression(new ReferenceExpression(piType.getParameters())), Type.OMEGA, def)) {
if (!piType.getCodomain().reportIfError(errorReporter, def) && !superType.getCodomain().reportIfError(errorReporter, def)) {
errorReporter.report(new TypecheckingError("The type of the field in super class '" + superClass.getName() + "' is not compatible with the specified type", def));
}
ok = false;
}
}
if (ok) {
Set<ClassField> allowedFields = new HashSet<>();
for (ClassField field : parentClass.getNotImplementedFields()) {
if (field == typedDef) {
break;
}
allowedFields.add(field);
}
if (piType.accept(new SearchVisitor<Void>() {
@Override
protected CoreExpression.FindAction processDefCall(DefCallExpression expression, Void param) {
return expression.getDefinition() instanceof ClassField field && parentClass.isSubClassOf(field.getParentClass()) && !allowedFields.contains(field) && !parentClass.isImplemented(field) ? CoreExpression.FindAction.STOP : CoreExpression.FindAction.CONTINUE;
}
}, null)) {
ok = false;
}
}
if (newDef && ok) {
overrideField(typedDef, piType, parentClass, def, parentClass);
}
if (!ok) {
return null;
}
}
if (typedDef != null || def instanceof Concrete.ClassField) {
addFieldInstance(typedDef != null ? typedDef : (ClassField) ((Concrete.ClassField) def).getData().getTypechecked(), parentClass, localInstances, false);
}
if (!newDef) {
return null;
}
if (def instanceof Concrete.ClassField field) {
if (field.isCoerce()) {
typedDef.setHideable(true);
parentClass.getCoerceData().addCoercingField(typedDef, errorReporter, field);
}
typedDef.setUniverseKind(new UniverseKindChecker(classDef.getRecursiveDefinitions()).getUniverseKind(typedDef.getType().getCodomain()));
typedDef.setNumberOfParameters(Concrete.getNumberOfParameters(field.getParameters()));
}
if (isProperty && def instanceof Concrete.ClassField) {
typedDef.setIsProperty();
}
if (!ok) {
typedDef.setStatus(Definition.TypeCheckingStatus.HAS_ERRORS);
}
return typedDef;
}