Idris2/libs/base/Data/Buffer.idr

345 lines
12 KiB
Idris
Raw Normal View History

2020-05-18 15:59:07 +03:00
module Data.Buffer
import System.Directory
2020-05-18 15:59:07 +03:00
import System.File
import Data.List
%default total
-- Reading and writing binary buffers. Note that this primitives are unsafe,
-- in that they don't check that buffer locations are within bounds.
-- We really need a safe wrapper!
-- They are used in the Idris compiler itself for reading/writing checked
-- files.
-- This is known to the compiler, so maybe ought to be moved to Builtin
2020-05-18 15:59:07 +03:00
export
data Buffer : Type where [external]
2020-06-18 01:29:54 +03:00
%foreign "scheme:blodwen-buffer-size"
"RefC:getBufferSize"
"node:lambda:b => b.length"
2020-05-18 15:59:07 +03:00
prim__bufferSize : Buffer -> Int
export %inline
2020-07-01 23:55:14 +03:00
rawSize : HasIO io => Buffer -> io Int
2020-05-18 15:59:07 +03:00
rawSize buf = pure (prim__bufferSize buf)
%foreign "scheme:blodwen-new-buffer"
"RefC:newBuffer"
"node:lambda:s=>Buffer.alloc(s)"
2020-05-18 15:59:07 +03:00
prim__newBuffer : Int -> PrimIO Buffer
export
2020-07-01 23:55:14 +03:00
newBuffer : HasIO io => Int -> io (Maybe Buffer)
2020-05-18 15:59:07 +03:00
newBuffer size
= if size >= 0
then do buf <- primIO (prim__newBuffer size)
pure $ Just buf
else pure Nothing
2020-05-18 15:59:07 +03:00
-- if prim__nullAnyPtr buf /= 0
-- then pure Nothing
-- else pure $ Just $ MkBuffer buf size 0
%foreign "scheme:blodwen-buffer-setbyte"
"RefC:setBufferByte"
"node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)"
2020-05-18 15:59:07 +03:00
prim__setByte : Buffer -> Int -> Int -> PrimIO ()
2020-06-18 01:29:54 +03:00
%foreign "scheme:blodwen-buffer-setbyte"
"RefC:setBufferByte"
"node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)"
prim__setBits8 : Buffer -> Int -> Bits8 -> PrimIO ()
2020-05-18 15:59:07 +03:00
-- Assumes val is in the range 0-255
export %inline
2020-07-01 23:55:14 +03:00
setByte : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
2020-05-18 15:59:07 +03:00
setByte buf loc val
= primIO (prim__setByte buf loc val)
export %inline
2020-07-01 23:55:14 +03:00
setBits8 : HasIO io => Buffer -> (loc : Int) -> (val : Bits8) -> io ()
setBits8 buf loc val
= primIO (prim__setBits8 buf loc val)
2020-05-18 15:59:07 +03:00
%foreign "scheme:blodwen-buffer-getbyte"
"RefC:getBufferByte"
"node:lambda:(buf,offset)=>buf.readUInt8(offset)"
2020-05-18 15:59:07 +03:00
prim__getByte : Buffer -> Int -> PrimIO Int
2020-06-18 01:29:54 +03:00
%foreign "scheme:blodwen-buffer-getbyte"
"RefC:getBufferByte"
"node:lambda:(buf,offset)=>buf.readUInt8(offset)"
prim__getBits8 : Buffer -> Int -> PrimIO Bits8
2020-05-18 15:59:07 +03:00
export %inline
2020-07-01 23:55:14 +03:00
getByte : HasIO io => Buffer -> (loc : Int) -> io Int
2020-05-18 15:59:07 +03:00
getByte buf loc
= primIO (prim__getByte buf loc)
export %inline
2020-07-01 23:55:14 +03:00
getBits8 : HasIO io => Buffer -> (loc : Int) -> io Bits8
getBits8 buf loc
= primIO (prim__getBits8 buf loc)
%foreign "scheme:blodwen-buffer-setbits16"
"node:lambda:(buf,offset,value)=>buf.writeUInt16LE(value, offset)"
prim__setBits16 : Buffer -> Int -> Bits16 -> PrimIO ()
export %inline
2020-07-01 23:55:14 +03:00
setBits16 : HasIO io => Buffer -> (loc : Int) -> (val : Bits16) -> io ()
setBits16 buf loc val
= primIO (prim__setBits16 buf loc val)
%foreign "scheme:blodwen-buffer-getbits16"
"node:lambda:(buf,offset)=>buf.readUInt16LE(offset)"
prim__getBits16 : Buffer -> Int -> PrimIO Bits16
export %inline
2020-07-01 23:55:14 +03:00
getBits16 : HasIO io => Buffer -> (loc : Int) -> io Bits16
getBits16 buf loc
= primIO (prim__getBits16 buf loc)
%foreign "scheme:blodwen-buffer-setbits32"
"node:lambda:(buf,offset,value)=>buf.writeUInt32LE(value, offset)"
prim__setBits32 : Buffer -> Int -> Bits32 -> PrimIO ()
export %inline
2020-07-01 23:55:14 +03:00
setBits32 : HasIO io => Buffer -> (loc : Int) -> (val : Bits32) -> io ()
setBits32 buf loc val
= primIO (prim__setBits32 buf loc val)
%foreign "scheme:blodwen-buffer-getbits32"
"node:lambda:(buf,offset)=>buf.readUInt32LE(offset)"
prim__getBits32 : Buffer -> Int -> PrimIO Bits32
export %inline
2020-07-01 23:55:14 +03:00
getBits32 : HasIO io => Buffer -> (loc : Int) -> io Bits32
getBits32 buf loc
= primIO (prim__getBits32 buf loc)
%foreign "scheme:blodwen-buffer-setbits64"
prim__setBits64 : Buffer -> Int -> Bits64 -> PrimIO ()
export %inline
2020-07-01 23:55:14 +03:00
setBits64 : HasIO io => Buffer -> (loc : Int) -> (val : Bits64) -> io ()
setBits64 buf loc val
= primIO (prim__setBits64 buf loc val)
%foreign "scheme:blodwen-buffer-getbits64"
prim__getBits64 : Buffer -> Int -> PrimIO Bits64
export %inline
2020-07-01 23:55:14 +03:00
getBits64 : HasIO io => Buffer -> (loc : Int) -> io Bits64
getBits64 buf loc
= primIO (prim__getBits64 buf loc)
2020-05-19 19:03:18 +03:00
%foreign "scheme:blodwen-buffer-setint32"
"node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
2020-05-19 19:03:18 +03:00
prim__setInt32 : Buffer -> Int -> Int -> PrimIO ()
export %inline
2020-07-01 23:55:14 +03:00
setInt32 : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
2020-05-19 19:03:18 +03:00
setInt32 buf loc val
= primIO (prim__setInt32 buf loc val)
%foreign "scheme:blodwen-buffer-getint32"
"node:lambda:(buf,offset)=>buf.readInt32LE(offset)"
2020-05-19 19:03:18 +03:00
prim__getInt32 : Buffer -> Int -> PrimIO Int
export %inline
2020-07-01 23:55:14 +03:00
getInt32 : HasIO io => Buffer -> (loc : Int) -> io Int
2020-05-19 19:03:18 +03:00
getInt32 buf loc
= primIO (prim__getInt32 buf loc)
2020-05-18 15:59:07 +03:00
%foreign "scheme:blodwen-buffer-setint"
"RefC:setBufferInt"
"node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
2020-05-18 15:59:07 +03:00
prim__setInt : Buffer -> Int -> Int -> PrimIO ()
export %inline
2020-07-01 23:55:14 +03:00
setInt : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
2020-05-18 15:59:07 +03:00
setInt buf loc val
= primIO (prim__setInt buf loc val)
%foreign "scheme:blodwen-buffer-getint"
"RefC:getBufferInt"
"node:lambda:(buf,offset)=>buf.readInt32LE(offset)"
2020-05-18 15:59:07 +03:00
prim__getInt : Buffer -> Int -> PrimIO Int
export %inline
2020-07-01 23:55:14 +03:00
getInt : HasIO io => Buffer -> (loc : Int) -> io Int
2020-05-18 15:59:07 +03:00
getInt buf loc
= primIO (prim__getInt buf loc)
%foreign "scheme:blodwen-buffer-setdouble"
"RefC:setBufferDouble"
"node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, offset)"
2020-05-18 15:59:07 +03:00
prim__setDouble : Buffer -> Int -> Double -> PrimIO ()
export %inline
2020-07-01 23:55:14 +03:00
setDouble : HasIO io => Buffer -> (loc : Int) -> (val : Double) -> io ()
2020-05-18 15:59:07 +03:00
setDouble buf loc val
= primIO (prim__setDouble buf loc val)
%foreign "scheme:blodwen-buffer-getdouble"
"RefC:getBufferDouble"
"node:lambda:(buf,offset)=>buf.readDoubleLE(offset)"
2020-05-18 15:59:07 +03:00
prim__getDouble : Buffer -> Int -> PrimIO Double
export %inline
2020-07-01 23:55:14 +03:00
getDouble : HasIO io => Buffer -> (loc : Int) -> io Double
2020-05-18 15:59:07 +03:00
getDouble buf loc
= primIO (prim__getDouble buf loc)
-- Get the length of a string in bytes, rather than characters
export
%foreign "scheme:blodwen-stringbytelen"
"C:strlen, libc 6"
2020-05-18 15:59:07 +03:00
stringByteLength : String -> Int
%foreign "scheme:blodwen-buffer-setstring"
"RefC:setBufferString"
"node:lambda:(buf,offset,value)=>buf.write(value, offset,buf.length - offset, 'utf-8')"
2020-05-18 15:59:07 +03:00
prim__setString : Buffer -> Int -> String -> PrimIO ()
export %inline
2020-07-01 23:55:14 +03:00
setString : HasIO io => Buffer -> (loc : Int) -> (val : String) -> io ()
2020-05-18 15:59:07 +03:00
setString buf loc val
= primIO (prim__setString buf loc val)
%foreign "scheme:blodwen-buffer-getstring"
"RefC:getBufferString"
"node:lambda:(buf,offset,len)=>buf.slice(offset, offset+len).toString('utf-8')"
2020-05-18 15:59:07 +03:00
prim__getString : Buffer -> Int -> Int -> PrimIO String
export %inline
2020-07-01 23:55:14 +03:00
getString : HasIO io => Buffer -> (loc : Int) -> (len : Int) -> io String
2020-05-18 15:59:07 +03:00
getString buf loc len
= primIO (prim__getString buf loc len)
export
covering
2020-07-01 23:55:14 +03:00
bufferData : HasIO io => Buffer -> io (List Int)
2020-05-18 15:59:07 +03:00
bufferData buf
= do len <- rawSize buf
unpackTo [] len
where
covering
2020-07-01 23:55:14 +03:00
unpackTo : List Int -> Int -> io (List Int)
2020-05-18 15:59:07 +03:00
unpackTo acc 0 = pure acc
unpackTo acc loc
= do val <- getByte buf (loc - 1)
unpackTo (val :: acc) (loc - 1)
2020-07-01 23:55:14 +03:00
2020-05-18 15:59:07 +03:00
%foreign "scheme:blodwen-buffer-copydata"
"RefC:copyBuffer"
"node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,o2,o1,o1+length)"
2020-05-18 15:59:07 +03:00
prim__copyData : Buffer -> Int -> Int -> Buffer -> Int -> PrimIO ()
export
2020-07-01 23:55:14 +03:00
copyData : HasIO io => (src : Buffer) -> (start, len : Int) ->
(dest : Buffer) -> (loc : Int) -> io ()
2020-05-18 15:59:07 +03:00
copyData src start len dest loc
= primIO (prim__copyData src start len dest loc)
%foreign "C:idris2_readBufferData, libidris2_support, idris_file.h"
"node:lambda:(f,b,l,m) => require('fs').readSync(f.fd,b,l,m)"
prim__readBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
2020-06-18 01:29:54 +03:00
%foreign "C:idris2_writeBufferData, libidris2_support, idris_file.h"
"node:lambda:(f,b,l,m) => require('fs').writeSync(f.fd,b,l,m)"
prim__writeBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
2020-05-18 15:59:07 +03:00
export
2020-07-01 23:55:14 +03:00
readBufferData : HasIO io => File -> Buffer ->
(loc : Int) -> -- position in buffer to start adding
(maxbytes : Int) -> -- maximums size to read, which must not
-- exceed buffer length
2020-07-01 23:55:14 +03:00
io (Either FileError ())
readBufferData (FHandle h) buf loc max
= do read <- primIO (prim__readBufferData h buf loc max)
if read >= 0
then pure (Right ())
else pure (Left FileReadError)
2020-05-18 15:59:07 +03:00
export
2020-07-01 23:55:14 +03:00
writeBufferData : HasIO io => File -> Buffer ->
(loc : Int) -> -- position in buffer to write from
(maxbytes : Int) -> -- maximums size to write, which must not
-- exceed buffer length
2020-07-01 23:55:14 +03:00
io (Either FileError ())
writeBufferData (FHandle h) buf loc max
= do written <- primIO (prim__writeBufferData h buf loc max)
if written >= 0
then pure (Right ())
else pure (Left FileWriteError)
2020-05-18 15:59:07 +03:00
export
2020-07-01 23:55:14 +03:00
writeBufferToFile : HasIO io => String -> Buffer -> Int -> io (Either FileError ())
2020-05-18 15:59:07 +03:00
writeBufferToFile fn buf max
= do Right f <- openFile fn WriteTruncate
| Left err => pure (Left err)
Right ok <- writeBufferData f buf 0 max
| Left err => pure (Left err)
closeFile f
pure (Right ok)
export
2020-07-01 23:55:14 +03:00
createBufferFromFile : HasIO io => String -> io (Either FileError Buffer)
createBufferFromFile fn
= do Right f <- openFile fn Read
| Left err => pure (Left err)
Right size <- fileSize f
| Left err => pure (Left err)
Just buf <- newBuffer size
| Nothing => pure (Left FileReadError)
Right ok <- readBufferData f buf 0 size
| Left err => pure (Left err)
closeFile f
pure (Right buf)
2020-05-18 15:59:07 +03:00
export
2020-07-01 23:55:14 +03:00
resizeBuffer : HasIO io => Buffer -> Int -> io (Maybe Buffer)
2020-05-18 15:59:07 +03:00
resizeBuffer old newsize
= do Just buf <- newBuffer newsize
| Nothing => pure Nothing
-- If the new buffer is smaller than the old one, just copy what
-- fits
oldsize <- rawSize old
let len = if newsize < oldsize then newsize else oldsize
copyData old 0 len buf 0
pure (Just buf)
||| Create a buffer containing the concatenated content from a
||| list of buffers.
export
concatBuffers : HasIO io => List Buffer -> io (Maybe Buffer)
concatBuffers xs
= do let sizes = map prim__bufferSize xs
let (totalSize, revCumulative) = foldl scanSize (0,[]) sizes
let cumulative = reverse revCumulative
Just buf <- newBuffer totalSize
| Nothing => pure Nothing
traverse_ (\(b, size, watermark) => copyData b 0 size buf watermark) (zip3 xs sizes cumulative)
pure (Just buf)
where
scanSize : (Int, List Int) -> Int -> (Int, List Int)
scanSize (s, cs) x = (s+x, s::cs)
||| Split a buffer into two at a position.
export
splitBuffer : HasIO io => Buffer -> Int -> io (Maybe (Buffer, Buffer))
splitBuffer buf pos = do size <- rawSize buf
if pos > 0 && pos < size
then do Just first <- newBuffer pos
| Nothing => pure Nothing
Just second <- newBuffer (size - pos)
| Nothing => pure Nothing
copyData buf 0 pos first 0
copyData buf pos (size-pos) second 0
pure $ Just (first, second)
else pure Nothing