idris-0.10.1: test/io001/test004.idr
module Main
mwhile : (test : IO Bool) -> (body : IO ()) -> IO ()
mwhile t b = do v <- t
case v of
True => do b
mwhile t b
False => return ()
dumpFile : String -> IO ()
dumpFile fn = do { Right h <- openFile fn Read
mwhile (do { -- putStrLn "TEST"
x <- fEOF h
return (not x) })
(do { Right l <- fGetLine h
putStr l })
closeFile h }
main : IO ()
main = do { Right h <- openFile "testfile" WriteTruncate
fPutStr h "Hello!\nWorld!\n...\n3\n4\nLast line\n"
closeFile h
putStrLn "Reading testfile"
Right f <- readFile "testfile"
putStrLn f
putStrLn "---"
dumpFile "testfile"
putStrLn "---"
}