
   0 | module Data.C.Array8
   1 | 
   2 | import Control.Monad.Resource
   3 | import Data.C.Integer
   4 | import Data.C.Array
   5 | import Data.Linear.ELift1
   6 | import Data.Vect
   7 | 
   8 | import public Data.Fin
   9 | import public Data.Linear.Token
  10 | import public Data.Array.Index
  11 | 
  12 | import Syntax.T1
  13 | 
  14 | %default total
  15 | 
  16 | export %foreign "scheme,chez:(lambda (x y z) (foreign-set! 'unsigned-8 x y z))"
  17 | prim__setbits8 : AnyPtr -> Integer -> Bits8 -> PrimIO ()
  18 | 
  19 | export %foreign "scheme,chez:(lambda (x y) (foreign-ref 'unsigned-8 x y))"
  20 | prim__getbits8 : AnyPtr -> Integer -> Bits8
  21 | 
  22 | --------------------------------------------------------------------------------
  23 | -- Immutable API
  24 | --------------------------------------------------------------------------------
  25 | 
  26 | export
  27 | record CIArray8 (n : Nat) where
  28 |   constructor IA
  29 |   ptr : AnyPtr
  30 | 
  31 | export %inline
  32 | at : CIArray8 n -> Fin n -> Bits8
  33 | at r x = prim__getbits8 r.ptr (cast $ finToNat x)
  34 | 
  35 | export %inline
  36 | ix : CIArray8 n -> (0 m : Nat) -> (x : Ix (S m) n) => Bits8
  37 | ix r m = at r (ixToFin x)
  38 | 
  39 | export %inline
  40 | atNat : CIArray8 n -> (m : Nat) -> (0 lt : LT m n) => Bits8
  41 | atNat r m = at r (natToFinLT m)
  42 | 
  43 | foldrI : (m : Nat) -> (0 _ : LTE m n) => (Bits8 -> b -> b) -> b -> CIArray8 n -> b
  44 | foldrI 0     _ x r = x
  45 | foldrI (S k) f x r = foldrI k f (f (atNat r k) x) r
  46 | 
  47 | foldrKV_ :
  48 |      (m : Nat)
  49 |   -> {auto 0 prf : LTE m n}
  50 |   -> (Fin n -> Bits8 -> b -> b)
  51 |   -> b
  52 |   -> CIArray8 n
  53 |   -> b
  54 | foldrKV_ 0     _ x r = x
  55 | foldrKV_ (S k) f x r =
  56 |   let fin := natToFinLT k @{prf} in foldrKV_ k f (f fin (at r fin) x) r
  57 | 
  58 | foldlI : (m : Nat) -> (x : Ix m n) => (b -> Bits8 -> b) -> b -> CIArray8 n -> b
  59 | foldlI 0     _ v r = v
  60 | foldlI (S k) f v r = foldlI k f (f v (ix r k)) r
  61 | 
  62 | foldlKV_ :
  63 |      (m : Nat)
  64 |   -> {auto x : Ix m n}
  65 |   -> (Fin n -> b -> Bits8 -> b)
  66 |   -> b
  67 |   -> CIArray8 n
  68 |   -> b
  69 | foldlKV_ 0     _ v r = v
  70 | foldlKV_ (S k) f v r =
  71 |   let fin := ixToFin x in foldlKV_ k f (f fin v (at r fin)) r
  72 | 
  73 | ontoVect :
  74 |      (r : CIArray8 n)
  75 |   -> Vect m Bits8
  76 |   -> (k : Nat)
  77 |   -> {auto 0 lt : LTE k n}
  78 |   -> Vect (m+k) Bits8
  79 | ontoVect r vs 0     = rewrite plusCommutative m 0 in vs
  80 | ontoVect r vs (S x) =
  81 |   let v := atNat r x {lt}
  82 |    in rewrite sym (plusSuccRightSucc m x) in ontoVect r (v::vs) x
  83 | 
  84 | ||| Reads the values from a C pointer into a vector.
  85 | export %inline
  86 | toVect : {n : _} -> (r : CIArray8 n) -> Vect n Bits8
  87 | toVect r = ontoVect r [] n
  88 | 
  89 | ||| Right fold over the values of an array plus their indices.
  90 | export %inline
  91 | foldrKV : {n : _} -> (Fin n -> Bits8 -> b -> b) -> b -> CIArray8 n -> b
  92 | foldrKV = foldrKV_ n
  93 | 
  94 | ||| Right fold over the values of an array
  95 | export %inline
  96 | foldr : {n : _} -> (Bits8 -> b -> b) -> b -> CIArray8 n -> b
  97 | foldr = foldrI n
  98 | 
  99 | ||| Left fold over the values of an array plus their indices.
 100 | export %inline
 101 | foldlKV : {n : _} -> (Fin n -> b -> Bits8 -> b) -> b -> CIArray8 n -> b
 102 | foldlKV = foldlKV_ n
 103 | 
 104 | ||| Left fold over the values of an array
 105 | export %inline
 106 | foldl : {n : _} -> (b -> Bits8 -> b) -> b -> CIArray8 n -> b
 107 | foldl = foldlI n
 108 | 
 109 | --------------------------------------------------------------------------------
 110 | -- IO-API
 111 | --------------------------------------------------------------------------------
 112 | 
 113 | export
 114 | record CArray8 (s : Type) (n : Nat) where
 115 |   constructor CA
 116 |   ptr : AnyPtr
 117 | 
 118 | ||| Convenience alias for `CArray8' RIO`
 119 | public export
 120 | 0 CArray8IO : Nat -> Type
 121 | CArray8IO = CArray8 World
 122 | 
 123 | export %inline
 124 | unsafeUnwrap : CArray8 s n -> AnyPtr
 125 | unsafeUnwrap = ptr
 126 | 
 127 | export %inline
 128 | unsafeWrap : AnyPtr -> CArray8 s n
 129 | unsafeWrap = CA
 130 | 
 131 | --------------------------------------------------------------------------------
 132 | -- Linear API
 133 | --------------------------------------------------------------------------------
 134 | 
 135 | ||| Allocates a new C-pointer of `sizeof a * n` bytes.
 136 | export %inline
 137 | malloc1 : (n : Nat) -> F1 s (CArray8 s n)
 138 | malloc1 n t =
 139 |   let p := prim__malloc (cast n)
 140 |    in CA p # t
 141 | 
 142 | ||| Like `malloc1` but resets all allocated bytes to zero.
 143 | export %inline
 144 | calloc1 : (n : Nat) -> F1 s (CArray8 s n)
 145 | calloc1 n t =
 146 |   let p := prim__calloc (cast n) 1
 147 |    in CA p # t
 148 | 
 149 | ||| Frees the memory allocated for a C pointer and removes it from the
 150 | ||| resources bound to the linear token.
 151 | export %inline
 152 | free1 : (r : CArray8 s n) -> F1' s
 153 | free1 r = ffi (prim__free r.ptr)
 154 | 
 155 | parameters {0 n      : Nat}
 156 |            (r        : CArray8 s n)
 157 | 
 158 |   ||| Reads a value from a C-pointer at the given position.
 159 |   export %inline
 160 |   get : Fin n -> F1 s Bits8
 161 |   get x t = prim__getbits8 r.ptr (cast $ finToNat x) # t
 162 | 
 163 |   ||| Reads a value from a C-pointer at the given position.
 164 |   export %inline
 165 |   getIx : (0 m : Nat) -> (x : Ix (S m) n) => F1 s Bits8
 166 |   getIx m = get (ixToFin x)
 167 | 
 168 |   ||| Reads a value from a C-pointer at the given position.
 169 |   export %inline
 170 |   getNat : (m : Nat) -> (0 lt : LT m n) => F1 s Bits8
 171 |   getNat m = get (natToFinLT m)
 172 | 
 173 |   ||| Writes a value to a C pointer at the given position.
 174 |   export %inline
 175 |   set : Fin n -> Bits8 -> F1' s
 176 |   set x v = ffi $ prim__setbits8 r.ptr (cast $ finToNat x) v
 177 | 
 178 |   ||| Writes a value to a C pointer at the given position.
 179 |   export %inline
 180 |   setIx : (0 m : Nat) -> (x : Ix (S m) n) => Bits8 -> F1' s
 181 |   setIx m = set (ixToFin x)
 182 | 
 183 |   ||| Writes a value to a C pointer at the given position.
 184 |   export %inline
 185 |   setNat : (m : Nat) -> (0 lt : LT m n) => Bits8 -> F1' s
 186 |   setNat m = set (natToFinLT m)
 187 | 
 188 |   writeVect1 : Vect k Bits8 -> Ix k n => F1' s
 189 |   writeVect1           []        t = () # t
 190 |   writeVect1 {k = S m} (x :: xs) t =
 191 |     let _ # t := Array8.setIx m x t
 192 |      in writeVect1 xs t
 193 | 
 194 |   ||| Writes the values from a vector to a C pointer
 195 |   export %inline
 196 |   writeVect : Vect n Bits8 -> F1' s
 197 |   writeVect as = writeVect1 as
 198 | 
 199 |   ||| Temporarily wraps the mutable array in an immutable wrapper and
 200 |   ||| run a computation with that.
 201 |   |||
 202 |   ||| This is safe, because the pure function cannot possibly share the
 203 |   ||| immutable array by storing it in a mutable reference. It is
 204 |   ||| referentially transparent, because we call it from a linear context.
 205 |   export %inline
 206 |   withIArray : (CIArray8 n -> b) -> F1 s b
 207 |   withIArray f t = f (IA r.ptr) # t
 208 | 
 209 | ||| Writes the values from a list to a C pointer
 210 | export %inline
 211 | writeList : (as : List Bits8) -> CArray8 s (length as) -> F1' s
 212 | writeList as r = writeVect r (fromList as)
 213 | 
 214 | export
 215 | withCArray : (n : Nat) -> (f : forall s . CArray8 s n -> F1 s b) -> b
 216 | withCArray n f =
 217 |   run1 $ \t =>
 218 |     let r # t := Array8.malloc1 n t
 219 |         v # t := f r t
 220 |         _ # t := Array8.free1 r t
 221 |      in v # t
 222 | 
 223 | --------------------------------------------------------------------------------
 224 | -- Lift1 API
 225 | --------------------------------------------------------------------------------
 226 | 
 227 | parameters {auto has : Lift1 s f}
 228 | 
 229 |   ||| Allocates a new C-pointer of `sizeof a * n` bytes.
 230 |   export %inline
 231 |   malloc : (n : Nat) -> f (CArray8 s n)
 232 |   malloc n = lift1 (malloc1 n)
 233 | 
 234 |   ||| Like `malloc` but resets all allocated bytes to zero.
 235 |   export %inline
 236 |   calloc : (n : Nat) -> f (CArray8 s n)
 237 |   calloc n = lift1 (calloc1 n)
 238 | 
 239 |   export %inline
 240 |   free : CArray8 s n -> f ()
 241 |   free arr = lift1 (free1 arr)
 242 | 
 243 |   export %inline
 244 |   fromList : (as : List Bits8) -> f (CArray8 s (length as))
 245 |   fromList as = Prelude.do
 246 |     arr <- Array8.malloc (length as)
 247 |     lift1 $ writeList as arr
 248 |     pure arr
 249 | 
 250 | --------------------------------------------------------------------------------
 251 | -- Resource
 252 | --------------------------------------------------------------------------------
 253 | 
 254 | export %inline
 255 | ELift1 s f => Resource f (CArray8 s n) where
 256 |   cleanup arr = lift1 (free1 arr)
 257 |