in base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java [359:537]
public TypecheckingResult checkResult(Expression expectedType, TypecheckingResult result, Concrete.Expression expr) {
boolean isOmega = expectedType instanceof Type && ((Type) expectedType).isOmega();
if (result == null || expectedType == null || isOmega && result.type instanceof UniverseExpression) {
return result;
}
CompareVisitor cmpVisitor = new CompareVisitor(DummyEquations.getInstance(), CMP.LE, expr);
if (!isOmega && cmpVisitor.nonNormalizingCompare(result.type, expectedType, Type.OMEGA)) {
return result;
}
result.type = result.type.normalize(NormalizationMode.WHNF);
expectedType = expectedType.normalize(NormalizationMode.WHNF);
if (result.expression instanceof FunCallExpression idp && ((FunCallExpression) result.expression).getDefinition() == Prelude.IDP) {
FunCallExpression equality = expectedType.toEquality();
if (equality != null) {
CompareVisitor visitor = new CompareVisitor(myEquations, CMP.LE, expr);
if (!idp.getLevels().compare(equality.getLevels(), CMP.LE, myEquations, expr)) {
Expression resultType = FunCallExpression.make(Prelude.PATH_INFIX, idp.getLevels(), Arrays.asList(idp.getDefCallArguments().get(0), idp.getDefCallArguments().get(1), idp.getDefCallArguments().get(1)));
errorReporter.report(new TypeMismatchWithSubexprError(new CompareVisitor.Result(resultType, equality, resultType, equality, idp.getLevels(), equality.getLevels()), expr));
return null;
}
if (!visitor.compare(idp.getDefCallArguments().get(0), equality.getDefCallArguments().get(0), Type.OMEGA, false)) {
Expression resultType = FunCallExpression.make(Prelude.PATH_INFIX, idp.getLevels(), Arrays.asList(idp.getDefCallArguments().get(0), idp.getDefCallArguments().get(1), idp.getDefCallArguments().get(1)));
errorReporter.report(new TypeMismatchWithSubexprError(new CompareVisitor.Result(resultType, equality, idp.getDefCallArguments().get(0), equality.getDefCallArguments().get(0), null, null), expr));
return null;
}
visitor.setCMP(CMP.EQ);
Expression type = equality.getDefCallArguments().get(0);
Expression left = equality.getDefCallArguments().get(1).getUnderlyingExpression();
Expression right = equality.getDefCallArguments().get(2).getUnderlyingExpression();
Expression idpArg = idp.getDefCallArguments().get(1).getUnderlyingExpression();
boolean isNotEqualError = idpArg instanceof InferenceReferenceExpression && ((InferenceReferenceExpression) idpArg).getVariable() != null;
if (!(visitor.compare(idpArg, left, type, true) && visitor.compare(idpArg, right, type, true))) {
errorReporter.report(isNotEqualError ? new NotEqualExpressionsError(getExpressionPrettifier(), left, right, expr) : new TypeMismatchError(equality, result.type, expr));
return null;
}
if (left instanceof ArrayExpression) {
Expression elementsType = ((ArrayExpression) left).getElementsType();
if (elementsType instanceof InferenceReferenceExpression && ((InferenceReferenceExpression) elementsType).getVariable() != null) {
type = type.normalize(NormalizationMode.WHNF);
if (type instanceof ClassCallExpression) {
myEquations.addEquation(elementsType, FieldCallExpression.make(Prelude.ARRAY_ELEMENTS_TYPE, right), type, CMP.EQ, expr, ((InferenceReferenceExpression) elementsType).getVariable(), right.getStuckInferenceVariable());
}
}
} else if (right instanceof ArrayExpression) {
Expression elementsType = ((ArrayExpression) right).getElementsType();
if (elementsType instanceof InferenceReferenceExpression && ((InferenceReferenceExpression) elementsType).getVariable() != null) {
type = type.normalize(NormalizationMode.WHNF);
if (type instanceof ClassCallExpression) {
myEquations.addEquation(elementsType, FieldCallExpression.make(Prelude.ARRAY_ELEMENTS_TYPE, left), type, CMP.EQ, expr, ((InferenceReferenceExpression) elementsType).getVariable(), left.getStuckInferenceVariable());
}
}
}
return result;
}
}
boolean actualIsType = result.type instanceof FunCallExpression && ((FunCallExpression) result.type).getDefinition().getKind() == CoreFunctionDefinition.Kind.TYPE;
boolean expectedIsType = expectedType instanceof FunCallExpression && ((FunCallExpression) expectedType).getDefinition().getKind() == CoreFunctionDefinition.Kind.TYPE;
if (!(actualIsType && expectedIsType && ((FunCallExpression) result.type).getDefinition() == ((FunCallExpression) expectedType).getDefinition())) {
if (actualIsType && expectedType.getStuckInferenceVariable() == null) {
TypecheckingResult coerceResult = coerceFromType(result);
if (coerceResult != null) {
result.expression = coerceResult.expression;
result.type = coerceResult.type.normalize(NormalizationMode.WHNF);
TypecheckingResult result2 = (TypecheckingResult) myArgsInference.inferTail(result, expectedType, expr);
if (result2 == null) return null;
result.expression = result2.expression;
result.type = result2.type;
}
}
if (expectedIsType && result.type.getStuckInferenceVariable() == null) {
Pair<TypecheckingResult, Boolean> coerceResult = coerceToType(expectedType, argType -> {
if (!CompareVisitor.compare(myEquations, CMP.LE, result.type, argType, Type.OMEGA, expr)) {
if (!result.type.reportIfError(errorReporter, expr)) {
errorReporter.report(new TypeMismatchError(argType, result.type, expr));
}
return new Pair<>(null, false);
}
return new Pair<>(result.expression, true);
});
if (coerceResult != null) return coerceResult.proj1;
}
}
if (result.type instanceof ClassCallExpression actualClassCall && expectedType instanceof ClassCallExpression expectedClassCall) {
if (actualClassCall.getDefinition().isSubClassOf(expectedClassCall.getDefinition()) && actualClassCall.getDefinition() != Prelude.DEP_ARRAY) {
boolean replace = false;
for (ClassField field : expectedClassCall.getImplementedHere().keySet()) {
if (!actualClassCall.isImplemented(field)) {
replace = true;
break;
}
}
if (replace) {
if (!actualClassCall.getImplementedHere().isEmpty()) {
actualClassCall = new ClassCallExpression(actualClassCall.getDefinition(), actualClassCall.getLevels(), Collections.emptyMap(), actualClassCall.getSort(), actualClassCall.getUniverseKind());
}
result.expression = new NewExpression(result.expression, actualClassCall);
result.type = result.expression.getType();
return checkResultExpr(expectedClassCall, result, expr);
}
}
}
if (expectedType instanceof ClassCallExpression && ((ClassCallExpression) expectedType).getDefinition() == Prelude.DEP_ARRAY && result.type instanceof PiExpression piExpr) {
Expression dom = piExpr.getParameters().getTypeExpr().normalize(NormalizationMode.WHNF);
if (dom instanceof DataCallExpression && ((DataCallExpression) dom).getDefinition() == Prelude.FIN || dom.getStuckInferenceVariable() != null) {
ClassCallExpression classCall = (ClassCallExpression) expectedType;
Expression length = classCall.getClosedImplementation(Prelude.ARRAY_LENGTH);
if (length == null && dom instanceof DataCallExpression) {
length = ((DataCallExpression) dom).getDefCallArguments().get(0);
}
if (length != null) {
Map<ClassField, Expression> impls = new LinkedHashMap<>();
ClassCallExpression resultClassCall = new ClassCallExpression(Prelude.DEP_ARRAY, classCall.getLevels(), impls, Sort.PROP, UniverseKind.NO_UNIVERSES);
Expression elementsType = piExpr.getParameters().getNext().hasNext() ? new LamExpression(piExpr.getResultSort(), DependentLink.Helper.take(piExpr.getParameters(), 1), new PiExpression(piExpr.getResultSort(), piExpr.getParameters().getNext(), piExpr.getCodomain())) : new LamExpression(piExpr.getResultSort(), piExpr.getParameters(), piExpr.getCodomain());
impls.put(Prelude.ARRAY_LENGTH, length);
impls.put(Prelude.ARRAY_ELEMENTS_TYPE, elementsType);
impls.put(Prelude.ARRAY_AT, result.expression);
return checkResultExpr(expectedType, new TypecheckingResult(new NewExpression(null, resultClassCall), resultClassCall), expr);
}
}
} else if (expectedType instanceof DataCallExpression && ((DataCallExpression) expectedType).getDefinition() == Prelude.PATH && result.type instanceof PiExpression) {
int n1 = 0;
Expression actualType = result.type;
while (actualType instanceof PiExpression && ((PiExpression) actualType).getParameters().isExplicit()) {
n1 += DependentLink.Helper.size(((PiExpression) actualType).getParameters());
actualType = ((PiExpression) actualType).getCodomain().normalize(NormalizationMode.WHNF);
}
int n2 = 0;
Expression eType = expectedType;
while (eType instanceof DataCallExpression && ((DataCallExpression) eType).getDefinition() == Prelude.PATH) {
n2++;
eType = AppExpression.make(((DataCallExpression) eType).getDefCallArguments().get(0), new ReferenceExpression(new TypedBinding("i", ExpressionFactory.Interval())), true).normalize(NormalizationMode.WHNF);
}
int n = Math.min(n1, n2);
if (n > 0) {
List<Referable> refs = new ArrayList<>(n - 1);
for (int i = 1; i < n; i++) {
refs.add(new GeneratedLocalReferable("i" + i));
}
Concrete.Expression newExpr = new Concrete.ReferenceExpression(expr.getData(), new CoreReferable(null, result));
if (!refs.isEmpty()) {
List<Concrete.Argument> args = new ArrayList<>(refs.size());
for (Referable ref : refs) {
args.add(new Concrete.Argument(new Concrete.ReferenceExpression(expr.getData(), ref), true));
}
newExpr = Concrete.AppExpression.make(expr.getData(), newExpr, args);
}
Concrete.Expression pathRef = new Concrete.ReferenceExpression(expr.getData(), Prelude.PATH_CON.getRef());
newExpr = Concrete.AppExpression.make(expr.getData(), pathRef, newExpr, true);
for (int i = refs.size() - 1; i >= 0; i--) {
newExpr = Concrete.AppExpression.make(expr.getData(), pathRef, new Concrete.LamExpression(expr.getData(), Collections.singletonList(new Concrete.NameParameter(expr.getData(), true, refs.get(i))), newExpr), true);
}
return checkExpr(newExpr, expectedType);
}
} else if (expectedType instanceof PiExpression && result.type instanceof DataCallExpression && ((DataCallExpression) result.type).getDefinition() == Prelude.PATH) {
return checkExpr(Concrete.AppExpression.make(expr.getData(), new Concrete.ReferenceExpression(expr.getData(), Prelude.AT.getRef()), new Concrete.ReferenceExpression(expr.getData(), new CoreReferable(null, result)), true), expectedType);
}
if (result.type instanceof DataCallExpression && ((DataCallExpression) result.type).getDefinition() == Prelude.FIN && expectedType instanceof DataCallExpression && ((DataCallExpression) expectedType).getDefinition() == Prelude.INT) {
result.expression = Pos(result.expression);
result.type = Int();
return checkResultExpr(expectedType, result, expr);
}
TypecheckingResult coercedResult = CoerceData.coerce(result, expectedType, expr, this);
if (coercedResult != null) {
return (TypecheckingResult) myArgsInference.inferTail(coercedResult, expectedType, expr);
}
return isOmega ? result : checkResultExpr(expectedType, result, expr);
}