max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf: eliminate some allocations in iterateLookaround

Browse source
This commit is contained in:
Sebastian Ullrich 2022-03-03 11:25:35 +01:00 • committed by Leonardo de Moura
parent 7106d3fb34
commit 896b9b48a3
1 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Data/FuzzyMatching.lean
View file

@ -29,7 +29,7 @@ inductive CharRole where
| head | tail | separator
deriving Inhabited
def charRole (prev? : Option CharType) (curr : CharType) (next?: Option CharType) : CharRole :=
@[inline] def charRole (prev? : Option CharType) (curr : CharType) (next?: Option CharType) : CharRole :=
if curr matches CharType.separator then
CharRole.separator
else if prev?.isNone || prev? matches some CharType.separator then
@ -49,17 +49,18 @@ def charRole (prev? : Option CharType) (curr : CharType) (next?: Option CharType
#[f (none, string.get 0, none)]
else Id.run <| do
let mut result := Array.mkEmpty string.length
result := result.push <| f (none, string.get 0, string.get 1)
let mut prev? := none
let mut curr := string.get 0
let mut prev := string.get 0
let mut curr := string.get 1
for i in [1:string.length] do
for i in [2:string.length] do
let next := string.get i
result := result.push <| f (prev?, curr, some next)
result := result.push <| f (prev, curr, some next)
prev? := some curr
prev := curr
curr := next
result.push <| f (prev?, curr, none)
result.push <| f (prev, curr, none)
/- Add additional information to each character in a string and return the