@@ -0,0 +1,119 @@
1+module Data.Buffer
2+
3+%include C "idris_buffer.h"
4+
5+||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory
6+export
7+record Buffer where
8+ constructor MkBuffer
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
12+ buf_size : Int
13+ ||| Next location to read/write (e.g. when reading from file)
14+ location : Int
15+
16+||| Create a new buffer 'size' bytes long. Returns 'Nothing' if allocation
17+||| fails
18+export
19+newBuffer : (size : Int) -> IO (Maybe Buffer)
20+newBuffer size = do bptr <- foreign FFI_C "idris_newBuffer" (Int -> IO Ptr)
21+ size
22+ bad <- nullPtr bptr
23+ if bad then pure Nothing
24+ else pure (Just (MkBuffer (prim__registerPtr bptr (size + 8)) size 0))
25+
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
29+export
30+resetBuffer : Buffer -> Buffer
31+resetBuffer buf = record { location = 0 } buf
32+
33+||| Return the space available in the buffer
34+export
35+rawSize : Buffer -> IO Int
36+rawSize b = foreign FFI_C "idris_getBufferSize" (ManagedPtr -> IO Int) (rawdata b)
37+
38+export
39+size : Buffer -> Int
40+size b = buf_size b
41+
42+||| Set the byte at position 'loc' to 'val'.
43+||| Does nothing if the location is outside the bounds of the buffer
44+export
45+setByte : Buffer -> (loc : Int) -> (val : Bits8) -> IO ()
46+setByte b loc val
47+ = foreign FFI_C "idris_setBufferByte" (ManagedPtr -> Int -> Bits8 -> IO ())
48+ (rawdata b) loc val
49+
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
53+export
54+setString : Buffer -> Int -> String -> IO ()
55+setString b loc val
56+ = foreign FFI_C "idris_setBufferString" (ManagedPtr -> Int -> String -> IO ())
57+ (rawdata b) loc val
58+
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
62+export
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
68+
69+||| Return the value at the given location in the buffer
70+export
71+getByte : Buffer -> (loc : Int) -> IO Bits8
72+getByte b loc
73+ = foreign FFI_C "idris_getBufferByte" (ManagedPtr -> Int -> IO Bits8)
74+ (rawdata b) loc
75+
76+||| Read 'maxbytes' into the buffer from a file, returning a new
77+||| buffer with the 'locaton' pointer moved along
78+export
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)
84+
85+||| Write 'maxbytes' from the buffer from a file, returning a new
86+||| buffer with the 'locaton' pointer moved along
87+export
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)
95+
96+||| Return the contents of the buffer as a list
97+export
98+bufferData : Buffer -> IO (List Bits8)
99+bufferData b = do let len = size b
100+ unpackTo [] len
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))
106+
107+||| Create a new buffer, copying the contents of the old buffer to the new.
108+||| Returns 'Nothing' if resizing fails
109+export
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
115+ -- fits
116+ let oldsize = size old
117+ let len = if newsize < oldsize then newsize else oldsize
118+ copyData old 0 len buf 0
119+ pure (Just buf)