git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4226 from XeFias/contrib_ST_File
5404934Ahmad Salim Al-Sibahi
CHANGELOG.md+2
compare with master
unifiedsplit
@@ -68,6 +68,8 @@
68+ Removed several deprecated items from the libraries shipped with Idris.
68+ Removed several deprecated items from the libraries shipped with Idris.
69+ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`
69+ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`
70 implements `Abs` with `abs = id`.
70 implements `Abs` with `abs = id`.
71++ Added `Control.ST.File`, an ST based implementation of the same behaviour
72+ implemented by `Effect.File` in the effects package.
71
73
72## Tool Updates
74## Tool Updates
73
75
libs/contrib/Control/ST/File.idrnew file+247
@@ -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 -------------------------------------------------------------------------
libs/contrib/contrib.ipkg+1
@@ -20,6 +20,7 @@ modules = CFFI
20 , Control.ST.Exception
20 , Control.ST.Exception
21 , Control.ST.ImplicitCall
21 , Control.ST.ImplicitCall
22 , Control.ST.Random
22 , Control.ST.Random
23+ , Control.ST.File
23
24
24 , Data.Bool.Extra
25 , Data.Bool.Extra
25 , Data.BoundedList
26 , Data.BoundedList
test/README.md+1
@@ -91,6 +91,7 @@ Tests are categorised with the following test families (and their identifiers):
91+ *reg*: Regression tests, covering previous bug fixes
91+ *reg*: Regression tests, covering previous bug fixes
92+ *regression*: Regression tests, covering previous bug fixes
92+ *regression*: Regression tests, covering previous bug fixes
93+ *sourceLocation*: Interaction with files from Idris
93+ *sourceLocation*: Interaction with files from Idris
94++ *st*: ST, state transition systems
94+ *sugar*: Syntactic sugar, syntax extensions
95+ *sugar*: Syntactic sugar, syntax extensions
95+ *syntax*: Syntax extensions
96+ *syntax*: Syntax extensions
96+ *tactics*: Testing for tactics
97+ *tactics*: Testing for tactics
test/TestData.hs+8
@@ -276,6 +276,14 @@ testFamiliesData = [
276 ( 3 , ANY )]),
276 ( 3 , ANY )]),
277 ("sourceLocation", "Source location",
277 ("sourceLocation", "Source location",
278 [ ( 1 , ANY )]),
278 [ ( 1 , ANY )]),
279+ ("st", "ST",
280+ [ ( 1, C_CG),
281+ ( 2, C_CG),
282+ ( 3, C_CG),
283+ ( 4, C_CG),
284+ ( 5, C_CG),
285+ ( 6, C_CG),
286+ ( 7, C_CG)]),
279 ("sugar", "Syntactic sugar",
287 ("sugar", "Syntactic sugar",
280 [ ( 1, ANY ),
288 [ ( 1, ANY ),
281 ( 2, ANY ),
289 ( 2, ANY ),
test/st001/expectednew file+8
@@ -0,0 +1,8 @@
1+# test001:
2+--test IO:
3+["HELLO!!\n", "WORLD!!"]
4+2
5+--test IOExcept:
6+["HELLO!!\n", "WORLD!!"]
7+2
8+()
test/st001/runnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ -p contrib test001.idr -o test001
3+echo "# test001:"
4+./test001
5+rm -f test001 *.ibc
6+
test/st001/test001.idrnew file+66
@@ -0,0 +1,66 @@
1+module Main
2+
3+import Control.IOExcept
4+import Control.ST
5+import Control.ST.File
6+import Control.ST.ImplicitCall
7+
8+increment : (x : Var) -> STrans m () [ x ::: State Int ]
9+ (const [x ::: State Int])
10+increment x = do num <- read x
11+ write x (num + 1)
12+
13+readFileCount : (ConsoleIO m, File m) =>
14+ (fileHandle : Var)
15+ -> (count : Var)
16+ -> {auto prf : ValidModeRead mode}
17+ -> ST m (Either FileError (List String))
18+ [ count ::: (State Int),
19+ fileHandle ::: FileHandleI {m} mode ]
20+readFileCount fh cnt =
21+ readAcc fh cnt []
22+ where
23+ readAcc : (ConsoleIO m, File m) =>
24+ (fileHandle : Var)
25+ -> (count : Var)
26+ -> List String
27+ -> {auto prf : ValidModeRead mode}
28+ -> ST m (Either FileError (List String))
29+ [ count ::: (State Int),
30+ fileHandle ::: FileHandleI {m} mode ]
31+ readAcc fileHandle cnt acc = with ST do
32+ e <- (eof fileHandle)
33+ if (not e)
34+ then do Right str <- (readLine fileHandle)
35+ | Left ferr => pure (Left ferr)
36+ (increment cnt)
37+ readAcc fileHandle cnt (str :: acc)
38+ else do let rev = reverse acc
39+ pure (Right rev)
40+
41+testFile : (ConsoleIO m, File m) => ST m () []
42+testFile = with ST do
43+ Right fileHandle <- open "testFile" Read
44+ | Left ferr => do putStrLn (show ferr)
45+ pure ()
46+ count <- new 0
47+ Right fContents <- readFileCount fileHandle count
48+ | Left ferr => do putStrLn (show ferr)
49+ delete count
50+ close fileHandle
51+ pure ()
52+ putStrLn (show fContents)
53+ putStrLn (show !(read count))
54+ delete count
55+ close fileHandle
56+ pure ()
57+
58+main : IO ()
59+main = do putStrLn "--test IO:"
60+ run testFile
61+ putStrLn "--test IOExcept:"
62+ ioe_run (run testFile)
63+ (\err => putStrLn err)
64+ (\ok => printLn ok)
65+
66+-- EOF -------------------------------------------------------------------------
test/st001/testFilenew file+2
@@ -0,0 +1,2 @@
1+HELLO!!
2+WORLD!!
test/st002/expectednew file+8
@@ -0,0 +1,8 @@
1+# test002:
2+--test IO:
3+['H', 'E', 'L', 'L', 'O', '!', '!', '\n', 'W', 'O', 'R', 'L', 'D', '!', '!', '\NUL']
4+16
5+--test IOExcept:
6+['H', 'E', 'L', 'L', 'O', '!', '!', '\n', 'W', 'O', 'R', 'L', 'D', '!', '!', '\NUL']
7+16
8+()
test/st002/runnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ -p contrib test002.idr -o test002
3+echo "# test002:"
4+./test002
5+rm -f test002 *.ibc
6+
test/st002/test002.idrnew file+66
@@ -0,0 +1,66 @@
1+module Main
2+
3+import Control.IOExcept
4+import Control.ST
5+import Control.ST.File
6+import Control.ST.ImplicitCall
7+
8+increment : (x : Var) -> STrans m () [ x ::: State Int ]
9+ (const [x ::: State Int])
10+increment x = do num <- read x
11+ write x (num + 1)
12+
13+readFileCount : (ConsoleIO m, File m) =>
14+ (fileHandle : Var)
15+ -> (count : Var)
16+ -> {auto prf : ValidModeRead mode}
17+ -> ST m (Either FileError (List Char))
18+ [ count ::: (State Int),
19+ fileHandle ::: FileHandleI {m} mode ]
20+readFileCount fh cnt =
21+ readAcc fh cnt []
22+ where
23+ readAcc : (ConsoleIO m, File m) =>
24+ (fileHandle : Var)
25+ -> (count : Var)
26+ -> List Char
27+ -> {auto prf : ValidModeRead mode}
28+ -> ST m (Either FileError (List Char))
29+ [ count ::: (State Int),
30+ fileHandle ::: FileHandleI {m} mode ]
31+ readAcc fileHandle cnt acc = with ST do
32+ e <- (eof fileHandle)
33+ if (not e)
34+ then do Right chr <- (readChar fileHandle)
35+ | Left ferr => pure (Left ferr)
36+ (increment cnt)
37+ readAcc fileHandle cnt (chr :: acc)
38+ else do let rev = reverse acc
39+ pure (Right rev)
40+
41+testFile : (ConsoleIO m, File m) => ST m () []
42+testFile = with ST do
43+ Right fileHandle <- open "testFile" Read
44+ | Left ferr => do putStrLn (show ferr)
45+ pure ()
46+ count <- new 0
47+ Right fContents <- readFileCount fileHandle count
48+ | Left ferr => do putStrLn (show ferr)
49+ delete count
50+ close fileHandle
51+ pure ()
52+ putStrLn (show fContents)
53+ putStrLn (show !(read count))
54+ delete count
55+ close fileHandle
56+ pure ()
57+
58+main : IO ()
59+main = do putStrLn "--test IO:"
60+ run testFile
61+ putStrLn "--test IOExcept:"
62+ ioe_run (run testFile)
63+ (\err => putStrLn err)
64+ (\ok => printLn ok)
65+
66+-- EOF -------------------------------------------------------------------------
test/st002/testFilenew file+2
@@ -0,0 +1,2 @@
1+HELLO!!
2+WORLD!!
test/st003/expectednew file+8
@@ -0,0 +1,8 @@
1+# test003:
2+--test IO:
3+HELLO!!
4+WORLD!!
5+--test IOExcept:
6+HELLO!!
7+WORLD!!
8+()
test/st003/runnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ -p contrib test003.idr -o test003
3+echo "# test003:"
4+./test003
5+rm -f test003 *.ibc
6+
test/st003/test003.idrnew file+25
@@ -0,0 +1,25 @@
1+module Main
2+
3+import Control.IOExcept
4+import Control.ST
5+import Control.ST.File
6+import Control.ST.ImplicitCall
7+
8+testFile : (ConsoleIO m, File m) => ST m () []
9+testFile = with ST do
10+ Right str <- readFile "testFile"
11+ | Left ferr => do putStrLn (show ferr)
12+ pure ()
13+ putStrLn str
14+ pure ()
15+
16+
17+main : IO ()
18+main = do putStrLn "--test IO:"
19+ run testFile
20+ putStrLn "--test IOExcept:"
21+ ioe_run (run testFile)
22+ (\err => putStrLn err)
23+ (\ok => printLn ok)
24+
25+-- EOF -------------------------------------------------------------------------
test/st003/testFilenew file+2
@@ -0,0 +1,2 @@
1+HELLO!!
2+WORLD!!
test/st004/expectednew file+6
@@ -0,0 +1,6 @@
1+# test004:
2+--test IO:
3+File Not Found
4+--test IOExcept:
5+File Not Found
6+()
test/st004/runnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ -p contrib test004.idr -o test004
3+echo "# test004:"
4+./test004
5+rm -f test004 *.ibc
6+
test/st004/test004.idrnew file+24
@@ -0,0 +1,24 @@
1+module Main
2+
3+import Control.IOExcept
4+import Control.ST
5+import Control.ST.File
6+import Control.ST.ImplicitCall
7+
8+testFile : (ConsoleIO m, File m) => ST m () []
9+testFile = with ST do
10+ Right str <- readFile "noneexistingtestFile"
11+ | Left ferr => do putStrLn (show ferr)
12+ pure ()
13+ putStr str
14+ pure ()
15+
16+main : IO ()
17+main = do putStrLn "--test IO:"
18+ run testFile
19+ putStrLn "--test IOExcept:"
20+ ioe_run (run testFile)
21+ (\err => putStrLn err)
22+ (\ok => printLn ok)
23+
24+-- EOF -------------------------------------------------------------------------
test/st005/expectednew file+6
@@ -0,0 +1,6 @@
1+# test005:
2+--test IO:
3+--test IOExcept:
4+()
5+HELLO!!
6+WORLD!!
test/st005/runnew file+7
@@ -0,0 +1,7 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ -p contrib test005.idr -o test005
3+echo "# test005:"
4+./test005
5+cat writeTestFile
6+rm -f test005 writeTestFile *.ibc
7+
test/st005/test005.idrnew file+33
@@ -0,0 +1,33 @@
1+module Main
2+
3+import Control.IOExcept
4+import Control.ST
5+import Control.ST.File
6+import Control.ST.ImplicitCall
7+
8+testFile : (ConsoleIO m, File m) => ST m () []
9+testFile = with ST do
10+ Right fileHandle <- open "writeTestFile" WriteTruncate
11+ | Left ferr => do putStrLn (show ferr)
12+ pure ()
13+ Right _ <- writeLine fileHandle "HELLO!!"
14+ | Left ferr => do putStrLn (show ferr)
15+ close fileHandle
16+ pure ()
17+ Right _ <- writeLine fileHandle "WORLD!!"
18+ | Left ferr => do putStrLn (show ferr)
19+ close fileHandle
20+ pure ()
21+ close fileHandle
22+ pure ()
23+
24+
25+main : IO ()
26+main = do putStrLn "--test IO:"
27+ run testFile
28+ putStrLn "--test IOExcept:"
29+ ioe_run (run testFile)
30+ (\err => putStrLn err)
31+ (\ok => printLn ok)
32+
33+-- EOF -------------------------------------------------------------------------
test/st006/expectednew file+5
@@ -0,0 +1,5 @@
1+# test006:
2+--test IO:
3+--test IOExcept:
4+()
5+HELLO!!WORLD!!
test/st006/runnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ -p contrib test006.idr -o test006
3+echo "# test006:"
4+./test006
5+cat writeStringTestFile
6+rm -f test006 writeStringTestFile *.ibc
test/st006/test006.idrnew file+37
@@ -0,0 +1,37 @@
1+module Main
2+
3+import Control.IOExcept
4+import Control.ST
5+import Control.ST.File
6+import Control.ST.ImplicitCall
7+
8+testFile : (ConsoleIO m, File m) => ST m () []
9+testFile = with ST do
10+ Right fileHandle <- open "writeStringTestFile" WriteTruncate
11+ | Left ferr => do putStrLn (show ferr)
12+ pure ()
13+ Right _ <- writeString fileHandle "HELLO!!"
14+ | Left ferr => do putStrLn (show ferr)
15+ close fileHandle
16+ pure ()
17+ Right _ <- writeString fileHandle "WORLD!!"
18+ | Left ferr => do putStrLn (show ferr)
19+ close fileHandle
20+ pure ()
21+ Right _ <- writeString fileHandle "\n"
22+ | Left ferr => do putStrLn (show ferr)
23+ close fileHandle
24+ pure ()
25+ close fileHandle
26+ pure ()
27+
28+
29+main : IO ()
30+main = do putStrLn "--test IO:"
31+ run testFile
32+ putStrLn "--test IOExcept:"
33+ ioe_run (run testFile)
34+ (\err => putStrLn err)
35+ (\ok => printLn ok)
36+
37+-- EOF -------------------------------------------------------------------------
test/st007/expectednew file+6
@@ -0,0 +1,6 @@
1+# test007:
2+--test IO:
3+--test IOExcept:
4+()
5+HELLO!!
6+WORLD!!
test/st007/runnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ -p contrib test007.idr -o test007
3+echo "# test007:"
4+./test007
5+cat writeFileTestFile
6+rm -f test007 writeFileTestFile *.ibc
test/st007/test007.idrnew file+24
@@ -0,0 +1,24 @@
1+module Main
2+
3+import Control.IOExcept
4+import Control.ST
5+import Control.ST.File
6+import Control.ST.ImplicitCall
7+
8+testFile : (ConsoleIO m, File m) => ST m () []
9+testFile = with ST do
10+ Right _ <- writeFile "writeFileTestFile" "HELLO!!\nWORLD!!\n"
11+ | Left ferr => do putStrLn (show ferr)
12+ pure ()
13+ pure ()
14+
15+
16+main : IO ()
17+main = do putStrLn "--test IO:"
18+ run testFile
19+ putStrLn "--test IOExcept:"
20+ ioe_run (run testFile)
21+ (\err => putStrLn err)
22+ (\ok => printLn ok)
23+
24+-- EOF -------------------------------------------------------------------------