Data.Buffer.Indexed

Reexports

Definitions

ix : IBuffer n -> (0 m : Nat) -> Ix (S m) n => Bits8

  Safely access a value in an immutable byte array at position `n - m`.

Totality: total
Visibility: export

atNat : IBuffer n -> (m : Nat) -> {auto 0 _ : LT m n} -> Bits8

  Safely access a value in an immutable byte array at the given position.

Totality: total
Visibility: export

atByte : IBuffer 256 -> Bits8 -> Bits8

  Safely access a value at the given byte position.

Totality: total
Visibility: export

empty : IBuffer 0

  The empty byte array.

Totality: total
Visibility: export

bufferL : (ls : List Bits8) -> IBuffer (length ls)

  Copy the values in a list to an immutable byte array of the same length.

Totality: total
Visibility: export

buffer : Vect n Bits8 -> IBuffer n

  Copy the values in a vector to an immutable byte array of the same length.

Totality: total
Visibility: export

revBuffer : Vect n Bits8 -> IBuffer n

  Copy the values in a vector to an immutable byte array of the same length
  in reverse order.
  
  This is useful the values in the byte array have been collected
  from tail to head for instance when parsing some data.

Totality: total
Visibility: export

generate : (n : Nat) -> (Fin n -> Bits8) -> IBuffer n

  Generate an immutable byte array of the given size using
  the given iteration function.

Totality: total
Visibility: export

fill : (n : Nat) -> Bits8 -> IBuffer n

  Fill an immutable byte array of the given size with the given value.

Totality: total
Visibility: export

iterate : (n : Nat) -> (Bits8 -> Bits8) -> Bits8 -> IBuffer n

  Generate an immutable byte array of the given size by filling it with the
  results of repeatedly applying `f` to the initial value.

Totality: total
Visibility: export

force : IBuffer n -> IBuffer n

  Copy the content of an immutable byte array to a new immutable byte array.
  
  This is mainly useful for reducing memory consumption, in case the
  original array is actually backed by a much larger array, for
  instance after taking a smaller prefix of a large array with `take`.

Totality: total
Visibility: export

hcomp : IBuffer m -> IBuffer n -> Ordering

  Lexicographic comparison of immutable byte arrays of distinct length.

Totality: total
Visibility: export

heq : IBuffer m -> IBuffer n -> Bool

  Heterogeneous equality for immutable byte arrays.

Totality: total
Visibility: export

toVect : IBuffer n -> Vect n Bits8

  Convert an immutable byte array to a vector of the same length.

Totality: total
Visibility: export

toVectWithIndex : IBuffer n -> Vect n (Fin n, Bits8)

  Convert an immutable byte array to a vector of the same length
  pairing all values with their index.

Totality: total
Visibility: export

foldr : (Bits8 -> a -> a) -> a -> IBuffer n -> a

  Right fold over the values of an immutable byte array plus their indices.

Totality: total
Visibility: export

toList : IBuffer n -> List Bits8

Totality: total
Visibility: export

foldrKV : (Fin n -> Bits8 -> a -> a) -> a -> IBuffer n -> a

  Right fold over the values of an immutable  byte array plus their indices.

Totality: total
Visibility: export

foldl : (a -> Bits8 -> a) -> a -> IBuffer n -> a

  Left fold over the values of an immutable byte array.

Totality: total
Visibility: export

toSnocList : IBuffer n -> SnocList Bits8

Totality: total
Visibility: export

foldlKV : (Fin n -> a -> Bits8 -> a) -> a -> IBuffer n -> a

  Left fold over the values of an immutable byte array plus their indices.

Totality: total
Visibility: export

mapWithIndex : (Fin n -> Bits8 -> Bits8) -> IBuffer n -> IBuffer n

  Mapping over the values of an immutable byte array together with their indices.

Totality: total
Visibility: export

map : (Bits8 -> Bits8) -> IBuffer n -> IBuffer n

  Mapping over the values of an immutable byte array together with their indices.

Totality: total
Visibility: export

updateAt : Fin n -> (Bits8 -> Bits8) -> IBuffer n -> IBuffer n

  Update a single position in an immutable array by applying the given
  function.
  
  This will have to copy the whole array, so it runs in O(n).

Totality: total
Visibility: export

setAt : Fin n -> Bits8 -> IBuffer n -> IBuffer n

  Set a single position in an immutable byte array.
  
  This will have to copy the whole array, so it runs in O(n).

Totality: total
Visibility: export

traverseWithIndex : Applicative f => (Fin n -> Bits8 -> f Bits8) -> IBuffer n -> f (IBuffer n)

  Effectful traversal of the values in an immutable byte array together with
  their corresponding indices.

Totality: total
Visibility: export

traverse : Applicative f => (Bits8 -> f Bits8) -> IBuffer n -> f (IBuffer n)

Totality: total
Visibility: export

append : IBuffer m -> IBuffer n -> IBuffer (m + n)

  Concatenate two immutable byte arrays.

Totality: total
Visibility: export

drop : (m : Nat) -> IBuffer n -> IBuffer (minus n m)

  Drop n elements from a immutable byte array. O(n)

Totality: total
Visibility: export

pack : List Bits8 -> AnyBuffer

Totality: total
Visibility: export

unpack : AnyBuffer -> List Bits8

Totality: total
Visibility: export