private boolean checkFin()

in base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java [975:1047]
69 lines of code
44 McCabe index (conditional complexity)

  private boolean checkFin(DataCallExpression expr1, DataCallExpression expr2, boolean correctOrder) {
    if (expr1.getDefinition() == Prelude.NAT) {
      return expr2.getDefinition() == Prelude.NAT;
    }
    if (expr2.getDefinition() == Prelude.NAT) {
      return myCMP != CMP.EQ;
    }

    Expression arg1 = expr1.getDefCallArguments().get(0);
    Expression arg2 = expr2.getDefCallArguments().get(0);
    if (myCMP == CMP.EQ) {
      return compare(correctOrder ? arg1 : arg2, correctOrder ? arg2 : arg1, ExpressionFactory.Nat(), false);
    }

    if (myNormalize) {
      arg1 = arg1.normalize(NormalizationMode.WHNF);
      arg2 = arg2.normalize(NormalizationMode.WHNF);
    }
    if (arg1 instanceof IntegerExpression && arg2 instanceof IntegerExpression) {
      return ((IntegerExpression) arg1).compare((IntegerExpression) arg2) <= 0;
    }

    var pair1 = getSucs(arg1);
    var pair2 = getSucs(arg2);
    InferenceVariable stuckVar1 = pair1.proj1.getStuckInferenceVariable();
    InferenceVariable stuckVar2 = pair2.proj1.getStuckInferenceVariable();
    if (stuckVar2 == null && pair1.proj2.compareTo(pair2.proj2) > 0) {
      return false;
    }
    if (stuckVar2 == null && pair1.proj1 instanceof IntegerExpression || stuckVar2 != null && pair1.proj1 instanceof IntegerExpression && pair1.proj2.compareTo(pair2.proj2) <= 0) {
      return true;
    }
    if (stuckVar1 != null || stuckVar2 != null) {
      if (pair1.proj1.getInferenceVariable() == null && pair2.proj1.getInferenceVariable() == null) {
        boolean allowEquations = myAllowEquations;
        CMP cmp = myCMP;
        myAllowEquations = false;
        boolean ok = normalizedCompare((correctOrder ? pair1 : pair2).proj1, (correctOrder ? pair2 : pair1).proj1, ExpressionFactory.Nat(), false);
        myAllowEquations = allowEquations;
        myCMP = cmp;
        if (ok) {
          return true;
        }
      }

      if (pair1.proj1 instanceof InferenceReferenceExpression && pair2.proj1 instanceof InferenceReferenceExpression && stuckVar1 == stuckVar2) {
        return pair1.proj2.compareTo(pair2.proj2) <= 0;
      }
      if (!myNormalCompare || myEquations == DummyEquations.getInstance()) {
        return false;
      }
      if (pair1.proj1 instanceof InferenceReferenceExpression && stuckVar2 == null) {
        return myEquations.addEquation(pair1.proj1, pair2.proj1 instanceof IntegerExpression ? new BigIntegerExpression(pair2.proj2.subtract(pair1.proj2)) : ExpressionFactory.add(pair2.proj1, pair2.proj2.intValueExact() - pair1.proj2.intValueExact()), ExpressionFactory.Nat(), CMP.EQ, stuckVar1.getSourceNode(), stuckVar1, null);
      }
      if (pair2.proj1 instanceof InferenceReferenceExpression && stuckVar1 == null) {
        return myEquations.addEquation(
          pair1.proj1 instanceof IntegerExpression
            ? new BigIntegerExpression(pair1.proj2.subtract(pair2.proj2))
            : pair1.proj2.compareTo(pair2.proj2) <= 0 ? pair1.proj1 : ExpressionFactory.add(pair1.proj1, pair1.proj2.intValueExact() - pair2.proj2.intValueExact()),
          pair2.proj1, ExpressionFactory.Nat(), CMP.EQ, stuckVar2.getSourceNode(), null, stuckVar2);
      }
      if (!myAllowEquations) {
        return false;
      }
      if (myNormalize) {
        expr1 = ExpressionFactory.Fin(pair1.proj1 instanceof IntegerExpression ? new BigIntegerExpression(pair1.proj2) : ExpressionFactory.add(pair1.proj1, pair1.proj2.intValueExact()));
        expr2 = ExpressionFactory.Fin(pair2.proj1 instanceof IntegerExpression ? new BigIntegerExpression(pair2.proj2) : ExpressionFactory.add(pair2.proj1, pair2.proj2.intValueExact()));
      }
      return myEquations.addEquation((correctOrder ? expr1 : expr2), substitute(correctOrder ? expr2 : expr1), Type.OMEGA, myCMP, (stuckVar1 != null ? stuckVar1 : stuckVar2).getSourceNode(), stuckVar1, stuckVar2);
    } else {
      return normalizedCompare((correctOrder ? pair1 : pair2).proj1, (correctOrder ? pair2 : pair1).proj1, ExpressionFactory.Nat(), false);
    }
  }