in meta/src/main/java/org/arend/lib/meta/cong/CongVisitor.java [343:384]
public Result visitApp(@NotNull CoreAppExpression expr, ParamType parameter) {
CoreExpression other = parameter.other.getUnderlyingExpression();
if (!(other instanceof CoreAppExpression)) {
return visit(expr, parameter);
}
List<CoreExpression> args1 = new ArrayList<>();
List<CoreExpression> args2 = new ArrayList<>();
CoreExpression expr1 = expr;
CoreExpression expr2 = other;
while (expr1 instanceof CoreAppExpression && expr2 instanceof CoreAppExpression) {
args1.add(((CoreAppExpression) expr1).getArgument());
args2.add(((CoreAppExpression) expr2).getArgument());
expr1 = ((CoreAppExpression) expr1).getFunction();
expr2 = ((CoreAppExpression) expr2).getFunction();
}
if (!typechecker.compare(expr1, expr2, CMP.EQ, marker, false, true, true)) {
return visit(expr, parameter);
}
CoreExpression type = expr1.computeType().normalize(NormalizationMode.WHNF);
List<CoreParameter> parameters = new ArrayList<>();
int s = 0;
while (type instanceof CorePiExpression) {
CoreParameter params = ((CorePiExpression) type).getParameters();
parameters.add(params);
s += Utils.parametersSize(params);
if (s >= args1.size()) break;
type = ((CorePiExpression) type).getCodomain();
}
if (s < args1.size()) {
return visit(expr, parameter);
}
Collections.reverse(args1);
Collections.reverse(args2);
List<ConcreteArgument> args = new ArrayList<>();
boolean abstracted = visitArgs(args1, args2, parameters, true, args);
return args.size() == args1.size() ? new Result(abstracted ? factory.app(factory.core(expr1.computeTyped()), args) : null) : null;
}