0 | module System.File.Buffer
 1 |
 2 | import public System.File.Error
 3 | import System.File.Handle
 4 | import System.File.Meta
 5 | import System.File.Mode
 6 | import System.File.ReadWrite
 7 | import System.File.Support
 8 | import public System.File.Types
 9 |
10 | import Data.Buffer
11 |
12 | %default total
13 |
14 | %foreign supportC "idris2_readBufferData"
15 |          "node:lambda:(f,b,l,m) => require('fs').readSync(f.fd,b,l,m)"
16 | prim__readBufferData : FilePtr -> Buffer -> (offset : Int) -> (maxbytes : Int) -> PrimIO Int
17 |
18 | %foreign supportC "idris2_writeBufferData"
19 |          "node:lambda:(f,b,l,m) => require('fs').writeSync(f.fd,b,l,m)"
20 | prim__writeBufferData : FilePtr -> Buffer -> (offset : Int) -> (size : Int) -> PrimIO Int
21 |
22 | ||| Read the data from the file into the given buffer.
23 | |||
24 | ||| @ fh       the file handle to read from
25 | ||| @ buf      the buffer to read the data into
26 | ||| @ offset   the position in buffer to start adding
27 | ||| @ maxbytes the maximum size to read; must not exceed buffer length
28 | export
29 | readBufferData : HasIO io => (fh : File) -> (buf : Buffer) ->
30 |                  (offset : Int) ->
31 |                  (maxbytes : Int) ->
32 |                  io (Either FileError Int)
33 | readBufferData (FHandle h) buf offset max
34 |     = do read <- primIO (prim__readBufferData h buf offset max)
35 |          if read >= 0
36 |             then pure (Right read)
37 |             else pure (Left FileReadError)
38 |
39 | ||| Write the data from the buffer to the given `File`. Returns the number
40 | ||| of bytes that have been written upon a write error. Otherwise, it can
41 | ||| be assumed that `size` number of bytes have been written.
42 | ||| (If you do not have a `File` and just want to write to a file at a known
43 | ||| path, you probably want to use `writeBufferToFile`.)
44 | |||
45 | ||| @ fh       the file handle to write to
46 | ||| @ buf      the buffer from which to get the data to write
47 | ||| @ offset   the position in buffer to write from
48 | ||| @ size     the number of bytes to write; must not exceed buffer length
49 | export
50 | writeBufferData : HasIO io => (fh : File) -> (buf : Buffer) ->
51 |                   (offset : Int) ->
52 |                   (size : Int) ->
53 |                   io (Either (FileError, Int) ())
54 | writeBufferData (FHandle h) buf offset size
55 |     = do written <- primIO (prim__writeBufferData h buf offset size)
56 |          if written == size
57 |             then pure (Right ())
58 |             else pure (Left (FileWriteError, written))
59 |
60 | ||| Attempt to write the data from the buffer to the file at the specified file
61 | ||| name. Returns the number of bytes that have been written upon a write error.
62 | ||| Otherwise, it can be assumed that `size` number of bytes have been written.
63 | |||
64 | ||| @ fn   the file name to write to
65 | ||| @ buf  the buffer from which to get the data to write
66 | ||| @ size the number of bytes to write; must not exceed buffer length
67 | export
68 | writeBufferToFile : HasIO io => (fn : String) -> (buf : Buffer) -> (size : Int) ->
69 |                                 io (Either (FileError, Int) ())
70 | writeBufferToFile fn buf size
71 |     = do Right f <- openFile fn WriteTruncate
72 |              | Left err => pure (Left (err, 0))
73 |          Right ok <- writeBufferData f buf 0 size
74 |              | Left err => pure (Left err)
75 |          closeFile f
76 |          pure (Right ok)
77 |
78 | ||| Create a new buffer by opening a file and reading its contents into a new
79 | ||| buffer whose size matches the file size.
80 | |||
81 | ||| @ fn the name of the file to read
82 | export
83 | createBufferFromFile : HasIO io => (fn : String) -> io (Either FileError Buffer)
84 | createBufferFromFile fn
85 |     = do Right f <- openFile fn Read
86 |              | Left err => pure (Left err)
87 |          Right size <- fileSize f
88 |              | Left err => pure (Left err)
89 |          Just buf <- newBuffer size
90 |              | Nothing => pure (Left FileReadError)
91 |          Right ok <- readBufferData f buf 0 size
92 |              | Left err => pure (Left err)
93 |          closeFile f
94 |          pure (Right buf)
95 |