git.iko.soy/Idris-dev
on ca34dec help sign in
Idris-dev/libs/contrib/Control/ST/File.idr
247 lines 7.9 kB history raw
1module Control.ST.File
3import Control.ST
4import Control.IOExcept
6%default total
8||| A record of the file modes that can read from a file.
9public export
10data ValidModeRead : Mode -> Type where
11 VMRRead : ValidModeRead Read
12 VMRReadW : ValidModeRead ReadWrite
13 VMRReadWT : ValidModeRead ReadWriteTruncate
14 VMRReadA : ValidModeRead ReadAppend
16||| A record of the file modes that can write from a file.
17public export
18data ValidModeWrite : Mode -> Type where
19 VMWWrite : ValidModeWrite WriteTruncate
20 VMWAppend : ValidModeWrite Append
21 VMWReadW : ValidModeWrite ReadWrite
22 VMWReadWT : ValidModeWrite ReadWriteTruncate
24||| The file handle which will be used as a State Transition
25||| resource in the `IO` and `IOExcept` implementations of `File`.
26|||
27||| @mode The `Mode` that the handle was generated under.
28|||
29public export
30data FileHandle : (mode : Mode) -> Type where
31 FH : File -> FileHandle mode
33||| Description of state transition operations on a file.
34|||
35||| +------------+-------------+----------------+----------------+----------------+
36||| | Operation | State in | Mode in | State out | Mode out |
37||| +------------+-------------+----------------+----------------+----------------+
38||| | open | - | - | file handle | input paramater|
39||| | close | file handle | any | - | - |
40||| | eof | file handle | ValidModeRead | file handle | ValidModeRead |
41||| | flush | file handle | any | file handle | unchanged |
42||| | readLine | file handle | ValidModeRead | file handle | ValidModeRead |
43||| | readChar | file handle | ValidModeRead | file handle | ValidModeRead |
44||| | readFile | - | - | - | - |
45||| | writeString| file handle | ValidModeWrite | file handle | ValidModeWrite |
46||| | writeLine | file handle | ValidModeWrite | file handle | ValidModeWrite |
47||| | writeFile | - | - | - | - |
48||| +------------+-------------+----------------+----------------+----------------+
49|||
50public export
51interface File (m : Type -> Type) where
52 FileHandleI : Mode -> Type
54 ||| Open a file.
55 |||
56 ||| @fname the filename.
57 ||| @mode the mode; either Read, WriteTruncate, Append, ReadWrite,
58 ||| ReadWriteTruncate, or ReadAppend
59 |||
60 open : (fname : String)
61 -> (mode : Mode)
62 -> ST m (Either FileError Var) [ addIfRight (FileHandleI mode) ]
64 ||| Close a file.
65 close : (fileHandle : Var)
66 -> ST m () [ remove fileHandle (FileHandleI mode) ]
68 ||| Have we reached the end of the file.
69 eof : (fileHandle : Var)
70 -> {auto prf : ValidModeRead mode}
71 -> ST m Bool [ fileHandle ::: (FileHandleI mode) ]
73 ||| Flush
74 flush : (fileHandle : Var)
75 -> ST m () [ fileHandle ::: (FileHandleI mode) ]
77 ||| Read a complete line.
78 readLine : (fileHandle : Var)
79 -> {auto prf : ValidModeRead mode}
80 -> ST m (Either FileError String) [ fileHandle ::: (FileHandleI mode) ]
82 ||| Read a `Char`.
83 readChar : (fileHandle : Var)
84 -> {auto prf : ValidModeRead mode}
85 -> ST m (Either FileError Char) [ fileHandle ::: (FileHandleI mode) ]
87 ||| Read the contents of a file into a string.
88 |||
89 ||| This checks the size of
90 ||| the file before beginning to read, and only reads that many bytes,
91 ||| to ensure that it remains a total function if the file is appended
92 ||| to while being read.
93 |||
94 ||| Returns an error if fname is not a normal file.
95 |||
96 readFile : (fileName : String)
97 -> ST m (Either FileError String) []
99 ||| Write a complete line to the file.
100 |||
101 ||| @string The string to be written to file.
102 |||
103 writeString : (fileHandle : Var)
104 -> (string : String)
105 -> {auto prf : ValidModeWrite mode}
106 -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
108 ||| Write a complete line to the file.
109 |||
110 ||| @string The text to be written to file.
111 |||
112 writeLine : (fileHandle : Var)
113 -> (string : String)
114 -> {auto prf : ValidModeWrite mode}
115 -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
117 ||| Create a file and write contents to the file.
118 |||
119 ||| @fname The fileName of the file.
120 ||| @string The text to be written to file.
121 |||
122 writeFile : (fname : String)
123 -> (string : String)
124 -> ST m (Either FileError ()) []
126public export
127File IO where
128 FileHandleI mode = State (FileHandle mode)
130 open fname mode = do
131 (Right file) <- lift ( openFile fname mode )
132 | (Left error ) => pure (Left error)
133 let fh = FH file
134 var <- new fh
135 pure (Right var)
137 close fh = do
138 (FH file) <- read fh
139 lift (closeFile file)
140 delete fh
141 pure ()
143 eof fh = do
144 (FH file) <- read fh
145 isEof <- lift (fEOF file)
146 pure (isEof)
148 flush fh = do
149 (FH file) <- read fh
150 lift (fEOF file)
151 pure ()
153 readLine fh = do
154 (FH file) <- read fh
155 (Right string) <- lift (fGetLine file)
156 | (Left error ) => pure (Left error)
157 pure (Right string)
159 readChar fh = do
160 (FH file) <- read fh
161 (Right chr) <- lift (fgetc file)
162 | (Left error ) => pure (Left error)
163 pure (Right chr)
165 readFile fname = do
166 (Right content) <- lift ( readFile fname )
167 | (Left error ) => pure (Left error)
168 pure (Right content)
170 writeString fh str = do
171 (FH file) <- read fh
172 Right x <- lift (fPutStr file str)
173 | (Left error ) => pure (Left error)
174 pure (Right x)
176 writeLine fh str = do
177 (FH file) <- read fh
178 Right x <- lift (fPutStrLn file str)
179 | (Left error ) => pure (Left error)
180 pure (Right x)
182 writeFile fname str = do
183 Right x <- lift (writeFile fname str)
184 | (Left error ) => pure (Left error)
185 pure (Right x)
187public export
188File (IOExcept a) where
189 FileHandleI mode = State (FileHandle mode)
191 open fname mode = do
192 (Right file) <- lift (ioe_lift (openFile fname mode))
193 | (Left error ) => pure (Left error)
194 let fh = FH file
195 var <- new fh
196 pure (Right var)
198 close fh = do
199 (FH file) <- read fh
200 lift (ioe_lift (closeFile file))
201 delete fh
202 pure ()
204 eof fh = do
205 (FH file) <- read fh
206 isEof <- lift (ioe_lift (fEOF file))
207 pure (isEof)
209 flush fh = do
210 (FH file) <- read fh
211 lift (ioe_lift (fEOF file))
212 pure ()
214 readLine fh = do
215 (FH file) <- read fh
216 (Right string) <- lift (ioe_lift (fGetLine file))
217 | (Left error ) => pure (Left error)
218 pure (Right string)
220 readChar fh = do
221 (FH file) <- read fh
222 (Right chr) <- lift (ioe_lift (fgetc file))
223 | (Left error ) => pure (Left error)
224 pure (Right chr)
226 readFile fname = do
227 (Right content) <- lift (ioe_lift (readFile fname))
228 | (Left error ) => pure (Left error)
229 pure (Right content)
231 writeString fh str = do
232 (FH file) <- read fh
233 Right x <- lift (ioe_lift (fPutStr file str))
234 | (Left error ) => pure (Left error)
235 pure (Right x)
237 writeLine fh str = do
238 (FH file) <- read fh
239 Right x <- lift (ioe_lift (fPutStrLn file str))
240 | (Left error ) => pure (Left error)
241 pure (Right x)
243 writeFile fname str = do
244 Right x <- lift (ioe_lift (writeFile fname str))
245 | (Left error ) => pure (Left error)
246 pure (Right x)
247--- EOF -------------------------------------------------------------------------