IdrisDoc: Data.Buffer

Data.Buffer

writeBufferToFile : File -> Buffer -> (maxbytes : Int) -> IO Buffer

Write 'maxbytes' from the buffer from a file, returning a new
buffer with the 'locaton' pointer moved along

size : Buffer -> Int
setString : Buffer -> Int -> String -> IO ()

Set the byte at position 'loc' to 'val'.
Does nothing if the location is out of bounds of the buffer, or the string
is too long for the location

setInt : Buffer -> (loc : Int) -> (val : Int) -> IO ()

Set the int at position 'loc' to 'val'.
Uses 4 bytes (assumes up to 32 bit Int).
Does nothing if the location is outside the bounds of the buffer

setByte : Buffer -> (loc : Int) -> (val : Bits8) -> IO ()

Set the byte at position 'loc' to 'val'.
Does nothing if the location is outside the bounds of the buffer

resizeBuffer : Buffer -> Int -> IO (Maybe Buffer)

Create a new buffer, copying the contents of the old buffer to the new.
Returns 'Nothing' if resizing fails

resetBuffer : Buffer -> Buffer

Reset the 'next location' pointer of the buffer to 0.
The 'next location' pointer gives the location for the next file read/write
so resetting this means you can write it again

readBufferFromFile : File -> Buffer -> (maxbytes : Int) -> IO Buffer

Read 'maxbytes' into the buffer from a file, returning a new
buffer with the 'locaton' pointer moved along

rawSize : Buffer -> IO Int

Return the space available in the buffer

newBuffer : (size : Int) -> IO (Maybe Buffer)

Create a new buffer 'size' bytes long. Returns 'Nothing' if allocation
fails

getString : Buffer -> (loc : Int) -> (len : Int) -> IO String

Return the string at the given location in the buffer, with the given
length. Returns "" if out of bounds.

getInt : Buffer -> (loc : Int) -> IO Int

Return the value at the given location in the buffer, assuming 4
bytes to store the Int.
Returns 0 if out of bounds.

getByte : Buffer -> (loc : Int) -> IO Bits8

Return the value at the given location in the buffer.
Returns 0 if out of bounds.

copyData : (src : Buffer) -> (start : Int) -> (len : Int) -> (dest : Buffer) -> (loc : Int) -> IO ()

Copy data from 'src' to 'dest'. Reads 'len' bytes starting at position
'start' in 'src', and writes them starting at position 'loc' in 'dest'.
Does nothing if a location is out of bounds, or there is not enough room

bufferData : Buffer -> IO (List Bits8)

Return the contents of the buffer as a list

MkBuffer : (rawdata : ManagedPtr) -> (buf_size : Int) -> (location : Int) -> Buffer
rawdata

Raw bytes, as a pointer to a block of memory

buf_size

Cached size of block

location

Next location to read/write (e.g. when reading from file)

record Buffer 

A buffer is a pointer to a sized, unstructured, mutable chunk of memory.
There are primitive operations for gettng and setting bytes, ints (32 bit)
and strings at a location in the buffer. These operations silently fail
if the location is out of bounds, so bounds checking should be done in
advance.

MkBuffer : (rawdata : ManagedPtr) -> (buf_size : Int) -> (location : Int) -> Buffer
rawdata

Raw bytes, as a pointer to a block of memory

buf_size

Cached size of block

location

Next location to read/write (e.g. when reading from file)

rawdata : (rec : Buffer) -> ManagedPtr

Raw bytes, as a pointer to a block of memory

buf_size : (rec : Buffer) -> Int

Cached size of block

location : (rec : Buffer) -> Int

Next location to read/write (e.g. when reading from file)