@@ -0,0 +1,119 @@
3+%include C "idris_buffer.h"
5+||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory
9+ ||| Raw bytes, as a pointer to a block of memory
10+ rawdata : ManagedPtr -- let Idris run time manage the memory
11+ ||| Cached size of block
13+ ||| Next location to read/write (e.g. when reading from file)
16+||| Create a new buffer 'size' bytes long. Returns 'Nothing' if allocation
19+newBuffer : (size : Int) -> IO (Maybe Buffer)
20+newBuffer size = do bptr <- foreign FFI_C "idris_newBuffer" (Int -> IO Ptr)
23+ if bad then pure Nothing
24+ else pure (Just (MkBuffer (prim__registerPtr bptr (size + 8)) size 0))
26+||| Reset the 'next location' pointer of the buffer to 0.
27+||| The 'next location' pointer gives the location for the next file read/write
28+||| so resetting this means you can write it again
30+resetBuffer : Buffer -> Buffer
31+resetBuffer buf = record { location = 0 } buf
33+||| Return the space available in the buffer
35+rawSize : Buffer -> IO Int
36+rawSize b = foreign FFI_C "idris_getBufferSize" (ManagedPtr -> IO Int) (rawdata b)
42+||| Set the byte at position 'loc' to 'val'.
43+||| Does nothing if the location is outside the bounds of the buffer
45+setByte : Buffer -> (loc : Int) -> (val : Bits8) -> IO ()
47+ = foreign FFI_C "idris_setBufferByte" (ManagedPtr -> Int -> Bits8 -> IO ())
50+||| Set the byte at position 'loc' to 'val'.
51+||| Does nothing if the location is out of bounds of the buffer, or the string
52+||| is too long for the location
54+setString : Buffer -> Int -> String -> IO ()
56+ = foreign FFI_C "idris_setBufferString" (ManagedPtr -> Int -> String -> IO ())
59+||| Copy data from 'src' to 'dest'. Reads 'len' bytes starting at position
60+||| 'start' in 'src', and writes them starting at position 'loc' in 'dest'.
61+||| Does nothing if a location is out of bounds, or there is not enough room
63+copyData : (src : Buffer) -> (start, len : Int) ->
64+ (dest : Buffer) -> (loc : Int) -> IO ()
65+copyData src start len dest loc
66+ = foreign FFI_C "idris_copyBuffer" (ManagedPtr -> Int -> Int -> ManagedPtr -> Int -> IO ())
67+ (rawdata src) start len (rawdata dest) loc
69+||| Return the value at the given location in the buffer
71+getByte : Buffer -> (loc : Int) -> IO Bits8
73+ = foreign FFI_C "idris_getBufferByte" (ManagedPtr -> Int -> IO Bits8)
76+||| Read 'maxbytes' into the buffer from a file, returning a new
77+||| buffer with the 'locaton' pointer moved along
79+readBufferFromFile : File -> Buffer -> (maxbytes : Int) -> IO Buffer
80+readBufferFromFile (FHandle h) buf max
81+ = do numread <- foreign FFI_C "idris_readBuffer" (Ptr -> ManagedPtr -> Int -> Int -> IO Int)
82+ h (rawdata buf) (location buf) max
83+ pure (record { location $= (+numread) } buf)
85+||| Write 'maxbytes' from the buffer from a file, returning a new
86+||| buffer with the 'locaton' pointer moved along
88+writeBufferToFile : File -> Buffer -> (maxbytes : Int) -> IO Buffer
89+writeBufferToFile (FHandle h) buf max
90+ = do let maxwrite = size buf - location buf
91+ let max' = if maxwrite < max then maxwrite else max
92+ foreign FFI_C "idris_writeBuffer" (Ptr -> ManagedPtr -> Int -> Int -> IO ())
93+ h (rawdata buf) (location buf) max'
94+ pure (record { location $= (+max') } buf)
96+||| Return the contents of the buffer as a list
98+bufferData : Buffer -> IO (List Bits8)
99+bufferData b = do let len = size b
101+ where unpackTo : List Bits8 -> Int -> IO (List Bits8)
102+ unpackTo acc 0 = pure acc
103+ unpackTo acc loc = do val <- getByte b (loc - 1)
104+ unpackTo (val :: acc)
105+ (assert_smaller loc (loc - 1))
107+||| Create a new buffer, copying the contents of the old buffer to the new.
108+||| Returns 'Nothing' if resizing fails
110+resizeBuffer : Buffer -> Int -> IO (Maybe Buffer)
111+resizeBuffer old newsize
112+ = do Just buf <- newBuffer newsize
113+ | Nothing => pure Nothing
114+ -- If the new buffer is smaller than the old one, just copy what
116+ let oldsize = size old
117+ let len = if newsize < oldsize then newsize else oldsize
118+ copyData old 0 len buf 0