private static boolean computeCovering()

in meta/src/main/java/org/arend/lib/pattern/PatternUtils.java [296:443]
133 lines of code
31 McCabe index (conditional complexity)

  private static boolean computeCovering(List<Pair<? extends List<? extends CorePattern>, Integer>> actualRows, List<? extends CorePattern> row, Set<Integer> indices) {
    if (actualRows.isEmpty()) {
      return false;
    }
    if (row.isEmpty()) {
      indices.add(actualRows.get(0).proj2);
      return true;
    }

    class MyBinding implements CoreBinding {
      final CoreExpression type;

      MyBinding(CoreExpression type) {
          this.type = type;
      }

      @Override
      public CoreExpression getTypeExpr() {
        return type;
      }

      @Override
      public CoreReferenceExpression makeReference() {
        return null;
      }

      @Override
      public String getName() {
        return null;
      }
    }

    CorePattern pattern = row.get(0);
    List<Pair<? extends List<? extends CorePattern>, Integer>> newRows = new ArrayList<>(actualRows.size());
    List<? extends CorePattern> rowTail = row.subList(1, row.size());
    if (pattern.getBinding() != null) {
      boolean allVars = true;
      boolean hasVars = false;
      Set<CoreDefinition> constructors = new LinkedHashSet<>();
      for (Pair<? extends List<? extends CorePattern>, Integer> actualRow : actualRows) {
        CorePattern actualPattern = actualRow.proj1.get(0);
        if (actualPattern.isAbsurd()) { // TODO: This is not needed if implemented properly; see TODO below
          indices.add(actualRow.proj2);
          return true;
        }
        if (actualPattern.getBinding() == null) {
          allVars = false;
          if (actualPattern.getConstructor() != null) {
            constructors.add(actualPattern.getConstructor());
          }
        } else {
          hasVars = true;
        }
      }

      if (allVars) {
        for (Pair<? extends List<? extends CorePattern>, Integer> actualRow : actualRows) {
          newRows.add(new Pair<>(actualRow.proj1.subList(1, actualRow.proj1.size()), actualRow.proj2));
        }
        return computeCovering(newRows, rowTail, indices);
      }

      List<Pair<CoreDefinition, CoreParameter>> consWithParams;
      CoreExpression type = pattern.getBinding().getTypeExpr();
      if (type != null) type = type.unfoldType();
      if (type instanceof CoreSigmaExpression sigmaExpr) {
        consWithParams = Collections.singletonList(new Pair<>(null, sigmaExpr.getParameters()));
      } else if (type instanceof CoreClassCallExpression classCall) {
        consWithParams = Collections.singletonList(new Pair<>(null, classCall.getClassFieldParameters()));
      } else {
        List<CoreExpression.ConstructorWithDataArguments> constructorsWithArgs = type == null ? null : type.computeMatchedConstructorsWithDataArguments();
        if (constructorsWithArgs == null) {
          // TODO: We should return null here, but to do this we need to substitute previous patterns in type
          consWithParams = new ArrayList<>(constructors.size());
          for (CoreDefinition constructor : constructors) {
            consWithParams.add(new Pair<>(constructor, constructor.getParameters()));
          }
        } else {
          if (!hasVars) {
            for (CoreExpression.ConstructorWithDataArguments cons : constructorsWithArgs) {
              if (!constructors.contains(cons.getConstructor())) {
                return false;
              }
            }
          }
          consWithParams = new ArrayList<>(constructorsWithArgs.size());
          for (CoreExpression.ConstructorWithDataArguments cons : constructorsWithArgs) {
            consWithParams.add(new Pair<>(cons.getConstructor(), cons.getParameters()));
          }
        }
      }

      for (Pair<CoreDefinition, CoreParameter> pair : consWithParams) {
        List<CorePattern> newRow = new ArrayList<>();
        for (CoreParameter param = pair.proj2; param.hasNext(); param = param.getNext()) {
          newRow.add(new ArendPattern(new MyBinding(param.getTypeExpr()), null, Collections.emptyList(), null, null));
        }
        newRow.addAll(rowTail);

        newRows.clear();
        for (Pair<? extends List<? extends CorePattern>, Integer> actualRow : actualRows) {
          CorePattern actualPattern = actualRow.proj1.get(0);
          if (actualPattern.getBinding() != null) {
            List<CorePattern> newActualRow = new ArrayList<>();
            for (CoreParameter param = pair.proj2; param.hasNext(); param = param.getNext()) {
              newActualRow.add(new ArendPattern(new MyBinding(null), null, Collections.emptyList(), null, null));
            }
            newActualRow.addAll(actualRow.proj1.subList(1, actualRow.proj1.size()));
            newRows.add(new Pair<>(newActualRow, actualRow.proj2));
          } else if (actualPattern.getConstructor() == pair.proj1) {
            List<CorePattern> newActualRow = new ArrayList<>();
            newActualRow.addAll(actualPattern.getSubPatterns());
            newActualRow.addAll(actualRow.proj1.subList(1, actualRow.proj1.size()));
            newRows.add(new Pair<>(newActualRow, actualRow.proj2));
          }
        }

        if (!computeCovering(newRows, newRow, indices)) {
          return false;
        }
      }

      return true;
    } else {
      List<CorePattern> newRow = new ArrayList<>();
      newRow.addAll(pattern.getSubPatterns());
      newRow.addAll(rowTail);

      for (Pair<? extends List<? extends CorePattern>, Integer> actualRow : actualRows) {
        CorePattern actualPattern = actualRow.proj1.get(0);
        if (actualPattern.getBinding() != null) {
          List<CorePattern> newActualRow = new ArrayList<>();
          for (CorePattern ignored : pattern.getSubPatterns()) {
            newActualRow.add(new ArendPattern(new MyBinding(null), null, Collections.emptyList(), null, null));
          }
          newActualRow.addAll(actualRow.proj1.subList(1, actualRow.proj1.size()));
          newRows.add(new Pair<>(newActualRow, actualRow.proj2));
        } else if (actualPattern.getConstructor() == pattern.getConstructor()) {
          List<CorePattern> newActualRow = new ArrayList<>();
          newActualRow.addAll(actualPattern.getSubPatterns());
          newActualRow.addAll(actualRow.proj1.subList(1, actualRow.proj1.size()));
          newRows.add(new Pair<>(newActualRow, actualRow.proj2));
        }
      }

      return computeCovering(newRows, newRow, indices);
    }
  }