@@ -0,0 +1,247 @@
1+module Control.ST.File
2+
3+import Control.ST
4+import Control.IOExcept
5+
6+%default total
7+
8+||| A record of the file modes that can read from a file.
9+public export
10+data ValidModeRead : Mode -> Type where
11+ VMRRead : ValidModeRead Read
12+ VMRReadW : ValidModeRead ReadWrite
13+ VMRReadWT : ValidModeRead ReadWriteTruncate
14+ VMRReadA : ValidModeRead ReadAppend
15+
16+||| A record of the file modes that can write from a file.
17+public export
18+data ValidModeWrite : Mode -> Type where
19+ VMWWrite : ValidModeWrite WriteTruncate
20+ VMWAppend : ValidModeWrite Append
21+ VMWReadW : ValidModeWrite ReadWrite
22+ VMWReadWT : ValidModeWrite ReadWriteTruncate
23+
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+|||
29+public export
30+data FileHandle : (mode : Mode) -> Type where
31+ FH : File -> FileHandle mode
32+
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+|||
50+public export
51+interface File (m : Type -> Type) where
52+ FileHandleI : Mode -> Type
53+
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) ]
63+
64+ ||| Close a file.
65+ close : (fileHandle : Var)
66+ -> ST m () [ remove fileHandle (FileHandleI mode) ]
67+
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) ]
72+
73+ ||| Flush
74+ flush : (fileHandle : Var)
75+ -> ST m () [ fileHandle ::: (FileHandleI mode) ]
76+
77+ ||| Read a complete line.
78+ readLine : (fileHandle : Var)
79+ -> {auto prf : ValidModeRead mode}
80+ -> ST m (Either FileError String) [ fileHandle ::: (FileHandleI mode) ]
81+
82+ ||| Read a `Char`.
83+ readChar : (fileHandle : Var)
84+ -> {auto prf : ValidModeRead mode}
85+ -> ST m (Either FileError Char) [ fileHandle ::: (FileHandleI mode) ]
86+
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) []
98+
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) ]
107+
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) ]
116+
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 ()) []
125+
126+public export
127+File IO where
128+ FileHandleI mode = State (FileHandle mode)
129+
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)
136+
137+ close fh = do
138+ (FH file) <- read fh
139+ lift (closeFile file)
140+ delete fh
141+ pure ()
142+
143+ eof fh = do
144+ (FH file) <- read fh
145+ isEof <- lift (fEOF file)
146+ pure (isEof)
147+
148+ flush fh = do
149+ (FH file) <- read fh
150+ lift (fEOF file)
151+ pure ()
152+
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)
158+
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)
164+
165+ readFile fname = do
166+ (Right content) <- lift ( readFile fname )
167+ | (Left error ) => pure (Left error)
168+ pure (Right content)
169+
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)
175+
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)
181+
182+ writeFile fname str = do
183+ Right x <- lift (writeFile fname str)
184+ | (Left error ) => pure (Left error)
185+ pure (Right x)
186+
187+public export
188+File (IOExcept a) where
189+ FileHandleI mode = State (FileHandle mode)
190+
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)
197+
198+ close fh = do
199+ (FH file) <- read fh
200+ lift (ioe_lift (closeFile file))
201+ delete fh
202+ pure ()
203+
204+ eof fh = do
205+ (FH file) <- read fh
206+ isEof <- lift (ioe_lift (fEOF file))
207+ pure (isEof)
208+
209+ flush fh = do
210+ (FH file) <- read fh
211+ lift (ioe_lift (fEOF file))
212+ pure ()
213+
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)
219+
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)
225+
226+ readFile fname = do
227+ (Right content) <- lift (ioe_lift (readFile fname))
228+ | (Left error ) => pure (Left error)
229+ pure (Right content)
230+
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)
236+
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)
242+
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 -------------------------------------------------------------------------