feat: extrinsic finiteness proofs for toList, toListRev and toArray on iterators

src/Init/Data/Iterators/Combinators/Monadic/Attach.lean

@@ -91,11 +91,6 @@ instance Attach.instIteratorCollect {α β : Type w} {m : Type w → Type w'} [M
     IteratorCollect (Attach α m P) m n :=
   .defaultImplementation
 
-instance Attach.instIteratorCollectPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Monad n] {P : β → Prop} [Iterator α m β] :
-    IteratorCollectPartial (Attach α m P) m n :=
-  .defaultImplementation
-
 instance Attach.instIteratorLoop {α β : Type w} {m : Type w → Type w'} [Monad m]
     {n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
     IteratorLoop (Attach α m P) m n :=

src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean

@@ -221,13 +221,6 @@ instance {α β γ : Type w} {m : Type w → Type w'}
     IteratorCollect (FilterMap α m n lift f) n o :=
   .defaultImplementation
 
-instance {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
-    {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n (Option γ)} [Finite α m] :
-    IteratorCollectPartial (FilterMap α m n lift f) n o :=
-  .defaultImplementation
-
 instance FilterMap.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type x → Type x'}
     [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
@@ -249,7 +242,7 @@ instance FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → T
 instance Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
     {lift₁ : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} [IteratorCollect α m o] [Finite α m] :
+    {f : β → PostconditionT n γ} [IteratorCollect α m o] :
     IteratorCollect (Map α m n lift₁ f) n o where
   toArrayMapped lift₂ _ g it :=
     letI : MonadLift m n := ⟨lift₁ (α := _)⟩
@@ -259,18 +252,6 @@ instance Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
       (fun x => do g (← (f x).operation))
       it.internalState.inner (m := m)
 
-@[no_expose]
-instance Map.instIteratorCollectPartial {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
-    {lift₁ : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} [IteratorCollectPartial α m o] :
-    IteratorCollectPartial (Map α m n lift₁ f) n o where
-  toArrayMappedPartial lift₂ _ g it :=
-    IteratorCollectPartial.toArrayMappedPartial
-      (lift := fun ⦃_⦄ a => lift₂ (lift₁ a))
-      (fun x => do g (← lift₂ (f x).operation))
-      it.internalState.inner (m := m)
-
 instance Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α}

src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean

@@ -370,10 +370,6 @@ public instance Flatten.instIteratorCollect [Monad m] [Monad n] [Iterator α m (
     [Iterator α₂ m β] : IteratorCollect (Flatten α α₂ β m) m n :=
   .defaultImplementation
 
-public instance Flatten.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
-    [Iterator α₂ m β] : IteratorCollectPartial (Flatten α α₂ β m) m n :=
-  .defaultImplementation
-
 public instance Flatten.instIteratorLoop [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
     [Iterator α₂ m β] : IteratorLoop (Flatten α α₂ β m) m n :=
   .defaultImplementation

src/Init/Data/Iterators/Combinators/Monadic/Take.lean

@@ -208,10 +208,6 @@ instance Take.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [
     IteratorCollect (Take α m) m n :=
   .defaultImplementation
 
-instance Take.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorCollectPartial (Take α m) m n :=
-  .defaultImplementation
-
 instance Take.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoop (Take α m) m n :=
   .defaultImplementation

src/Init/Data/Iterators/Combinators/Monadic/ULift.lean

@@ -136,10 +136,6 @@ instance Types.ULiftIterator.instIteratorCollect [Monad n] [Monad o] [Iterator 
     IteratorCollect (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
-instance Types.ULiftIterator.instIteratorCollectPartial {o} [Monad n] [Monad o] [Iterator α m β] :
-    IteratorCollectPartial (ULiftIterator α m n β lift) n o :=
-  .defaultImplementation
-
 /--
 Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with
 values in `ULift β`. Requires a `MonadLift m (ULiftT n)` instance.

src/Init/Data/Iterators/Consumers.lean

@@ -11,5 +11,6 @@ public import Init.Data.Iterators.Consumers.Access
 public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Partial
+public import Init.Data.Iterators.Consumers.Total
 
 public import Init.Data.Iterators.Consumers.Stream

src/Init/Data/Iterators/Consumers/Collect.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers.Partial
+public import Init.Data.Iterators.Consumers.Total
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 
 @[expose] public section
@@ -21,40 +22,113 @@ Concretely, the following operations are provided:
 * `Iter.toListRev`, collecting the values in a list in reverse order but more efficiently
 * `Iter.toArray`, collecting the values in an array
 
-Some operations are implemented using the `IteratorCollect` and `IteratorCollectPartial`
-typeclasses.
+Some operations are implemented using the `IteratorCollect` type class.
 -/
 
 namespace Std.Iterators
 
-@[always_inline, inline, inherit_doc IterM.toArray]
+/--
+Traverses the given iterator and stores the emitted values in an array.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toArray` always terminates after finitely many steps.
+-/
+@[always_inline, inline]
 def Iter.toArray {α : Type w} {β : Type w}
-    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter (α := α) β) : Array β :=
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : Array β :=
   it.toIterM.toArray.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toArray]
+/--
+Traverses the given iterator and stores the emitted values in an array.
+
+This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
+-/
+@[always_inline, inline, deprecated Iter.toArray (since := "2025-10-23")]
 def Iter.Partial.toArray {α : Type w} {β : Type w}
-    [Iterator α Id β] [IteratorCollectPartial α Id Id] (it : Iter.Partial (α := α) β) : Array β :=
-  it.it.toIterM.allowNontermination.toArray.run
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : Array β :=
+  it.it.toArray
+
+/--
+Traverses the given iterator and stores the emitted values in an array.
 
-@[always_inline, inline, inherit_doc IterM.toListRev]
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.toArray`.
+-/
+@[always_inline, inline]
+def Iter.Total.toArray {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter.Total (α := α) β) :
+    Array β :=
+  it.it.toArray
+
+/--
+Traverses the given iterator and stores the emitted values in reverse order in a list. Because
+lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toListRev` always terminates after finitely many steps.
+-/
+@[always_inline, inline]
 def Iter.toListRev {α : Type w} {β : Type w}
-    [Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) : List β :=
+    [Iterator α Id β] (it : Iter (α := α) β) : List β :=
   it.toIterM.toListRev.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toListRev]
+/--
+Traverses the given iterator and stores the emitted values in reverse order in a list. Because
+lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
+
+This function is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
+-/
+@[always_inline, inline, deprecated Iter.toListRev (since := "2025-10-23")]
 def Iter.Partial.toListRev {α : Type w} {β : Type w}
     [Iterator α Id β] (it : Iter.Partial (α := α) β) : List β :=
-  it.it.toIterM.allowNontermination.toListRev.run
+  it.it.toListRev
 
-@[always_inline, inline, inherit_doc IterM.toList]
+/--
+Traverses the given iterator and stores the emitted values in reverse order in a list. Because
+lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.toListRev`.
+-/
+@[always_inline, inline]
+def Iter.Total.toListRev {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] (it : Iter.Total (α := α) β) : List β :=
+  it.it.toListRev
+
+/--
+Traverses the given iterator and stores the emitted values in a list. Because
+lists are prepend-only, `toListRev` is usually more efficient that `toList`.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toList` always terminates after finitely many steps.
+-/
+@[always_inline, inline]
 def Iter.toList {α : Type w} {β : Type w}
-    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter (α := α) β) : List β :=
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : List β :=
   it.toIterM.toList.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toList]
+/--
+Traverses the given iterator and stores the emitted values in a list. Because
+lists are prepend-only, `toListRev` is usually more efficient that `toList`.
+
+This function is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
+-/
+@[always_inline, deprecated Iter.toList (since := "2025-10-23")]
 def Iter.Partial.toList {α : Type w} {β : Type w}
-    [Iterator α Id β] [IteratorCollectPartial α Id Id] (it : Iter.Partial (α := α) β) : List β :=
-  it.it.toIterM.allowNontermination.toList.run
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : List β :=
+  it.it.toList
+
+/--
+Traverses the given iterator and stores the emitted values in a list. Because
+lists are prepend-only, `toListRev` is usually more efficient that `toList`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.toList`.
+-/
+@[always_inline, inline]
+def Iter.Total.toList {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter.Total (α := α) β) :
+    List β :=
+  it.it.toList
 
 end Std.Iterators