From 015b7f8cb1d793323ec45a8da7545477a0b340dd Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Wed, 15 Jun 2022 22:47:43 -0400
Subject: [PATCH] Rename *Maybe functions to *NB

---
 src/Data/NumIdr/Array/Array.idr  | 20 ++++++++++----------
 src/Data/NumIdr/Array/Coords.idr |  8 ++++----
 src/Data/NumIdr/Matrix.idr       |  4 ++--
 src/Data/NumIdr/Vector.idr       |  6 +++---
 4 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr
index cbbbfc6..cec9f81 100644
--- a/src/Data/NumIdr/Array/Array.idr
+++ b/src/Data/NumIdr/Array/Array.idr
@@ -245,23 +245,23 @@ indexSet is = indexUpdate is . const
 
 
 export
-indexMaybe : Vect rk Nat -> Array {rk} s a -> Maybe a
-indexMaybe is arr with (viewShape arr)
+indexNB : Vect rk Nat -> Array {rk} s a -> Maybe a
+indexNB is arr with (viewShape arr)
   _ | Shape s = if concat @{All} $ zipWith (<) s (shape arr)
                 then Just $ index (getLocation' (strides arr) is) (getPrim arr)
                 else Nothing
 
 export
 (!?) : Array {rk} s a -> Vect rk Nat -> Maybe a
-(!?) = flip indexMaybe
+(!?) = flip indexNB
 
 export
-indexUpdateMaybe : Vect rk Nat -> (a -> a) -> Array {rk} s a -> Array s a
-indexUpdateMaybe is f (MkArray ord sts s arr) = MkArray ord sts s (updateAt (getLocation' sts is) f arr)
+indexUpdateNB : Vect rk Nat -> (a -> a) -> Array {rk} s a -> Array s a
+indexUpdateNB is f (MkArray ord sts s arr) = MkArray ord sts s (updateAt (getLocation' sts is) f arr)
 
 export
-indexSetMaybe : Vect rk Nat -> a -> Array {rk} s a -> Array s a
-indexSetMaybe is = indexUpdateMaybe is . const
+indexSetNB : Vect rk Nat -> a -> Array {rk} s a -> Array s a
+indexSetNB is = indexUpdateNB is . const
 
 
 ||| Index the array using the given `CoordsRange` object.
@@ -320,7 +320,7 @@ reorder ord' arr with (viewShape arr)
 
 export
 resize : (s' : Vect rk Nat) -> a -> Array {rk} s a -> Array s' a
-resize s' x arr = fromFunction' s' (getOrder arr) (fromMaybe x . (arr !?) . toNats)
+resize s' x arr = fromFunction' s' (getOrder arr) (fromMaybe x . (arr !?) . toNB)
 
 export
 enumerate' : Array {rk} s a -> List (Vect rk Nat, a)
@@ -342,8 +342,8 @@ concat axis a b = let sA = shape a
                       dB = index axis sB
                       s = replaceAt axis (dA + dB) sA
                       sts = calcStrides COrder s
-                      ins = map (mapFst $ getLocation' sts . toNats) (enumerate a)
-                            ++ map (mapFst $ getLocation' sts . updateAt axis (+dA) . toNats) (enumerate b)
+                      ins = map (mapFst $ getLocation' sts . toNB) (enumerate a)
+                            ++ map (mapFst $ getLocation' sts . updateAt axis (+dA) . toNB) (enumerate b)
                       -- TODO: prove that the type-level shape and `s` are equivalent
                   in  believe_me $ MkArray COrder sts s (unsafeFromIns (product s) ins)
 
diff --git a/src/Data/NumIdr/Array/Coords.idr b/src/Data/NumIdr/Array/Coords.idr
index e1bc6c5..2f8f3bd 100644
--- a/src/Data/NumIdr/Array/Coords.idr
+++ b/src/Data/NumIdr/Array/Coords.idr
@@ -17,9 +17,9 @@ namespace Coords
 
   ||| Forget the shape of the array by converting each index to type `Nat`.
   export
-  toNats : Coords {rk} s -> Vect rk Nat
-  toNats [] = []
-  toNats (i :: is) = finToNat i :: toNats is
+  toNB : Coords {rk} s -> Vect rk Nat
+  toNB [] = []
+  toNB (i :: is) = finToNat i :: toNB is
 
 
   public export
@@ -51,7 +51,7 @@ namespace Coords
   ||| given its coordinate and the strides of the array.
   export
   getLocation : Vect rk Nat -> Coords {rk} s -> Nat
-  getLocation sts is = getLocation' sts (toNats is)
+  getLocation sts is = getLocation' sts (toNB is)
 
 
 namespace CoordsRange
diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr
index 17feb04..c9f0d67 100644
--- a/src/Data/NumIdr/Matrix.idr
+++ b/src/Data/NumIdr/Matrix.idr
@@ -77,8 +77,8 @@ index : Fin m -> Fin n -> Matrix m n a -> a
 index m n = index [m,n]
 
 export
-indexMaybe : Nat -> Nat -> Matrix m n a -> Maybe a
-indexMaybe m n = indexMaybe [m,n]
+indexNB : Nat -> Nat -> Matrix m n a -> Maybe a
+indexNB m n = indexNB [m,n]
 
 
 export
diff --git a/src/Data/NumIdr/Vector.idr b/src/Data/NumIdr/Vector.idr
index 1e40068..7e35969 100644
--- a/src/Data/NumIdr/Vector.idr
+++ b/src/Data/NumIdr/Vector.idr
@@ -66,12 +66,12 @@ export
 (!!) = flip index
 
 export
-indexMaybe : Nat -> Vector n a -> Maybe a
-indexMaybe n = Array.indexMaybe [n]
+indexNB : Nat -> Vector n a -> Maybe a
+indexNB n = Array.indexNB [n]
 
 export
 (!?) : Vector n a -> Nat -> Maybe a
-(!?) = flip indexMaybe
+(!?) = flip indexNB
 
 
 -- Named projections