in src/main/kotlin/org/arend/quickfix/ImplementMissingClausesQuickFix.kt [115:182]
fun insertClauses(psiFactory: ArendPsiFactory, cause: ArendCompositeElement, clauses: List<ArendClause>) {
var primerClause: ArendClause? = null// a "primer" clause which is needed only to simplify insertion of proper clauses
val anchor = when (cause) {
is ArendCoClauseDef -> {
val coClauseBody = cause.body
?: (cause.addAfter(psiFactory.createCoClauseBody(), cause.lastChild) as ArendFunctionBody)
val elim = coClauseBody.elim
?: coClauseBody.add(psiFactory.createCoClauseBody().descendantOfType<ArendElim>()!!)
if (coClauseBody.lbrace == null)
insertPairOfBraces(psiFactory, elim)
coClauseBody.clauseList.lastOrNull() ?: coClauseBody.lbrace ?: cause.lastChild
}
is ArendFunctionDefinition<*> -> {
val fBody = cause.body
val fClauses = if (fBody != null && fBody.kind != ArendFunctionBody.Kind.COCLAUSE) fBody.functionClauses else null
if (fBody != null) {
val lastChild = fBody.lastChild
if (fClauses != null) {
fClauses.clauseList.lastOrNull() ?: fClauses.lbrace ?: throw IllegalStateException()
} else {
val newClauses = psiFactory.createFunctionClauses()
val insertedClauses = lastChild.parent?.addAfter(newClauses, lastChild) as ArendFunctionClauses
lastChild.parent?.addAfter(psiFactory.createWhitespace(" "), lastChild)
primerClause = insertedClauses.lastChild as? ArendClause
primerClause
}
} else {
val newBody = psiFactory.createFunctionClauses().parent as ArendFunctionBody
val lastChild = cause.returnExpr ?: cause.parameters.lastOrNull() ?: throw IllegalStateException()
cause.addAfter(newBody, lastChild)
cause.addAfter(psiFactory.createWhitespace(" "), lastChild)
primerClause = cause.body?.functionClauses?.lastChild as? ArendClause
primerClause
}
}
is ArendCaseExpr -> {
val body = cause.withBody
val caseExprAnchor = cause.returnExpr ?: cause.caseArguments.lastOrNull()
body?.clauseList?.lastOrNull() ?: (body?.lbrace ?: (
body?.let {
insertPairOfBraces(psiFactory, it.withKw)
body.lbrace
} ?: (cause.addAfter(psiFactory.createWithBody(), caseExprAnchor) as ArendWithBody).lbrace))
}
is ArendLongName -> {
findWithBodyAnchor(cause.ancestor(), psiFactory)
}
is ArendWithBody -> findWithBodyAnchor(cause.parent as? ArendNewExpr, psiFactory)
else -> null
}
val anchorParent = anchor?.parent
for (clause in clauses) if (anchorParent != null) {
val pipe = clause.findPrevSibling()
var currAnchor: PsiElement? = null
if (pipe != null) currAnchor = anchorParent.addAfter(pipe, anchor)
anchorParent.addBefore(psiFactory.createWhitespace("\n"), currAnchor)
currAnchor = anchorParent.addAfter(clause, currAnchor)
anchorParent.addBefore(psiFactory.createWhitespace(" "), currAnchor)
}
primerClause?.let {
it.findPrevSibling()?.delete()
it.delete()
}
}