From e9a80891b7e16e824b21d295a11cc9f2dd8d6a05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tim=20S=C3=BCberkr=C3=BCb?= Date: Thu, 11 Jun 2020 21:35:18 +0200 Subject: [PATCH 1/3] Extend Control.App.FileIO --- libs/base/Control/App/FileIO.idr | 23 +++++++++++++++++-- support/c/idris_file.c | 2 +- support/c/idris_file.h | 2 +- tests/Main.idr | 2 +- tests/chez/chez023/File.idr | 39 ++++++++++++++++++++++++++++++++ tests/chez/chez023/expected | 7 ++++++ tests/chez/chez023/input | 2 ++ tests/chez/chez023/run | 3 +++ 8 files changed, 75 insertions(+), 5 deletions(-) create mode 100644 tests/chez/chez023/File.idr create mode 100644 tests/chez/chez023/expected create mode 100644 tests/chez/chez023/input create mode 100644 tests/chez/chez023/run diff --git a/libs/base/Control/App/FileIO.idr b/libs/base/Control/App/FileIO.idr index 29395196c..271934b3d 100644 --- a/libs/base/Control/App/FileIO.idr +++ b/libs/base/Control/App/FileIO.idr @@ -16,12 +16,15 @@ 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 () fEOF : File -> App e Bool -- TODO : Add Binary File IO with buffers @@ -47,6 +50,7 @@ Has [PrimIO, Exception IOError] e => FileIO e where = 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 @@ -54,11 +58,26 @@ Has [PrimIO, Exception IOError] e => FileIO e where | Left err => throw (FileErr (toFileEx err)) pure str + fGetChars f n + = do Right str <- primIO $ fGetChars f n + | Left err => throw (FileErr (toFileEx err)) + pure str + + fGetChar f + = do Right chr <- primIO $ fGetChar f + | Left err => throw (FileErr (toFileEx err)) + pure chr + fPutStr f str = do Right () <- primIO $ File.fPutStr f str | Left err => throw (FileErr (toFileEx err)) pure () + fPutStrLn f str + = do Right () <- primIO $ File.fPutStrLn f str + | Left err => throw (FileErr (toFileEx err)) + pure () + fEOF f = primIO $ fEOF f export 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 5af947a9c..cae981f5d 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 From 535918a3ac7fdac2c54830bd76032376a6974aad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tim=20S=C3=BCberkr=C3=BCb?= Date: Thu, 11 Jun 2020 21:50:03 +0200 Subject: [PATCH 2/3] Deduplicate Control.App.FileIO --- libs/base/Control/App/FileIO.idr | 31 +++++++++++-------------------- 1 file changed, 11 insertions(+), 20 deletions(-) diff --git a/libs/base/Control/App/FileIO.idr b/libs/base/Control/App/FileIO.idr index 271934b3d..91a71b72b 100644 --- a/libs/base/Control/App/FileIO.idr +++ b/libs/base/Control/App/FileIO.idr @@ -44,6 +44,12 @@ 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 @@ -53,30 +59,15 @@ Has [PrimIO, Exception IOError] e => FileIO e where 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) - fGetChars f n - = do Right str <- primIO $ fGetChars f n - | Left err => throw (FileErr (toFileEx err)) - pure str + fGetChars f n = fileOp (fGetChars f n) - fGetChar f - = do Right chr <- primIO $ fGetChar f - | Left err => throw (FileErr (toFileEx err)) - pure chr + fGetChar f = fileOp (fGetChar f) - fPutStr f str - = do Right () <- primIO $ File.fPutStr f str - | Left err => throw (FileErr (toFileEx err)) - pure () + fPutStr f str = fileOp (fPutStr f str) - fPutStrLn f str - = do Right () <- primIO $ File.fPutStrLn f str - | Left err => throw (FileErr (toFileEx err)) - pure () + fPutStrLn f str = fileOp (File.fPutStrLn f str) fEOF f = primIO $ fEOF f From 30410eda5242c2583b71bf2e2b36bb609fab3f18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tim=20S=C3=BCberkr=C3=BCb?= Date: Fri, 12 Jun 2020 17:30:31 +0200 Subject: [PATCH 3/3] Add fflush to Control.App.FileIO --- libs/base/Control/App/FileIO.idr | 3 +++ 1 file changed, 3 insertions(+) diff --git a/libs/base/Control/App/FileIO.idr b/libs/base/Control/App/FileIO.idr index 91a71b72b..c5786873c 100644 --- a/libs/base/Control/App/FileIO.idr +++ b/libs/base/Control/App/FileIO.idr @@ -25,6 +25,7 @@ interface Has [Exception IOError] e => FileIO e where 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 @@ -69,6 +70,8 @@ Has [PrimIO, Exception IOError] e => FileIO e where fPutStrLn f str = fileOp (File.fPutStrLn f str) + fflush f = primIO $ fflush f + fEOF f = primIO $ fEOF f export