
   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 | prim__setInt8 : Buffer -> (offset : Int) -> (val : Int8) -> PrimIO ()
 163 | 
 164 | export %inline
 165 | setInt8 : HasIO io => Buffer -> (offset : Int) -> (val : Int8) -> io ()
 166 | setInt8 buf offset val
 167 |     = primIO (prim__setInt8 buf offset val)
 168 | 
 169 | %foreign "scheme:blodwen-buffer-getint8"
 170 | prim__getInt8 : Buffer -> (offset : Int) -> PrimIO Int8
 171 | 
 172 | export %inline
 173 | getInt8 : HasIO io => Buffer -> (offset : Int) -> io Int8
 174 | getInt8 buf offset
 175 |     = primIO (prim__getInt8 buf offset)
 176 | 
 177 | %foreign "scheme:blodwen-buffer-setint16"
 178 |          "RefC:setBufferInt16LE"
 179 |          "node:lambda:(buf,offset,value)=>buf.writeInt16LE(value, offset)"
 180 | prim__setInt16 : Buffer -> (offset : Int) -> (val : Int16) -> PrimIO ()
 181 | 
 182 | export %inline
 183 | setInt16 : HasIO io => Buffer -> (offset : Int) -> (val : Int16) -> io ()
 184 | setInt16 buf offset val
 185 |     = primIO (prim__setInt16 buf offset val)
 186 | 
 187 | %foreign "scheme:blodwen-buffer-getint16"
 188 | prim__getInt16 : Buffer -> (offset : Int) -> PrimIO Int16
 189 | 
 190 | export %inline
 191 | getInt16 : HasIO io => Buffer -> (offset : Int) -> io Int16
 192 | getInt16 buf offset
 193 |     = primIO (prim__getInt16 buf offset)
 194 | 
 195 | 
 196 | %foreign "scheme:blodwen-buffer-setint32"
 197 |          "RefC:setBufferInt32LE"
 198 |          "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
 199 | prim__setInt32 : Buffer -> (offset : Int) -> (val : Int32) -> PrimIO ()
 200 | 
 201 | export %inline
 202 | setInt32 : HasIO io => Buffer -> (offset : Int) -> (val : Int32) -> io ()
 203 | setInt32 buf offset val
 204 |     = primIO (prim__setInt32 buf offset val)
 205 | 
 206 | %foreign "scheme:blodwen-buffer-getint32"
 207 |          "RefC:getBufferInt32LE"
 208 |          "node:lambda:(buf,offset)=>buf.readInt32LE(offset)"
 209 | prim__getInt32 : Buffer -> (offset : Int) -> PrimIO Int32
 210 | 
 211 | export %inline
 212 | getInt32 : HasIO io => Buffer -> (offset : Int) -> io Int32
 213 | getInt32 buf offset
 214 |     = primIO (prim__getInt32 buf offset)
 215 | 
 216 | %foreign "scheme:blodwen-buffer-setint64"
 217 | prim__setInt64 : Buffer -> (offset : Int) -> (val : Int64) -> PrimIO ()
 218 | 
 219 | export %inline
 220 | setInt64 : HasIO io => Buffer -> (offset : Int) -> (val : Int64) -> io ()
 221 | setInt64 buf offset val
 222 |     = primIO (prim__setInt64 buf offset val)
 223 | 
 224 | %foreign "scheme:blodwen-buffer-getint64"
 225 | prim__getInt64 : Buffer -> (offset : Int) -> PrimIO Int64
 226 | 
 227 | export %inline
 228 | getInt64 : HasIO io => Buffer -> (offset : Int) -> io Int64
 229 | getInt64 buf offset
 230 |     = primIO (prim__getInt64 buf offset)
 231 | 
 232 | ------------------------------------------------------------------------
 233 | -- Int (backend-dependent: 64 on scheme, refc, and 32 on js)
 234 | 
 235 | %foreign "scheme:blodwen-buffer-setint"
 236 |          "RefC:setBufferInt64LE"
 237 |          "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
 238 | prim__setInt : Buffer -> (offset : Int) -> (val : Int) -> PrimIO ()
 239 | 
 240 | export %inline
 241 | setInt : HasIO io => Buffer -> (offset : Int) -> (val : Int) -> io ()
 242 | setInt buf offset val
 243 |     = primIO (prim__setInt buf offset val)
 244 | 
 245 | %foreign "scheme:blodwen-buffer-getint"
 246 |          "RefC:getBufferInt64LE"
 247 |          "node:lambda:(buf,offset)=>buf.readInt32LE(offset)"
 248 | prim__getInt : Buffer -> (offset : Int) -> PrimIO Int
 249 | 
 250 | export %inline
 251 | getInt : HasIO io => Buffer -> (offset : Int) -> io Int
 252 | getInt buf offset
 253 |     = primIO (prim__getInt buf offset)
 254 | 
 255 | ------------------------------------------------------------------------
 256 | -- Double
 257 | 
 258 | %foreign "scheme:blodwen-buffer-setdouble"
 259 |          "RefC:setBufferDouble"
 260 |          "node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, offset)"
 261 | prim__setDouble : Buffer -> (offset : Int) -> (val : Double) -> PrimIO ()
 262 | 
 263 | export %inline
 264 | setDouble : HasIO io => Buffer -> (offset : Int) -> (val : Double) -> io ()
 265 | setDouble buf offset val
 266 |     = primIO (prim__setDouble buf offset val)
 267 | 
 268 | %foreign "scheme:blodwen-buffer-getdouble"
 269 |          "RefC:getBufferDouble"
 270 |          "node:lambda:(buf,offset)=>buf.readDoubleLE(offset)"
 271 | prim__getDouble : Buffer -> (offset : Int) -> PrimIO Double
 272 | 
 273 | export %inline
 274 | getDouble : HasIO io => Buffer -> (offset : Int) -> io Double
 275 | getDouble buf offset
 276 |     = primIO (prim__getDouble buf offset)
 277 | 
 278 | ------------------------------------------------------------------------
 279 | -- Bool
 280 | 
 281 | export
 282 | setBool : HasIO io => Buffer -> (offset : Int) -> (val : Bool) -> io ()
 283 | setBool buf offset val = setBits8 buf offset (ifThenElse val 0 1)
 284 | 
 285 | export
 286 | getBool : HasIO io => Buffer -> (offset : Int) -> io Bool
 287 | getBool buf offset = (0 ==) <$> getBits8 buf offset
 288 | 
 289 | ------------------------------------------------------------------------
 290 | -- Arbitrary precision nums
 291 | 
 292 | ||| setNat returns the end offset
 293 | export
 294 | setNat : HasIO io => Buffer -> (offset : Int) -> (val : Nat) -> io Int
 295 | setNat buf offset val
 296 |   = do let limbs = toLimbs (cast val)
 297 |        let len = foldl (const . (1+)) 0 limbs -- tail recursive length
 298 |        setInt64 buf offset len
 299 |        setLimbs (offset + 8) limbs
 300 | 
 301 |   where
 302 | 
 303 |   toLimbs : Integer -> List Bits32
 304 |   toLimbs 0 = []
 305 |   toLimbs (-1) = [-1]
 306 |   toLimbs x = fromInteger (prim__and_Integer x 0xffffffff) ::
 307 |               toLimbs (assert_smaller x (prim__shr_Integer x 32))
 308 | 
 309 |   setLimbs : (offset : Int) -> List Bits32 -> io Int
 310 |   setLimbs offset [] = pure offset
 311 |   setLimbs offset (limb :: limbs)
 312 |     = do setBits32 buf offset limb
 313 |          setLimbs (offset + 4) limbs
 314 | 
 315 | ||| getNat returns the end offset
 316 | export
 317 | getNat : HasIO io => Buffer -> (offset : Int) -> io (Int, Nat)
 318 | getNat buf offset
 319 |   = do len <- getInt64 buf offset
 320 |        when (len < 0) $ assert_total $ idris_crash "INTERNAL ERROR: getNat -> corrupt Nat"
 321 |        limbs <- getLimbs [<] (offset + 8) len
 322 |        pure (offset + 8 + 4 * cast len, cast $ fromLimbs limbs)
 323 | 
 324 |   where
 325 | 
 326 |   fromLimbs : List Bits32 -> Integer
 327 |   fromLimbs [] = 0
 328 |   fromLimbs (x :: xs) = cast x + prim__shl_Integer (fromLimbs xs) 32
 329 | 
 330 |   getLimbs : SnocList Bits32 -> (offset : Int) -> (len : Int64) -> io (List Bits32)
 331 |   getLimbs acc offset 0 = pure (acc <>> [])
 332 |   getLimbs acc offset len
 333 |     = do limb <- getBits32 buf offset
 334 |          getLimbs (acc :< limb) (offset + 4) (assert_smaller len (len -1))
 335 | 
 336 | ||| setInteger returns the end offset
 337 | export
 338 | setInteger : HasIO io => Buffer -> (offset : Int) -> (val : Integer) -> io Int
 339 | setInteger buf offset val = if val < 0
 340 |   then do setBool buf offset True
 341 |           setNat buf (offset + 1) (cast (- val))
 342 |   else do setBool buf offset False
 343 |           setNat buf (offset + 1) (cast val)
 344 | 
 345 | ||| getInteger returns the end offset
 346 | export
 347 | getInteger : HasIO io => Buffer -> (offset : Int) -> io (Int, Integer)
 348 | getInteger buf offset
 349 |   = do b <- getBool buf offset
 350 |        map (ifThenElse b negate id . cast) <$> getNat buf (offset + 1)
 351 | 
 352 | ------------------------------------------------------------------------
 353 | -- String
 354 | 
 355 | -- Get the length of a string in bytes, rather than characters
 356 | export
 357 | %foreign "scheme:blodwen-stringbytelen"
 358 |          "C:strlen, libc 6"
 359 |          "javascript:lambda:(string)=>new TextEncoder().encode(string).length"
 360 | stringByteLength : String -> Int
 361 | 
 362 | %foreign "scheme:blodwen-buffer-setstring"
 363 |          "RefC:setBufferString"
 364 |          "node:lambda:(buf,offset,value)=>buf.write(value, offset,buf.length - offset, 'utf-8')"
 365 | prim__setString : Buffer -> (offset : Int) -> (val : String) -> PrimIO ()
 366 | 
 367 | export %inline
 368 | setString : HasIO io => Buffer -> (offset : Int) -> (val : String) -> io ()
 369 | setString buf offset val
 370 |     = primIO (prim__setString buf offset val)
 371 | 
 372 | %foreign "scheme:blodwen-buffer-getstring"
 373 |          "RefC:getBufferString"
 374 |          "node:lambda:(buf,offset,len)=>buf.slice(offset, offset+len).toString('utf-8')"
 375 | prim__getString : Buffer -> (offset : Int) -> (len : Int) -> PrimIO String
 376 | 
 377 | export %inline
 378 | getString : HasIO io => Buffer -> (offset : Int) -> (len : Int) -> io String
 379 | getString buf offset len
 380 |     = primIO (prim__getString buf offset len)
 381 | 
 382 | ||| Use `bufferData'` instead, as its value is correctly limited.
 383 | %deprecate
 384 | export
 385 | covering
 386 | bufferData : HasIO io => Buffer -> io (List Int)
 387 | bufferData buf
 388 |     = do len <- rawSize buf
 389 |          unpackTo [] len
 390 |   where
 391 |     covering
 392 |     unpackTo : List Int -> Int -> io (List Int)
 393 |     unpackTo acc 0 = pure acc
 394 |     unpackTo acc offset
 395 |         = do val <- getBits8 buf (offset - 1)
 396 |              unpackTo (cast val :: acc) (offset - 1)
 397 | 
 398 | ||| This function performs the same task as `bufferData` but it
 399 | ||| returns `List Bits8` which is more correct than `List Int`.
 400 | export
 401 | covering
 402 | bufferData' : HasIO io => Buffer -> io (List Bits8)
 403 | bufferData' buf
 404 |     = do len <- rawSize buf
 405 |          unpackTo [] len
 406 |   where
 407 |     covering
 408 |     unpackTo : List Bits8 -> Int -> io (List Bits8)
 409 |     unpackTo acc 0 = pure acc
 410 |     unpackTo acc offset
 411 |         = do val <- getBits8 buf (offset - 1)
 412 |              unpackTo (val :: acc) (offset - 1)
 413 | 
 414 | 
 415 | %foreign "scheme:blodwen-buffer-copydata"
 416 |          "RefC:copyBuffer"
 417 |          "node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,o2,o1,o1+length)"
 418 | prim__copyData : (src : Buffer) -> (srcOffset, len : Int) ->
 419 |                  (dst : Buffer) -> (dstOffset : Int) -> PrimIO ()
 420 | 
 421 | export
 422 | copyData : HasIO io => Buffer -> (srcOffset, len : Int) ->
 423 |            (dst : Buffer) -> (dstOffset : Int) -> io ()
 424 | copyData src start len dest offset
 425 |     = primIO (prim__copyData src start len dest offset)
 426 | 
 427 | export
 428 | resizeBuffer : HasIO io => Buffer -> Int -> io (Maybe Buffer)
 429 | resizeBuffer old newsize
 430 |     = do Just buf <- newBuffer newsize
 431 |               | Nothing => pure Nothing
 432 |          -- If the new buffer is smaller than the old one, just copy what
 433 |          -- fits
 434 |          oldsize <- rawSize old
 435 |          let len = if newsize < oldsize then newsize else oldsize
 436 |          copyData old 0 len buf 0
 437 |          pure (Just buf)
 438 | 
 439 | ||| Create a buffer containing the concatenated content from a
 440 | ||| list of buffers.
 441 | export
 442 | concatBuffers : HasIO io => List Buffer -> io (Maybe Buffer)
 443 | concatBuffers xs
 444 |     = do let sizes = map prim__bufferSize xs
 445 |          let (totalSize, revCumulative) = foldl scanSize (0,[]) sizes
 446 |          let cumulative = reverse revCumulative
 447 |          Just buf <- newBuffer totalSize
 448 |               | Nothing => pure Nothing
 449 |          traverse_ (\(b, size, watermark) => copyData b 0 size buf watermark) (zip3 xs sizes cumulative)
 450 |          pure (Just buf)
 451 |     where
 452 |         scanSize : (Int, List Int) -> Int -> (Int, List Int)
 453 |         scanSize (s, cs) x  = (s+x, s::cs)
 454 | 
 455 | ||| Split a buffer into two at a position.
 456 | export
 457 | splitBuffer : HasIO io => Buffer -> Int -> io (Maybe (Buffer, Buffer))
 458 | splitBuffer buf pos = do size <- rawSize buf
 459 |                          if pos > 0 && pos < size
 460 |                              then do Just first <- newBuffer pos
 461 |                                         | Nothing => pure Nothing
 462 |                                      Just second <- newBuffer (size - pos)
 463 |                                         | Nothing => pure Nothing
 464 |                                      copyData buf 0 pos first 0
 465 |                                      copyData buf pos (size-pos) second 0
 466 |                                      pure $ Just (first, second)
 467 |                              else pure Nothing
 468 |