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