in base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java [2416:2590]
private TypecheckingResult visitLam(List<? extends Concrete.Parameter> parameters, Concrete.LamExpression expr, ParametersProvider provider) {
if (parameters.isEmpty()) {
return checkExpr(expr.getBody(), provider.getType());
}
Function<Pair<ParametersProvider,SingleDependentLink>, Pair<TypecheckingResult,Boolean>> checker = pair -> {
ParametersProvider newProvider = pair.proj1;
SingleDependentLink piParam = pair.proj2;
Concrete.Parameter param = parameters.get(0);
if (param.isProperty()) {
errorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.PROPERTY_IGNORED, param));
}
if (piParam != null && !piParam.isExplicit() && param.isExplicit()) {
for (SingleDependentLink link = piParam; link.hasNext(); link = link.getNext()) {
addBinding(null, link);
if (link instanceof UntypedSingleDependentLink) {
newProvider.nextParameter();
}
}
return new Pair<>(bodyToLam(piParam, visitLam(parameters, expr, newProvider), expr), true);
}
if (param instanceof Concrete.NameParameter) {
if (piParam == null) {
TypedSingleDependentLink link = visitNameParameter((Concrete.NameParameter) param, expr);
TypecheckingResult bodyResult = visitLam(parameters.subList(1, parameters.size()), expr, new ExpressionParametersProvider(new InferenceReferenceExpression(new ExpressionInferenceVariable(new UniverseExpression(Sort.generateInferVars(myEquations, false, expr)), expr, getAllBindings(), true, true))));
if (bodyResult == null) return new Pair<>(null, true);
Sort sort = PiExpression.generateUpperBound(link.getType().getSortOfType(), getSortOfType(bodyResult.type, expr), myEquations, expr);
TypecheckingResult result = new TypecheckingResult(new LamExpression(sort, link, bodyResult.expression), new PiExpression(sort, link, bodyResult.type));
Expression expectedType = newProvider.getType();
return new Pair<>(expectedType == null ? result : checkResult(expectedType, result, expr), true);
} else {
Referable referable = ((Concrete.NameParameter) param).getReferable();
if (piParam.isExplicit() && !param.isExplicit()) {
errorReporter.report(new ImplicitLambdaError(referable, -1, param));
}
Type paramType = piParam.getType();
DefCallExpression defCallParamType = paramType.getExpr().cast(DefCallExpression.class);
if (defCallParamType != null && defCallParamType.getDefinition().getUniverseKind() == UniverseKind.NO_UNIVERSES) { // fixes test pLevelTest
Definition definition = defCallParamType.getDefinition();
Levels levels = definition instanceof DataDefinition || definition instanceof FunctionDefinition || definition instanceof ClassDefinition ? definition.generateInferVars(myEquations, false, param) : null;
if (definition instanceof ClassDefinition) {
ClassCallExpression classCall = (ClassCallExpression) defCallParamType;
for (Map.Entry<ClassField, Expression> entry : classCall.getImplementedHere().entrySet()) {
Expression type = entry.getValue().getType();
if (type == null || !CompareVisitor.compare(myEquations, CMP.LE, type, classCall.getDefinition().getFieldType(entry.getKey(), levels, new ReferenceExpression(classCall.getThisBinding())), Type.OMEGA, param)) {
levels = null;
break;
}
}
} else if (levels != null) {
ExprSubstitution substitution = new ExprSubstitution();
DependentLink link = definition.getParameters();
LevelSubstitution levelSubst = levels.makeSubstitution(definition);
for (Expression arg : defCallParamType.getDefCallArguments()) {
Expression type = arg.getType();
if (type == null || !CompareVisitor.compare(myEquations, CMP.LE, type, link.getTypeExpr().subst(substitution, levelSubst), Type.OMEGA, param)) {
levels = null;
break;
}
substitution.add(link, arg);
link = link.getNext();
}
}
if (levels != null) {
if (definition instanceof DataDefinition) {
paramType = DataCallExpression.make((DataDefinition) definition, levels, new ArrayList<>(defCallParamType.getDefCallArguments()));
} else if (definition instanceof FunctionDefinition) {
paramType = new TypeExpression(FunCallExpression.make((FunctionDefinition) definition, levels, new ArrayList<>(defCallParamType.getDefCallArguments())), paramType.getSortOfType());
} else {
ClassCallExpression classCall = (ClassCallExpression) defCallParamType;
paramType = new ClassCallExpression((ClassDefinition) definition, levels, classCall.getImplementedHere(), classCall.getDefinition().computeSort(classCall.getImplementedHere(), classCall.getThisBinding()), classCall.getUniverseKind());
}
}
}
SingleDependentLink link = new TypedSingleDependentLink(piParam.isExplicit(), referable == null ? null : referable.textRepresentation(), paramType);
addBinding(referable, link);
newProvider.subst(piParam, new ReferenceExpression(link));
return new Pair<>(bodyToLam(link, visitLam(parameters.subList(1, parameters.size()), expr, newProvider), expr), true);
}
} else if (param instanceof Concrete.TypeParameter) {
SingleDependentLink link = visitTypeParameter((Concrete.TypeParameter) param, null, piParam == null || piParam.isExplicit() != param.isExplicit() ? null : piParam.getType());
if (link == null) {
return new Pair<>(null, true);
}
int namesCount = param.getNumberOfParameters();
SingleDependentLink actualLink = link;
if (piParam != null) {
Expression argType = link.getTypeExpr();
for (int i = 0; i < namesCount; i++, actualLink = actualLink.getNext()) {
while (piParam instanceof UntypedDependentLink && i < namesCount - 1) {
newProvider.subst(piParam, new ReferenceExpression(actualLink));
piParam = newProvider.nextParameter();
actualLink = actualLink.getNext();
i++;
}
if (piParam == null) {
break;
}
if (piParam.isExplicit() && !param.isExplicit() && i < namesCount) {
errorReporter.report(new ImplicitLambdaError(param.getReferableList().get(i), namesCount > 1 ? i : -1, param));
}
if (!CompareVisitor.compare(myEquations, CMP.EQ, argType, piParam.getTypeExpr(), Type.OMEGA, param.getType())) {
if (!argType.reportIfError(errorReporter, param.getType())) {
errorReporter.report(new TypeMismatchError("Type mismatch in an argument of the lambda", piParam.getTypeExpr(), argType, param.getType()));
return new Pair<>(null, true);
}
}
newProvider.subst(piParam, new ReferenceExpression(actualLink));
if (i < namesCount - 1) {
piParam = newProvider.nextParameter();
}
}
}
TypecheckingResult bodyResult = visitLam(parameters.subList(1, parameters.size()), expr, actualLink.hasNext() ? NULL_PARAMETERS_PROVIDER : newProvider);
if (bodyResult == null) return new Pair<>(null, true);
Sort sort = PiExpression.generateUpperBound(link.getType().getSortOfType(), getSortOfType(bodyResult.type, expr), myEquations, expr);
if (actualLink.hasNext()) {
Expression expectedType = newProvider.getType();
if (expectedType != null) {
TypecheckingResult result = checkResult(expectedType, new TypecheckingResult(new LamExpression(sort, actualLink, bodyResult.expression), new PiExpression(sort, actualLink, bodyResult.type)), expr);
if (result == null || link == actualLink) return new Pair<>(result, true);
if (!(result.expression instanceof LamExpression)) {
DependentLink prevLink = link;
while (prevLink.getNext() != actualLink) {
prevLink = prevLink.getNext();
}
prevLink.setNext(EmptyDependentLink.getInstance());
prevLink = link;
while (prevLink.getNext().hasNext()) {
prevLink = prevLink.getNext();
}
if (prevLink instanceof UntypedDependentLink) {
TypedSingleDependentLink lastLink = new TypedSingleDependentLink(prevLink.isExplicit(), prevLink.getName(), actualLink.getType(), prevLink.isHidden());
if (prevLink == link) {
link = lastLink;
} else {
DependentLink prevPrevLink = link;
while (prevPrevLink.getNext() != prevLink) {
prevPrevLink = prevPrevLink.getNext();
}
prevPrevLink.setNext(lastLink);
}
}
return new Pair<>(new TypecheckingResult(new LamExpression(sort, link, result.expression), new PiExpression(sort, link, result.type)), true);
}
}
}
return new Pair<>(new TypecheckingResult(new LamExpression(sort, link, bodyResult.expression), new PiExpression(sort, link, bodyResult.type)), true);
} else {
throw new IllegalStateException();
}
};
SingleDependentLink piParam = provider.nextParameter();
if (piParam != null) {
return checker.apply(new Pair<>(provider, piParam)).proj1;
}
var pair2 = provider.coerce(newProvider -> {
SingleDependentLink newPiParam = newProvider.nextParameter();
if (newPiParam == null) return null;
var pair = checker.apply(new Pair<>(newProvider, newPiParam));
return new Pair<>(pair.proj1 == null ? null : pair.proj1.expression, pair.proj2);
});
return pair2 != null ? pair2.proj1 : checker.apply(new Pair<>(provider, null)).proj1;
}