From cc1cef621bccb6a5b234c241590f7f5d98abc9c2 Mon Sep 17 00:00:00 2001
From: kiana-S <kiana.a.sheibani@gmail.com>
Date: Wed, 11 May 2022 07:12:25 -0400
Subject: [PATCH] Create Data.NumIdr.Array

---
 src/Data/NumIdr/Array.idr | 41 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 src/Data/NumIdr/Array.idr

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