git.iko.soy/Idris-dev
on cb005bc help sign in
Idris-dev/libs/effects/Effect/File.idr
146 lines 5.0 kB history raw
1-- -------------------------------------------------------- [ Effectful FileIO ]
2module Effect.File
4import Effects
5import Control.IOExcept
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.
13data OpenFile : (m : Mode) -> Type where
14 FH : File -> OpenFile m
16openOK : Mode -> Bool -> Type
17openOK m True = OpenFile m
18openOK m False = ()
20-- ------------------------------------------------------------ [ The Protocol ]
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||| }
39data FileIO : Effect where
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
53 ||| Close a file.
54 |||
55 ||| Closing a file moves the state from Open to closed.
56 Close : {OpenFile m ==> ()} FileIO ()
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
63 ||| Write a string to a file.
64 |||
65 ||| Only file that are open for writing can be written to.
66 WriteString : String -> {OpenFile Write} FileIO ()
68 ||| End of file?
69 |||
70 ||| Only files open for reading can be tested for EOF
71 EOF : {OpenFile Read} FileIO Bool
73-- ------------------------------------------------------------ [ The Handlers ]
75--- An implementation of the resource access protocol for the IO Context.
76instance Handler FileIO IO where
77 handle () (Open fname m) k = do h <- openFile fname m
78 valid <- validFile h
79 if valid then k True (FH h)
80 else k False ()
81 handle (FH h) Close k = do closeFile h
82 k () ()
83 handle (FH h) ReadLine k = do str <- fread h
84 k str (FH h)
85 handle (FH h) (WriteString str) k = do fwrite h str
86 k () (FH h)
87 handle (FH h) EOF k = do e <- feof h
88 k e (FH h)
90instance Handler FileIO (IOExcept a) where
91 handle () (Open fname m) k = do h <- ioe_lift $ openFile fname m
92 valid <- ioe_lift $ validFile h
93 if valid then k True (FH h)
94 else k False ()
95 handle (FH h) Close k = do ioe_lift $ closeFile h
96 k () ()
97 handle (FH h) ReadLine k = do str <- ioe_lift $ fread h
98 k str (FH h)
99 handle (FH h) (WriteString str) k = do ioe_lift $ fwrite h str
100 k () (FH h)
101 handle (FH h) EOF k = do e <- ioe_lift $ feof h
102 k e (FH h)
104-- -------------------------------------------------------------- [ The Effect ]
105FILE_IO : Type -> EFFECT
106FILE_IO t = MkEff t FileIO
108-- ------------------------------------------------------------ [ The Bindings ]
109--
110-- Bind the IO context handlers to functions. These functions will run
111-- in the IO context.
112--
114||| Open a file with the specified mode.
115|||
116||| @ fname The file name to be opened.
117||| @ m The file mode.
118open : (fname : String)
119 -> (m : Mode)
120 -> { [FILE_IO ()] ==> [FILE_IO (if result
121 then OpenFile m
122 else ())] } Eff Bool
123open f m = call $ Open f m
126||| Close a file.
127close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff ()
128close = call $ Close
130||| Read a line from the file.
131readLine : { [FILE_IO (OpenFile Read)] } Eff String
132readLine = call $ ReadLine
134||| Write a string to a file.
135writeString : String -> { [FILE_IO (OpenFile Write)] } Eff ()
136writeString str = call $ WriteString str
138||| Write a line to a file.
139writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()
140writeLine str = call $ WriteString (str ++ "\n")
142||| End of file?
143eof : { [FILE_IO (OpenFile Read)] } Eff Bool
144eof = call $ EOF
146-- --------------------------------------------------------------------- [ EOF ]