@@ -1,24 +1,78 @@
1+-- -------------------------------------------------------- [ Effectful FileIO ]
12module Effect.File
23
34import Effects
45import Control.IOExcept
56
6−data OpenFile : Mode -> Type where
7+
8+||| A Dependent type to describe File Handles. File handles are
9+||| parameterised with the current state of the file: Closed; Open for
10+||| reading; and Open for writing.
11+|||
12+||| @ m The file mode.
13+data OpenFile : (m : Mode) -> Type where
714 FH : File -> OpenFile m
815
916openOK : Mode -> Bool -> Type
1017openOK m True = OpenFile m
1118openOK m False = ()
1219
20+-- ------------------------------------------------------------ [ The Protocol ]
21+
22+||| Here the protocol for resource access is defined as an effect.
23+||| The state transitions diagram for the protocol is as follows:
24+|||
25+||| digraph G {
26+|||
27+||| empty; read; write; // States
28+|||
29+||| empty -> read [label="Open R"];
30+||| read -> empty [label="Close"];
31+||| read -> read [label="ReadLine"];
32+||| read -> read [label="EOF"];
33+|||
34+||| empty -> write [label="Open W"];
35+||| write -> empty [label="Close"];
36+||| write -> write [label="WriteLine"];
37+|||
38+||| }
1339data FileIO : Effect where
14− Open : String -> (m : Mode) ->
15− {() ==> {res} if res then OpenFile m else ()} FileIO Bool
16− Close : {OpenFile m ==> ()} FileIO ()
17−
18− ReadLine : {OpenFile Read} FileIO String
19− WriteLine : String -> {OpenFile Write} FileIO ()
20− EOF : {OpenFile Read} FileIO Bool
21−
40+ ||| Open a file with the specified mode.
41+ |||
42+ ||| Opening a file successful moves the state from 'empty' to the
43+ ||| specified mode. If not successful the state is still 'empty'.
44+ |||
45+ ||| @ fname The file name to be opened.
46+ ||| @ m The file mode.
47+ Open : (fname: String)
48+ -> (m : Mode)
49+ -> {() ==> {res} if res
50+ then OpenFile m
51+ else ()} FileIO Bool
52+
53+ ||| Close a file.
54+ |||
55+ ||| Closing a file moves the state from Open to closed.
56+ Close : {OpenFile m ==> ()} FileIO ()
57+
58+ ||| Read a line from the file.
59+ |||
60+ ||| Only files that are open for reading can be read.
61+ ReadLine : {OpenFile Read} FileIO String
62+
63+ ||| Write a line to a file.
64+ |||
65+ ||| Only file that are open for writing can be written to.
66+ WriteLine : String -> {OpenFile Write} FileIO ()
67+
68+ ||| End of file?
69+ |||
70+ ||| Only files open for reading can be tested for EOF
71+ EOF : {OpenFile Read} FileIO Bool
72+
73+-- ------------------------------------------------------------ [ The Handlers ]
74+
75+--- An implementation of the resource access protocol for the IO Context.
2276instance Handler FileIO IO where
2377 handle () (Open fname m) k = do h <- openFile fname m
2478 valid <- validFile h
@@ -33,30 +87,47 @@ instance Handler FileIO IO where
3387 handle (FH h) EOF k = do e <- feof h
3488 k e (FH h)
3589
90+-- -------------------------------------------------------------- [ The Effect ]
3691FILE_IO : Type -> EFFECT
3792FILE_IO t = MkEff t FileIO
3893
94+-- ------------------------------------------------------------ [ The Bindings ]
95+--
96+-- Bind the IO context handlers to functions. These functions will run
97+-- in the IO context.
98+--
99+
100+||| Open a file with the specified mode.
101+|||
102+||| @ fname The file name to be opened.
103+||| @ m The file mode.
39104open : Handler FileIO e =>
40− String -> (m : Mode) ->
41− { [FILE_IO ()] ==> [FILE_IO (if result then OpenFile m else ())] } Eff e Bool
105+ (fname : String)
106+ -> (m : Mode)
107+ -> { [FILE_IO ()] ==> [FILE_IO (if result
108+ then OpenFile m
109+ else ())] } Eff e Bool
42110open f m = Open f m
43111
112+
113+||| Close a file.
44114close : Handler FileIO e =>
45115 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
46116close = Close
47117
118+||| Read a line from the file.
48119readLine : Handler FileIO e =>
49120 { [FILE_IO (OpenFile Read)] } Eff e String
50121readLine = ReadLine
51122
123+||| Write a line to a file.
52124writeLine : Handler FileIO e =>
53125 String -> { [FILE_IO (OpenFile Write)] } Eff e ()
54126writeLine str = WriteLine str
55127
128+||| End of file?
56129eof : Handler FileIO e =>
57130 { [FILE_IO (OpenFile Read)] } Eff e Bool
58131eof = EOF
59132
60−
61−
62−
133+-- --------------------------------------------------------------------- [ EOF ]