ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 14:09:30 +03:00
Code Issues Projects Releases Wiki Activity

Change file operation names

Browse Source 
Old names still work with a deprecation warning. New names are intended
to be more self consistent.
This commit is contained in:
Edwin Brady 2015-12-14 20:14:03 +00:00
parent 75aa4df79f
commit bf4bdcc31e
6 changed files with 44 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libs/effects/Effect/File.idr
View File

@ -79,14 +79,14 @@ instance Handler FileIO IO where
k True (FH h)
handle (FH h) Close k = do closeFile h
k () ()
handle (FH h) ReadLine k = do Right str <- fread h
handle (FH h) ReadLine k = do Right str <- fGetStr h
-- Need proper error handling!
| Left err => k "" (FH h)
k str (FH h)
handle (FH h) (WriteString str) k = do Right () <- fwrite h str
handle (FH h) (WriteString str) k = do Right () <- fPutStr h str
| Left err => k () (FH h)
k () (FH h)
handle (FH h) EOF k = do e <- feof h
handle (FH h) EOF k = do e <- fEOF h
k e (FH h)
instance Handler FileIO (IOExcept a) where
@ -95,14 +95,14 @@ instance Handler FileIO (IOExcept a) where
k True (FH h)
handle (FH h) Close k = do ioe_lift $ closeFile h
k () ()
handle (FH h) ReadLine k = do Right str <- ioe_lift $ fread h
handle (FH h) ReadLine k = do Right str <- ioe_lift $ fGetStr h
-- Need proper error handling!
| Left err => k "" (FH h)
k str (FH h)
handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fwrite h str
handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fPutStr h str
| Left err => k () (FH h)
k () (FH h)
handle (FH h) EOF k = do e <- ioe_lift $ feof h
handle (FH h) EOF k = do e <- ioe_lift $ fEOF h
k e (FH h)
-- -------------------------------------------------------------- [ The Effect ]

2
libs/prelude/Decidable/Equality.idr
View File

@ -178,7 +178,7 @@ instance DecEq Char where
instance DecEq Integer where
decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
where primitiveEq : x = y
primitiveEq = believe_me (Refl {x})
primitiveEq = really_believe_me (Refl {x})
postulate primitiveNotEq : x = y -> Void

36
libs/prelude/Prelude/File.idr
View File

@ -92,7 +92,7 @@ data Mode = Read | Write | ReadWrite
||| Open a file
||| @ f the filename
||| @ m the mode
||| @ m the mode; either Read, Write, or ReadWrite
openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
openFile f m = fopen f (modeStr m) where
modeStr Read = "r"
@ -143,6 +143,13 @@ fread (FHandle h) = do str <- do_fread h
then return (Left FileReadError)
else return (Right str)
||| Read a line from a file
||| @h a file handle which must be open for reading
fGetLine : (h : File) -> IO (Either FileError String)
fGetLine = fread
%deprecate fread "Use fGetLine instead"
do_fwrite : Ptr -> String -> IO (Either FileError ())
do_fwrite h s = do res <- prim_fwrite h s
if (res /= 0)
@ -156,14 +163,31 @@ do_fwrite h s = do res <- prim_fwrite h s
fwrite : File -> String -> IO (Either FileError ())
fwrite (FHandle h) s = do_fwrite h s
||| Write a line to a file
||| @h a file handle which must be open for writing
||| @str the line to write to the file
fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
fPutStr (FHandle h) s = do_fwrite h s
fPutStrLn : File -> String -> IO (Either FileError ())
fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")
%deprecate fwrite "Use fPutStr instead"
do_feof : Ptr -> IO Int
do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
||| Check if a file handle has reached the end
feof : File -> IO Bool
feof (FHandle h) = do eof <- do_feof h
fEOF : File -> IO Bool
fEOF (FHandle h) = do eof <- do_feof h
return (not (eof == 0))
||| Check if a file handle has reached the end
feof : File -> IO Bool
feof = fEOF
%deprecate feof "Use fEOF instead"
fpoll : File -> IO Bool
fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
return (p > 0)
@ -181,8 +205,8 @@ readFile fn = do Right h <- openFile fn Read
partial
readFile' : File -> String -> IO (Either FileError String)
readFile' h contents =
do x <- feof h
if not x then do Right l <- fread h
do x <- fEOF h
if not x then do Right l <- fGetLine h
| Left err => return (Left err)
readFile' h (contents ++ l)
else return (Right contents)
@ -192,6 +216,6 @@ writeFile : (filepath : String) -> (contents : String) ->
IO (Either FileError ())
writeFile fn contents = do
Right h <- openFile fn Write | Left err => return (Left err)
Right () <- fwrite h contents | Left err => return (Left err)
Right () <- fPutStr h contents | Left err => return (Left err)
closeFile h
return (Right ())

4
libs/prelude/Prelude/Interactive.idr
View File

@ -121,9 +121,9 @@ processHandle : File ->
(onEOF : a -> String) ->
IO ()
processHandle h acc onRead onEOF
= if !(feof h)
= if !(fEOF h)
then putStr (onEOF acc)
else do Right x <- fread h
else do Right x <- fGetLine h
| Left err => putStr (onEOF acc)
let (out, acc') = onRead acc x
putStr out

4
test/dsl002/test014.idr
View File

@ -23,12 +23,12 @@ close : FILE p -> Updater ()
close (OpenH h) = iou (closeFile h)
readLine : FILE Reading -> Reader String
readLine (OpenH h) = ior (do Right str <- fread h
readLine (OpenH h) = ior (do Right str <- fGetLine h
| return ""
return str)
eof : FILE Reading -> Reader Bool
eof (OpenH h) = ior (feof h)
eof (OpenH h) = ior (fEOF h)
syntax rclose [h] = Update close h
syntax rreadLine [h] = Use readLine h

6
test/io001/test004.idr
View File

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