Add ranged unsafe indexing

This commit is contained in:
Kiana Sheibani 2023-03-16 09:16:57 -04:00
parent 3ca15ac2f6
commit 7b6b71780a
Signed by: toki
GPG key ID: 6CB106C25E86A9F7

View file

@ -10,6 +10,7 @@ import Data.NumIdr.Interfaces
import Data.NumIdr.PrimArray import Data.NumIdr.PrimArray
import Data.NumIdr.Array.Order import Data.NumIdr.Array.Order
import Data.NumIdr.Array.Coords import Data.NumIdr.Array.Coords
import Data.NumIdr.Array.Shape
%default total %default total
@ -411,6 +412,34 @@ export %inline
arr !# is = indexUnsafe is arr 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 -- Operations on arrays
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------