From 6a68eeaa726489f3e69d8a0e71237f3132ab6d8d Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 20 May 2026 09:59:33 -0700 Subject: [PATCH] perf: use `String.compare` in `ConfigEval` decision tree This PR improves performance of matching configuration items by using `String.compare` to implement the decision tree for interpreting configuration option names. --- src/Lean/Elab/ConfigEval/Util.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Lean/Elab/ConfigEval/Util.lean b/src/Lean/Elab/ConfigEval/Util.lean index f4418b7c720f..d75f9e0b4bf2 100644 --- a/src/Lean/Elab/ConfigEval/Util.lean +++ b/src/Lean/Elab/ConfigEval/Util.lean @@ -24,16 +24,19 @@ partial def makeStringMatcher (discr : Ident) (cases : Array (String × Term)) ( build 0 cases.size cases where build (start stop : Nat) (cases : Array (String × Term)) : TermElabM Term := do - if stop - start ≤ 5 then + if stop - start ≤ 2 then -- Switch to if/else chains once we get to a small number of options. cases[start:stop].foldrM (init := onFail) fun (s, body) res => `(if $discr == $(quote s) then $body else $res) else let mid := (start + stop) / 2 - let (s, _) := cases[mid]! + let (s, body) := cases[mid]! let low ← build start mid cases - let high ← build mid stop cases - `(if $discr < $(quote s) then $low else $high) + let high ← build (mid + 1) stop cases + `(match String.compare $discr $(quote s) with + | Ordering.lt => $low + | Ordering.eq => $body + | Ordering.gt => $high) /-- Returns a list of types that are are missing `cls` instances such that