fun collectArendExprs()

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()
    }
}