@@ -1,3 +1,4 @@
1+||| Effectful file operations.
1module Effect.File
2module Effect.File
3import Effects
4import Effects
@@ -7,50 +8,85 @@ import Control.IOExcept
8-- -------------------------------------------------------------- [ Predicates ]
9-- -------------------------------------------------------------- [ Predicates ]
11+||| A record of the file modes that can read from a file.
10data ValidModeRead : Mode -> Type where
12data ValidModeRead : Mode -> Type where
11 VMRRead : ValidModeRead Read
13 VMRRead : ValidModeRead Read
12 VMRReadW : ValidModeRead ReadWrite
14 VMRReadW : ValidModeRead ReadWrite
13 VMRReadWT : ValidModeRead ReadWriteTruncate
15 VMRReadWT : ValidModeRead ReadWriteTruncate
14 VMRReadA : ValidModeRead ReadAppend
16 VMRReadA : ValidModeRead ReadAppend
18+||| A record of the file modes that can write from a file.
16data ValidModeWrite : Mode -> Type where
19data ValidModeWrite : Mode -> Type where
17 VMWWrite : ValidModeWrite WriteTruncate
20 VMWWrite : ValidModeWrite WriteTruncate
18 VMWAppend : ValidModeWrite Append
21 VMWAppend : ValidModeWrite Append
19 VMWReadW : ValidModeWrite ReadWrite
22 VMWReadW : ValidModeWrite ReadWrite
20 VMWReadWT : ValidModeWrite ReadWriteTruncate
23 VMWReadWT : ValidModeWrite ReadWriteTruncate
23-- -------------------------------------------------- [ Custom Error Reporting ]
25-- -------------------------------------------------- [ Custom Error Reporting ]
25namespace FileResult
27namespace FileResult
29+ ||| A type to describe the return type of file operations.
27 data ResultDesc = SUCCESS | RESULT
30 data ResultDesc = SUCCESS | RESULT
32+ ||| A custom return type for file operations that is dependent on
33+ ||| the type of file operation.
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.
29− data FileOpReturnTy : ResultDesc -> Type -> Type where
39+ data FileOpReturnTy : (desc : ResultDesc)
43+ ||| The operation completed successfully and doesn't return a
30− Success : FileOpReturnTy SUCCESS a
45+ Success : FileOpReturnTy SUCCESS ty
47+ ||| The operation returns a result of type `ty`.
49+ ||| @ty The value returned.
31− Result : a -> FileOpReturnTy RESULT a
50+ Result : ty -> FileOpReturnTy RESULT ty
52+ ||| The operation failed and the RTS produced the given error.
54+ ||| @err The reported error code.
32− FError : FileError -> FileOpReturnTy ty a
55+ FError : (err : FileError) -> FileOpReturnTy desc ty
57+ ||| Type alias to describe a file operatons that returns a result.
34 FileOpResult : Type -> Type
58 FileOpResult : Type -> Type
35 FileOpResult ty = FileOpReturnTy RESULT ty
59 FileOpResult ty = FileOpReturnTy RESULT ty
61+ ||| Type alias to describe file oeprations that indicate success.
37 FileOpSuccess : Type
62 FileOpSuccess : Type
38 FileOpSuccess = FileOpReturnTy SUCCESS ()
63 FileOpSuccess = FileOpReturnTy SUCCESS ()
40-- ------------------------------------------------------------ [ The Resource ]
65-- ------------------------------------------------------------ [ The Resource ]
67+||| The file handle associated with the effect.
69+||| @m The `Mode` that the handle was generated under.
42data FileHandle : (m : Mode) -> Type where
70data FileHandle : (m : Mode) -> Type where
43 FH : File -> FileHandle m
71 FH : File -> FileHandle m
45-- ---------------------------------------------- [ Resource Type Construction ]
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.
79+||| @m The mode the file handle was generated under.
80+||| @ty The functions return type.
47−calcResourceTy : (m : Mode)
81+calcResourceTy : (m : Mode)
48− -> FileOpReturnTy fOpTy retTy
82+ -> (ty : FileOpReturnTy fOpTy retTy)
50calcResourceTy _ (FError e) = ()
84calcResourceTy _ (FError e) = ()
51calcResourceTy m _ = FileHandle m
85calcResourceTy m _ = FileHandle m
53-- ------------------------------------------------------- [ Effect Definition ]
87-- ------------------------------------------------------- [ Effect Definition ]
89+||| An effect to describe operations on a file.
54data FileE : Effect where
90data FileE : Effect where
56 -- Open/Close
92 -- Open/Close
@@ -111,6 +147,12 @@ data FileE : Effect where
111 (FileOpSuccess)
147 (FileOpSuccess)
115 FEOF : {auto prf : ValidModeRead m}
157 FEOF : {auto prf : ValidModeRead m}
116 -> sig FileE
158 -> sig FileE
@@ -176,6 +218,11 @@ Handler FileE IO where
176 Left err => k (FError err) ()
218 Left err => k (FError err) ()
177 Right () => k Success ()
219 Right () => k Success ()
222+ handle (FH fh) FFlush k = do
180 handle (FH fh) FEOF k = do
227 handle (FH fh) FEOF k = do
181 res <- fEOF fh
228 res <- fEOF fh
@@ -240,6 +287,12 @@ Handler FileE (IOExcept a) where
240 Left err => k (FError err) ()
287 Left err => k (FError err) ()
241 Right () => k Success ()
288 Right () => k Success ()
291+ handle (FH fh) FFlush k = do
292+ ioe_lift $ fflush fh
244 handle (FH fh) FEOF k = do
297 handle (FH fh) FEOF k = do
245 res <- ioe_lift $ fEOF fh
298 res <- ioe_lift $ fEOF fh
@@ -247,24 +300,35 @@ Handler FileE (IOExcept a) where
248-- ------------------------------------------------------ [ Effect and Helpers ]
301-- ------------------------------------------------------ [ Effect and Helpers ]
303+||| Effectful operations for interacting with files.
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.
250−FILE : Type -> EFFECT
307+FILE : (ty : Type) -> EFFECT
251FILE t = MkEff t FileE
308FILE t = MkEff t FileE
310+||| A file has been opened for reading.
254R = FileHandle Read
312R = FileHandle Read
314+||| A file has been opened for writing.
257W = FileHandle WriteTruncate
316W = FileHandle WriteTruncate
318+||| A file can only be appeneded to.
260A = FileHandle Append
320A = FileHandle Append
322+||| A file can be read and written to.
263RW = FileHandle ReadWrite
324RW = FileHandle ReadWrite
326+||| A file opened for reading and writing and has been truncated to
327+||| zero if it previsiouly existed.
265RWPlus : Type
328RWPlus : Type
266RWPlus = FileHandle ReadWriteTruncate
329RWPlus = FileHandle ReadWriteTruncate
331+||| A file will read from the beginning and write at the end.
268APlus : Type
332APlus : Type
269APlus = FileHandle ReadAppend
333APlus = FileHandle ReadAppend
@@ -272,7 +336,12 @@ APlus = FileHandle ReadAppend
273-- -------------------------------------------------------- [ Open/Close/Query ]
337-- -------------------------------------------------------- [ Open/Close/Query ]
341+||| @ fname the filename.
342+||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,
343+||| ReadWriteTruncate, or ReadAppend
276open : (fname : String)
345open : (fname : String)
277 -> (m : Mode)
346 -> (m : Mode)
278 -> Eff (FileOpSuccess)
347 -> Eff (FileOpSuccess)
@@ -280,6 +349,11 @@ open : (fname : String)
280 (\res => [FILE (calcResourceTy m res)])
349 (\res => [FILE (calcResourceTy m res)])
281open f m = call $ Open f m
350open f m = call $ Open f m
352+||| Open a file using C11 extended modes.
354+||| @ fname the filename
355+||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,
356+||| ReadWriteTruncate, or ReadAppend
283openX : (fname : String)
357openX : (fname : String)
284 -> (m : Mode)
358 -> (m : Mode)
285 -> Eff (FileOpSuccess)
359 -> Eff (FileOpSuccess)
@@ -287,21 +361,27 @@ openX : (fname : String)
287 (\res => [FILE (calcResourceTy m res)])
361 (\res => [FILE (calcResourceTy m res)])
288openX f m = call $ OpenX f m
362openX f m = call $ OpenX f m
290close : Eff () [FILE (FileHandle m)] [FILE ()]
365close : Eff () [FILE (FileHandle m)] [FILE ()]
291close = call (Close)
366close = call (Close)
368+||| Have we reached the end of the file.
293eof : {auto prf : ValidModeRead m}
369eof : {auto prf : ValidModeRead m}
294 -> Eff Bool [FILE (FileHandle m)]
370 -> Eff Bool [FILE (FileHandle m)]
295eof = call FEOF
371eof = call FEOF
373+flush : Eff () [FILE (FileHandle m)]
298-- -------------------------------------------------------------------- [ Read ]
376-- -------------------------------------------------------------------- [ Read ]
300readChar : {auto prf : ValidModeRead m}
379readChar : {auto prf : ValidModeRead m}
301 -> Eff (FileOpResult Char)
380 -> Eff (FileOpResult Char)
302 [FILE (FileHandle m)]
381 [FILE (FileHandle m)]
303readChar = call FGetC
382readChar = call FGetC
384+||| Read a complete line.
305readLine : {auto prf : ValidModeRead m}
385readLine : {auto prf : ValidModeRead m}
306 -> Eff (FileOpResult String)
386 -> Eff (FileOpResult String)
307 [FILE (FileHandle m)]
387 [FILE (FileHandle m)]
@@ -309,12 +389,14 @@ readLine = call FGetLine
310-- ------------------------------------------------------------------- [ Write ]
390-- ------------------------------------------------------------------- [ Write ]
392+||| Write a string to the file.
312writeString : (str : String)
393writeString : (str : String)
313 -> {auto prf : ValidModeWrite m}
394 -> {auto prf : ValidModeWrite m}
314 -> Eff (FileOpSuccess)
395 -> Eff (FileOpSuccess)
315 [FILE (FileHandle m)]
396 [FILE (FileHandle m)]
316writeString str = call $ FPutStr str
397writeString str = call $ FPutStr str
399+||| Write a complete line to the file.
318writeLine : (str : String)
400writeLine : (str : String)
319 -> {auto prf : ValidModeWrite m}
401 -> {auto prf : ValidModeWrite m}
320 -> Eff (FileOpSuccess)
402 -> Eff (FileOpSuccess)
@@ -323,11 +405,20 @@ writeLine str = call $ FPutStrLn str
324-- -------------------------------------------------------------- [ Whole File ]
406-- -------------------------------------------------------------- [ Whole File ]
408+||| Read the contents of a file into a string.
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.
415+||| Returns an error if fname is not a normal file.
326readFile : (fname : String)
416readFile : (fname : String)
327 -> Eff (FileOpResult String)
417 -> Eff (FileOpResult String)
328 [FILE ()]
418 [FILE ()]
329readFile fn = call $ FReadFile fn
419readFile fn = call $ FReadFile fn
421+||| Create a file and write contents to the file.
331writeFile : (fname : String)
422writeFile : (fname : String)
332 -> (contents : String)
423 -> (contents : String)
333 -> Eff (FileOpSuccess)
424 -> Eff (FileOpSuccess)