From a19ccd59a10594dd9d7e25f93edfea882a87b30f Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Wed, 11 May 2022 23:37:56 -0400
Subject: [PATCH] Move Array module into new directory

---
 src/Data/NumIdr/Array.idr       | 63 ---------------------------------
 src/Data/NumIdr/Array/Array.idr | 52 +++++++++++++++++++++++++++
 2 files changed, 52 insertions(+), 63 deletions(-)
 delete mode 100644 src/Data/NumIdr/Array.idr
 create mode 100644 src/Data/NumIdr/Array/Array.idr

diff --git a/src/Data/NumIdr/Array.idr b/src/Data/NumIdr/Array.idr
deleted file mode 100644
index 81adcfe..0000000
--- a/src/Data/NumIdr/Array.idr
+++ /dev/null
@@ -1,63 +0,0 @@
-module Data.NumIdr.Array
-
-import Data.Vect
-import Data.Reify
-import Data.NumIdr.PrimArray
-
-%default total
-
-
-export
-record Array {0 rk : Nat} (s : Vect rk Nat) a where
-  constructor MkArray
-  shape : Reify s
-  contents : PrimArray a
-
-mkArray : {s : _} -> PrimArray a -> Array s a
-mkArray arr = MkArray (MkReify _) arr
-
-
-export
-size : Array s a -> Nat
-size arr = length arr.contents
-
-export
-shape : {0 s : Vect rk Nat} -> Array s a -> Vect rk Nat
-shape arr = getReify arr.shape
-
-export
-rank : Array s a -> Nat
-rank arr = length $ shape arr
-
-export
-fromVect : {s : Vect rk Nat} -> Vect (product s) a -> Array s a
-fromVect = mkArray . fromList . toList
-
-public export
-Vects : Vect rk Nat -> Type -> Type
-Vects [] a = a
-Vects (d :: s) a = Vect d (Vects s a)
-
-export
-fromVects : {s : _} -> Vects s a -> Array s a
-fromVects = mkArray . fromList . collapse
-  where
-    collapse : {s : Vect rk Nat} -> Vects s a -> List a
-    collapse {s=[]} x = [x]
-    collapse {s=_::_} v = concat $ map collapse v
-
-export
-reshape : {0 s : Vect rk Nat} -> (s' : Vect rk' Nat) ->
-           Array s a -> product s = product s' =>
-           Array s' a
-reshape _ arr = mkArray arr.contents
-
-
-
-export
-constant : a -> (s : Vect rk Nat) -> Array s a
-constant x s = mkArray $ create (product s) (const x)
-
-export
-zeros : Num a => (s : Vect rk Nat) -> Array s a
-zeros = constant 0
diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr
new file mode 100644
index 0000000..7ce1cc7
--- /dev/null
+++ b/src/Data/NumIdr/Array/Array.idr
@@ -0,0 +1,52 @@
+module Data.NumIdr.Array.Array
+
+import Data.Vect
+import Data.Reify
+import Data.NumIdr.PrimArray
+import Data.NumIdr.Array.Order
+
+%default total
+
+
+export
+record Array {0 rk : Nat} (s : Vect rk Nat) a where
+  constructor MkArray
+  shape : Reify s
+  strides : Vect rk Nat
+  contents : PrimArray a
+
+
+export
+getPrim : Array s a -> PrimArray a
+getPrim = contents
+
+export
+getStrides : Array {rk} s a -> Vect rk Nat
+getStrides = strides
+
+export
+size : Array s a -> Nat
+size arr = length arr.contents
+
+export
+shape : Array {rk} s a -> Vect rk Nat
+shape arr = getReify arr.shape
+
+export
+rank : Array s a -> Nat
+rank arr = length $ shape arr
+
+
+
+export
+fromVect' : (s : Vect rk Nat) -> Order rk -> Vect (product s) a -> Array s a
+fromVect' s ord v = MkArray (MkReify s) (calcStrides ord s) (fromList $ toList v)
+
+export
+fromVect : (s : Vect rk Nat) -> Vect (product s) a -> Array s a
+fromVect s = fromVect' s $ rewrite sym (lengthCorrect s) in COrder {rk = length s}
+
+public export
+Vects : Vect rk Nat -> Type -> Type
+Vects []     a = a
+Vects (d::s) a = Vect d (Vects s a)