fun getIntegralNumber()

in src/main/kotlin/org/arend/quickfix/ImplementMissingClausesQuickFix.kt [254:270]


        fun getIntegralNumber(pattern: CorePattern): Int? {
            val definition = pattern.constructor
            val isSuc = definition == Prelude.SUC
            val isFinSuc = definition == Prelude.FIN_SUC
            val isPos = definition == Prelude.POS
            val isNeg = definition == Prelude.NEG
            val firstArgument = (pattern as? ConstructorExpressionPattern)?.dataTypeArguments?.firstOrNull()
            if (isSuc || isFinSuc || isPos || isNeg) {
                val number = if (isFinSuc && (firstArgument as? SmallIntegerExpression)?.isOne == true) 0 else
                    getIntegralNumber(pattern.subPatterns.firstOrNull() ?: return null)
                if ((isSuc || isFinSuc) && number != null) return number + 1
                if (isPos && number != null) return number
                if (isNeg && number != null && number != 0) return -number
                return null
            } else if (definition == Prelude.ZERO || definition == Prelude.FIN_ZERO) return 0
            return null
        }