remove partial

Author: datokrat

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

@@ -96,11 +96,6 @@ instance Attach.instIteratorLoop {α β : Type w} {m : Type w → Type w'} [Mona
     IteratorLoop (Attach α m P) m n :=
   .defaultImplementation
 
-instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
-    {n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
-    IteratorLoopPartial (Attach α m P) m n :=
-  .defaultImplementation
-
 instance {α β : Type w} {m : Type w → Type w'} [Monad m]
     {P : β → Prop} [Iterator α m β] [IteratorSize α m] :
     IteratorSize (Attach α m P) m where

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

@@ -222,17 +222,10 @@ instance {α β γ : Type w} {m : Type w → Type w'}
   .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 α}
-    {f : β → PostconditionT n (Option γ)} [Finite α m] :
-    IteratorLoop (FilterMap α m n lift f) n o :=
-  .defaultImplementation
-
-instance FilterMap.instIteratorLoopPartial {α β γ : 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 α}
     {f : β → PostconditionT n (Option γ)} :
-    IteratorLoopPartial (FilterMap α m n lift f) n o :=
+    IteratorLoop (FilterMap α m n lift f) n o :=
   .defaultImplementation
 
 /--
@@ -259,13 +252,6 @@ instance Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
     IteratorLoop (Map α m n lift f) n o :=
   .defaultImplementation
 
-instance Map.instIteratorLoopPartial {α β γ : 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 α}
-    {f : β → PostconditionT n γ} :
-    IteratorLoopPartial (Map α m n lift f) n o :=
-  .defaultImplementation
-
 /--
 *Note: This is a very general combinator that requires an advanced understanding of monads, dependent
 types and termination proofs. The variants `map` and `mapM` are easier to use and sufficient

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

@@ -374,8 +374,4 @@ public instance Flatten.instIteratorLoop [Monad m] [Monad n] [Iterator α m (Ite
     [Iterator α₂ m β] : IteratorLoop (Flatten α α₂ β m) m n :=
   .defaultImplementation
 
-public instance Flatten.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
-    [Iterator α₂ m β] : IteratorLoopPartial (Flatten α α₂ β m) m n :=
-  .defaultImplementation
-
 end Std.Iterators

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

@@ -128,10 +128,6 @@ instance Types.ULiftIterator.instIteratorLoop {o : Type x → Type x'} [Monad n]
     IteratorLoop (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
-instance Types.ULiftIterator.instIteratorLoopPartial {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] :
-    IteratorLoopPartial (ULiftIterator α m n β lift) n o :=
-  .defaultImplementation
-
 instance Types.ULiftIterator.instIteratorCollect [Monad n] [Monad o] [Iterator α m β] :
     IteratorCollect (ULiftIterator α m n β lift) n o :=
   .defaultImplementation

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

@@ -48,16 +48,16 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
 
 @[always_inline, inline]
 def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
-    [Iterator α Id β] [IteratorLoopPartial α Id n] :
+    [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn' n (Iter.Partial (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
   forIn' it init f :=
-    IteratorLoopPartial.forInPartial (α := α) (m := Id) (n := n) (fun _ _ f c => f c.run)
+    IteratorLoop.forIn (α := α) (m := Id) (n := n) (fun _ _ f c => f c.run) _
       it.it.toIterM init
       fun out h acc =>
         f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
 
 instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
-    [Iterator α Id β] [IteratorLoopPartial α Id n] :
+    [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn n (Iter.Partial (α := α) β) β :=
   haveI : ForIn' n (Iter.Partial (α := α) β) β _ := Iter.Partial.instForIn'
   instForInOfForIn'
@@ -68,7 +68,7 @@ instance {m : Type x → Type x'}
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
 instance {m : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id m] :
+    {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id m] :
     ForM m (Iter.Partial (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
@@ -77,11 +77,6 @@ Folds a monadic function over an iterator from the left, accumulating a value st
 The accumulated value is combined with the each element of the list in order, using `f`.
 
 It is equivalent to `it.toList.foldlM`.
-
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.foldM` instead of `it.foldM`. However, it is not possible to formally
-verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
 def Iter.foldM {m : Type x → Type x'} [Monad m]
@@ -96,13 +91,12 @@ The accumulated value is combined with the each element of the list in order, us
 
 It is equivalent to `it.toList.foldlM`.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.
+This function is deprecated. Instead of `it.allowNontermination.foldM`, use `it.foldM`.
 -/
 @[always_inline, inline]
 def Iter.Partial.foldM {m : Type x → Type x'} [Monad m]
     {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
-    [IteratorLoopPartial α Id m] (f : γ → β → m γ)
+    [IteratorLoop α Id m] (f : γ → β → m γ)
     (init : γ) (it : Iter.Partial (α := α) β) : m γ :=
   ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
 
@@ -111,11 +105,6 @@ Folds a function over an iterator from the left, accumulating a value starting w
 The accumulated value is combined with the each element of the list in order, using `f`.
 
 It is equivalent to `it.toList.foldl`.
-
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.fold` instead of `it.fold`. However, it is not possible to formally
-verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
 def Iter.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
@@ -129,12 +118,11 @@ The accumulated value is combined with the each element of the list in order, us
 
 It is equivalent to `it.toList.foldl`.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.fold` instead.
+This function is deprecated. Instead of `it.allowNontermination.fold`, use `it.fold`.
 -/
 @[always_inline, inline]
 def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
-    [IteratorLoopPartial α Id Id] (f : γ → β → γ)
+    [IteratorLoop α Id Id] (f : γ → β → γ)
     (init : γ) (it : Iter.Partial (α := α) β) : γ :=
   ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
 
@@ -211,56 +199,53 @@ def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Mon
     | none => return .yield none
     | some fx => return .done (some fx))
 
-@[inline]
+@[inline, deprecated Iter.findSomeM? (since := "2025-10-21")]
 def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
-    [Iterator α Id β] [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β)
+    [Iterator α Id β] [IteratorLoop α Id m] (it : Iter.Partial (α := α) β)
     (f : β → m (Option γ)) :
     m (Option γ) :=
-  ForIn.forIn it none (fun x _ => do
-    match ← f x with
-    | none => return .yield none
-    | some fx => return .done (some fx))
+  it.it.findSomeM? f
 
 @[inline]
 def Iter.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
     [IteratorLoop α Id Id] (it : Iter (α := α) β) (f : β → Option γ) :
     Option γ :=
   Id.run (it.findSomeM? (pure <| f ·))
 
-@[inline]
+@[inline, deprecated Iter.findSome? (since := "2025-10-21")]
 def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
-    [IteratorLoopPartial α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
+    [IteratorLoop α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
     Option γ :=
-  Id.run (it.findSomeM? (pure <| f ·))
+  it.it.findSome? f
 
 @[inline]
 def Iter.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
     [IteratorLoop α Id m] (it : Iter (α := α) β) (f : β → m (ULift Bool)) :
     m (Option β) :=
   it.findSomeM? (fun x => return if (← f x).down then some x else none)
 
-@[inline]
+@[inline, deprecated Iter.findM? (since := "2025-10-21")]
 def Iter.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
-    [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
+    [IteratorLoop α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
     m (Option β) :=
-  it.findSomeM? (fun x => return if (← f x).down then some x else none)
+  it.it.findM? f
 
 @[inline]
 def Iter.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter (α := α) β) (f : β → Bool) : Option β :=
   Id.run (it.findM? (pure <| .up <| f ·))
 
-@[inline]
-def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
+@[inline, deprecated Iter.find? (since := "2025-10-21")]
+def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter.Partial (α := α) β) (f : β → Bool) : Option β :=
-  Id.run (it.findM? (pure <| .up <| f ·))
+  it.it.find? f
 
-@[always_inline, inline, expose, inherit_doc IterM.size]
+@[always_inline, expose, inherit_doc IterM.size]
 def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
     (it : Iter (α := α) β) : Nat :=
   (IteratorSize.size it.toIterM).run.down
 
-@[always_inline, inline, inherit_doc IterM.Partial.size]
+@[always_inline, inherit_doc IterM.Partial.size]
 def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id]
     (it : Iter (α := α) β) : Nat :=
   (IteratorSizePartial.size it.toIterM).run.down