Also RevSplitIterator

Author: TwoFX

src/Init/Data/String/Slice.lean

@@ -534,25 +534,34 @@ Examples:
 def endsWith [BackwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
   BackwardPattern.endsWith s pat
 
-inductive RevSplitIterator (ρ : Type) [ToBackwardSearcher ρ σ] where
-  | operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
+inductive RevSplitIterator (ρ : Type) (s : Slice) [ToBackwardSearcher ρ σ] where
+  | operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
   | atEnd
 deriving Inhabited
 
 namespace RevSplitIterator
 
 variable [ToBackwardSearcher ρ σ]
 
-instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ) m Slice where
-  IsPlausibleStep := fun _ _ => True
+instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ s) m Slice where
+  IsPlausibleStep it
+    | .yield it' out =>
+      match it.internalState, it'.internalState with
+      | .operating _ searcher, .operating _ searcher' =>
+          searcher'.finitelyManySteps.Rel searcher.finitelyManySteps
+      | .operating _ searcher, .atEnd => True
+      | .atEnd, _ => False
+    | .skip _ => False
+    | .done => True
   step := fun ⟨iter⟩ =>
     match iter with
-    | .operating s currPos searcher =>
-      match Internal.nextMatch searcher with
+    | .operating currPos searcher =>
+      match h : Internal.nextMatch searcher with
       | some (searcher, startPos, endPos) =>
         let slice := s.replaceStartEnd! endPos currPos
-        let nextIt := ⟨.operating s startPos searcher⟩
-        pure (.deflate ⟨.yield nextIt slice, by simp⟩)
+        let nextIt := ⟨.operating startPos searcher⟩
+        pure (.deflate ⟨.yield nextIt slice,
+          by simpa [nextIt] using Pattern.Internal.finitelyManySteps_rel_nextMatch h⟩)
       | none =>
         if currPos ≠ s.startPos then
           let slice := s.replaceEnd currPos
@@ -561,19 +570,57 @@ instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ) m Slice where
           pure (.deflate ⟨.done, by simp⟩)
     | .atEnd => pure (.deflate ⟨.done, by simp⟩)
 
+private def toOption : RevSplitIterator ρ s → Option (Std.Iter (α := σ s) (SearchStep s))
+  | .operating _ s => some s
+  | .atEnd => none
+
+private instance {s} [Std.Iterators.Finite (σ s) Id] :
+    WellFoundedRelation (RevSplitIterator ρ s) where
+  rel := InvImage (Option.lt (InvImage Std.Iterators.IterM.TerminationMeasures.Finite.Rel
+    Std.Iterators.Iter.finitelyManySteps)) RevSplitIterator.toOption
+  wf := by
+    apply InvImage.wf
+    apply Option.wellFounded_lt
+    apply InvImage.wf
+    exact WellFoundedRelation.wf
+
+private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
+    Std.Iterators.FinitenessRelation (RevSplitIterator ρ s) Id where
+  rel := InvImage WellFoundedRelation.rel (fun it => it.internalState)
+  wf := InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    simp_wf
+    obtain ⟨step, h, h'⟩ := h
+    match step with
+    | .yield it'' out =>
+      obtain rfl : it' = it'' := by simpa [Std.Iterators.IterStep.successor] using h.symm
+      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
+      revert h'
+      match it.internalState, it'.internalState with
+      | .operating _ searcher, .operating _ searcher' =>
+        simp [RevSplitIterator.toOption, Option.lt]
+      | .operating _ searcher, .atEnd =>
+        simp [RevSplitIterator.toOption, Option.lt]
+      | .atEnd, _ => simp
+
+@[no_expose]
+instance [Std.Iterators.Finite (σ s) Id] :
+    Std.Iterators.Finite (RevSplitIterator ρ s) Id :=
+  .of_finitenessRelation finitenessRelation
+
 -- TODO: Finiteness after we have a notion of lawful searcher
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ) m n :=
+instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
 instance [Monad m] [Monad n] :
-    Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ) m n :=
+    Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ) m n :=
+instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ) m n :=
+instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
 end RevSplitIterator
@@ -594,8 +641,8 @@ Examples:
 -/
 @[specialize pat]
 def revSplit [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) :
-    Std.Iter (α := RevSplitIterator ρ) Slice :=
-  { internalState := .operating s s.endPos (ToBackwardSearcher.toSearcher s pat) }
+    Std.Iter (α := RevSplitIterator ρ s) Slice :=
+  { internalState := .operating s.endPos (ToBackwardSearcher.toSearcher s pat) }
 
 /--
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.