override fun invoke()

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