public TypecheckingResult visitNew()

in base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java [1660:1771]


  public TypecheckingResult visitNew(Concrete.NewExpression expr, Expression expectedType) {
    if (expr.getExpression() instanceof Concrete.ClassExtExpression classExt) {
      Concrete.Expression baseClassExpr = classExt.getBaseClassExpression();
      if (baseClassExpr instanceof Concrete.AppExpression) {
        baseClassExpr = ((Concrete.AppExpression) baseClassExpr).getFunction();
      }
      if (baseClassExpr instanceof Concrete.ReferenceExpression && ((Concrete.ReferenceExpression) baseClassExpr).getReferent() instanceof MetaReferable && ((MetaReferable) ((Concrete.ReferenceExpression) baseClassExpr).getReferent()).getDefinition() == null) {
        return makeNew(checkMeta((Concrete.ReferenceExpression) baseClassExpr, classExt.getBaseClassExpression() instanceof Concrete.AppExpression ? ((Concrete.AppExpression) classExt.getBaseClassExpression()).getArguments() : Collections.emptyList(), classExt.getCoclauses(), null), expr, expectedType, Collections.emptySet());
      }
    }

    TypecheckingResult exprResult = null;
    Set<ClassField> pseudoImplemented = Collections.emptySet();
    Concrete.Expression classExpr = desugarClassApp(expr.getExpression() instanceof Concrete.ClassExtExpression ? ((Concrete.ClassExtExpression) expr.getExpression()).getBaseClassExpression() : expr.getExpression(), !(expr.getExpression() instanceof Concrete.ClassExtExpression), Collections.emptySet());
    boolean isClassExtOrRef = classExpr instanceof Concrete.ClassExtExpression || classExpr instanceof Concrete.ReferenceExpression;
    if (expr.getExpression() instanceof Concrete.ClassExtExpression) {
      if (classExpr instanceof Concrete.ClassExtExpression) {
        ((Concrete.ClassExtExpression) classExpr).getStatements().addAll(((Concrete.ClassExtExpression) expr.getExpression()).getStatements());
      } else {
        classExpr = expr.getExpression();
      }
    }
    if (isClassExtOrRef) {
      Expression unfoldedType = expectedType == null ? null : TypeConstructorExpression.unfoldType(expectedType);
      Concrete.Expression baseExpr = classExpr instanceof Concrete.ClassExtExpression ? ((Concrete.ClassExtExpression) classExpr).getBaseClassExpression() : classExpr;
      Definition actualDef = unfoldedType instanceof ClassCallExpression && baseExpr instanceof Concrete.ReferenceExpression && ((Concrete.ReferenceExpression) baseExpr).getReferent() instanceof TCDefReferable ? ((TCDefReferable) ((Concrete.ReferenceExpression) baseExpr).getReferent()).getTypechecked() : null;
      if (baseExpr instanceof Concrete.HoleExpression || actualDef instanceof ClassDefinition) {
        ClassCallExpression actualClassCall = null;
        if (baseExpr instanceof Concrete.HoleExpression && !(unfoldedType instanceof ClassCallExpression)) {
          errorReporter.report(new TypecheckingError("Cannot infer an expression", baseExpr));
          return null;
        }

        ClassCallExpression expectedClassCall = (ClassCallExpression) unfoldedType;
        if (baseExpr instanceof Concrete.ReferenceExpression baseRefExpr) {
          ClassDefinition actualClass = (ClassDefinition) actualDef;
          boolean ok = actualClass.isSubClassOf(expectedClassCall.getDefinition());
          if (ok && (actualDef != expectedClassCall.getDefinition() || baseRefExpr.getPLevels() != null || baseRefExpr.getHLevels() != null)) {
            boolean fieldsOK = true;
            for (ClassField implField : expectedClassCall.getImplementedHere().keySet()) {
              if (actualClass.isImplemented(implField)) {
                fieldsOK = false;
                break;
              }
            }
            Levels levels = typecheckLevels(actualDef, baseRefExpr, actualDef.generateInferVars(myEquations, expr), false);
            actualClassCall = new ClassCallExpression(actualClass, levels, new LinkedHashMap<>(), expectedClassCall.getSort(), actualDef.getUniverseKind());
            // It's probably better to use CMP.LE here, but then we need to check that copied implementations fit into their types with new levels.
            if (!actualClass.castLevels(expectedClassCall.getDefinition(), levels).compare(expectedClassCall.getLevels(), CMP.EQ, myEquations, expr)) {
              errorReporter.report(new TypeMismatchWithSubexprError(new CompareVisitor.Result(actualClassCall, expectedClassCall, actualClassCall, expectedClassCall, actualClassCall.getLevels(), expectedClassCall.getLevels()), expr));
              fieldsOK = false;
            }
            if (fieldsOK) {
              copyImplementationsFrom(actualClassCall, expectedClassCall, expr);
            }
          }
          if (!ok) {
            errorReporter.report(new TypeMismatchError(unfoldedType, baseExpr, baseExpr));
            return null;
          }
        }

        if (actualClassCall != null) {
          expectedClassCall = actualClassCall;
          expectedClassCall.updateHasUniverses();
        }
        pseudoImplemented = new HashSet<>();
        exprResult = typecheckClassExt(classExpr instanceof Concrete.ClassExtExpression ? ((Concrete.ClassExtExpression) classExpr).getStatements() : Collections.emptyList(), null, expectedClassCall, pseudoImplemented, classExpr, true);
        if (exprResult == null) {
          return null;
        }
      }
    }

    Expression renewExpr = null;
    if (exprResult == null) {
      Concrete.Expression baseClassExpr;
      List<Concrete.ClassFieldImpl> classFieldImpls;
      if (classExpr instanceof Concrete.ClassExtExpression) {
        baseClassExpr = ((Concrete.ClassExtExpression) classExpr).getBaseClassExpression();
        classFieldImpls = ((Concrete.ClassExtExpression) classExpr).getStatements();
      } else {
        baseClassExpr = classExpr;
        classFieldImpls = Collections.emptyList();
      }

      TypecheckingResult typeCheckedBaseClass = baseClassExpr instanceof Concrete.ReferenceExpression && ((Concrete.ReferenceExpression) baseClassExpr).getReferent() == Prelude.DEP_ARRAY.getRef()
        ? tResultToResult(null, visitReference((Concrete.ReferenceExpression) baseClassExpr, true), baseClassExpr)
        : baseClassExpr instanceof Concrete.ReferenceExpression
          ? visitReference((Concrete.ReferenceExpression) baseClassExpr, null, false)
          : baseClassExpr instanceof Concrete.AppExpression
            ? visitApp((Concrete.AppExpression) baseClassExpr, null, false)
            : checkExpr(baseClassExpr, null);
      if (typeCheckedBaseClass == null) {
        return null;
      }

      ClassCallExpression classCall = TypeConstructorExpression.unfoldType(typeCheckedBaseClass.expression).cast(ClassCallExpression.class);
      if (classCall == null) {
        classCall = TypeConstructorExpression.unfoldType(typeCheckedBaseClass.type).cast(ClassCallExpression.class);
        if (classCall == null) {
          errorReporter.report(new TypecheckingError("Expected a class or a class instance", baseClassExpr));
          return null;
        }
        renewExpr = typeCheckedBaseClass.expression;
      }

      exprResult = typecheckClassExt(classFieldImpls, null, renewExpr, classCall, null, baseClassExpr, true);
    }

    return makeNew(exprResult, expr, expectedType, pseudoImplemented);
  }