From ad25af6e3feca25f3f98c11db3260bec4309d091 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 12 May 2022 08:52:45 -0400
Subject: [PATCH] Remove unnecessary Data.Reify module

---
 src/Data/NumIdr/Array/Array.idr | 27 +++++++++++++++++----------
 src/Data/Reify.idr              | 13 -------------
 2 files changed, 17 insertions(+), 23 deletions(-)
 delete mode 100644 src/Data/Reify.idr

diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr
index 7ce1cc7..51ddb81 100644
--- a/src/Data/NumIdr/Array/Array.idr
+++ b/src/Data/NumIdr/Array/Array.idr
@@ -1,7 +1,6 @@
 module Data.NumIdr.Array.Array
 
 import Data.Vect
-import Data.Reify
 import Data.NumIdr.PrimArray
 import Data.NumIdr.Array.Order
 
@@ -9,28 +8,30 @@ import Data.NumIdr.Array.Order
 
 
 export
-record Array {0 rk : Nat} (s : Vect rk Nat) a where
-  constructor MkArray
-  shape : Reify s
-  strides : Vect rk Nat
-  contents : PrimArray a
+data Array : Vect rk Nat -> Type -> Type where
+  MkArray : (ord : Order rk) -> (sts : Vect rk Nat) ->
+              (s : Vect rk Nat) -> PrimArray a -> Array s a
 
 
 export
 getPrim : Array s a -> PrimArray a
-getPrim = contents
+getPrim (MkArray _ _ _ arr) = arr
+
+export
+getOrder : Array {rk} s a -> Order rk
+getOrder (MkArray ord _ _ _) = ord
 
 export
 getStrides : Array {rk} s a -> Vect rk Nat
-getStrides = strides
+getStrides (MkArray _ sts _ _) = sts
 
 export
 size : Array s a -> Nat
-size arr = length arr.contents
+size = length . getPrim
 
 export
 shape : Array {rk} s a -> Vect rk Nat
-shape arr = getReify arr.shape
+shape (MkArray _ _ s _) = s
 
 export
 rank : Array s a -> Nat
@@ -50,3 +51,9 @@ public export
 Vects : Vect rk Nat -> Type -> Type
 Vects []     a = a
 Vects (d::s) a = Vect d (Vects s a)
+
+
+export
+reshape' : (s' : Vect rk' Nat) -> Order rk -> Array {rk} s a ->
+             product s = product s' => Array rk' s' a
+reshape' s' ord arr = MkArray 
diff --git a/src/Data/Reify.idr b/src/Data/Reify.idr
deleted file mode 100644
index 38c173b..0000000
--- a/src/Data/Reify.idr
+++ /dev/null
@@ -1,13 +0,0 @@
-module Data.Reify
-
-%default total
-
-
-public export
-data Reify : a -> Type where
-  MkReify : (x : a) -> Reify x
-
-public export
-getReify : {0 x : a} -> Reify x -> a
-getReify (MkReify x) = x
-