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)