Data.Array.Mutable

Reexports

Definitions

setAtSuffix : MArray s (length ys) a -> Suffix (x :: xs) ys -> a -> F1' s

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

Totality: total
Visibility: export

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

  Set a value at index `n - m` in a mutable 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 : MArray s n a -> (m : Nat) -> {auto 0 _ : LT m n} -> a -> F1' s

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

Totality: total
Visibility: export

getIx : MArray s n a -> (0 m : Nat) -> Ix (S m) n => F1 s a

  Read a value at index `n - m` from a mutable 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 : MArray s n a -> (m : Nat) -> {auto 0 _ : LT m n} -> F1 s a

  Read a value at index `m` from a mutable array.

Totality: total
Visibility: export

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

  Modify a value at index `n - m` in a mutable 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 : MArray s n a -> (m : Nat) -> {auto 0 _ : LT m n} -> (a -> a) -> F1' s

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

Totality: total
Visibility: export

writeList : MArray s (length xs) a -> (ys : List a) -> Suffix ys xs => F1' s

  Writes the data from a list to a mutable array.
  
  This uses the `Suffix` proof for safely indexing into the array.

Totality: total
Visibility: export

writeListWith : MArray s (length xs) b -> (ys : List a) -> (a -> b) -> Suffix ys xs => F1' s

  Writes the data from a list to a mutable array.
  
  This uses the `Suffix` proof for safely indexing into the array.

Totality: total
Visibility: export

writeVect : MArray s n a -> Vect k a -> Ix k n => F1' s

  Writes the data from a vector to a mutable array.

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

iterateFrom : MArray s n a -> (m : Nat) -> Ix m n => (a -> a) -> a -> F1' s

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

Totality: total
Visibility: export

allocList : (xs : List a) -> WithMArray (length xs) a b -> b

Totality: total
Visibility: export

allocListWith : (xs : List a) -> (a -> b) -> WithMArray (length xs) b c -> c

Totality: total
Visibility: export

allocVect : Vect n a -> WithMArray n a b -> b

Totality: total
Visibility: export

allocVectRev : Vect n a -> WithMArray n a b -> b

Totality: total
Visibility: export

allocGen : (n : Nat) -> (Fin n -> a) -> WithMArray n a b -> b

Totality: total
Visibility: export

allocIter : (n : Nat) -> (a -> a) -> a -> WithMArray n a b -> b

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

mappend : MArray s m a -> MArray s n a -> F1 s (MArray s (m + n) a)

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

Totality: total
Visibility: export

mfilterWithKey : MArray s n a -> (Fin n -> a -> Bool) -> F1 s (m : Nat ** MArray s m a)

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

Totality: total
Visibility: export

mfilter : MArray s n a -> (a -> Bool) -> F1 s (m : Nat ** MArray s m a)

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

Totality: total
Visibility: export

mmapMaybeWithKey : MArray s n a -> (Fin n -> a -> Maybe b) -> F1 s (m : Nat ** MArray s m b)

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

Totality: total
Visibility: export

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

  Drop `m` elements from a mutable array.

Totality: total
Visibility: export

mupdate1 : (a -> F1 s a) -> MArray s n a -> F1' s

  Apply an effectful function `f` to each element of the mutable array.
  
  Unlike `mmap1` and `mmap`, this function performs inplace mutation.

Totality: total
Visibility: export

mupdate : (a -> a) -> MArray s n a -> F1' s

  Apply a function `f` to each element of the mutable array.
  
  Unlike `mmap1` and `mmap`, this function performs inplace mutation.

Totality: total
Visibility: export

mmap1 : (a -> F1 s b) -> MArray s n a -> F1 s (MArray s n b)

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

Totality: total
Visibility: export

mmap : (a -> b) -> MArray s n a -> F1 s (MArray s n b)

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

Totality: total
Visibility: export

mreverse : MArray s k a -> F1 s (MArray s k a)

  Reverse the order of elements in a mutable array.

Totality: total
Visibility: export

foldrLin : MArray s k a -> (a -> b -> b) -> b -> F1 s b

  Accumulate the values stored in a mutable array.

Totality: total
Visibility: export

toVect : MArray s k a -> F1 s (Vect k a)

  Store the values in a mutable array in a `Vect` of the same size.

Totality: total
Visibility: export

toVectWith : MArray s k a -> (Fin k -> a -> b) -> F1 s (Vect k b)

  Extract and convert the values stored in a mutable array
  and store them in a `Vect` of the same size.

Totality: total
Visibility: export

0 Matrix1 : Type -> Nat -> Nat -> Type -> Type

  A linear, mutable `w*h` matrix holding values of type `a`.

Totality: total
Visibility: public export

newM1 : (w : Nat) -> (h : Nat) -> a -> F1 s (Matrix1 s w h a)

Totality: total
Visibility: export

writeM1 : Matrix1 s w h a -> Fin w -> Fin h -> a -> F1' s

Totality: total
Visibility: export

readM1 : Matrix1 s w h a -> Fin w -> Fin h -> F1 s a

Totality: total
Visibility: export