File IO type indicates possibility of failure

At the cost of having to check the result, file IO operations no longer
silently fail, so you won't get a segfault on trying to read a
non-existent file any more.

Pattern matching alternative notation makes this not too painful (see
Prelude.File.readFile for example)

Also, versions which throw exceptions instead could be implemented in
IOExcept, if exceptions are preferred.

CHANGELOG

@@ -37,6 +37,9 @@ Library updates
   from Effectful programs.
 * Some constructors that never actually occurred have been removed from
   the TT and Raw reflection datatypes in Language.Reflection.
+* File IO operations (for example openFile/fread/fwrite) now return 
+  'Either FileError ty' where the return type was previously 'ty' to indicate
+  that they may fail.
 
 Tool updates
 ------------

libs/contrib/Network/Socket.idr

@@ -143,10 +143,6 @@ record Socket where
   socketType : SocketType
   protocalNumber : ProtocolNumber
 
-||| Get the C error number
-getErrno : IO Int
-getErrno = foreign FFI_C "idrnet_errno" (IO Int)
-
 ||| Creates a UNIX socket with the given family, socket type and protocol
 ||| number. Returns either a socket or an error.
 socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)

libs/effects/Effect/File.idr

@@ -74,29 +74,33 @@ data FileIO : Effect where
 
 --- An implementation of the resource access protocol for the IO Context.
 instance Handler FileIO IO where
-    handle () (Open fname m) k = do h <- openFile fname m
-                                    valid <- validFile h
-                                    if valid then k True (FH h)
-                                             else k False ()
+    handle () (Open fname m) k = do Right h <- openFile fname m
+                                        | Left err => k False ()
+                                    k True (FH h)
     handle (FH h) Close      k = do closeFile h
                                     k () ()
-    handle (FH h) ReadLine        k = do str <- fread h
+    handle (FH h) ReadLine        k = do Right str <- fread h
+                                         -- Need proper error handling!
+                                             | Left err => k "" (FH h)
                                          k str (FH h)
-    handle (FH h) (WriteString str) k = do fwrite h str
+    handle (FH h) (WriteString str) k = do Right () <- fwrite h str
+                                             | Left err => k () (FH h)
                                            k () (FH h)
     handle (FH h) EOF             k = do e <- feof h
                                          k e (FH h)
 
 instance Handler FileIO (IOExcept a) where
-    handle () (Open fname m) k = do h <- ioe_lift $ openFile fname m
-                                    valid <- ioe_lift $ validFile h
-                                    if valid then k True (FH h)
-                                             else k False ()
+    handle () (Open fname m) k = do Right h <- ioe_lift $ openFile fname m
+                                        | Left err => k False ()
+                                    k True (FH h)
     handle (FH h) Close      k = do ioe_lift $ closeFile h
                                     k () ()
-    handle (FH h) ReadLine        k = do str <- ioe_lift $ fread h
+    handle (FH h) ReadLine        k = do Right str <- ioe_lift $ fread h
+                                         -- Need proper error handling!
+                                             | Left err => k "" (FH h)
                                          k str (FH h)
-    handle (FH h) (WriteString str) k = do ioe_lift $ fwrite h str
+    handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fwrite h str
+                                             | Left err => k () (FH h)
                                            k () (FH h)
     handle (FH h) EOF             k = do e <- ioe_lift $ feof h
                                          k e (FH h)

libs/prelude/IO.idr

@@ -198,6 +198,9 @@ namespace IO
   forceGC : IO ()
   forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm
 
+  getErrno : IO Int
+  getErrno = foreign FFI_C "idris_errno" (IO Int)
+
 --------- The Javascript/Node FFI
 
 

libs/prelude/Prelude/File.idr

@@ -10,7 +10,8 @@ import Prelude.Cast
 import Prelude.Bool
 import Prelude.Basics
 import Prelude.Classes
-import Prelude.Monad
+import Prelude.Either
+import Prelude.Show
 import IO
 
 %access public
@@ -19,6 +20,31 @@ import IO
 abstract
 data File = FHandle Ptr
 
+||| An error from a file operation
+-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
+-- the values correspond!
+data FileError = FileReadError
+               | FileWriteError
+               | FileNotFound
+               | PermissionDenied
+               | GenericFileError Int -- errno
+
+private
+strError : Int -> String
+strError err = unsafePerformIO -- yeah, yeah...
+                  (foreign FFI_C "idris_showerror" (Int -> IO String) err)
+
+getFileError : IO FileError
+getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError" 
+                                    (Ptr -> IO (Raw FileError)) prim__vm
+                  return err
+
+instance Show FileError where
+  show Success = "Success"
+  show FileNotFound = "File Not Found"
+  show PermissionDenied = "Permission Denied"
+  show (GenericFileError errno) = strError errno
+
 ||| Standard input
 stdin : File
 stdin = FHandle prim__stdin
@@ -31,6 +57,13 @@ stdout = FHandle prim__stdout
 stderr : File
 stderr = FHandle prim__stderr
 
+do_ferror : Ptr -> IO Int
+do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
+
+ferror : File -> IO Bool
+ferror (FHandle h) = do err <- do_ferror h
+                        return (not (err == 0))
+
 ||| Call the RTS's file opening function
 do_fopen : String -> String -> IO Ptr
 do_fopen f m
@@ -39,12 +72,14 @@ do_fopen f m
 ||| Open a file
 ||| @ f the filename
 ||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
-fopen : (f : String) -> (m : String) -> IO File
+fopen : (f : String) -> (m : String) -> IO (Either FileError File)
 fopen f m = do h <- do_fopen f m
-               return (FHandle h)
+               if !(nullPtr h)
+                  then do err <- getFileError
+                          return (Left err)
+                  else return (Right (FHandle h))
 
 ||| Check whether a file handle is actually a null pointer
-partial
 validFile : File -> IO Bool
 validFile (FHandle h) = do x <- nullPtr h
                            return (not x)
@@ -55,33 +90,26 @@ data Mode = Read | Write | ReadWrite
 ||| Open a file
 ||| @ f the filename
 ||| @ m the mode
-partial
-openFile : (f : String) -> (m : Mode) -> IO File
+openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
 openFile f m = fopen f (modeStr m) where
   modeStr Read  = "r"
   modeStr Write = "w"
   modeStr ReadWrite = "r+"
 
-partial
 do_fclose : Ptr -> IO ()
 do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h
 
-partial
 closeFile : File -> IO ()
 closeFile (FHandle h) = do_fclose h
 
-partial
 do_fread : Ptr -> IO' l String
 do_fread h = prim_fread h
 
-fgetc : File -> IO Char
-fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))
-
-fgetc' : File -> IO (Maybe Char)
-fgetc' (FHandle h)
-   = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h
-        if (x < 0) then return Nothing
-                   else return (Just (cast x))
+fgetc : File -> IO (Either FileError Char)
+fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)
+                       if !(ferror (FHandle h))
+                          then return (Left FileReadError)
+                          else return (Right c)
 
 fflush : File -> IO ()
 fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
@@ -89,9 +117,12 @@ fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
 do_popen : String -> String -> IO Ptr
 do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m
 
-popen : String -> Mode -> IO File
+popen : String -> Mode -> IO (Either FileError File)
 popen f m = do ptr <- do_popen f (modeStr m)
-               return (FHandle ptr)
+               if !(nullPtr ptr)
+                  then do err <- getFileError
+                          return (Left err)
+                  else return (Right (FHandle ptr))
   where
     modeStr Read  = "r"
     modeStr Write = "w"
@@ -103,20 +134,25 @@ pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
 -- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
 --                        prim__vm h
 
-partial
-fread : File -> IO' l String
-fread (FHandle h) = do_fread h
+fread : File -> IO (Either FileError String)
+fread (FHandle h) = do str <- do_fread h
+                       if !(ferror (FHandle h))
+                          then return (Left FileReadError)
+                          else return (Right str)
 
-partial
-do_fwrite : Ptr -> String -> IO ()
-do_fwrite h s = do prim_fwrite h s
-                   return ()
+do_fwrite : Ptr -> String -> IO (Either FileError ())
+do_fwrite h s = do res <- prim_fwrite h s
+                   if (res /= 0)
+                      then do errno <- getErrno
+                              if errno == 0 
+                                 then return (Left FileWriteError)
+                                 else do err <- getFileError
+                                         return (Left err)
+                      else return (Right ())
 
-partial
-fwrite : File -> String -> IO ()
+fwrite : File -> String -> IO (Either FileError ())
 fwrite (FHandle h) s = do_fwrite h s
 
-partial
 do_feof : Ptr -> IO Int
 do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
 
@@ -125,32 +161,27 @@ feof : File -> IO Bool
 feof (FHandle h) = do eof <- do_feof h
                       return (not (eof == 0))
 
-partial
-do_ferror : Ptr -> IO Int
-do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
-
-ferror : File -> IO Bool
-ferror (FHandle h) = do err <- do_ferror h
-                        return (not (err == 0))
-
 fpoll : File -> IO Bool
 fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
                        return (p > 0)
 
 ||| Read the contents of a file into a string
-partial -- no error checking!
-readFile : String -> IO String
-readFile fn = do h <- openFile fn Read
+partial -- might be reading something infinitely long like /dev/null ... 
+covering
+readFile : String -> IO (Either FileError String)
+readFile fn = do Right h <- openFile fn Read
+                    | Left err => return (Left err)
                  c <- readFile' h ""
                  closeFile h
                  return c
   where
     partial
-    readFile' : File -> String -> IO String
+    readFile' : File -> String -> IO (Either FileError String)
     readFile' h contents =
        do x <- feof h
-          if not x then do l <- fread h
+          if not x then do Right l <- fread h
+                               | Left err => return (Left err)
                            readFile' h (contents ++ l)
-                   else return contents
+                   else return (Right contents)
 
 

libs/prelude/Prelude/Interactive.idr

@@ -17,6 +17,7 @@ import Prelude.Show
 import Prelude.Cast
 import Prelude.Maybe
 import Prelude.Functor
+import Prelude.Either
 import Prelude.Monad
 import IO
 
@@ -97,7 +98,8 @@ processHandle : File ->
 processHandle h acc onRead onEOF 
    = if !(feof h)
         then putStr (onEOF acc)
-        else do x <- fread h
+        else do Right x <- fread h
+                    | Left err => putStr (onEOF acc)
                 let (out, acc') = onRead acc x
                 putStr out
                 processHandle h acc' onRead onEOF    

libs/prelude/Prelude/Show.idr

@@ -10,6 +10,7 @@ import Prelude.Chars
 import Prelude.Classes
 import Prelude.List
 import Prelude.Maybe
+import Prelude.Either
 import Prelude.Nat
 import Prelude.Strings
 
@@ -185,6 +186,10 @@ instance Show a => Show (Maybe a) where
   showPrec d Nothing  = "Nothing"
   showPrec d (Just x) = showCon d "Just" $ showArg x
 
+instance (Show a, Show b) => Show (Either a b) where
+  showPrec d (Left x)  = showCon d "Left" $ showArg x
+  showPrec d (Right x) = showCon d "Right" $ showArg x
+
 instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
     show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
 

rts/idris_rts.c

@@ -1,4 +1,5 @@
 #include <assert.h>
+#include <errno.h>
 
 #include "idris_rts.h"
 #include "idris_gc.h"
@@ -934,6 +935,14 @@ void idris_freeMsg(Msg* msg) {
     free(msg);
 }
 
+int idris_errno() {
+    return errno;
+}
+
+char* idris_showerror(int err) {
+    return strerror(err);
+}
+
 VAL* nullary_cons;
 
 void init_nullaries() {

rts/idris_rts.h

@@ -255,6 +255,9 @@ void idris_free(void* ptr, size_t size);
 
 #define NULL_CON(x) nullary_cons[x]
 
+int idris_errno();
+char* idris_showerror(int err);
+
 extern VAL* nullary_cons;
 void init_nullaries();
 void free_nullaries();

rts/idris_stdfgn.c

@@ -4,6 +4,7 @@
 #include "idris_gc.h"
 #include <sys/select.h>
 #include <fcntl.h>
+#include <errno.h>
 #include <stdio.h>
 #include <time.h>
 
@@ -86,6 +87,25 @@ VAL idris_time() {
     return MKBIGI(t);
 }
 
+VAL idris_mkFileError(VM* vm) {
+    VAL result;
+    switch(errno) {
+        // Make sure this corresponds to the FileError structure in
+        // Prelude.File
+        case ENOENT:
+            idris_constructor(result, vm, 2, 0, 0);
+            break;
+        case EACCES:
+            idris_constructor(result, vm, 3, 0, 0);
+            break;
+        default:
+            idris_constructor(result, vm, 4, 1, 0);
+            idris_setConArg(result, 0, MKINT((intptr_t)errno));
+            break;
+    }
+    return result;
+}
+
 void idris_forceGC(void* vm) {
    idris_gc((VM*)vm); 
 }

rts/idris_stdfgn.h

@@ -14,6 +14,8 @@ int fileEOF(void* h);
 int fileError(void* h);
 // return 0 on success
 int idris_writeStr(void*h, char* str);
+// construct a file error structure (see Prelude.File) from errno
+VAL idris_mkFileError(VM* vm);
 
 void* do_popen(const char* cmd, const char* mode);
 int fpoll(void* h);

src/Idris/Core/Evaluate.hs

@@ -2,7 +2,8 @@
              PatternGuards #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 
-module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll, toValue, quoteTerm,
+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, 
+                normaliseAll, normaliseBlocking, toValue, quoteTerm,
                 rt_simplify, simplify, specialise, hnf, convEq, convEq',
                 Def(..), CaseInfo(..), CaseDefs(..),
                 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),
@@ -79,11 +80,19 @@ normaliseC ctxt env t
    = evalState (do val <- eval False ctxt [] (map finalEntry env) t []
                    quote 0 val) initEval
 
+-- | Normalise everything, whether abstract, private or public
 normaliseAll :: Context -> Env -> TT Name -> TT Name
 normaliseAll ctxt env t
    = evalState (do val <- eval False ctxt [] (map finalEntry env) t [AtREPL]
                    quote 0 val) initEval
 
+-- | As normaliseAll, but with an explicit list of names *not* to reduce
+normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name
+normaliseBlocking ctxt env blocked t
+   = evalState (do val <- eval False ctxt (map (\n -> (n, 0)) blocked)
+                                          (map finalEntry env) t [AtREPL]
+                   quote 0 val) initEval
+
 normalise :: Context -> Env -> TT Name -> TT Name
 normalise = normaliseTrace False
 

src/Idris/Core/Execute.hs

@@ -349,6 +349,17 @@ execForeign env ctxt arity ty fn xs onfail
                       "The argument to fileEOF should be a file handle, but it was " ++
                       show handle ++
                       ". Are all cases covered?"
+    | Just (FFun "fileError" [(_,handle)] _) <- foreignFromTT arity ty fn xs
+           = case handle of
+             -- errors handled differently in Haskell than in C, so if
+             -- there's been an error we'll have had an exception already.
+             -- Therefore, assume we're okay.
+               EHandle h -> do let res = ioWrap (EConstant (I 0))
+                               execApp env ctxt res (drop arity xs)
+               _ -> execFail . Msg $
+                      "The argument to fileError should be a file handle, but it was " ++
+                      show handle ++
+                      ". Are all cases covered?"
     | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs
            = case handle of
                EHandle h -> do execIO $ hClose h

src/Idris/REPL.hs

@@ -805,7 +805,11 @@ process fn (Eval t)
                       getIState >>= flip warnDisamb t
                       (tm, ty) <- elabREPL recinfo ERHS t
                       ctxt <- getContext
-                      let tm' = perhapsForce $ normaliseAll ctxt [] tm
+                      let tm' = perhapsForce $ normaliseBlocking ctxt [] 
+                                                  [sUN "foreign",
+                                                   sUN "prim_read",
+                                                   sUN "prim_write"]
+                                                 tm
                       let ty' = perhapsForce $ normaliseAll ctxt [] ty
                       -- Add value to context, call it "it"
                       updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
@@ -813,7 +817,8 @@ process fn (Eval t)
                       logLvl 3 $ "Raw: " ++ show (tm', ty')
                       logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
                       let tmDoc = pprintDelab ist tm'
-                          tyDoc =  pprintDelab ist ty'
+                          -- errReverse to make type more readable
+                          tyDoc =  pprintDelab ist (errReverse ist ty')
                       iPrintTermWithType tmDoc tyDoc
   where perhapsForce tm | termSmallerThan 100 tm = force tm
                         | otherwise = tm

test/dsl002/test014.idr

@@ -15,16 +15,17 @@ syntax "ifM" [test] "then" [t] "else" [e]
     = test >>= (\b => if b then t else e)
 
 open : String -> (p:Purpose) -> Creator (Either () (FILE p))
-open fn p = ioc (do h <- fopen fn (pstring p)
-                    ifM validFile h
-                        then return (Right (OpenH h))
-                        else return (Left ()))
+open fn p = ioc (do Right h <- fopen fn (pstring p)
+                       | Left err => return (Left ())
+                    return (Right (OpenH h)))
 
 close : FILE p -> Updater ()
 close (OpenH h) = iou (closeFile h)
 
 readLine : FILE Reading -> Reader String
-readLine (OpenH h) = ior (fread h)
+readLine (OpenH h) = ior (do Right str <- fread h
+                                   | return ""
+                             return str)
 
 eof : FILE Reading -> Reader Bool
 eof (OpenH h) = ior (feof h)

test/ffi004/test026.idr

@@ -10,7 +10,8 @@ strToType _ = Nat
 
 -- If the file contains "Int", provide Int as a type, otherwise provide Nat
 fromFile : String -> IO (Provider Type)
-fromFile fname = do str <- readFile fname
+fromFile fname = do Right str <- readFile fname
+                          | Left err => return (Provide Void)
                     return (Provide (strToType (trim str)))
 
 %provide (T1 : Type) with fromFile "theType"

test/io001/test004.idr

@@ -8,20 +8,20 @@ mwhile t b = do v <- t
                      False => return ()
 
 dumpFile : String -> IO ()
-dumpFile fn = do { h <- openFile fn Read
+dumpFile fn = do { Right h <- openFile fn Read
                    mwhile (do { -- putStrLn "TEST"
                                 x <- feof h
                                 return (not x) })
-                          (do { l <- fread h
+                          (do { Right l <- fread h
                                 putStr l })
                    closeFile h }
 
 main : IO ()
-main = do { h <- openFile "testfile" Write
+main = do { Right h <- openFile "testfile" Write
             fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"
             closeFile h
             putStrLn "Reading testfile"
-            f <- readFile "testfile"
+            Right f <- readFile "testfile"
             putStrLn f
             putStrLn "---"
             dumpFile "testfile"