private TResult inferArg()

in base/src/main/java/org/arend/typechecking/implicitargs/StdImplicitArgsInference.java [160:275]
107 lines of code
40 McCabe index (conditional complexity)

  private TResult inferArg(TResult result, Concrete.Expression arg, boolean isExplicit, Concrete.Expression fun) {
    if (result == null) {
      myVisitor.checkExpr(arg, null);
      return null;
    }
    if (arg == null || result instanceof TypecheckingResult && ((TypecheckingResult) result).expression.reportIfError(myVisitor.getErrorReporter(), fun)) {
      myVisitor.checkArgument(arg, null, result, null);
      return result;
    }

    if (isExplicit) {
      if (result instanceof DefCallResult defCallResult && ((DefCallResult) result).getDefinition() == Prelude.PATH_CON) {
        SingleDependentLink lamParam = new TypedSingleDependentLink(true, "i", Interval());
        Sort sort0 = Sort.STD.subst(defCallResult.getLevels().toLevelPair());
        Sort sort = sort0.succ();
        TypecheckingResult argResult;
        if (defCallResult.getArguments().isEmpty()) {
          Expression binding = InferenceReferenceExpression.make(new FunctionInferenceVariable(Prelude.PATH_CON, Prelude.PATH_CON.getDataTypeParameters(), 1, new UniverseExpression(sort0), fun, myVisitor.getAllBindings()), myVisitor.getEquations());
          result = result.applyExpression(new LamExpression(sort, lamParam, binding), true, myVisitor, fun);
          argResult = myVisitor.checkArgument(arg, new PiExpression(sort, lamParam, binding), result, null);
        } else {
          argResult = myVisitor.checkArgument(arg, new PiExpression(sort, lamParam, AppExpression.make(defCallResult.getArguments().get(0), new ReferenceExpression(lamParam), true)), result, null);
        }
        return argResult == null ? null : ((DefCallResult) result).applyPathArgument(argResult.expression, myVisitor, arg);
      }

      result = fixImplicitArgs(result, result.getImplicitParameters(), fun, false, null);
    }

    DependentLink param = result.getParameter();
    if (!param.hasNext() && result instanceof TypecheckingResult) {
      TResult coercedResult = CheckTypeVisitor.coerceFromType((TypecheckingResult) result);
      if (coercedResult != null) {
        result = coercedResult;
        if (isExplicit) {
          result = fixImplicitArgs(result, result.getImplicitParameters(), fun, false, null);
        }
        param = result.getParameter();
      }
      if (!param.hasNext()) {
        TypecheckingResult tcResult = ((TypecheckingResult) result).normalizeType();
        result = tcResult;
        if (tcResult.type instanceof DataCallExpression && ((DataCallExpression) tcResult.type).getDefinition() == Prelude.PATH) {
          List<Expression> args = ((DataCallExpression) tcResult.type).getDefCallArguments();
          result = DefCallResult.makeTResult(new Concrete.ReferenceExpression(fun.getData(), Prelude.AT.getRef()), Prelude.AT, ((DataCallExpression) tcResult.type).getLevels())
            .applyExpression(args.get(0), false, myVisitor, fun)
            .applyExpression(args.get(1), false, myVisitor, fun)
            .applyExpression(args.get(2), false, myVisitor, fun)
            .applyExpression(tcResult.expression, true, myVisitor, fun);
          param = result.getParameter();
        } else {
          coercedResult = CoerceData.coerceToKey(tcResult, new CoerceData.PiKey(), fun, myVisitor);
          if (coercedResult != null) {
            result = coercedResult;
            if (isExplicit) {
              result = fixImplicitArgs(result, result.getImplicitParameters(), fun, false, null);
            }
            param = result.getParameter();
          }
        }
      }
    }
    if (arg instanceof Concrete.HoleExpression && param.hasNext()) {
      if (!isExplicit && param.isExplicit()) {
        myVisitor.getErrorReporter().report(new ArgumentExplicitnessError(true, arg));
      }
      return fixImplicitArgs(result, Collections.singletonList(param), fun, false, arg instanceof RecursiveInstanceHoleExpression ? (RecursiveInstanceHoleExpression) arg : null);
    }

    TypecheckingResult argResult = myVisitor.checkArgument(arg, param.hasNext() ? param.getTypeExpr() : null, result, null);
    if (argResult == null) {
      return null;
    }

    if (!param.hasNext()) {
      TypecheckingResult result1 = result.toResult(myVisitor);
      if (!result1.type.reportIfError(myVisitor.getErrorReporter(), fun)) {
        myVisitor.getErrorReporter().report(new NotPiType(myVisitor.getExpressionPrettifier(), argResult.expression, result1.type, fun));
      }
      return null;
    }

    if (param.isExplicit() != isExplicit) {
      myVisitor.getErrorReporter().report(new ArgumentExplicitnessError(param.isExplicit(), arg));
      return null;
    }

    if (result instanceof DefCallResult defCallResult && !isExplicit && ((DefCallResult) result).getDefinition() instanceof ClassField) {
      ClassField field = (ClassField) defCallResult.getDefinition();
      ClassCallExpression classCall = argResult.type.normalize(NormalizationMode.WHNF).cast(ClassCallExpression.class);
      PiExpression piType = null;
      if (classCall != null) {
        piType = classCall.getDefinition().getOverriddenType(field, classCall.getLevels());
        if (piType != null) {
          ClassCallExpression expectedClassCall = new ClassCallExpression(field.getParentClass(), defCallResult.getLevels());
          if (!CompareVisitor.compare(myVisitor.getEquations(), CMP.LE, classCall, expectedClassCall, Type.OMEGA, arg)) {
            myVisitor.getErrorReporter().report(new TypeMismatchError(expectedClassCall, classCall, arg));
            return null;
          }
        }
      }
      if (piType == null) {
        piType = field.getType(defCallResult.getLevels());
      }
      return new TypecheckingResult(FieldCallExpression.make(field, argResult.expression), piType.applyExpression(argResult.expression));
    }

    if (result instanceof DefCallResult && ((DefCallResult) result).getDefinition() == Prelude.SUC) {
      Expression type = argResult.type.normalize(NormalizationMode.WHNF);
      if (type instanceof DataCallExpression && ((DataCallExpression) type).getDefinition() == Prelude.FIN) {
        return new TypecheckingResult(Suc(argResult.expression), DataCallExpression.make(Prelude.FIN, ((DataCallExpression) type).getLevels(), new SingletonList<>(Suc(((DataCallExpression) type).getDefCallArguments().get(0)))));
      }
    }

    return result.applyExpression(argResult.expression, isExplicit, myVisitor, fun);
  }