Extend Control.App.FileIO

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

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);

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);
 

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

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

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!

tests/chez/chez023/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez023/run

@@ -0,0 +1,3 @@
+$1 --no-banner File.idr < input
+
+rm -rf build test.txt