Skip to content

perf: use String.compare in ConfigEval decision tree #13806

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
kmill wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

perf: use String.compare in ConfigEval decision tree #13806

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 7 additions & 4 deletions src/Lean/Elab/ConfigEval/Util.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading