fun correspondedSubExpr()

in src/main/kotlin/org/arend/refactoring/ArendSubExprUtils.kt [115:169]
49 lines of code
9 McCabe index (conditional complexity)

fun correspondedSubExpr(range: TextRange, file: PsiFile, project: Project): SubExprResult {
    val exprAncestor = selectedExpr(file, range) { throw SubExprException(it) }

    val (head, tail) = collectArendExprs(exprAncestor.parent, range)
        ?: throw SubExprException("cannot find a suitable concrete expression")
    val subExpr =
        if (tail.isNotEmpty()) {
            val data = if (exprAncestor.textRange == range) exprAncestor else null
            parseBinOp(data, head, tail)
        }
        else SyntacticDesugarVisitor.desugar(ConcreteBuilder.convertExpression(head), DummyErrorReporter.INSTANCE)
    val resolver = subExpr.underlyingReferenceExpression?.let { refExpr -> refExpr.data?.let { MyResolverListener(it) } }

    // if (possibleParent is PsiWhiteSpace) return "selected text are whitespaces"
    val psiDef = exprAncestor.ancestor<TCDefinition>()
        ?: throw SubExprException("selected text is not in a definition")
    val concreteDef = PsiConcreteProvider(project, DummyErrorReporter.INSTANCE, null, true, resolver).getConcrete(psiDef) as? Concrete.Definition
    val body = concreteDef?.let { it to psiDef }

    val injectionContext = (file as? ArendFile)?.injectionContext
    val injectionHost = injectionContext?.containingFile as? PsiInjectionTextFile
    val errors: List<SubExprError>
    val result = (if (injectionHost != null) {
        val index = when (injectionHost.injectedExpressions.size) {
            0 -> null
            1 -> 0
            else -> InjectedLanguageManager.getInstance(project).getInjectedPsiFiles(injectionContext)?.indexOfFirst { it.first == file }
        }
        val injectedExpr = if (index != null) injectionHost.injectedExpressions[index] else null
        val cExpr = (psiDef as? ArendDefFunction)?.body?.expr?.let { ConcreteBuilder.convertExpression(it) }
        if (injectedExpr != null && cExpr != null && index != null && index < injectionHost.injectedExpressions.size) {
            val scope = CachingScope.make(injectionHost.scope)
            val subExprVisitor = CorrespondedSubExprVisitor(resolver?.result ?: subExpr)
            errors = subExprVisitor.errors
            SyntacticDesugarVisitor.desugar(cExpr.accept(ExpressionResolveNameVisitor(ArendReferableConverter, scope, null, DummyErrorReporter.INSTANCE, null), null), DummyErrorReporter.INSTANCE).accept(subExprVisitor, injectedExpr)
        } else {
            errors = emptyList()
            null
        }
    } else {
        concreteDef ?: throw SubExprException("selected text is not in a definition")
        val def = psiDef.tcReferable?.typechecked
            ?: throw SubExprException("underlying definition is not type checked")
        val subDefVisitor = CorrespondedSubDefVisitor(resolver?.result ?: subExpr)
        errors = subDefVisitor.exprError
        concreteDef.accept(subDefVisitor, def)
    }) ?: throw SubExprException(buildString {
        append("cannot find a suitable subexpression")

        if (errors.any { it.kind == SubExprError.Kind.MetaRef })
            append(" (maybe because you're using meta defs)")
    }, body)

    return SubExprResult(result.proj1, resolver?.originalExpr ?: result.proj2, exprAncestor)
}