diff --git a/src/Data/NumIdr/Array.idr b/src/Data/NumIdr/Array.idr new file mode 100644 index 0000000..6476eec --- /dev/null +++ b/src/Data/NumIdr/Array.idr @@ -0,0 +1,41 @@ +module Data.NumIdr.Array + +import Data.Vect +import Data.NumIdr.PrimArray + +%default total + + +export +data Array : Vect rank Nat -> Type -> Type where + MkArray : PrimArray a -> Array dim a + + + +export +size : Array dim a -> Nat +size (MkArray arr) = length arr + +export +fromVect : {0 dim : Vect rank Nat} -> Vect (product dim) a -> Array dim a +fromVect = MkArray . fromList . toList + +export +reshape : {0 dim : Vect rank Nat} -> (0 dim' : Vect rank' Nat) -> + Array dim a -> product dim = product dim' => + Array dim' a +reshape _ (MkArray arr) = MkArray arr + +Vects : Vect rank Nat -> Type -> Type +Vects [] a = a +Vects (d :: dim) a = Vect d (Vects dim a) + + + +export +constant : a -> (dim : Vect rank Nat) -> Array dim a +constant x dim = MkArray $ create (product dim) (const x) + +export +zeros : Num a => (dim : Vect rank Nat) -> Array dim a +zeros = constant 0