git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/libs/effects/Effect/File.idr
428 lines 12 kB history raw
1||| Effectful file operations.
2module Effect.File
4import Effects
5import Control.IOExcept
7%access public export
9-- -------------------------------------------------------------- [ Predicates ]
11||| A record of the file modes that can read from a file.
12data ValidModeRead : Mode -> Type where
13 VMRRead : ValidModeRead Read
14 VMRReadW : ValidModeRead ReadWrite
15 VMRReadWT : ValidModeRead ReadWriteTruncate
16 VMRReadA : ValidModeRead ReadAppend
18||| A record of the file modes that can write from a file.
19data ValidModeWrite : Mode -> Type where
20 VMWWrite : ValidModeWrite WriteTruncate
21 VMWAppend : ValidModeWrite Append
22 VMWReadW : ValidModeWrite ReadWrite
23 VMWReadWT : ValidModeWrite ReadWriteTruncate
25-- -------------------------------------------------- [ Custom Error Reporting ]
27namespace FileResult
29 ||| A type to describe the return type of file operations.
30 data ResultDesc = SUCCESS | RESULT
32 ||| A custom return type for file operations that is dependent on
33 ||| the type of file operation.
34 |||
35 ||| @desc Parameterises the constructors to describe if the function
36 ||| returns a value or not.
37 ||| @ty The return type for a file operation that returns a value.
38 |||
39 data FileOpReturnTy : (desc : ResultDesc)
40 -> (ty : Type)
41 -> Type where
43 ||| The operation completed successfully and doesn't return a
44 ||| result.
45 Success : FileOpReturnTy SUCCESS ty
47 ||| The operation returns a result of type `ty`.
48 |||
49 ||| @ty The value returned.
50 Result : ty -> FileOpReturnTy RESULT ty
52 ||| The operation failed and the RTS produced the given error.
53 |||
54 ||| @err The reported error code.
55 FError : (err : FileError) -> FileOpReturnTy desc ty
57 ||| Type alias to describe a file operatons that returns a result.
58 FileOpResult : Type -> Type
59 FileOpResult ty = FileOpReturnTy RESULT ty
61 ||| Type alias to describe file oeprations that indicate success.
62 FileOpSuccess : Type
63 FileOpSuccess = FileOpReturnTy SUCCESS ()
65-- ------------------------------------------------------------ [ The Resource ]
67||| The file handle associated with the effect.
68|||
69||| @m The `Mode` that the handle was generated under.
70data FileHandle : (m : Mode) -> Type where
71 FH : File -> FileHandle m
73-- ---------------------------------------------- [ Resource Type Construction ]
75||| Calculates the type for the resource being computed over. `Unit`
76||| to describe pre-and-post file handle acquisistion, and `FileHandle
77||| m` when a file handle has been aqcuired.
78|||
79||| @m The mode the file handle was generated under.
80||| @ty The functions return type.
81calcResourceTy : (m : Mode)
82 -> (ty : FileOpReturnTy fOpTy retTy)
83 -> Type
84calcResourceTy _ (FError e) = ()
85calcResourceTy m _ = FileHandle m
87-- ------------------------------------------------------- [ Effect Definition ]
89||| An effect to describe operations on a file.
90data FileE : Effect where
92 -- Open/Close
94 Open : (fname : String)
95 -> (m : Mode)
96 -> sig FileE
97 (FileOpSuccess)
98 ()
99 (\res => calcResourceTy m res)
101 OpenX : (fname : String)
102 -> (m : Mode)
103 -> sig FileE
104 (FileOpSuccess)
105 ()
106 (\res => calcResourceTy m res)
108 Close : sig FileE () (FileHandle m) ()
110 -- Read
112 FGetC : {auto prf : ValidModeRead m}
113 -> sig FileE
114 (FileOpResult Char)
115 (FileHandle m)
116 (FileHandle m)
118 FGetLine : {auto prf : ValidModeRead m}
119 -> sig FileE
120 (FileOpResult String)
121 (FileHandle m)
122 (FileHandle m)
124 FReadFile : (fname : String)
125 -> sig FileE
126 (FileOpResult String)
127 ()
128 ()
129 -- Write
130 FPutStr : (str : String)
131 -> {auto prf : ValidModeWrite m}
132 -> sig FileE
133 (FileOpSuccess)
134 (FileHandle m)
135 (FileHandle m)
137 FPutStrLn : (str : String)
138 -> {auto prf : ValidModeWrite m}
139 -> sig FileE
140 (FileOpSuccess)
141 (FileHandle m)
142 (FileHandle m)
144 FWriteFile : (fname : String)
145 -> (contents : String)
146 -> sig FileE
147 (FileOpSuccess)
148 ()
150 -- Flush
151 FFlush : sig FileE
152 ()
153 (FileHandle m)
154 (FileHandle m)
156 -- Query
157 FEOF : {auto prf : ValidModeRead m}
158 -> sig FileE
159 Bool
160 (FileHandle m)
162-- ---------------------------------------------------------------------- [ IO ]
164Handler FileE IO where
166 -- Open Close
167 handle () (Open fname m) k = do
168 res <- openFile fname m
169 case res of
170 Left err => k (FError err) ()
171 Right fh => k Success (FH fh)
173 handle () (OpenX fname m) k = do
174 res <- openFileX fname m
175 case res of
176 Left err => k (FError err) ()
177 Right fh => k Success (FH fh)
179 handle (FH h) Close k = do
180 closeFile h
181 k () ()
183 -- Read
184 handle (FH h) FGetC k = do
185 res <- fgetc h
186 case res of
187 Left err => k (FError err) (FH h)
188 Right c => k (Result c) (FH h)
190 handle (FH h) FGetLine k = do
191 res <- fGetLine h
192 case res of
193 Left err => k (FError err) (FH h)
194 Right ln => k (Result ln) (FH h)
196 handle () (FReadFile fname) k = do
197 res <- readFile fname
198 case res of
199 Left err => k (FError err) ()
200 Right str => k (Result str) ()
202 -- Write
203 handle (FH fh) (FPutStr str) k = do
204 res <- fPutStr fh str
205 case res of
206 Left err => k (FError err) (FH fh)
207 Right () => k Success (FH fh)
209 handle (FH fh) (FPutStrLn str) k = do
210 res <- fPutStr fh str
211 case res of
212 Left err => k (FError err) (FH fh)
213 Right () => k Success (FH fh)
215 handle () (FWriteFile fname str) k = do
216 res <- writeFile fname str
217 case res of
218 Left err => k (FError err) ()
219 Right () => k Success ()
221 -- Flush
222 handle (FH fh) FFlush k = do
223 fflush fh
224 k () (FH fh)
226 -- Query
227 handle (FH fh) FEOF k = do
228 res <- fEOF fh
229 k res (FH fh)
231-- ---------------------------------------------------------------- [ IOExcept ]
233Handler FileE (IOExcept a) where
235 -- Open Close
236 handle () (Open fname m) k = do
237 res <- ioe_lift $ openFile fname m
238 case res of
239 Left err => k (FError err) ()
240 Right fh => k Success (FH fh)
242 handle () (OpenX fname m) k = do
243 res <- ioe_lift $ openFileX fname m
244 case res of
245 Left err => k (FError err) ()
246 Right fh => k Success (FH fh)
248 handle (FH h) Close k = do
249 ioe_lift $ closeFile h
250 k () ()
252 -- Read
253 handle (FH h) FGetC k = do
254 res <- ioe_lift $ fgetc h
255 case res of
256 Left err => k (FError err) (FH h)
257 Right c => k (Result c) (FH h)
259 handle (FH h) FGetLine k = do
260 res <- ioe_lift $ fGetLine h
261 case res of
262 Left err => k (FError err) (FH h)
263 Right ln => k (Result ln) (FH h)
265 handle () (FReadFile fname) k = do
266 res <- ioe_lift $ readFile fname
267 case res of
268 Left err => k (FError err) ()
269 Right str => k (Result str) ()
271 -- Write
272 handle (FH fh) (FPutStr str) k = do
273 res <- ioe_lift $ fPutStr fh str
274 case res of
275 Left err => k (FError err) (FH fh)
276 Right () => k Success (FH fh)
278 handle (FH fh) (FPutStrLn str) k = do
279 res <- ioe_lift $ fPutStr fh str
280 case res of
281 Left err => k (FError err) (FH fh)
282 Right () => k Success (FH fh)
284 handle () (FWriteFile fname str) k = do
285 res <- ioe_lift $ writeFile fname str
286 case res of
287 Left err => k (FError err) ()
288 Right () => k Success ()
290 -- Flush
291 handle (FH fh) FFlush k = do
292 ioe_lift $ fflush fh
293 k () (FH fh)
296 -- Query
297 handle (FH fh) FEOF k = do
298 res <- ioe_lift $ fEOF fh
299 k res (FH fh)
301-- ------------------------------------------------------ [ Effect and Helpers ]
303||| Effectful operations for interacting with files.
304|||
305||| The `FILE` effect is parameterised by a file handle once a handle has been acquired, and Unit (`()`) if the file handle is expected to be released once the function has returned.
306|||
307FILE : (ty : Type) -> EFFECT
308FILE t = MkEff t FileE
310||| A file has been opened for reading.
311R : Type
312R = FileHandle Read
314||| A file has been opened for writing.
315W : Type
316W = FileHandle WriteTruncate
318||| A file can only be appeneded to.
319A : Type
320A = FileHandle Append
322||| A file can be read and written to.
323RW : Type
324RW = FileHandle ReadWrite
326||| A file opened for reading and writing and has been truncated to
327||| zero if it previsiouly existed.
328RWPlus : Type
329RWPlus = FileHandle ReadWriteTruncate
331||| A file will read from the beginning and write at the end.
332APlus : Type
333APlus = FileHandle ReadAppend
335-- --------------------------------------------------------------------- [ API ]
337-- -------------------------------------------------------- [ Open/Close/Query ]
339||| Open a file.
340|||
341||| @ fname the filename.
342||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,
343||| ReadWriteTruncate, or ReadAppend
344|||
345open : (fname : String)
346 -> (m : Mode)
347 -> Eff (FileOpSuccess)
348 [FILE ()]
349 (\res => [FILE (calcResourceTy m res)])
350open f m = call $ Open f m
352||| Open a file using C11 extended modes.
353|||
354||| @ fname the filename
355||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,
356||| ReadWriteTruncate, or ReadAppend
357openX : (fname : String)
358 -> (m : Mode)
359 -> Eff (FileOpSuccess)
360 [FILE ()]
361 (\res => [FILE (calcResourceTy m res)])
362openX f m = call $ OpenX f m
364||| Close a file.
365close : Eff () [FILE (FileHandle m)] [FILE ()]
366close = call (Close)
368||| Have we reached the end of the file.
369eof : {auto prf : ValidModeRead m}
370 -> Eff Bool [FILE (FileHandle m)]
371eof = call FEOF
373flush : Eff () [FILE (FileHandle m)]
374flush = call FFlush
376-- -------------------------------------------------------------------- [ Read ]
378||| Read a `Char`.
379readChar : {auto prf : ValidModeRead m}
380 -> Eff (FileOpResult Char)
381 [FILE (FileHandle m)]
382readChar = call FGetC
384||| Read a complete line.
385readLine : {auto prf : ValidModeRead m}
386 -> Eff (FileOpResult String)
387 [FILE (FileHandle m)]
388readLine = call FGetLine
390-- ------------------------------------------------------------------- [ Write ]
392||| Write a string to the file.
393writeString : (str : String)
394 -> {auto prf : ValidModeWrite m}
395 -> Eff (FileOpSuccess)
396 [FILE (FileHandle m)]
397writeString str = call $ FPutStr str
399||| Write a complete line to the file.
400writeLine : (str : String)
401 -> {auto prf : ValidModeWrite m}
402 -> Eff (FileOpSuccess)
403 [FILE (FileHandle m)]
404writeLine str = call $ FPutStrLn str
406-- -------------------------------------------------------------- [ Whole File ]
408||| Read the contents of a file into a string.
409|||
410||| This checks the size of
411||| the file before beginning to read, and only reads that many bytes,
412||| to ensure that it remains a total function if the file is appended
413||| to while being read.
414|||
415||| Returns an error if fname is not a normal file.
416readFile : (fname : String)
417 -> Eff (FileOpResult String)
418 [FILE ()]
419readFile fn = call $ FReadFile fn
421||| Create a file and write contents to the file.
422writeFile : (fname : String)
423 -> (contents : String)
424 -> Eff (FileOpSuccess)
425 [FILE ()]
426writeFile fn str = call $ FWriteFile fn str
428-- --------------------------------------------------------------------- [ EOF ]