public Result visitApp()

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;
  }