FS.Chunk

(source)

Utilities for working with chunks of data.

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

Definitions

record ChunkSize : Type

  Pulls and streams produce their output in chunks (lists of value)
  for reasons of efficiency, because the whole streaming machinery
  comes with quite a bit of a performance overhead.
  
  Many functions for generating pure streams
  and pulls therefore take an auto-implicit value of type `ChunkSize`.
  If not provided explicitly, this defaults to 128.

Totality: total
Visibility: public export
Constructor:

CS : (size : Nat) -> {auto 0 _ : IsSucc size} -> ChunkSize

Projections:

0 .prf : ({rec:0} : ChunkSize) -> IsSucc (size {rec:0})
.size : ChunkSize -> Nat

Hints:

ChunkSize
Eq ChunkSize
Ord ChunkSize
Show ChunkSize

.size : ChunkSize -> Nat

Totality: total
Visibility: public export

size : ChunkSize -> Nat

Totality: total
Visibility: public export

0 .prf : ({rec:0} : ChunkSize) -> IsSucc (size {rec:0})

Totality: total
Visibility: public export

0 prf : ({rec:0} : ChunkSize) -> IsSucc (size {rec:0})

Totality: total
Visibility: public export

fromInteger : Integer -> ChunkSize

Totality: total
Visibility: export

defaultChunkSize : ChunkSize

Totality: total
Visibility: public export

data SplitRes : Type -> Type

Totality: total
Visibility: public export
Constructors:

Middle : c -> c -> SplitRes c
All : Nat -> SplitRes c

interface Chunk : Type -> Type -> Type

  A `Chunk c o` is a container type `c` holding elements of type `o`.
  
  Examples include `List a` with element type `a` and `ByteString` with
  element type `Bits8`.

Parameters: c, o
Constraints: Monoid c
Methods:

unfoldChunk : ChunkSize => (s -> Either r (o, s)) -> s -> UnfoldRes r s c
replicateChunk : ChunkSize => o -> c
isEmpty : c -> Bool
unconsChunk : c -> Maybe (o, Maybe c)
splitChunkAt : Nat -> c -> SplitRes c
breakChunk : BreakInstruction -> (o -> Bool) -> c -> BreakRes c
filterChunk : (o -> Bool) -> c -> Maybe c

Implementations:

Chunk (List a) a
Chunk ByteString Bits8

unfoldChunk : Chunk c o => ChunkSize => (s -> Either r (o, s)) -> s -> UnfoldRes r s c

Totality: total
Visibility: public export

replicateChunk : Chunk c o => ChunkSize => o -> c

Totality: total
Visibility: public export

isEmpty : Chunk c o => c -> Bool

Totality: total
Visibility: public export

unconsChunk : Chunk c o => c -> Maybe (o, Maybe c)

Totality: total
Visibility: public export

splitChunkAt : Chunk c o => Nat -> c -> SplitRes c

Totality: total
Visibility: public export

breakChunk : Chunk c o => BreakInstruction -> (o -> Bool) -> c -> BreakRes c

Totality: total
Visibility: public export

filterChunk : Chunk c o => (o -> Bool) -> c -> Maybe c

Totality: total
Visibility: public export

nonEmpty : Chunk c o => c -> Maybe c

Totality: total
Visibility: export

unfold : ChunkSize => Chunk c o => s -> (s -> Either r (o, s)) -> Pull f c es r

  Like `unfold` but generates chunks of values of up to the given size.

Totality: total
Visibility: export

fill : ChunkSize => (0 c : Type) -> Chunk c o => o -> Pull f c es ()

  Like `P.fill` but generates chunks of values of up to the given size.

Totality: total
Visibility: export

iterate : ChunkSize => (0 c : Type) -> Chunk c o => o -> (o -> o) -> Pull f c es ()

  Like `P.iterate` but generates chunks of values of up to the given size.

Totality: total
Visibility: export

replicate : ChunkSize => (0 c : Type) -> Chunk c o => Nat -> o -> Stream f es c

  Like `P.replicate` but generates chunks of values of up to the given size.

Totality: total
Visibility: export

uncons : Chunk c o => Pull f c es r -> Pull f q es (Either r (o, Pull f c es r))

  Splits the very first element from the head of a `Pull`

Totality: total
Visibility: export

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

  Emits the first `n` elements of a `Pull`, returning the remainder.

Totality: total
Visibility: export

take : Chunk c o => Nat -> Pull f c es r -> Pull f c es ()

  Emits the first `n` elements of a `Pull`, returning the remainder.

Totality: total
Visibility: export

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

  Like `take` but limits the number of emitted values.
  
  This fails with the given error in case the limit is exceeded.

Totality: total
Visibility: export

drop : Chunk c o => Nat -> Pull f c es r -> Pull f c es r

  Drops the first `n` elements of a `Pull`, returning the
  remainder.

Totality: total
Visibility: export

head : Chunk c o => Pull f c es r -> Pull f c es ()

  Emits the first element of a `Pull`, returning the remainder.

Totality: total
Visibility: export

tail : Chunk c o => Pull f c es r -> Pull f c es r

  Discards the first element of a `Pull`.

Totality: total
Visibility: export

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

  Breaks a pull as soon as the given predicate returns `True` for
  an emitted element.
  
  `orElse` determines what to do if the pull is exhausted before any
  splitting of output occurred.
  
  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 : Chunk c o => Has e es => Lazy e -> BreakInstruction -> (o -> Bool) -> Pull f c es r -> Pull f c es (Pull f c es r)

  Like `breakFull` but fails with an error if the `Pull` is
  exhausted before the prediate returns `True`.

Totality: total
Visibility: export

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

  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 : Chunk c o => (o -> Bool) -> Pull f c es r -> Stream f es c

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

Totality: total
Visibility: export

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

  Like `takeWhile` but also includes the first failure.

Totality: total
Visibility: export

dropUntil : Chunk c o => BreakInstruction -> (o -> Bool) -> Pull f c es r -> Pull f c 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 : Chunk c o => (o -> Bool) -> Pull f c es r -> Pull f c es r

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

split : Chunk c o => (o -> Bool) -> Pull f c es r -> Pull f (List c) es r

  Splits a stream of chunks whenever an element fulfills the given
  predicate.

Totality: total
Visibility: export

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

  Maps elements of output via a partial function.

Totality: total
Visibility: export

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

  Element-wise filtering of a stream of chunks.

Totality: total
Visibility: export

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

  Element-wise filtering of a stream of chunks.

Totality: total
Visibility: export

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

  Maps a function over all elements emitted by a pull.

Totality: total
Visibility: export

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

Totality: total
Visibility: export

foldPair : Foldable t => (p -> o -> p) -> p -> Pull f (t 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

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

  Convenience version of `foldPair` for working on streams.

Totality: total
Visibility: export

fold1 : Foldable t => Chunk (t o) o => (o -> o -> o) -> Pull f (t 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 : Foldable t => (o -> Bool) -> Pull f (t o) es r -> Stream f es Bool

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

Totality: total
Visibility: export

any : Foldable t => (o -> Bool) -> Pull f (t 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 : Foldable t => Num o => Pull f (t o) es r -> Pull f o es r

  Emits the sum over all elements emitted by a `Pull`.

Totality: total
Visibility: export

count : Foldable t => Pull f (t o) es r -> Pull f Nat es r

  Emits the number of elements emitted by a `Pull`.

Totality: total
Visibility: export

maximum : Foldable t => Chunk (t o) o => Ord o => Pull f (t o) es r -> Pull f o es r

  Emits the largest output encountered.

Totality: total
Visibility: export

minimum : Foldable t => Chunk (t o) o => Ord o => Pull f (t o) es r -> Pull f o es r

  Emits the smallest output encountered.

Totality: total
Visibility: export

mappend : Foldable t => Chunk (t o) o => Semigroup o => Pull f (t o) es r -> Pull f o es r

  Emits the smallest output encountered.

Totality: total
Visibility: export

foldMap : Foldable t => Monoid m => (o -> m) -> Pull f (t 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

interface Scan : (Type -> Type) -> Type

Parameters: f
Constraints: Functor f
Methods:

scanChunk : (s -> o -> (p, s)) -> s -> f o -> (f p, s)

Implementation:

Scan List

scanChunk : Scan f => (s -> o -> (p, s)) -> s -> f o -> (f p, s)

Totality: total
Visibility: public export

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

  Computes a stateful running total over all elements emitted by a
  pull.

Totality: total
Visibility: export

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

  Zips the input with a running total according to `s`, up to but
  not including the current element. Thus the initial
  `vp` value is the first emitted to the output:

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

runningCount : Scan t => Pull f (t o) es r -> Pull f (t Nat) es r

  Emits the count of each element.

Totality: total
Visibility: export

data ZipRes : Type -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

ZB : List c -> ZipRes a b c
ZL : List a -> List c -> ZipRes a b c
ZR : List b -> List c -> ZipRes a b c

zipAllWith : o1 -> o2 -> (o1 -> o2 -> o3) -> Stream f es (List o1) -> Stream f es (List o2) -> Stream f es (List 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 (List o1) -> Stream f es (List o2) -> Stream f es (List (o1, o2))

  `zipAllWith` specialized to returning a pair of values

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

  `zipAll` specialized to returning a pair of values

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

zipRight : Stream f es (List o1) -> Stream f es (List o2) -> Stream f es (List o2)

Totality: total
Visibility: export

zipLeft : Stream f es (List o1) -> Stream f es (List o2) -> Stream f es (List o1)

Totality: total
Visibility: export