FS.Pull

(source)

General operations on `Pull`s
and `Stream`s: Splits, scans, filters, and maps

It is suggested to import this qualified `import FS.Pull as P` or
via the catch-all module `FS` and use qualified names such
as `P.filter` for those functions that overlap with the ones
from `FS.Chunk`.

Reexports

import public FS.Core

Definitions

data UnfoldRes : Type -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

More : o -> s -> UnfoldRes r s o
Done : r -> UnfoldRes r s o
Last : r -> o -> UnfoldRes r s o

emits : List o -> Stream f es o

  Emits a list of chunks.

Totality: total
Visibility: export

emitList : List o -> Stream f es (List o)

  Emits a list of values as a single chunk.

Totality: total
Visibility: export

emitMaybe : Maybe o -> Stream f es o

  Emits a single optional value.

Totality: total
Visibility: export

emitSnoc : SnocList o -> Maybe o -> Stream f es (List o)

  Utility to emit a single list chunk from a snoc list.

Totality: total
Visibility: export

eval : f es o -> Stream f es o

  Emits a single chunk of output generated from an effectful
  computation.

Totality: total
Visibility: export

unfold : s -> (s -> UnfoldRes r s o) -> Pull f o es r

  Like `unfold` but emits values in larger chunks.
  
  This allows us to potentially emit a bunch of values right before
  we are done.
  
  This overlaps with function `FS.Chunk.unfold`, so it is typically
  used qualified: `P.unfold`.

Totality: total
Visibility: export

unfoldEval : s -> (s -> f es (UnfoldRes r s o)) -> Pull f o es r

  Like `unfold` but produces values via an effectful computation
  until a `Done` or `Last` is returned.

Totality: total
Visibility: export

unfoldEvalMaybe : f es (Maybe o) -> Stream f es o

  Produces values via an effectful computation
  until a `Nothing` is returned.

Totality: total
Visibility: export

fill : o -> Pull f o es ()

  Infinitely produces chunks of values of the given size

Totality: total
Visibility: export

iterate : o -> (o -> o) -> Pull f o es ()

  An infinite stream of values of type `o` where
  the next value is built from the previous one by
  applying the given function.

Totality: total
Visibility: export

replicate : Nat -> o -> Stream f es o

  Produces the given chunk of value `n` times.

Totality: total
Visibility: export

repeat : Stream f es o -> Pull f o es ()

  Infinitely cycles through the given `Pull`

Totality: total
Visibility: export

consMaybe : Maybe o -> Pull f o es r -> Pull f o es r

  Prepends the given optional output to a pull.

Totality: total
Visibility: export

cycle : (as : List a) -> {auto 0 _ : NonEmpty as} -> Stream f es a

  Infinitely cycles through the values in the given
  non-empty list.

Totality: total
Visibility: export

data BreakInstruction : Type

Totality: total
Visibility: public export
Constructors:

TakeHit : BreakInstruction

  Take the first succeeding value as part of the emitted prefix

PostHit : BreakInstruction

  Keep the succeeding value as part of the postfix.

DropHit : BreakInstruction

  Discard the succeeding value

peek : Pull f o es r -> Pull f q es (Either r (o, Pull f o es r))

  Like `uncons` but does not consume the chunk

Totality: total
Visibility: export

peekRes : Pull f o es r -> Pull f q es (Either r (Pull f o es r))

  Like `peeks` but only checks if the pull has been exhausted or not.

Totality: total
Visibility: export

drain : Pull f o es r -> Pull f q es r

  Empties a stream silently dropping all output.

Totality: total
Visibility: export

splitAt : Nat -> Pull f o es r -> Pull f o es (Pull f o es r)

  Emits the first `n` values of a `Pull`, returning the remainder.
  
  In case the remaining pull is exhausted, with will wrap the
  final result in a `Left`, otherwise, the (non-empty) remainder will be
  wrapped in a right.

Totality: total
Visibility: export

take : Nat -> Pull f o es r -> Stream f es o

  Emits only the first `n` values of a `Stream`.

Totality: total
Visibility: export

limit : Has e es => Lazy e -> Nat -> Pull f o es r -> Pull f o es r

  Like `take` but limits the number of emitted values.
  
  This fails with the given error in case the limit is exceeded.
  
  Note: This tries to read past the end of a pull by invoking `peekRes`.
        This is not suitable for limitting the input from a stream that
        blocks once it is exhausted.

Totality: total
Visibility: export

drop : Nat -> Pull f o es r -> Pull f o es r

  Discards the first `n` values of a `Stream`, returning the
  remainder.

Totality: total
Visibility: export

head : Pull f o es r -> Stream f es o

  Only keeps the first element of the input.

Totality: total
Visibility: export

tail : Pull f o es r -> Pull f o es r

  Drops the first element of the input.

Totality: total
Visibility: export

data BreakRes : Type -> Type

  Result of splitting a value into two parts. This is used to
  split up streams of data along logical boundaries.

Totality: total
Visibility: public export
Constructors:

Broken : Maybe c -> Maybe c -> BreakRes c

  The value was broken and we got a (possibly empty) pre- and postfix.

Keep : c -> BreakRes c

  The value could not be broken.

breakPull : (r -> Pull f o es r) -> (o -> BreakRes o) -> Pull f o es r -> Pull f o es (Pull f o es r)

  Uses the given breaking function to break the pull into
  a prefix of emitted chunks and a suffix that is returned as
  the result.

Totality: total
Visibility: export

breakFull : (r -> Pull f o es r) -> BreakInstruction -> (o -> Bool) -> Pull f o es r -> Pull f o es (Pull f o es r)

  Breaks a pull as soon as the given predicate returns `True`.
  
  The `BreakInstruction` dictates, if the value, for which the
  predicate held, should be emitted as part of the prefix or the
  suffix, or if it should be discarded.

Totality: total
Visibility: export

forceBreakFull : Has e es => Lazy e -> BreakInstruction -> (o -> Bool) -> Pull f o es r -> Pull f o es (Pull f o es r)

  Like `breakFull` but fails with the given execption if no
  breaking point was found.

Totality: total
Visibility: export

takeUntil : BreakInstruction -> (o -> Bool) -> Pull f o es r -> Stream f es o

  Emits values until the given predicate returns `True`.
  
  The `BreakInstruction` dictates, if the value, for which the
  predicate held, should be emitted as part of the prefix or not.

Totality: total
Visibility: export

takeWhile : (o -> Bool) -> Pull f o es r -> Stream f es o

  Emits values until the given predicate returns `False`,
  returning the remainder of the `Pull`.

Totality: total
Visibility: export

takeThrough : (o -> Bool) -> Pull f o es r -> Stream f es o

  Like `takeWhile` but also includes the first failure.

Totality: total
Visibility: export

takeWhileJust : Pull f (Maybe o) es r -> Stream f es o

  Emits values until the given pull emits a `Nothing`.

Totality: total
Visibility: export

dropUntil : BreakInstruction -> (o -> Bool) -> Pull f o es r -> Pull f o es r

  Discards values until the given predicate returns `True`.
  
  The `BreakInstruction` dictates, if the value, for which the
  predicate held, should be emitted as part of the remainder or not.

Totality: total
Visibility: export

dropWhile : (o -> Bool) -> Pull f o es r -> Pull f o es r

  Drops values from a stream while the given predicate returns `True`,
  returning the remainder of the stream.

Totality: total
Visibility: export

dropThrough : (o -> Bool) -> Pull f o es r -> Pull f o es r

  Like `dropWhile` but also drops the first value where
  the predicate returns `False`.

Totality: total
Visibility: export

mapMaybe : (o -> Maybe p) -> Pull f o es r -> Pull f p es r

  Maps chunks of output via a partial function.

Totality: total
Visibility: export

catMaybes : Pull f (Maybe o) es r -> Pull f o es r

  Emits a values wrapped in a `Just` from the initial stream.

Totality: total
Visibility: export

mapRight : (o -> Either e p) -> Pull f o es r -> Pull f p es r

  Emits the values, for which the given function returns a `Right`.

Totality: total
Visibility: export

catRights : Pull f (Either e o) es r -> Pull f o es r

  Emits the values wrapped `Rights`.

Totality: total
Visibility: export

mapLeft : (o -> Either e p) -> Pull f o es r -> Pull f e es r

  Emits the values, for which the given function returns a `Right`.

Totality: total
Visibility: export

catLefts : Pull f (Either e o) es r -> Pull f e es r

  Emits the values wrapped `Rights`.

Totality: total
Visibility: export

mapOutput : (o -> p) -> Pull f o es r -> Pull f p es r

  Chunk-wise maps the emit of a `Pull`

Totality: total
Visibility: export

evalMap : (o -> f es p) -> Pull f o es r -> Pull f p es r

  Chunk-wise effectful mapping of the emit of a `Pull`

Totality: total
Visibility: export

evalMapMaybe : (o -> f es (Maybe p)) -> Pull f o es r -> Pull f p es r

  Chunk-wise effectful mapping of the emit of a `Pull`

Totality: total
Visibility: export

filter : (o -> Bool) -> Pull f o es r -> Pull f o es r

  Chunk-wise filters the emit of a `Pull` emitting only the
  values that fulfill the given predicate

Totality: total
Visibility: export

filterNot : (o -> Bool) -> Pull f o es r -> Pull f o es r

  Convenience alias for `filterC (not . pred)`.

Totality: total
Visibility: export

endWithNothing : Pull f o es r -> Pull f (Maybe o) es r

  Wraps the values emitted by this stream in a `Just` and
  marks its end with a `Nothing`.

Totality: total
Visibility: export

pairLastOr : Lazy o -> Pull f o es r -> Pull f p es (o, r)

  Returns the first output of this stream and pairs it with the
  result.
  
  The remainder of the pull is drained and run to completion.

Totality: total
Visibility: export

lastOr : Lazy o -> Stream f es o -> Pull f p es o

  Like `pairLastOr` but operates on a stream and therefore only returns
  the last output.

Totality: total
Visibility: export

pairLastOrErr : Has e es => Lazy e -> Pull f o es r -> Pull f p es (o, r)

  Like `firstOr` but fails with the given error in case no
  value is emitted.

Totality: total
Visibility: export

lastOrErr : Has e es => Lazy e -> Stream f es o -> Pull f p es o

  Like `pairLastOrErr` but operates on a stream and therefore only returns
  the last output.

Totality: total
Visibility: export

fold : (p -> o -> p) -> p -> Pull f o es r -> Pull f p es r

  Folds the emit of a pull using an initial value and binary operator.
  
  The accumulated result is emitted as a single value.

Totality: total
Visibility: export

foldPair : (p -> o -> p) -> p -> Pull f o es r -> Pull f q es (p, r)

  Like `fold` but instead of emitting the result as a single
  value of output, it is paired with the `Pull`s result.

Totality: total
Visibility: export

foldPairE : Has e es => (p -> o -> Either e p) -> p -> Pull f o es r -> Pull f q es (p, r)

  Like `foldPair` but with a function that can fail.

Totality: total
Visibility: export

foldGet : (p -> o -> p) -> p -> Stream f es o -> Pull f q es p

  Convenience version of `foldPair` for working on streams.

Totality: total
Visibility: export

fold1 : (o -> o -> o) -> Pull f o es r -> Pull f o es r

  Like `foldC` but will not emit a value in case of an empty pull.

Totality: total
Visibility: export

all : (o -> Bool) -> Pull f o es r -> Stream f es Bool

  Emits `True` if all emitted values of the given stream fulfill
  the given predicate

Totality: total
Visibility: export

any : (o -> Bool) -> Pull f o es r -> Stream f es Bool

  Returns `True` if any of the emitted values of the given stream fulfills
  the given predicate

Totality: total
Visibility: export

sum : Num o => Pull f o es r -> Pull f o es r

  Sums up the emitted chunks.

Totality: total
Visibility: export

count : Pull f o es r -> Pull f Nat es r

  Counts the number of emitted chunks.

Totality: total
Visibility: export

maximum : Ord o => Pull f o es r -> Pull f o es r

  Emits the largest output encountered.

Totality: total
Visibility: export

minimum : Ord o => Pull f o es r -> Pull f o es r

  Emits the smallest output encountered.

Totality: total
Visibility: export

mappend : Semigroup o => Pull f o es r -> Pull f o es r

  Emits the smallest output encountered.

Totality: total
Visibility: export

foldMap : Monoid m => (o -> m) -> Pull f o es r -> Pull f m es r

  Accumulates the emitted values over a monoid.
  
  Note: This corresponds to a left fold, so it will
        run in quadratic time for monoids that are
        naturally accumulated from the right (such as List)

Totality: total
Visibility: export

evalFold : (p -> o -> f es p) -> p -> Pull f o es r -> Pull f p es r

  Folds the emit of a pull using an initial value and binary operator.
  
  The accumulated result is emitted as a single value.

Totality: total
Visibility: export

evalFoldPair : (p -> o -> f es p) -> p -> Pull f o es r -> Pull f q es (p, r)

  Like `fold` but instead of emitting the result as a single
  value of output, it is paired with the `Pull`s result.

Totality: total
Visibility: export

evalFoldGet : (p -> o -> f es p) -> p -> Stream f es o -> Pull f q es p

  Convenience version of `evalFoldPair` for working on streams.

Totality: total
Visibility: export

scan : s -> (s -> o -> (p, s)) -> Pull f o es r -> Pull f p es r

  Runs a stateful computation across all chunks of data.

Totality: total
Visibility: export

scanReturn : s -> (s -> o -> (p, s)) -> Stream f es o -> Pull f p es s

  Like `scan` but returns the final state as the pull's result

Totality: total
Visibility: export

escanReturn : s -> (s -> o -> Result es (p, s)) -> Stream f es o -> Pull f p es s

  Like `scanReturn` but with the possibility of failure

Totality: total
Visibility: export

distinctBy : (o -> o -> Bool) -> Pull f o es r -> Pull f o es r

  Emits values of the original pull, but emits consecutive
  values for which `f` returns `True` only once.
  
  Note: For this to work correctly, `f` must be an equivalence relation.
        This function makes no guarantees about the order in which arguments
        are passed to `f`, so `f` must be symmetric. It also makes
        no guarantees about which emitted value is being kept in its
        internal state, so `f` must be transitive.

Totality: total
Visibility: export

distinct : Eq o => Pull f o es r -> Pull f o es r

  Emits values of the original pull, but emits consecutive
  identical values only once.

Totality: total
Visibility: export

scanMaybe : s -> (s -> Maybe (o -> (p, s))) -> Pull f o es r -> Pull f p es s

  General stateful conversion of a `Pull`s emit.
  
  Aborts as soon as the given accumulator function returns `Nothing`

Totality: total
Visibility: export

scanFull : s -> (s -> o -> (Maybe p, s)) -> (s -> Maybe p) -> Pull f o es r -> Pull f p es r

  Like `scan` but will possibly also emit the final state.

Totality: total
Visibility: export

zipWithScan : p -> (p -> o -> p) -> Pull f o es r -> Pull f (o, p) es r

  Zips the input with a running total, up to but
  not including the current element.

Totality: total
Visibility: export

zipWithScan1 : p -> (p -> o -> p) -> Pull f o es r -> Pull f (o, p) es r

  Like `zipWithScan` but the running total is including the current element.

Totality: total
Visibility: export

zipWithIndex : Pull f o es r -> Pull f (o, Nat) es r

  Pairs each element in the stream with its 0-based index.

Totality: total
Visibility: export

zipWithCount : Pull f o es r -> Pull f (o, Nat) es r

  Pairs each element in the stream with its 1-based count.

Totality: total
Visibility: export

scans : p -> (p -> o -> p) -> Pull f o es r -> Pull f p es r

  Accumulates the input value using the given function.
  
  The emitted result will include the input up to but
  not including the current value.

Totality: total
Visibility: export

scans1 : p -> (p -> o -> p) -> Pull f o es r -> Pull f p es r

  Like `scans` but the running total is including the current element.
  
  Emits the initial value as its first output.

Totality: total
Visibility: export

scanFrom : o -> Pull f (o -> o) es r -> Pull f o es r

  Like `scans` but specialized to a pull of unary functions.

Totality: total
Visibility: export

scanFrom1 : o -> Pull f (o -> o) es r -> Pull f o es r

  Like `scans1` but specialized to a pull of unary functions.

Totality: total
Visibility: export

runningCount : Pull f o es r -> Pull f Nat es r

  Emits the count of each element.

Totality: total
Visibility: export

evalScan : s -> (s -> o -> f es (p, s)) -> Pull f o es r -> Pull f p es r

  Like `scan` but with an effectful computation.

Totality: total
Visibility: export

evalScans : Functor (f es) => p -> (p -> o -> f es p) -> Pull f o es r -> Pull f p es r

  Accumulates the input value using the given function.
  
  The emitted result will include the input up to but
  not including the current value.

Totality: total
Visibility: export

evalScans1 : Functor (f es) => p -> (p -> o -> f es p) -> Pull f o es r -> Pull f p es r

  Like `scans` but the running total is including the current element.

Totality: total
Visibility: export

evalScanFrom : Functor (f es) => o -> Pull f (o -> f es o) es r -> Pull f o es r

  Like `evalScans` but specialized to a pull of unary effectful functions.

Totality: total
Visibility: export

evalScanFrom1 : Functor (f es) => o -> Pull f (o -> f es o) es r -> Pull f o es r

  Like `evalScans1` but specialized to a pull of unary effectful functions.

Totality: total
Visibility: export

foreach : (o -> f es ()) -> Pull f o es r -> Pull f q es r

  Performs the given action on each emitted chunk of values, thus draining
  the stream, consuming all its output.
  
  For acting on output without actually draining the stream, see
  `observe` and `observe1`.

Totality: total
Visibility: export

foreach' : f es () -> Pull f o es r -> Pull f q es r

  Utility alias for `foreach . const`.

Totality: total
Visibility: export

observe : (o -> f es ()) -> Pull f o es r -> Pull f o es r

  Performs the given action on every chunk of values of the stream without
  otherwise affecting the emitted values.

Totality: total
Visibility: export

observe' : f es () -> Pull f o es r -> Pull f o es r

  Utility alias for `observe . const`.

Totality: total
Visibility: export

flatMap : Pull f o es r -> (o -> Stream f es p) -> Pull f p es r

  Converts every chunk of output to a new stream,
  concatenating the resulting streams before emitting the final
  result.

Totality: total
Visibility: export

bind : (o -> Pull f p es ()) -> Pull f o es r -> Pull f p es r

  Flipped version of `flatMapC`

Totality: total
Visibility: export

attemptOutput : Pull f o es () -> Pull f (Result es o) fs ()

Totality: total
Visibility: export

stepLeg : Stream f es o -> Pull f p es (Maybe (StepLeg f es o))

  This is an internal utility to run the remainder of a stream
  in the correct scope.

Totality: total
Visibility: export

step : StepLeg f es o -> Pull f p es (Maybe (StepLeg f es o))

  Runs a `StepLeg` in its scope, returning then next `StepLeg`.

Totality: total
Visibility: export

0 ZipWithLeft : (List Type -> Type -> Type) -> List Type -> Type -> Type -> Type

  Type alias for a function that converts a stream plus
  a prefix to a stream emitting different values.

Totality: total
Visibility: public export

zipAllWith : o1 -> o2 -> (o1 -> o2 -> o3) -> Stream f es o1 -> Stream f es o2 -> Stream f es o3

  Determinsitically zips elements with the specified function, terminating
  when the ends of both branches are reached naturally, padding the left
  branch with `pad1` and padding the right branch with `pad2` as necessary.

Totality: total
Visibility: export

zipAll : o1 -> o2 -> Stream f es o1 -> Stream f es o2 -> Stream f es (o1, o2)

  `zipAllWith` specialized to returning a pair of values

Totality: total
Visibility: export

zipWith : (o1 -> o2 -> o3) -> Stream f es o1 -> Stream f es o2 -> Stream f es o3

  Deterministically zips elements, terminating when the end
  of either branch is reached naturally.

Totality: total
Visibility: export

zip : Stream f es o1 -> Stream f es o2 -> Stream f es (o1, o2)

  `zipAll` specialized to returning a pair of values

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 6

zipRight : Stream f es o1 -> Stream f es o2 -> Stream f es o2

Totality: total
Visibility: export

zipLeft : Stream f es o1 -> Stream f es o2 -> Stream f es o1

Totality: total
Visibility: export

hzip : All (Stream f es) ts -> Stream f es (HList ts)

  Zips the values in a heterogeneous list of streams.

Totality: total
Visibility: export

0 HZipFun : List Type -> Type -> Type

Totality: total
Visibility: public export

happly : HZipFun ts r -> HList ts -> r

Totality: total
Visibility: export

hzipWith : HZipFun ts r -> All (Stream f es) ts -> Stream f es r

  Zips the given streams applying the resulting heterogeneous
  lists of values to the given function.

Totality: total
Visibility: export