fun generateProofSearchResults()

in src/main/kotlin/org/arend/search/proof/ProofSearchUtils.kt [41:111]
65 lines of code
11 McCabe index (conditional complexity)

fun generateProofSearchResults(
    project: Project,
    pattern: String,
): Sequence<ProofSearchEntry?> = sequence {
    val settings = ProofSearchUISettings(project)
    val query = (ProofSearchQuery.fromString(pattern) as? ParsingResult.OK<ProofSearchQuery>)?.value
        ?: return@sequence
    val matcher = ArendExpressionMatcher(query)

    val listedIdentifiers = query.getAllIdentifiers()

    val keys = DumbService.getInstance(project).runReadActionInSmartMode(Computable {
        StubIndex.getInstance().getAllKeys(ArendDefinitionIndex.KEY, project)
    })

    val searchScope = if (listedIdentifiers.isNotEmpty()) {
        val scopes = collectSearchScopes(listedIdentifiers, GlobalSearchScope.allScope(project).isSearchInLibraries, project)
        runReadAction {
            scopes.map { GlobalSearchScope.fileScope(project, it) }.reduce(GlobalSearchScope::union)
        }
    } else {
        GlobalSearchScope.allScope(project)
    }

    val concreteProvider = PsiConcreteProvider(project, DummyErrorReporter.INSTANCE, null)

    var idleCounter = 0

    for (definitionName in keys) {
        val list = SmartList<ProofSearchEntry>()
        runReadAction {
            StubIndex.getInstance().processElements(
                ArendDefinitionIndex.KEY,
                definitionName,
                project,
                searchScope,
                PsiReferable::class.java
            ) { def ->
                if (!settings.checkAllowed(def)) return@processElements true
                if (def !is ReferableBase<*>) return@processElements true
                val (parameters, codomain, info) = getSignature(concreteProvider, def, query.shouldConsiderParameters())
                    ?: return@processElements true
                val (parameterResults, codomainResults) = matcher.match(parameters, codomain, def.scope, def) ?: return@processElements true
                val parameterRangesRegistry = mutableMapOf<Int, List<TextRange>>()
                val rangeComputer = caching { e : Concrete.Expression -> if (e is Concrete.ReferenceExpression && e.referent is ArendDefData) (e.referent as ArendDefData).nameIdentifier!!.textRange else rangeOfConcrete(e) }
                for ((parameterConcrete, ranges) in parameterResults) {
                    val index = parameters.indexOf(parameterConcrete)
                    val existing = parameterRangesRegistry.getOrDefault(index, emptyList())
                    parameterRangesRegistry[index] = existing + ranges.map { rangeComputer(it).shiftLeft(rangeComputer(parameterConcrete).startOffset) }
                }
                val codomainRange = codomainResults.map { rangeComputer(it).shiftLeft(rangeComputer(codomain).startOffset) }
                list.add(ProofSearchEntry(def,
                    info.value.copy(
                        parameters = info.value.parameters.mapIndexedNotNull { index, data -> data.takeIf { index in parameterRangesRegistry }?.copy(match = parameterRangesRegistry[index]!!) },
                        codomain = info.value.codomain.copy(match = codomainRange))))
                true
            }
        }
        if (list.isNotEmpty()) {
            for (def in list) {
                yield(def)
            }
        } else {
            idleCounter += 1
            if (idleCounter >= 50) {
                idleCounter = 0
                yield(null)
            }
        }
    }
}