in src/main/kotlin/org/arend/quickfix/ExpectedConstructorQuickFix.kt [576:627]
override fun computeMatchingPatterns(ecEntry: ElimWithErrorEntry, definitionParameters: List<DependentLink>, elimParams: List<DependentLink>) {
val parameterType = ecEntry.error.parameter?.type
val currentClause = ecEntry.clause.data as Abstract.Clause
val concreteCurrentClause = ecEntry.clause
// STEP 1: Compute matching patterns
val rawSubsts = HashMap<Binding, ExpressionPattern>()
if (parameterType !is DataCallExpression || ExpressionMatcher.computeMatchingPatterns(parameterType, ecEntry.constructorTypechecked, ExprSubstitution(), rawSubsts) == null) {
errorHintBuffer.append("ExpectedConstructorError quickfix was unable to compute matching patterns for the parameter ${ecEntry.error.parameter}\n")
reportError(ecEntry, currentClause)
return
}
// STEP 2: Calculate lists of variables which need to be eliminated or specialized
val clauseParameters = DependentLink.Helper.toList(ecEntry.error.patternParameters)
val definitionToClauseMap = HashMap<Variable, Variable>()
val clauseToDefinitionMap = HashMap<Variable, Variable>()
for (variable in ecEntry.substitution.keys) {
val binding = (ecEntry.substitution.get(variable) as? ReferenceExpression)?.binding
if (binding != null && variable is Binding && definitionParameters.contains(variable) && clauseParameters.contains(binding)) {
definitionToClauseMap[variable] = binding
clauseToDefinitionMap[binding] = variable
}
}
//This piece of code filters out trivial substitutions and also ensures that the key of each substitution is either an element of definitionParametersToEliminate or clauseParametersToSpecialize
for (subst in rawSubsts) if (subst.value !is BindingPattern) {
if (definitionParameters.contains(subst.key)) {
ecEntry.clauseDefinitionParametersToEliminate.add(subst.key)
ecEntry.correctedSubsts[subst.key] = subst.value
} else {
val localClauseBinding =
if (clauseParameters.contains(subst.key)) subst.key else (ecEntry.substitution[subst.key] as? ReferenceExpression)?.binding
if (localClauseBinding != null) {
val definitionBinding = clauseToDefinitionMap[localClauseBinding]
if (definitionBinding != null && definitionParameters.contains(definitionBinding)) {
ecEntry.correctedSubsts[definitionBinding] = subst.value
ecEntry.clauseDefinitionParametersToEliminate.add(definitionBinding)
} else if (clauseParameters.contains(localClauseBinding)) {
ecEntry.correctedSubsts[localClauseBinding] = subst.value
ecEntry.clauseParametersToSpecialize.add(localClauseBinding)
}
}
}
}
//STEP 3: Match clauseParameters with currentClause PSI
if (!matchConcreteWithWellTyped(currentClause as PsiElement, concreteCurrentClause.patterns, prepareExplicitnessMask(definitionParameters, elimParams), clauseParameters.iterator(), ecEntry.matchData) ||
ecEntry.clauseParametersToSpecialize.any { ecEntry.matchData[it] == null })
throw IllegalStateException("ExpectedConstructorError quickfix failed to calculate the correspondence between psi and concrete name patterns")
}