fun parameterText()

in src/main/kotlin/org/arend/refactoring/changeSignature/ArendParametersInfo.kt [38:98]


    fun parameterText(): String {
        data class TeleEntry(val typeText: String?, val isExplicit: Boolean, val isCoerce: Boolean, val isClassifying: Boolean, val isProperty: Boolean, val accessModifier: org.arend.term.group.AccessModifier = org.arend.term.group.AccessModifier.PUBLIC, val parameterNames: MutableList<Pair<String?, Int>>)
        val teleEntries = ArrayList<TeleEntry>()
        val associatedWhitespaceData = HashSet<Pair<TeleEntry, TeleWhitespaceData>>()
        val usedWhitespaceData = HashSet<TeleWhitespaceData>()

        for (parameter in parameterInfo) {
            if (teleEntries.isEmpty() || teleEntries.last().typeText != parameter.typeText || teleEntries.last().isExplicit != parameter.isExplicit() || parameter.isCoerce || parameter.isClassifying)
                teleEntries.add(TeleEntry(parameter.typeText, parameter.isExplicit(), parameter.isCoerce, parameter.isClassifying, parameter.isProperty, parameter.accessModifier, Collections.singletonList(
                    Pair(parameter.name, parameter.oldIndex)
                ).toMutableList())) else
                teleEntries.last().parameterNames.add(Pair(parameter.name, parameter.oldIndex))
            val data = parameterToTeleWhitespaceData[parameter.oldIndex]
            if (data != null && !usedWhitespaceData.contains(data)) {
                usedWhitespaceData.add(data)
                associatedWhitespaceData.add(Pair(teleEntries.last(), data))
            }
        }

        val newTeles = StringBuilder()
        for (entry in teleEntries) {
            val whitespaceData = associatedWhitespaceData.firstOrNull { it.first == entry }?.second
            newTeles.append(whitespaceData?.beforeTeleWhitespace ?: " ")
            val parameterNames = StringBuilder()
            for ((i, p) in entry.parameterNames.withIndex()) {
                var space = parameterWhitespaceData[p.second] ?: " "
                if (i == 0 && space.startsWith(" ")) space = space.drop(1)
                if (i > 0 && space.isEmpty()) space = " "
                parameterNames.append(space)
                parameterNames.append(p.first.let{ if (it.isNullOrEmpty()) ArendElementTypes.UNDERSCORE else it })
            }

            val referableAllowsTypeTeles = locatedReferable is ArendConstructor || locatedReferable is ArendDefData
            val printParameterNames = parameterNames.toString() != "_" || !referableAllowsTypeTeles
            val printSurroundingParens = !entry.isExplicit || entry.typeText == null || printParameterNames
            if (printSurroundingParens) newTeles.append (if (entry.isExplicit) ArendElementTypes.LPAREN else ArendElementTypes.LBRACE)
            when (entry.accessModifier) {
                AccessModifier.PRIVATE -> newTeles.append("${ArendElementTypes.PRIVATE_KW} ")
                AccessModifier.PROTECTED -> newTeles.append("${ArendElementTypes.PROTECTED_KW} ")
                else -> {}
            }
            if (entry.isCoerce) newTeles.append("${ArendElementTypes.COERCE_KW} ") else
                if (entry.isClassifying) newTeles.append("${ArendElementTypes.CLASSIFYING_KW} ") else
                    if (entry.isProperty) newTeles.append("${ArendElementTypes.PROPERTY_KW} ")


            if (entry.typeText != null) {
                if (printParameterNames) {
                    newTeles.append(parameterNames.toString())
                    newTeles.append(whitespaceData?.colonText ?: " ${ArendElementTypes.COLON} ")
                }
                newTeles.append(if (entry.typeText.trim().contains(" ") && !printParameterNames && !printSurroundingParens) "(${entry.typeText})" else entry.typeText)
            } else {
                newTeles.append(parameterNames.toString())
            }

            newTeles.append(whitespaceData?.afterTypeText ?: "")
            if (printSurroundingParens) newTeles.append (if (entry.isExplicit) ArendElementTypes.RPAREN else ArendElementTypes.RBRACE)
        }
        return newTeles.toString()
    }