@@ -8,8 +8,8 @@ import Control.IOExcept
88||| A Dependent type to describe File Handles. File handles are
99||| parameterised with the current state of the file: Closed; Open for
1010||| reading; and Open for writing.
11−|||
12−||| @ m The file mode.
11+|||
12+||| @ m The file mode.
1313data OpenFile : (m : Mode) -> Type where
1414 FH : File -> OpenFile m
1515
@@ -21,27 +21,27 @@ openOK m False = ()
2121
2222||| Here the protocol for resource access is defined as an effect.
2323||| The state transitions diagram for the protocol is as follows:
24−|||
24+|||
2525||| digraph G {
26−|||
26+|||
2727||| empty; read; write; // States
28−|||
28+|||
2929||| empty -> read [label="Open R"];
3030||| read -> empty [label="Close"];
3131||| read -> read [label="ReadLine"];
3232||| read -> read [label="EOF"];
33−|||
33+|||
3434||| empty -> write [label="Open W"];
3535||| write -> empty [label="Close"];
3636||| write -> write [label="WriteLine"];
37−|||
37+|||
3838||| }
3939data FileIO : Effect where
4040 ||| Open a file with the specified mode.
41− |||
41+ |||
4242 ||| Opening a file successful moves the state from 'empty' to the
4343 ||| specified mode. If not successful the state is still 'empty'.
44− |||
44+ |||
4545 ||| @ fname The file name to be opened.
4646 ||| @ m The file mode.
4747 Open : (fname: String)
@@ -51,22 +51,22 @@ data FileIO : Effect where
5151 False => ())
5252
5353 ||| Close a file.
54− |||
54+ |||
5555 ||| Closing a file moves the state from Open to closed.
56− Close : sig FileIO () (OpenFile m) ()
56+ Close : sig FileIO () (OpenFile m) ()
5757
5858 ||| Read a line from the file.
59− |||
59+ |||
6060 ||| Only files that are open for reading can be read.
6161 ReadLine : sig FileIO String (OpenFile Read)
62−
62+
6363 ||| Write a string to a file.
64− |||
64+ |||
6565 ||| Only file that are open for writing can be written to.
6666 WriteString : String -> sig FileIO () (OpenFile Write)
6767
6868 ||| End of file?
69− |||
69+ |||
7070 ||| Only files open for reading can be tested for EOF
7171 EOF : sig FileIO Bool (OpenFile Read)
7272
@@ -76,7 +76,7 @@ data FileIO : Effect where
7676instance Handler FileIO IO where
7777 handle () (Open fname m) k = do h <- openFile fname m
7878 valid <- validFile h
79− if valid then k True (FH h)
79+ if valid then k True (FH h)
8080 else k False ()
8181 handle (FH h) Close k = do closeFile h
8282 k () ()
@@ -112,12 +112,12 @@ FILE_IO t = MkEff t FileIO
112112--
113113
114114||| Open a file with the specified mode.
115−|||
115+|||
116116||| @ fname The file name to be opened.
117117||| @ m The file mode.
118118open : (fname : String)
119119 -> (m : Mode)
120− -> Eff Bool [FILE_IO ()]
120+ -> Eff Bool [FILE_IO ()]
121121 (\res => [FILE_IO (case res of
122122 True => OpenFile m
123123 False => ())])
@@ -144,4 +144,45 @@ writeLine str = call $ WriteString (str ++ "\n")
144144eof : Eff Bool [FILE_IO (OpenFile Read)]
145145eof = call $ EOF
146146
147+||| Read a complete file, returning a user defined error if
148+||| unsuccesful.
149+|||
150+readFile : (errFunc : String -> e)
151+ -> (fname : String)
152+ -> Eff (Either e String) [FILE_IO ()]
153+readFile errFunc fname = do
154+ case !(open fname Read) of
155+ False => pure $ Left (errFunc fname)
156+ True => do
157+ src <- readAcc ""
158+ close
159+ pure $ Right src
160+ where
161+ readAcc : String -> Eff String [FILE_IO (OpenFile Read)]
162+ readAcc acc = if (not !(eof))
163+ then readAcc (acc ++ !(readLine))
164+ else pure acc
165+
166+||| Write a file containing the provided string, returning a user
167+||| defined error if unsuccesful.
168+|||
169+writeFile : (errFunc : String -> e)
170+ -> (fname : String)
171+ -> (content : String)
172+ -> Eff (Either e ()) [FILE_IO ()]
173+writeFile errFunc fname content = do
174+ case !(open fname Write) of
175+ True => do
176+ writeString content
177+ close
178+ pure $ Right ()
179+ False => pure $ Left (errFunc fname)
180+
181+
182+namespace Default
183+ readFile : String -> Eff (Either String String) [FILE_IO ()]
184+ readFile = File.readFile id
185+
186+ writeFile : String -> String -> Eff (Either String ()) [FILE_IO ()]
187+ writeFile = File.writeFile id
147188-- --------------------------------------------------------------------- [ EOF ]