@@ -1,3 +1,4 @@
1+||| Effectful file operations.
12module Effect.File
23
34import Effects
@@ -7,50 +8,85 @@ import Control.IOExcept
78
89-- -------------------------------------------------------------- [ Predicates ]
910
11+||| A record of the file modes that can read from a file.
1012data ValidModeRead : Mode -> Type where
1113 VMRRead : ValidModeRead Read
1214 VMRReadW : ValidModeRead ReadWrite
1315 VMRReadWT : ValidModeRead ReadWriteTruncate
1416 VMRReadA : ValidModeRead ReadAppend
1517
18+||| A record of the file modes that can write from a file.
1619data ValidModeWrite : Mode -> Type where
1720 VMWWrite : ValidModeWrite WriteTruncate
1821 VMWAppend : ValidModeWrite Append
1922 VMWReadW : ValidModeWrite ReadWrite
2023 VMWReadWT : ValidModeWrite ReadWriteTruncate
2124
22−
2325-- -------------------------------------------------- [ Custom Error Reporting ]
2426
2527namespace FileResult
2628
29+ ||| A type to describe the return type of file operations.
2730 data ResultDesc = SUCCESS | RESULT
2831
29− data FileOpReturnTy : ResultDesc -> Type -> Type where
30− Success : FileOpReturnTy SUCCESS a
31− Result : a -> FileOpReturnTy RESULT a
32− FError : FileError -> FileOpReturnTy ty a
33−
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
42+
43+ ||| The operation completed successfully and doesn't return a
44+ ||| result.
45+ Success : FileOpReturnTy SUCCESS ty
46+
47+ ||| The operation returns a result of type `ty`.
48+ |||
49+ ||| @ty The value returned.
50+ Result : ty -> FileOpReturnTy RESULT ty
51+
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
56+
57+ ||| Type alias to describe a file operatons that returns a result.
3458 FileOpResult : Type -> Type
3559 FileOpResult ty = FileOpReturnTy RESULT ty
3660
61+ ||| Type alias to describe file oeprations that indicate success.
3762 FileOpSuccess : Type
3863 FileOpSuccess = FileOpReturnTy SUCCESS ()
3964
4065-- ------------------------------------------------------------ [ The Resource ]
4166
67+||| The file handle associated with the effect.
68+|||
69+||| @m The `Mode` that the handle was generated under.
4270data FileHandle : (m : Mode) -> Type where
4371 FH : File -> FileHandle m
4472
4573-- ---------------------------------------------- [ Resource Type Construction ]
4674
47−calcResourceTy : (m : Mode)
48− -> FileOpReturnTy fOpTy retTy
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.
81+calcResourceTy : (m : Mode)
82+ -> (ty : FileOpReturnTy fOpTy retTy)
4983 -> Type
5084calcResourceTy _ (FError e) = ()
5185calcResourceTy m _ = FileHandle m
5286
5387-- ------------------------------------------------------- [ Effect Definition ]
88+
89+||| An effect to describe operations on a file.
5490data FileE : Effect where
5591
5692 -- Open/Close
@@ -111,6 +147,12 @@ data FileE : Effect where
111147 (FileOpSuccess)
112148 ()
113149
150+ -- Flush
151+ FFlush : sig FileE
152+ ()
153+ (FileHandle m)
154+ (FileHandle m)
155+
114156 -- Query
115157 FEOF : {auto prf : ValidModeRead m}
116158 -> sig FileE
@@ -176,6 +218,11 @@ Handler FileE IO where
176218 Left err => k (FError err) ()
177219 Right () => k Success ()
178220
221+ -- Flush
222+ handle (FH fh) FFlush k = do
223+ fflush fh
224+ k () (FH fh)
225+
179226 -- Query
180227 handle (FH fh) FEOF k = do
181228 res <- fEOF fh
@@ -240,6 +287,12 @@ Handler FileE (IOExcept a) where
240287 Left err => k (FError err) ()
241288 Right () => k Success ()
242289
290+ -- Flush
291+ handle (FH fh) FFlush k = do
292+ ioe_lift $ fflush fh
293+ k () (FH fh)
294+
295+
243296 -- Query
244297 handle (FH fh) FEOF k = do
245298 res <- ioe_lift $ fEOF fh
@@ -247,24 +300,35 @@ Handler FileE (IOExcept a) where
247300
248301-- ------------------------------------------------------ [ Effect and Helpers ]
249302
250−FILE : Type -> EFFECT
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+|||
307+FILE : (ty : Type) -> EFFECT
251308FILE t = MkEff t FileE
252309
310+||| A file has been opened for reading.
253311R : Type
254312R = FileHandle Read
255313
314+||| A file has been opened for writing.
256315W : Type
257316W = FileHandle WriteTruncate
258317
318+||| A file can only be appeneded to.
259319A : Type
260320A = FileHandle Append
261321
322+||| A file can be read and written to.
262323RW : Type
263324RW = FileHandle ReadWrite
264325
326+||| A file opened for reading and writing and has been truncated to
327+||| zero if it previsiouly existed.
265328RWPlus : Type
266329RWPlus = FileHandle ReadWriteTruncate
267330
331+||| A file will read from the beginning and write at the end.
268332APlus : Type
269333APlus = FileHandle ReadAppend
270334
@@ -272,7 +336,12 @@ APlus = FileHandle ReadAppend
272336
273337-- -------------------------------------------------------- [ Open/Close/Query ]
274338
275−
339+||| Open a file.
340+|||
341+||| @ fname the filename.
342+||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,
343+||| ReadWriteTruncate, or ReadAppend
344+|||
276345open : (fname : String)
277346 -> (m : Mode)
278347 -> Eff (FileOpSuccess)
@@ -280,6 +349,11 @@ open : (fname : String)
280349 (\res => [FILE (calcResourceTy m res)])
281350open f m = call $ Open f m
282351
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
283357openX : (fname : String)
284358 -> (m : Mode)
285359 -> Eff (FileOpSuccess)
@@ -287,21 +361,27 @@ openX : (fname : String)
287361 (\res => [FILE (calcResourceTy m res)])
288362openX f m = call $ OpenX f m
289363
364+||| Close a file.
290365close : Eff () [FILE (FileHandle m)] [FILE ()]
291366close = call (Close)
292367
368+||| Have we reached the end of the file.
293369eof : {auto prf : ValidModeRead m}
294370 -> Eff Bool [FILE (FileHandle m)]
295371eof = call FEOF
296372
373+flush : Eff () [FILE (FileHandle m)]
374+flush = call FFlush
297375
298376-- -------------------------------------------------------------------- [ Read ]
299377
378+||| Read a `Char`.
300379readChar : {auto prf : ValidModeRead m}
301380 -> Eff (FileOpResult Char)
302381 [FILE (FileHandle m)]
303382readChar = call FGetC
304383
384+||| Read a complete line.
305385readLine : {auto prf : ValidModeRead m}
306386 -> Eff (FileOpResult String)
307387 [FILE (FileHandle m)]
@@ -309,12 +389,14 @@ readLine = call FGetLine
309389
310390-- ------------------------------------------------------------------- [ Write ]
311391
392+||| Write a string to the file.
312393writeString : (str : String)
313394 -> {auto prf : ValidModeWrite m}
314395 -> Eff (FileOpSuccess)
315396 [FILE (FileHandle m)]
316397writeString str = call $ FPutStr str
317398
399+||| Write a complete line to the file.
318400writeLine : (str : String)
319401 -> {auto prf : ValidModeWrite m}
320402 -> Eff (FileOpSuccess)
@@ -323,11 +405,20 @@ writeLine str = call $ FPutStrLn str
323405
324406-- -------------------------------------------------------------- [ Whole File ]
325407
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.
326416readFile : (fname : String)
327417 -> Eff (FileOpResult String)
328418 [FILE ()]
329419readFile fn = call $ FReadFile fn
330420
421+||| Create a file and write contents to the file.
331422writeFile : (fname : String)
332423 -> (contents : String)
333424 -> Eff (FileOpSuccess)