@@ -3,6 +3,7 @@ module Prelude.File
33import Builtins
44import Prelude.List
55import Prelude.Maybe
6+import Prelude.Functor
67import Prelude.Monad
78import Prelude.Chars
89import Prelude.Strings
@@ -80,7 +81,7 @@ do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
8081export
8182ferror : File -> IO Bool
8283ferror (FHandle h) = do err <- do_ferror h
83− pure (not (err == 0))
84+ pure (err /= 0)
8485
8586||| Call the RTS's file opening function
8687private
@@ -95,15 +96,13 @@ export
9596fopen : (f : String) -> (m : String) -> IO (Either FileError File)
9697fopen f m = do h <- do_fopen f m
9798 if !(nullPtr h)
98− then do err <- getFileError
99− pure (Left err)
99+ then Left <$> getFileError
100100 else pure (Right (FHandle h))
101101
102102||| Check whether a file handle is actually a null pointer
103103export
104104validFile : File -> IO Bool
105−validFile (FHandle h) = do x <- nullPtr h
106− pure (not x)
105+validFile (FHandle h) = not <$> nullPtr h
107106
108107||| Modes for opening files
109108data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend
@@ -169,8 +168,7 @@ fileSize : File -> IO (Either FileError Int)
169168fileSize (FHandle h)
170169 = do s <- do_getFileSize h
171170 if (s < 0)
172− then do err <- getFileError
173− pure (Left err)
171+ then Left <$> getFileError
174172 else pure (Right s)
175173
176174export
@@ -178,8 +176,7 @@ fileModifiedTime : File -> IO (Either FileError Integer)
178176fileModifiedTime (FHandle h)
179177 = do s <- do_getFileModifiedTime h
180178 if (s < 0)
181− then do err <- getFileError
182− pure (Left err)
179+ then Left <$> getFileError
183180 else pure (Right s)
184181
185182export
@@ -187,8 +184,7 @@ fileAccessTime : File -> IO (Either FileError Integer)
187184fileAccessTime (FHandle h)
188185 = do s <- do_getFileAccessTime h
189186 if (s < 0)
190− then do err <- getFileError
191− pure (Left err)
187+ then Left <$> getFileError
192188 else pure (Right s)
193189
194190export
@@ -196,11 +192,9 @@ fileStatusTime : File -> IO (Either FileError Integer)
196192fileStatusTime (FHandle h)
197193 = do s <- do_getFileStatusTime h
198194 if (s < 0)
199− then do err <- getFileError
200− pure (Left err)
195+ then Left <$> getFileError
201196 else pure (Right s)
202197
203−
204198private
205199do_fread : Ptr -> IO' l String
206200do_fread h = prim_fread h
@@ -264,8 +258,7 @@ do_fwrite h s = do res <- prim_fwrite h s
264258 then do errno <- getErrno
265259 if errno == 0
266260 then pure (Left FileWriteError)
267− else do err <- getFileError
268− pure (Left err)
261+ else Left <$> getFileError
269262 else pure (Right ())
270263
271264||| Write a line to a file
@@ -287,7 +280,7 @@ do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
287280export
288281fEOF : File -> IO Bool
289282fEOF (FHandle h) = do eof <- do_feof h
290− pure (not (eof == 0))
283+ pure (eof /= 0)
291284
292285private
293286do_fremove : String -> IO Int
@@ -317,7 +310,8 @@ readFile : (filepath : String) -> IO (Either FileError String)
317310readFile fn = do Right h <- openFile fn Read
318311 | Left err => pure (Left err)
319312 Right max <- fileSize h
320− | Left err => pure (Left err)
313+ | Left err => do closeFile h
314+ pure (Left err)
321315 sb <- newStringBuffer (max + 1)
322316 c <- readFile' h max sb
323317 closeFile h
@@ -340,8 +334,11 @@ export
340334writeFile : (filepath : String) -> (contents : String) ->
341335 IO (Either FileError ())
342336writeFile fn contents = do
343− Right h <- openFile fn WriteTruncate | Left err => pure (Left err)
344− Right () <- fPutStr h contents | Left err => pure (Left err)
337+ Right h <- openFile fn WriteTruncate
338+ | Left err => pure (Left err)
339+ Right () <- fPutStr h contents
340+ | Left err => do closeFile h
341+ pure (Left err)
345342 closeFile h
346343 pure (Right ())
347344
@@ -351,8 +348,7 @@ dirOpen : (d : String) -> IO (Either FileError Directory)
351348dirOpen d
352349 = do dptr <- foreign FFI_C "idris_dirOpen" (String -> IO Ptr) d
353350 if !(nullPtr dptr)
354− then do err <- getFileError
355− pure (Left err)
351+ then Left <$> getFileError
356352 else pure (Right (DHandle dptr))
357353
358354export
@@ -363,7 +359,7 @@ export
363359dirError : Directory -> IO Bool
364360dirError (DHandle d)
365361 = do err <- foreign FFI_C "idris_dirError" (Ptr -> IO Int) d
366− pure (not (err == 0))
362+ pure (err /= 0)
367363
368364export
369365dirEntry : Directory -> IO (Either FileError String)
@@ -379,8 +375,7 @@ createDir d
379375 = do ok <- foreign FFI_C "idris_mkdir" (String -> IO Int) d
380376 if (ok == 0)
381377 then pure (Right ())
382− else do err <- getFileError
383− pure (Left err)
378+ else Left <$> getFileError
384379
385380export
386381changeDir : String -> IO Bool