diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 8b55505..e9ec0d9 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -13,6 +13,8 @@ import Data.NumIdr.Array.Coords %default total +||| 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 @@ -23,22 +25,18 @@ import Data.NumIdr.Array.Coords ||| array's total size. ||| ||| Arrays are indexed by row first, as in the standard mathematical notation for -||| matrices. This is independent of the actual order in which they are stored; the -||| default order is row-major, but this is configurable. +||| matrices. ||| ||| @ rk The rank of the array ||| @ s The shape of the array ||| @ a The type of the array's elements export data Array : (s : Vect rk Nat) -> (a : Type) -> Type where - ||| Internally, arrays are stored using Idris's primitive array type. This is - ||| stored along with the array's shape, and a vector of values called the - ||| *strides*, which determine how indexes into the internal array should be - ||| performed. This is how the order of the array is configurable. + ||| Internally, arrays are stored via one of a handful of representations. ||| - ||| @ ord The order of the elements of the array - ||| @ sts The strides of the array ||| @ s The shape of the array + ||| @ rep The internal representation of the array + ||| @ rc A witness that the element type satisfies the representation constraint MkArray : (rep : Rep) -> (rc : RepConstraint rep a) => (s : Vect rk Nat) -> PrimArray rep s a @{rc} -> Array s a @@ -56,24 +54,27 @@ unsafeMkArray = MkArray -------------------------------------------------------------------------------- -||| The shape of the array +||| The shape of the array. export shape : Array {rk} s a -> Vect rk Nat shape (MkArray _ s _) = s -||| The rank of the array +||| The rank of the array. export rank : Array s a -> Nat rank = length . shape +||| The internal representation of the array. export getRep : Array s a -> Rep getRep (MkArray rep _ _) = rep +||| The representation constraint of the array. export getRepC : (arr : Array s a) -> RepConstraint (getRep arr) a getRepC (MkArray _ @{rc} _ _) = rc +||| Extract the primitive backend array. export getPrim : (arr : Array s a) -> PrimArray (getRep arr) s a @{getRepC arr} getPrim (MkArray _ _ pr) = pr @@ -340,14 +341,26 @@ arr !#.. is = indexRangeUnsafe is arr -- Operations on arrays -------------------------------------------------------------------------------- +||| Map a function over an array. +||| +||| You should almost always use `map` instead; only use this function if you +||| know what you are doing! export mapArray' : (a -> a) -> Array s a -> Array s a mapArray' f (MkArray rep _ arr) = MkArray rep _ (mapPrim f arr) +||| Map a function over an array. +||| +||| You should almost always use `map` instead; only use this function if you +||| know what you are doing! export mapArray : (a -> b) -> (arr : Array s a) -> RepConstraint (getRep arr) b => Array s b mapArray f (MkArray rep _ arr) @{rc} = MkArray rep @{rc} _ (mapPrim f arr) +||| 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! export zipWithArray' : (a -> a -> a) -> Array s a -> Array s a -> Array s a zipWithArray' {s} f a b with (viewShape a) @@ -356,6 +369,10 @@ zipWithArray' {s} f a b with (viewShape a) $ PrimArray.fromFunctionNB @{mergeRepConstraint (getRepC a) (getRepC b)} _ (\is => f (a !# is) (b !# is)) +||| 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! export zipWithArray : (a -> b -> c) -> (arr : Array s a) -> (arr' : Array s b) -> RepConstraint (mergeRep (getRep arr) (getRep arr')) c => Array s c @@ -446,6 +463,7 @@ stack axis arrs = rewrite sym (lengthCorrect arrs) in getAxisInd FZ (i :: is) = (i, is) getAxisInd {s=_::_} (FS ax) (i :: is) = mapSnd (i::) (getAxisInd ax is) +||| Join the axes of a nested array structure to form a single array. export joinAxes : {s' : _} -> Array s (Array s' a) -> Array (s ++ s') a joinAxes {s} arr with (viewShape arr) @@ -460,6 +478,7 @@ joinAxes {s} arr with (viewShape arr) dropUpTo (x::xs) (y::ys) = dropUpTo xs ys +||| Split an array into a nested array structure along the specified axes. export splitAxes : (rk : Nat) -> {0 rk' : Nat} -> {s : _} -> Array {rk=rk+rk'} s a -> Array (take {m=rk'} rk s) (Array (drop {m=rk'} rk s) a) @@ -577,7 +596,8 @@ export -- Foldable and Traversable operate on the primitive array directly. This means --- that their operation is dependent on the order of the array. +-- that their operation is dependent on the internal representation of the +-- array. export Foldable (Array s) where diff --git a/src/Data/NumIdr/Array/Rep.idr b/src/Data/NumIdr/Array/Rep.idr index 3410d13..c673c14 100644 --- a/src/Data/NumIdr/Array/Rep.idr +++ b/src/Data/NumIdr/Array/Rep.idr @@ -12,10 +12,10 @@ import Data.Buffer -------------------------------------------------------------------------------- -||| An order is an abstract representation of the way in which 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. +||| 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. public export data Order : Type where ||| C-like order, or contiguous order. This order stores elements in a @@ -49,24 +49,57 @@ calcStrides FOrder v@(_::_) = scanl (*) 1 $ init v -------------------------------------------------------------------------------- +||| An internal representation of an array. +||| +||| Each array internally stores its values based on one of these +||| representations. public export data Rep : Type where - Bytes : Order -> Rep - Boxed : 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 + Bytes : (o : Order) -> Rep + + ||| Boxed array representation. + ||| + ||| This representation uses a boxed array type to store its elements. + ||| + ||| @ o The order to store array elements in + Boxed : (o : Order) -> Rep + + ||| Linked list array representation. + ||| + ||| This representation uses Idris's standard linked list types to store its + ||| elements. Linked : Rep + + ||| Delayed/Lazy array representation. + ||| + ||| This representation delays the computation of the array's elements, which + ||| may be useful in writing efficient algorithms. Delayed : Rep %name Rep rep +||| An alias for the representation `Boxed COrder`, the C-like boxed array +||| representation. +||| +||| This representation is the default for all newly created arrays. public export B : Rep B = Boxed COrder +||| An alias for the representation `Linked COrder`. public export L : Rep L = Linked +||| An alias for the representation `Delayed`. public export D : Rep D = Delayed @@ -80,6 +113,8 @@ Eq Rep where Delayed == Delayed = True _ == _ = False +||| A predicate on representations for those that store their elements +||| linearly. public export data LinearRep : Rep -> Type where BytesIsL : LinearRep (Bytes o) @@ -140,11 +175,19 @@ forceRepNCCorrect Delayed = DelayedNC -------------------------------------------------------------------------------- +||| An interface for elements that can be converted into raw bytes. +||| +||| An implementation of this interface is required to use the `Bytes` array +||| representation. public export interface ByteRep a where + ||| The number of bytes used to store each value. bytes : Nat + ||| Convert a value into a list of bytes. toBytes : a -> Vect bytes Bits8 + + ||| Convert a list of bytes into a value. fromBytes : Vect bytes Bits8 -> a export @@ -294,6 +337,11 @@ export in fromBytes bs1 :: fromBytes bs2 +||| 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. public export RepConstraint : Rep -> Type -> Type RepConstraint (Bytes _) a = ByteRep a