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