public boolean areDisjointConstructors()

in base/src/main/java/org/arend/core/expr/Expression.java [438:518]
78 lines of code
37 McCabe index (conditional complexity)

  public boolean areDisjointConstructors(@NotNull UncheckedExpression expr2) {
    Expression expr1 = normalize(NormalizationMode.WHNF);
    expr2 = UncheckedExpressionImpl.extract(expr2).normalize(NormalizationMode.WHNF);
    if (expr1 instanceof IntegerExpression) {
      return checkInteger(((IntegerExpression) expr1).getBigInteger(), expr2);
    }
    if (expr2 instanceof IntegerExpression) {
      return checkInteger(((IntegerExpression) expr2).getBigInteger(), expr1);
    }
    if (expr1 instanceof ArrayExpression array1 && expr2 instanceof ArrayExpression array2) {
      if (array1.getTail() == null && array1.getElements().size() < array2.getElements().size() || array2.getTail() == null && array2.getElements().size() < array1.getElements().size()) {
        return true;
      }
      for (int i = 0; i < array1.getElements().size() && i < array2.getElements().size(); i++) {
        if (array1.getElements().get(i).areDisjointConstructors(array2.getElements().get(i))) {
          return true;
        }
      }
      return array1.getTail() != null && Boolean.TRUE.equals(ConstructorExpressionPattern.isArrayEmpty(array1.getTail().getType())) || array2.getTail() != null && Boolean.TRUE.equals(ConstructorExpressionPattern.isArrayEmpty(array2.getTail().getType()));
    }
    if (!(expr1 instanceof ConCallExpression conCall1) || !(expr2 instanceof ConCallExpression conCall2)) {
      return false;
    }

    Constructor con1 = conCall1.getDefinition();
    Constructor con2 = conCall2.getDefinition();
    if (con1.getDataType() != con2.getDataType() || con1.getDataType() == Prelude.INTERVAL) {
      return false;
    }

    if (con1.getDataType().isHIT()) {
      GraphClosure<Constructor> closure = new GraphClosure<>();
      for (Constructor constructor : con1.getDataType().getConstructors()) {
        Body body = constructor.getBody();
        if (body instanceof IntervalElim) {
          for (IntervalElim.CasePair pair : ((IntervalElim) body).getCases()) {
            if (!addConstructor(pair.proj1, constructor, closure) || !addConstructor(pair.proj2, constructor, closure)) {
              return false;
            }
          }
          body = ((IntervalElim) body).getOtherwise();
        }
        if (body instanceof ElimBody) {
          for (ElimClause<Pattern> clause : ((ElimBody) body).getClauses()) {
            if (!addConstructor(clause.getExpression(), constructor, closure)) {
              return false;
            }
          }
        } else if (body != null) {
          throw new IllegalStateException();
        }
      }

      return !closure.areEquivalent(con1, con2);
    } else {
      List<ConCallExpression> conCalls1 = new ArrayList<>();
      conCalls1.add(conCall1);
      List<ConCallExpression> conCalls2 = new ArrayList<>();
      conCalls2.add(conCall2);
      if (!computeClosure(conCalls1) || !computeClosure(conCalls2)) {
        return false;
      }
      for (ConCallExpression cc1 : conCalls1) {
        for (ConCallExpression cc2 : conCalls2) {
          if (cc1.getDefinition() == cc2.getDefinition()) {
            boolean ok = false;
            for (int i = 0; i < cc1.getDefCallArguments().size(); i++) {
              if (cc1.getDefCallArguments().get(i).areDisjointConstructors(cc2.getDefCallArguments().get(i))) {
                ok = true;
                break;
              }
            }
            if (!ok) {
              return false;
            }
          }
        }
      }
      return true;
    }
  }