fix: search for empty string (#10985)

This PR ensures that searching for an empty string returns the expected
pattern of alternating size-zero matches and size-one rejects.

In particular, splitting by an empty string returns an array formed of
the empty string, all of the string's characters as singleton strings,
followed by another empty string. This matches the [Rust
behavior](https://doc.rust-lang.org/std/primitive.str.html#method.split),
for example.

Author: TwoFX

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

@@ -38,7 +38,7 @@ inductive SearchStep (s : Slice) where
   The subslice starting at {name}`startPos` and ending at {name}`endPos` did not match the pattern.
   -/
   | matched (startPos endPos : s.Pos)
-deriving Inhabited
+deriving Inhabited, BEq
 
 /--
 Provides a conversion from a pattern to an iterator of {name}`SearchStep` that searches for matches

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

@@ -22,7 +22,8 @@ public section
 namespace String.Slice.Pattern
 
 inductive ForwardSliceSearcher (s : Slice) where
-  | empty (pos : s.Pos)
+  | emptyBefore (pos : s.Pos)
+  | emptyAt (pos : s.Pos) (h : pos ≠ s.endPos)
   | proper (needle : Slice) (table : Array String.Pos.Raw) (stackPos : String.Pos.Raw) (needlePos : String.Pos.Raw)
   | atEnd
 deriving Inhabited
@@ -56,7 +57,7 @@ where
 @[inline]
 def iter (s : Slice) (pat : Slice) : Std.Iter (α := ForwardSliceSearcher s) (SearchStep s) :=
   if pat.utf8ByteSize == 0 then
-    { internalState := .empty s.startPos }
+    { internalState := .emptyBefore s.startPos }
   else
     { internalState := .proper pat (buildTable pat) s.startPos.offset pat.startPos.offset }
 
@@ -71,9 +72,8 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
   IsPlausibleStep it
     | .yield it' out =>
       match it.internalState with
-      | .empty pos =>
-        (∃ newPos, pos < newPos ∧ it'.internalState = .empty newPos) ∨
-        it'.internalState = .atEnd
+      | .emptyBefore pos => (∃ h, it'.internalState = .emptyAt pos h) ∨ it'.internalState = .atEnd
+      | .emptyAt pos h => ∃ newPos, pos < newPos ∧ it'.internalState = .emptyBefore newPos
       | .proper needle table stackPos needlePos =>
         (∃ newStackPos newNeedlePos,
           stackPos < newStackPos ∧
@@ -85,12 +85,15 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
     | .done => True
   step := fun ⟨iter⟩ =>
     match iter with
-    | .empty pos =>
+    | .emptyBefore pos =>
       let res := .matched pos pos
       if h : pos ≠ s.endPos then
-        pure (.deflate ⟨.yield ⟨.empty (pos.next h)⟩ res, by simp⟩)
+        pure (.deflate ⟨.yield ⟨.emptyAt pos h⟩ res, by simp [h]⟩)
       else
         pure (.deflate ⟨.yield ⟨.atEnd⟩ res, by simp⟩)
+    | .emptyAt pos h =>
+      let res := .rejected pos (pos.next h)
+      pure (.deflate ⟨.yield ⟨.emptyBefore (pos.next h)⟩ res, by simp⟩)
     | .proper needle table stackPos needlePos =>
       let rec findNext (startPos : String.Pos.Raw)
           (currStackPos : String.Pos.Raw) (needlePos : String.Pos.Raw) (h : stackPos ≤ currStackPos) :=
@@ -148,15 +151,17 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
       findNext stackPos stackPos needlePos (by simp)
     | .atEnd => pure (.deflate ⟨.done, by simp⟩)
 
-private def toPair : ForwardSliceSearcher s → (Nat × Nat)
-  | .empty pos => (1, s.utf8ByteSize - pos.offset.byteIdx)
-  | .proper _ _ sp _ => (1, s.utf8ByteSize - sp.byteIdx)
-  | .atEnd => (0, 0)
+private def toOption : ForwardSliceSearcher s → Option (Nat × Nat)
+  | .emptyBefore pos => some (s.utf8ByteSize - pos.offset.byteIdx, 1)
+  | .emptyAt pos _ => some (s.utf8ByteSize - pos.offset.byteIdx, 0)
+  | .proper _ _ sp _ => some (s.utf8ByteSize - sp.byteIdx, 0)
+  | .atEnd => none
 
 private instance : WellFoundedRelation (ForwardSliceSearcher s) where
-  rel s1 s2 := Prod.Lex (· < ·) (· < ·) s1.toPair s2.toPair
+  rel := InvImage (Option.lt (Prod.Lex (· < ·) (· < ·))) ForwardSliceSearcher.toOption
   wf := by
     apply InvImage.wf
+    apply Option.wellFounded_lt
     apply (Prod.lex _ _).wf
 
 private def finitenessRelation :
@@ -168,30 +173,26 @@ private def finitenessRelation :
     obtain ⟨step, h, h'⟩ := h
     cases step
     · cases h
-      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
-      split at h'
-      · next heq =>
-        rw [heq]
-        rcases h' with ⟨np, h1', h2'⟩ | h'
-        · rw [h2']
-          apply Prod.Lex.right'
-          · simp
-          · have haux := np.isValidForSlice.le_utf8ByteSize
-            simp [Slice.Pos.lt_iff, String.Pos.Raw.le_iff, String.Pos.Raw.lt_iff] at h1' haux ⊢
-            omega
-        · apply Prod.Lex.left
-          simp [h']
-      · next heq =>
-        rw [heq]
-        rcases h' with ⟨np, sp, h1', h2', h3'⟩ | h'
-        · rw [h3']
-          apply Prod.Lex.right'
-          · simp
-          · simp [String.Pos.Raw.le_iff, String.Pos.Raw.lt_iff] at h1' h2' ⊢
-            omega
-        · apply Prod.Lex.left
-          simp [h']
-      · contradiction
+      revert h'
+      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep]
+      match it.internalState with
+      | .emptyBefore pos =>
+        rintro (⟨h, h'⟩|h') <;> simp [h', ForwardSliceSearcher.toOption, Option.lt, Prod.lex_def]
+      | .emptyAt pos h =>
+        simp only [forall_exists_index, and_imp]
+        intro x hx h
+        have := x.isValidForSlice.le_utf8ByteSize
+        simp [h, ForwardSliceSearcher.toOption, Option.lt, Prod.lex_def, Pos.lt_iff,
+          Pos.Raw.lt_iff, Pos.Raw.le_iff] at hx ⊢ this
+        omega
+      | .proper needle table stackPos needlePos =>
+        simp only [exists_and_left]
+        rintro (⟨newStackPos, h₁, h₂, ⟨x, hx⟩⟩|h)
+        · simp [hx, ForwardSliceSearcher.toOption, Option.lt, Prod.lex_def, Pos.Raw.lt_iff,
+            Pos.Raw.le_iff] at ⊢ h₁ h₂
+          omega
+        · simp [h, ForwardSliceSearcher.toOption, Option.lt]
+      | .atEnd .. => simp
     · cases h'
     · cases h
 

tests/lean/run/string_slice.lean

@@ -209,3 +209,25 @@ Tests for `String.Slice` functions
 
 #guard "abc".toSlice.back = 'c'
 #guard "".toSlice.back = (default : Char)
+
+section
+open String.Slice.Pattern
+
+instance [Monad n]{s : String.Slice} : Std.Iterators.IteratorCollect (ForwardSliceSearcher s) Id n :=
+  .defaultImplementation
+
+#guard (ToForwardSearcher.toSearcher "".toSlice "").toList == [.matched "".toSlice.startPos "".toSlice.startPos]
+#guard (ToForwardSearcher.toSearcher "abc".toSlice "").toList == [
+  .matched ("abc".toSlice.pos ⟨0⟩ (by decide)) ("abc".toSlice.pos ⟨0⟩ (by decide)),
+  .rejected ("abc".toSlice.pos ⟨0⟩ (by decide)) ("abc".toSlice.pos ⟨1⟩ (by decide)),
+  .matched ("abc".toSlice.pos ⟨1⟩ (by decide)) ("abc".toSlice.pos ⟨1⟩ (by decide)),
+  .rejected ("abc".toSlice.pos ⟨1⟩ (by decide)) ("abc".toSlice.pos ⟨2⟩ (by decide)),
+  .matched ("abc".toSlice.pos ⟨2⟩ (by decide)) ("abc".toSlice.pos ⟨2⟩ (by decide)),
+  .rejected ("abc".toSlice.pos ⟨2⟩ (by decide)) ("abc".toSlice.pos ⟨3⟩ (by decide)),
+  .matched ("abc".toSlice.pos ⟨3⟩ (by decide)) ("abc".toSlice.pos ⟨3⟩ (by decide)),
+]
+
+end
+
+#guard ("".toSlice.split "").allowNontermination.toList == ["".toSlice, "".toSlice]
+#guard ("abc".toSlice.split "").allowNontermination.toList == ["".toSlice, "a".toSlice, "b".toSlice, "c".toSlice, "".toSlice]