perf: unbundle needle from char/pred pattern (#11376)

This PR aims to improve the performance of `String.contains`,
`String.find`, etc. when using patterns of type `Char` or `Char -> Bool`
by moving the needle out of the iterator state and thus working around
missing unboxing in the compiler.

Author: TwoFX

src/Init/Data/String/Pattern/Char.lean

@@ -21,65 +21,63 @@ public section
 
 namespace String.Slice.Pattern
 
-structure ForwardCharSearcher (s : Slice) where
+structure ForwardCharSearcher (needle : Char) (s : Slice) where
   currPos : s.Pos
-  needle : Char
 deriving Inhabited
 
 namespace ForwardCharSearcher
 
 @[inline]
-def iter (c : Char) (s : Slice) : Std.Iter (α := ForwardCharSearcher s) (SearchStep s) :=
-  { internalState := { currPos := s.startPos, needle := c }}
+def iter (c : Char) (s : Slice) : Std.Iter (α := ForwardCharSearcher c s) (SearchStep s) :=
+  { internalState := { currPos := s.startPos }}
 
-instance (s : Slice) : Std.Iterators.Iterator (ForwardCharSearcher s) Id (SearchStep s) where
+instance (s : Slice) : Std.Iterators.Iterator (ForwardCharSearcher c s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' out =>
-      it.internalState.needle = it'.internalState.needle ∧
       ∃ h1 : it.internalState.currPos ≠ s.endPos,
         it'.internalState.currPos = it.internalState.currPos.next h1 ∧
         match out with
         | .matched startPos endPos =>
           it.internalState.currPos = startPos ∧
           it'.internalState.currPos = endPos ∧
-          it.internalState.currPos.get h1 = it.internalState.needle
+          it.internalState.currPos.get h1 = c
         | .rejected startPos endPos =>
           it.internalState.currPos = startPos ∧
           it'.internalState.currPos = endPos ∧
-          it.internalState.currPos.get h1 ≠ it.internalState.needle
+          it.internalState.currPos.get h1 ≠ c
     | .skip _ => False
     | .done => it.internalState.currPos = s.endPos
-  step := fun ⟨currPos, needle⟩ =>
+  step := fun ⟨⟨currPos⟩⟩ =>
     if h1 : currPos = s.endPos then
       pure (.deflate ⟨.done, by simp [h1]⟩)
     else
       let nextPos := currPos.next h1
-      let nextIt := ⟨nextPos, needle⟩
-      if h2 : currPos.get h1 = needle then
+      let nextIt := ⟨⟨nextPos⟩⟩
+      if h2 : currPos.get h1 = c then
         pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
       else
         pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
-def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s) Id where
+def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s c) Id where
   rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf
     obtain ⟨step, h, h'⟩ := h
     cases step
     · cases h
-      obtain ⟨_, h1, h2, _⟩ := h'
+      obtain ⟨_, h2, _⟩ := h'
       simp [h2]
     · cases h'
     · cases h
 
-instance : Std.Iterators.Finite (ForwardCharSearcher s) Id :=
+instance : Std.Iterators.Finite (ForwardCharSearcher s c) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance : Std.Iterators.IteratorLoop (ForwardCharSearcher s) Id Id :=
+instance : Std.Iterators.IteratorLoop (ForwardCharSearcher s c) Id Id :=
   .defaultImplementation
 
-instance {c : Char} : ToForwardSearcher c ForwardCharSearcher where
+instance {c : Char} : ToForwardSearcher c (ForwardCharSearcher c) where
   toSearcher := iter c
 
 instance {c : Char} : ForwardPattern c := .defaultImplementation

src/Init/Data/String/Pattern/Pred.lean

@@ -22,71 +22,69 @@ public section
 
 namespace String.Slice.Pattern
 
-structure ForwardCharPredSearcher (s : Slice) where
+structure ForwardCharPredSearcher (p : Char → Bool) (s : Slice) where
   currPos : s.Pos
-  needle : Char → Bool
 deriving Inhabited
 
 namespace ForwardCharPredSearcher
 
 @[inline]
-def iter (p : Char → Bool) (s : Slice) : Std.Iter (α := ForwardCharPredSearcher s) (SearchStep s) :=
-  { internalState := { currPos := s.startPos, needle := p }}
+def iter (p : Char → Bool) (s : Slice) : Std.Iter (α := ForwardCharPredSearcher p s) (SearchStep s) :=
+  { internalState := { currPos := s.startPos }}
 
-instance (s : Slice) : Std.Iterators.Iterator (ForwardCharPredSearcher s) Id (SearchStep s) where
+instance (s : Slice) : Std.Iterators.Iterator (ForwardCharPredSearcher p s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' out =>
-      it.internalState.needle = it'.internalState.needle ∧
       ∃ h1 : it.internalState.currPos ≠ s.endPos,
         it'.internalState.currPos = it.internalState.currPos.next h1 ∧
         match out with
         | .matched startPos endPos =>
           it.internalState.currPos = startPos ∧
           it'.internalState.currPos = endPos ∧
-          it.internalState.needle (it.internalState.currPos.get h1)
+          p (it.internalState.currPos.get h1)
         | .rejected startPos endPos =>
           it.internalState.currPos = startPos ∧
           it'.internalState.currPos = endPos ∧
-          ¬ it.internalState.needle (it.internalState.currPos.get h1)
+          ¬ p (it.internalState.currPos.get h1)
     | .skip _ => False
     | .done => it.internalState.currPos = s.endPos
-  step := fun ⟨currPos, needle⟩ =>
+  step := fun ⟨⟨currPos⟩⟩ =>
     if h1 : currPos = s.endPos then
       pure (.deflate ⟨.done, by simp [h1]⟩)
     else
       let nextPos := currPos.next h1
-      let nextIt := ⟨nextPos, needle⟩
-      if h2 : needle <| currPos.get h1 then
+      let nextIt := ⟨⟨nextPos⟩⟩
+      if h2 : p <| currPos.get h1 then
         pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
       else
         pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
 
 
-def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher s) Id where
+def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher p s) Id where
   rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
     simp_wf
     obtain ⟨step, h, h'⟩ := h
     cases step
     · cases h
-      obtain ⟨_, h1, h2, _⟩ := h'
+      obtain ⟨_, h2, _⟩ := h'
       simp [h2]
     · cases h'
     · cases h
 
-instance : Std.Iterators.Finite (ForwardCharPredSearcher s) Id :=
+instance : Std.Iterators.Finite (ForwardCharPredSearcher p s) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance : Std.Iterators.IteratorLoop (ForwardCharPredSearcher s) Id Id :=
+instance : Std.Iterators.IteratorLoop (ForwardCharPredSearcher p s) Id Id :=
   .defaultImplementation
 
-instance {p : Char → Bool} : ToForwardSearcher p ForwardCharPredSearcher where
+instance {p : Char → Bool} : ToForwardSearcher p (ForwardCharPredSearcher p) where
   toSearcher := iter p
 
 instance {p : Char → Bool} : ForwardPattern p := .defaultImplementation
 
-instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p ForwardCharPredSearcher where
+instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ForwardCharPredSearcher p) where
   toSearcher := iter (decide <| p ·)
 
 instance {p : Char → Prop} [DecidablePred p] : ForwardPattern p :=