
  0 | module Libraries.Utils.Binary
  1 | 
  2 | import Data.Buffer
  3 | 
  4 | import System.File
  5 | 
  6 | -- Serialising data as binary. Provides an interface TTC which allows
  7 | -- reading and writing to chunks of memory, "Binary", which can be written
  8 | -- to and read from files.
  9 | 
 10 | %default covering
 11 | 
 12 | public export
 13 | record Binary where
 14 |   constructor MkBin
 15 |   buf : Buffer
 16 |   loc : Integer
 17 |   size : Integer -- Capacity
 18 |   used : Integer -- Amount used
 19 | 
 20 | export
 21 | newBinary : Buffer -> Integer -> Binary
 22 | newBinary b s = MkBin b 0 s 0
 23 | 
 24 | %inline export
 25 | blockSize : Int
 26 | blockSize = 655360
 27 | 
 28 | export
 29 | avail : Binary -> Integer
 30 | avail c = (size c - loc c) - 1
 31 | 
 32 | export
 33 | toRead : Binary -> Integer
 34 | toRead c = used c - loc c
 35 | 
 36 | export
 37 | appended : Integer -> Binary -> Binary
 38 | appended i (MkBin b loc s used) = MkBin b (loc+i) s (used + i)
 39 | 
 40 | export
 41 | incLoc : Integer -> Binary -> Binary
 42 | incLoc i c = { loc $= (+i) } c
 43 | 
 44 | export
 45 | dumpBin : Binary -> IO ()
 46 | dumpBin chunk
 47 |    = do -- printLn !(traverse bufferData' (map buf done))
 48 |         printLn !(bufferData' (buf chunk))
 49 |         -- printLn !(traverse bufferData' (map buf rest))
 50 | 
 51 | export
 52 | fromBuffer : Buffer -> IO Binary
 53 | fromBuffer buf
 54 |     = do len <- rawSize buf
 55 |          let len = cast len
 56 |          pure (MkBin buf 0 len len)
 57 | 
 58 | export
 59 | writeToFile : (fname : String) -> Binary -> IO (Either FileError ())
 60 | writeToFile fname c
 61 |     = do Right ok <- writeBufferToFile fname (buf c) (cast $ used c)
 62 |                | Left (err, size) => pure (Left err)
 63 |          pure (Right ok)
 64 | 
 65 | export
 66 | readFromFile : (fname : String) -> IO (Either FileError Binary)
 67 | readFromFile fname
 68 |     = do Right b <- createBufferFromFile fname
 69 |                | Left err => pure (Left err)
 70 |          bsize <- rawSize b
 71 |          let bsize = cast bsize
 72 |          pure (Right (MkBin b 0 bsize bsize))
 73 |