private TypecheckingResult visitApp()

in base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java [3371:3452]
74 lines of code
50 McCabe index (conditional complexity)

  private TypecheckingResult visitApp(Concrete.AppExpression expr, Expression expectedType, boolean inferTailImplicits) {
    if (expr.getFunction() instanceof Concrete.ReferenceExpression refExpr && refExpr.getReferent() instanceof TCDefReferable && ((TCDefReferable) refExpr.getReferent()).getTypechecked() instanceof ClassDefinition) {
      List<SingleDependentLink> params = expectedType == null ? null : new ArrayList<>();
      if (expectedType != null) {
        expectedType = expectedType.normalizePi(params);
      }
      Concrete.Expression dExpr = desugarClassApp(refExpr, expr.getArguments(), expr, params, inferTailImplicits, Collections.emptySet());
      if (dExpr != expr) {
        return checkExpr(dExpr, expectedType);
      }
    }

    if (expr.getFunction() instanceof Concrete.ReferenceExpression && ((Concrete.ReferenceExpression) expr.getFunction()).getReferent() instanceof MetaReferable) {
      return checkMeta((Concrete.ReferenceExpression) expr.getFunction(), expr.getArguments(), null, expectedType);
    }

    Referable referable = expr.getFunction() instanceof Concrete.ReferenceExpression ? ((Concrete.ReferenceExpression) expr.getFunction()).getReferent() : null;
    Definition definition = referable instanceof TCDefReferable ? ((TCDefReferable) referable).getTypechecked() : null;
    if ((definition == Prelude.MOD || definition == Prelude.DIV_MOD) && expr.getArguments().size() == 2 && expr.getArguments().get(0).isExplicit() && expr.getArguments().get(1).isExplicit()) {
      TypecheckingResult arg1 = checkExpr(expr.getArguments().get(0).getExpression(), ExpressionFactory.Nat());
      TypecheckingResult arg2 = checkExpr(expr.getArguments().get(1).getExpression(), ExpressionFactory.Nat());
      if (arg1 == null || arg2 == null) {
        return null;
      }

      Type type;
      IntegerExpression intExpr = arg2.expression.cast(IntegerExpression.class);
      ConCallExpression conCall = arg2.expression.cast(ConCallExpression.class);
      if (intExpr != null && !intExpr.isZero() || conCall != null && conCall.getDefinition() == Prelude.SUC) {
        type = ExpressionFactory.Fin(arg2.expression);
      } else {
        type = ExpressionFactory.Nat();
      }

      boolean isMod = definition == Prelude.MOD;
      if (!isMod) {
        type = ExpressionFactory.divModType(type);
      }
      return checkResult(expectedType, new TypecheckingResult(FunCallExpression.make(isMod ? Prelude.MOD : Prelude.DIV_MOD, Levels.EMPTY, Arrays.asList(arg1.expression, arg2.expression)), type.getExpr()), expr);
    }

    if (expectedType != null && (definition == Prelude.ARRAY_AT && expr.getNumberOfExplicitArguments() == 0 || definition == Prelude.ARRAY_INDEX && expr.getNumberOfExplicitArguments() == 1 || definition == Prelude.ARRAY_CONS && expr.getNumberOfExplicitArguments() == 2)) {
      PiExpression piExpr = TypeConstructorExpression.unfoldType(expectedType).cast(PiExpression.class);
      if (piExpr != null && piExpr.getParameters().isExplicit()) {
        Referable lamParam = new LocalReferable("a");
        return visitLam(new Concrete.LamExpression(expr.getData(), Collections.singletonList(new Concrete.NameParameter(expr.getData(), true, lamParam)), Concrete.AppExpression.make(expr.getData(), expr, new Concrete.ReferenceExpression(expr.getData(), lamParam), true)), expectedType);
      }
    }

    TResult result = myArgsInference.infer(expr, expectedType);
    if (result == null || !checkPath(result, expr)) {
      return null;
    }

    if (definition instanceof DataDefinition || definition == Prelude.PATH_INFIX) {
      List<? extends Expression> args = null;
      if (result instanceof DefCallResult) {
        args = ((DefCallResult) result).getArguments();
      } else if (result instanceof TypecheckingResult) {
        Expression resultExpr = ((TypecheckingResult) result).expression;
        while (resultExpr instanceof AppExpression) {
          resultExpr = resultExpr.getFunction();
        }
        if (resultExpr instanceof DefCallExpression) {
          args = ((DefCallExpression) resultExpr).getDefCallArguments();
        }
      }
      if (args != null) {
        DataDefinition dataDef = definition instanceof DataDefinition ? (DataDefinition) definition : Prelude.PATH;
        for (int i = 0; i < args.size(); i++) {
          if (args.get(i) instanceof InferenceReferenceExpression && ((InferenceReferenceExpression) args.get(i)).getVariable() != null && dataDef.isCovariant(i)) {
            myEquations.solveLowerBounds(((InferenceReferenceExpression) args.get(i)).getVariable());
          }
        }
      }
    }

    if (result instanceof TypecheckingResult tcResult && tcResult.expression instanceof DefCallExpression && !(tcResult.expression instanceof FieldCallExpression)) {
      return checkResult(expectedType, tcResult, expr);
    }
    return tResultToResult(expectedType, result, expr);
  }