private boolean typecheckFunctionHeader()

in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [1072:1212]
129 lines of code
63 McCabe index (conditional complexity)

  private boolean typecheckFunctionHeader(FunctionDefinition typedDef, Concrete.BaseFunctionDefinition def, LocalInstancePool localInstancePool) {
    def.getData().setTypecheckedIfNotCancelled(typedDef);
    if (myNewDef) {
      typedDef.setParametersOriginalDefinitions(def.getParametersOriginalDefinitions());
    }
    if (def.enclosingClass != null) {
      typedDef.setHasEnclosingClass(true);
    }
    ClassField implementedField = def instanceof Concrete.CoClauseFunctionDefinition ? typechecker.referableToClassField(((Concrete.CoClauseFunctionDefinition) def).getImplementedField(), def) : null;
    FunctionKind kind = implementedField == null ? def.getKind() : implementedField.isProperty() && implementedField.getTypeLevel() == null ? FunctionKind.LEMMA : FunctionKind.FUNC;
    checkFunctionLevel(def, kind);

    if (def.isRecursive() && def.getResultType() == null && !(def.getBody() instanceof Concrete.ElimFunctionBody)) {
      errorReporter.report(new TypecheckingError("The type of a recursive function must be specified explictly", def));
    }

    if (def.getKind() == FunctionKind.LEVEL) {
      Definition useParent = def.getUseParent().getTypechecked();
      if (def.getPLevelParameters() == null && useParent.hasNonTrivialPLevelParameters()) {
        def.setPLevelParameters(Concrete.LevelParameters.makeLevelParameters(useParent.getLevelParameters().subList(0, useParent.getNumberOfPLevelParameters()), true));
      }
      if (def.getHLevelParameters() == null && useParent.hasNonTrivialHLevelParameters()) {
        def.setHLevelParameters(Concrete.LevelParameters.makeLevelParameters(useParent.getLevelParameters().subList(useParent.getNumberOfPLevelParameters(), useParent.getLevelParameters().size()), false));
      }
    }

    if (myNewDef) {
      if (def.getKind() == FunctionKind.CLASS_COCLAUSE) {
        Definition enclosingClass = def.enclosingClass.getTypechecked();
        List<? extends LevelVariable> params = enclosingClass.getLevelParameters();
        if (params != null) {
          if (typedDef.getLevelParameters() == null) {
            int n = enclosingClass.getNumberOfPLevelParameters();
            Concrete.LevelParameters pLevelParams = levelVariablesToParameters(def.getData(), enclosingClass.getLevelParameters().subList(0, n), true);
            Concrete.LevelParameters hLevelParams = levelVariablesToParameters(def.getData(), enclosingClass.getLevelParameters().subList(n, enclosingClass.getLevelParameters().size()), false);
            def.setPLevelParameters(pLevelParams);
            def.setHLevelParameters(hLevelParams);
            if (!def.getParameters().isEmpty()) {
              Concrete.Expression type = def.getParameters().get(0).getType();
              if (type instanceof Concrete.ClassExtExpression) {
                type = ((Concrete.ClassExtExpression) type).getBaseClassExpression();
              }
              if (type instanceof Concrete.ReferenceExpression refExpr) {
                if (pLevelParams != null) {
                  refExpr.setPLevels(levelParametersToExpressions(refExpr.getData(), pLevelParams, LevelVariable.LvlType.PLVL));
                }
                if (hLevelParams != null) {
                  refExpr.setHLevels(levelParametersToExpressions(refExpr.getData(), hLevelParams, LevelVariable.LvlType.HLVL));
                }
              }
            }
            typedDef.setLevelParameters(typecheckLevelParameters(def));
            typedDef.setPLevelsParent(enclosingClass.getPLevelsParent());
            typedDef.setHLevelsParent(enclosingClass.getHLevelsParent());
          } else {
            boolean setPLevel = def.getPLevelParameters() == null && enclosingClass.hasNonTrivialPLevelParameters();
            boolean setHLevel = def.getHLevelParameters() == null && enclosingClass.hasNonTrivialHLevelParameters();
            if (setPLevel || setHLevel) {
              List<LevelVariable> newParams = new ArrayList<>();
              newParams.addAll(setPLevel ? enclosingClass.getLevelParameters().subList(0, enclosingClass.getNumberOfPLevelParameters()) : typedDef.getLevelParameters().subList(0, typedDef.getNumberOfPLevelParameters()));
              newParams.addAll(setHLevel ? enclosingClass.getLevelParameters().subList(enclosingClass.getNumberOfPLevelParameters(), enclosingClass.getLevelParameters().size()) : typedDef.getLevelParameters().subList(typedDef.getNumberOfPLevelParameters(), typedDef.getLevelParameters().size()));
              typedDef.setLevelParameters(newParams);
              if (setPLevel) typedDef.setPLevelsParent(enclosingClass.getPLevelsParent());
              if (setHLevel) typedDef.setHLevelsParent(enclosingClass.getHLevelsParent());
            }
          }
        }
      } else {
        if (def.getKind().isUse()) {
          Definition useParent = def.getUseParent().getTypechecked();
          int n = useParent.getNumberOfPLevelParameters();
          if (def.getPLevelParameters() != null) {
            compareUseLevelParameters(def.getPLevelParameters(), levelVariablesToParameters(def.getPLevelParameters().getData(), useParent.getLevelParameters().subList(0, n), true));
          }
          if (def.getHLevelParameters() != null) {
            compareUseLevelParameters(def.getHLevelParameters(), levelVariablesToParameters(def.getHLevelParameters().getData(), useParent.getLevelParameters().subList(n, useParent.getLevelParameters().size()), false));
          }
        }
        findLevelsParentsInParameters(typedDef, def, def.getParameters());
        typedDef.setLevelParameters(typecheckLevelParameters(def));
      }
    }

    LinkList list = new LinkList();
    Pair<Sort, Expression> pair = typecheckParameters(def, typedDef, list, localInstancePool, null, myNewDef ? null : typedDef.getParameters(), implementedField, null);
    if (def.getBody() instanceof Concrete.CoelimFunctionBody || def.getBody() instanceof Concrete.ElimFunctionBody && def.getBody().getClauses().isEmpty()) {
      checkNoStrictParameters(def.getParameters());
    } else if (myNewDef) {
      typedDef.setStrictParameters(getStrictParameters(def.getParameters()));
    }

    if (def.getKind() == FunctionKind.TYPE && def.getBody() instanceof Concrete.ElimFunctionBody && def.getResultType() == null) {
      def.setResultType(new Concrete.UniverseExpression(def.getData(), null, null));
    }

    Expression expectedType = null;
    Concrete.Expression cResultType = def.getResultType();
    if (cResultType != null) {
      Type expectedTypeResult = pair == null
        ? new ErrorExpression()
        : def.getBody() instanceof Concrete.CoelimFunctionBody && !def.isRecursive()
          ? null // The result type will be typechecked together with all field implementations during body typechecking.
          : checkResultTypeLater(def)
            ? typechecker.checkType(cResultType, Type.OMEGA)
            : typechecker.finalCheckType(cResultType, Type.OMEGA, kind == FunctionKind.LEMMA && def.getResultTypeLevel() == null);
      if (expectedTypeResult != null) {
        expectedType = expectedTypeResult.getExpr();
      }
    }

    if (myNewDef) {
      if (pair != null && pair.proj2 != null && cResultType == null && implementedField != null) {
        expectedType = pair.proj2;
        if (expectedType.findBinding(implementedField.getType().getParameters())) {
          errorReporter.report(new TypeFromFieldError(typechecker.getExpressionPrettifier(), TypeFromFieldError.resultType(), expectedType, def));
          expectedType = null;
        }
      }
      if (expectedType == null) {
        expectedType = new ErrorExpression();
      }

      typedDef.setResultType(expectedType);
      typedDef.setKind(kind.isSFunc() ? (kind == FunctionKind.LEMMA || kind == FunctionKind.AXIOM ? CoreFunctionDefinition.Kind.LEMMA : kind == FunctionKind.TYPE ? CoreFunctionDefinition.Kind.TYPE : CoreFunctionDefinition.Kind.SFUNC) : kind == FunctionKind.INSTANCE ? CoreFunctionDefinition.Kind.INSTANCE : CoreFunctionDefinition.Kind.FUNC);

      calculateTypeClassParameters(def, typedDef);
      calculateParametersTypecheckingOrder(typedDef);

      GoodThisParametersVisitor goodThisParametersVisitor;
      goodThisParametersVisitor = new GoodThisParametersVisitor(typedDef.getParameters());
      expectedType.accept(goodThisParametersVisitor, null);
      if (typedDef.getResultTypeLevel() != null) {
        typedDef.getResultTypeLevel().accept(goodThisParametersVisitor, null);
      }
      typedDef.setGoodThisParameters(goodThisParametersVisitor.getGoodParameters());

      typedDef.setUniverseKind(checkForUniverses(typedDef, def));
    }

    return pair != null;
  }