in base/src/main/java/org/arend/typechecking/implicitargs/StdImplicitArgsInference.java [294:496]
private TResult checkArrayCons(DefCallResult defCallResult, List<Concrete.Argument> arguments, Expression expectedType, Concrete.Expression fun) {
int index = 0;
Expression length = null;
Definition definition = defCallResult.getDefinition();
if (definition == Prelude.ARRAY_CONS && !arguments.isEmpty() && !arguments.get(0).isExplicit()) {
TypecheckingResult result = myVisitor.checkExpr(arguments.get(0).expression, Nat());
if (result == null) return null;
length = result.expression;
index++;
}
Sort sort = defCallResult.getLevels().toLevelPair().toSort();
Sort sort0 = sort.max(Sort.SET0);
Expression elementsType = null;
if (index < arguments.size() && !arguments.get(index).isExplicit()) {
TypecheckingResult result = myVisitor.checkExpr(arguments.get(index).expression, definition == Prelude.EMPTY_ARRAY ? new PiExpression(sort.succ(), new TypedSingleDependentLink(true, null, Fin(Zero())), new UniverseExpression(sort)) : length == null ? null : new PiExpression(sort.succ(), new TypedSingleDependentLink(true, null, Fin(Suc(length))), new UniverseExpression(sort)));
if (result == null) return null;
elementsType = result.expression;
index++;
}
for (; index < arguments.size() && !arguments.get(index).isExplicit(); index++) {
myVisitor.getErrorReporter().report(new ArgumentExplicitnessError(true, arguments.get(index).expression));
}
int index2 = index + 1;
for (; index2 < arguments.size() && !arguments.get(index2).isExplicit(); index2++) {
myVisitor.getErrorReporter().report(new ArgumentExplicitnessError(true, arguments.get(index2).expression));
}
TResult result = defCallResult;
if (expectedType != null) {
ClassCallExpression expectedClassCall = TypeConstructorExpression.unfoldType(expectedType).cast(ClassCallExpression.class);
if (expectedClassCall != null) {
if (expectedClassCall.getDefinition() != Prelude.DEP_ARRAY || !expectedClassCall.getLevels().compare(defCallResult.getLevels(), CMP.LE, myVisitor.getEquations(), fun)) {
myVisitor.getErrorReporter().report(new TypeMismatchError(expectedClassCall, refDoc(Prelude.DEP_ARRAY.getRef()), fun));
return null;
}
if (elementsType == null) {
elementsType = expectedClassCall.getAbsImplementationHere(Prelude.ARRAY_ELEMENTS_TYPE);
}
if (definition != Prelude.EMPTY_ARRAY && length == null) {
length = expectedClassCall.getAbsImplementationHere(Prelude.ARRAY_LENGTH);
length = length == null ? null : length.normalize(NormalizationMode.WHNF).pred();
}
}
}
if (definition == Prelude.EMPTY_ARRAY) {
if (elementsType != null) {
result = result.applyExpression(elementsType, false, myVisitor, fun);
}
} else {
if (length != null) {
result = result.applyExpression(length, false, myVisitor, fun);
if (elementsType != null) {
result = result.applyExpression(elementsType, false, myVisitor, fun);
}
}
}
defCallResult = result instanceof DefCallResult ? (DefCallResult) result : null;
if (definition == Prelude.ARRAY_CONS && defCallResult != null && defCallResult.getArguments().isEmpty() && index2 < arguments.size()) {
InferenceVariable var = null;
Expression constType;
ClassCallExpression argClassCall = null;
if (elementsType != null) {
elementsType = elementsType.normalize(NormalizationMode.WHNF);
var = getInferenceVariableFromElementsType(elementsType);
if (var == null) {
constType = elementsType.removeConstLam();
if (constType != null && constType.getInferenceVariable() != null) {
constType = null;
}
if (constType != null) {
Map<ClassField, Expression> impls = new HashMap<>();
argClassCall = new ClassCallExpression(Prelude.DEP_ARRAY, defCallResult.getLevels(), impls, Sort.STD, UniverseKind.NO_UNIVERSES);
impls.put(Prelude.ARRAY_ELEMENTS_TYPE, new LamExpression(sort0, new TypedSingleDependentLink(true, null, Fin(FieldCallExpression.make(Prelude.ARRAY_LENGTH, new ReferenceExpression(argClassCall.getThisBinding())))), constType));
}
}
}
if (argClassCall == null) {
argClassCall = new ClassCallExpression(Prelude.DEP_ARRAY, defCallResult.getLevels());
}
TypecheckingResult result2 = myVisitor.checkExpr(arguments.get(index2).expression, argClassCall);
if (result2 == null) return null;
ClassCallExpression classCall = result2.type.normalize(NormalizationMode.WHNF).cast(ClassCallExpression.class);
if (classCall != null && classCall.getDefinition() != Prelude.DEP_ARRAY) {
myVisitor.getErrorReporter().report(new TypeMismatchError(refDoc(Prelude.DEP_ARRAY.getRef()), result2.type, arguments.get(index2).expression));
return null;
}
TypecheckingResult result1 = null;
boolean checked = false;
if (classCall != null && (elementsType == null || var != null)) {
Expression elementsType1 = classCall.getAbsImplementationHere(Prelude.ARRAY_ELEMENTS_TYPE);
if (elementsType1 != null) {
elementsType = elementsType1.normalize(NormalizationMode.WHNF);
var = getInferenceVariableFromElementsType(elementsType);
}
}
if (var == null) {
constType = elementsType == null ? null : elementsType.removeConstLam();
if (constType != null && constType.getInferenceVariable() == null) {
result1 = myVisitor.checkExpr(arguments.get(index).expression, constType);
if (result1 == null) return null;
checked = true;
if (length == null) length = classCall == null ? null : classCall.getAbsImplementationHere(Prelude.ARRAY_LENGTH);
if (length == null) length = FieldCallExpression.make(Prelude.ARRAY_LENGTH, result2.expression);
result = result
.applyExpression(length, false, myVisitor, fun)
.applyExpression(new LamExpression(sort0, new TypedSingleDependentLink(true, null, DataCallExpression.make(Prelude.FIN, Levels.EMPTY, new SingletonList<>(Suc(length)))), constType), false, myVisitor, fun);
}
}
if (!checked) {
result1 = myVisitor.checkExpr(arguments.get(index).expression, null);
if (result1 == null) return null;
if (var != null) {
if (length == null) length = classCall == null ? null : classCall.getAbsImplementationHere(Prelude.ARRAY_LENGTH);
if (length == null) length = FieldCallExpression.make(Prelude.ARRAY_LENGTH, result2.expression);
Expression actualElementsType = new LamExpression(sort0, new TypedSingleDependentLink(true, null, DataCallExpression.make(Prelude.FIN, Levels.EMPTY, new SingletonList<>(length))), result1.type);
if (new CompareVisitor(myVisitor.getEquations(), CMP.LE, fun).normalizedCompare(actualElementsType, elementsType, null, false)) {
checked = true;
result = result
.applyExpression(length, false, myVisitor, fun)
.applyExpression(new LamExpression(sort0, new TypedSingleDependentLink(true, null, DataCallExpression.make(Prelude.FIN, Levels.EMPTY, new SingletonList<>(Suc(length)))), result1.type), false, myVisitor, fun);
}
}
if (!checked) {
result = fixImplicitArgs(result, result.getImplicitParameters(), fun, false, null);
List<? extends Expression> args = ((DefCallResult) result).getArguments();
Expression expected1 = AppExpression.make(args.get(1), Zero(), true);
if (!new CompareVisitor(myVisitor.getEquations(), CMP.LE, fun).normalizedCompare(result1.type, expected1, null, false)) {
myVisitor.getErrorReporter().report(new TypeMismatchError(expected1, result1.type, arguments.get(index).expression));
return null;
}
Map<ClassField, Expression> impls = new LinkedHashMap<>();
impls.put(Prelude.ARRAY_LENGTH, args.get(0));
TypedSingleDependentLink lamParam = new TypedSingleDependentLink(true, "j", DataCallExpression.make(Prelude.FIN, Levels.EMPTY, new SingletonList<>(args.get(0))));
impls.put(Prelude.ARRAY_ELEMENTS_TYPE, new LamExpression(sort0, lamParam, AppExpression.make(args.get(1), Suc(new ReferenceExpression(lamParam)), true)));
Expression expected2 = new ClassCallExpression(Prelude.DEP_ARRAY, defCallResult.getLevels(), impls, Sort.STD, UniverseKind.NO_UNIVERSES);
if (!new CompareVisitor(myVisitor.getEquations(), CMP.LE, fun).normalizedCompare(result2.type, expected2, null, false)) {
myVisitor.getErrorReporter().report(new TypeMismatchError(expected2, result2.type, arguments.get(index2).expression));
return null;
}
}
}
result = result
.applyExpression(result1.expression, true, myVisitor, arguments.get(index).expression)
.applyExpression(result2.expression, true, myVisitor, arguments.get(index2).expression);
index = index2 + 1;
if (result instanceof TypecheckingResult tcResult && tcResult.type instanceof ClassCallExpression resultClassCall && arguments.get(0).isExplicit() && result2.type instanceof ClassCallExpression result2ClassCall && !result2ClassCall.isImplemented(Prelude.ARRAY_LENGTH)) {
Expression resultElementsType = resultClassCall.getAbsImplementationHere(Prelude.ARRAY_ELEMENTS_TYPE);
if (resultElementsType != null) {
resultElementsType = resultElementsType.removeConstLam();
if (resultElementsType != null) {
resultClassCall.getImplementedHere().remove(Prelude.ARRAY_LENGTH);
resultClassCall.getImplementedHere().put(Prelude.ARRAY_ELEMENTS_TYPE, new LamExpression(result2ClassCall.getSort(), new TypedSingleDependentLink(true, null, ExpressionFactory.Fin(ExpressionFactory.FieldCall(Prelude.ARRAY_LENGTH, new ReferenceExpression(resultClassCall.getThisBinding())))), resultElementsType));
}
} else {
resultClassCall.getImplementedHere().remove(Prelude.ARRAY_LENGTH);
}
}
} else if (definition == Prelude.ARRAY_CONS && elementsType == null && index2 == arguments.size() && index < arguments.size() && defCallResult != null && defCallResult.getArguments().isEmpty()) {
TypecheckingResult result1 = myVisitor.checkExpr(arguments.get(index).expression, null);
if (result1 == null) return null;
Sort sort1 = result1.type.getSortOfType();
if (sort1 == null) return null;
if (!Sort.compare(sort1, sort, CMP.LE, myVisitor.getEquations(), arguments.get(index).expression)) {
return null;
}
Type type;
if (length == null) {
type = new TypeExpression(FunCallExpression.make(Prelude.ARRAY, defCallResult.getLevels(), new SingletonList<>(result1.type)), sort);
} else {
Map<ClassField, Expression> impls = new LinkedHashMap<>();
impls.put(Prelude.ARRAY_LENGTH, length);
impls.put(Prelude.ARRAY_ELEMENTS_TYPE, new LamExpression(sort0, new TypedSingleDependentLink(true, null, Fin(length)), result1.type));
type = new ClassCallExpression(Prelude.DEP_ARRAY, defCallResult.getLevels(), impls, Sort.STD, UniverseKind.NO_UNIVERSES);
}
TypedSingleDependentLink lamParam = new TypedSingleDependentLink(true, "l", type);
if (length == null) length = FieldCallExpression.make(Prelude.ARRAY_LENGTH, new ReferenceExpression(lamParam));
elementsType = new LamExpression(sort0, new TypedSingleDependentLink(true, null, Fin(Suc(length))), result1.type);
Expression resultExpr = new LamExpression(sort, lamParam, ArrayExpression.make(defCallResult.getLevels().toLevelPair(), elementsType, new SingletonList<>(result1.expression), new ReferenceExpression(lamParam)));
return new TypecheckingResult(resultExpr, resultExpr.getType());
} else if (index + 1 < index2) {
arguments.subList(index + 1, index2).clear();
}
for (; index < arguments.size(); index++) {
result = inferArg(result, arguments.get(index).expression, arguments.get(index).isExplicit(), fun);
}
return result;
}