bf4bdcc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change file operation names

Old names still work with a deprecation warning. New names are intended to be more self consistent.

commitbf4bdcc31ed1ac8cced32fad42d40984296da2a7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 14 Dec 2015, 20:14 (11 years ago) parent75aa4df

6 files changed+44−20

compare with master

unifiedsplit

libs/effects/Effect/File.idr+6−6 libs/prelude/Decidable/Equality.idr+1−1 libs/prelude/Prelude/File.idr+30−6 libs/prelude/Prelude/Interactive.idr+2−2 test/dsl002/test014.idr+2−2 test/io001/test004.idr+3−3

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

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

7979 k True (FH h)

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

8181 k () ()

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

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

8383 -- Need proper error handling!

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

8585 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

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

8888 k () (FH h)

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

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

9090 k e (FH h)

9191

9292instance Handler FileIO (IOExcept a) where

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

9595 k True (FH h)

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

9797 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

9999 -- Need proper error handling!

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

101101 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

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

104104 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

106106 k e (FH h)

107107

108108-- -------------------------------------------------------------- [ The Effect ]

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

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

178178instance DecEq Integer where

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

180180 where primitiveEq : x = y

181− primitiveEq = believe_me (Refl {x})

181+ primitiveEq = really_believe_me (Refl {x})

182182 postulate primitiveNotEq : x = y -> Void

183183

184184

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

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

9292

9393||| Open a file

9494||| @ f the filename

95−||| @ m the mode

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

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

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

9898 modeStr Read = "r"

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

143143 then return (Left FileReadError)

144144 else return (Right str)

145145

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+

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

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

148155 if (res /= 0)

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

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

157164fwrite (FHandle h) s = do_fwrite h s

158165

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+

159177do_feof : Ptr -> IO Int

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

161179

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

163−feof : File -> IO Bool

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

181+fEOF : File -> IO Bool

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

165183 return (not (eof == 0))

166184

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+

167191fpoll : File -> IO Bool

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

169193 return (p > 0)

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

181205 partial

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

183207 readFile' h contents =

184− do x <- feof h

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

208+ do x <- fEOF h

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

186210 | Left err => return (Left err)

187211 readFile' h (contents ++ l)

188212 else return (Right contents)

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

192216 IO (Either FileError ())

193217writeFile fn contents = do

194218 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)

196220 closeFile h

197221 return (Right ())

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

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

121121 (onEOF : a -> String) ->

122122 IO ()

123123processHandle h acc onRead onEOF

124− = if !(feof h)

124+ = if !(fEOF h)

125125 then putStr (onEOF acc)

126− else do Right x <- fread h

126+ else do Right x <- fGetLine h

127127 | Left err => putStr (onEOF acc)

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

129129 putStr out

test/dsl002/test014.idr+2−2

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

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

2424

2525readLine : FILE Reading -> Reader String

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

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

2727 | return ""

2828 return str)

2929

3030eof : FILE Reading -> Reader Bool

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

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

3232

3333syntax rclose [h] = Update close h

3434syntax rreadLine [h] = Use readLine h

test/io001/test004.idr+3−3

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

1010dumpFile : String -> IO ()

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

1212 mwhile (do { -- putStrLn "TEST"

13− x <- feof h

13+ x <- fEOF h

1414 return (not x) })

15− (do { Right l <- fread h

15+ (do { Right l <- fGetLine h

1616 putStr l })

1717 closeFile h }

1818

1919main : IO ()

2020main = 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"

2222 closeFile h

2323 putStrLn "Reading testfile"

2424 Right f <- readFile "testfile"