private DependentLink reportNoClauses()

in base/src/main/java/org/arend/typechecking/patternmatching/ElimTypechecking.java [531:648]
104 lines of code
36 McCabe index (conditional complexity)

  private DependentLink reportNoClauses(DependentLink parameters, List<DependentLink> elimParams) {
    if (myErrorReporter == null) return null;
    if (elimParams.isEmpty()) {
      for (int i = 0; i < myNumberOfExternalParameters && parameters.hasNext(); i++) {
        parameters = parameters.getNext();
      }
    }

    if (parameters.hasNext() && !parameters.getNext().hasNext()) {
      DataCallExpression dataCall = parameters.getTypeExpr().cast(DataCallExpression.class);
      if (dataCall != null && dataCall.getDefinition() == Prelude.INTERVAL) {
        myErrorReporter.report(new TypecheckingError("Pattern matching on the interval is not allowed here", mySourceNode));
        return null;
      }
    }

    // If paramSpec[p] is non-null, then it gives a specification for parameter p.
    // We should generate the list of patterns corresponding to the first projection of elements of paramSpec[p].
    // Moreover, for every index i and every parameter p' such that paramSpec[p][i].proj2[p'] is non-null and is equal to con,
    // then this spec applies only if the pattern generated for parameter p is of the form (con p_1 ... p_k).
    Map<DependentLink, List<Pair<ExpressionPattern, Map<DependentLink, Constructor>>>> paramSpec = new HashMap<>();
    Map<DependentLink, List<ConCallExpression>> paramSpec2 = new HashMap<>();
    DependentLink emptyLink = null;
    for (DependentLink param = parameters; param.hasNext(); param = param.getNext()) {
      if (!elimParams.isEmpty() && !elimParams.contains(param)) {
        continue;
      }
      DataCallExpression dataCall = param.getTypeExpr().normalize(NormalizationMode.WHNF).cast(DataCallExpression.class);
      if (dataCall != null) {
        Map<DependentLink, List<Pair<ExpressionPattern, Map<DependentLink, Constructor>>>> newParamSpec = computeParamSpec(param, dataCall, elimParams, paramSpec2, parameters);
        if (newParamSpec == null) {
          return null;
        }
        if (!newParamSpec.isEmpty()) {
          emptyLink = param;
        }
        for (Map.Entry<DependentLink, List<Pair<ExpressionPattern, Map<DependentLink, Constructor>>>> entry : newParamSpec.entrySet()) {
          paramSpec.compute(entry.getKey(), (k,list) -> {
            if (list == null) {
              return entry.getValue();
            }
            List<Pair<ExpressionPattern, Map<DependentLink, Constructor>>> result = new ArrayList<>();
            for (Pair<ExpressionPattern, Map<DependentLink, Constructor>> pair1 : list) {
              for (Pair<ExpressionPattern, Map<DependentLink, Constructor>> pair2 : entry.getValue()) {
                ExpressionPattern pattern = pair1.proj1.intersect(pair2.proj1);
                if (pattern != null) {
                  Map<DependentLink, Constructor> newMap = new HashMap<>();
                  newMap.putAll(pair1.proj2);
                  newMap.putAll(pair2.proj2);
                  result.add(new Pair<>(pattern, newMap));
                }
              }
            }
            return result;
          });
        }
      }
    }

    List<List<ExpressionPattern>> missingClauses = generateMissingClauses(elimParams.isEmpty() ? DependentLink.Helper.toList(parameters) : elimParams, 0, new ExprSubstitution(), paramSpec, paramSpec2);
    for (int i = 0; i < missingClauses.size(); i++) {
      for (int j = i + 1; j < missingClauses.size(); j++) {
        if (ExpressionPattern.compare(missingClauses.get(i), missingClauses.get(j))) {
          missingClauses.remove(j--);
        }
      }
    }

    if (myLevel != null) {
      missingClauses.removeIf(clause -> numberOfIntervals(clause) > myLevel);
    }

    if (missingClauses.isEmpty()) {
      return emptyLink;
    }

    for (List<ExpressionPattern> patterns : missingClauses) {
      Collections.reverse(patterns);
    }

    boolean allVars = missingClauses.size() == 1;
    for (List<ExpressionPattern> patterns : missingClauses) {
      DependentLink param = parameters;
      for (int i = 0; i < patterns.size(); i++, param = param.getNext()) {
        if (!(patterns.get(i) instanceof BindingPattern)) {
          allVars = false;
        }
        if (patterns.get(i) instanceof BindingPattern && !paramSpec.containsKey(param)) {
          ConstructorExpressionPattern newPattern;
          List<ExpressionPattern> subPatterns;
          Expression type = ((BindingPattern) patterns.get(i)).getBinding().getTypeExpr().getUnderlyingExpression();
          if (type instanceof SigmaExpression) {
            subPatterns = new ArrayList<>();
            newPattern = new ConstructorExpressionPattern((SigmaExpression) type, subPatterns);
          } else if (type instanceof ClassCallExpression) {
            subPatterns = new ArrayList<>();
            newPattern = new ConstructorExpressionPattern((ClassCallExpression) type, subPatterns);
          } else {
            continue;
          }

          allVars = false;
          patterns.set(i, newPattern);
          for (DependentLink link = newPattern.getParameters(); link.hasNext(); link = link.getNext()) {
            subPatterns.add(new BindingPattern(link));
          }
        }
      }
    }

    if (allVars) {
      myErrorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.BODY_REQUIRED, mySourceNode));
      return null;
    }

    myErrorReporter.report(new MissingClausesError(missingClauses, parameters, elimParams, true, mySourceNode));
    return null;
  }