5_3_5_Exercises.idr

foldLString : (List String) -> String
foldLString [] = ""
foldLString (x :: xs) = x ++ "\n" ++ foldLString xs

readAndSave : IO ()
readAndSave = do lines <- readToBlank
                 putStrLn "Enter file name:"
                 fileName <- getLine
                 writeFile fileName (foldLString lines)
                 pure ()

subReadVectFile : (handle : File) -> IO (n ** Vect n String)
subReadVectFile handle = do Right x <- fGetLine handle
                            | Left err => pure (_ ** [])
                            isEnd <- fEOF handle
                            if (isEnd)
                              then pure (_ ** [])
                              else do (_ ** xs) <- subReadVectFile handle
                                      pure(_ ** x :: xs)

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do Right h <- openFile filename Read
                           | Left err => pure (_ ** [])
                           result <- subReadVectFile h
                           closeFile h
                           pure(result)