Documentation

Init.Data.Iterators.Consumers.Monadic.Loop

Loop-based consumers #

This module provides consumers that iterate over a given iterator, applying a certain user-supplied function in every iteration. Concretely, the following operations are provided:

Some producers and combinators provide specialized implementations. These are captured by the IteratorLoop and IteratorLoopPartial typeclasses. They should be implemented by all types of iterators. A default implementation is provided. The typeclass LawfulIteratorLoop asserts that an IteratorLoop instance equals the default implementation.

def Std.Iterators.IteratorLoop.rel (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] {γ : Type x} (plausible_forInStep : βγForInStep γProp) (p' p : IterM m β × γ) :

Relation that needs to be well-formed in order for a loop over an iterator to terminate. It is assumed that the plausible_forInStep predicate relates the input and output of the stepper function.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Std.Iterators.IteratorLoop.WellFounded (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] {γ : Type x} (plausible_forInStep : βγForInStep γProp) :

    Asserts that IteratorLoop.rel is well-founded.

    Equations
    Instances For
      class Std.Iterators.IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] (n : Type w → Type w'') :
      Type (max (max (w + 1) w') w'')

      IteratorLoop α m provides efficient implementations of loop-based consumers for α-based iterators. The basis is a ForIn-style loop construct with the complication that it can be used for infinite iterators, too -- given a proof that the given loop will nevertheless terminate.

      This class is experimental and users of the iterator API should not explicitly depend on it. They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library.

      Instances
        class Std.Iterators.IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] (n : Type w → Type w'') :
        Type (max (max (w + 1) w') w'')

        IteratorLoopPartial α m provides efficient implementations of loop-based consumers for α-based iterators. The basis is a partial, i.e. potentially nonterminating, ForIn instance.

        This class is experimental and users of the iterator API should not explicitly depend on it. They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library.

        Instances
          class Std.Iterators.IteratorSize (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] :
          Type (max w w')

          IteratorSize α m provides an implementation of the IterM.size function.

          This class is experimental and users of the iterator API should not explicitly depend on it. They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library.

          Instances
            class Std.Iterators.IteratorSizePartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] :
            Type (max w w')

            IteratorSizePartial α m provides an implementation of the IterM.Partial.size function that can be used as it.allowTermination.size.

            This class is experimental and users of the iterator API should not explicitly depend on it. They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library.

            Instances
              def Std.Iterators.IteratorLoop.WFRel {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {γ : Type x} {plausible_forInStep : βγForInStep γProp} (_wf : WellFounded α m plausible_forInStep) :
              Type (max w x)

              Internal implementation detail of the iterator library.

              Equations
              Instances For
                def Std.Iterators.IteratorLoop.WFRel.mk {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {γ : Type x} {plausible_forInStep : βγForInStep γProp} (wf : WellFounded α m plausible_forInStep) (it : IterM m β) (c : γ) :

                Internal implementation detail of the iterator library.

                Equations
                Instances For
                  @[irreducible, specialize #[]]
                  def Std.Iterators.IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α β : Type w} [Iterator α m β] {n : Type w → Type w''} [Monad n] (lift : (γ : Type w) → m γn γ) (γ : Type w) (plausible_forInStep : βγForInStep γProp) (wf : IteratorLoop.WellFounded α m plausible_forInStep) (it : IterM m β) (init : γ) (P : βProp) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput bP b) (f : (b : β) → P b(c : γ) → n (Subtype (plausible_forInStep b c))) :
                  n γ

                  This is the loop implementation of the default instance IteratorLoop.defaultImplementation.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[inline]
                    def Std.Iterators.IteratorLoop.defaultImplementation {β α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] :

                    This is the default implementation of the IteratorLoop class. It simply iterates through the iterator using IterM.step. For certain iterators, more efficient implementations are possible and should be used instead.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      class Std.Iterators.LawfulIteratorLoop {β : Type w} (α : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Monad n] [Iterator α m β] [Finite α m] [i : IteratorLoop α m n] :

                      Asserts that a given IteratorLoop instance is equal to IteratorLoop.defaultImplementation. (Even though equal, the given instance might be vastly more efficient.)

                      Instances
                        @[specialize #[]]
                        partial def Std.Iterators.IterM.DefaultConsumers.forInPartial {m : Type w → Type w'} {α β : Type w} [Iterator α m β] {n : Type w → Type w''} [Monad n] (lift : (γ : Type w) → m γn γ) (γ : Type w) (it : IterM m β) (init : γ) (f : (b : β) → it.IsPlausibleIndirectOutput bγn (ForInStep γ)) :
                        n γ

                        This is the loop implementation of the default instance IteratorLoopPartial.defaultImplementation.

                        @[inline]
                        def Std.Iterators.IteratorLoopPartial.defaultImplementation {β α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [Monad n] [Iterator α m β] :

                        This is the default implementation of the IteratorLoopPartial class. It simply iterates through the iterator using IterM.step. For certain iterators, more efficient implementations are possible and should be used instead.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          instance Std.Iterators.instLawfulIteratorLoopOfMonad {β : Type w} (α : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
                          theorem Std.Iterators.IteratorLoop.wellFounded_of_finite {m : Type w → Type w'} {α β γ : Type w} [Iterator α m β] [Finite α m] :
                          WellFounded α m fun (x : β) (x : γ) (x : ForInStep γ) => True
                          @[inline]
                          def Std.Iterators.IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] (lift : (γ : Type w) → m γn γ) :
                          ForIn' n (IterM m β) β { mem := fun (it : IterM m β) (out : β) => it.IsPlausibleIndirectOutput out }

                          This ForIn'-style loop construct traverses a finite iterator using an IteratorLoop instance.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[inline]
                            def Std.Iterators.IterM.instForIn' {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n] :
                            ForIn' n (IterM m β) β { mem := fun (it : IterM m β) (out : β) => it.IsPlausibleIndirectOutput out }

                            A ForIn' instance for iterators. Its generic membership relation is not easy to use, so this is not marked as instance. This way, more convenient instances can be built on top of it or future library improvements will make it more comfortable.

                            Equations
                            Instances For
                              instance Std.Iterators.instForIn'PartialMkIsPlausibleIndirectOutputItOfIteratorLoopPartialOfMonadLiftT {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] :
                              ForIn' n (IterM.Partial m β) β { mem := fun (it : IterM.Partial m β) (out : β) => it.it.IsPlausibleIndirectOutput out }
                              Equations
                              • One or more equations did not get rendered due to their size.
                              instance Std.Iterators.instForMIterMOfFiniteOfIteratorLoopOfMonadLiftT {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n] :
                              ForM n (IterM m β) β
                              Equations
                              • One or more equations did not get rendered due to their size.
                              instance Std.Iterators.instForMPartialOfFiniteOfIteratorLoopPartialOfMonadLiftT {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [Finite α m] [IteratorLoopPartial α m n] [MonadLiftT m n] :
                              ForM n (IterM.Partial m β) β
                              Equations
                              • One or more equations did not get rendered due to their size.
                              @[inline]
                              def Std.Iterators.IterM.foldM {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] {α β γ : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n] (f : γβn γ) (init : γ) (it : IterM m β) :
                              n γ

                              Folds a monadic function over an iterator from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

                              The monadic effects of f are interleaved with potential effects caused by the iterator's step function. Therefore, it may not be 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.

                              Equations
                              Instances For
                                @[inline]
                                def Std.Iterators.IterM.Partial.foldM {m n : Type w → Type w'} [Monad n] {α β γ : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] (f : γβn γ) (init : γ) (it : Partial m β) :
                                n γ

                                Folds a monadic function over an iterator from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

                                The monadic effects of f are interleaved with potential effects caused by the iterator's step function. Therefore, it may not be 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.

                                Equations
                                Instances For
                                  @[inline]
                                  def Std.Iterators.IterM.fold {m : Type w → Type w'} {α β γ : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] (f : γβγ) (init : γ) (it : IterM m β) :
                                  m γ

                                  Folds a function over an iterator from the left, accumulating a value starting with init. 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.

                                  Equations
                                  Instances For
                                    @[inline]
                                    def Std.Iterators.IterM.Partial.fold {m : Type w → Type w'} {α β γ : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] (f : γβγ) (init : γ) (it : Partial m β) :
                                    m γ

                                    Folds a function over an iterator from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

                                    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.

                                    Equations
                                    Instances For
                                      @[inline]
                                      def Std.Iterators.IterM.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] [Finite α m] (it : IterM m β) [IteratorLoop α m m] :

                                      Iterates over the whole iterator, applying the monadic effects of each step, discarding all emitted values.

                                      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.drain instead of it.drain. However, it is not possible to formally verify the behavior of the partial variant.

                                      Equations
                                      Instances For
                                        @[inline]
                                        def Std.Iterators.IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] (it : Partial m β) [IteratorLoopPartial α m m] :

                                        Iterates over the whole iterator, applying the monadic effects of each step, discarding all emitted values.

                                        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.drain instead.

                                        Equations
                                        Instances For
                                          @[inline]
                                          def Std.Iterators.IterM.DefaultConsumers.size {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] [IteratorLoop α m m] [Finite α m] (it : IterM m β) :

                                          This is the implementation of the default instance IteratorSize.defaultImplementation.

                                          Equations
                                          Instances For
                                            @[inline]
                                            def Std.Iterators.IterM.DefaultConsumers.sizePartial {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] [IteratorLoopPartial α m m] (it : IterM m β) :

                                            This is the implementation of the default instance IteratorSizePartial.defaultImplementation.

                                            Equations
                                            Instances For
                                              @[inline]
                                              def Std.Iterators.IteratorSize.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] :

                                              This is the default implementation of the IteratorSize class. It simply iterates using IteratorLoop and counts the elements. For certain iterators, more efficient implementations are possible and should be used instead.

                                              Equations
                                              Instances For
                                                @[inline]

                                                This is the default implementation of the IteratorSizePartial class. It simply iterates using IteratorLoopPartial and counts the elements. For certain iterators, more efficient implementations are possible and should be used instead.

                                                Equations
                                                @[inline]
                                                def Std.Iterators.IterM.size {α : Type} {m : TypeType w'} {β : Type} [Iterator α m β] [Monad m] (it : IterM m β) [IteratorSize α m] :
                                                m Nat

                                                Computes how many elements the iterator returns. In monadic situations, it is unclear which effects are caused by calling size, and if the monad is nondeterministic, it is also unclear what the 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.

                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Std.Iterators.IterM.Partial.size {α : Type} {m : TypeType w'} {β : Type} [Iterator α m β] [Monad m] (it : Partial m β) [IteratorSizePartial α m] :
                                                  m Nat

                                                  Computes how many elements the iterator emits.

                                                  With monadic iterators (IterM), it is unclear which effects are caused by calling size, and if the monad is nondeterministic, it is also unclear what the 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.

                                                  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.

                                                  Equations
                                                  Instances For