public static ParametersLevel typecheckLevel()

in base/src/main/java/org/arend/typechecking/UseTypechecking.java [135:248]
108 lines of code
54 McCabe index (conditional complexity)

  public static ParametersLevel typecheckLevel(Concrete.UseDefinition def, FunctionDefinition typedDef, Definition useParent, ErrorReporter errorReporter) {
    if (!(useParent instanceof DataDefinition || useParent instanceof ClassDefinition || useParent instanceof FunctionDefinition)) {
      return null;
    }

    Expression resultType = def == null || def.getResultType() != null ? typedDef.getResultType() : null;
    boolean ok = true;
    List<ClassField> levelFields = null;
    List<Pair<ClassDefinition, Set<ClassField>>> strictList = null;
    Expression type = null;
    DependentLink parameters = null;
    DependentLink link = typedDef.getParameters();
    if (useParent instanceof DataDefinition || useParent instanceof FunctionDefinition) {
      ExprSubstitution substitution = new ExprSubstitution();
      List<Expression> defCallArgs = new ArrayList<>();
      for (DependentLink defLink = useParent.getParameters(); defLink.hasNext(); defLink = defLink.getNext(), link = link.getNext()) {
        if (!link.hasNext()) {
          ok = false;
          break;
        }
        if (!Expression.compare(link.getTypeExpr(), defLink.getTypeExpr().subst(substitution), Type.OMEGA, CMP.EQ)) {
          if (parameters == null) {
            parameters = DependentLink.Helper.take(typedDef.getParameters(), DependentLink.Helper.size(defLink));
          }
        }
        ReferenceExpression refExpr = new ReferenceExpression(link);
        defCallArgs.add(refExpr);
        substitution.add(defLink, refExpr);
      }

      if (ok) {
        if (link.hasNext() || resultType != null) {
          type = useParent instanceof DataDefinition
            ? DataCallExpression.make((DataDefinition) useParent, useParent.makeIdLevels(), defCallArgs)
            : FunCallExpression.make((FunctionDefinition) useParent, useParent.makeIdLevels(), defCallArgs);
        } else {
          ok = false;
        }
      }
    } else {
      ClassCallExpression classCall = null;
      DependentLink classCallLink = link;
      for (; classCallLink.hasNext(); classCallLink = classCallLink.getNext()) {
        classCallLink = classCallLink.getNextTyped(null);
        classCall = classCallLink.getTypeExpr().cast(ClassCallExpression.class);
        if (classCall != null && classCall.getDefinition() == useParent && (classCall.getUniverseKind() == UniverseKind.NO_UNIVERSES || typedDef.isIdLevels(classCall.getLevels()))) {
          break;
        }
      }
      if (!classCallLink.hasNext() && resultType != null) {
        PiExpression piType = resultType.normalize(NormalizationMode.WHNF).cast(PiExpression.class);
        if (piType != null) {
          classCall = piType.getParameters().getTypeExpr().normalize(NormalizationMode.WHNF).cast(ClassCallExpression.class);
          if (classCall != null && classCall.getDefinition() == useParent && (classCall.getUniverseKind() == UniverseKind.NO_UNIVERSES || typedDef.isIdLevels(classCall.getLevels()))) {
            classCallLink = piType.getParameters();
          }
        }
      }

      if (classCall == null || !classCallLink.hasNext()) {
        ok = false;
      } else {
        if (!classCall.getImplementedHere().isEmpty()) {
          levelFields = new ArrayList<>();
          strictList = new ArrayList<>();
          Expression thisExpr = new ReferenceExpression(classCallLink);
          for (Map.Entry<ClassField, Expression> entry : classCall.getImplementedHere().entrySet()) {
            ClassField classField = entry.getKey();
            if (classField.isProperty()) {
              continue;
            }
            if (!(link.hasNext() && entry.getValue() instanceof ReferenceExpression && ((ReferenceExpression) entry.getValue()).getBinding() == link)) {
              ok = false;
              break;
            }
            levelFields.add(classField);
            Expression fieldType = classCall.getDefinition().getFieldType(classField, classCall.getLevels(classField.getParentClass()), thisExpr);
            Expression paramType = link.getTypeExpr();
            if (!Expression.compare(fieldType, paramType, Type.OMEGA, CMP.EQ)) {
              if (parameters == null) {
                int numberOfClassParameters = 0;
                for (DependentLink link1 = link; link1 != classCallLink && link1.hasNext(); link1 = link1.getNext()) {
                  numberOfClassParameters++;
                }
                parameters = DependentLink.Helper.take(typedDef.getParameters(), numberOfClassParameters);
              }

              ClassCallExpression fieldClassCall = fieldType.cast(ClassCallExpression.class);
              ClassCallExpression paramClassCall = paramType.cast(ClassCallExpression.class);
              if (strictList != null && paramClassCall != null && fieldClassCall != null && paramClassCall.getDefinition().isSubClassOf(fieldClassCall.getDefinition()) && paramClassCall.getLevels(fieldClassCall.getDefinition()).equals(fieldClassCall.getLevels()) && paramClassCall.getUniverseKind().ordinal() <= fieldClassCall.getUniverseKind().ordinal()) {
                strictList.add(new Pair<>(paramClassCall.getDefinition(), paramClassCall.getImplementedHere().keySet()));
              } else {
                strictList = null;
              }
            } else if (strictList != null) {
              strictList.add(null);
            }
            link = link.getNext();
          }
        }
        type = classCall;
      }
    }

    Integer level = CheckTypeVisitor.getExpressionLevel(link, resultType, ok ? type : null, DummyEquations.getInstance(), def, errorReporter);
    if (level == null) {
      return null;
    }
    if (def != null && useParent instanceof DataDefinition && parameters == null && Level.compare(((DataDefinition) useParent).getSort().getHLevel(), new Level(level), CMP.LE, DummyEquations.getInstance(), def)) {
      errorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.USELESS_LEVEL, def));
    }

    return useParent instanceof ClassDefinition ? new ClassDefinition.ParametersLevel(parameters, level, levelFields, strictList) : new ParametersLevel(parameters, level);
  }