From a499d14e87f2cd9ee732fba32b3c1d3cc2ec6204 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 13 May 2022 15:26:43 -0400 Subject: [PATCH] Add comments to everything --- src/Data/NumIdr/Array/Array.idr | 106 ++++++++++++++++++++++--------- src/Data/NumIdr/Array/Coords.idr | 10 ++- src/Data/NumIdr/Array/Order.idr | 18 +++++- src/Data/NumIdr/PrimArray.idr | 12 ++++ src/Data/Permutation.idr | 8 ++- 5 files changed, 119 insertions(+), 35 deletions(-) diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 2687974..b4bc931 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -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 +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) diff --git a/src/Data/NumIdr/Array/Coords.idr b/src/Data/NumIdr/Array/Coords.idr index 8fcacb6..e47d421 100644 --- a/src/Data/NumIdr/Array/Coords.idr +++ b/src/Data/NumIdr/Array/Coords.idr @@ -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) diff --git a/src/Data/NumIdr/Array/Order.idr b/src/Data/NumIdr/Array/Order.idr index 5032851..83ff31f 100644 --- a/src/Data/NumIdr/Array/Order.idr +++ b/src/Data/NumIdr/Array/Order.idr @@ -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 diff --git a/src/Data/NumIdr/PrimArray.idr b/src/Data/NumIdr/PrimArray.idr index 694a480..3477d4a 100644 --- a/src/Data/NumIdr/PrimArray.idr +++ b/src/Data/NumIdr/PrimArray.idr @@ -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) diff --git a/src/Data/Permutation.idr b/src/Data/Permutation.idr index ef8d6ac..ca3fabe 100644 --- a/src/Data/Permutation.idr +++ b/src/Data/Permutation.idr @@ -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