mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
Merge pull request #283 from timsueberkrueb/more-file-io
Extend Control.App.FileIO
This commit is contained in:
commit
4dc151086c
@ -21,7 +21,11 @@ interface Has [Exception IOError] e => FileIO e where
|
||||
(onOpen : File -> App e a) ->
|
||||
App e a
|
||||
fGetStr : File -> App e String
|
||||
fGetChars : File -> Int -> App e String
|
||||
fGetChar : File -> App e Char
|
||||
fPutStr : File -> String -> App e ()
|
||||
fPutStrLn : File -> String -> App e ()
|
||||
fflush : File -> App e ()
|
||||
fEOF : File -> App e Bool
|
||||
|
||||
-- TODO : Add Binary File IO with buffers
|
||||
@ -41,23 +45,32 @@ readFile f
|
||||
else do str <- fGetStr h
|
||||
read (str :: acc) h
|
||||
|
||||
fileOp : IO (Either FileError a) -> Has [PrimIO, Exception IOError] e => App e a
|
||||
fileOp fileRes
|
||||
= do Right res <- primIO $ fileRes
|
||||
| Left err => throw (FileErr (toFileEx err))
|
||||
pure res
|
||||
|
||||
export
|
||||
Has [PrimIO, Exception IOError] e => FileIO e where
|
||||
withFile fname m onError proc
|
||||
= do Right h <- primIO $ openFile fname m
|
||||
| Left err => onError (FileErr (toFileEx err))
|
||||
res <- catch (proc h) onError
|
||||
primIO $ closeFile h
|
||||
pure res
|
||||
|
||||
fGetStr f
|
||||
= do Right str <- primIO $ fGetLine f
|
||||
| Left err => throw (FileErr (toFileEx err))
|
||||
pure str
|
||||
fGetStr f = fileOp (fGetLine f)
|
||||
|
||||
fPutStr f str
|
||||
= do Right () <- primIO $ File.fPutStr f str
|
||||
| Left err => throw (FileErr (toFileEx err))
|
||||
pure ()
|
||||
fGetChars f n = fileOp (fGetChars f n)
|
||||
|
||||
fGetChar f = fileOp (fGetChar f)
|
||||
|
||||
fPutStr f str = fileOp (fPutStr f str)
|
||||
|
||||
fPutStrLn f str = fileOp (File.fPutStrLn f str)
|
||||
|
||||
fflush f = primIO $ fflush f
|
||||
|
||||
fEOF f = primIO $ fEOF f
|
||||
|
||||
|
@ -107,7 +107,7 @@ char* idris2_readLine(FILE* f) {
|
||||
return buffer; // freed by RTS if not NULL
|
||||
}
|
||||
|
||||
char* idris_readChars(int num, FILE* f) {
|
||||
char* idris2_readChars(int num, FILE* f) {
|
||||
char *buffer = malloc((num+1)*sizeof(char));
|
||||
size_t len;
|
||||
len = fread(buffer, sizeof(char), (size_t)num, f);
|
||||
|
@ -18,7 +18,7 @@ int idris2_fpoll(FILE* f);
|
||||
|
||||
// Treat as a Ptr String (might be NULL)
|
||||
char* idris2_readLine(FILE* f);
|
||||
char* idris_readChars(int num, FILE* f);
|
||||
char* idris2_readChars(int num, FILE* f);
|
||||
|
||||
int idris2_writeLine(FILE* f, char* str);
|
||||
|
||||
|
@ -113,7 +113,7 @@ chezTests
|
||||
= ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
|
||||
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
|
||||
"chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
|
||||
"chez019", "chez020", "chez021", "chez022",
|
||||
"chez019", "chez020", "chez021", "chez022", "chez023",
|
||||
"reg001"]
|
||||
|
||||
ideModeTests : List String
|
||||
|
39
tests/chez/chez023/File.idr
Normal file
39
tests/chez/chez023/File.idr
Normal file
@ -0,0 +1,39 @@
|
||||
import System.File
|
||||
|
||||
import Control.App
|
||||
import Control.App.FileIO
|
||||
import Control.App.Console
|
||||
|
||||
testFileReadOps : File -> Has [Console, FileIO] e => App e ()
|
||||
testFileReadOps file = do
|
||||
testStr <- fGetChars file 6
|
||||
putStrLn testStr
|
||||
chr <- fGetChar file
|
||||
putStrLn (show chr)
|
||||
rest <- fGetStr file
|
||||
putStrLn rest
|
||||
|
||||
testFileWriteOps : File -> Has [Console, FileIO] e => App e ()
|
||||
testFileWriteOps file = do
|
||||
fPutStr file "Hello "
|
||||
fPutStrLn file "Idris!"
|
||||
fPutStrLn file "Another line"
|
||||
|
||||
runTests : Has [Console, FileIO] e => App e ()
|
||||
runTests = do
|
||||
withFile "test.txt" WriteTruncate
|
||||
(\err => putStrLn $ "Failed to open file in write mode: " ++ show err)
|
||||
(\file => testFileWriteOps file)
|
||||
withFile "test.txt" Read
|
||||
(\err => putStrLn $ "Failed to open file in read mode: " ++ show err)
|
||||
(\file => testFileReadOps file)
|
||||
|
||||
prog : App Init ()
|
||||
prog =
|
||||
handle runTests
|
||||
(\() => putStrLn "No exceptions occurred")
|
||||
(\err: IOError =>
|
||||
putStrLn $ "Caught file error : " ++ show err)
|
||||
|
||||
main : IO ()
|
||||
main = run prog
|
7
tests/chez/chez023/expected
Normal file
7
tests/chez/chez023/expected
Normal file
@ -0,0 +1,7 @@
|
||||
Hello
|
||||
'I'
|
||||
dris!
|
||||
|
||||
No exceptions occurred
|
||||
1/1: Building File (File.idr)
|
||||
Main> Main> Bye for now!
|
2
tests/chez/chez023/input
Normal file
2
tests/chez/chez023/input
Normal file
@ -0,0 +1,2 @@
|
||||
:exec main
|
||||
:q
|
3
tests/chez/chez023/run
Normal file
3
tests/chez/chez023/run
Normal file
@ -0,0 +1,3 @@
|
||||
$1 --no-banner File.idr < input
|
||||
|
||||
rm -rf build test.txt
|
Loading…
Reference in New Issue
Block a user