private CompiledTerm removePair()

in meta/src/main/java/org/arend/lib/meta/simplify/GroupInverseRule.java [84:126]


  private CompiledTerm removePair(CompiledTerm term, int fstIndToRemove) {
    if (term instanceof VarTerm) {
      if (fstIndToRemove <= 1) return null;
      return term;
    }

    if (term instanceof CompositeTerm compositeTerm) {
      if (compositeTerm.matcher == mulMatcher) {
        var left = compositeTerm.subterms.get(0);
        var right = compositeTerm.subterms.get(1);
        int numLeavesLeft = countLeaves(left);
        var result = new CompositeTerm();
        result.matcher = mulMatcher;
        if (fstIndToRemove < numLeavesLeft) {
          var leftRes = removePair(compositeTerm.subterms.get(0), fstIndToRemove);
          if (leftRes == null) {
            return right;
          }
          result.subterms.add(leftRes);
          result.subterms.add(right);
          return result;
        }
        if (fstIndToRemove == numLeavesLeft) {
          var leftRes = removePair(compositeTerm.subterms.get(0), numLeavesLeft);
          var rightRes = removePair(compositeTerm.subterms.get(1), 0);
          if (leftRes == null) return rightRes;
          if (rightRes == null) return leftRes;
          result.subterms.add(leftRes);
          result.subterms.add(rightRes);
          return result;
        }
        var rightRes = removePair(compositeTerm.subterms.get(1), fstIndToRemove - numLeavesLeft);
        if (rightRes == null) {
          return left;
        }
        result.subterms.add(left);
        result.subterms.add(rightRes);
        return result;
      }
    }

    return null;
  }