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