override fun calculateEntriesToEliminate()

in src/main/kotlin/org/arend/quickfix/ExpectedConstructorQuickFix.kt [503:539]


            override fun calculateEntriesToEliminate(ecEntry: CaseErrorEntry) {
                // STEP 2C: Calculate the list of expressions which need to be eliminated or specialized
                val cmd = ecEntry.caseMatchData
                if (cmd != null) {
                    val stuckParameter = ecEntry.error.parameter
                    val correspondingCaseArg = parameterToCaseArgMap[stuckParameter]!! //Safe as stuckParameter is one error.clauseParameters
                    val sampleQualification = caseTypeQualifications[correspondingCaseArg]
                    if (sampleQualification == null) {
                        caseTypeQualifications[correspondingCaseArg] = cmd.first
                        for (mr in cmd.second) {
                            caseBindings[mr.binding] = Pair(correspondingCaseArg, mr.expression)
                            val mrPattern = mr.pattern
                            if (mrPattern !is BindingPattern && mrPattern is ExpressionPattern) ecEntry.correctedSubsts[mr.binding] = mrPattern
                        }
                    } else {
                        val substitution = ExprSubstitution()
                        sBELoop@for (sampleBindingEntry in caseBindings) for (mr in cmd.second) {
                            val expr1 = mr.expression
                            val expr2 = sampleBindingEntry.value.second
                            if (expr1 == expr2) {
                                substitution.add(mr.binding, ReferenceExpression(sampleBindingEntry.key))
                                continue@sBELoop
                            }
                        }
                        val cmdType = cmd.first.accept(SubstVisitor(substitution, LevelSubstitution.EMPTY), null)
                        if (cmdType != sampleQualification) {
                            errorHintBuffer.append("Calculated type expressions for the case argument do not match between the clauses")
                            errorHintBuffer.append("Case argument: ${parameterToCaseArgMap[stuckParameter]?.text}")
                            reportError(ecEntry, ecEntry.clause.data as Abstract.Clause)
                        } else for (mr in cmd.second) {
                            val matchedCaseBinding = (substitution.get(mr.binding) as? ReferenceExpression)?.binding
                            val mrPattern = mr.pattern
                            if (matchedCaseBinding != null && mrPattern !is BindingPattern && mrPattern is ExpressionPattern) ecEntry.correctedSubsts[matchedCaseBinding] = mrPattern
                        }
                    }
                }
            }