Documentation

Std.Data.Iterators.Combinators.Monadic.DropWhile

Monadic dropWhile iterator combinator #

This module provides the iterator combinator IterM.dropWhile that will drop all values emitted by a given iterator until a given predicate on these values becomes false the first fime. Beginning with that moment, the combinator will forward all emitted values.

Several variants of this combinator are provided:

@[unbox]
structure Std.Iterators.DropWhile (α : Type w) (m : Type w → Type w') (β : Type w) (P : βPostconditionT m (ULift Bool)) :

Internal state of the dropWhile combinator. Do not depend on its internals.

  • dropping : Bool

    Internal implementation detail of the iterator library.

  • inner : IterM m β

    Internal implementation detail of the iterator library.

Instances For
    @[inline]
    def Std.Iterators.IterM.Intermediate.dropWhileWithPostcondition {α : Type w} {m : Type w → Type w'} {β : Type w} (P : βPostconditionT m (ULift Bool)) (dropping : Bool) (it : IterM m β) :
    IterM m β

    Constructs intermediate states of an iterator created with the combinator IterM.dropWhileWithPostcondition. When it.dropWhileWithPostcondition P has stopped dropping elements, its new state cannot be created directly with IterM.dropWhileWithPostcondition but only with Intermediate.dropWhileWithPostcondition.

    Intermediate.dropWhileWithPostcondition is meant to be used only for internally or for verification purposes.

    Equations
    Instances For
      @[inline]
      def Std.Iterators.IterM.Intermediate.dropWhileM {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] (P : βm (ULift Bool)) (dropping : Bool) (it : IterM m β) :
      IterM m β

      Constructs intermediate states of an iterator created with the combinator IterM.dropWhileM. When it.dropWhileM P has stopped dropping elements, its new state cannot be created directly with IterM.dropWhileM but only with Intermediate.dropWhileM.

      Intermediate.dropWhileM is meant to be used only for internally or for verification purposes.

      Equations
      Instances For
        @[inline]
        def Std.Iterators.IterM.Intermediate.dropWhile {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] (P : βBool) (dropping : Bool) (it : IterM m β) :
        IterM m β

        Constructs intermediate states of an iterator created with the combinator IterM.dropWhile. When it.dropWhile P has stopped dropping elements, its new state cannot be created directly with IterM.dropWhile but only with Intermediate.dropWhile.

        Intermediate.dropWhile is meant to be used only for internally or for verification purposes.

        Equations
        Instances For
          @[inline]
          def Std.Iterators.IterM.dropWhileWithPostcondition {α : Type w} {m : Type w → Type w'} {β : Type w} (P : βPostconditionT m (ULift Bool)) (it : IterM m β) :
          IterM m β

          Note: This is a very general combinator that requires an advanced understanding of monads, dependent types and termination proofs. The variants dropWhile and dropWhileM are easier to use and sufficient for most use cases.

          Given an iterator it and a monadic predicate P, it.dropWhileWithPostcondition P is an iterator that emits the values emitted by it starting from the first value that is rejected by P. The elements before are dropped.

          P is expected to return PostconditionT m (ULift Bool). The PostconditionT transformer allows the caller to intrinsically prove properties about P's return value in the monad m, enabling termination proofs depending on the specific behavior of P.

          Marble diagram (ignoring monadic effects):

          Assuming that the predicate P accepts a and b but rejects c:

          it                                ---a----b---c--d-e--⊥
          it.dropWhileWithPostcondition P   ------------c--d-e--⊥
          
          it                                ---a----⊥
          it.dropWhileWithPostcondition P   --------⊥
          

          Termination properties:

          • Finite instance: only if it is finite
          • Productive instance: only if it is finite

          Depending on P, it is possible that it.dropWhileWithPostcondition P is finite (or productive) although it is not. In this case, the Finite (or Productive) instance needs to be proved manually.

          Performance:

          This combinator calls P on each output of it until the predicate evaluates to false. After that, the combinator incurs an addictional O(1) cost for each value emitted by it.

          Equations
          Instances For
            @[inline]
            def Std.Iterators.IterM.dropWhileM {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] (P : βm (ULift Bool)) (it : IterM m β) :
            IterM m β

            Given an iterator it and a monadic predicate P, it.dropWhileM P is an iterator that emits the values emitted by it starting from the first value that is rejected by P. The elements before are dropped.

            If P is pure, then the simpler variant dropWhile can be used instead.

            Marble diagram (ignoring monadic effects):

            Assuming that the predicate P accepts a and b but rejects c:

            it                ---a----b---c--d-e--⊥
            it.dropWhileM P   ------------c--d-e--⊥
            
            it                ---a----⊥
            it.dropWhileM P   --------⊥
            

            Termination properties:

            • Finite instance: only if it is finite
            • Productive instance: only if it is finite

            Depending on P, it is possible that it.dropWhileM P is finite (or productive) although it is not. In this case, the Finite (or Productive) instance needs to be proved manually. Use dropWhileWithPostcondition if the termination behavior depends on P's behavior.

            Performance:

            This combinator calls P on each output of it until the predicate evaluates to false. After that, the combinator incurs an addictional O(1) cost for each value emitted by it.

            Equations
            Instances For
              @[inline]
              def Std.Iterators.IterM.dropWhile {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] (P : βBool) (it : IterM m β) :
              IterM m β

              Given an iterator it and a predicate P, it.dropWhile P is an iterator that emits the values emitted by it starting from the first value that is rejected by P. The elements before are dropped.

              In situations where P is monadic, use dropWhileM instead.

              Marble diagram (ignoring monadic effects):

              Assuming that the predicate P accepts a and b but rejects c:

              it               ---a----b---c--d-e--⊥
              it.dropWhile P   ------------c--d-e--⊥
              
              it               ---a----⊥
              it.dropWhile P   --------⊥
              

              Termination properties:

              • Finite instance: only if it is finite
              • Productive instance: only if it is finite

              Depending on P, it is possible that it.dropWhileM P is productive although it is not. In this case, the Productive instance needs to be proved manually.

              Performance:

              This combinator calls P on each output of it until the predicate evaluates to false. After that, the combinator incurs an addictional O(1) cost for each value emitted by it.

              Equations
              Instances For
                inductive Std.Iterators.DropWhile.PlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {P : βPostconditionT m (ULift Bool)} (it : IterM m β) (step : IterStep (IterM m β) β) :

                it.PlausibleStep step is the proposition that step is a possible next step from the dropWhile iterator it. This is mostly internally relevant, except if one needs to manually prove termination (Finite or Productive instances, for example) of a dropWhile iterator.

                Instances For
                  @[inline]
                  instance Std.Iterators.DropWhile.instIterator {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] {P : βPostconditionT m (ULift Bool)} :
                  Iterator (DropWhile α m β P) m β
                  Equations
                  • One or more equations did not get rendered due to their size.
                  instance Std.Iterators.DropWhile.instFinite {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Finite α m] {P : βPostconditionT m (ULift Bool)} :
                  Finite (DropWhile α m β P) m