in src/main/kotlin/org/arend/quickfix/ExpectedConstructorQuickFix.kt [878:922]
fun insertPrimers(psiFactory: ArendPsiFactory, insertData: HashMap<Pair<PsiElement, PsiElement?>, MutableList<Pair<Int, Variable>>>, callback: (Variable, ArendPattern) -> Unit) {
for (insertDataEntry in insertData) {
val toInsertList = insertDataEntry.value
var enclosingNode = insertDataEntry.key.first as ArendPattern
val position = insertDataEntry.key.second as? ArendPattern
var skippedParams = 0
toInsertList.sortBy { it.first }
for (entry in toInsertList) {
var patternLine = ""
for (i in 0 until entry.first - skippedParams) patternLine += " {_}"
patternLine += " {${entry.second.name}}"
val atomPattern = psiFactory.createPattern(patternLine)
val templateList = atomPattern.sequence.takeIf { it.isNotEmpty() } ?: listOf(atomPattern)
if (position == null) {
enclosingNode = if (enclosingNode.parent is ArendPattern && enclosingNode.singleReferable != null && !enclosingNode.isTuplePattern) {
enclosingNode.replace(psiFactory.createPattern("(${enclosingNode.text})")) as ArendPattern
} else {
enclosingNode
}
if (!enclosingNode.isExplicit || enclosingNode.isTuplePattern && enclosingNode.sequence.size == 1) {
val rightBrace = enclosingNode.lastChild
val first = enclosingNode.addRangeBefore(templateList.first(), templateList.last(), rightBrace)
enclosingNode.addBefore(psiFactory.createWhitespace(" "), first)
(rightBrace.findPrevSibling() as? ArendPattern)?.let { callback.invoke(entry.second, it) }
} else {
if (enclosingNode.sequence.isEmpty()) {
enclosingNode = enclosingNode.replace(psiFactory.createPattern("${enclosingNode.text}$patternLine")) as ArendPattern
} else {
val first = enclosingNode.addRangeAfter(templateList.first(), templateList.last(), enclosingNode.sequence.last())
enclosingNode.addBefore(psiFactory.createWhitespace(" "), first)
}
enclosingNode.sequence.last().let { callback.invoke(entry.second, it) }
}
} else {
val actualPosition = absorbParenthesesUp(position)
enclosingNode.addRangeBefore(templateList.first(), templateList.last(), actualPosition)
enclosingNode.addBefore(psiFactory.createWhitespace(" "), actualPosition)
(actualPosition.findPrevSibling() as? ArendPattern)?.let { callback.invoke(entry.second, it) }
}
skippedParams = entry.first + 1
}
}
}