override fun computeMatchingPatterns()

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