From eeb2967f6f92584274e450486e7197a2c903dedf Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 5 May 2023 13:41:21 -0400 Subject: [PATCH] Rename Data.NumIdr.Array.Order to Rep --- numidr.ipkg | 2 +- src/Data/NumIdr/Array/Array.idr | 2 +- src/Data/NumIdr/Array/Rep.idr | 71 +++++++++++++++++++++++++++++++++ 3 files changed, 73 insertions(+), 2 deletions(-) create mode 100644 src/Data/NumIdr/Array/Rep.idr diff --git a/numidr.ipkg b/numidr.ipkg index 1f09230..40eb48c 100644 --- a/numidr.ipkg +++ b/numidr.ipkg @@ -15,7 +15,7 @@ modules = Data.NP, Data.NumIdr.Array, Data.NumIdr.Array.Array, Data.NumIdr.Array.Coords, - Data.NumIdr.Array.Order, + Data.NumIdr.Array.Rep, Data.NumIdr.Homogeneous, Data.NumIdr.Matrix, Data.NumIdr.Interfaces, diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 7a04e0f..5cbb030 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -8,7 +8,7 @@ import Data.NP import Data.Permutation import Data.NumIdr.Interfaces import Data.NumIdr.PrimArray -import Data.NumIdr.Array.Order +import Data.NumIdr.Array.Rep import Data.NumIdr.Array.Coords import Data.NumIdr.Array.Shape diff --git a/src/Data/NumIdr/Array/Rep.idr b/src/Data/NumIdr/Array/Rep.idr new file mode 100644 index 0000000..31b5ab5 --- /dev/null +++ b/src/Data/NumIdr/Array/Rep.idr @@ -0,0 +1,71 @@ +module Data.NumIdr.Array.Rep + +import Data.Vect + +%default total + + +-------------------------------------------------------------------------------- +-- Array orders +-------------------------------------------------------------------------------- + + +||| 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. +public export +data Order : 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 + ||| Fortran-like order. This order stores elements in a column-major + ||| fashion (the first axis is the least significant). + FOrder : Order + + +public export +Eq Order where + COrder == COrder = True + FOrder == FOrder = True + COrder == FOrder = False + FOrder == COrder = False + + +||| Calculate an array's strides given its order and shape. +export +calcStrides : Order -> Vect rk Nat -> Vect rk Nat +calcStrides _ [] = [] +calcStrides COrder v@(_::_) = scanr (*) 1 $ tail v +calcStrides FOrder v@(_::_) = scanl (*) 1 $ init v + + +-------------------------------------------------------------------------------- +-- Array representations +-------------------------------------------------------------------------------- + + +public export +data Rep : Type where + Bytes : Order -> Rep + Boxed : Order -> Rep + Linked : Rep + Delayed : Rep + +public export +B : Rep +B = Boxed COrder + +public export +L : Rep +L = Linked + +public export +D : Rep +D = Delayed + + +public export +data LinearRep : Rep -> Type where + BytesIsL : LinearRep (Bytes o) + BoxedIsL : LinearRep (Boxed o)