bf4bdcc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Change file operation names

bf4bdccEdwin Brady11 years ago

libs/effects/Effect/File.idr+6−6

compare with master

unifiedsplit

@@ -79,14 +79,14 @@ instance Handler FileIO IO where

79 k True (FH h)

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

81 k () ()

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

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

83 -- Need proper error handling!

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

85 k str (FH h)

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

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

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

88 k () (FH h)

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

89+ handle (FH h) EOF k = do e <- fEOF h

90 k e (FH h)

92instance Handler FileIO (IOExcept a) where

@@ -95,14 +95,14 @@ instance Handler FileIO (IOExcept a) where

95 k True (FH h)

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

97 k () ()

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

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

99 -- Need proper error handling!

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

101 k str (FH h)

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

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

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

104 k () (FH h)

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

105+ handle (FH h) EOF k = do e <- ioe_lift $ fEOF h

106 k e (FH h)

107

108-- -------------------------------------------------------------- [ The Effect ]

libs/prelude/Decidable/Equality.idr+1−1

@@ -178,7 +178,7 @@ instance DecEq Char where

178instance DecEq Integer where

179 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

180 where primitiveEq : x = y

181− primitiveEq = believe_me (Refl {x})

181+ primitiveEq = really_believe_me (Refl {x})

182 postulate primitiveNotEq : x = y -> Void

183

184

libs/prelude/Prelude/File.idr+30−6

@@ -92,7 +92,7 @@ data Mode = Read | Write | ReadWrite

93||| Open a file

94||| @ f the filename

95−||| @ m the mode

95+||| @ m the mode; either Read, Write, or ReadWrite

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

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

98 modeStr Read = "r"

@@ -143,6 +143,13 @@ fread (FHandle h) = do str <- do_fread h

143 then return (Left FileReadError)

144 else return (Right str)

145

146+||| Read a line from a file

147+||| @h a file handle which must be open for reading

148+fGetLine : (h : File) -> IO (Either FileError String)

149+fGetLine = fread

150+

151+%deprecate fread "Use fGetLine instead"

152+

146do_fwrite : Ptr -> String -> IO (Either FileError ())

153do_fwrite : Ptr -> String -> IO (Either FileError ())

147do_fwrite h s = do res <- prim_fwrite h s

154do_fwrite h s = do res <- prim_fwrite h s

148 if (res /= 0)

155 if (res /= 0)

@@ -156,14 +163,31 @@ do_fwrite h s = do res <- prim_fwrite h s

156fwrite : File -> String -> IO (Either FileError ())

163fwrite : File -> String -> IO (Either FileError ())

157fwrite (FHandle h) s = do_fwrite h s

164fwrite (FHandle h) s = do_fwrite h s

158

165

166+||| Write a line to a file

167+||| @h a file handle which must be open for writing

168+||| @str the line to write to the file

169+fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())

170+fPutStr (FHandle h) s = do_fwrite h s

171+

172+fPutStrLn : File -> String -> IO (Either FileError ())

173+fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")

174+

175+%deprecate fwrite "Use fPutStr instead"

176+

159do_feof : Ptr -> IO Int

177do_feof : Ptr -> IO Int

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

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

161

179

162||| Check if a file handle has reached the end

180||| Check if a file handle has reached the end

163−feof : File -> IO Bool

181+fEOF : File -> IO Bool

164−feof (FHandle h) = do eof <- do_feof h

182+fEOF (FHandle h) = do eof <- do_feof h

165 return (not (eof == 0))

183 return (not (eof == 0))

166

184

185+||| Check if a file handle has reached the end

186+feof : File -> IO Bool

187+feof = fEOF

188+

189+%deprecate feof "Use fEOF instead"

190+

167fpoll : File -> IO Bool

191fpoll : File -> IO Bool

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

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

169 return (p > 0)

193 return (p > 0)

@@ -181,8 +205,8 @@ readFile fn = do Right h <- openFile fn Read

181 partial

205 partial

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

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

183 readFile' h contents =

207 readFile' h contents =

184− do x <- feof h

208+ do x <- fEOF h

185− if not x then do Right l <- fread h

209+ if not x then do Right l <- fGetLine h

186 | Left err => return (Left err)

210 | Left err => return (Left err)

187 readFile' h (contents ++ l)

211 readFile' h (contents ++ l)

188 else return (Right contents)

212 else return (Right contents)

@@ -192,6 +216,6 @@ writeFile : (filepath : String) -> (contents : String) ->

192 IO (Either FileError ())

216 IO (Either FileError ())

193writeFile fn contents = do

217writeFile fn contents = do

194 Right h <- openFile fn Write | Left err => return (Left err)

218 Right h <- openFile fn Write | Left err => return (Left err)

195− Right () <- fwrite h contents | Left err => return (Left err)

219+ Right () <- fPutStr h contents | Left err => return (Left err)

196 closeFile h

220 closeFile h

197 return (Right ())

221 return (Right ())

libs/prelude/Prelude/Interactive.idr+2−2

@@ -121,9 +121,9 @@ processHandle : File ->

121 (onEOF : a -> String) ->

122 IO ()

123processHandle h acc onRead onEOF

124− = if !(feof h)

124+ = if !(fEOF h)

125 then putStr (onEOF acc)

126− else do Right x <- fread h

126+ else do Right x <- fGetLine h

127 | Left err => putStr (onEOF acc)

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

129 putStr out

test/dsl002/test014.idr+2−2

@@ -23,12 +23,12 @@ close : FILE p -> Updater ()

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

25readLine : FILE Reading -> Reader String

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

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

27 | return ""

28 return str)

30eof : FILE Reading -> Reader Bool

31−eof (OpenH h) = ior (feof h)

31+eof (OpenH h) = ior (fEOF h)

33syntax rclose [h] = Update close h

34syntax rreadLine [h] = Use readLine h

test/io001/test004.idr+3−3

@@ -10,15 +10,15 @@ mwhile t b = do v <- t

10dumpFile : String -> IO ()

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

12 mwhile (do { -- putStrLn "TEST"

13− x <- feof h

13+ x <- fEOF h

14 return (not x) })

15− (do { Right l <- fread h

15+ (do { Right l <- fGetLine h

16 putStr l })

17 closeFile h }

19main : IO ()

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

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

21+ fPutStr h "Hello!\nWorld!\n...\n3\n4\nLast line\n"

22 closeFile h

23 putStrLn "Reading testfile"

24 Right f <- readFile "testfile"