Idris2Doc : Data.Array.Indexed

Data.Array.Indexed

(source)
Definitions
record Array : Type -> Type
  An immutable array paired with its size (= number of values).
  
  This is the dependent pair version of `IArray size a`.

  Totality: total
  Visibility: public export
  Constructor: 
A : (size : Nat) -> IArray size a -> Array a

  Projections:
  
.arr : ({rec:0} : Array a) -> IArray (size {rec:0}) a
  
.size : Array a -> Nat

  Hints:
  
Foldable1 Array
  
Traversable1 Array
.size : Array a -> Nat
  Totality: total
  Visibility: public export
size : Array a -> Nat
  Totality: total
  Visibility: public export
.arr : ({rec:0} : Array a) -> IArray (size {rec:0}) a
  Totality: total
  Visibility: public export
arr : ({rec:0} : Array a) -> IArray (size {rec:0}) a
  Totality: total
  Visibility: public export
ix : IArray n a -> (0 m : Nat) -> Ix (S m) n => a
  Safely access a value in an immutable array at position `n - m`.

  Totality: total
  Visibility: export
atNat : IArray n a -> (m : Nat) -> {auto 0 _ : LT m n} -> a
  Safely access a value in an array at the given position.

  Totality: total
  Visibility: export
empty : IArray 0 a
  The empty array.

  Totality: total
  Visibility: export
arrayL : (ls : List a) -> IArray (length ls) a
  Copy the values in a list to an immutable array of the same length.

  Totality: total
  Visibility: export
array : Vect n a -> IArray n a
  Copy the values in a vector to an immutable array of the same length.

  Totality: total
  Visibility: export
revArray : Vect n a -> IArray n a
  Copy the values in a vector to an immutable array of the same length
  in reverse order.
  
  This is useful if the values in the array have been collected
  from tail to head for instance when parsing some data.

  Totality: total
  Visibility: export
fill : (n : Nat) -> a -> IArray n a
  Fill an immutable array of the given size with the given value.

  Totality: total
  Visibility: export
generate : (n : Nat) -> (Fin n -> a) -> IArray n a
  Generate an immutable array of the given size using
  the given iteration function.

  Totality: total
  Visibility: export
iterate : (n : Nat) -> (a -> a) -> a -> IArray n a
  Generate an immutable array of the given size by filling it with the
  results of repeatedly applying `f` to the initial value.

  Totality: total
  Visibility: export
force : IArray n a -> IArray n a
  Copy the content of an array to a new immutable 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
fromPairs : (n : Nat) -> a -> List (Nat, a) -> IArray n a
  Allocate an immutable array, fill it with the given default value, and use a list
  of pairs to replace specific positions.

  Totality: total
  Visibility: export
fromFinPairs : (n : Nat) -> a -> List (Fin n, a) -> IArray n a
  Like `fromPairs` but with `Fin n` as indices.

  Totality: total
  Visibility: export
unsafeJSArrayOf1 : (0 a : Type) -> AnyPtr -> F1 s (Array a)
  Wraps a pointer to a mutable JS array in an immutable array
  by copying the values first.
  
  Use this for wrapping arrays that can still be mutated in JS land, or if
  you are uncertain about whether the pointer points to a mutable array or
  not. The array will first be copied before being wrapped in an `Array a`.

  Totality: total
  Visibility: export
unsafeJSArrayOf : HasIO io => (0 a : Type) -> AnyPtr -> io (Array a)
  Like `unsafeJSArrayOf1` but runs in an `IO` monad.

  Totality: total
  Visibility: export
unsafeWrapJSArray : (0 a : Type) -> AnyPtr -> Array a
  Like `unsafeJSArrayOf1` but wraps the pointer without copying
  it first.
  
  Use this only if the pointer points to an array that cannot be
  inadvertently mutated later on.

  Totality: total
  Visibility: export
hcomp : Ord a => IArray m a -> IArray n a -> Ordering
  Lexicographic comparison of immutable arrays of distinct length.

  Totality: total
  Visibility: export
heq : Eq a => IArray m a -> IArray n a -> Bool
  Heterogeneous equality for immutable arrays.

  Totality: total
  Visibility: export
toVect : IArray n a -> Vect n a
  Convert an immutable array to a vector of the same length.

  Totality: total
  Visibility: export
toVectWithIndex : IArray n a -> Vect n (Fin n, a)
  Convert an immutable array to a vector of the same length
  pairing all values with their index.

  Totality: total
  Visibility: export
foldrKV : (Fin n -> e -> a -> a) -> a -> IArray n e -> a
  Right fold over the values of an immutable array plus their indices.

  Totality: total
  Visibility: export
foldlKV : (Fin n -> a -> e -> a) -> a -> IArray n e -> a
  Left fold over the values of an immutable array plus their indices.

  Totality: total
  Visibility: export
mapWithIndex : (Fin n -> a -> b) -> IArray n a -> IArray n b
  Mapping over the values of an immutable array together with their indices.

  Totality: total
  Visibility: export
updateAt : Fin n -> (a -> a) -> IArray n a -> IArray n a
  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 -> a -> IArray n a -> IArray n a
  Set a single position in an immutable array.
  
  This will have to copy the whole array, so it runs in O(n).

  Totality: total
  Visibility: export
traverseWithIndex : Applicative f => (Fin n -> a -> f b) -> IArray n a -> f (IArray n b)
  Effectful traversal of the values in an immutable array together with
  their corresponding indices.

  Totality: total
  Visibility: export
drop : (m : Nat) -> IArray n a -> IArray (minus n m) a
  Drop n elements from a immutable array. O(n)

  Totality: total
  Visibility: export
filterWithKey : (Fin n -> a -> Bool) -> IArray n a -> Array a
  Filter the values in an immutable array together with their corresponding
  indices according to the given predicate.

  Totality: total
  Visibility: export
filter : (a -> Bool) -> IArray n a -> Array a
  Filters the values in an immutable array according to the given predicate.

  Totality: total
  Visibility: export
mapMaybeWithKey : (Fin n -> a -> Maybe b) -> IArray n a -> Array b
  Map the values in an immutable array together with their corresponding indices
  over a function that might not return a result for all values.

  Totality: total
  Visibility: export
mapMaybe : (a -> Maybe b) -> IArray n a -> Array b
  Map the values in an immutable array together with their corresponding indices
  over a function that might not return a result for all values.

  Totality: total
  Visibility: export
SnocSize : SnocList (Array a) -> Nat
  Size of an array after concatenating a SnocList of arrays.
  
  It is easier to implement this and keep the indices correct,
  therefore, this is the default for concatenating arrays.

  Totality: total
  Visibility: public export
ListSize : List (Array a) -> Nat
  Size of an immutable array after concatenating a List of arrays.

  Totality: total
  Visibility: public export
snocConcat : (sa : SnocList (Array a)) -> IArray (SnocSize sa) a
  Concatenate a SnocList of arrays.
  
  This allocates a large enough array in advance, and therefore runs in
  O(SnocSize sa).

  Totality: total
  Visibility: export
listConcat : (as : List (Array a)) -> IArray (ListSize as) a
  Concatenate a List of arrays.
  
  This allocates a large enough array in advance, and therefore runs in
  O(ListSize as).

  Totality: total
  Visibility: export
append : IArray m a -> IArray n a -> IArray (m + n) a
  Concatenate two immutable arrays in O(m+n) runtime.

  Totality: total
  Visibility: export
traverseKV1_ : (Fin n -> a -> F1' q) -> IArray n a -> F1' q
  Runs a linear effect over the values plus their indices in an array.

  Totality: total
  Visibility: export