
   0 | module Data.C.Array
   1 | 
   2 | import Control.Monad.Resource
   3 | import Data.Buffer
   4 | import Data.C.Deref
   5 | import Data.C.Integer
   6 | import Data.C.SizeOf
   7 | import Data.Linear.ELift1
   8 | import Data.Vect
   9 | 
  10 | import public Data.Fin
  11 | import public Data.Linear.Token
  12 | import public Data.Array.Index
  13 | import public Data.C.Struct
  14 | 
  15 | import Syntax.T1
  16 | 
  17 | %default total
  18 | 
  19 | --------------------------------------------------------------------------------
  20 | -- FFI
  21 | --------------------------------------------------------------------------------
  22 | 
  23 | export %foreign "C__collect_safe:cptr_copy, cptr-idris"
  24 | prim__copy_pp : AnyPtr -> AnyPtr -> Bits32 -> PrimIO ()
  25 | 
  26 | export %foreign "C:cptr_copy, cptr-idris"
  27 | prim__copy_pb : AnyPtr -> Buffer -> Bits32 -> PrimIO ()
  28 | 
  29 | export %foreign "C:cptr_copy, cptr-idris"
  30 | prim__copy_bp : Buffer -> AnyPtr -> Bits32 -> PrimIO ()
  31 | 
  32 | export %foreign "C:cptr_inc_ptr, cptr-idris"
  33 |                 "scheme,chez:(lambda (p x y) (+ p (* x y)))"
  34 | prim__inc_ptr : AnyPtr -> Bits32 -> Bits32 -> AnyPtr
  35 | 
  36 | export %foreign "C:cptr_scrub, cptr-idris"
  37 | prim__scrub : AnyPtr -> Bits32 -> PrimIO ()
  38 | 
  39 | --------------------------------------------------------------------------------
  40 | -- Immutable API
  41 | --------------------------------------------------------------------------------
  42 | 
  43 | ||| A wrapped pointer to a C-array holding `n` values of (C-primitive)
  44 | ||| type `a`.
  45 | |||
  46 | ||| Reading from such an array is O(1) and can be done in pure functions.
  47 | |||
  48 | ||| See `CArrayIO` for a version of mutable C arrays running in `IO`.
  49 | ||| See `CArray` for an mutable wrapper to be used in pure (linear) code.
  50 | |||
  51 | ||| Note : In general, this type is not for prolonged storage in an Idris data
  52 | |||        structure (although this is still possible), because it needs to be
  53 | |||        eventually freed. A typical use case is to make use of this for
  54 | |||        its pure and clean API, but to do so from within `IO` or `F1` by
  55 | |||        using `withIArray`.
  56 | export
  57 | record CIArray (n : Nat) (a : Type) where
  58 |   constructor IA
  59 |   ptr : AnyPtr
  60 | 
  61 | parameters {0 a      : Type}
  62 |            {0 n      : Nat}
  63 |            {auto so  : SizeOf a}
  64 |            {auto dr  : Deref a}
  65 | 
  66 |   export %inline
  67 |   at : CIArray n a -> Fin n -> a
  68 |   at r x =
  69 |     let MkIORes v _ := toPrim (deref $ prim__inc_ptr r.ptr (sizeof a) (cast $ finToNat x)) %MkWorld
  70 |      in v
  71 | 
  72 |   export %inline
  73 |   ix : CIArray n a -> (0 m : Nat) -> (x : Ix (S m) n) => a
  74 |   ix r m = at r (ixToFin x)
  75 | 
  76 |   export %inline
  77 |   atNat : CIArray n a -> (m : Nat) -> (0 lt : LT m n) => a
  78 |   atNat r m = at r (natToFinLT m)
  79 | 
  80 |   foldrI : (m : Nat) -> (0 _ : LTE m n) => (a -> b -> b) -> b -> CIArray n a -> b
  81 |   foldrI 0     _ x r = x
  82 |   foldrI (S k) f x r = foldrI k f (f (atNat r k) x) r
  83 | 
  84 |   foldrKV_ :
  85 |        (m : Nat)
  86 |     -> {auto 0 prf : LTE m n}
  87 |     -> (Fin n -> a -> b -> b)
  88 |     -> b
  89 |     -> CIArray n a
  90 |     -> b
  91 |   foldrKV_ 0     _ x r = x
  92 |   foldrKV_ (S k) f x r =
  93 |     let fin := natToFinLT k @{prf} in foldrKV_ k f (f fin (at r fin) x) r
  94 | 
  95 |   foldlI : (m : Nat) -> (x : Ix m n) => (b -> a -> b) -> b -> CIArray n a -> b
  96 |   foldlI 0     _ v r = v
  97 |   foldlI (S k) f v r = foldlI k f (f v (ix r k)) r
  98 | 
  99 |   foldlKV_ :
 100 |        (m : Nat)
 101 |     -> {auto x : Ix m n}
 102 |     -> (Fin n -> b -> a -> b)
 103 |     -> b
 104 |     -> CIArray n a
 105 |     -> b
 106 |   foldlKV_ 0     _ v r = v
 107 |   foldlKV_ (S k) f v r =
 108 |     let fin := ixToFin x in foldlKV_ k f (f fin v (at r fin)) r
 109 | 
 110 |   ontoVect :
 111 |        (r : CIArray n a)
 112 |     -> Vect m a
 113 |     -> (k : Nat)
 114 |     -> {auto 0 lt : LTE k n}
 115 |     -> Vect (m+k) a
 116 |   ontoVect r vs 0     = rewrite plusCommutative m 0 in vs
 117 |   ontoVect r vs (S x) =
 118 |     let v := atNat r x {lt}
 119 |      in rewrite sym (plusSuccRightSucc m x) in ontoVect r (v::vs) x
 120 | 
 121 | parameters {n : Nat}
 122 |            {auto sz : SizeOf a}
 123 |            {auto de : Deref a}
 124 | 
 125 |   ||| Reads the values from a C pointer into a vector.
 126 |   export %inline
 127 |   toVect : (r : CIArray n a) -> Vect n a
 128 |   toVect r = ontoVect r [] n
 129 | 
 130 |   ||| Right fold over the values of an array plus their indices.
 131 |   export %inline
 132 |   foldrKV : (Fin n -> a -> b -> b) -> b -> CIArray n a -> b
 133 |   foldrKV = foldrKV_ n
 134 | 
 135 |   ||| Right fold over the values of an array
 136 |   export %inline
 137 |   foldr : (a -> b -> b) -> b -> CIArray n a -> b
 138 |   foldr = foldrI n
 139 | 
 140 |   ||| Left fold over the values of an array plus their indices.
 141 |   export %inline
 142 |   foldlKV : (Fin n -> b -> a -> b) -> b -> CIArray n a -> b
 143 |   foldlKV = foldlKV_ n
 144 | 
 145 |   ||| Left fold over the values of an array
 146 |   export %inline
 147 |   foldl : (b -> a -> b) -> b -> CIArray n a -> b
 148 |   foldl = foldlI n
 149 | 
 150 | --------------------------------------------------------------------------------
 151 | -- Mutable C Arrays
 152 | --------------------------------------------------------------------------------
 153 | 
 154 | ||| Allocates a pointer of the given size and uses it for running
 155 | ||| the given computation. The pointer is freed afterwards.
 156 | export %inline
 157 | withPtr : HasIO io => Bits32 -> (AnyPtr -> io a) -> io a
 158 | withPtr sz f = Prelude.do
 159 |   ptr <- pure $ prim__malloc sz
 160 |   res <- f ptr
 161 |   primIO $ prim__free ptr
 162 |   pure res
 163 | 
 164 | ||| A wrapped pointer to a C-array holding `n` values of (C-primitive)
 165 | ||| type `a`.
 166 | |||
 167 | ||| Reading from and writing to such an array is O(1) and runs in `IO`.
 168 | |||
 169 | ||| See `CArray` for a pure version of mutable C arrays using linear types.
 170 | ||| See `CArrayS` for a pure versoin of mutable C arrays using linear types (overwritting/scrubbing before freeing).
 171 | ||| See `CArrayIO` for a version of mutable C arrays usable in IO.
 172 | ||| See `CArrayIOS` for a version of the mutable C arrays usuable in IO (overwritting/scrubbing before freeing)
 173 | |||
 174 | ||| Note : In typical use cases, the memory allocated for a C array must
 175 | |||        be manually released with a call to `free` unless it is part
 176 | |||        of a larger structure `Struct` or managed by an external library.
 177 | export
 178 | record PrimCArray (s : Type) (b : Bool) (n : Nat) (a : Type) where
 179 |   constructor PCA
 180 |   ptr : AnyPtr
 181 | 
 182 | ||| Convenience alias for `PrimCArray s False n a`
 183 | public export
 184 | 0 CArray : (s : Type) -> (n : Nat) -> (a : Type) -> Type
 185 | CArray s n a = PrimCArray s False n a
 186 | 
 187 | ||| Convenience alias for `PrimCArray s True n a`
 188 | public export
 189 | 0 CArrayS : (s : Type) -> (n : Nat) -> (a : Type) -> Type
 190 | CArrayS s n a = PrimCArray s True n a
 191 | 
 192 | ||| Convenience alias for `PrimCArray World False n a`
 193 | public export
 194 | 0 CArrayIO : (n : Nat) -> (a : Type) -> Type
 195 | CArrayIO n a = PrimCArray World False n a
 196 | 
 197 | ||| Convenience alias for `PrimCArray World True n a`
 198 | public export
 199 | 0 CArrayIOS : (n : Nat) -> (a : Type) -> Type
 200 | CArrayIOS n a = PrimCArray World True n a
 201 | 
 202 | public export %inline
 203 | {n : Nat} -> SizeOf a => SizeOf (CArray s n a) where
 204 |   sizeof_ = cast n * sizeof a
 205 | 
 206 | export %inline
 207 | unsafeUnwrap : CArray s n a -> AnyPtr
 208 | unsafeUnwrap = ptr
 209 | 
 210 | export %inline
 211 | unsafeWrap : AnyPtr -> CArray s n a
 212 | unsafeWrap = PCA
 213 | 
 214 | public export
 215 | 0 IOBox : Type -> Type
 216 | IOBox = CArrayIO 1
 217 | 
 218 | public export
 219 | 0 Box : Type -> Type -> Type
 220 | Box s = CArray s 1
 221 | 
 222 | --------------------------------------------------------------------------------
 223 | -- Linear API
 224 | --------------------------------------------------------------------------------
 225 | 
 226 | ||| Allocates a new C-pointer of `sizeof a * n` bytes.
 227 | export %inline
 228 | malloc1 :
 229 |      (0 a : Type)
 230 |   -> {auto so : SizeOf a}
 231 |   -> (n : Nat)
 232 |   -> F1 s (CArray s n a)
 233 | malloc1 a n t =
 234 |   let p := prim__malloc (cast n * sizeof a)
 235 |    in PCA p # t
 236 | 
 237 | ||| Like `malloc1` but resets all allocated bytes to zero.
 238 | export %inline
 239 | calloc1 :
 240 |      (0 a : Type)
 241 |   -> {auto so : SizeOf a}
 242 |   -> (n : Nat)
 243 |   -> F1 s (CArray s n a)
 244 | calloc1 a n t =
 245 |   let p := prim__calloc (cast n) (sizeof a)
 246 |    in PCA p # t
 247 | 
 248 | ||| Frees the memory allocated for a C pointer and removes it from the
 249 | ||| resources bound to the linear token.
 250 | export %inline
 251 | free1 : (r : CArray s n a) -> F1' s
 252 | free1 r = ffi (prim__free r.ptr)
 253 | 
 254 | ||| Frees the memory allocated for a C pointer, after overwriting the data,
 255 | ||| and removes it from the resources bound to the linear token.
 256 | export %inline
 257 | frees1 : {0 a : Type} -> {auto so : SizeOf a} -> {n : Nat} -> (r : CArrayS s n a) -> F1' s
 258 | frees1 r t =
 259 |   let () # t := ffi (prim__scrub r.ptr (cast n * sizeof a)) t
 260 |    in ffi (prim__free r.ptr) t
 261 | 
 262 | ||| Extracts the first value stored in a C pointer.
 263 | export %inline
 264 | unbox : Deref a => (r : CArray s (S n) a) -> F1 s a
 265 | unbox r = ffi $ toPrim (deref r.ptr)
 266 | 
 267 | parameters {0 f      : Type -> Type}
 268 |            {0 n      : Nat}
 269 |            {0 s      : Type}
 270 |            {auto sr  : Struct f}
 271 |            {auto so  : SizeOf (f s)}
 272 |            (r        : CArray s n (f s))
 273 | 
 274 |   ||| Reads a struct from a C-pointer at the given position.
 275 |   export %inline
 276 |   getStruct : Fin n -> F1 s (f s)
 277 |   getStruct x t =
 278 |     let ptr := prim__inc_ptr r.ptr (cast $ finToNat x) (sizeof $ f s)
 279 |      in swrap ptr # t
 280 | 
 281 |   ||| Reads a struct from a C-pointer at the given position.
 282 |   export %inline
 283 |   getStructIx : (0 m : Nat) -> (x : Ix (S m) n) => F1 s (f s)
 284 |   getStructIx m = getStruct (ixToFin x)
 285 | 
 286 |   ||| Reads a struct from a C-pointer at the given position.
 287 |   export %inline
 288 |   getStructNat : (m : Nat) -> (0 lt : LT m n) => F1 s (f s)
 289 |   getStructNat m = getStruct (natToFinLT m)
 290 | 
 291 | parameters {0 a      : Type}
 292 |            {0 n      : Nat}
 293 |            {auto so  : SizeOf a}
 294 |            (r        : CArray s n a)
 295 | 
 296 |   ||| Reads a value from a C-pointer at the given position.
 297 |   export %inline
 298 |   get : Deref a => Fin n -> F1 s a
 299 |   get x = ffi $ toPrim (deref $ prim__inc_ptr r.ptr (cast $ finToNat x) (sizeof a))
 300 | 
 301 |   ||| Reads a value from a C-pointer at the given position.
 302 |   export %inline
 303 |   getIx : Deref a => (0 m : Nat) -> (x : Ix (S m) n) => F1 s a
 304 |   getIx m = get (ixToFin x)
 305 | 
 306 |   ||| Reads a value from a C-pointer at the given position.
 307 |   export %inline
 308 |   getNat : Deref a => (m : Nat) -> (0 lt : LT m n) => F1 s a
 309 |   getNat m = get (natToFinLT m)
 310 | 
 311 |   ||| Writes a value to a C pointer at the given position.
 312 |   export %inline
 313 |   set : SetPtr a => Fin n -> a -> F1' s
 314 |   set x v = ffi $ toPrim (setPtr (prim__inc_ptr r.ptr (cast $ finToNat x) (sizeof a)) v)
 315 | 
 316 |   ||| Writes a value to a C pointer at the given position.
 317 |   export %inline
 318 |   setIx : SetPtr a => (0 m : Nat) -> (x : Ix (S m) n) => a -> F1' s
 319 |   setIx m = set (ixToFin x)
 320 | 
 321 |   ||| Writes a value to a C pointer at the given position.
 322 |   export %inline
 323 |   setNat : SetPtr a => (m : Nat) -> (0 lt : LT m n) => a -> F1' s
 324 |   setNat m = set (natToFinLT m)
 325 | 
 326 |   writeVect1 : SetPtr a => Vect k a -> Ix k n => F1' s
 327 |   writeVect1           []        t = () # t
 328 |   writeVect1 {k = S m} (x :: xs) t =
 329 |     let _ # t := setIx m x t
 330 |      in writeVect1 xs t
 331 | 
 332 |   ||| Writes the values from a vector to a C pointer
 333 |   export %inline
 334 |   writeVect : SetPtr a => Vect n a -> F1' s
 335 |   writeVect as = writeVect1 as
 336 | 
 337 |   ||| Temporarily wraps the mutable array in an immutable wrapper and
 338 |   ||| run a computation with that.
 339 |   |||
 340 |   ||| This is safe, because the pure function cannot possibly share the
 341 |   ||| immutable array by storing it in a mutable reference. It is
 342 |   ||| referentially transparent, because we call it from a linear context.
 343 |   export %inline
 344 |   withIArray : (CIArray n a -> b) -> F1 s b
 345 |   withIArray f t = f (IA r.ptr) # t
 346 | 
 347 | ||| Writes the values from a list to a C pointer
 348 | export %inline
 349 | writeList :
 350 |      {auto so  : SizeOf a}
 351 |   -> {auto sp  : SetPtr a}
 352 |   -> (as       : List a)
 353 |   -> (r        : CArray s (length as) a)
 354 |   -> F1' s
 355 | writeList as r = writeVect r (fromList as)
 356 | 
 357 | export
 358 | withCArray : SizeOf a => (n : Nat) -> (f : forall s . CArray s n a -> F1 s b) -> b
 359 | withCArray n f =
 360 |   run1 $ \t =>
 361 |     let r # t := malloc1 a n t
 362 |         v # t := f r t
 363 |         _ # t := free1 r t
 364 |      in v # t
 365 | 
 366 | --------------------------------------------------------------------------------
 367 | -- Lift1 API
 368 | --------------------------------------------------------------------------------
 369 | 
 370 | parameters {auto has : Lift1 s f}
 371 | 
 372 |   ||| Allocates a new C-pointer of `sizeof a * n` bytes.
 373 |   export %inline
 374 |   malloc : (0 a : Type) -> SizeOf a => (n : Nat) -> f (CArray s n a)
 375 |   malloc a n = lift1 (malloc1 a n)
 376 | 
 377 |   ||| Like `malloc` but resets all allocated bytes to zero.
 378 |   export %inline
 379 |   calloc : (0 a : Type) -> SizeOf a => (n : Nat) -> f (CArray s n a)
 380 |   calloc a n = lift1 (calloc1 a n)
 381 | 
 382 |   ||| Frees the memory allocated for a C-array.
 383 |   |||
 384 |   ||| Note: Only call this if the C array is no longer used and has been
 385 |   |||       allocated via a call to `malloc` or `alloc` (either in C land
 386 |   |||       or in Idris). Afterwards, it is no longer safe to use the array
 387 |   |||       for reading or writing, nor is it safe to call `free` on it again.
 388 |   |||
 389 |   |||       For safe resource management, use the linear version of
 390 |   |||       C arrays if possible. Otherwise, consider using a safer monad
 391 |   |||       than `IO` if possible.
 392 |   export %inline
 393 |   free : CArray s n a -> f ()
 394 |   free arr = lift1 (free1 arr)
 395 | 
 396 |   export %inline
 397 |   fromList : SizeOf a => SetPtr a => (as : List a) -> f (CArray s (length as) a)
 398 |   fromList as = Prelude.do
 399 |     arr <- malloc a (length as)
 400 |     lift1 $ writeList as arr
 401 |     pure arr
 402 | 
 403 | --------------------------------------------------------------------------------
 404 | -- Resource
 405 | --------------------------------------------------------------------------------
 406 | 
 407 | export %inline
 408 | ELift1 s f => Resource f (CArray s n a) where
 409 |   cleanup arr = lift1 (free1 arr)
 410 |