From 7b6b71780a084c85770326aacd585f93e26c4851 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Thu, 16 Mar 2023 09:16:57 -0400 Subject: [PATCH] Add ranged unsafe indexing --- src/Data/NumIdr/Array/Array.idr | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 6e5eaf6..7a04e0f 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -10,6 +10,7 @@ import Data.NumIdr.Interfaces import Data.NumIdr.PrimArray import Data.NumIdr.Array.Order import Data.NumIdr.Array.Coords +import Data.NumIdr.Array.Shape %default total @@ -411,6 +412,34 @@ export %inline arr !# is = indexUnsafe is arr +||| Index the array using the given range of coordinates, returning a new array. +||| WARNING: This function does not perform any bounds check on its inputs. +||| Misuse of this function can easily break memory safety. +export +indexRangeUnsafe : (rs : Vect rk CRangeNB) -> Array s a -> Array (newShape s rs) a +indexRangeUnsafe {s} rs arr with (viewShape arr) + _ | Shape s = + let ord = getOrder arr + sts = calcStrides ord s' + in MkArray ord sts s' + (unsafeFromIns (product s') $ + map (\(is,is') => (getLocation' sts is', + index (getLocation' (strides arr) is) (getPrim arr))) + $ getCoordsList s rs) + where s' : Vect ? Nat + s' = newShape s rs + +||| Index the array using the given range of coordinates, returning a new array. +||| WARNING: This function does not perform any bounds check on its inputs. +||| Misuse of this function can easily break memory safety. +||| +||| This is the operator form of `indexRangeUnsafe`. +export %inline +(!#..) : Array s a -> (rs : Vect rk CRangeNB) -> Array (newShape s rs) a +arr !#.. is = indexRangeUnsafe is arr + + + -------------------------------------------------------------------------------- -- Operations on arrays --------------------------------------------------------------------------------