toki/numidr
1
0
Fork 0
Code Issues Pull requests Activity

Add comments to everything

Browse source
This commit is contained in:
Kiana Sheibani 2022-05-13 15:26:43 -04:00
parent a88fc5d9c6
commit a499d14e87
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
5 changed files with 119 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

104
src/Data/NumIdr/Array/Array.idr
View file

@ -8,46 +8,88 @@ import Data.NumIdr.Array.Coords
%default total
||| 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. This is independent of the actual order in which they are stored; the
||| default order is row-major, but this is configurable.
|||
||| @ rk The rank of the array
||| @ s The shape of the array
||| @ a The type of the array's elements
export
data Array : Vect rk Nat -> Type -> Type where
MkArray : (sts : Vect rk Nat) -> (s : Vect rk Nat) -> PrimArray a -> Array s a
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.
|||
||| @ s The shape of the array
||| @ sts The strides of the array
MkArray : (s : Vect rk Nat) -> (sts : Vect rk Nat) -> PrimArray a -> Array s a
||| Extract the primitive array value.
export
getPrim : Array s a -> PrimArray a
getPrim (MkArray _ _ arr) = arr
||| The strides of the array, returned in the same axis order as in the shape.
export
getStrides : Array {rk} s a -> Vect rk Nat
getStrides (MkArray sts _ _) = sts
getStrides (MkArray _ sts _) = sts
||| The total number of elements of the array
||| This is equivalent to `product s`.
export
size : Array s a -> Nat
size = length . getPrim
||| The shape of the array
export
shape : Array {rk} s a -> Vect rk Nat
shape (MkArray _ s _) = s
shape (MkArray s _ _) = s
||| The rank of the array
export
rank : Array s a -> Nat
rank = length . shape
||| 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
||| @ ord The order to interpret the elements
export
fromVect' : (s : Vect rk Nat) -> Order rk -> Vect (product s) a -> Array s a
fromVect' s ord v = MkArray (calcStrides ord s) s (fromList $ toList v)
fromVect' : (s : Vect rk Nat) -> (ord : Order rk) -> Vect (product s) a -> Array s a
fromVect' s ord v = MkArray s (calcStrides ord s) (fromList $ toList v)
||| Create an array given a vector of its elements. The elements of the vector
||| are assembled into the provided shape using row-major order (the last axis is the
||| least significant).
|||
||| @ s The shape of the constructed array
export
fromVect : (s : Vect rk Nat) -> Vect (product s) a -> Array s a
fromVect s = fromVect' s (orderOfShape s COrder)
fromVect s = fromVect' s COrder
||| Construct an array using a structure of nested vectors. The elements are arranged
||| to the specified order before being written.
|||
||| @ s The shape of the constructed array
||| @ ord The order of the constructed array
export
array' : (s : Vect rk Nat) -> Order rk -> Vects s a -> Array s a
array' s ord v = MkArray sts s (unsafeFromIns (product s) ins)
array' : (s : Vect rk Nat) -> (ord : Order rk) -> Vects s a -> Array s a
array' s ord v = MkArray s sts (unsafeFromIns (product s) ins)
where
sts : Vect rk Nat
sts = calcStrides ord s
@ -55,29 +97,35 @@ array' s ord v = MkArray sts s (unsafeFromIns (product s) ins)
ins : List (Nat, a)
ins = collapse $ mapWithIndex (\i,x => (sum $ zipWith (*) i sts, x)) v
||| Construct an array using a structure of nested vectors.
export
reshape' : (s' : Vect rk' Nat) -> Order rk' -> Array {rk} s a ->
product s = product s' => Array s' a
reshape' s' ord' arr = MkArray (calcStrides ord' s') s' (getPrim arr)
array : {s : _} -> Vects s a -> Array s a
array v = MkArray s (calcStrides COrder s) (fromList $ collapse v)
||| Reshape the array into the given shape and reinterpret it according to
||| the given order.
|||
||| @ s' The shape to convert the array to
||| @ ord The order to reinterpret the array by
export
reshape' : (s' : Vect rk' Nat) -> (ord : Order rk') -> Array {rk} s a ->
product s = product s' => Array s' a
reshape' s' ord' arr = MkArray s' (calcStrides ord' s') (getPrim arr)
||| Reshape the array into the given shape.
|||
||| The array is also reinterpreted in row-major order; if this is undesirable,
||| then `reshape'` must be used instead.
|||
||| @ s' The shape to convert the array to
export
reshape : (s' : Vect rk' Nat) -> Array {rk} s a ->
product s = product s' => Array s' a
reshape s' = reshape' s' (orderOfShape s' COrder)
reshape s' = reshape' s' COrder
||| Index the array using the given `Coords` object.
export
index : Coords s -> Array s a -> a
index is arr = index (computeLoc (getStrides arr) is) (getPrim arr)
export
test : Array [2,2,3] Int
test = array' _ FOrder [[[1,2,3],[4,5,6]],[[7,8,9],[10,11,12]]]
export
main : IO ()
main = do
printLn $ index [0,1,0] test
printLn $ index [1,1,2] test
index is arr = index (getLocation (getStrides arr) is) (getPrim arr)

10
src/Data/NumIdr/Array/Coords.idr
View file

@ -5,18 +5,20 @@ import Data.Vect
%default total
||| A type-safe coordinate system for an array. The coordinates are
||| values of `Fin dim`, where `dim` is the dimension of each axis.
public export
data Coords : (s : Vect rk Nat) -> Type where
Nil : Coords Nil
(::) : Fin dim -> Coords s -> Coords (dim :: s)
||| Forget the shape of the array by converting each index to type `Nat`.
export
toNats : Coords {rk} s -> Vect rk Nat
toNats [] = []
toNats (i :: is) = finToNat i :: toNats is
public export
Vects : Vect rk Nat -> Type -> Type
Vects [] a = a
@ -44,6 +46,8 @@ index [] x = x
index (i::is) v = index is $ index i v
||| Compute the memory location of an array element
||| given its coordinate and the strides of the array.
export
computeLoc : Vect rk Nat -> Coords {rk} s -> Nat
computeLoc sts is = sum $ zipWith (*) sts (toNats is)
getLocation : Vect rk Nat -> Coords {rk} s -> Nat
getLocation sts is = sum $ zipWith (*) sts (toNats is)

18
src/Data/NumIdr/Array/Order.idr
View file

@ -6,9 +6,21 @@ import Data.Permutation
%default total
||| 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.
|||
||| @ rk The rank of the array this order applies to
public export
data Order : (rk : Nat) -> Type where
||| C-like order, or contiguous order. This order stores elements in a
||| row-major fashion (the last axis is the least significant).
COrder : Order rk
||| Fortran-like order. This order stores elements in a column-major
||| fashion (the first axis is the least significant).
FOrder : Order rk
@ -24,7 +36,9 @@ scanr f q0 (x::xs) = f x (head qs) :: qs
where qs : Vect len res
qs = scanr f q0 xs
||| Calculate an array's strides given its order and shape.
export
calcStrides : Order rk -> Vect rk Nat -> Vect rk Nat
calcStrides COrder v = tail $ scanr (*) 1 v
calcStrides FOrder v = init $ scanl (*) 1 v
calcStrides _ [] = []
calcStrides COrder v@(_::_) = scanr (*) 1 $ tail v
calcStrides FOrder v@(_::_) = scanl (*) 1 $ init v

12
src/Data/NumIdr/PrimArray.idr
View file

@ -4,6 +4,8 @@ import Data.IOArray.Prims
%default total
||| A wrapper for Idris's primitive array type.
export
record PrimArray a where
constructor MkPrimArray
@ -26,6 +28,8 @@ arrayDataSet : Nat -> a -> ArrayData a -> IO ()
arrayDataSet n x arr = fromPrim $ prim__arraySet arr (cast n) x
||| Construct an array from a list of "instructions" to write a
||| value to a particular index.
export
unsafeFromIns : Nat -> List (Nat, a) -> PrimArray a
unsafeFromIns size ins = unsafePerformIO $ do
@ -33,6 +37,8 @@ unsafeFromIns size ins = unsafePerformIO $ do
for_ ins $ \(i,x) => arrayDataSet i x arr
pure $ MkPrimArray size arr
||| Create an array given its size and a function to generate
||| its elements by its index.
export
create : Nat -> (Nat -> a) -> PrimArray a
create size f = unsafePerformIO $ do
@ -47,10 +53,13 @@ create size f = unsafePerformIO $ do
addToArray (S loc) n arr
||| Index into a primitive array. This function is unsafe, as it
||| performs no boundary check on the index given.
export
index : Nat -> PrimArray a -> a
index n arr = unsafePerformIO $ arrayDataGet n $ content arr
||| A safe version of `index` that ensures the index entered is valid.
export
safeIndex : Nat -> PrimArray a -> Maybe a
safeIndex n arr = if n < length arr
@ -58,6 +67,7 @@ safeIndex n arr = if n < length arr
else Nothing
||| Convert a primitive array to a list.
export
toList : PrimArray a -> List a
toList arr = iter (length arr) []
@ -67,6 +77,7 @@ toList arr = iter (length arr) []
iter (S n) acc = let el = index n arr
in iter n (el :: acc)
||| Construct a primitive array from a list.
export
fromList : List a -> PrimArray a
fromList xs = create (length xs)
@ -76,6 +87,7 @@ fromList xs = create (length xs)
fromJust : Maybe a -> a
fromJust (Just x) = x
||| Map a function over a primitive array.
export
map : (a -> b) -> PrimArray a -> PrimArray b
map f arr = create (length arr) (\n => f $ index n arr)

8
src/Data/Permutation.idr
View file

@ -5,22 +5,28 @@ import Data.Vect
%default total
||| A permutation of `n` elements represented as a vector of indices.
||| For example, `[1,2,0]` is a permutation that maps element `0` to
||| element `1`, element `1` to element `2`, and element `2` to element `0`.
public export
Permutation : Nat -> Type
Permutation : (n : Nat) -> Type
Permutation n = Vect n (Fin n)
||| The identity permutation.
public export
identity : {n : _} -> Permutation n
identity {n=Z} = []
identity {n=S n} = FZ :: map FS identity
||| The permutation that reverses the order of elements.
public export
reversed : {n : _} -> Permutation n
reversed {n=Z} = []
reversed {n=S n} = last :: map weaken reversed
||| Apply a permutation to a vector.
public export
permuteVect : Permutation n -> Vect n a -> Vect n a
permuteVect p v = map (\i => index i v) p