diff --git a/libs/base/Control/App/FileIO.idr b/libs/base/Control/App/FileIO.idr index 29395196c..c5786873c 100644 --- a/libs/base/Control/App/FileIO.idr +++ b/libs/base/Control/App/FileIO.idr @@ -16,12 +16,16 @@ toFileEx FileExists = FileExists public export interface Has [Exception IOError] e => FileIO e where - withFile : String -> Mode -> + withFile : String -> Mode -> (onError : IOError -> App e a) -> - (onOpen : File -> App e a) -> + (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 diff --git a/support/c/idris_file.c b/support/c/idris_file.c index e1b6b5f95..e84e5eb4b 100644 --- a/support/c/idris_file.c +++ b/support/c/idris_file.c @@ -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); diff --git a/support/c/idris_file.h b/support/c/idris_file.h index 4c4b34669..8567a11c9 100644 --- a/support/c/idris_file.h +++ b/support/c/idris_file.h @@ -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); diff --git a/tests/Main.idr b/tests/Main.idr index ec6123c7c..5a6d15b46 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -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 diff --git a/tests/chez/chez023/File.idr b/tests/chez/chez023/File.idr new file mode 100644 index 000000000..94e9dddc0 --- /dev/null +++ b/tests/chez/chez023/File.idr @@ -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 diff --git a/tests/chez/chez023/expected b/tests/chez/chez023/expected new file mode 100644 index 000000000..ab3e74d3c --- /dev/null +++ b/tests/chez/chez023/expected @@ -0,0 +1,7 @@ +Hello +'I' +dris! + +No exceptions occurred +1/1: Building File (File.idr) +Main> Main> Bye for now! diff --git a/tests/chez/chez023/input b/tests/chez/chez023/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/chez/chez023/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/chez/chez023/run b/tests/chez/chez023/run new file mode 100644 index 000000000..a04a0bfc0 --- /dev/null +++ b/tests/chez/chez023/run @@ -0,0 +1,3 @@ +$1 --no-banner File.idr < input + +rm -rf build test.txt