@@ -1,4 +1,3 @@
1−-- -------------------------------------------------------- [ Effectful FileIO ]
2module Effect.File
1module Effect.File
4import Effects
3import Effects
@@ -6,188 +5,333 @@ import Control.IOExcept
7%access public export
6%access public export
9−||| A Dependent type to describe File Handles. File handles are
8+-- -------------------------------------------------------------- [ Predicates ]
10−||| parameterised with the current state of the file: Closed; Open for
9+
11−||| reading; and Open for writing.
10+data ValidModeRead : Mode -> Type where
12−|||
11+ VMRRead : ValidModeRead Read
13−||| @ m The file mode.
12+ VMRReadW : ValidModeRead ReadWrite
14−data OpenFile : (m : Mode) -> Type where
13+ VMRReadWT : ValidModeRead ReadWriteTruncate
15− FH : File -> OpenFile m
14+ VMRReadA : ValidModeRead ReadAppend
17−openOK : Mode -> Bool -> Type
16+data ValidModeWrite : Mode -> Type where
18−openOK m True = OpenFile m
17+ VMWWrite : ValidModeWrite WriteTruncate
19−openOK m False = ()
18+ VMWAppend : ValidModeWrite Append
20−
19+ VMWReadW : ValidModeWrite ReadWrite
21−-- ------------------------------------------------------------ [ The Protocol ]
20+ VMWReadWT : ValidModeWrite ReadWriteTruncate
23−||| Here the protocol for resource access is defined as an effect.
22+
24−||| The state transitions diagram for the protocol is as follows:
23+-- -------------------------------------------------- [ Custom Error Reporting ]
26−||| digraph G {
25+namespace FileResult
28−||| empty; read; write; // States
27+ data ResultDesc = SUCCESS | RESULT
30−||| empty -> read [label="Open R"];
29+ data FileOpReturnTy : ResultDesc -> Type -> Type where
31−||| read -> empty [label="Close"];
30+ Success : FileOpReturnTy SUCCESS a
32−||| read -> read [label="ReadLine"];
31+ Result : a -> FileOpReturnTy RESULT a
33−||| read -> read [label="EOF"];
32+ FError : FileError -> FileOpReturnTy ty a
35−||| empty -> write [label="Open W"];
34+ FileOpResult : Type -> Type
36−||| write -> empty [label="Close"];
35+ FileOpResult ty = FileOpReturnTy RESULT ty
37−||| write -> write [label="WriteLine"];
36+
38−|||
37+ FileOpSuccess : Type
39−||| }
38+ FileOpSuccess = FileOpReturnTy SUCCESS ()
40−data FileIO : Effect where
39+
41− ||| Open a file with the specified mode.
40+-- ------------------------------------------------------------ [ The Resource ]
43− ||| Opening a file successful moves the state from 'empty' to the
42+data FileHandle : (m : Mode) -> Type where
44− ||| specified mode. If not successful the state is still 'empty'.
43+ FH : File -> FileHandle m
46− ||| @ fname The file name to be opened.
45+-- ---------------------------------------------- [ Resource Type Construction ]
47− ||| @ m The file mode.
46+
48− Open : (fname: String)
47+calcResourceTy : (m : Mode)
49− -> (m : Mode)
48+ -> FileOpReturnTy fOpTy retTy
50− -> sig FileIO Bool () (\res => case res of
49+ -> Type
51− True => OpenFile m
50+calcResourceTy _ (FError e) = ()
52− False => ())
51+calcResourceTy m _ = FileHandle m
54− ||| Close a file.
53+-- ------------------------------------------------------- [ Effect Definition ]
55− |||
54+data FileE : Effect where
56− ||| Closing a file moves the state from Open to closed.
55+
57− Close : sig FileIO () (OpenFile m) ()
56+ -- Open/Close
59− ||| Read a line from the file.
58+ Open : (fname : String)
61− ||| Only files that are open for reading can be read.
60+ -> sig FileE
62− ReadLine : sig FileIO String (OpenFile Read)
61+ (FileOpSuccess)
64− ||| Write a string to a file.
63+ (\res => calcResourceTy m res)
66− ||| Only file that are open for writing can be written to.
67− WriteString : String -> sig FileIO () (OpenFile WriteTruncate)
71− ||| Only files open for reading can be tested for EOF
72− EOF : sig FileIO Bool (OpenFile Read)
74−-- ------------------------------------------------------------ [ The Handlers ]
76−--- An implementation of the resource access protocol for the IO Context.
77−implementation Handler FileIO IO where
78− handle () (Open fname m) k = do Right h <- openFile fname m
79− | Left err => k False ()
81− handle (FH h) Close k = do closeFile h
83− handle (FH h) ReadLine k = do Right str <- fGetLine h
84− -- Need proper error handling!
85− | Left err => k "" (FH h)
87− handle (FH h) (WriteString str) k = do Right () <- fPutStr h str
88− | Left err => k () (FH h)
90− handle (FH h) EOF k = do e <- fEOF h
93−implementation Handler FileIO (IOExcept a) where
94− handle () (Open fname m) k = do Right h <- ioe_lift $ openFile fname m
95− | Left err => k False ()
97− handle (FH h) Close k = do ioe_lift $ closeFile h
99− handle (FH h) ReadLine k = do Right str <- ioe_lift $ fGetLine h
100− -- Need proper error handling!
101− | Left err => k "" (FH h)
103− handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fPutStr h str
104− | Left err => k () (FH h)
106− handle (FH h) EOF k = do e <- ioe_lift $ fEOF h
109−-- -------------------------------------------------------------- [ The Effect ]
110−FILE_IO : Type -> EFFECT
111−FILE_IO t = MkEff t FileIO
113−-- ------------------------------------------------------------ [ The Bindings ]
115−-- Bind the IO context handlers to functions. These functions will run
116−-- in the IO context.
119−||| Open a file with the specified mode.
121−||| @ fname The file name to be opened.
122−||| @ m The file mode.
123−open : (fname : String)
65+ OpenX : (fname : String)
124 -> (m : Mode)
66 -> (m : Mode)
125− -> Eff Bool [FILE_IO ()]
67+ -> sig FileE
126− (\res => [FILE_IO (case res of
68+ (FileOpSuccess)
127− True => OpenFile m
69+ ()
128− False => ())])
70+ (\res => calcResourceTy m res)
72+ Close : sig FileE () (FileHandle m) ()
76+ FGetC : {auto prf : ValidModeRead m}
82+ FGetLine : {auto prf : ValidModeRead m}
84+ (FileOpResult String)
88+ FReadFile : (fname : String)
90+ (FileOpResult String)
94+ FPutStr : (str : String)
95+ -> {auto prf : ValidModeWrite m}
101+ FPutStrLn : (str : String)
102+ -> {auto prf : ValidModeWrite m}
108+ FWriteFile : (fname : String)
109+ -> (contents : String)
115+ FEOF : {auto prf : ValidModeRead m}
120+-- ---------------------------------------------------------------------- [ IO ]
122+Handler FileE IO where
125+ handle () (Open fname m) k = do
126+ res <- openFile fname m
128+ Left err => k (FError err) ()
129+ Right fh => k Success (FH fh)
131+ handle () (OpenX fname m) k = do
132+ res <- openFileX fname m
134+ Left err => k (FError err) ()
135+ Right fh => k Success (FH fh)
137+ handle (FH h) Close k = do
142+ handle (FH h) FGetC k = do
145+ Left err => k (FError err) (FH h)
146+ Right c => k (Result c) (FH h)
148+ handle (FH h) FGetLine k = do
151+ Left err => k (FError err) (FH h)
152+ Right ln => k (Result ln) (FH h)
154+ handle () (FReadFile fname) k = do
155+ res <- readFile fname
157+ Left err => k (FError err) ()
158+ Right str => k (Result str) ()
161+ handle (FH fh) (FPutStr str) k = do
162+ res <- fPutStr fh str
164+ Left err => k (FError err) (FH fh)
165+ Right () => k Success (FH fh)
167+ handle (FH fh) (FPutStrLn str) k = do
168+ res <- fPutStr fh str
170+ Left err => k (FError err) (FH fh)
171+ Right () => k Success (FH fh)
173+ handle () (FWriteFile fname str) k = do
174+ res <- writeFile fname str
176+ Left err => k (FError err) ()
177+ Right () => k Success ()
180+ handle (FH fh) FEOF k = do
184+-- ---------------------------------------------------------------- [ IOExcept ]
186+Handler FileE (IOExcept a) where
189+ handle () (Open fname m) k = do
190+ res <- ioe_lift $ openFile fname m
192+ Left err => k (FError err) ()
193+ Right fh => k Success (FH fh)
195+ handle () (OpenX fname m) k = do
196+ res <- ioe_lift $ openFileX fname m
198+ Left err => k (FError err) ()
199+ Right fh => k Success (FH fh)
201+ handle (FH h) Close k = do
202+ ioe_lift $ closeFile h
206+ handle (FH h) FGetC k = do
207+ res <- ioe_lift $ fgetc h
209+ Left err => k (FError err) (FH h)
210+ Right c => k (Result c) (FH h)
212+ handle (FH h) FGetLine k = do
213+ res <- ioe_lift $ fGetLine h
215+ Left err => k (FError err) (FH h)
216+ Right ln => k (Result ln) (FH h)
218+ handle () (FReadFile fname) k = do
219+ res <- ioe_lift $ readFile fname
221+ Left err => k (FError err) ()
222+ Right str => k (Result str) ()
225+ handle (FH fh) (FPutStr str) k = do
226+ res <- ioe_lift $ fPutStr fh str
228+ Left err => k (FError err) (FH fh)
229+ Right () => k Success (FH fh)
231+ handle (FH fh) (FPutStrLn str) k = do
232+ res <- ioe_lift $ fPutStr fh str
234+ Left err => k (FError err) (FH fh)
235+ Right () => k Success (FH fh)
237+ handle () (FWriteFile fname str) k = do
238+ res <- ioe_lift $ writeFile fname str
240+ Left err => k (FError err) ()
241+ Right () => k Success ()
244+ handle (FH fh) FEOF k = do
245+ res <- ioe_lift $ fEOF fh
248+-- ------------------------------------------------------ [ Effect and Helpers ]
250+FILE : Type -> EFFECT
251+FILE t = MkEff t FileE
257+W = FileHandle WriteTruncate
260+A = FileHandle Append
263+RW = FileHandle ReadWrite
266+RWPlus = FileHandle ReadWriteTruncate
269+APlus = FileHandle ReadAppend
271+-- --------------------------------------------------------------------- [ API ]
273+-- -------------------------------------------------------- [ Open/Close/Query ]
276+open : (fname : String)
278+ -> Eff (FileOpSuccess)
280+ (\res => [FILE (calcResourceTy m res)])
129open f m = call $ Open f m
281open f m = call $ Open f m
283+openX : (fname : String)
285+ -> Eff (FileOpSuccess)
287+ (\res => [FILE (calcResourceTy m res)])
288+openX f m = call $ OpenX f m
290+close : Eff () [FILE (FileHandle m)] [FILE ()]
293+eof : {auto prf : ValidModeRead m}
294+ -> Eff Bool [FILE (FileHandle m)]
298+-- -------------------------------------------------------------------- [ Read ]
300+readChar : {auto prf : ValidModeRead m}
301+ -> Eff (FileOpResult Char)
302+ [FILE (FileHandle m)]
303+readChar = call FGetC
305+readLine : {auto prf : ValidModeRead m}
306+ -> Eff (FileOpResult String)
307+ [FILE (FileHandle m)]
308+readLine = call FGetLine
310+-- ------------------------------------------------------------------- [ Write ]
312+writeString : (str : String)
313+ -> {auto prf : ValidModeWrite m}
314+ -> Eff (FileOpSuccess)
315+ [FILE (FileHandle m)]
316+writeString str = call $ FPutStr str
318+writeLine : (str : String)
319+ -> {auto prf : ValidModeWrite m}
320+ -> Eff (FileOpSuccess)
321+ [FILE (FileHandle m)]
322+writeLine str = call $ FPutStrLn str
324+-- -------------------------------------------------------------- [ Whole File ]
326+readFile : (fname : String)
327+ -> Eff (FileOpResult String)
329+readFile fn = call $ FReadFile fn
331+writeFile : (fname : String)
332+ -> (contents : String)
333+ -> Eff (FileOpSuccess)
335+writeFile fn str = call $ FWriteFile fn str
133−close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
136−||| Read a line from the file.
137−readLine : Eff String [FILE_IO (OpenFile Read)]
138−readLine = call $ ReadLine
140−||| Write a string to a file.
141−writeString : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
142−writeString str = call $ WriteString str
144−||| Write a line to a file.
145−writeLine : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
146−writeLine str = call $ WriteString (str ++ "\n")
149−eof : Eff Bool [FILE_IO (OpenFile Read)]
152−||| Read a complete file, returning a user defined error if
155−readFile : (errFunc : String -> e)
157− -> Eff (Either e String) [FILE_IO ()]
158−readFile errFunc fname = do
159− case !(open fname Read) of
160− False => pure $ Left (errFunc fname)
166− readAcc : String -> Eff String [FILE_IO (OpenFile Read)]
167− readAcc acc = if (not !(eof))
168− then readAcc (acc ++ !(readLine))
171−||| Write a file containing the provided string, returning a user
172−||| defined error if unsuccesful.
174−writeFile : (errFunc : String -> e)
176− -> (content : String)
177− -> Eff (Either e ()) [FILE_IO ()]
178−writeFile errFunc fname content = do
179− case !(open fname WriteTruncate) of
184− False => pure $ Left (errFunc fname)
188− readFile : String -> Eff (Either String String) [FILE_IO ()]
189− readFile = File.readFile id
191− writeFile : String -> String -> Eff (Either String ()) [FILE_IO ()]
192− writeFile = File.writeFile id
193-- --------------------------------------------------------------------- [ EOF ]
337-- --------------------------------------------------------------------- [ EOF ]