override fun doEliminateAndInitializePrimers()

in src/main/kotlin/org/arend/quickfix/ExpectedConstructorQuickFix.kt [681:747]


            override fun doEliminateAndInitializePrimers(expectedConstructorErrorEntries: List<ElimWithErrorEntry>, clausesListPsi: List<Abstract.Clause>?, definitionParameters: List<DependentLink>, elimParams: List<DependentLink>) {
                if (elimParams.isNotEmpty() && elimPsi != null) { //elim
                    val paramsMap = HashMap<DependentLink, ArendRefIdentifier>()
                    for (e in elimParams.zip(elimPsi.refIdentifierList)) paramsMap[e.first] = e.second
                    for (ecEntry in expectedConstructorErrorEntries) for (e in elimParams.zip((ecEntry.clause.data as Abstract.Clause).patterns)) (e.second as? ArendPattern)?.let { ecEntry.patternPrimers[e.first] = it}

                    definitionParametersToEliminate.removeAll(elimParams.toSet())

                    doInsertElimVars(psiFactory, definitionParameters, definitionParametersToEliminate, elimPsi, paramsMap)

                    if (clausesListPsi != null) for (transformedClause in clausesListPsi)
                        doInsertPrimers(psiFactory, transformedClause, definitionParameters, elimParams, definitionParametersToEliminate, clauseToEntryMap[transformedClause]?.patternPrimers) { p -> p.name }
                } else if (clausesListPsi != null) {
                    for (ecEntry in expectedConstructorErrorEntries) {
                        val currentClause = ecEntry.clause.data as ArendClause
                        val parameterIterator = definitionParameters.iterator()
                        val patternIterator = currentClause.patterns.iterator()
                        val patternMatchedParameters = LinkedHashSet<Variable>()
                        while (parameterIterator.hasNext() && patternIterator.hasNext()) {
                            val pattern = patternIterator.next()
                            var parameter: DependentLink? = parameterIterator.next()
                            if (pattern.isExplicit) while (parameter != null && !parameter.isExplicit)
                                parameter = if (parameterIterator.hasNext()) parameterIterator.next() else null
                            if (parameter != null && pattern.isExplicit == parameter.isExplicit) {
                                patternMatchedParameters.add(parameter)
                                ecEntry.patternPrimers[parameter] = pattern
                            }
                        }

                        val newVars = definitionParametersToEliminate.minus(patternMatchedParameters)
                        val newVarsPlusPrecedingImplicitVars = HashSet<Variable>(newVars)
                        var implicitFlag = false
                        for (param in definitionParameters.reversed()) {
                            if (implicitFlag && !param.isExplicit) newVarsPlusPrecedingImplicitVars.add(param)
                            if (newVars.contains(param) && !param.isExplicit) implicitFlag = true
                            if (param.isExplicit) implicitFlag = false
                        }

                        doInsertPrimers(psiFactory, currentClause, definitionParameters, ArrayList(patternMatchedParameters), newVarsPlusPrecedingImplicitVars, ecEntry.patternPrimers) { binding ->
                            val builder = StringBuilder()
                            if (binding is DependentLink && !binding.isExplicit) builder.append("{")
                            builder.append(if (newVars.contains(binding)) binding.name else "_")
                            if (binding is DependentLink && !binding.isExplicit) builder.append("}")
                            builder.toString()
                        }
                    }
                }

                for (ecEntry in expectedConstructorErrorEntries) {
                    for (p in ecEntry.clauseParametersToSpecialize) {
                        when (val descriptor = ecEntry.matchData[p]) {
                            is ExplicitNamePattern -> ecEntry.patternPrimers[p] = descriptor.bindingPsi.let { if (it is ArendPattern) it else it.parent as ArendPattern }
                            is ImplicitConstructorPattern -> {
                                val positionKey = Pair(descriptor.enclosingNode, descriptor.followingParameter)
                                var positionList = ecEntry.insertData[positionKey]
                                if (positionList == null) {
                                    positionList = ArrayList()
                                    ecEntry.insertData[positionKey] = positionList
                                }
                                positionList.add(Pair(descriptor.implicitArgCount, p))
                            }
                        }
                    }

                    insertPrimers(psiFactory, ecEntry.insertData) { a, b -> ecEntry.patternPrimers[a] = b }
                }
            }