public Body typecheckElim()

in base/src/main/java/org/arend/typechecking/patternmatching/ElimTypechecking.java [198:326]
120 lines of code
46 McCabe index (conditional complexity)

  public Body typecheckElim(List<? extends ElimClause<ExpressionPattern>> clauses, DependentLink parameters, List<DependentLink> elimParams) {
    myOK = true;
    myUnusedClauses = new LinkedHashSet<>();
    for (int i = 0; i < clauses.size(); i++) {
      myUnusedClauses.add(i);
    }

    List<ElimClause<ExpressionPattern>> intervalClauses;
    List<ExtElimClause> nonIntervalClauses = new ArrayList<>();
    if (myAllowInterval && myMode.allowInterval()) {
      intervalClauses = new ArrayList<>();
      Concrete.SourceNode errorClause = null;
      for (int i = 0; i < clauses.size(); i++) {
        ElimClause<ExpressionPattern> clause = clauses.get(i);
        boolean hasNonIntervals = false;
        int intervals = 0;
        for (Pattern pattern : clause.getPatterns()) {
          if (pattern instanceof BindingPattern) {
            continue;
          }
          if (pattern instanceof ConstructorPattern) {
            Definition constructor = pattern.getDefinition();
            if (constructor == Prelude.LEFT || constructor == Prelude.RIGHT) {
              intervals++;
              continue;
            }
          }
          hasNonIntervals = true;
          break;
        }
        if (hasNonIntervals || intervals == 0) {
          nonIntervalClauses.add(new ExtElimClause(clause.getPatterns(), clause.getExpression(), i));
          if (!intervalClauses.isEmpty() && errorClause == null && myErrorReporter != null) {
            errorClause = getClause(i, null);
          }
        } else {
          if (intervals > 1) {
            if (myErrorReporter != null) myErrorReporter.report(new TypecheckingError("Only a single interval pattern per row is allowed", getClause(i, null)));
            myUnusedClauses.remove(i);
          } else {
            intervalClauses.add(clause);
          }
          clauses.remove(i--);
        }
      }
      if (errorClause != null) {
        myErrorReporter.report(new TypecheckingError("Non-interval clauses must be placed before the interval ones", errorClause));
      }
    } else {
      intervalClauses = Collections.emptyList();
      for (int i = 0; i < clauses.size(); i++) {
        nonIntervalClauses.add(new ExtElimClause(clauses.get(i).getPatterns(), clauses.get(i).getExpression(), i));
      }
    }

    List<IntervalElim.CasePair> cases = intervalClauses.isEmpty() ? null : clausesToIntervalElim(intervalClauses, nonIntervalClauses.size(), parameters);
    if (cases != null) {
      int i = 0;
      for (; i < cases.size(); i++) {
        if (cases.get(i).proj1 != null || cases.get(i).proj2 != null) {
          break;
        }
      }
      cases = cases.subList(i, cases.size());

      for (int k = 0; k < nonIntervalClauses.size(); k++) {
        for (int j = i; j < nonIntervalClauses.get(k).getPatterns().size(); j++) {
          if (!(nonIntervalClauses.get(k).getPatterns().get(j) instanceof BindingPattern) && myErrorReporter != null) {
            myErrorReporter.report(new TypecheckingError("A pattern matching on a data type is allowed only before the pattern matching on the interval", getClause(k, null)));
            myOK = false;
          }
        }
      }
    }

    ElimTree elimTree;
    if (nonIntervalClauses.isEmpty()) {
      DependentLink emptyLink = null;
      if (elimParams.isEmpty()) {
        for (DependentLink link = parameters; link.hasNext(); link = link.getNext()) {
          link = link.getNextTyped(null);
          List<ConCallExpression> conCalls = getMatchedConstructors(TypeConstructorExpression.unfoldType(link.getTypeExpr()));
          if (conCalls != null && conCalls.isEmpty()) {
            emptyLink = link;
            break;
          }
        }
      } else {
        for (DependentLink link : elimParams) {
          List<ConCallExpression> conCalls = getMatchedConstructors(TypeConstructorExpression.unfoldType(link.getTypeExpr()));
          if (conCalls != null && conCalls.isEmpty()) {
            emptyLink = link;
            break;
          }
        }
      }

      if (emptyLink == null && myMode.checkCoverage()) {
        if (!reportMissingClauses(null, parameters, elimParams)) {
          emptyLink = reportNoClauses(parameters, elimParams);
        }
      }

      if (emptyLink != null) {
        int index = 0;
        for (DependentLink link = parameters; link != emptyLink; link = link.getNext()) {
          index++;
        }
        elimTree = new BranchElimTree(index, false);
      } else {
        elimTree = null;
      }
    } else {
      myContext = new Stack<>();
      myCoreClauses = nonIntervalClauses;
      elimTree = clausesToElimTree(nonIntervalClauses, 0, 0);

      reportMissingClauses(elimTree, parameters, elimParams);

      if (myOK && myErrorReporter != null) {
        for (Integer clauseIndex : myUnusedClauses) {
          myErrorReporter.report(new RedundantClauseError(getClause(clauseIndex, null)));
        }
      }
    }

    ElimBody elimBody = elimTree == null ? null : new ElimBody(removeExpressionsFromPatterns(clauses), elimTree);
    return cases == null ? elimBody : new IntervalElim(DependentLink.Helper.size(parameters), cases, elimBody);
  }