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