Rename *Maybe functions to *NB
This commit is contained in:
parent
b0d48eaf00
commit
015b7f8cb1
|
@ -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)
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue