Idris2Doc : FS.Chunk

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)
escanChunk : (s -> o -> Either e (p, s)) -> s -> f o -> Either e (f p, s)

Implementation: 
Scan List
scanChunk : Scan f => (s -> o -> (p, s)) -> s -> f o -> (f p, s)
Totality: total
Visibility: public export
escanChunk : Scan f => (s -> o -> Either e (p, s)) -> s -> f o -> Either e (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
scanReturn : Scan t => s -> (s -> o -> (p, s)) -> Stream f es (t o) -> Pull f (t p) es s
  Like `scan` but returns the final state as the pull's result

Totality: total
Visibility: export
escanReturn : Scan t => s -> (s -> o -> Result es (p, s)) -> Stream f es (t o) -> Pull f (t p) es s
  Like `scan` but returns the final state as the pull's result

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