fun admitsPatternMatchingOnIdp()

in src/main/kotlin/org/arend/refactoring/ArendRefactoringUtils.kt [539:557]

• 19 lines of code
• 15 McCabe index (conditional complexity)

fun admitsPatternMatchingOnIdp(expr: CoreExpression,
                               caseParameters: CoreParameter?,
                               eliminatedBindings: Set<CoreBinding>? = null): PatternMatchingOnIdpResult {
    val equality = expr.toEquality() ?: return PatternMatchingOnIdpResult.INAPPLICABLE
    val leftBinding = (equality.defCallArguments[1] as? CoreReferenceExpression)?.binding
    val rightBinding = (equality.defCallArguments[2] as? CoreReferenceExpression)?.binding
    val leftNotEliminated = eliminatedBindings == null || !eliminatedBindings.contains(leftBinding)
    val rightNotEliminated = eliminatedBindings == null || !eliminatedBindings.contains(rightBinding)
    var leftSideOk = caseParameters == null && leftBinding != null && leftNotEliminated
    var rightSideOk = caseParameters == null && rightBinding != null && rightNotEliminated
    var caseP = caseParameters
    while (caseP?.hasNext() == true) {
        if (caseP == leftBinding && leftNotEliminated) leftSideOk = true
        if (caseP == rightBinding && rightNotEliminated) rightSideOk = true
        caseP = caseP.next
    }
    return if ((leftSideOk || rightSideOk) && leftBinding != rightBinding)
        PatternMatchingOnIdpResult.IDP else PatternMatchingOnIdpResult.DO_NOT_ELIMINATE
}