git.iko.soy/Idris-dev
on 87fb53a help sign in
Idris-dev/libs/effects/Effect/File.idr
193 lines 6.7 kB history raw
1-- -------------------------------------------------------- [ Effectful FileIO ]
2module Effect.File
4import Effects
5import Control.IOExcept
7%access public export
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.
14data OpenFile : (m : Mode) -> Type where
15 FH : File -> OpenFile m
17openOK : Mode -> Bool -> Type
18openOK m True = OpenFile m
19openOK m False = ()
21-- ------------------------------------------------------------ [ The Protocol ]
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||| }
40data 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 => ())
54 ||| Close a file.
55 |||
56 ||| Closing a file moves the state from Open to closed.
57 Close : sig FileIO () (OpenFile m) ()
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)
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)
69 ||| End of file?
70 |||
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.
77implementation 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)
93implementation 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)
109-- -------------------------------------------------------------- [ The Effect ]
110FILE_IO : Type -> EFFECT
111FILE_IO t = MkEff t FileIO
113-- ------------------------------------------------------------ [ The Bindings ]
114--
115-- Bind the IO context handlers to functions. These functions will run
116-- in the IO context.
117--
119||| Open a file with the specified mode.
120|||
121||| @ fname The file name to be opened.
122||| @ m The file mode.
123open : (fname : String)
124 -> (m : Mode)
125 -> Eff Bool [FILE_IO ()]
126 (\res => [FILE_IO (case res of
127 True => OpenFile m
128 False => ())])
129open f m = call $ Open f m
132||| Close a file.
133close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
134close = call $ Close
136||| Read a line from the file.
137readLine : Eff String [FILE_IO (OpenFile Read)]
138readLine = call $ ReadLine
140||| Write a string to a file.
141writeString : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
142writeString str = call $ WriteString str
144||| Write a line to a file.
145writeLine : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
146writeLine str = call $ WriteString (str ++ "\n")
148||| End of file?
149eof : Eff Bool [FILE_IO (OpenFile Read)]
150eof = call $ EOF
152||| Read a complete file, returning a user defined error if
153||| unsuccesful.
154|||
155readFile : (errFunc : String -> e)
156 -> (fname : String)
157 -> Eff (Either e String) [FILE_IO ()]
158readFile 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
171||| Write a file containing the provided string, returning a user
172||| defined error if unsuccesful.
173|||
174writeFile : (errFunc : String -> e)
175 -> (fname : String)
176 -> (content : String)
177 -> Eff (Either e ()) [FILE_IO ()]
178writeFile 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)
187namespace Default
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 ]