in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [1497:2006]
private List<ExtElimClause> typecheckFunctionBody(FunctionDefinition typedDef, Concrete.BaseFunctionDefinition def) {
UniverseKind universeKind = typedDef.getUniverseKind();
if (myNewDef) {
typedDef.setUniverseKind(UniverseKind.WITH_UNIVERSES);
}
FunctionKind kind = def.getKind();
if (def instanceof Concrete.CoClauseFunctionDefinition) {
Referable ref = ((Concrete.CoClauseFunctionDefinition) def).getImplementedField();
if (ref instanceof TCDefReferable) {
Definition fieldDef = ((TCDefReferable) ref).getTypechecked();
if (fieldDef instanceof ClassField && DependentLink.Helper.size(typedDef.getParameters()) != Concrete.getNumberOfParameters(def.getParameters())) {
if (myNewDef) {
typechecker.setStatus(def.getStatus().getTypecheckingStatus());
typedDef.addStatus(Definition.TypeCheckingStatus.HAS_ERRORS);
def.setTypechecked();
}
return null;
}
if (fieldDef instanceof ClassField && ((ClassField) fieldDef).isProperty()) {
if (((ClassField) fieldDef).getTypeLevel() == null) {
kind = FunctionKind.LEMMA;
} else if (def.getResultType() == null) {
boolean ok = true;
for (Concrete.Parameter parameter : def.getParameters()) {
if (parameter.getType() != null) {
ok = false;
}
}
if (ok) {
kind = FunctionKind.LEMMA;
}
}
}
}
if (kind != FunctionKind.LEMMA) {
kind = FunctionKind.FUNC;
}
}
if (typedDef.getResultType() == null) {
typedDef.setResultType(new ErrorExpression());
}
Expression expectedType = typedDef.getResultType();
List<ExtElimClause> clauses = null;
Concrete.FunctionBody body = def.getBody();
boolean checkLevelNow = (body instanceof Concrete.ElimFunctionBody || body.getTerm() instanceof Concrete.CaseExpression && def.getKind() != FunctionKind.LEVEL) && def.getKind() != FunctionKind.AXIOM && !checkResultTypeLater(def);
Integer typeLevel = checkLevelNow ? checkTypeLevel(def, typedDef, false) : null;
if (typeLevel != null && typedDef.isSFunc()) {
if (body instanceof Concrete.ElimFunctionBody) {
for (Concrete.FunctionClause clause : body.getClauses()) {
CheckTypeVisitor.setCaseLevel(clause.getExpression(), typeLevel, true);
}
} else {
CheckTypeVisitor.setCaseLevel(body.getTerm(), typeLevel, true);
}
}
boolean bodyIsOK = false;
ClassCallExpression consType = null;
boolean checkCanBeLemma = true;
if (def.getKind() == FunctionKind.LEVEL && typedDef.getResultType() instanceof UniverseExpression && ((UniverseExpression) typedDef.getResultType()).getSort().getHLevel().isClosed() && (body instanceof Concrete.TermFunctionBody || body instanceof Concrete.ElimFunctionBody && body.getClauses().isEmpty())) {
ArendExtension extension = typechecker.getExtension();
LevelProver prover = extension == null ? null : extension.getLevelProver();
Definition useParent = def.getUseParent() == null ? null : def.getUseParent().getTypechecked();
if (prover != null && useParent instanceof CallableDefinition callableUseParent && (!typedDef.getParameters().hasNext() || DependentLink.Helper.size(typedDef.getParameters()) == DependentLink.Helper.size(useParent.getParameters()))) {
try (var ignored = new Utils.RefContextSaver(typechecker.getContext(), typechecker.getLocalExpressionPrettifier())) {
boolean ok = true;
if (typedDef.getParameters().hasNext()) {
ExprSubstitution substitution = new ExprSubstitution();
DependentLink useParam = useParent.getParameters();
for (DependentLink param = typedDef.getParameters(); param.hasNext(); param = param.getNext(), useParam = useParam.getNext()) {
if (!param.getTypeExpr().subst(substitution).isLessOrEquals(useParam.getTypeExpr(), DummyEquations.getInstance(), null)) {
ok = false;
break;
}
substitution.add(param, new ReferenceExpression(useParam));
}
} else {
typedDef.setParameters(useParent.getParameters());
for (DependentLink param = typedDef.getParameters(); param.hasNext(); param = param.getNext()) {
typechecker.addBinding(null, param);
}
}
if (ok) {
List<Expression> args = new ArrayList<>();
for (DependentLink param = typedDef.getParameters(); param.hasNext(); param = param.getNext()) {
args.add(new ReferenceExpression(param));
}
Expression type = callableUseParent.getDefCall(useParent.makeIdLevels(), args);
Sort sort = type.getSortOfType();
if (sort != null) {
int level = ((UniverseExpression) typedDef.getResultType()).getSort().getHLevel().getConstant();
CountingErrorReporter countingErrorReporter = new CountingErrorReporter(GeneralError.Level.ERROR, errorReporter);
TypecheckingResult result = typechecker.withErrorReporter(countingErrorReporter, tc ->
typechecker.finalize(TypecheckingResult.fromChecked(prover.prove(body.getTerm(), type, CheckTypeVisitor.getLevelExpression(new TypeExpression(type, sort), level), level, def, tc)), def, false));
if (result == null) {
if (countingErrorReporter.getErrorsNumber() == 0) {
errorReporter.report(new TypecheckingError("Cannot prove level", def));
}
typedDef.setResultType(new ErrorExpression());
} else {
typedDef.setBody(result.expression);
typedDef.setResultType(result.type);
}
}
}
}
}
} else if (body instanceof Concrete.ElimFunctionBody elimBody) {
List<DependentLink> elimParams = ElimTypechecking.getEliminatedParameters(elimBody.getEliminatedReferences(), elimBody.getClauses(), typedDef.getParameters(), typechecker);
CountingErrorReporter countingErrorReporter = new CountingErrorReporter(PathEndpointMismatchError.class, errorReporter);
if (elimParams != null) {
clauses = typechecker.withErrorReporter(countingErrorReporter, tc -> new PatternTypechecking(PatternTypechecking.Mode.FUNCTION, typechecker, true, null, elimParams).typecheckClauses(elimBody.getClauses(), def.getParameters(), typedDef.getParameters(), expectedType, myNewDef ? typedDef : null));
}
Sort sort = expectedType.getSortOfType();
Body typedBody = clauses == null || def.getKind() == FunctionKind.AXIOM ? null : new ElimTypechecking(errorReporter, typechecker.getEquations(), expectedType, PatternTypechecking.Mode.FUNCTION, typeLevel, sort != null ? sort.getHLevel() : Level.INFINITY, kind.isSFunc() && kind != FunctionKind.TYPE, elimBody.getClauses(), typedDef.getParametersOriginalDefinitions().size(), def).typecheckElim(clauses, typedDef.getParameters(), elimParams);
if (typedBody != null) {
if (myNewDef) {
typedDef.setBody(typedBody);
typedDef.addStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
boolean conditionsResult = countingErrorReporter.getErrorsNumber() > 0 || typedDef.getKind() == CoreFunctionDefinition.Kind.LEMMA || new ConditionsChecking(DummyEquations.getInstance(), errorReporter, def).check(typedBody, clauses, elimBody.getClauses(), typedDef);
if (myNewDef && !conditionsResult) {
typedDef.addStatus(Definition.TypeCheckingStatus.HAS_ERRORS);
}
} else {
clauses = null;
}
} else if (body instanceof Concrete.CoelimFunctionBody) {
if (def.getResultType() != null) {
fixClassElements(typedDef, def, body.getCoClauseElements());
checkCanBeLemma = false;
Pair<Expression, ClassCallExpression> result = typecheckCoClauses(typedDef, def, kind, body.getCoClauseElements());
if (result != null) {
if (myNewDef && !def.isRecursive()) {
if (kind == FunctionKind.CONS) {
typedDef.setResultType(result.proj1.getType());
} else {
ClassCallExpression resultType = result.proj2;
boolean hasProperties = false;
for (ClassField field : resultType.getImplementedHere().keySet()) {
if (field.isProperty()) {
hasProperties = true;
break;
}
}
if (hasProperties) {
Map<ClassField, Expression> resultTypeImpls = new LinkedHashMap<>();
resultType = new ClassCallExpression(result.proj2.getDefinition(), result.proj2.getLevels(), resultTypeImpls, Sort.PROP, UniverseKind.NO_UNIVERSES);
ExprSubstitution substitution = new ExprSubstitution(result.proj2.getThisBinding(), new ReferenceExpression(resultType.getThisBinding()));
for (Map.Entry<ClassField, Expression> entry : result.proj2.getImplementedHere().entrySet()) {
if (!entry.getKey().isProperty()) {
resultTypeImpls.put(entry.getKey(), entry.getValue().subst(substitution));
}
}
typechecker.fixClassExtSort(resultType, def.getResultType());
resultType.updateHasUniverses();
}
typedDef.setResultType(resultType);
if (hasProperties || result.proj2.getNumberOfNotImplementedFields() > 0) {
typedDef.setBody(result.proj1);
if (hasProperties) typedDef.reallyHideBody();
}
}
}
consType = result.proj2;
}
bodyIsOK = true;
}
} else if (body instanceof Concrete.TermFunctionBody) {
Concrete.Expression bodyTerm = ((Concrete.TermFunctionBody) body).getTerm();
boolean useExpectedType = !expectedType.isError();
TypecheckingResult nonFinalResult = typechecker.checkExpr(bodyTerm, useExpectedType ? expectedType : null);
if (useExpectedType && !(expectedType instanceof Type && ((Type) expectedType).isOmega())) {
if (kind == FunctionKind.LEMMA || def.getData().getKind() == GlobalReferable.Kind.DEFINED_CONSTRUCTOR || nonFinalResult == null || !nonFinalResult.type.isInstance(ClassCallExpression.class)) {
if (nonFinalResult == null) {
nonFinalResult = new TypecheckingResult(null, expectedType);
} else {
nonFinalResult.type = expectedType;
}
} else {
checkCanBeLemma = false;
}
}
TypecheckingResult termResult = typechecker.finalize(nonFinalResult, bodyTerm, kind == FunctionKind.LEMMA);
if (termResult != null) {
if (myNewDef) {
Expression expr = termResult.expression;
while (expr instanceof LetExpression) {
expr = ((LetExpression) expr).getExpression();
}
if (expr instanceof NewExpression) {
ExprSubstitution substitution = new ExprSubstitution();
expr = termResult.expression;
while (expr instanceof LetExpression) {
for (HaveClause clause : ((LetExpression) expr).getClauses()) {
substitution.add(clause, new ReferenceExpression(new PersistentEvaluatingBinding(clause.getName(), clause.getExpression().subst(substitution))));
}
expr = ((LetExpression) expr).getExpression();
}
termResult.expression = expr.subst(substitution);
if (termResult.type instanceof LetExpression) {
expr = termResult.type;
while (expr instanceof LetExpression) {
expr = ((LetExpression) expr).getExpression();
}
termResult.type = expr.subst(substitution);
}
}
if (!def.isRecursive()) {
Expression newType = termResult.type;
if ((typedDef.isSFunc() || kind == FunctionKind.CONS) && typedDef.getResultType() != null) {
Expression normNewType = newType.normalize(NormalizationMode.WHNF);
Expression oldType = typedDef.getResultType().normalize(NormalizationMode.WHNF);
if (oldType instanceof ClassCallExpression oldClassCall && normNewType instanceof ClassCallExpression newClassCall) {
Map<ClassField, Expression> impls = new LinkedHashMap<>();
for (Map.Entry<ClassField, Expression> entry : newClassCall.getImplementedHere().entrySet()) {
if (oldClassCall.isImplemented(entry.getKey())) {
impls.put(entry.getKey(), entry.getValue());
}
}
if (impls.size() != newClassCall.getImplementedHere().size()) {
newClassCall = new ClassCallExpression(newClassCall.getDefinition(), newClassCall.getLevels(), impls, newClassCall.getDefinition().getSort(), newClassCall.getDefinition().getUniverseKind());
newClassCall.updateHasUniverses();
typechecker.fixClassExtSort(newClassCall, def.getResultType());
newType = newClassCall;
}
}
}
typedDef.setResultType(newType);
}
if (termResult.expression != null) {
typedDef.setBody(termResult.expression);
}
}
if (termResult.expression instanceof NewExpression && myNewDef && def.getData().getKind() != GlobalReferable.Kind.DEFINED_CONSTRUCTOR && (expectedType.isError() || !typedDef.isSFunc()) && !def.isRecursive()) {
typedDef.setResultType(((NewExpression) termResult.expression).getType());
}
}
} else {
throw new IllegalStateException();
}
if (typedDef.getKind() == CoreFunctionDefinition.Kind.SFUNC && typedDef.getActualBody() instanceof IntervalElim) {
errorReporter.report(new TypecheckingError("\\sfunc cannot be defined by pattern matching on the interval", def));
typedDef.setKind(CoreFunctionDefinition.Kind.FUNC);
}
if (typedDef instanceof DConstructor) {
Set<DependentLink> usedVars = new HashSet<>();
ExpressionPattern pattern = null;
if (body instanceof Concrete.TermFunctionBody) {
Body coreBody = typedDef.getReallyActualBody();
if (coreBody instanceof NewExpression && typedDef.getResultType() instanceof ClassCallExpression) {
pattern = checkDConstructor((ClassCallExpression) typedDef.getResultType(), (NewExpression) coreBody, usedVars, def);
} else if (coreBody instanceof Expression) {
pattern = checkDConstructor((Expression) coreBody, usedVars, body.getTerm());
}
} else if (body instanceof Concrete.CoelimFunctionBody) {
if (consType != null && typedDef.getResultType() instanceof ClassCallExpression && ((ClassCallExpression) typedDef.getResultType()).getNumberOfNotImplementedFields() == 0) {
pattern = checkDConstructor(consType, new NewExpression(null, (ClassCallExpression) typedDef.getResultType()), usedVars, def);
}
} else {
errorReporter.report(new TypecheckingError("\\cons cannot be defined by pattern matching", def));
}
if (pattern != null) {
int numberOfParameters = 0;
for (DependentLink link = typedDef.getParameters(); link.hasNext(); link = link.getNext()) {
if (usedVars.contains(link)) {
break;
}
numberOfParameters++;
}
for (DependentLink link = DependentLink.Helper.get(typedDef.getParameters(), numberOfParameters); link.hasNext(); link = link.getNext()) {
if (!usedVars.contains(link)) {
errorReporter.report(new TypecheckingError("Parameters of \\cons that do not occur in patterns must be listed before other parameters", def));
pattern = null;
break;
}
}
if (pattern != null) {
DependentLink link = typedDef.getParameters();
for (int i = 0; i < numberOfParameters; i++) {
if (link.isExplicit()) {
errorReporter.report(new TypecheckingError("Parameters of \\cons that do not occur in patterns must be implicit", def));
pattern = null;
break;
}
if (!typedDef.getResultType().findBinding(link)) {
if (!typedDef.getResultType().reportIfError(errorReporter, def)) {
errorReporter.report(new TypecheckingError("Parameters of \\cons that do not occur in patterns must occur in the result type", def));
}
pattern = null;
break;
}
link = link.getNext();
}
}
if (myNewDef && pattern != null) {
((DConstructor) typedDef).setPattern(pattern);
((DConstructor) typedDef).setNumberOfParameters(numberOfParameters);
}
}
}
if (myNewDef) {
ClassCallExpression typeClassCall = typedDef.getResultType().cast(ClassCallExpression.class);
if (typeClassCall != null) {
Map<ClassField, Expression> newImpls = new LinkedHashMap<>();
ClassCallExpression newClassCall = new ClassCallExpression(typeClassCall.getDefinition(), typeClassCall.getLevels(), newImpls, typeClassCall.getSort(), typeClassCall.getUniverseKind());
Expression newThisBinding = new ReferenceExpression(newClassCall.getThisBinding());
boolean allImpl = true;
for (ClassField field : typeClassCall.getDefinition().getNotImplementedFields()) {
if (!field.isProperty()) {
Expression impl = typeClassCall.getAbsImplementationHere(field);
if (impl != null) {
newImpls.put(field, impl.subst(typeClassCall.getThisBinding(), newThisBinding));
} else {
allImpl = false;
}
}
}
if (typedDef.getResultTypeLevel() == null) {
typedDef.setResultType(newClassCall);
}
if (allImpl) {
bodyIsOK = true;
if (typedDef.getResultTypeLevel() == null) {
typedDef.reallyHideBody();
if (typedDef.getReallyActualBody() instanceof NewExpression && ((NewExpression) typedDef.getReallyActualBody()).getRenewExpression() == null) {
ClassCallExpression bodyClassCall = ((NewExpression) typedDef.getReallyActualBody()).getClassCall();
Map<ClassField, Expression> newBodyImpls = new LinkedHashMap<>();
ClassCallExpression newBodyClassCall = new ClassCallExpression(bodyClassCall.getDefinition(), bodyClassCall.getLevels(), newBodyImpls, bodyClassCall.getSort(), bodyClassCall.getUniverseKind());
Expression newBodyThisBinding = new ReferenceExpression(newBodyClassCall.getThisBinding());
for (ClassField field : bodyClassCall.getDefinition().getNotImplementedFields()) {
if (field.isProperty()) {
Expression impl = bodyClassCall.getAbsImplementationHere(field);
if (impl != null) {
newBodyImpls.put(field, impl.subst(bodyClassCall.getThisBinding(), newBodyThisBinding));
}
}
}
typedDef.setBody(newBodyClassCall.getImplementedHere().isEmpty() ? null : new NewExpression(null, newBodyClassCall));
}
} else {
typedDef.setBody(null);
}
}
}
if (kind != FunctionKind.LEMMA && kind != FunctionKind.LEVEL && typedDef.getBody() instanceof DefCallExpression) {
Integer level = ((DefCallExpression) typedDef.getBody()).getUseLevel();
if (level != null) {
typedDef.addParametersLevel(new ParametersLevel(null, level));
}
}
if (typedDef.getResultType() == null) {
typedDef.setResultType(new ErrorExpression());
}
ElimBody elimBody;
if (typedDef.getActualBody() instanceof ElimBody) {
elimBody = (ElimBody) typedDef.getActualBody();
} else if (typedDef.getActualBody() instanceof IntervalElim) {
elimBody = ((IntervalElim) typedDef.getActualBody()).getOtherwise();
} else {
elimBody = null;
}
GoodThisParametersVisitor goodThisParametersVisitor;
if (elimBody != null) {
goodThisParametersVisitor = new GoodThisParametersVisitor(typedDef.getGoodThisParameters(), elimBody, DependentLink.Helper.size(typedDef.getParameters()));
} else {
goodThisParametersVisitor = new GoodThisParametersVisitor(typedDef.getGoodThisParameters(), typedDef.getParameters());
goodThisParametersVisitor.visitBody(typedDef.getActualBody(), null);
}
typedDef.setGoodThisParameters(goodThisParametersVisitor.getGoodParameters());
if (universeKind != UniverseKind.WITH_UNIVERSES) {
if (new UniverseKindChecker(def.getRecursiveDefinitions()).check(typedDef.getResultType())) {
typedDef.setUniverseKind(UniverseKind.WITH_UNIVERSES);
} else {
typedDef.setUniverseKind(universeKind);
if (typedDef.getKind() != CoreFunctionDefinition.Kind.LEMMA && def.getKind() != FunctionKind.LEVEL) {
typedDef.setUniverseKind(universeKind.max(new UniverseKindChecker(def.getRecursiveDefinitions()).getUniverseKind(typedDef.getActualBody())));
}
}
}
}
if (checkCanBeLemma) {
checkCanBeLemma(typedDef, def);
}
if (!checkLevelNow) {
checkTypeLevel(def, typedDef, true);
}
if (kind == FunctionKind.INSTANCE) {
ClassCallExpression typecheckedResultType = typedDef.getResultType() instanceof ClassCallExpression ? (ClassCallExpression) typedDef.getResultType() : null;
if (typecheckedResultType != null && !typecheckedResultType.getDefinition().isRecord()) {
ClassField classifyingField = typecheckedResultType.getDefinition().getClassifyingField();
Expression classifyingExpr;
if (classifyingField != null) {
classifyingExpr = typecheckedResultType.getImplementation(classifyingField, new NewExpression(null, typecheckedResultType));
Set<SingleDependentLink> params = new LinkedHashSet<>();
while (classifyingExpr instanceof LamExpression) {
for (SingleDependentLink link = ((LamExpression) classifyingExpr).getParameters(); link.hasNext(); link = link.getNext()) {
params.add(link);
}
classifyingExpr = ((LamExpression) classifyingExpr).getBody();
}
if (classifyingExpr != null) {
classifyingExpr = classifyingExpr.normalize(NormalizationMode.WHNF);
}
if (!(classifyingExpr == null || classifyingExpr instanceof ErrorExpression || classifyingExpr instanceof DataCallExpression || classifyingExpr instanceof ConCallExpression || classifyingExpr instanceof FunCallExpression && ((FunCallExpression) classifyingExpr).getDefinition().getKind() == CoreFunctionDefinition.Kind.TYPE || classifyingExpr instanceof ClassCallExpression || params.isEmpty() && (classifyingExpr instanceof UniverseExpression || classifyingExpr instanceof SigmaExpression || classifyingExpr instanceof PiExpression || classifyingExpr instanceof IntegerExpression))) {
errorReporter.report(new TypecheckingError("Classifying field must be either a universe, a sigma type, a record, or a partially applied data or constructor", def.getResultType() == null ? def : def.getResultType()));
}
} else {
classifyingExpr = null;
}
int index = 0;
for (DependentLink link = typedDef.getParameters(); link.hasNext(); link = link.getNext()) {
if (link instanceof TypedDependentLink && typedDef.getTypeClassParameterKind(index) == Definition.TypeClassParameterKind.YES) {
Expression type = link.getTypeExpr();
if (type instanceof ClassCallExpression classCall && !classCall.getDefinition().isRecord()) {
ClassField paramClassifyingField = classCall.getDefinition().getClassifyingField();
ReferenceExpression refExpr = new ReferenceExpression(link);
Expression classifyingImpl = null;
Expression classifyingExprType = null;
if (paramClassifyingField != null) {
Levels fieldLevels = classCall.getLevels(paramClassifyingField.getParentClass());
classifyingImpl = classCall.getImplementation(paramClassifyingField, refExpr);
if (classifyingImpl == null) {
classifyingImpl = FieldCallExpression.make(paramClassifyingField, refExpr);
}
classifyingExprType = classCall.getDefinition().getFieldType(paramClassifyingField, fieldLevels, refExpr);
}
if (classifyingImpl == null || classifyingExpr == null || compareExpressions(classifyingImpl, classifyingExpr, classifyingExprType) != -1) {
typedDef.setTypeClassParameter(index, Definition.TypeClassParameterKind.ONLY_LOCAL);
}
}
}
index++;
}
} else if (!expectedType.isError()) {
errorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.INSTANCE_TYPE, def));
}
} else if (kind == FunctionKind.TYPE) {
if (!(typedDef.getResultType() instanceof UniverseExpression)) {
if (!typedDef.getResultType().reportIfError(errorReporter, def.getResultType())) {
errorReporter.report(new TypeMismatchError(new UniverseExpression(Sort.STD), typedDef.getResultType(), def.getResultType()));
}
typedDef.setKind(CoreFunctionDefinition.Kind.SFUNC);
}
} else if (kind == FunctionKind.AXIOM) {
if (!(body instanceof Concrete.ElimFunctionBody && body.getClauses().isEmpty() && body.getEliminatedReferences().isEmpty())) {
errorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.AXIOM_WITH_BODY, def));
if (myNewDef) {
typedDef.setBody(null);
}
}
} else if (myNewDef && def instanceof Concrete.CoClauseFunctionDefinition && def.getKind() == FunctionKind.CLASS_COCLAUSE) {
Referable fieldRef = ((Concrete.CoClauseFunctionDefinition) def).getImplementedField();
Definition fieldDef = fieldRef instanceof TCDefReferable ? ((TCDefReferable) fieldRef).getTypechecked() : null;
Definition useParent = def.getUseParent().getTypechecked();
if (fieldDef instanceof ClassField && useParent instanceof ClassDefinition classDef) {
Map<ClassField, Expression> defaultImpl = new LinkedHashMap<>();
ClassCallExpression thisType = new ClassCallExpression(classDef, classDef.makeIdLevels(), defaultImpl, classDef.getSort(), classDef.getUniverseKind());
for (ClassField field : classDef.getNotImplementedFields()) {
Pair<AbsExpression, Boolean> defaultPair = classDef.getDefaultPair(field);
if (defaultPair != null && defaultPair.proj2) {
defaultImpl.put(field, defaultPair.proj1.apply(new ReferenceExpression(thisType.getThisBinding()), LevelSubstitution.EMPTY));
}
}
TypedSingleDependentLink thisBinding = new TypedSingleDependentLink(false, "this", thisType, true);
thisType.setSort(classDef.computeSort(defaultImpl, thisBinding));
thisType.updateHasUniverses();
Expression result = DefCallResult.makeTResult(new Concrete.ReferenceExpression(def.getData().getData(), def.getData()), typedDef, classDef.makeIdLevels()).applyExpression(new ReferenceExpression(thisBinding), false, typechecker, def).toResult(typechecker).expression;
Expression actualType = result.getType();
Expression fieldType = ((ClassField) fieldDef).getType().applyExpression(new ReferenceExpression(thisBinding));
CompareVisitor visitor = new CompareVisitor(DummyEquations.getInstance(), CMP.LE, def);
if (visitor.compare(actualType, fieldType, Type.OMEGA, true)) {
classDef.addDefault((ClassField) fieldDef, new AbsExpression(thisBinding, result), true);
} else {
CompareVisitor.Result compareResult = visitor.getResult();
errorReporter.report(compareResult == null ? new TypeMismatchError(fieldType, actualType, def) : new TypeMismatchWithSubexprError(compareResult, def));
}
}
}
if (myNewDef) {
typechecker.setStatus(def.getStatus().getTypecheckingStatus());
typedDef.addStatus(typechecker.getStatus().max(!bodyIsOK && typedDef.getActualBody() == null && def.getKind() != FunctionKind.AXIOM ? Definition.TypeCheckingStatus.HAS_ERRORS : Definition.TypeCheckingStatus.NO_ERRORS));
def.setTypechecked();
}
return clauses;
}