Idris2Doc : Data.NumIdr.Array.Array

Data.NumIdr.Array.Array

(source)
Definitions
data Array : Vect rk Nat -> Type -> Type
  The type of an array.
  
  Arrays are the central data structure of NumIdr. They are an `n`-dimensional
  grid of values, where `n` is a value known as the *rank* of the array. Arrays
  of rank 0 are single values, arrays of rank 1 are vectors, and arrays of rank
  2 are matrices.
  
  Each array has a *shape*, which is a vector of values giving the dimensions
  of each axis of the array. The shape is also sometimes used to determine the
  array's total size.
  
  Arrays are indexed by row first, as in the standard mathematical notation for
  matrices.
  
  @ rk The rank of the array
  @ s The shape of the array
  @ a The type of the array's elements

  Totality: total
  Visibility: export
  Constructor: 
MkArray : (rep : Rep) -> {auto rc : RepConstraint rep a} -> (s : Vect rk Nat) -> PrimArray rep s a -> Array s a
  Internally, arrays are stored via one of a handful of representations.
  
  @ s   The shape of the array
  @ rep The internal representation of the array
  @ rc  A witness that the element type satisfies the representation constraint

  Hints:
  
Applicative (Array s)
  
Cast a b => Cast (Array s a) (Array s b)
  
Eq a => Eq (Array s a)
  
Foldable (Array s)
  
Fractional a => Fractional (Array s a)
  
Functor (Array s)
  
Monad (Array s)
  
Monoid a => Monoid (Array s a)
  
Num a => Mult a (Array s a) (Array s a)
  
Num a => Mult (Array s a) a (Array s a)
  
Neg a => Neg (Array s a)
  
Num a => Num (Array s a)
  
Semigroup a => Semigroup (Array s a)
  
Show a => Show (Array s a)
  
Traversable (Array s)
  
Zippable (Array s)
unsafeMkArray : (rep : Rep) -> {auto rc : RepConstraint rep a} -> (s : Vect rk Nat) -> PrimArray rep s a -> Array s a
  Totality: total
  Visibility: export
shape : Array s a -> Vect rk Nat
  The shape of the array.

  Totality: total
  Visibility: export
size : Array s a -> Nat
  The size of the array, i.e. the total number of elements.

  Totality: total
  Visibility: export
rank : Array s a -> Nat
  The rank of the array.

  Totality: total
  Visibility: export
getRep : Array s a -> Rep
  The internal representation of the array.

  Totality: total
  Visibility: export
getRepC : (arr : Array s a) -> RepConstraint (getRep arr) a
  The representation constraint of the array.

  Totality: total
  Visibility: export
getPrim : (arr : Array s a) -> PrimArray (getRep arr) s a
  Extract the primitive backend array.

  Totality: total
  Visibility: export
shapeEq : (arr : Array s a) -> s = shape arr
  Totality: total
  Visibility: export
data ShapeView : Array s a -> Type
  A view for extracting the shape of an array.

  Totality: total
  Visibility: public export
  Constructor: 
Shape : (s : Vect rk Nat) -> ShapeView arr
viewShape : (arr : Array s a) -> ShapeView arr
  The covering function for the view `ShapeView`. This function takes an array
  of type `Array s a` and returns `Shape s`.

  Totality: total
  Visibility: export
repeat : {default B rep : Rep} -> RepConstraint rep a => (s : Vect rk Nat) -> a -> Array s a
  Create an array by repeating a single value.
  
  @ s    The shape of the constructed array
  @ rep  The internal representation of the constructed array

  Totality: total
  Visibility: export
zeros : {default B rep : Rep} -> RepConstraint rep a => Num a => (s : Vect rk Nat) -> Array s a
  Create an array filled with zeros.
  
  @ s The shape of the constructed array
  @ rep  The internal representation of the constructed array

  Totality: total
  Visibility: export
ones : {default B rep : Rep} -> RepConstraint rep a => Num a => (s : Vect rk Nat) -> Array s a
  Create an array filled with ones.
  
  @ s The shape of the constructed array
  @ rep  The internal representation of the constructed array

  Totality: total
  Visibility: export
fromVect : {default B rep : Rep} -> LinearRep rep => RepConstraint rep a => (s : Vect rk Nat) -> Vect (product s) a -> Array s a
  Create an array given a vector of its elements. The elements of the vector
  are arranged into the provided shape using the provided order.
  
  @ s   The shape of the constructed array
  @ rep  The internal representation of the constructed array

  Totality: total
  Visibility: export
fromStream : {default B rep : Rep} -> LinearRep rep => RepConstraint rep a => (s : Vect rk Nat) -> Stream a -> Array s a
  Create an array by taking values from a stream.
  
  @ s   The shape of the constructed array
  @ rep  The internal representation of the constructed array

  Totality: total
  Visibility: export
fromFunctionNB : {default B rep : Rep} -> RepConstraint rep a => (s : Vect rk Nat) -> (Vect rk Nat -> a) -> Array s a
  Create an array given a function to generate its elements.
  
  @ s   The shape of the constructed array
  @ rep  The internal representation of the constructed array

  Totality: total
  Visibility: export
fromFunction : {default B rep : Rep} -> RepConstraint rep a => (s : Vect rk Nat) -> (Coords s -> a) -> Array s a
  Create an array given a function to generate its elements.
  
  @ s   The shape of the constructed array
  @ rep  The internal representation of the constructed array

  Totality: total
  Visibility: export
array : {default B rep : Rep} -> RepConstraint rep a => Vects s a -> Array s a
  Construct an array using a structure of nested vectors.
  To explicitly specify the shape and order of the array, use `array'`.

  Totality: total
  Visibility: export
index : Coords s -> Array s a -> a
  Index the array using the given coordinates.

  Totality: total
  Visibility: export
(!!) : Array s a -> Coords s -> a
  Index the array using the given coordinates.
  
  This is the operator form of `index`.

  Totality: total
  Visibility: export
  Fixity Declarations:
  infixl operator, level 10
infixl operator, level 10
infixl operator, level 10
indexUpdate : Coords s -> (a -> a) -> Array s a -> Array s a
  Update the entry at the given coordinates using the function.

  Totality: total
  Visibility: export
indexSet : Coords s -> a -> Array s a -> Array s a
  Set the entry at the given coordinates to the given value.

  Totality: total
  Visibility: export
indexRange : (rs : CoordsRange s) -> Array s a -> Array (newShape rs) a
  Index the array using the given range of coordinates, returning a new array.

  Totality: total
  Visibility: export
(!!..) : Array s a -> (rs : CoordsRange s) -> Array (newShape rs) a
  Index the array using the given range of coordinates, returning a new array.
  
  This is the operator form of `indexRange`.

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 11
indexSetRange : (rs : CoordsRange s) -> Array (newShape rs) a -> Array s a -> Array s a
  Set the sub-array at the given range of coordinates to the given array.

  Totality: total
  Visibility: export
indexUpdateRange : (rs : CoordsRange s) -> (Array (newShape rs) a -> Array (newShape rs) a) -> Array s a -> Array s a
  Update the sub-array at the given range of coordinates by applying
  a function to it.

  Totality: total
  Visibility: export
indexNB : Vect rk Nat -> Array s a -> Maybe a
  Index the array using the given coordinates, returning `Nothing` if the
  coordinates are out of bounds.

  Totality: total
  Visibility: export
(!?) : Array s a -> Vect rk Nat -> Maybe a
  Index the array using the given coordinates, returning `Nothing` if the
  coordinates are out of bounds.
  
  This is the operator form of `indexNB`.

  Totality: total
  Visibility: export
  Fixity Declarations:
  infixl operator, level 10
infixl operator, level 10
infixl operator, level 10
indexUpdateNB : Vect rk Nat -> (a -> a) -> Array s a -> Maybe (Array s a)
  Update the entry at the given coordinates using the function. `Nothing` is
  returned if the coordinates are out of bounds.

  Totality: total
  Visibility: export
indexSetNB : Vect rk Nat -> a -> Array s a -> Maybe (Array s a)
  Set the entry at the given coordinates using the function. `Nothing` is
  returned if the coordinates are out of bounds.

  Totality: total
  Visibility: export
indexRangeNB : (rs : Vect rk CRangeNB) -> Array s a -> Maybe (Array (newShape s rs) a)
  Index the array using the given range of coordinates, returning a new array.
  If any of the given indices are out of bounds, then `Nothing` is returned.

  Totality: total
  Visibility: export
(!?..) : Array s a -> (rs : Vect rk CRangeNB) -> Maybe (Array (newShape s rs) a)
  Index the array using the given range of coordinates, returning a new array.
  If any of the given indices are out of bounds, then `Nothing` is returned.
  
  This is the operator form of `indexRangeNB`.

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 11
indexUnsafe : Vect rk Nat -> Array s a -> a
  Index the array using the given coordinates.
  WARNING: This function does not perform any bounds check on its inputs.
  Misuse of this function can easily break memory safety.

  Totality: total
  Visibility: export
(!#) : Array s a -> Vect rk Nat -> a
  Index the array using the given coordinates.
  WARNING: This function does not perform any bounds check on its inputs.
  Misuse of this function can easily break memory safety.
  
  This is the operator form of `indexUnsafe`.

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 10
indexRangeUnsafe : (rs : Vect rk CRangeNB) -> Array s a -> Array (newShape s rs) a
  Index the array using the given range of coordinates, returning a new array.
  WARNING: This function does not perform any bounds check on its inputs.
  Misuse of this function can easily break memory safety.

  Totality: total
  Visibility: export
(!#..) : Array s a -> (rs : Vect rk CRangeNB) -> Array (newShape s rs) a
  Index the array using the given range of coordinates, returning a new array.
  WARNING: This function does not perform any bounds check on its inputs.
  Misuse of this function can easily break memory safety.
  
  This is the operator form of `indexRangeUnsafe`.

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 11
mapArray' : (a -> a) -> Array s a -> Array s a
  Map a function over an array.
  
  You should almost always use `map` instead; only use this function if you
  know what you are doing!

  Totality: total
  Visibility: export
mapArray : (a -> b) -> (arr : Array s a) -> RepConstraint (getRep arr) b => Array s b
  Map a function over an array.
  
  You should almost always use `map` instead; only use this function if you
  know what you are doing!

  Totality: total
  Visibility: export
zipWithArray' : (a -> a -> a) -> Array s a -> Array s a -> Array s a
  Combine two arrays of the same element type using a binary function.
  
  You should almost always use `zipWith` instead; only use this function if
  you know what you are doing!

  Totality: total
  Visibility: export
zipWithArray : (a -> b -> c) -> (arr : Array s a) -> (arr' : Array s b) -> RepConstraint (mergeRep (getRep arr) (getRep arr')) c => Array s c
  Combine two arrays using a binary function.
  
  You should almost always use `zipWith` instead; only use this function if
  you know what you are doing!

  Totality: total
  Visibility: export
reshape : (s' : Vect rk' Nat) -> (arr : Array s a) -> LinearRep (getRep arr) => {auto 0 _ : product s = product s'} -> Array s' a
  Reshape the array into the given shape.
  
  @ s' The shape to convert the array to

  Totality: total
  Visibility: export
convertRep : (rep : Rep) -> RepConstraint rep a => Array s a -> Array s a
  Change the internal representation of the array's elements.

  Totality: total
  Visibility: export
delayed : (Array s a -> Array s' a) -> Array s a -> Array s' a
  Temporarily convert an array to a delayed representation to make modifying
  it more efficient, then convert it back to its original representation.

  Totality: total
  Visibility: export
resize : (s' : Vect rk Nat) -> a -> Array s a -> Array s' a
  Resize the array to a new shape, preserving the coordinates of the original
  elements. New coordinates are filled with a default value.
  
  @ s'  The shape to resize the array to
  @ def The default value to fill the array with

  Totality: total
  Visibility: export
resizeLTE : (s' : Vect rk Nat) -> {auto 0 _ : All id (zipWith LTE s' s)} -> Array s a -> Array s' a
  Resize the array to a new shape, preserving the coordinates of the original
  elements. This function requires a proof that the new shape is strictly
  smaller than the current shape of the array.
  
  @ s' The shape to resize the array to

  Totality: total
  Visibility: export
enumerateNB : Array s a -> List (Vect rk Nat, a)
  List all of the values in an array along with their coordinates.

  Totality: total
  Visibility: export
enumerate : Array s a -> List (Coords s, a)
  List all of the values in an array along with their coordinates.

  Totality: total
  Visibility: export
elements : Array s a -> Vect (product s) a
  List all of the values in an array in row-major order.

  Totality: total
  Visibility: export
concat : (axis : Fin rk) -> Array s a -> Array (replaceAt axis d s) a -> Array (updateAt axis (\{arg:0} => {arg:0} + d) s) a
  Join two arrays along a particular axis, e.g. combining two matrices
  vertically or horizontally. All other axes of the arrays must have the
  same dimensions.
  
  @ axis The axis to join the arrays on

  Totality: total
  Visibility: export
stack : (axis : Fin (S rk)) -> Vect n (Array s a) -> Array (insertAt axis n s) a
  Stack multiple arrays along a new axis, e.g. stacking vectors to form a matrix.
  
  @ axis The axis to stack the arrays along

  Totality: total
  Visibility: export
joinAxes : Array s (Array s' a) -> Array (s ++ s') a
  Join the axes of a nested array structure to form a single array.

  Totality: total
  Visibility: export
splitAxes : (rk : Nat) -> Array s a -> Array (take rk s) (Array (drop rk s) a)
  Split an array into a nested array structure along the specified axes.

  Totality: total
  Visibility: export
transpose : Array s a -> Array (reverse s) a
  Construct the transpose of an array by reversing the order of its axes.

  Totality: total
  Visibility: export
.T : Array s a -> Array (reverse s) a
  Construct the transpose of an array by reversing the order of its axes.
  
  This is the postfix form of `transpose`.

  Totality: total
  Visibility: export
swapAxes : (i : Fin rk) -> (j : Fin rk) -> Array s a -> Array (swapElems i j s) a
  Swap two axes in an array.

  Totality: total
  Visibility: export
permuteAxes : (p : Permutation rk) -> Array s a -> Array (permuteVect p s) a
  Apply a permutation to the axes of an array.

  Totality: total
  Visibility: export
swapInAxis : (axis : Fin rk) -> Fin (index axis s) -> Fin (index axis s) -> Array s a -> Array s a
  Swap two coordinates along a specific axis (e.g. swapping two rows in a matrix).
  
  @ axis The axis to swap the coordinates along. Slices of the array
  perpendicular to this axis are taken when swapping.

  Totality: total
  Visibility: export
permuteInAxis : (axis : Fin rk) -> Permutation (index axis s) -> Array s a -> Array s a
  Permute the coordinates along a specific axis (e.g. permuting the rows in
  a matrix).
  
  @ axis The axis to permute the coordinates along. Slices of the array
  perpendicular to this axis are taken when permuting.

  Totality: total
  Visibility: export
lerp : Neg a => a -> Array s a -> Array s a -> Array s a
  Linearly interpolate between two arrays.

  Totality: total
  Visibility: export
normSq : Num a => Array s a -> a
  Calculate the square of an array's Eulidean norm.

  Totality: total
  Visibility: export
norm : Array s Double -> Double
  Calculate an array's Eucliean norm.

  Totality: total
  Visibility: export
normalize : Array s Double -> Array s Double
  Normalize the array to a norm of 1.
  
  If the array contains all zeros, then it is returned unchanged.

  Totality: total
  Visibility: export
pnorm : Double -> Array s Double -> Double
  Calculate the Lp-norm of an array.

  Totality: total
  Visibility: export