0 | module System.File.ReadWrite
  1 |
  2 | import public Data.Fuel
  3 |
  4 | import Data.SnocList
  5 |
  6 | import System.File.Handle
  7 | import public System.File.Error
  8 | import System.File.Support
  9 | import public System.File.Types
 10 | import System.FFI
 11 |
 12 | %default total
 13 |
 14 | %foreign supportC "idris2_seekLine"
 15 |          supportNode "seekLine"
 16 | prim__seekLine : FilePtr -> PrimIO Int
 17 |
 18 | %foreign supportC "idris2_readLine"
 19 |          supportNode "readLine"
 20 | prim__readLine : FilePtr -> PrimIO (Ptr String)
 21 |
 22 | %foreign supportC "idris2_readChars"
 23 | prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
 24 | %foreign "C:fgetc,libc 6"
 25 | prim__readChar : FilePtr -> PrimIO Int
 26 |
 27 | %foreign supportC "idris2_writeLine"
 28 |          "node:lambda:(filePtr, line) => require('fs').writeSync(filePtr.fd, line, undefined, 'utf-8')"
 29 | prim__writeLine : FilePtr -> String -> PrimIO Int
 30 |
 31 | %foreign supportC "idris2_eof"
 32 |          "node:lambda:f=>(f.eof?1:0)"
 33 | prim__eof : FilePtr -> PrimIO Int
 34 |
 35 | %foreign supportC "idris2_removeFile"
 36 |          supportNode "removeFile"
 37 | prim__removeFile : String -> PrimIO Int
 38 |
 39 | ||| Seek through the next newline.
 40 | ||| This is @fGetLine@ without the overhead of copying
 41 | ||| any characters.
 42 | |||
 43 | ||| @ h the file handle to seek through
 44 | export
 45 | covering
 46 | fSeekLine : HasIO io => (h : File) -> io (Either FileError ())
 47 | fSeekLine (FHandle f)
 48 |     = do res <- primIO (prim__seekLine f)
 49 |          if res /= 0
 50 |             then returnError
 51 |             else ok ()
 52 |
 53 |
 54 | ||| Get a garbage collected String from a Ptr String and and free the original
 55 | export
 56 | getStringAndFree : HasIO io => File -> Ptr String -> io (Either FileError String)
 57 | getStringAndFree f res
 58 |     = if prim__nullPtr res /= 0
 59 |          then if !(fileError f) then returnError else pure @{Compose} ""
 60 |          else do let s = prim__getString res
 61 |                  free $ prim__forgetPtr res
 62 |                  ok s
 63 |
 64 | ||| Get the next line from the given file handle, returning the empty string if
 65 | ||| nothing was read.
 66 | |||
 67 | ||| @ h the file handle to get the line from
 68 | export
 69 | covering
 70 | fGetLine : HasIO io => (h : File) -> io (Either FileError String)
 71 | fGetLine ff@(FHandle f)
 72 |     = do res <- primIO (prim__readLine f)
 73 |          getStringAndFree ff res
 74 |
 75 | ||| Get a number of characters from the given file handle.
 76 | |||
 77 | ||| @ h   the file handle to read from
 78 | ||| @ max the number of characters to read
 79 | export
 80 | fGetChars : HasIO io => (h : File) -> (max : Int) -> io (Either FileError String)
 81 | fGetChars ff@(FHandle f) max
 82 |     = do res <- primIO (prim__readChars max f)
 83 |          getStringAndFree ff res
 84 |
 85 | ||| Get the next character from the given file handle.
 86 | |||
 87 | ||| @ h the file handle to read from
 88 | export
 89 | fGetChar : HasIO io => (h : File) -> io (Either FileError Char)
 90 | fGetChar h@(FHandle f)
 91 |     = do c <- primIO (prim__readChar f)
 92 |          ferr <- fileError h
 93 |          if ferr
 94 |             then returnError
 95 |             else ok (cast c)
 96 |
 97 | ||| Write the given string to the file handle.
 98 | |||
 99 | ||| @ h   the file handle to write to
100 | ||| @ str the string to write
101 | export
102 | fPutStr : HasIO io => (h : File) -> (str : String) -> io (Either FileError ())
103 | fPutStr (FHandle f) str
104 |     = do res <- primIO (prim__writeLine f str)
105 |          if res == 0
106 |             then returnError
107 |             else ok ()
108 |
109 | ||| Write the given string, followed by a newline, to the file handle.
110 | |||
111 | ||| @ fh  the file handle to write to
112 | ||| @ str the string to write
113 | export
114 | fPutStrLn : HasIO io => (fh : File) -> (str : String) -> io (Either FileError ())
115 | fPutStrLn fh str = fPutStr fh (str ++ "\n")
116 |
117 | ||| Check whether the end-of-file indicator for the given file handle is set.
118 | |||
119 | ||| @ h the file handle to check
120 | export
121 | fEOF : HasIO io => (h : File) -> io Bool
122 | fEOF (FHandle f)
123 |     = do res <- primIO (prim__eof f)
124 |          pure (res /= 0)
125 |
126 | ||| Read all the remaining contents of a file handle
127 | export
128 | covering
129 | fRead : HasIO io => (h : File) -> io (Either FileError String)
130 | fRead h = fRead' h [<]
131 |   where
132 |     fRead' : HasIO io' => (h : File) -> (acc : SnocList String) -> io' (Either FileError String)
133 |     fRead' h acc = do
134 |       if !(fEOF h)
135 |          then pure $ Right $ concat acc
136 |          else do
137 |              Right line <- fGetLine h
138 |                 | Left err => pure $ Left err
139 |              fRead' h $ acc :< line
140 |
141 | ||| Delete the file at the given name.
142 | |||
143 | ||| @ fname the file to delete
144 | export
145 | removeFile : HasIO io => (fname : String) -> io (Either FileError ())
146 | removeFile fname
147 |     = do res <- primIO (prim__removeFile fname)
148 |          if res == 0
149 |             then ok ()
150 |             else returnError
151 |
152 | ||| Read a number of lines into an accumulator, optionally starting at an offset
153 | ||| in the given file handle. Requires `Fuel` to run since the operation is
154 | ||| total but may run indefinitely; the functions `limit` and `forever` help
155 | ||| with providing `Fuel`.
156 | |||
157 | ||| On success, returns a tuple of whether the EOF was reached (if it wasn't, we
158 | ||| ran out of fuel first) and the lines accumulated.
159 | |||
160 | ||| Note: each line will still have a newline character at the end.
161 | |||
162 | ||| @ acc    the accumulator to read the lines onto
163 | ||| @ offset the offset to start reading at
164 | ||| @ fuel   an amount of `Fuel`
165 | ||| @ h      the file handle to read from
166 | readLinesOnto : HasIO io => (acc : List String) ->
167 |                             (offset : Nat) ->
168 |                             (fuel : Fuel) ->
169 |                             (h : File) ->
170 |                             io (Either FileError (Bool, List String))
171 | readLinesOnto acc _ Dry h = pure (Right (False, reverse acc))
172 | readLinesOnto acc offset (More fuel) h
173 |   = do False <- fEOF h
174 |          | True => pure $ Right (True, reverse acc)
175 |        case offset of
176 |             (S offset') => (fSeekLine h *> readLinesOnto acc offset' (More fuel) h) @{Applicative.Compose}
177 |             0           => (fGetLine h >>= \str => readLinesOnto (str :: acc) 0 fuel h) @{Monad.Compose}
178 |
179 | ||| Read a chunk of a file in a line-delimited fashion.
180 | ||| You can use this function to read an entire file
181 | ||| as with @readFile@ by reading until @forever@ or by
182 | ||| iterating through pages until hitting the end of
183 | ||| the file.
184 | |||
185 | ||| The @limit@ function can provide you with enough
186 | ||| fuel to read exactly a given number of lines.
187 | |||
188 | ||| On success, returns a tuple of whether the end of
189 | ||| the file was reached or not and the lines read in
190 | ||| from the file.
191 | |||
192 | ||| Note that each line will still have a newline
193 | ||| character at the end.
194 | |||
195 | ||| Important: because we are chunking by lines, this
196 | ||| function's totality depends on the assumption that
197 | ||| no single line in the input file is infinite.
198 | |||
199 | ||| @ offset the offset to start reading at
200 | ||| @ until  the `Fuel` limiting how far we can read
201 | ||| @ fname  the name of the file to read
202 | export
203 | readFilePage : HasIO io => (offset : Nat) -> (until : Fuel) -> (fname :  String) ->
204 |                            io (Either FileError (Bool, List String))
205 | readFilePage offset fuel fname
206 |   = withFile fname Read pure $
207 |       readLinesOnto [] offset fuel
208 |
209 | ||| Read the entire file at the given name. This function is `partial` since
210 | ||| there is no guarantee that the given file isn't infinite.
211 | |||
212 | ||| @ fname the name of the file to read
213 | export
214 | covering
215 | readFile : HasIO io => (fname : String) -> io (Either FileError String)
216 | readFile = (map $ map (fastConcat . snd)) . readFilePage 0 forever
217 |
218 | ||| Write the given string to the file at the specified name. Opens the file
219 | ||| with the `WriteTruncate` mode.
220 | ||| (If you have a file handle (a `File`), you may be looking for `fPutStr`.)
221 | |||
222 | ||| @ filePath the file to write to
223 | ||| @ contents the string to write to the file
224 | export
225 | writeFile : HasIO io =>
226 |             (filePath : String) -> (contents : String) ->
227 |             io (Either FileError ())
228 | writeFile file contents
229 |   = withFile file WriteTruncate pure $
230 |       flip fPutStr contents
231 |
232 | ||| Append the given string to the file at the specified name. Opens the file in
233 | ||| with the `Append` mode.
234 | |||
235 | ||| @ filePath the file to write to
236 | ||| @ contents the string to write to the file
237 | export
238 | appendFile : HasIO io =>
239 |              (filePath : String) -> (contents : String) ->
240 |              io (Either FileError ())
241 | appendFile file contents
242 |   = withFile file Append pure $
243 |       flip fPutStr contents
244 |