in src/main/kotlin/org/arend/quickfix/ImpossibleEliminationQuickFix.kt [44:159]
override fun invoke(project: Project, editor: Editor?, file: PsiFile?) {
val psiFactory = ArendPsiFactory(project)
val dataDefinition = error.defCall.definition as? DataDefinition ?: return
val definition = error.definition as DataLocatedReferable
val definitionPsi = definition.data?.element
val constructorPsi = cause.element?.ancestor<ArendConstructor>()
val typecheckedParameters = when {
constructorPsi != null -> {
(definition.typechecked as DataDefinition).constructors.firstOrNull { (it.referable as DataLocatedReferable).data?.element == constructorPsi }?.parameters
}
else -> definition.typechecked.parameters
} ?: return
val bodyPsi = (definitionPsi as? ArendFunctionDefinition<*>)?.body
val dataBodyPsi = (definitionPsi as? ArendDefData)?.dataBody
val elimPsi = when {
bodyPsi != null -> bodyPsi.elim
constructorPsi != null -> constructorPsi.elim
dataBodyPsi != null -> dataBodyPsi.elim
else -> null
}
val definitionParameters = toList(typecheckedParameters)
val ddEliminatedParameters = HashSet<DependentLink>()
for (constructor in dataDefinition.constructors) constructor.patterns?.let {
for (p in it.zip(toList(dataDefinition.parameters))) if (p.first !is BindingPattern) ddEliminatedParameters.add(p.second)
}
// determine matching expressions
val elimParams = error.myElimParams
if (error.myCaseExpressions != null) { // case
val stuckParameter = error.myParameters
val stuckParameterType = stuckParameter.type
val caseExprPsi = cause.element?.ancestor<ArendCaseExpr>()
val clausesListPsi = caseExprPsi?.withBody?.clauseList
if (caseExprPsi != null && stuckParameterType is DataCallExpression && clausesListPsi != null) {
val exprsToEliminate = stuckParameterType.defCallArguments.zip(toList(dataDefinition.parameters)).filter { ddEliminatedParameters.contains(it.second) }.toList()
val sampleDataCall = DataCallExpression.make(dataDefinition, error.defCall.levels, toList(dataDefinition.parameters).map { it.makeReference() })
val toActualParametersSubstitution = ExprSubstitution(); for (entry in stuckParameterType.defCallArguments.zip(toList(dataDefinition.parameters))) toActualParametersSubstitution.add(entry.second, entry.first)
val oldCaseArgs = caseExprPsi.caseArguments
val parameterToCaseArgMap = HashMap<DependentLink, ArendCaseArg>()
val parameterToCaseExprMap = ExprSubstitution()
val caseOccupiedLocalNames = HashSet<String>(); doInitOccupiedLocalNames(caseExprPsi, caseOccupiedLocalNames)
val bindingToCaseArgMap = HashMap<Binding, ArendCaseArg>()
if (error.myCaseExpressions != null) for (triple in toList(error.clauseParameters).zip(error.myCaseExpressions.zip(caseExprPsi.caseArguments))) {
parameterToCaseArgMap[triple.first] = triple.second.second
parameterToCaseExprMap.add(triple.first, triple.second.first)
}
val dependentCaseArg =
parameterToCaseArgMap[stuckParameter]!! //Safe as stuckParameter is one of error.clauseParameters
for (expression in exprsToEliminate) {
val exprSubst =
expression.first.accept(SubstVisitor(parameterToCaseExprMap, LevelSubstitution.EMPTY), null)
doInsertCaseArgs(psiFactory, caseExprPsi, oldCaseArgs, expression.second, exprSubst, dependentCaseArg, error.myCaseExpressions, caseOccupiedLocalNames, bindingToCaseArgMap,null)
}
val toInsertedBindingsSubstitution = ExprSubstitution(); for (e in bindingToCaseArgMap) toInsertedBindingsSubstitution.add(e.key, ReferenceExpression(UntypedDependentLink(e.value.referable!!.name)))
val typeQualification = sampleDataCall.accept(SubstVisitor(toInsertedBindingsSubstitution, LevelSubstitution.EMPTY), null).accept(SubstVisitor(toActualParametersSubstitution, LevelSubstitution.EMPTY), null)
doWriteTypeQualification(psiFactory, typeQualification, dependentCaseArg)
doInsertPatternPrimers(psiFactory, clausesListPsi, caseExprPsi, oldCaseArgs, bindingToCaseArgMap, null)
}
} else
if (elimParams != null && elimPsi != null) { // elim
val clausesListPsi = when {
bodyPsi is ArendFunctionBody -> bodyPsi.functionClauses?.clauseList
constructorPsi != null -> constructorPsi.clauses
dataBodyPsi != null -> dataBodyPsi.constructorClauseList
else -> null
}
val clauseToDefinitionMap = HashMap<Variable, Variable>()
if (error.substitution != null) for (variable in error.substitution.keys) {
val binding = (error.substitution.get(variable) as? ReferenceExpression)?.binding
if (binding != null && variable is Binding) clauseToDefinitionMap[binding] = variable
}
val definitionParametersToEliminate = HashSet<Variable>()
val exprsToEliminate = toList(dataDefinition.parameters).zip(error.defCall.defCallArguments)
.filter { ddEliminatedParameters.contains(it.first) }.map { it.second }.toList()
for (expr in exprsToEliminate) if (expr is ReferenceExpression) (clauseToDefinitionMap[expr.binding]
?: expr.binding).let { definitionParametersToEliminate.add(it) }
definitionParametersToEliminate.removeAll(elimParams.toSet())
val paramsMap = HashMap<DependentLink, ArendRefIdentifier>()
for (e in elimParams.zip(elimPsi.refIdentifierList)) paramsMap[e.first] = e.second
ExpectedConstructorQuickFix.doInsertElimVars(
psiFactory,
definitionParameters,
definitionParametersToEliminate,
elimPsi,
paramsMap
)
if (clausesListPsi != null) for (transformedClause in clausesListPsi)
ExpectedConstructorQuickFix.doInsertPrimers(
psiFactory,
transformedClause,
definitionParameters,
elimParams,
definitionParametersToEliminate,
null
) { p -> p.name }
}
val clause = (error.cause.data as? PsiElement)?.ancestors?.firstOrNull{ it is ArendClause || it is ArendConstructorClause }
if (clause != null) doRemoveClause(clause)
}