in base/src/main/java/org/arend/typechecking/implicitargs/StdImplicitArgsInference.java [499:751]
public TResult infer(Concrete.AppExpression expr, Expression expectedType) {
TResult result;
Concrete.Expression fun = expr.getFunction();
if (fun instanceof Concrete.ReferenceExpression refExpr) {
if (!expr.getArguments().get(0).isExplicit() && (refExpr.getReferent() == Prelude.ZERO.getRef() || refExpr.getReferent() == Prelude.SUC.getRef())) {
TypecheckingResult argResult = myVisitor.checkExpr(expr.getArguments().get(0).getExpression(), Nat());
if (argResult == null) {
return null;
}
if (refExpr.getReferent() == Prelude.ZERO.getRef()) {
result = new TypecheckingResult(new SmallIntegerExpression(0), Fin(Suc(argResult.expression)));
if (expr.getArguments().size() > 1) {
myVisitor.getErrorReporter().report(new NotPiType(myVisitor.getExpressionPrettifier(), argResult.expression, result.getType(), fun));
return null;
}
return result;
}
if (expr.getArguments().size() == 1) {
SingleDependentLink param = new TypedSingleDependentLink(true, "x", Fin(argResult.expression));
return new TypecheckingResult(new LamExpression(Sort.SET0, param, Suc(new ReferenceExpression(param))), new PiExpression(Sort.SET0, param, Fin(Suc(argResult.expression))));
}
TypecheckingResult arg2Result = myVisitor.checkExpr(expr.getArguments().get(1).getExpression(), Fin(argResult.expression));
if (arg2Result == null) {
return null;
}
result = new TypecheckingResult(Suc(arg2Result.expression), Fin(Suc(argResult.expression)));
if (expr.getArguments().size() > 2) {
myVisitor.getErrorReporter().report(new NotPiType(myVisitor.getExpressionPrettifier(), arg2Result.expression, result.getType(), fun));
return null;
}
return result;
}
result = myVisitor.visitReference(refExpr);
} else if (fun instanceof Concrete.GoalExpression) {
List<TypecheckingResult> argumentResults = new ArrayList<>();
for (Concrete.Argument argument : expr.getArguments()) {
var typecheckedArgument = myVisitor.checkExpr(argument.expression, null);
if (typecheckedArgument != null) {
TypecheckingResult normalized = typecheckedArgument.normalizeType();
argumentResults.add(normalized);
}
}
Expression expectedGoalType = null;
if (expectedType != null && argumentResults.size() == expr.getArguments().size()) {
expectedGoalType = generatePiExpressionByArguments(expectedType, argumentResults, expr.getArguments(), fun);
}
TypecheckingResult goalCheckingResult = myVisitor.checkExpr(fun, expectedGoalType);
Expression appExpr;
if (argumentResults.size() == expr.getArguments().size()) {
appExpr = generateAppExpressionByArguments(goalCheckingResult.expression, argumentResults, expr.getArguments());
} else {
appExpr = goalCheckingResult.expression;
}
return new TypecheckingResult(appExpr, expectedType != null && !(expectedType instanceof Type && ((Type) expectedType).isOmega()) ? expectedType : goalCheckingResult.expression);
} else {
result = myVisitor.checkExpr(fun, null);
}
if (result == null) {
for (Concrete.Argument argument : expr.getArguments()) {
myVisitor.checkExpr(argument.expression, null);
}
return null;
}
if (result instanceof DefCallResult defCallResult && expr.getArguments().get(0).isExplicit() && expectedType != null && defCallResult.getDefinition() instanceof Constructor && defCallResult.getArguments().size() < DependentLink.Helper.size(((Constructor) defCallResult.getDefinition()).getDataTypeParameters())) {
DataCallExpression dataCall = TypeConstructorExpression.unfoldType(expectedType).cast(DataCallExpression.class);
if (dataCall != null) {
if (((Constructor) defCallResult.getDefinition()).getDataType() != dataCall.getDefinition()) {
myVisitor.getErrorReporter().report(new TypeMismatchError(dataCall, refDoc(((Constructor) defCallResult.getDefinition()).getDataType().getReferable()), fun));
return null;
}
List<? extends Expression> args = dataCall.getDefCallArguments();
List<Expression> args1 = new ArrayList<>(args.size());
args1.addAll(defCallResult.getArguments());
args1.addAll(args.subList(defCallResult.getArguments().size(), args.size()));
args1 = ((Constructor) defCallResult.getDefinition()).matchDataTypeArguments(args1);
if (args1 != null) {
boolean ok = dataCall.getLevels().compare(defCallResult.getLevels(), CMP.LE, myVisitor.getEquations(), fun);
if (ok && !defCallResult.getArguments().isEmpty()) {
ok = new CompareVisitor(myVisitor.getEquations(), CMP.LE, fun).compareLists(defCallResult.getArguments(), dataCall.getDefCallArguments().subList(0, defCallResult.getArguments().size()), dataCall.getDefinition().getParameters(), dataCall.getDefinition(), new ExprSubstitution());
}
if (!ok) {
myVisitor.getErrorReporter().report(new TypeMismatchError(dataCall, DataCallExpression.make(dataCall.getDefinition(), defCallResult.getLevels(), args1), fun));
return null;
}
if (!args1.isEmpty()) {
result = ((DefCallResult) result).applyExpressions(args1);
}
}
}
}
DefCallResult defCallResult = result instanceof DefCallResult ? (DefCallResult) result : null;
Definition definition = defCallResult != null ? defCallResult.getDefinition() : null;
List<Concrete.Argument> arguments = expr.getArguments();
if ((definition == Prelude.EMPTY_ARRAY || definition == Prelude.ARRAY_CONS) && defCallResult != null && defCallResult.getArguments().isEmpty()) {
return checkArrayCons(defCallResult, arguments, expectedType, fun);
}
List<Integer> order = definition != null ? definition.getParametersTypecheckingOrder() : null;
if (order != null) {
int skip = ((DefCallResult) result).getArguments().size();
if (skip > 0) {
List<Integer> newOrder = new ArrayList<>();
for (Integer index : order) {
if (index >= skip) {
newOrder.add(index - skip);
}
}
boolean trivial = true;
for (int i = 0; i < newOrder.size(); i++) {
if (i != newOrder.get(i)) {
trivial = false;
break;
}
}
order = trivial ? null : newOrder;
}
}
if (order != null) {
int current = 0; // Position in arguments
int numberOfImplicitArguments = 0; // Number of arguments not present in arguments
Map<Integer,Pair<InferenceVariable,Concrete.Expression>> deferredArguments = new LinkedHashMap<>();
for (Integer i : order) {
if (i == -1) {
Expression expectedType1 = dropPiParameters(definition, arguments, expectedType);
if (expectedType1 != null) {
new CompareVisitor(myVisitor.getEquations(), CMP.LE, expr).compare(result.getType(), expectedType1, Type.OMEGA, false);
}
continue;
}
// Defer arguments up to i
while (current < arguments.size()) {
DependentLink parameter = result.getParameter();
if (!parameter.hasNext()) {
break;
}
if (!parameter.isExplicit() && arguments.get(current).isExplicit()) {
List<? extends DependentLink> implicitParameters = result.getImplicitParameters();
result = fixImplicitArgs(result, implicitParameters, fun, false, null);
parameter = result.getParameter();
numberOfImplicitArguments += implicitParameters.size();
}
if (current + numberOfImplicitArguments >= i) {
break;
}
Concrete.Argument argument = arguments.get(current);
if (parameter.isExplicit() != argument.isExplicit()) {
myVisitor.getErrorReporter().report(new ArgumentExplicitnessError(parameter.isExplicit(), argument.getExpression()));
return null;
}
InferenceVariable var = new ExpressionInferenceVariable(parameter.getTypeExpr(), argument.getExpression(), myVisitor.getAllBindings(), false);
deferredArguments.put(current + numberOfImplicitArguments, new Pair<>(var, argument.getExpression()));
result = result.applyExpression(new InferenceReferenceExpression(var), parameter.isExplicit(), myVisitor, fun);
current++;
}
if (i == current + numberOfImplicitArguments) {
// If we are at i-th argument, simply typecheck it
if (current >= arguments.size()) {
break;
}
Concrete.Argument argument = arguments.get(current);
result = inferArg(result, argument.expression, argument.isExplicit(), fun);
if (result == null) {
return null;
}
current++;
} else {
// If i-th argument were deferred, get it from the map and typecheck
Pair<InferenceVariable, Concrete.Expression> pair = deferredArguments.remove(i);
if (pair != null) {
typecheckDeferredArgument(pair, result);
}
}
}
// Typecheck all deferred arguments
for (Pair<InferenceVariable, Concrete.Expression> pair : deferredArguments.values()) {
typecheckDeferredArgument(pair, result);
}
// Typecheck the rest of the arguments
for (; current < arguments.size(); current++) {
result = inferArg(result, arguments.get(current).expression, arguments.get(current).isExplicit(), fun);
}
} else {
if (result instanceof DefCallResult && ((DefCallResult) result).getDefinition() instanceof ClassField && (arguments.isEmpty() || arguments.get(0).isExplicit())) {
arguments = new ArrayList<>(expr.getArguments().size() + 1);
arguments.add(new Concrete.Argument(new Concrete.HoleExpression(fun.getData()), false));
arguments.addAll(expr.getArguments());
}
int i = 0;
if (expectedType != null && expectedType.getStuckInferenceVariable() == null) {
for (; i < arguments.size(); i++) {
Concrete.Argument argument = arguments.get(i);
if (result instanceof TypecheckingResult && argument.isExplicit()) {
DependentLink param = result.getParameter();
if (param.hasNext() && !param.isExplicit()) {
break;
}
}
result = inferArg(result, argument.expression, argument.isExplicit(), fun);
}
if (result == null || i == arguments.size()) {
return result;
}
Pair<Expression, Integer> pair = normalizePi(arguments, i, result.getType());
((TypecheckingResult) result).type = pair.proj1;
for (; i < pair.proj2; i++) {
Concrete.Argument argument = arguments.get(i);
result = inferArg(result, argument.expression, argument.isExplicit(), fun);
}
if (result == null) {
return null;
}
if (i < arguments.size()) {
result = fixImplicitArgs(result, result.getImplicitParameters(), fun, false, null);
Expression actualType = dropPiParameters(result.getType(), arguments, i);
if (actualType != null) {
new CompareVisitor(myVisitor.getEquations(), CMP.LE, fun).compare(actualType, expectedType, Type.OMEGA, false);
}
}
}
for (; i < arguments.size(); i++) {
Concrete.Argument argument = arguments.get(i);
result = inferArg(result, argument.expression, argument.isExplicit(), fun);
}
}
return result;
}