From 1ebf0dcbe9dfb59e7056770fb97ffc9678da0995 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 4 Aug 2022 15:08:17 -0400
Subject: [PATCH] Add Show instance for NP

---
 src/Data/NP.idr                  | 13 +++++++++++--
 src/Data/NumIdr/Array/Array.idr  | 15 +++++++++++----
 src/Data/NumIdr/Array/Coords.idr |  4 ++--
 src/Data/NumIdr/Array/Order.idr  |  2 --
 4 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/src/Data/NP.idr b/src/Data/NP.idr
index d026024..3a0f3d3 100644
--- a/src/Data/NP.idr
+++ b/src/Data/NP.idr
@@ -13,8 +13,17 @@ data NP : (f : k -> Type) -> (ts : Vect n k) -> Type where
 
 public export
 (all : NP (Eq . f) ts) => Eq (NP f ts) where
-  (==) {all = []} [] [] = True
-  (==) {all = _ :: _} (x :: xs) (y :: ys) = (x == y) && (xs == ys)
+  (==) {all=[]} [] [] = True
+  (==) {all=_::_} (x :: xs) (y :: ys) = (x == y) && (xs == ys)
+
+public export
+(all : NP (Show . f) ts) => Show (NP f ts) where
+  show xs = "[" ++ elems xs ++ "]"
+    where
+      elems : {0 f,ts : _} -> (all : NP (Show . f) ts) => NP f ts -> String
+      elems {all=[]} [] = ""
+      elems {all=[_]} [x] = show x
+      elems {all=_::_} (x :: xs) = show x ++ ", " ++ elems xs
 
 
 
diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr
index 81d0e2c..a479500 100644
--- a/src/Data/NumIdr/Array/Array.idr
+++ b/src/Data/NumIdr/Array/Array.idr
@@ -276,10 +276,9 @@ indexSet is = indexUpdate is . const
 ||| coordinates are out of bounds.
 export
 indexNB : Vect rk Nat -> Array {rk} s a -> Maybe a
-indexNB is arr with (viewShape arr)
-  _ | Shape s = if concat @{All} $ zipWith (<) is s
-                then Just $ index (getLocation' (strides arr) is) (getPrim arr)
-                else Nothing
+indexNB is arr = if and $ map delay $ zipWith (<) is (shape arr)
+                  then Just $ index (getLocation' (strides arr) is) (getPrim arr)
+                  else Nothing
 
 ||| Index the array using the given coordinates, returning `Nothing` if the
 ||| coordinates are out of bounds.
@@ -391,6 +390,14 @@ resizeLTE : (s' : Vect rk Nat) -> (0 ok : NP Prelude.id (zipWith LTE s' s)) =>
 resizeLTE s' arr = resize s' (believe_me ()) arr
 
 
+||| List all of the values in an array in row-major order.
+export
+elements : Array {rk} s a -> Vect (product s) a
+elements (MkArray _ sts sh p) =
+  let elems = map (flip index p . getLocation' sts) (getAllCoords' sh)
+  in assert_total $ case toVect (product sh) elems of Just v => v
+
+
 ||| List all of the values in an array along with their coordinates.
 export
 enumerateNB : Array {rk} s a -> List (Vect rk Nat, a)
diff --git a/src/Data/NumIdr/Array/Coords.idr b/src/Data/NumIdr/Array/Coords.idr
index 8dd0fae..5a8033c 100644
--- a/src/Data/NumIdr/Array/Coords.idr
+++ b/src/Data/NumIdr/Array/Coords.idr
@@ -103,8 +103,8 @@ namespace CoordsRange
   getNewPos : {s : _} -> (rs : CoordsRange {rk} s) -> Vect rk Nat -> Vect (newRank rs) Nat
   getNewPos [] [] = []
   getNewPos (r :: rs) (i :: is) with (cRangeToBounds r)
-    getNewPos (r :: rs) (i :: is) | Left _ = getNewPos rs is
-    getNewPos (r :: rs) (i :: is) | Right (x, _) = minus i x :: getNewPos rs is
+    _ | Left _ = getNewPos rs is
+    _ | Right (x, _) = minus i x :: getNewPos rs is
 
   export
   getCoordsList : {s : Vect rk Nat} -> (rs : CoordsRange s) -> List (Vect rk Nat, Vect (newRank rs) Nat)
diff --git a/src/Data/NumIdr/Array/Order.idr b/src/Data/NumIdr/Array/Order.idr
index 633d778..41c35be 100644
--- a/src/Data/NumIdr/Array/Order.idr
+++ b/src/Data/NumIdr/Array/Order.idr
@@ -11,11 +11,9 @@ import Data.Vect
 ||| 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