fun transformPostfixToPrefix()

in src/main/kotlin/org/arend/refactoring/ArendRefactoringUtils.kt [663:705]


fun transformPostfixToPrefix(psiFactory: ArendPsiFactory,
                             argumentOrFieldsAcc: PsiElement,
                             ipName: ArendIPName,
                             operatorConcrete: Concrete.Expression,
                             rangeData: HashMap<Concrete.SourceNode, TextRange>? = null,
                             rangeCallback: ((TextRange, Int) -> Unit)? = null): ArendArgumentAppExpr? {
    val argumentAppExpr = argumentOrFieldsAcc.parent as ArendArgumentAppExpr
    val nodes = argumentAppExpr.firstChild.siblings().map { it.node }.toList()
    val operatorRange = getBounds(operatorConcrete, nodes, rangeData)!!
    val psiElements = nodes.filter { operatorRange.contains(it.textRange) }.map { it.psi }
    val psiElementsRange = TextRange(psiElements.first().textRange.startOffset, psiElements.last().textRange.endOffset)
    val (resultingExpr, isLambda) = transformPostfixToPrefix1(argumentOrFieldsAcc, ipName, operatorConcrete, psiElements)

    val result: ArendExpr? = when {
        psiElements.size == nodes.size -> {
            val tupleExpr = surroundingTupleExpr(argumentAppExpr)
            val appExpr = psiFactory.createExpression(resultingExpr.trim()).descendantOfType<ArendArgumentAppExpr>()!!
            if (tupleExpr != null && tupleExpr.colon == null && isLambda) {
                val newPsi = appExpr.descendantOfType<ArendLamExpr>()!!
                rangeCallback?.invoke(argumentAppExpr.textRange, newPsi.textLength)
                argumentAppExpr.parent.replace(newPsi) as? ArendExpr
            } else {
                rangeCallback?.invoke(argumentAppExpr.textRange, appExpr.textLength)
                argumentAppExpr.replace(appExpr) as ArendArgumentAppExpr
            }
        }
        operatorRange.contains(nodes.first().textRange) -> {
            val atomFieldsAcc = psiFactory.createExpression("(${resultingExpr.trim()}) foo").descendantOfType<ArendAtomFieldsAcc>()!!
            rangeCallback?.invoke(psiElementsRange, atomFieldsAcc.textLength)
            val insertedExpr = argumentAppExpr.addAfter(atomFieldsAcc, psiElements.last())
            argumentAppExpr.deleteChildRange(psiElements.first(), psiElements.last())
            insertedExpr.descendantOfType<ArendArgumentAppExpr>()
        }
        else -> {
            val atom = psiFactory.createExpression("foo (${resultingExpr.trim()})").descendantOfType<ArendAtomArgument>()!!
            rangeCallback?.invoke(TextRange(psiElements.first().textRange.startOffset, psiElements.last().textRange.endOffset), atom.textLength)
            val insertedExpr = argumentAppExpr.addBefore(atom, psiElements.first())
            argumentAppExpr.deleteChildRange(psiElements.first(), psiElements.last())
            insertedExpr.descendantOfType<ArendArgumentAppExpr>()
        }
    }
    return if (isLambda) result?.descendantOfType(true) else result as ArendArgumentAppExpr
}