in src/main/kotlin/org/arend/refactoring/ArendSubExprUtils.kt [248:291]
fun collectArendExprs(
parent: PsiElement,
range: TextRange
): Pair<Abstract.Expression, List<Abstract.BinOpSequenceElem>>? {
val head: PsiElement
val tail: Sequence<PsiElement>
if (range.isEmpty) {
when (val firstExpr = parent.linearDescendants.filterIsInstance<Abstract.Expression>().lastOrNull()
?: parent.childrenWithLeaves.filterIsInstance<Abstract.Expression>().toList().takeIf { it.size == 1 }?.first()) {
is ArendTuple -> {
val tupleExprList = firstExpr.tupleExprList
head = tupleExprList.firstOrNull() ?: return null
tail = tupleExprList.asSequence().drop(1)
}
is ArendTupleExpr -> {
head = firstExpr.expr
tail = firstExpr.type?.let { sequenceOf(it) } ?: emptySequence()
}
null -> return null
else -> return firstExpr to emptyList()
}
} else {
val exprSeq = parent.childrenWithLeaves
.dropWhile { it.textRange.endOffset < range.startOffset }
.takeWhile { it.textRange.startOffset < range.endOffset }
.filter { it !is PsiWhiteSpace && it !is LeafPsiElement }
head = (exprSeq.firstOrNull() ?: return null)
tail = exprSeq.drop(1)
}
if (tail.none()) {
val subCollected = collectArendExprs(head, range)
if (subCollected != null) {
val (_, tails) = subCollected
if (tails.isNotEmpty()) return subCollected
}
return if (head is Abstract.Expression) head to emptyList()
else null
} else return when (val headExpr = head.linearDescendants.filterIsInstance<Abstract.Expression>().lastOrNull()) {
null -> null
else -> headExpr to tail.mapNotNull {
it.linearDescendants.filterIsInstance<Abstract.BinOpSequenceElem>().firstOrNull()
}.toList()
}
}