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;
}