introduce default size instances

Author: datokrat

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

@@ -411,8 +411,8 @@ It simply iterates using `IteratorLoopPartial` and counts the elements.
 For certain iterators, more efficient implementations are possible and should be used instead.
 -/
 @[always_inline, inline]
-instance IteratorSize.Partial.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorLoopPartial α m m] :
+instance IteratorSizePartial.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoopPartial α m m] :
     IteratorSizePartial α m where
   size := IterM.DefaultConsumers.sizePartial
 
@@ -422,6 +422,10 @@ are caused by calling `size`, and if the monad is nondeterministic, it is also u
 returned value should be. The reference implementation, `IteratorSize.defaultImplementation`,
 simply iterates over the whole iterator monadically, counting the number of emitted values.
 An `IteratorSize` instance is considered lawful if it is equal to the reference implementation.
+
+**Performance**:
+
+Default performance is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline]
 def IterM.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m]
@@ -439,6 +443,10 @@ An `IteratorSize` instance is considered lawful if it is equal to the reference
 
 This is the partial version of `size`. It does not require a proof of finiteness and might loop
 forever. It is not possible to verify the behavior in Lean because it uses `partial`.
+
+**Performance**:
+
+Default performance is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline]
 def IterM.Partial.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m]

src/Std/Data/Iterators/Combinators/Monadic/Drop.lean

@@ -166,4 +166,12 @@ instance Drop.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoopPartial (Drop α m β) m n :=
   .defaultImplementation
 
+instance {α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] :
+    IteratorSize (Drop α m β) m :=
+  .defaultImplementation
+
+instance {α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] :
+    IteratorSizePartial (Drop α m β) m :=
+  .defaultImplementation
+
 end Std.Iterators

src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean

@@ -286,4 +286,12 @@ instance DropWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
     IteratorLoopPartial (DropWhile α m β P) m n :=
   .defaultImplementation
 
+instance {α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] {P} :
+    IteratorSize (DropWhile α m β P) m :=
+  .defaultImplementation
+
+instance {α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] {P} :
+    IteratorSizePartial (DropWhile α m β P) m :=
+  .defaultImplementation
+
 end Std.Iterators

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

@@ -232,7 +232,7 @@ instance FilterMap.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
 instance FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type w → Type w'''}
     [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n (Option γ)} [Finite α m] :
+    {f : β → PostconditionT n (Option γ)} :
     IteratorLoopPartial (FilterMap α m n lift f) n o :=
   .defaultImplementation
 
@@ -597,4 +597,16 @@ def IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [M
     (f : β → Bool) (it : IterM (α := α) m β) :=
   (it.filterMap (fun b => if f b then some b else none) : IterM m β)
 
+instance {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
+    {f : β → PostconditionT n (Option γ)} [Finite α m] :
+    IteratorSize (FilterMap α m n lift f) n :=
+  .defaultImplementation
+
+instance {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
+    {f : β → PostconditionT n (Option γ)} :
+    IteratorSizePartial (FilterMap α m n lift f) n :=
+  .defaultImplementation
+
 end Std.Iterators

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

@@ -148,4 +148,12 @@ instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β]
     IteratorLoopPartial (Take α m β) m n :=
   .defaultImplementation
 
+instance {α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] :
+    IteratorSize (Take α m β) m :=
+  .defaultImplementation
+
+instance {α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] :
+    IteratorSizePartial (Take α m β) m :=
+  .defaultImplementation
+
 end Std.Iterators

src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean

@@ -242,4 +242,12 @@ instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
     IteratorLoopPartial (TakeWhile α m β P) m n :=
   .defaultImplementation
 
+instance {α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] {P} :
+    IteratorSize (TakeWhile α m β P) m :=
+  .defaultImplementation
+
+instance {α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] {P} :
+    IteratorSizePartial (TakeWhile α m β P) m :=
+  .defaultImplementation
+
 end Std.Iterators

src/Std/Data/Iterators/Combinators/Monadic/Zip.lean

@@ -392,4 +392,12 @@ instance Zip.instIteratorLoopPartial [Monad m] [Monad n] :
     IteratorLoopPartial (Zip α₁ m α₂ β₂) m n :=
   .defaultImplementation
 
+instance Zip.instIteratorSize [Monad m] [Finite (Zip α₁ m α₂ β₂) m] :
+    IteratorSize (Zip α₁ m α₂ β₂) m :=
+  .defaultImplementation
+
+instance Zip.instIteratorSizePartial [Monad m] :
+    IteratorSizePartial (Zip α₁ m α₂ β₂) m :=
+  .defaultImplementation
+
 end Std.Iterators

src/Std/Data/Iterators/Producers/Monadic/Array.lean

@@ -125,4 +125,12 @@ instance {α : Type w} [Monad m] [Monad n] : IteratorLoop (ArrayIterator α) m n
 instance {α : Type w} [Monad m] [Monad n] : IteratorLoopPartial (ArrayIterator α) m n :=
   .defaultImplementation
 
+@[always_inline, inline]
+instance {α : Type w} [Monad m] : IteratorSize (ArrayIterator α) m :=
+  .defaultImplementation
+
+@[always_inline, inline]
+instance {α : Type w} [Monad m] : IteratorSizePartial (ArrayIterator α) m :=
+  .defaultImplementation
+
 end Std.Iterators

src/Std/Data/Iterators/Producers/Monadic/List.lean

@@ -74,4 +74,12 @@ instance {α : Type w} [Monad m] [Monad n] : IteratorLoop (ListIterator α) m n
 instance {α : Type w} [Monad m] [Monad n] : IteratorLoopPartial (ListIterator α) m n :=
   .defaultImplementation
 
+@[always_inline, inline]
+instance {α : Type w} [Monad m] : IteratorSize (ListIterator α) m :=
+  .defaultImplementation
+
+@[always_inline, inline]
+instance {α : Type w} [Monad m] : IteratorSizePartial (ListIterator α) m :=
+  .defaultImplementation
+
 end Std.Iterators