Data.Buffer.Mutable

Reexports

Definitions

setAtSuffix : MBuffer s (length ys) -> Suffix (x :: xs) ys -> Bits8 -> F1' s

  Set a value in a mutable byte array corresponding to a position in a list
  used for filling said array.

Totality: total
Visibility: export

setBits8 : MBuffer s 256 -> Bits8 -> Bits8 -> F1' s

  Safely access a value at the given byte position.

Totality: total
Visibility: export

getBits8 : MBuffer s 256 -> Bits8 -> F1 s Bits8

  Safely access a value at the given byte position.

Totality: total
Visibility: export

setIx : MBuffer s n -> (0 m : Nat) -> Ix (S m) n => Bits8 -> F1' s

  Set a value at index `n - m` in a mutable byte array.
  
  This actually uses the auto implicit argument for accessing the
  the array. It is mainly useful for iterating over an array from the left
  by using a natural number for counting down (see also the documentation
  for `Ix`).

Totality: total
Visibility: export

setNat : MBuffer s n -> (m : Nat) -> {auto 0 _ : LT m n} -> Bits8 -> F1' s

  Set a value at index `m` in a mutable byte array.

Totality: total
Visibility: export

getIx : MBuffer s n -> (0 m : Nat) -> Ix (S m) n => F1 s Bits8

  Read a value at index `n - m` from a mutable byte array.
  
  This actually uses the auto implicit argument for accessing the
  the array. It is mainly useful for iterating over an array from the left
  by using a natural number for counting down (see also the documentation
  for `Ix`).

Totality: total
Visibility: export

getNat : MBuffer s n -> (m : Nat) -> {auto 0 _ : LT m n} -> F1 s Bits8

  Read a value at index `m` from a mutable byte array.
  
  Since mutable arrays must be used in a linear context, and this
  function "uses up" its input as far as the linearity checker is
  concerned, this also returns a new `MBuffer` wrapper, which must then
  again be used exactly once.

Totality: total
Visibility: export

modifyIx : MBuffer s n -> (0 m : Nat) -> Ix (S m) n => (Bits8 -> Bits8) -> F1' s

  Modify a value at index `n - m` in a mutable byte array.
  
  This actually uses the auto implicit argument for accessing the
  the array. It is mainly useful for iterating over an array from the left
  by using a natural number for counting down (see also the documentation
  for `Ix`).

Totality: total
Visibility: export

modifyNat : MBuffer s n -> (m : Nat) -> {auto 0 _ : LT m n} -> (Bits8 -> Bits8) -> F1' s

  Modify a value at index `m` in a mutable byte array.

Totality: total
Visibility: export

writeList : MBuffer s (length xs) -> (ys : List Bits8) -> Suffix ys xs => F1' s

  Writes the data from a list to a mutable byte array.

Totality: total
Visibility: export

writeVect : MBuffer s n -> Vect k Bits8 -> Ix k n => F1' s

  Writes the data from a vector to a mutable byte array.

Totality: total
Visibility: export

writeVectRev : MBuffer s n -> (m : Nat) -> Vect k Bits8 -> {auto 0 _ : LTE m n} -> F1' s

  Writes the data from a vector to a mutable byte array in reverse order.

Totality: total
Visibility: export

genFrom : MBuffer s n -> (m : Nat) -> {auto 0 _ : LTE m n} -> (Fin n -> Bits8) -> F1' s

  Overwrite the values in a mutable byte array from the
  given index downward with the result of the given function.

Totality: total
Visibility: export

genFrom' : MBuffer s n -> (m : Nat) -> {auto 0 _ : LTE m n} -> (Fin n -> F1 s Bits8) -> F1' s

  Overwrite the values in a mutable buffer from the
  given index downward with the result of the given function.

Totality: total
Visibility: export

iterateFrom : MBuffer s n -> (m : Nat) -> Ix m n => (Bits8 -> Bits8) -> Bits8 -> F1' s

  Overwrite the values in a mutable byte array from the
  given index upward with the results of applying the given
  function repeatedly.

Totality: total
Visibility: export

mgrow : MBuffer s n -> (m : Nat) -> F1 s (MBuffer s (m + n))

  Allocates a new mutable byte array and adds the elements from `r`
  at its beginning.

Totality: total
Visibility: export

mappend : MBuffer s m -> MBuffer s n -> F1 s (MBuffer s (m + n))

  Allocates a new mutable byte array and adds the elements from `p`
  at its beginning, followed by adding the elements from `q`.

Totality: total
Visibility: export

mfilter : (Bits8 -> Bool) -> MBuffer s n -> F1 s (m : Nat ** MBuffer s m)

  Filters the values in a mutable byte array according to the given predicate.

Totality: total
Visibility: export

mdrop : (m : Nat) -> MBuffer s n -> F1 s (MBuffer s (minus n m))

  Drop `m` elements from a mutable byte array.

Totality: total
Visibility: export

mmap1 : (Bits8 -> F1 s Bits8) -> MBuffer s n -> F1 s (MBuffer s n)

  Apply a function `f` to each element of the mutable buffer.

Totality: total
Visibility: export

mmap : (Bits8 -> Bits8) -> MBuffer s n -> F1 s (MBuffer s n)

  Apply a function `f` to each element of the mutable buffer.

Totality: total
Visibility: export

mreverse : MBuffer s n -> F1 s (MBuffer s n)

  Reverse the order of elements in a mutable buffer.

Totality: total
Visibility: export