
   0 | module Data.NumIdr.Array.Rep
   1 | 
   2 | import Data.Vect
   3 | import Data.Bits
   4 | import Data.Buffer
   5 | 
   6 | %default total
   7 | 
   8 | 
   9 | --------------------------------------------------------------------------------
  10 | -- Array orders
  11 | --------------------------------------------------------------------------------
  12 | 
  13 | 
  14 | ||| An order is an abstract representation of the way in which contiguous array
  15 | ||| elements are stored in memory. Orders are used to calculate strides, which
  16 | ||| provide a method of converting an array coordinate into a linear memory
  17 | ||| location.
  18 | public export
  19 | data Order : Type where
  20 |   ||| C-like order, or contiguous order. This order stores elements in a
  21 |   ||| row-major fashion (the last axis is the least significant).
  22 |   COrder : Order
  23 |   ||| Fortran-like order. This order stores elements in a column-major
  24 |   ||| fashion (the first axis is the least significant).
  25 |   FOrder : Order
  26 | 
  27 | %name Order o
  28 | 
  29 | 
  30 | public export
  31 | Eq Order where
  32 |   COrder == COrder = True
  33 |   FOrder == FOrder = True
  34 |   COrder == FOrder = False
  35 |   FOrder == COrder = False
  36 | 
  37 | 
  38 | ||| Calculate an array's strides given its order and shape.
  39 | export
  40 | calcStrides : Order -> Vect rk Nat -> Vect rk Nat
  41 | calcStrides _      []        = []
  42 | calcStrides COrder v@(_::_)  = scanr (*) 1 $ tail v
  43 | calcStrides FOrder v@(_::_)  = scanl (*) 1 $ init v
  44 | 
  45 | 
  46 | --------------------------------------------------------------------------------
  47 | -- Array representations
  48 | --------------------------------------------------------------------------------
  49 | 
  50 | 
  51 | ||| An internal representation of an array.
  52 | |||
  53 | ||| Each array internally stores its values based on one of these
  54 | ||| representations.
  55 | public export
  56 | data Rep : Type where
  57 |   ||| Byte-buffer array representation.
  58 |   |||
  59 |   ||| This representations stores elements by converting them into byte values
  60 |   ||| storing them in a `Buffer`. Use of this representation is only valid if
  61 |   ||| the element type implements `ByteRep`.
  62 |   |||
  63 |   ||| @ o The order to store array elements in
  64 |   Bytes : (o : Order) -> Rep
  65 | 
  66 |   ||| Boxed array representation.
  67 |   |||
  68 |   ||| This representation uses a boxed array type to store its elements.
  69 |   |||
  70 |   ||| @ o The order to store array elements in
  71 |   Boxed : (o : Order) -> Rep
  72 | 
  73 |   ||| Linked list array representation.
  74 |   |||
  75 |   ||| This representation uses Idris's standard linked list types to store its
  76 |   ||| elements.
  77 |   Linked : Rep
  78 | 
  79 |   ||| Delayed/Lazy array representation.
  80 |   |||
  81 |   ||| This representation delays the computation of the array's elements, which
  82 |   ||| may be useful in writing efficient algorithms.
  83 |   Delayed : Rep
  84 | 
  85 | %name Rep rep
  86 | 
  87 | 
  88 | ||| An alias for the representation `Boxed COrder`, the C-like boxed array
  89 | ||| representation.
  90 | |||
  91 | ||| This representation is the default for all newly created arrays.
  92 | public export
  93 | B : Rep
  94 | B = Boxed COrder
  95 | 
  96 | ||| An alias for the representation `Linked COrder`.
  97 | public export
  98 | L : Rep
  99 | L = Linked
 100 | 
 101 | ||| An alias for the representation `Delayed`.
 102 | public export
 103 | D : Rep
 104 | D = Delayed
 105 | 
 106 | 
 107 | public export
 108 | Eq Rep where
 109 |   Bytes o == Bytes o' = o == o'
 110 |   Boxed o == Boxed o' = o == o'
 111 |   Linked == Linked = True
 112 |   Delayed == Delayed = True
 113 |   _ == _ = False
 114 | 
 115 | ||| A predicate on representations for those that store their elements
 116 | ||| linearly.
 117 | public export
 118 | data LinearRep : Rep -> Type where
 119 |   BytesIsL : LinearRep (Bytes o)
 120 |   BoxedIsL : LinearRep (Boxed o)
 121 | 
 122 | 
 123 | public export
 124 | forceRepNC : Rep -> Rep
 125 | forceRepNC (Bytes o) = Boxed o
 126 | forceRepNC r = r
 127 | 
 128 | public export
 129 | mergeRep : Rep -> Rep -> Rep
 130 | mergeRep r r' = if r == Delayed || r' == Delayed then Delayed else r
 131 | 
 132 | public export
 133 | mergeRepNC : Rep -> Rep -> Rep
 134 | mergeRepNC r r' =
 135 |   if r == Delayed || r' == Delayed then Delayed
 136 |   else case r of
 137 |         Bytes _ => case r' of
 138 |                     Bytes o => Boxed o
 139 |                     _ => r'
 140 |         _ => r
 141 | 
 142 | public export
 143 | data NoConstraintRep : Rep -> Type where
 144 |   BoxedNC : NoConstraintRep (Boxed o)
 145 |   LinkedNC : NoConstraintRep Linked
 146 |   DelayedNC : NoConstraintRep Delayed
 147 | 
 148 | public export
 149 | mergeRepNCCorrect : (r, r' : Rep) -> NoConstraintRep (mergeRepNC r r')
 150 | mergeRepNCCorrect Delayed _ = DelayedNC
 151 | mergeRepNCCorrect (Bytes y) (Bytes x) = BoxedNC
 152 | mergeRepNCCorrect (Boxed y) (Bytes x) = BoxedNC
 153 | mergeRepNCCorrect Linked (Bytes x) = LinkedNC
 154 | mergeRepNCCorrect (Bytes y) (Boxed x) = BoxedNC
 155 | mergeRepNCCorrect (Boxed y) (Boxed x) = BoxedNC
 156 | mergeRepNCCorrect Linked (Boxed x) = LinkedNC
 157 | mergeRepNCCorrect (Bytes x) Linked = LinkedNC
 158 | mergeRepNCCorrect (Boxed x) Linked = BoxedNC
 159 | mergeRepNCCorrect Linked Linked = LinkedNC
 160 | mergeRepNCCorrect (Bytes x) Delayed = DelayedNC
 161 | mergeRepNCCorrect (Boxed x) Delayed = DelayedNC
 162 | mergeRepNCCorrect Linked Delayed = DelayedNC
 163 | 
 164 | public export
 165 | forceRepNCCorrect : (r : Rep) -> NoConstraintRep (forceRepNC r)
 166 | forceRepNCCorrect (Bytes x) = BoxedNC
 167 | forceRepNCCorrect (Boxed x) = BoxedNC
 168 | forceRepNCCorrect Linked = LinkedNC
 169 | forceRepNCCorrect Delayed = DelayedNC
 170 | 
 171 | 
 172 | --------------------------------------------------------------------------------
 173 | -- Byte representations of elements
 174 | --------------------------------------------------------------------------------
 175 | 
 176 | 
 177 | ||| An interface for elements that can be converted into raw bytes.
 178 | |||
 179 | ||| An implementation of this interface is required to use the `Bytes` array
 180 | ||| representation.
 181 | public export
 182 | interface ByteRep a where
 183 |   ||| The number of bytes used to store each value.
 184 |   bytes : Nat
 185 | 
 186 |   ||| Convert a value into a list of bytes.
 187 |   toBytes : a -> Vect bytes Bits8
 188 | 
 189 |   ||| Convert a list of bytes into a value.
 190 |   fromBytes : Vect bytes Bits8 -> a
 191 | 
 192 | export
 193 | ByteRep Bits8 where
 194 |   bytes = 1
 195 | 
 196 |   toBytes x = [x]
 197 |   fromBytes [x] = x
 198 | 
 199 | export
 200 | ByteRep Bits16 where
 201 |   bytes = 2
 202 | 
 203 |   toBytes x = [cast (x `shiftR` 8), cast x]
 204 |   fromBytes [b1,b2] = cast b1 `shiftL` 8 .|. cast b2
 205 | 
 206 | export
 207 | ByteRep Bits32 where
 208 |   bytes = 4
 209 | 
 210 |   toBytes x = [cast (x `shiftR` 24),
 211 |                cast (x `shiftR` 16),
 212 |                cast (x `shiftR` 8),
 213 |                cast x]
 214 |   fromBytes [b1,b2,b3,b4] =
 215 |     cast b1 `shiftL` 24 .|.
 216 |     cast b2 `shiftL` 16 .|.
 217 |     cast b3 `shiftL` 8 .|.
 218 |     cast b4
 219 | 
 220 | export
 221 | ByteRep Bits64 where
 222 |   bytes = 8
 223 | 
 224 |   toBytes x = [cast (x `shiftR` 56),
 225 |                cast (x `shiftR` 48),
 226 |                cast (x `shiftR` 40),
 227 |                cast (x `shiftR` 32),
 228 |                cast (x `shiftR` 24),
 229 |                cast (x `shiftR` 16),
 230 |                cast (x `shiftR` 8),
 231 |                cast x]
 232 |   fromBytes [b1,b2,b3,b4,b5,b6,b7,b8] =
 233 |     cast b1 `shiftL` 56 .|.
 234 |     cast b2 `shiftL` 48 .|.
 235 |     cast b3 `shiftL` 40 .|.
 236 |     cast b4 `shiftL` 32 .|.
 237 |     cast b5 `shiftL` 24 .|.
 238 |     cast b6 `shiftL` 16 .|.
 239 |     cast b7 `shiftL` 8 .|.
 240 |     cast b8
 241 | 
 242 | export
 243 | ByteRep Int where
 244 |   bytes = 8
 245 | 
 246 |   toBytes x = [cast (x `shiftR` 56),
 247 |                cast (x `shiftR` 48),
 248 |                cast (x `shiftR` 40),
 249 |                cast (x `shiftR` 32),
 250 |                cast (x `shiftR` 24),
 251 |                cast (x `shiftR` 16),
 252 |                cast (x `shiftR` 8),
 253 |                cast x]
 254 |   fromBytes [b1,b2,b3,b4,b5,b6,b7,b8] =
 255 |     cast b1 `shiftL` 56 .|.
 256 |     cast b2 `shiftL` 48 .|.
 257 |     cast b3 `shiftL` 40 .|.
 258 |     cast b4 `shiftL` 32 .|.
 259 |     cast b5 `shiftL` 24 .|.
 260 |     cast b6 `shiftL` 16 .|.
 261 |     cast b7 `shiftL` 8 .|.
 262 |     cast b8
 263 | 
 264 | export
 265 | ByteRep Int8 where
 266 |   bytes = 1
 267 | 
 268 |   toBytes x = [cast x]
 269 |   fromBytes [x] = cast x
 270 | 
 271 | export
 272 | ByteRep Int16 where
 273 |   bytes = 2
 274 | 
 275 |   toBytes x = [cast (x `shiftR` 8), cast x]
 276 |   fromBytes [b1,b2] = cast b1 `shiftL` 8 .|. cast b2
 277 | 
 278 | export
 279 | ByteRep Int32 where
 280 |   bytes = 4
 281 | 
 282 |   toBytes x = [cast (x `shiftR` 24),
 283 |                cast (x `shiftR` 16),
 284 |                cast (x `shiftR` 8),
 285 |                cast x]
 286 |   fromBytes [b1,b2,b3,b4] =
 287 |     cast b1 `shiftL` 24 .|.
 288 |     cast b2 `shiftL` 16 .|.
 289 |     cast b3 `shiftL` 8 .|.
 290 |     cast b4
 291 | 
 292 | export
 293 | ByteRep Int64 where
 294 |   bytes = 8
 295 | 
 296 |   toBytes x = [cast (x `shiftR` 56),
 297 |                cast (x `shiftR` 48),
 298 |                cast (x `shiftR` 40),
 299 |                cast (x `shiftR` 32),
 300 |                cast (x `shiftR` 24),
 301 |                cast (x `shiftR` 16),
 302 |                cast (x `shiftR` 8),
 303 |                cast x]
 304 |   fromBytes [b1,b2,b3,b4,b5,b6,b7,b8] =
 305 |     cast b1 `shiftL` 56 .|.
 306 |     cast b2 `shiftL` 48 .|.
 307 |     cast b3 `shiftL` 40 .|.
 308 |     cast b4 `shiftL` 32 .|.
 309 |     cast b5 `shiftL` 24 .|.
 310 |     cast b6 `shiftL` 16 .|.
 311 |     cast b7 `shiftL` 8 .|.
 312 |     cast b8
 313 | 
 314 | export
 315 | ByteRep Bool where
 316 |   bytes = 1
 317 | 
 318 |   toBytes b = [if b then 1 else 0]
 319 |   fromBytes [x] = x /= 0
 320 | 
 321 | export
 322 | ByteRep a => ByteRep b => ByteRep (a, b) where
 323 |   bytes = bytes {a} + bytes {a=b}
 324 | 
 325 |   toBytes (x,y) = toBytes x ++ toBytes y
 326 |   fromBytes = bimap fromBytes fromBytes . splitAt _
 327 | 
 328 | export
 329 | {n : _} -> ByteRep a => ByteRep (Vect n a) where
 330 |   bytes = n * bytes {a}
 331 | 
 332 |   toBytes xs = concat $ map toBytes xs
 333 |   fromBytes {n = 0} bs = []
 334 |   fromBytes {n = S n} bs =
 335 |     let (bs1, bs2) = splitAt _ bs
 336 |     in  fromBytes bs1 :: fromBytes bs2
 337 | 
 338 | 
 339 | ||| The constraint that each array representation requires.
 340 | |||
 341 | ||| Currently, only the `Bytes` representation has a constraint, requiring an
 342 | ||| implementation of `ByteRep`. All other representations can be used without
 343 | ||| constraint.
 344 | public export
 345 | RepConstraint : Rep -> Type -> Type
 346 | RepConstraint (Bytes _) a = ByteRep a
 347 | RepConstraint (Boxed _) a = ()
 348 | RepConstraint Linked a = ()
 349 | RepConstraint Delayed a = ()
 350 |