ex_5_3_5.idr

import Data.Vect

readToBlank : IO (List String)
readToBlank = do x <- getLine
                 if (x == "")
                    then pure []
                    else do xs <- readToBlank
                            pure (x :: xs)

readAndSave : IO ()
readAndSave = do xs <- readToBlank
                 filename <- getLine
                 Right h <- writeFile filename (unlines xs)
                   | Left err => putStrLn (show err)
                 pure ()
                                                   
readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename =
  do
    Right h <- openFile filename Read
    | Left err => pure (_ ** [])
    lines <- readFileLines h
    pure lines 
  where
    readFileLines: (h: File) -> IO (n ** Vect n String)
    readFileLines h =
      do isEnd <- fEOF h
         if (isEnd)
           then do closeFile h
                   pure (_ ** [])
           else do Right line <- fGetLine h
                   | Left err => pure (_ ** [])
                   (_ ** lines) <- readFileLines h
                   pure (_ ** line :: lines)