private boolean compareClassInstances()

in base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java [1853:1991]
134 lines of code
53 McCabe index (conditional complexity)

  private boolean compareClassInstances(Expression expr1, ClassCallExpression classCall1, Expression expr2, ClassCallExpression classCall2, Expression type) {
    if (expr1 instanceof ArrayExpression array1 && expr2 instanceof ArrayExpression array2 && array1.getElements().size() == array2.getElements().size()) return false;
    if (classCall1.getDefinition() == Prelude.DEP_ARRAY && classCall2.getDefinition() == Prelude.DEP_ARRAY) {
      Expression length1 = classCall1.getImplementationHere(Prelude.ARRAY_LENGTH, expr1);
      Expression length2 = classCall2.getImplementationHere(Prelude.ARRAY_LENGTH, expr1);
      if (length1 != null && length2 != null) {
        length1 = length1.normalize(NormalizationMode.WHNF);
        length2 = length2.normalize(NormalizationMode.WHNF);
        if (length1 instanceof IntegerExpression && ((IntegerExpression) length1).isZero() && length2 instanceof IntegerExpression && ((IntegerExpression) length2).isZero()) {
          Expression elemsType1 = classCall1.getImplementationHere(Prelude.ARRAY_ELEMENTS_TYPE, expr1);
          if (elemsType1 == null) elemsType1 = FieldCallExpression.make(Prelude.ARRAY_ELEMENTS_TYPE, expr1);
          Expression elemsType2 = classCall2.getImplementationHere(Prelude.ARRAY_ELEMENTS_TYPE, expr2);
          if (elemsType2 == null) elemsType2 = FieldCallExpression.make(Prelude.ARRAY_ELEMENTS_TYPE, expr2);
          if (!compare(elemsType1, elemsType2, null, false)) {
            myResult = null;
            return false;
          }
          return true;
        } else {
          if (!classCall1.isImplemented(Prelude.ARRAY_AT) && !(expr1 instanceof ArrayExpression) && !classCall2.isImplemented(Prelude.ARRAY_AT) && !(expr2 instanceof ArrayExpression)) {
            return false;
          }
          var pair1 = getSucs(length1);
          var pair2 = getSucs(length2);
          BigInteger m = pair1.proj2.min(pair2.proj2);
          if (!m.equals(BigInteger.ZERO)) {
            for (BigInteger i = BigInteger.ZERO; i.compareTo(m) < 0; i = i.add(BigInteger.ONE)) {
              IntegerExpression index = new BigIntegerExpression(i);
              if (!normalizedCompare(FunCallExpression.make(Prelude.ARRAY_INDEX, classCall1.getLevels(), Arrays.asList(expr1, index)).normalize(NormalizationMode.WHNF),
                                     FunCallExpression.make(Prelude.ARRAY_INDEX, classCall2.getLevels(), Arrays.asList(expr2, index)).normalize(NormalizationMode.WHNF), null, true) ||
                  !compare(dropElements(expr1, pair1.proj1, classCall1, m), dropElements(expr2, pair2.proj1, classCall2, m), new ClassCallExpression(Prelude.DEP_ARRAY, classCall1.getLevels()), true)) {
                myResult = null;
                return false;
              }
            }
            return true;
          }
        }
      }
    }

    Set<? extends ClassField> fields = null;
    if (type != null) {
      ClassCallExpression classCall = type.cast(ClassCallExpression.class);
      if (classCall != null) {
        Set<ClassField> fieldsCopy = new LinkedHashSet<>();
        for (ClassField field : classCall.getDefinition().getNotImplementedFields()) {
          if (!classCall.isImplementedHere(field)) {
            fieldsCopy.add(field);
          }
        }
        fields = fieldsCopy;
      }
    }
    if (fields == null) {
      if (classCall1.getDefinition() == classCall2.getDefinition()) {
        fields = classCall1.getDefinition().getAllFields();
      } else {
        Set<ClassField> fields1 = new LinkedHashSet<>();
        for (ClassField field : classCall1.getDefinition().getNotImplementedFields()) {
          if (classCall2.getDefinition().containsField(field)) {
            fields1.add(field);
          }
        }
        for (ClassField field : classCall1.getDefinition().getImplementedFields()) {
          if (classCall2.getDefinition().containsField(field)) {
            fields1.add(field);
          }
        }
        fields = fields1;
      }
    }

    for (ClassField field : fields) {
      if (!field.isProperty() && !classCall1.isImplemented(field) && !classCall2.isImplemented(field)) {
        return false;
      }
    }

    for (ClassField field : fields) {
      if (field.isProperty()) {
        continue;
      }

      AbsExpression absImpl1 = classCall1.getAbsImplementation(field);
      AbsExpression absImpl2 = classCall2.getAbsImplementation(field);
      if (absImpl1 == null || absImpl2 == null) {
        Expression impl1 = absImpl1 == null ? FieldCallExpression.make(field, expr1) : classCall1.getImplementation(field, expr1);
        Expression impl2 = absImpl2 == null ? FieldCallExpression.make(field, expr2) : classCall2.getImplementation(field, expr2);
        if (!compare(impl1, impl2, field.getType(classCall1.getLevels(field.getParentClass())).applyExpression(expr1), true)) {
          myResult = null;
          return false;
        }
      } else {
        Binding prevBinding = mySubstitution.put(classCall2.getThisBinding(), classCall1.getThisBinding());
        Expression impl1 = classCall1.getAbsImplementationHere(field);
        Expression impl2 = classCall2.getAbsImplementationHere(field);
        if (impl1 == null) {
          impl1 = Objects.requireNonNull(classCall1.getDefinition().getImplementation(field)).apply(expr1, LevelSubstitution.EMPTY);
        }
        if (impl2 == null) {
          impl2 = Objects.requireNonNull(classCall2.getDefinition().getImplementation(field)).apply(expr2, LevelSubstitution.EMPTY);
        }
        boolean ok = compare(impl1, impl2, field.getType(classCall1.getLevels(field.getParentClass())).applyExpression(expr1), true);
        if (prevBinding == null) {
          mySubstitution.remove(classCall2.getThisBinding());
        } else {
          mySubstitution.put(classCall2.getThisBinding(), prevBinding);
        }
        if (!ok) {
          if (expr1 instanceof NewExpression && expr2 instanceof NewExpression) {
            if (myResult == null) {
              initResult(expr1, expr2);
            } else {
              if (classCall1.isImplementedHere(field)) {
                Map<ClassField, Expression> impls = new LinkedHashMap<>(classCall1.getImplementedHere());
                impls.put(field, myResult.wholeExpr1);
                myResult.wholeExpr1 = new NewExpression(null, new ClassCallExpression(classCall1.getDefinition(), classCall1.getLevels(), impls, classCall1.getSort(), classCall1.getUniverseKind()));
              } else {
                myResult.wholeExpr1 = expr1;
              }
              if (classCall2.isImplementedHere(field)) {
                Map<ClassField, Expression> impls = new LinkedHashMap<>(classCall2.getImplementedHere());
                impls.put(field, myResult.wholeExpr2);
                myResult.wholeExpr2 = new NewExpression(null, new ClassCallExpression(classCall2.getDefinition(), classCall2.getLevels(), impls, classCall2.getSort(), classCall2.getUniverseKind()));
              } else {
                myResult.wholeExpr2 = expr2;
              }
            }
          } else {
            myResult = null;
          }
          return false;
        }
      }
    }

    return true;
  }