public static boolean compare()

in base/src/main/java/org/arend/core/sort/Level.java [153:204]
44 lines of code
37 McCabe index (conditional complexity)

  public static boolean compare(Level level1, Level level2, CMP cmp, Equations equations, Concrete.SourceNode sourceNode) {
    if (cmp == CMP.GE) {
      return compare(level2, level1, CMP.LE, equations, sourceNode);
    }

    if (level1.isInfinity()) {
      return level2.isInfinity() || !level2.isClosed() && (equations == null || equations.addEquation(INFINITY, level2, CMP.LE, sourceNode));
    }
    if (level2.isInfinity()) {
      return cmp == CMP.LE || !level1.isClosed() && (equations == null || equations.addEquation(INFINITY, level1, CMP.LE, sourceNode));
    }

    if (level2.myVar == null && level1.myVar != null && !(level1.myVar instanceof InferenceLevelVariable)) {
      return false;
    }

    if (level1.myVar == null) {
      if (level2.myVar == null) {
        return cmp == CMP.LE ? level1.myConstant <= level2.myConstant : level1.myConstant == level2.myConstant;
      }
      if (cmp == CMP.EQ) {
        // c == max(l + c', m') can be true only if l is an inference var and c >= m' and c >= c' + l.minValue
        if (!(level2.myVar instanceof InferenceLevelVariable) || level1.myConstant < level2.myMaxConstant || level1.myConstant < level2.myConstant + level2.myVar.getMinValue()) {
          return false;
        }
      } else {
        // c <= max(l + c', m') always can be true if l is an inference var
        if (!(level2.myVar instanceof InferenceLevelVariable)) {
          // If l is not an inference var, then c <= max(l + c', m') is true if and only if either c <= m' or c <= c' + l.minValue
          return level1.myConstant <= level2.myMaxConstant || level1.myConstant <= level2.myConstant + level2.myVar.getMinValue();
        }
      }
    }

    if (level1.myVar != null && level2.myVar != null) {
      if (level1.myVar.compare(level2.myVar, cmp)) {
        if (cmp == CMP.EQ && level1.myConstant != level2.myConstant || cmp == CMP.LE && level1.myConstant > level2.myConstant) {
          return false;
        }
        if (level1.myMaxConstant == level2.myMaxConstant || cmp == CMP.LE && (level1.myMaxConstant <= level2.myMaxConstant || level1.myMaxConstant <= level2.myConstant + level2.myVar.getMinValue())) {
          return true;
        }
        if (!(level1.myVar instanceof InferenceLevelVariable)) {
          return false;
        }
      } else if (!(level1.myVar instanceof InferenceLevelVariable) && !(level2.myVar instanceof InferenceLevelVariable)) {
        return false;
      }
    }

    return equations == null || equations.addEquation(level1, level2, cmp, sourceNode);
  }