@@ -0,0 +1,215 @@
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+public export
25+data FileHandle : (mode : Mode) -> Type where
26+ FH : File -> FileHandle mode
27+
28+public export
29+interface File (m : Type -> Type) where
30+ FileHandleI : Mode -> Type
31+
32+ ||| Open a file.
33+ |||
34+ ||| @ fname the filename.
35+ ||| @ mode the mode; either Read, WriteTruncate, Append, ReadWrite,
36+ ||| ReadWriteTruncate, or ReadAppend
37+ |||
38+ open : (fname : String)
39+ -> (mode : Mode)
40+ -> ST m (Either FileError Var) [ addIfRight (FileHandleI mode) ]
41+
42+ ||| Close a file.
43+ close : (fileHandle : Var)
44+ -> ST m () [ remove fileHandle (FileHandleI mode) ]
45+
46+ ||| Have we reached the end of the file.
47+ eof : (fileHandle : Var)
48+ -> {auto prf : ValidModeRead mode}
49+ -> ST m Bool [ fileHandle ::: (FileHandleI mode) ]
50+
51+ ||| Flush
52+ flush : (fileHandle : Var)
53+ -> ST m () [ fileHandle ::: (FileHandleI mode) ]
54+
55+ ||| Read a complete line.
56+ readLine : (fileHandle : Var)
57+ -> {auto prf : ValidModeRead mode}
58+ -> ST m (Either FileError String) [ fileHandle ::: (FileHandleI mode) ]
59+
60+ ||| Read a `Char`.
61+ readChar : (fileHandle : Var)
62+ -> {auto prf : ValidModeRead mode}
63+ -> ST m (Either FileError Char) [ fileHandle ::: (FileHandleI mode) ]
64+
65+ ||| Read the contents of a file into a string.
66+ |||
67+ ||| This checks the size of
68+ ||| the file before beginning to read, and only reads that many bytes,
69+ ||| to ensure that it remains a total function if the file is appended
70+ ||| to while being read.
71+ |||
72+ ||| Returns an error if fname is not a normal file.
73+ readFile : (fileName : String)
74+ -> ST m (Either FileError String) []
75+
76+ ||| Write a complete line to the file.
77+ writeString : (fileHandle : Var)
78+ -> (string : String)
79+ -> {auto prf : ValidModeWrite mode}
80+ -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
81+
82+ ||| Write a complete line to the file.
83+ writeLine : (fileHandle : Var)
84+ -> (string : String)
85+ -> {auto prf : ValidModeWrite mode}
86+ -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
87+
88+ -- ||| Create a file and write contents to the file.
89+ -- writeFile
90+ writeFile : (fileName : String)
91+ -> (string : String)
92+ -> ST m (Either FileError ()) []
93+
94+public export
95+File IO where
96+ FileHandleI mode = State (FileHandle mode)
97+
98+ open fname mode = do
99+ (Right file) <- lift ( openFile fname mode )
100+ | (Left error ) => pure (Left error)
101+ let fh = FH file
102+ var <- new fh
103+ pure (Right var)
104+
105+ close fh = do
106+ (FH file) <- read fh
107+ lift (closeFile file)
108+ delete fh
109+ pure ()
110+
111+ eof fh = do
112+ (FH file) <- read fh
113+ isEof <- lift (fEOF file)
114+ pure (isEof)
115+
116+ flush fh = do
117+ (FH file) <- read fh
118+ lift (fEOF file)
119+ pure ()
120+
121+ readLine fh = do
122+ (FH file) <- read fh
123+ (Right string) <- lift (fGetLine file)
124+ | (Left error ) => pure (Left error)
125+ pure (Right string)
126+
127+ readChar fh = do
128+ (FH file) <- read fh
129+ (Right chr) <- lift (fgetc file)
130+ | (Left error ) => pure (Left error)
131+ pure (Right chr)
132+
133+ readFile fname = do
134+ (Right content) <- lift ( readFile fname )
135+ | (Left error ) => pure (Left error)
136+ pure (Right content)
137+
138+ writeString fh str = do
139+ (FH file) <- read fh
140+ Right x <- lift (fPutStr file str)
141+ | (Left error ) => pure (Left error)
142+ pure (Right x)
143+
144+ writeLine fh str = do
145+ (FH file) <- read fh
146+ Right x <- lift (fPutStrLn file str)
147+ | (Left error ) => pure (Left error)
148+ pure (Right x)
149+
150+ writeFile fname str = do
151+ Right x <- lift (writeFile fname str)
152+ | (Left error ) => pure (Left error)
153+ pure (Right x)
154+
155+public export
156+File (IOExcept a) where
157+ FileHandleI mode = State (FileHandle mode)
158+
159+ open fname mode = do
160+ (Right file) <- lift (ioe_lift (openFile fname mode))
161+ | (Left error ) => pure (Left error)
162+ let fh = FH file
163+ var <- new fh
164+ pure (Right var)
165+
166+ close fh = do
167+ (FH file) <- read fh
168+ lift (ioe_lift (closeFile file))
169+ delete fh
170+ pure ()
171+
172+ eof fh = do
173+ (FH file) <- read fh
174+ isEof <- lift (ioe_lift (fEOF file))
175+ pure (isEof)
176+
177+ flush fh = do
178+ (FH file) <- read fh
179+ lift (ioe_lift (fEOF file))
180+ pure ()
181+
182+ readLine fh = do
183+ (FH file) <- read fh
184+ (Right string) <- lift (ioe_lift (fGetLine file))
185+ | (Left error ) => pure (Left error)
186+ pure (Right string)
187+
188+ readChar fh = do
189+ (FH file) <- read fh
190+ (Right chr) <- lift (ioe_lift (fgetc file))
191+ | (Left error ) => pure (Left error)
192+ pure (Right chr)
193+
194+ readFile fname = do
195+ (Right content) <- lift (ioe_lift (readFile fname))
196+ | (Left error ) => pure (Left error)
197+ pure (Right content)
198+
199+ writeString fh str = do
200+ (FH file) <- read fh
201+ Right x <- lift (ioe_lift (fPutStr file str))
202+ | (Left error ) => pure (Left error)
203+ pure (Right x)
204+
205+ writeLine fh str = do
206+ (FH file) <- read fh
207+ Right x <- lift (ioe_lift (fPutStrLn file str))
208+ | (Left error ) => pure (Left error)
209+ pure (Right x)
210+
211+ writeFile fname str = do
212+ Right x <- lift (ioe_lift (writeFile fname str))
213+ | (Left error ) => pure (Left error)
214+ pure (Right x)
215+--- EOF -------------------------------------------------------------------------