git.iko.soy/Idris-dev
on master help sign in
First attempt at implementing ST alternative for File.idr in Effects.
cf491baXefias
libs/contrib/Control/ST/File.idrnew file+215
compare with master
unifiedsplit
@@ -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 -------------------------------------------------------------------------
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+77
@@ -0,0 +1,77 @@
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+{-TestFileIO : Type -> (ConsoleIO m, STFile m) => ST m () []-}
14+{-TestFileIO x = ?TestFileIO_rhs-}
15+
16+{-TestFileIO : Type -> Type-}
17+{-TestFileIO : (ConsoleIO m, STFile m) => ST m () []-}
18+
19+{-TestFileCount : Type-}
20+{-TestFileCount : ST m (Either FileError (List String)) -}
21+ {-[ count ::: (State Int), -}
22+ {-fileHandle ::: FileHandleI {m} mode ]-}
23+
24+readFileCount : (ConsoleIO m, File m) =>
25+ (fileHandle : Var)
26+ -> (count : Var)
27+ -> {auto prf : ValidModeRead mode}
28+ -> ST m (Either FileError (List String))
29+ [ count ::: (State Int),
30+ fileHandle ::: FileHandleI {m} mode ]
31+readFileCount fh cnt =
32+ readAcc fh cnt []
33+ where
34+ readAcc : (ConsoleIO m, File m) =>
35+ (fileHandle : Var)
36+ -> (count : Var)
37+ -> List String
38+ -> {auto prf : ValidModeRead mode}
39+ -> ST m (Either FileError (List String))
40+ [ count ::: (State Int),
41+ fileHandle ::: FileHandleI {m} mode ]
42+ readAcc fileHandle cnt acc = with ST do
43+ e <- (eof fileHandle)
44+ if (not e)
45+ then do Right str <- (readLine fileHandle)
46+ | Left ferr => pure (Left ferr)
47+ (increment cnt)
48+ readAcc fileHandle cnt (str :: acc)
49+ else do let rev = reverse acc
50+ pure (Right rev)
51+
52+testFile : (ConsoleIO m, File m) => ST m () []
53+testFile = with ST do
54+ Right fileHandle <- open "testFile" Read
55+ | Left ferr => do putStrLn (show ferr)
56+ pure ()
57+ count <- new 0
58+ Right fContents <- readFileCount fileHandle count
59+ | Left ferr => do putStrLn (show ferr)
60+ delete count
61+ close fileHandle
62+ pure ()
63+ putStrLn (show fContents)
64+ putStrLn (show !(read count))
65+ delete count
66+ close fileHandle
67+ pure ()
68+
69+main : IO ()
70+main = do putStrLn "--test IO:"
71+ run testFile
72+ putStrLn "--test IOExcept:"
73+ ioe_run (run testFile)
74+ (\err => putStrLn err)
75+ (\ok => printLn ok)
76+
77+-- 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 -------------------------------------------------------------------------