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
}