private boolean check()

in base/src/main/java/org/arend/typechecking/doubleChecker/CoreDefinitionChecker.java [73:195]
109 lines of code
42 McCabe index (conditional complexity)

  private boolean check(FunctionDefinition definition) {
    Body body = definition.getReallyActualBody();
    boolean checkType = true;
    if (body instanceof NewExpression && ((NewExpression) body).getRenewExpression() == null && definition.getResultType() instanceof ClassCallExpression typeClassCall && definition.getResultTypeLevel() == null) {
      Map<ClassField, Expression> newImpls = new LinkedHashMap<>();
      ClassCallExpression bodyClassCall = ((NewExpression) body).getClassCall();
      ClassCallExpression newClassCall = new ClassCallExpression(bodyClassCall.getDefinition(), typeClassCall.getLevels(), newImpls, Sort.PROP, UniverseKind.NO_UNIVERSES);
      Expression newThisBinding = new ReferenceExpression(newClassCall.getThisBinding());
      boolean ok = true;
      for (ClassField field : typeClassCall.getDefinition().getNotImplementedFields()) {
        Expression typeImpl = typeClassCall.getAbsImplementationHere(field);
        Expression bodyImpl = bodyClassCall.getAbsImplementationHere(field);
        if (typeImpl != null && bodyImpl != null) {
          ok = false;
          break;
        }
        if (typeImpl != null || bodyImpl != null) {
          newImpls.put(field, typeImpl != null ? typeImpl.subst(typeClassCall.getThisBinding(), newThisBinding) : bodyImpl.subst(bodyClassCall.getThisBinding(), newThisBinding));
        }
      }
      for (ClassField field : typeClassCall.getDefinition().getImplementedFields()) {
        Expression bodyImpl = bodyClassCall.getAbsImplementationHere(field);
        if (bodyImpl != null) {
          newImpls.put(field, bodyImpl.subst(bodyClassCall.getThisBinding(), newThisBinding));
        }
      }
      if (ok) {
        checkType = false;
        body = new NewExpression(null, newClassCall);
      }
    }

    Expression typeType = checkType ? definition.getResultType().accept(myChecker, Type.OMEGA) : null;
    Integer level = definition.getResultTypeLevel() == null ? null : myChecker.checkLevelProof(definition.getResultTypeLevel(), definition.getResultType());

    if (definition.getKind() == CoreFunctionDefinition.Kind.LEMMA && (level == null || level != -1)) {
      if (!DefinitionTypechecker.isBoxed(definition)) {
        DefCallExpression resultDefCall = definition.getResultType().cast(DefCallExpression.class);
        if (resultDefCall == null || !Objects.equals(resultDefCall.getUseLevel(), -1)) {
          Sort sort = typeType == null ? definition.getResultType().getSortOfType() : typeType.toSort();
          if (sort == null) {
            errorReporter.report(CoreErrorWrapper.make(new TypecheckingError("Cannot infer the sort of the type", null), definition.getResultType()));
            return false;
          }
          if (!sort.isProp()) {
            errorReporter.report(CoreErrorWrapper.make(new TypeMismatchError(new UniverseExpression(Sort.PROP), new UniverseExpression(sort), null), definition.getResultType()));
            return false;
          }
        }
      }
    }

    if (definition.isAxiom()) {
      if (body != null) {
        errorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.AXIOM_WITH_BODY, null));
        return false;
      } else {
        return true;
      }
    }

    if (body instanceof Expression) {
      if (body instanceof CaseExpression) {
        myChecker.checkCase((CaseExpression) body, definition.getResultType(), level);
      } else {
        ((Expression) body).accept(myChecker, checkType ? definition.getResultType() : null);
      }
      return true;
    }

    ElimBody elimBody;
    if (body instanceof IntervalElim intervalElim) {
      if (intervalElim.getCases().isEmpty()) {
        errorReporter.report(new TypecheckingError("Empty IntervalElim", null));
        return false;
      }

      int offset = intervalElim.getOffset();
      DependentLink link = definition.getParameters();
      for (int i = 0; i < offset && link.hasNext(); i++) {
        link = link.getNext();
      }

      for (IntervalElim.CasePair ignored : intervalElim.getCases()) {
        if (!link.hasNext()) {
          errorReporter.report(new TypecheckingError("Interval elim has too many parameters", null));
          return false;
        }

        DataCallExpression dataCall = link.getTypeExpr().normalize(NormalizationMode.WHNF).cast(DataCallExpression.class);
        if (!(dataCall != null && dataCall.getDefinition() == Prelude.INTERVAL)) {
          errorReporter.report(new TypeMismatchError(DataCallExpression.make(Prelude.INTERVAL, Levels.EMPTY, Collections.emptyList()), link.getTypeExpr(), null));
          return false;
        }

        link = link.getNext();
      }

      // TODO[double_check]: Check interval conditions

      if (intervalElim.getOtherwise() == null) {
        errorReporter.report(new TypecheckingError("Missing non-interval clauses", null));
        return false;
      }

      elimBody = intervalElim.getOtherwise();
    } else if (body instanceof ElimBody) {
      elimBody = (ElimBody) body;
    } else if (body == null) {
      ClassCallExpression classCall = definition.getResultType().normalize(NormalizationMode.WHNF).cast(ClassCallExpression.class);
      if (classCall == null) {
        errorReporter.report(new TypecheckingError("Missing a body", null));
        return false;
      }
      myChecker.checkCocoverage(classCall);
      return true;
    } else {
      throw new IllegalStateException();
    }

    myChecker.checkElimBody(definition, elimBody, definition.getParameters(), definition.getResultType(), level, null, definition.isSFunc(), PatternTypechecking.Mode.FUNCTION);
    return true;
  }