fun insertPrimers()

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