in src/main/kotlin/org/arend/quickfix/ExpectedConstructorQuickFix.kt [765:817]
fun printPattern(pattern: Pattern,
location: ArendCompositeElement,
occupiedVariables: List<Variable>,
newVariables: MutableList<String>,
renamer: Renamer): PatternPrintResult {
if (pattern.isAbsurd)
return PatternPrintResult("()", false, 1, false)
else {
val binding = pattern.binding
if (binding != null) {
val result = renamer.generateFreshName(binding, occupiedVariables + newVariables.map { VariableImpl(it) })
newVariables.add(result)
return PatternPrintResult(result, false, 1, false)
} else {
val integralNumber = ImplementMissingClausesQuickFix.getIntegralNumber(pattern)
if (integralNumber != null && abs(integralNumber) < Concrete.NumberPattern.MAX_VALUE)
return PatternPrintResult(integralNumber.toString(), false, 1, false)
else {
val constructor = pattern.constructor
val tupleMode = constructor == null
var constructorArgument: DependentLink = pattern.parameters
val locatedReferable = if (constructor != null) PsiLocatedReferable.fromReferable(constructor.referable) else null
var result = if (locatedReferable != null) {
val (name, namespaceCommand) = ResolveReferenceAction.getTargetName(locatedReferable, location)
namespaceCommand?.execute()
"$name "
} else "("
val patternIterator = pattern.subPatterns.iterator()
var complexity = 1
var containsClassConstructor = tupleMode && pattern.definition is ClassDefinition
while (patternIterator.hasNext()) {
val argumentPattern = patternIterator.next()
val argumentData = printPattern(argumentPattern, location, occupiedVariables, newVariables, renamer)
complexity += argumentData.complexity
if (argumentData.containsClassConstructor) containsClassConstructor = true
result += when {
!constructorArgument.isExplicit -> "{${argumentData.patternString}}"
!tupleMode && argumentData.requiresParentheses -> "(${argumentData.patternString})"
else -> argumentData.patternString
}
if (patternIterator.hasNext()) result += if (tupleMode) ", " else " "
if (constructorArgument.hasNext()) constructorArgument = constructorArgument.next
}
if (tupleMode) result += ")"
return PatternPrintResult(result, pattern.subPatterns.isNotEmpty() && !tupleMode, complexity, containsClassConstructor)
}
}
}
}