b1872fb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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.

commitb1872fb1891c9be74d82d2b9a8f5593d686eee7c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 1 Nov 2015, 01:17 (11 years ago) parentad9ef67

17 files changed+180−75

compare with master

unifiedsplit

CHANGELOG+3 libs/contrib/Network/Socket.idr−4 libs/effects/Effect/File.idr+16−12 libs/prelude/IO.idr+3 libs/prelude/Prelude/File.idr+76−45 libs/prelude/Prelude/Interactive.idr+3−1 libs/prelude/Prelude/Show.idr+5 rts/idris_rts.c+9 rts/idris_rts.h+3 rts/idris_stdfgn.c+20 rts/idris_stdfgn.h+2 src/Idris/Core/Evaluate.hs+10−1 src/Idris/Core/Execute.hs+11 src/Idris/REPL.hs+7−2 test/dsl002/test014.idr+6−5 test/ffi004/test026.idr+2−1 test/io001/test004.idr+4−4

CHANGELOG+3

@@ -37,6 +37,9 @@ Library updates

3737 from Effectful programs.

3838* Some constructors that never actually occurred have been removed from

3939 the TT and Raw reflection datatypes in Language.Reflection.

40+* File IO operations (for example openFile/fread/fwrite) now return

41+ 'Either FileError ty' where the return type was previously 'ty' to indicate

42+ that they may fail.

4043

4144Tool updates

4245------------

libs/contrib/Network/Socket.idr−4

@@ -143,10 +143,6 @@ record Socket where

143143 socketType : SocketType

144144 protocalNumber : ProtocolNumber

145145

146−||| Get the C error number

147−getErrno : IO Int

148−getErrno = foreign FFI_C "idrnet_errno" (IO Int)

149−

150146||| Creates a UNIX socket with the given family, socket type and protocol

151147||| number. Returns either a socket or an error.

152148socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)

libs/effects/Effect/File.idr+16−12

@@ -74,29 +74,33 @@ data FileIO : Effect where

7474

7575--- An implementation of the resource access protocol for the IO Context.

7676instance Handler FileIO IO where

77− handle () (Open fname m) k = do h <- openFile fname m

78− valid <- validFile h

79− if valid then k True (FH h)

80− else k False ()

77+ handle () (Open fname m) k = do Right h <- openFile fname m

78+ | Left err => k False ()

79+ k True (FH h)

8180 handle (FH h) Close k = do closeFile h

8281 k () ()

83− handle (FH h) ReadLine k = do str <- fread h

82+ handle (FH h) ReadLine k = do Right str <- fread h

83+ -- Need proper error handling!

84+ | Left err => k "" (FH h)

8485 k str (FH h)

85− handle (FH h) (WriteString str) k = do fwrite h str

86+ handle (FH h) (WriteString str) k = do Right () <- fwrite h str

87+ | Left err => k () (FH h)

8688 k () (FH h)

8789 handle (FH h) EOF k = do e <- feof h

8890 k e (FH h)

8991

9092instance Handler FileIO (IOExcept a) where

91− handle () (Open fname m) k = do h <- ioe_lift $ openFile fname m

92− valid <- ioe_lift $ validFile h

93− if valid then k True (FH h)

94− else k False ()

93+ handle () (Open fname m) k = do Right h <- ioe_lift $ openFile fname m

94+ | Left err => k False ()

95+ k True (FH h)

9596 handle (FH h) Close k = do ioe_lift $ closeFile h

9697 k () ()

97− handle (FH h) ReadLine k = do str <- ioe_lift $ fread h

98+ handle (FH h) ReadLine k = do Right str <- ioe_lift $ fread h

99+ -- Need proper error handling!

100+ | Left err => k "" (FH h)

98101 k str (FH h)

99− handle (FH h) (WriteString str) k = do ioe_lift $ fwrite h str

102+ handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fwrite h str

103+ | Left err => k () (FH h)

100104 k () (FH h)

101105 handle (FH h) EOF k = do e <- ioe_lift $ feof h

102106 k e (FH h)

libs/prelude/IO.idr+3

@@ -198,6 +198,9 @@ namespace IO

198198 forceGC : IO ()

199199 forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

200200

201+ getErrno : IO Int

202+ getErrno = foreign FFI_C "idris_errno" (IO Int)

203+

201204--------- The Javascript/Node FFI

202205

203206

libs/prelude/Prelude/File.idr+76−45

@@ -10,7 +10,8 @@ import Prelude.Cast

1010import Prelude.Bool

1111import Prelude.Basics

1212import Prelude.Classes

13−import Prelude.Monad

13+import Prelude.Either

14+import Prelude.Show

1415import IO

1516

1617%access public

@@ -19,6 +20,31 @@ import IO

1920abstract

2021data File = FHandle Ptr

2122

23+||| An error from a file operation

24+-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure

25+-- the values correspond!

26+data FileError = FileReadError

27+ | FileWriteError

28+ | FileNotFound

29+ | PermissionDenied

30+ | GenericFileError Int -- errno

31+

32+private

33+strError : Int -> String

34+strError err = unsafePerformIO -- yeah, yeah...

35+ (foreign FFI_C "idris_showerror" (Int -> IO String) err)

36+

37+getFileError : IO FileError

38+getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"

39+ (Ptr -> IO (Raw FileError)) prim__vm

40+ return err

41+

42+instance Show FileError where

43+ show Success = "Success"

44+ show FileNotFound = "File Not Found"

45+ show PermissionDenied = "Permission Denied"

46+ show (GenericFileError errno) = strError errno

47+

2248||| Standard input

2349stdin : File

2450stdin = FHandle prim__stdin

@@ -31,6 +57,13 @@ stdout = FHandle prim__stdout

3157stderr : File

3258stderr = FHandle prim__stderr

3359

60+do_ferror : Ptr -> IO Int

61+do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h

62+

63+ferror : File -> IO Bool

64+ferror (FHandle h) = do err <- do_ferror h

65+ return (not (err == 0))

66+

3467||| Call the RTS's file opening function

3568do_fopen : String -> String -> IO Ptr

3669do_fopen f m

@@ -39,12 +72,14 @@ do_fopen f m

3972||| Open a file

4073||| @ f the filename

4174||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)

42−fopen : (f : String) -> (m : String) -> IO File

75+fopen : (f : String) -> (m : String) -> IO (Either FileError File)

4376fopen f m = do h <- do_fopen f m

44− return (FHandle h)

77+ if !(nullPtr h)

78+ then do err <- getFileError

79+ return (Left err)

80+ else return (Right (FHandle h))

4581

4682||| Check whether a file handle is actually a null pointer

47−partial

4883validFile : File -> IO Bool

4984validFile (FHandle h) = do x <- nullPtr h

5085 return (not x)

@@ -55,33 +90,26 @@ data Mode = Read | Write | ReadWrite

5590||| Open a file

5691||| @ f the filename

5792||| @ m the mode

58−partial

59−openFile : (f : String) -> (m : Mode) -> IO File

93+openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)

6094openFile f m = fopen f (modeStr m) where

6195 modeStr Read = "r"

6296 modeStr Write = "w"

6397 modeStr ReadWrite = "r+"

6498

65−partial

6699do_fclose : Ptr -> IO ()

67100do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h

68101

69−partial

70102closeFile : File -> IO ()

71103closeFile (FHandle h) = do_fclose h

72104

73−partial

74105do_fread : Ptr -> IO' l String

75106do_fread h = prim_fread h

76107

77−fgetc : File -> IO Char

78−fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))

79−

80−fgetc' : File -> IO (Maybe Char)

81−fgetc' (FHandle h)

82− = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h

83− if (x < 0) then return Nothing

84− else return (Just (cast x))

108+fgetc : File -> IO (Either FileError Char)

109+fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)

110+ if !(ferror (FHandle h))

111+ then return (Left FileReadError)

112+ else return (Right c)

85113

86114fflush : File -> IO ()

87115fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h

@@ -89,9 +117,12 @@ fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h

89117do_popen : String -> String -> IO Ptr

90118do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m

91119

92−popen : String -> Mode -> IO File

120+popen : String -> Mode -> IO (Either FileError File)

93121popen f m = do ptr <- do_popen f (modeStr m)

94− return (FHandle ptr)

122+ if !(nullPtr ptr)

123+ then do err <- getFileError

124+ return (Left err)

125+ else return (Right (FHandle ptr))

95126 where

96127 modeStr Read = "r"

97128 modeStr Write = "w"

@@ -103,20 +134,25 @@ pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h

103134-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))

104135-- prim__vm h

105136

106−partial

107−fread : File -> IO' l String

108−fread (FHandle h) = do_fread h

109−

110−partial

111−do_fwrite : Ptr -> String -> IO ()

112−do_fwrite h s = do prim_fwrite h s

113− return ()

114−

115−partial

116−fwrite : File -> String -> IO ()

137+fread : File -> IO (Either FileError String)

138+fread (FHandle h) = do str <- do_fread h

139+ if !(ferror (FHandle h))

140+ then return (Left FileReadError)

141+ else return (Right str)

142+

143+do_fwrite : Ptr -> String -> IO (Either FileError ())

144+do_fwrite h s = do res <- prim_fwrite h s

145+ if (res /= 0)

146+ then do errno <- getErrno

147+ if errno == 0

148+ then return (Left FileWriteError)

149+ else do err <- getFileError

150+ return (Left err)

151+ else return (Right ())

152+

153+fwrite : File -> String -> IO (Either FileError ())

117154fwrite (FHandle h) s = do_fwrite h s

118155

119−partial

120156do_feof : Ptr -> IO Int

121157do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h

122158

@@ -125,32 +161,27 @@ feof : File -> IO Bool

125161feof (FHandle h) = do eof <- do_feof h

126162 return (not (eof == 0))

127163

128−partial

129−do_ferror : Ptr -> IO Int

130−do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h

131−

132−ferror : File -> IO Bool

133−ferror (FHandle h) = do err <- do_ferror h

134− return (not (err == 0))

135−

136164fpoll : File -> IO Bool

137165fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

138166 return (p > 0)

139167

140168||| Read the contents of a file into a string

141−partial -- no error checking!

142−readFile : String -> IO String

143−readFile fn = do h <- openFile fn Read

169+partial -- might be reading something infinitely long like /dev/null ...

170+covering

171+readFile : String -> IO (Either FileError String)

172+readFile fn = do Right h <- openFile fn Read

173+ | Left err => return (Left err)

144174 c <- readFile' h ""

145175 closeFile h

146176 return c

147177 where

148178 partial

149− readFile' : File -> String -> IO String

179+ readFile' : File -> String -> IO (Either FileError String)

150180 readFile' h contents =

151181 do x <- feof h

152− if not x then do l <- fread h

182+ if not x then do Right l <- fread h

183+ | Left err => return (Left err)

153184 readFile' h (contents ++ l)

154− else return contents

185+ else return (Right contents)

155186

156187

libs/prelude/Prelude/Interactive.idr+3−1

@@ -17,6 +17,7 @@ import Prelude.Show

1717import Prelude.Cast

1818import Prelude.Maybe

1919import Prelude.Functor

20+import Prelude.Either

2021import Prelude.Monad

2122import IO

2223

@@ -97,7 +98,8 @@ processHandle : File ->

9798processHandle h acc onRead onEOF

9899 = if !(feof h)

99100 then putStr (onEOF acc)

100− else do x <- fread h

101+ else do Right x <- fread h

102+ | Left err => putStr (onEOF acc)

101103 let (out, acc') = onRead acc x

102104 putStr out

103105 processHandle h acc' onRead onEOF

libs/prelude/Prelude/Show.idr+5

@@ -10,6 +10,7 @@ import Prelude.Chars

1010import Prelude.Classes

1111import Prelude.List

1212import Prelude.Maybe

13+import Prelude.Either

1314import Prelude.Nat

1415import Prelude.Strings

1516

@@ -185,6 +186,10 @@ instance Show a => Show (Maybe a) where

185186 showPrec d Nothing = "Nothing"

186187 showPrec d (Just x) = showCon d "Just" $ showArg x

187188

189+instance (Show a, Show b) => Show (Either a b) where

190+ showPrec d (Left x) = showCon d "Left" $ showArg x

191+ showPrec d (Right x) = showCon d "Right" $ showArg x

192+

188193instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

189194 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

190195

rts/idris_rts.c+9

@@ -1,4 +1,5 @@

11#include <assert.h>

2+#include <errno.h>

34#include "idris_rts.h"

45#include "idris_gc.h"

@@ -934,6 +935,14 @@ void idris_freeMsg(Msg* msg) {

934935 free(msg);

935936}

936937

938+int idris_errno() {

939+ return errno;

940+}

941+

942+char* idris_showerror(int err) {

943+ return strerror(err);

944+}

945+

937946VAL* nullary_cons;

938947

939948void init_nullaries() {

rts/idris_rts.h+3

@@ -255,6 +255,9 @@ void idris_free(void* ptr, size_t size);

255255

256256#define NULL_CON(x) nullary_cons[x]

257257

258+int idris_errno();

259+char* idris_showerror(int err);

260+

258261extern VAL* nullary_cons;

259262void init_nullaries();

260263void free_nullaries();

rts/idris_stdfgn.c+20

@@ -4,6 +4,7 @@

44#include "idris_gc.h"

55#include <sys/select.h>

66#include <fcntl.h>

7+#include <errno.h>

78#include <stdio.h>

89#include <time.h>

910

@@ -86,6 +87,25 @@ VAL idris_time() {

8687 return MKBIGI(t);

8788}

8889

90+VAL idris_mkFileError(VM* vm) {

91+ VAL result;

92+ switch(errno) {

93+ // Make sure this corresponds to the FileError structure in

94+ // Prelude.File

95+ case ENOENT:

96+ idris_constructor(result, vm, 2, 0, 0);

97+ break;

98+ case EACCES:

99+ idris_constructor(result, vm, 3, 0, 0);

100+ break;

101+ default:

102+ idris_constructor(result, vm, 4, 1, 0);

103+ idris_setConArg(result, 0, MKINT((intptr_t)errno));

104+ break;

105+ }

106+ return result;

107+}

108+

89109void idris_forceGC(void* vm) {

90110 idris_gc((VM*)vm);

91111}

rts/idris_stdfgn.h+2

@@ -14,6 +14,8 @@ int fileEOF(void* h);

1414int fileError(void* h);

1515// return 0 on success

1616int idris_writeStr(void*h, char* str);

17+// construct a file error structure (see Prelude.File) from errno

18+VAL idris_mkFileError(VM* vm);

1719

1820void* do_popen(const char* cmd, const char* mode);

1921int fpoll(void* h);

src/Idris/Core/Evaluate.hs+10−1

@@ -2,7 +2,8 @@

22 PatternGuards #-}

33{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

5−module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll, toValue, quoteTerm,

5+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

6+ normaliseAll, normaliseBlocking, toValue, quoteTerm,

67 rt_simplify, simplify, specialise, hnf, convEq, convEq',

78 Def(..), CaseInfo(..), CaseDefs(..),

89 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

@@ -79,11 +80,19 @@ normaliseC ctxt env t

7980 = evalState (do val <- eval False ctxt [] (map finalEntry env) t []

8081 quote 0 val) initEval

8182

83+-- | Normalise everything, whether abstract, private or public

8284normaliseAll :: Context -> Env -> TT Name -> TT Name

8385normaliseAll ctxt env t

8486 = evalState (do val <- eval False ctxt [] (map finalEntry env) t [AtREPL]

8587 quote 0 val) initEval

8688

89+-- | As normaliseAll, but with an explicit list of names *not* to reduce

90+normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name

91+normaliseBlocking ctxt env blocked t

92+ = evalState (do val <- eval False ctxt (map (\n -> (n, 0)) blocked)

93+ (map finalEntry env) t [AtREPL]

94+ quote 0 val) initEval

95+

8796normalise :: Context -> Env -> TT Name -> TT Name

8897normalise = normaliseTrace False

8998

src/Idris/Core/Execute.hs+11

@@ -349,6 +349,17 @@ execForeign env ctxt arity ty fn xs onfail

349349 "The argument to fileEOF should be a file handle, but it was " ++

350350 show handle ++

351351 ". Are all cases covered?"

352+ | Just (FFun "fileError" [(_,handle)] _) <- foreignFromTT arity ty fn xs

353+ = case handle of

354+ -- errors handled differently in Haskell than in C, so if

355+ -- there's been an error we'll have had an exception already.

356+ -- Therefore, assume we're okay.

357+ EHandle h -> do let res = ioWrap (EConstant (I 0))

358+ execApp env ctxt res (drop arity xs)

359+ _ -> execFail . Msg $

360+ "The argument to fileError should be a file handle, but it was " ++

361+ show handle ++

362+ ". Are all cases covered?"

352363 | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs

353364 = case handle of

354365 EHandle h -> do execIO $ hClose h

src/Idris/REPL.hs+7−2

@@ -805,7 +805,11 @@ process fn (Eval t)

805805 getIState >>= flip warnDisamb t

806806 (tm, ty) <- elabREPL recinfo ERHS t

807807 ctxt <- getContext

808− let tm' = perhapsForce $ normaliseAll ctxt [] tm

808+ let tm' = perhapsForce $ normaliseBlocking ctxt []

809+ [sUN "foreign",

810+ sUN "prim_read",

811+ sUN "prim_write"]

812+ tm

809813 let ty' = perhapsForce $ normaliseAll ctxt [] ty

810814 -- Add value to context, call it "it"

811815 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))

@@ -813,7 +817,8 @@ process fn (Eval t)

813817 logLvl 3 $ "Raw: " ++ show (tm', ty')

814818 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

815819 let tmDoc = pprintDelab ist tm'

816− tyDoc = pprintDelab ist ty'

820+ -- errReverse to make type more readable

821+ tyDoc = pprintDelab ist (errReverse ist ty')

817822 iPrintTermWithType tmDoc tyDoc

818823 where perhapsForce tm | termSmallerThan 100 tm = force tm

819824 | otherwise = tm

test/dsl002/test014.idr+6−5

@@ -15,16 +15,17 @@ syntax "ifM" [test] "then" [t] "else" [e]

1515 = test >>= (\b => if b then t else e)

1616

1717open : String -> (p:Purpose) -> Creator (Either () (FILE p))

18−open fn p = ioc (do h <- fopen fn (pstring p)

19− ifM validFile h

20− then return (Right (OpenH h))

21− else return (Left ()))

18+open fn p = ioc (do Right h <- fopen fn (pstring p)

19+ | Left err => return (Left ())

20+ return (Right (OpenH h)))

2221

2322close : FILE p -> Updater ()

2423close (OpenH h) = iou (closeFile h)

2524

2625readLine : FILE Reading -> Reader String

27−readLine (OpenH h) = ior (fread h)

26+readLine (OpenH h) = ior (do Right str <- fread h

27+ | return ""

28+ return str)

2829

2930eof : FILE Reading -> Reader Bool

3031eof (OpenH h) = ior (feof h)

test/ffi004/test026.idr+2−1

@@ -10,7 +10,8 @@ strToType _ = Nat

1010

1111-- If the file contains "Int", provide Int as a type, otherwise provide Nat

1212fromFile : String -> IO (Provider Type)

13−fromFile fname = do str <- readFile fname

13+fromFile fname = do Right str <- readFile fname

14+ | Left err => return (Provide Void)

1415 return (Provide (strToType (trim str)))

1516

1617%provide (T1 : Type) with fromFile "theType"

test/io001/test004.idr+4−4

@@ -8,20 +8,20 @@ mwhile t b = do v <- t

88 False => return ()

1010dumpFile : String -> IO ()

11−dumpFile fn = do { h <- openFile fn Read

11+dumpFile fn = do { Right h <- openFile fn Read

1212 mwhile (do { -- putStrLn "TEST"

1313 x <- feof h

1414 return (not x) })

15− (do { l <- fread h

15+ (do { Right l <- fread h

1616 putStr l })

1717 closeFile h }

1818

1919main : IO ()

20−main = do { h <- openFile "testfile" Write

20+main = do { Right h <- openFile "testfile" Write

2121 fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"

2222 closeFile h

2323 putStrLn "Reading testfile"

24− f <- readFile "testfile"

24+ Right f <- readFile "testfile"

2525 putStrLn f

2626 putStrLn "---"

2727 dumpFile "testfile"