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))
}
}