make writeBufferData return the number of bytes that have been written (#2276)

CHANGELOG.md

@@ -88,6 +88,8 @@
 * Deprecates `base`'s `Data.Nat.Order.decideLTE` in favor of `Data.Nat.isLTE`.
 * Removes `base`'s deprecated `System.Directory.dirEntry`. Use `nextDirEntry` instead.
 * Removes `base`'s deprecated `Data.String.fastAppend`. Use `fastConcat` instead.
+* `System.File.Buffer.writeBufferData` now returns the number of bytes that have
+   been written when there is a write error.
 * `System.File.Buffer.readBufferData` now returns the number of bytes that have
    been read into the buffer.
 

CONTRIBUTORS

@@ -62,6 +62,7 @@ Thomas E. Hansen
 Tim Süberkrüb
 Timmy Jose
 Wen Kokke
+Wind Wong
 Zoe Stafford
 
 Apologies to anyone we've missed - let us know and we'll correct it (or just

idris2api.ipkg

@@ -170,6 +170,8 @@ modules =
     Libraries.Data.UserNameMap,
     Libraries.Data.Version,
 
+    Libraries.System.File,
+    Libraries.System.File.Buffer,
     Libraries.System.Directory.Tree,
 
     Libraries.Text.Bounded,

libs/base/System/File.idr

@@ -14,12 +14,13 @@ import public System.File.Types
 import public System.File.Virtual
 
 ||| Copy the file at the specified source to the given destination.
+||| Returns the number of bytes that have been written upon a write error.
 |||
 ||| @ src  the file to copy
 ||| @ dest the place to copy the file to
 export
-copyFile : HasIO io => (src : String) -> (dest : String) -> io (Either FileError ())
+copyFile : HasIO io => (src : String) -> (dest : String) -> io (Either (FileError, Int) ())
 copyFile src dest
     = do Right buf <- createBufferFromFile src
-             | Left err => pure (Left err)
+             | Left err => pure (Left (err, 0))
          writeBufferToFile dest buf !(rawSize buf)

libs/base/System/File/Buffer.idr

@@ -18,7 +18,7 @@ prim__readBufferData : FilePtr -> Buffer -> (offset : Int) -> (maxbytes : Int) -
 
 %foreign support "idris2_writeBufferData"
          "node:lambda:(f,b,l,m) => require('fs').writeSync(f.fd,b,l,m)"
-prim__writeBufferData : FilePtr -> Buffer -> (offset : Int) -> (maxbytes : Int) -> PrimIO Int
+prim__writeBufferData : FilePtr -> Buffer -> (offset : Int) -> (size : Int) -> PrimIO Int
 
 ||| Read the data from the file into the given buffer.
 |||
@@ -37,38 +37,41 @@ readBufferData (FHandle h) buf offset max
             then pure (Right read)
             else pure (Left FileReadError)
 
-||| Write the data from the buffer to the given `File`.
+||| Write the data from the buffer to the given `File`. Returns the number
+||| of bytes that have been written upon a write error. Otherwise, it can
+||| be assumed that `size` number of bytes have been written.
 ||| (If you do not have a `File` and just want to write to a file at a known
 ||| path, you probably want to use `writeBufferToFile`.)
 |||
 ||| @ fh       the file handle to write to
 ||| @ buf      the buffer from which to get the data to write
 ||| @ offset   the position in buffer to write from
-||| @ maxbytes the maximum size to write; must not exceed buffer length
+||| @ size     the number of bytes to write; must not exceed buffer length
 export
 writeBufferData : HasIO io => (fh : File) -> (buf : Buffer) ->
                   (offset : Int) ->
-                  (maxbytes : Int) ->
-                  io (Either FileError ())
-writeBufferData (FHandle h) buf offset max
-    = do written <- primIO (prim__writeBufferData h buf offset max)
-         if written >= 0
+                  (size : Int) ->
+                  io (Either (FileError, Int) ())
+writeBufferData (FHandle h) buf offset size
+    = do written <- primIO (prim__writeBufferData h buf offset size)
+         if written == size
             then pure (Right ())
-            else pure (Left FileWriteError)
+            else pure (Left (FileWriteError, written))
 
 ||| Attempt to write the data from the buffer to the file at the specified file
-||| name.
+||| name. Returns the number of bytes that have been written upon a write error.
+||| Otherwise, it can be assumed that `size` number of bytes have been written.
 |||
 ||| @ fn   the file name to write to
 ||| @ buf  the buffer from which to get the data to write
-||| @ max the maximum size to write; must not exceed buffer length
+||| @ size the number of bytes to write; must not exceed buffer length
 export
-writeBufferToFile : HasIO io => (fn : String) -> (buf : Buffer) -> (max : Int) ->
-                                io (Either FileError ())
-writeBufferToFile fn buf max
+writeBufferToFile : HasIO io => (fn : String) -> (buf : Buffer) -> (size : Int) ->
+                                io (Either (FileError, Int) ())
+writeBufferToFile fn buf size
     = do Right f <- openFile fn WriteTruncate
-             | Left err => pure (Left err)
-         Right ok <- writeBufferData f buf 0 max
+             | Left err => pure (Left (err, 0))
+         Right ok <- writeBufferData f buf 0 size
              | Left err => pure (Left err)
          closeFile f
          pure (Right ok)

libs/contrib/System/Directory/Tree.idr

@@ -213,8 +213,10 @@ copyDir src target = runEitherT $ do
     copyDirContents !(liftIO $ explore src) target
   where
     copyFile' : (srcDir : Path) -> (targetDir : Path) -> (fileName : String) -> EitherT FileError io ()
-    copyFile' srcDir targetDir fileName = do
-      MkEitherT $ copyFile (show $ srcDir /> fileName) (show $ targetDir /> fileName)
+    copyFile' srcDir targetDir fileName = MkEitherT $ do
+      Right ok <- copyFile (show $ srcDir /> fileName) (show $ targetDir /> fileName)
+      | Left (err, size) => pure (Left err)
+      pure (Right ok)
 
     covering
     copyDirContents : {srcDir : Path} -> Tree srcDir -> (targetDir : Path) -> EitherT FileError io ()

src/Libraries/System/Directory/Tree.idr

@@ -5,9 +5,10 @@ import Data.DPair
 import Data.List
 import Data.Nat
 import System.Directory
-import System.File
 import Libraries.Utils.Path
 
+import Libraries.System.File as LibFile
+
 %default total
 
 ------------------------------------------------------------------------------
@@ -201,8 +202,10 @@ copyDir src target = runEitherT $ do
     copyDirContents !(liftIO $ explore src) target
   where
     copyFile' : (srcDir : Path) -> (targetDir : Path) -> (fileName : String) -> EitherT FileError io ()
-    copyFile' srcDir targetDir fileName = do
-      MkEitherT $ copyFile (show $ srcDir /> fileName) (show $ targetDir /> fileName)
+    copyFile' srcDir targetDir fileName = MkEitherT $ do
+      Right ok <- LibFile.copyFile (show $ srcDir /> fileName) (show $ targetDir /> fileName)
+      | Left (err, size) => pure (Left err)
+      pure (Right ok)
 
     covering
     copyDirContents : {srcDir : Path} -> Tree srcDir -> (targetDir : Path) -> EitherT FileError io ()

src/Libraries/System/File.idr

@@ -0,0 +1,27 @@
+module Libraries.System.File
+
+import Data.Buffer
+
+import public System.File.Error
+import public System.File.Handle
+import public System.File.Meta
+import public System.File.Mode
+import public System.File.Permissions
+import public System.File.Process
+import public System.File.ReadWrite
+import public System.File.Types
+import public System.File.Virtual
+
+import public Libraries.System.File.Buffer
+
+||| Copy the file at the specified source to the given destination.
+||| Returns the number of bytes that have been written upon a write error.
+|||
+||| @ src  the file to copy
+||| @ dest the place to copy the file to
+export
+copyFile : HasIO io => (src : String) -> (dest : String) -> io (Either (FileError, Int) ())
+copyFile src dest
+    = do Right buf <- createBufferFromFile src
+             | Left err => pure (Left (err, 0))
+         writeBufferToFile dest buf !(rawSize buf)

src/Libraries/System/File/Buffer.idr

@@ -0,0 +1,95 @@
+module Libraries.System.File.Buffer
+
+import public System.File.Error
+import System.File.Handle
+import System.File.Meta
+import System.File.Mode
+import System.File.ReadWrite
+import System.File.Support
+import public System.File.Types
+
+import Data.Buffer
+
+%default total
+
+%foreign support "idris2_readBufferData"
+         "node:lambda:(f,b,l,m) => require('fs').readSync(f.fd,b,l,m)"
+prim__readBufferData : FilePtr -> Buffer -> (offset : Int) -> (maxbytes : Int) -> PrimIO Int
+
+%foreign support "idris2_writeBufferData"
+         "node:lambda:(f,b,l,m) => require('fs').writeSync(f.fd,b,l,m)"
+prim__writeBufferData : FilePtr -> Buffer -> (offset : Int) -> (size : Int) -> PrimIO Int
+
+||| Read the data from the file into the given buffer.
+|||
+||| @ fh       the file handle to read from
+||| @ buf      the buffer to read the data into
+||| @ offset   the position in buffer to start adding
+||| @ maxbytes the maximum size to read; must not exceed buffer length
+export
+readBufferData : HasIO io => (fh : File) -> (buf : Buffer) ->
+                 (offset : Int) ->
+                 (maxbytes : Int) ->
+                 io (Either FileError ())
+readBufferData (FHandle h) buf offset max
+    = do read <- primIO (prim__readBufferData h buf offset max)
+         if read >= 0
+            then pure (Right ())
+            else pure (Left FileReadError)
+
+||| Write the data from the buffer to the given `File`. Returns the number
+||| of bytes that have been written upon a write error. Otherwise, it can
+||| be assumed that `size` number of bytes have been written.
+||| (If you do not have a `File` and just want to write to a file at a known
+||| path, you probably want to use `writeBufferToFile`.)
+|||
+||| @ fh       the file handle to write to
+||| @ buf      the buffer from which to get the data to write
+||| @ offset   the position in buffer to write from
+||| @ size     the number of bytes to write; must not exceed buffer length
+export
+writeBufferData : HasIO io => (fh : File) -> (buf : Buffer) ->
+                  (offset : Int) ->
+                  (size : Int) ->
+                  io (Either (FileError, Int) ())
+writeBufferData (FHandle h) buf offset size
+    = do written <- primIO (prim__writeBufferData h buf offset size)
+         if written == size
+            then pure (Right ())
+            else pure (Left (FileWriteError, written))
+
+||| Attempt to write the data from the buffer to the file at the specified file
+||| name. Returns the number of bytes that have been written upon a write error.
+||| Otherwise, it can be assumed that `size` number of bytes have been written.
+|||
+||| @ fn   the file name to write to
+||| @ buf  the buffer from which to get the data to write
+||| @ size the number of bytes to write; must not exceed buffer length
+export
+writeBufferToFile : HasIO io => (fn : String) -> (buf : Buffer) -> (size : Int) ->
+                                io (Either (FileError, Int) ())
+writeBufferToFile fn buf size
+    = do Right f <- openFile fn WriteTruncate
+             | Left err => pure (Left (err, 0))
+         Right ok <- writeBufferData f buf 0 size
+             | Left err => pure (Left err)
+         closeFile f
+         pure (Right ok)
+
+||| Create a new buffer by opening a file and reading its contents into a new
+||| buffer whose size matches the file size.
+|||
+||| @ fn the name of the file to read
+export
+createBufferFromFile : HasIO io => (fn : String) -> io (Either FileError Buffer)
+createBufferFromFile fn
+    = do Right f <- openFile fn Read
+             | Left err => pure (Left err)
+         Right size <- fileSize f
+             | Left err => pure (Left err)
+         Just buf <- newBuffer size
+             | Nothing => pure (Left FileReadError)
+         Right ok <- readBufferData f buf 0 size
+             | Left err => pure (Left err)
+         closeFile f
+         pure (Right buf)

src/Libraries/Utils/Binary.idr

@@ -3,7 +3,7 @@ module Libraries.Utils.Binary
 import Data.Buffer
 import Data.List
 
-import System.File
+import Libraries.System.File
 
 -- Serialising data as binary. Provides an interface TTC which allows
 -- reading and writing to chunks of memory, "Binary", which can be written
@@ -65,7 +65,9 @@ fromBuffer buf
 export
 writeToFile : (fname : String) -> Binary -> IO (Either FileError ())
 writeToFile fname c
-    = writeBufferToFile fname (buf c) (used c)
+    = do Right ok <- writeBufferToFile fname (buf c) (used c)
+               | Left (err, size) => pure (Left err)
+         pure (Right ok)
 
 export
 readFromFile : (fname : String) -> IO (Either FileError Binary)