in src/main/kotlin/org/arend/quickfix/ImplementMissingClausesQuickFix.kt [46:102]
override fun invoke(project: Project, editor: Editor?, file: PsiFile?) {
val psiFactory = ArendPsiFactory(project)
val element = causeRef.element ?: return
clauses.clear()
val definedVariables: List<Variable> = collectDefinedVariables(element)
missingClausesError.setMaxListSize(service<ArendSettings>().clauseActualLimit)
for (clause in missingClausesError.limitedMissingClauses.reversed()) if (clause != null) {
val filters = HashMap<CorePattern, List<Boolean>>()
val previewResults = ArrayList<PatternKind>()
val recursiveTypeUsagesInBindings = ArrayList<Int>()
val elimMode = missingClausesError.isElim
run {
var parameter: CoreParameter? = if (!elimMode) missingClausesError.parameters else null
val iterator = clause.iterator()
var i = 0
while (iterator.hasNext()) {
val pattern = iterator.next()
val recTypeUsagesInPattern = HashSet<CorePattern>()
val sampleParameter = if (elimMode) missingClausesError.eliminatedParameters[i] else parameter?.binding
previewResults.add(previewPattern(pattern, filters, if (parameter == null || parameter.isExplicit) Companion.Braces.NONE else Companion.Braces.BRACES, recTypeUsagesInPattern, (sampleParameter?.typeExpr as? DefCallExpression)?.definition))
recursiveTypeUsagesInBindings.add(recTypeUsagesInPattern.size)
parameter = if (parameter != null && parameter.hasNext()) parameter.next else null
i++
}
}
val topLevelFilter = computeFilter(previewResults)
val patternStrings = ArrayList<String>()
var containsEmptyPattern = false
run {
val iterator = clause.iterator()
val recursiveTypeUsagesInBindingsIterator = recursiveTypeUsagesInBindings.iterator()
var parameter2: CoreParameter? = if (!elimMode) missingClausesError.parameters else null
val clauseBindings: MutableList<Variable> = definedVariables.toMutableList()
val eliminatedBindings = HashSet<CoreBinding>()
var i = 0
while (iterator.hasNext()) {
val pattern = iterator.next()
val nRecursiveBindings = recursiveTypeUsagesInBindingsIterator.next()
val braces = if (parameter2 == null || parameter2.isExplicit) Companion.Braces.NONE else Companion.Braces.BRACES
val sampleParameter = if (elimMode) missingClausesError.eliminatedParameters[i] else parameter2!!.binding
val patternData = doTransformPattern(pattern, element, project, filters, braces, clauseBindings, sampleParameter, nRecursiveBindings, eliminatedBindings, missingClausesError)
patternStrings.add(patternData.first)
containsEmptyPattern = containsEmptyPattern || patternData.second
parameter2 = if (parameter2 != null && parameter2.hasNext()) parameter2.next else null
i++
}
}
clauses.add(psiFactory.createClause(concat(patternStrings, topLevelFilter), containsEmptyPattern))
}
insertClauses(psiFactory, element, clauses)
}