fun doParseTokens()

in src/main/kotlin/org/arend/search/proof/ProofSearchQuery.kt [100:142]


    fun doParseTokens(position: Int, limit: Int): ParsingResult<PatternTree> {
        if (position == limit) {
            val range = if (tokens.isEmpty()) IntRange(0, 0) else if (limit == tokens.size) tokens[position - 1].range else tokens[position].range
            return ParsingResult.Error("Unexpected end of input", range)
        }
        val nodes: MutableList<Pair<PatternTree, PatternTree.Implicitness>> = mutableListOf()
        var currentPosition = position

        while (currentPosition != limit) {
            when (val tokenRepr = tokens[currentPosition].repr) {
                "_" -> nodes.add(PatternTree.Wildcard to PatternTree.Implicitness.EXPLICIT)
                "(" -> {
                    val closingBrace = braceMatcher[currentPosition]
                    when (val result = doParseTokens(currentPosition + 1, closingBrace)) {
                        is ParsingResult.OK -> {
                            nodes.add(result.value to PatternTree.Implicitness.EXPLICIT)
                            currentPosition = closingBrace
                        }
                        is ParsingResult.Error -> return result
                    }
                }
                ")" -> return ParsingResult.Error("Unexpected ')'", tokens[currentPosition].range)
                "{" -> {
                    val closingBrace = braceMatcher[currentPosition]
                    when (val result = doParseTokens(currentPosition + 1, closingBrace)) {
                        is ParsingResult.OK -> {
                            nodes.add(result.value to PatternTree.Implicitness.IMPLICIT)
                            currentPosition = closingBrace
                        }
                        is ParsingResult.Error -> return result
                    }
                }
                "}" -> return ParsingResult.Error("Unexpected '}'", tokens[currentPosition].range)
                else -> nodes.add(PatternTree.LeafNode(tokenRepr.split(".")) to PatternTree.Implicitness.EXPLICIT)
            }
            currentPosition += 1
        }
        return if (nodes.size == 1 && nodes[0].second != PatternTree.Implicitness.IMPLICIT) {
            ParsingResult.OK(nodes[0].first)
        } else {
            ParsingResult.OK(PatternTree.BranchingNode(nodes))
        }
    }