Data.Buffer


   0 | module Data.Buffer
   1 | 
   2 | import Data.List
   3 | 
   4 | %default total
   5 | 
   6 | -- Reading and writing binary buffers. Note that this primitives are unsafe,
   7 | -- in that they don't check that buffer locations are within bounds.
   8 | -- We really need a safe wrapper!
   9 | -- They are used in the Idris compiler itself for reading/writing checked
  10 | -- files.
  11 | 
  12 | -- This is known to the compiler, so maybe ought to be moved to Builtin
  13 | export
  14 | data Buffer : Type where [external]
  15 | 
  16 | %foreign "scheme:blodwen-buffer-size"
  17 |          "RefC:getBufferSize"
  18 |          "node:lambda:b => b.length"
  19 | prim__bufferSize : Buffer -> Int
  20 | 
  21 | export %inline
  22 | rawSize : HasIO io => Buffer -> io Int
  23 | rawSize buf = pure (prim__bufferSize buf)
  24 | 
  25 | %foreign "scheme:blodwen-new-buffer"
  26 |          "RefC:newBuffer"
  27 |          "node:lambda:s=>Buffer.alloc(s)"
  28 | prim__newBuffer : Int -> PrimIO Buffer
  29 | 
  30 | ||| An empty buffer of size 0
  31 | export
  32 | emptyBuffer : HasIO io => io Buffer
  33 | emptyBuffer = primIO $ prim__newBuffer 0
  34 | 
  35 | export
  36 | newBuffer : HasIO io => Int -> io (Maybe Buffer)
  37 | newBuffer size
  38 |     = if size >= 0
  39 |             then do buf <- primIO (prim__newBuffer size)
  40 |                     pure $ Just buf
  41 |                  else pure Nothing
  42 | 
  43 | 
  44 | ------------------------------------------------------------------------
  45 | -- BitsN primitives
  46 | 
  47 | -- There is no endianness indication (LE/BE) for UInt8 since it is a single byte
  48 | 
  49 | -- TODO: remove me when we remove the deprecated `setByte` in a future release
  50 | %foreign "scheme:blodwen-buffer-setbyte"
  51 |          "RefC:setBufferUInt8"
  52 |          "node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)"
  53 | prim__setByte : Buffer -> (offset : Int) -> (val : Int) -> PrimIO ()
  54 | 
  55 | %foreign "scheme:blodwen-buffer-setbyte"
  56 |          "RefC:setBufferUInt8"
  57 |          "node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)"
  58 | prim__setBits8 : Buffer -> (offset : Int) -> (val: Bits8) -> PrimIO ()
  59 | 
  60 | -- Assumes val is in the range 0-255
  61 | ||| Use `setBits8` instead, as its value is correctly limited.
  62 | %deprecate
  63 | export %inline
  64 | setByte : HasIO io => Buffer -> (offset : Int) -> (val : Int) -> io ()
  65 | setByte buf offset val
  66 |     = primIO (prim__setByte buf offset val)
  67 | 
  68 | export %inline
  69 | setBits8 : HasIO io => Buffer -> (offset : Int) -> (val : Bits8) -> io ()
  70 | setBits8 buf offset val
  71 |     = primIO (prim__setBits8 buf offset val)
  72 | 
  73 | -- TODO: remove me when we remove the deprecated `getByte` in a future release
  74 | %foreign "scheme:blodwen-buffer-getbyte"
  75 |          "RefC:getBufferByte"
  76 |          "node:lambda:(buf,offset)=>buf.readUInt8(offset)"
  77 | prim__getByte : Buffer -> (offset : Int) -> PrimIO Int
  78 | 
  79 | %foreign "scheme:blodwen-buffer-getbyte"
  80 |          "RefC:getBufferUInt8"
  81 |          "node:lambda:(buf,offset)=>buf.readUInt8(offset)"
  82 | prim__getBits8 : Buffer -> (offset : Int) -> PrimIO Bits8
  83 | 
  84 | ||| Use `getBits8` instead, as its value is correctly limited.
  85 | %deprecate
  86 | export %inline
  87 | getByte : HasIO io => Buffer -> (offset : Int) -> io Int
  88 | getByte buf offset
  89 |     = primIO (prim__getByte buf offset)
  90 | 
  91 | export %inline
  92 | getBits8 : HasIO io => Buffer -> (offset : Int) -> io Bits8
  93 | getBits8 buf offset
  94 |     = primIO (prim__getBits8 buf offset)
  95 | 
  96 | %foreign "scheme:blodwen-buffer-setbits16"
  97 |          "RefC:setBufferUInt16LE"
  98 |          "node:lambda:(buf,offset,value)=>buf.writeUInt16LE(value, offset)"
  99 | prim__setBits16 : Buffer -> (offset : Int) -> (value : Bits16) -> PrimIO ()
 100 | 
 101 | export %inline
 102 | setBits16 : HasIO io => Buffer -> (offset : Int) -> (val : Bits16) -> io ()
 103 | setBits16 buf offset val
 104 |     = primIO (prim__setBits16 buf offset val)
 105 | 
 106 | %foreign "scheme:blodwen-buffer-getbits16"
 107 |          "RefC:getBufferUInt16LE"
 108 |          "node:lambda:(buf,offset)=>buf.readUInt16LE(offset)"
 109 | prim__getBits16 : Buffer -> (offset : Int) -> PrimIO Bits16
 110 | 
 111 | export %inline
 112 | getBits16 : HasIO io => Buffer -> (offset : Int) -> io Bits16
 113 | getBits16 buf offset
 114 |     = primIO (prim__getBits16 buf offset)
 115 | 
 116 | %foreign "scheme:blodwen-buffer-setbits32"
 117 |          "RefC:setBufferUInt32LE"
 118 |          "node:lambda:(buf,offset,value)=>buf.writeUInt32LE(value, offset)"
 119 | prim__setBits32 : Buffer -> (offset : Int) -> (value : Bits32) -> PrimIO ()
 120 | 
 121 | export %inline
 122 | setBits32 : HasIO io => Buffer -> (offset : Int) -> (val : Bits32) -> io ()
 123 | setBits32 buf offset val
 124 |     = primIO (prim__setBits32 buf offset val)
 125 | 
 126 | %foreign "scheme:blodwen-buffer-getbits32"
 127 |          "RefC:getBufferUInt32LE"
 128 |          "node:lambda:(buf,offset)=>buf.readUInt32LE(offset)"
 129 | prim__getBits32 : Buffer -> Int -> PrimIO Bits32
 130 | 
 131 | export %inline
 132 | getBits32 : HasIO io => Buffer -> (offset : Int) -> io Bits32
 133 | getBits32 buf offset
 134 |     = primIO (prim__getBits32 buf offset)
 135 | 
 136 | %foreign "scheme:blodwen-buffer-setbits64"
 137 |          "RefC:setBufferUInt64LE"
 138 |          "node:lambda:(buf,offset,value)=>buf.writeBigUInt64LE(value, offset)"
 139 | prim__setBits64 : Buffer -> Int -> Bits64 -> PrimIO ()
 140 | 
 141 | export %inline
 142 | setBits64 : HasIO io => Buffer -> (offset : Int) -> (val : Bits64) -> io ()
 143 | setBits64 buf offset val
 144 |     = primIO (prim__setBits64 buf offset val)
 145 | 
 146 | %foreign "scheme:blodwen-buffer-getbits64"
 147 |          "RefC:getBufferUInt64LE"
 148 |          "node:lambda:(buf,offset)=>buf.readBigUInt64LE(offset)"
 149 | prim__getBits64 : Buffer -> (offset : Int) -> PrimIO Bits64
 150 | 
 151 | export %inline
 152 | getBits64 : HasIO io => Buffer -> (offset : Int) -> io Bits64
 153 | getBits64 buf offset
 154 |     = primIO (prim__getBits64 buf offset)
 155 | 
 156 | ------------------------------------------------------------------------
 157 | -- IntN primitives
 158 | 
 159 | -- There is no endianness indication (LE/BE) for Int8 since it is a single byte
 160 | 
 161 | %foreign "scheme:blodwen-buffer-setint8"
 162 |          "RefC:setBufferUInt8"
 163 | prim__setInt8 : Buffer -> (offset : Int) -> (val : Int8) -> PrimIO ()
 164 | 
 165 | export %inline
 166 | setInt8 : HasIO io => Buffer -> (offset : Int) -> (val : Int8) -> io ()
 167 | setInt8 buf offset val
 168 |     = primIO (prim__setInt8 buf offset val)
 169 | 
 170 | %foreign "scheme:blodwen-buffer-getint8"
 171 |          "RefC:getBufferByte"
 172 | prim__getInt8 : Buffer -> (offset : Int) -> PrimIO Int8
 173 | 
 174 | export %inline
 175 | getInt8 : HasIO io => Buffer -> (offset : Int) -> io Int8
 176 | getInt8 buf offset
 177 |     = primIO (prim__getInt8 buf offset)
 178 | 
 179 | %foreign "scheme:blodwen-buffer-setint16"
 180 |          "RefC:setBufferInt16LE"
 181 |          "node:lambda:(buf,offset,value)=>buf.writeInt16LE(value, offset)"
 182 | prim__setInt16 : Buffer -> (offset : Int) -> (val : Int16) -> PrimIO ()
 183 | 
 184 | export %inline
 185 | setInt16 : HasIO io => Buffer -> (offset : Int) -> (val : Int16) -> io ()
 186 | setInt16 buf offset val
 187 |     = primIO (prim__setInt16 buf offset val)
 188 | 
 189 | %foreign "scheme:blodwen-buffer-getint16"
 190 |          "RefC:getBufferInt16LE"
 191 | prim__getInt16 : Buffer -> (offset : Int) -> PrimIO Int16
 192 | 
 193 | export %inline
 194 | getInt16 : HasIO io => Buffer -> (offset : Int) -> io Int16
 195 | getInt16 buf offset
 196 |     = primIO (prim__getInt16 buf offset)
 197 | 
 198 | 
 199 | %foreign "scheme:blodwen-buffer-setint32"
 200 |          "RefC:setBufferInt32LE"
 201 |          "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
 202 | prim__setInt32 : Buffer -> (offset : Int) -> (val : Int32) -> PrimIO ()
 203 | 
 204 | export %inline
 205 | setInt32 : HasIO io => Buffer -> (offset : Int) -> (val : Int32) -> io ()
 206 | setInt32 buf offset val
 207 |     = primIO (prim__setInt32 buf offset val)
 208 | 
 209 | %foreign "scheme:blodwen-buffer-getint32"
 210 |          "RefC:getBufferInt32LE"
 211 |          "node:lambda:(buf,offset)=>buf.readInt32LE(offset)"
 212 | prim__getInt32 : Buffer -> (offset : Int) -> PrimIO Int32
 213 | 
 214 | export %inline
 215 | getInt32 : HasIO io => Buffer -> (offset : Int) -> io Int32
 216 | getInt32 buf offset
 217 |     = primIO (prim__getInt32 buf offset)
 218 | 
 219 | %foreign "scheme:blodwen-buffer-setint64"
 220 |          "RefC:setBufferInt64LE"
 221 | prim__setInt64 : Buffer -> (offset : Int) -> (val : Int64) -> PrimIO ()
 222 | 
 223 | export %inline
 224 | setInt64 : HasIO io => Buffer -> (offset : Int) -> (val : Int64) -> io ()
 225 | setInt64 buf offset val
 226 |     = primIO (prim__setInt64 buf offset val)
 227 | 
 228 | %foreign "scheme:blodwen-buffer-getint64"
 229 |          "RefC:getBufferInt64LE"
 230 | prim__getInt64 : Buffer -> (offset : Int) -> PrimIO Int64
 231 | 
 232 | export %inline
 233 | getInt64 : HasIO io => Buffer -> (offset : Int) -> io Int64
 234 | getInt64 buf offset
 235 |     = primIO (prim__getInt64 buf offset)
 236 | 
 237 | ------------------------------------------------------------------------
 238 | -- Int (backend-dependent: 64 on scheme, refc, and 32 on js)
 239 | 
 240 | %foreign "scheme:blodwen-buffer-setint"
 241 |          "RefC:setBufferInt64LE"
 242 |          "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
 243 | prim__setInt : Buffer -> (offset : Int) -> (val : Int) -> PrimIO ()
 244 | 
 245 | export %inline
 246 | setInt : HasIO io => Buffer -> (offset : Int) -> (val : Int) -> io ()
 247 | setInt buf offset val
 248 |     = primIO (prim__setInt buf offset val)
 249 | 
 250 | %foreign "scheme:blodwen-buffer-getint"
 251 |          "RefC:getBufferInt64LE"
 252 |          "node:lambda:(buf,offset)=>buf.readInt32LE(offset)"
 253 | prim__getInt : Buffer -> (offset : Int) -> PrimIO Int
 254 | 
 255 | export %inline
 256 | getInt : HasIO io => Buffer -> (offset : Int) -> io Int
 257 | getInt buf offset
 258 |     = primIO (prim__getInt buf offset)
 259 | 
 260 | ------------------------------------------------------------------------
 261 | -- Double
 262 | 
 263 | %foreign "scheme:blodwen-buffer-setdouble"
 264 |          "RefC:setBufferDouble"
 265 |          "node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, offset)"
 266 | prim__setDouble : Buffer -> (offset : Int) -> (val : Double) -> PrimIO ()
 267 | 
 268 | export %inline
 269 | setDouble : HasIO io => Buffer -> (offset : Int) -> (val : Double) -> io ()
 270 | setDouble buf offset val
 271 |     = primIO (prim__setDouble buf offset val)
 272 | 
 273 | %foreign "scheme:blodwen-buffer-getdouble"
 274 |          "RefC:getBufferDouble"
 275 |          "node:lambda:(buf,offset)=>buf.readDoubleLE(offset)"
 276 | prim__getDouble : Buffer -> (offset : Int) -> PrimIO Double
 277 | 
 278 | export %inline
 279 | getDouble : HasIO io => Buffer -> (offset : Int) -> io Double
 280 | getDouble buf offset
 281 |     = primIO (prim__getDouble buf offset)
 282 | 
 283 | ------------------------------------------------------------------------
 284 | -- Bool
 285 | 
 286 | export
 287 | setBool : HasIO io => Buffer -> (offset : Int) -> (val : Bool) -> io ()
 288 | setBool buf offset val = setBits8 buf offset (ifThenElse val 0 1)
 289 | 
 290 | export
 291 | getBool : HasIO io => Buffer -> (offset : Int) -> io Bool
 292 | getBool buf offset = (0 ==) <$> getBits8 buf offset
 293 | 
 294 | ------------------------------------------------------------------------
 295 | -- Arbitrary precision nums
 296 | 
 297 | ||| setNat returns the end offset
 298 | export
 299 | setNat : HasIO io => Buffer -> (offset : Int) -> (val : Nat) -> io Int
 300 | setNat buf offset val
 301 |   = do let limbs = toLimbs (cast val)
 302 |        let len = foldl (const . (1+)) 0 limbs -- tail recursive length
 303 |        setInt64 buf offset len
 304 |        setLimbs (offset + 8) limbs
 305 | 
 306 |   where
 307 | 
 308 |   toLimbs : Integer -> List Bits32
 309 |   toLimbs 0 = []
 310 |   toLimbs (-1) = [-1]
 311 |   toLimbs x = fromInteger (prim__and_Integer x 0xffffffff) ::
 312 |               toLimbs (assert_smaller x (prim__shr_Integer x 32))
 313 | 
 314 |   setLimbs : (offset : Int) -> List Bits32 -> io Int
 315 |   setLimbs offset [] = pure offset
 316 |   setLimbs offset (limb :: limbs)
 317 |     = do setBits32 buf offset limb
 318 |          setLimbs (offset + 4) limbs
 319 | 
 320 | ||| getNat returns the end offset
 321 | export
 322 | getNat : HasIO io => Buffer -> (offset : Int) -> io (Int, Nat)
 323 | getNat buf offset
 324 |   = do len <- getInt64 buf offset
 325 |        when (len < 0) $ assert_total $ idris_crash "INTERNAL ERROR: getNat -> corrupt Nat"
 326 |        limbs <- getLimbs [<] (offset + 8) len
 327 |        pure (offset + 8 + 4 * cast len, cast $ fromLimbs limbs)
 328 | 
 329 |   where
 330 | 
 331 |   fromLimbs : List Bits32 -> Integer
 332 |   fromLimbs [] = 0
 333 |   fromLimbs (x :: xs) = cast x + prim__shl_Integer (fromLimbs xs) 32
 334 | 
 335 |   getLimbs : SnocList Bits32 -> (offset : Int) -> (len : Int64) -> io (List Bits32)
 336 |   getLimbs acc offset 0 = pure (acc <>> [])
 337 |   getLimbs acc offset len
 338 |     = do limb <- getBits32 buf offset
 339 |          getLimbs (acc :< limb) (offset + 4) (assert_smaller len (len -1))
 340 | 
 341 | ||| setInteger returns the end offset
 342 | export
 343 | setInteger : HasIO io => Buffer -> (offset : Int) -> (val : Integer) -> io Int
 344 | setInteger buf offset val = if val < 0
 345 |   then do setBool buf offset True
 346 |           setNat buf (offset + 1) (cast (- val))
 347 |   else do setBool buf offset False
 348 |           setNat buf (offset + 1) (cast val)
 349 | 
 350 | ||| getInteger returns the end offset
 351 | export
 352 | getInteger : HasIO io => Buffer -> (offset : Int) -> io (Int, Integer)
 353 | getInteger buf offset
 354 |   = do b <- getBool buf offset
 355 |        map (ifThenElse b negate id . cast) <$> getNat buf (offset + 1)
 356 | 
 357 | ------------------------------------------------------------------------
 358 | -- String
 359 | 
 360 | -- Get the length of a string in bytes, rather than characters
 361 | export
 362 | %foreign "scheme:blodwen-stringbytelen"
 363 |          "C:strlen, libc 6"
 364 |          "javascript:lambda:(string)=>new TextEncoder().encode(string).length"
 365 | stringByteLength : String -> Int
 366 | 
 367 | %foreign "scheme:blodwen-buffer-setstring"
 368 |          "RefC:setBufferString"
 369 |          "node:lambda:(buf,offset,value)=>buf.write(value, offset,buf.length - offset, 'utf-8')"
 370 | prim__setString : Buffer -> (offset : Int) -> (val : String) -> PrimIO ()
 371 | 
 372 | export %inline
 373 | setString : HasIO io => Buffer -> (offset : Int) -> (val : String) -> io ()
 374 | setString buf offset val
 375 |     = primIO (prim__setString buf offset val)
 376 | 
 377 | %foreign "scheme:blodwen-buffer-getstring"
 378 |          "RefC:getBufferString"
 379 |          "node:lambda:(buf,offset,len)=>buf.slice(offset, offset+len).toString('utf-8')"
 380 | prim__getString : Buffer -> (offset : Int) -> (len : Int) -> PrimIO String
 381 | 
 382 | export %inline
 383 | getString : HasIO io => Buffer -> (offset : Int) -> (len : Int) -> io String
 384 | getString buf offset len
 385 |     = primIO (prim__getString buf offset len)
 386 | 
 387 | ||| Use `bufferData'` instead, as its value is correctly limited.
 388 | %deprecate
 389 | export
 390 | covering
 391 | bufferData : HasIO io => Buffer -> io (List Int)
 392 | bufferData buf
 393 |     = do len <- rawSize buf
 394 |          unpackTo [] len
 395 |   where
 396 |     covering
 397 |     unpackTo : List Int -> Int -> io (List Int)
 398 |     unpackTo acc 0 = pure acc
 399 |     unpackTo acc offset
 400 |         = do val <- getBits8 buf (offset - 1)
 401 |              unpackTo (cast val :: acc) (offset - 1)
 402 | 
 403 | ||| This function performs the same task as `bufferData` but it
 404 | ||| returns `List Bits8` which is more correct than `List Int`.
 405 | export
 406 | covering
 407 | bufferData' : HasIO io => Buffer -> io (List Bits8)
 408 | bufferData' buf
 409 |     = do len <- rawSize buf
 410 |          unpackTo [] len
 411 |   where
 412 |     covering
 413 |     unpackTo : List Bits8 -> Int -> io (List Bits8)
 414 |     unpackTo acc 0 = pure acc
 415 |     unpackTo acc offset
 416 |         = do val <- getBits8 buf (offset - 1)
 417 |              unpackTo (val :: acc) (offset - 1)
 418 | 
 419 | 
 420 | %foreign "scheme:blodwen-buffer-copydata"
 421 |          "RefC:copyBuffer"
 422 |          "node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,o2,o1,o1+length)"
 423 | prim__copyData : (src : Buffer) -> (srcOffset, len : Int) ->
 424 |                  (dst : Buffer) -> (dstOffset : Int) -> PrimIO ()
 425 | 
 426 | export
 427 | copyData : HasIO io => Buffer -> (srcOffset, len : Int) ->
 428 |            (dst : Buffer) -> (dstOffset : Int) -> io ()
 429 | copyData src start len dest offset
 430 |     = primIO (prim__copyData src start len dest offset)
 431 | 
 432 | export
 433 | resizeBuffer : HasIO io => Buffer -> Int -> io (Maybe Buffer)
 434 | resizeBuffer old newsize
 435 |     = do Just buf <- newBuffer newsize
 436 |               | Nothing => pure Nothing
 437 |          -- If the new buffer is smaller than the old one, just copy what
 438 |          -- fits
 439 |          oldsize <- rawSize old
 440 |          let len = if newsize < oldsize then newsize else oldsize
 441 |          copyData old 0 len buf 0
 442 |          pure (Just buf)
 443 | 
 444 | ||| Create a buffer containing the concatenated content from a
 445 | ||| list of buffers.
 446 | export
 447 | concatBuffers : HasIO io => List Buffer -> io (Maybe Buffer)
 448 | concatBuffers xs
 449 |     = do let sizes = map prim__bufferSize xs
 450 |          let (totalSize, revCumulative) = foldl scanSize (0,[]) sizes
 451 |          let cumulative = reverse revCumulative
 452 |          Just buf <- newBuffer totalSize
 453 |               | Nothing => pure Nothing
 454 |          traverse_ (\(b, size, watermark) => copyData b 0 size buf watermark) (zip3 xs sizes cumulative)
 455 |          pure (Just buf)
 456 |     where
 457 |         scanSize : (Int, List Int) -> Int -> (Int, List Int)
 458 |         scanSize (s, cs) x  = (s+x, s::cs)
 459 | 
 460 | ||| Split a buffer into two at a position.
 461 | export
 462 | splitBuffer : HasIO io => Buffer -> Int -> io (Maybe (Buffer, Buffer))
 463 | splitBuffer buf pos = do size <- rawSize buf
 464 |                          if pos > 0 && pos < size
 465 |                              then do Just first <- newBuffer pos
 466 |                                         | Nothing => pure Nothing
 467 |                                      Just second <- newBuffer (size - pos)
 468 |                                         | Nothing => pure Nothing
 469 |                                      copyData buf 0 pos first 0
 470 |                                      copyData buf pos (size-pos) second 0
 471 |                                      pure $ Just (first, second)
 472 |                              else pure Nothing
 473 |