Data.NumIdr.Array.Rep

Definitions

data Order : Type

  An order is an abstract representation of the way in which contiguous array
  elements are stored in memory. Orders are used to calculate strides, which
  provide a method of converting an array coordinate into a linear memory
  location.

Totality: total
Visibility: public export
Constructors:

COrder : Order

  C-like order, or contiguous order. This order stores elements in a
  row-major fashion (the last axis is the least significant).

FOrder : Order

  Fortran-like order. This order stores elements in a column-major
  fashion (the first axis is the least significant).

Hint: 

Eq Order

calcStrides : Order -> Vect rk Nat -> Vect rk Nat

  Calculate an array's strides given its order and shape.

Totality: total
Visibility: export

data Rep : Type

  An internal representation of an array.
  
  Each array internally stores its values based on one of these
  representations.

Totality: total
Visibility: public export
Constructors:

Bytes : Order -> Rep

  Byte-buffer array representation.
  
  This representations stores elements by converting them into byte values
  storing them in a `Buffer`. Use of this representation is only valid if
  the element type implements `ByteRep`.
  
  @ o The order to store array elements in

Boxed : Order -> Rep

  Boxed array representation.
  
  This representation uses a boxed array type to store its elements.
  
  @ o The order to store array elements in

Linked : Rep

  Linked list array representation.
  
  This representation uses Idris's standard linked list types to store its
  elements.

Delayed : Rep

  Delayed/Lazy array representation.
  
  This representation delays the computation of the array's elements, which
  may be useful in writing efficient algorithms.

Hint: 

Eq Rep

B : Rep

  An alias for the representation `Boxed COrder`, the C-like boxed array
  representation.
  
  This representation is the default for all newly created arrays.

Totality: total
Visibility: public export

L : Rep

  An alias for the representation `Linked COrder`.

Totality: total
Visibility: public export

D : Rep

  An alias for the representation `Delayed`.

Totality: total
Visibility: public export

data LinearRep : Rep -> Type

  A predicate on representations for those that store their elements
  linearly.

Totality: total
Visibility: public export
Constructors:

BytesIsL : LinearRep (Bytes o)

BoxedIsL : LinearRep (Boxed o)

forceRepNC : Rep -> Rep

Totality: total
Visibility: public export

mergeRep : Rep -> Rep -> Rep

Totality: total
Visibility: public export

mergeRepNC : Rep -> Rep -> Rep

Totality: total
Visibility: public export

data NoConstraintRep : Rep -> Type

Totality: total
Visibility: public export
Constructors:

BoxedNC : NoConstraintRep (Boxed o)

LinkedNC : NoConstraintRep Linked

DelayedNC : NoConstraintRep Delayed

mergeRepNCCorrect : (r : Rep) -> (r' : Rep) -> NoConstraintRep (mergeRepNC r r')

Totality: total
Visibility: public export

forceRepNCCorrect : (r : Rep) -> NoConstraintRep (forceRepNC r)

Totality: total
Visibility: public export

interface ByteRep : Type -> Type

  An interface for elements that can be converted into raw bytes.
  
  An implementation of this interface is required to use the `Bytes` array
  representation.

Parameters: a
Methods:

bytes : Nat

  The number of bytes used to store each value.

toBytes : a -> Vect bytes Bits8

  Convert a value into a list of bytes.

fromBytes : Vect bytes Bits8 -> a

  Convert a list of bytes into a value.

Implementations:

ByteRep Bits8

ByteRep Bits16

ByteRep Bits32

ByteRep Bits64

ByteRep Int

ByteRep Int8

ByteRep Int16

ByteRep Int32

ByteRep Int64

ByteRep Bool

ByteRep a => ByteRep b => ByteRep (a, b)

ByteRep a => ByteRep (Vect n a)

bytes : ByteRep a => Nat

  The number of bytes used to store each value.

Totality: total
Visibility: public export

toBytes : {auto __con : ByteRep a} -> a -> Vect bytes Bits8

  Convert a value into a list of bytes.

Totality: total
Visibility: public export

fromBytes : {auto __con : ByteRep a} -> Vect bytes Bits8 -> a

  Convert a list of bytes into a value.

Totality: total
Visibility: public export

RepConstraint : Rep -> Type -> Type

  The constraint that each array representation requires.
  
  Currently, only the `Bytes` representation has a constraint, requiring an
  implementation of `ByteRep`. All other representations can be used without
  constraint.

Totality: total
Visibility: public export