3-- Raw access to IOArrays. This interface is unsafe because there's no
4-- bounds checking, and is merely intended to provide primitive access via
5-- the RTS. Safe interfaces (either with run time or compile time
6-- bounds checking) can be implemented on top of this
8-- Implemented entirely by the array primitives in the RTS
9data ArrayData : Type -> Type where
12data IOArray elem = MkIOArray (ArrayData elem)
14||| Create a new array of the given size, with all entries set to the
15||| given default element.
17newArray : Int -> elem -> IO (IOArray elem)
20 MkRaw p <- foreign FFI_C "idris_newArray"
21 (Ptr -> Int -> Raw elem -> IO (Raw (ArrayData elem)))
22 vm size (MkRaw default)
25||| Write an element at a location in an array.
26||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can
27||| be implemented on top of this, either with a run time or compile time
30unsafeWriteArray : IOArray elem -> Int -> elem -> IO ()
31unsafeWriteArray (MkIOArray p) i val
32 = foreign FFI_C "idris_arraySet"
33 (Raw (ArrayData elem) -> Int -> Raw elem -> IO ())
34 (MkRaw p) i (MkRaw val)
36||| Read the element at a location in an array.
37||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can
38||| be implemented on top of this, either with a run time or compile time
41unsafeReadArray : IOArray elem -> Int -> IO elem
42unsafeReadArray (MkIOArray p) i
43 = do MkRaw val <- foreign FFI_C "idris_arrayGet"
44 (Raw (ArrayData elem) -> Int -> IO (Raw elem))
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list