module System.File import Data.Listimport Data.Strings public exportdata Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend public exportdata FilePtr : Type where %extern prim__open : String -> String -> Int ->                     (1 x : %World) -> IORes (Either Int FilePtr)%extern prim__close : FilePtr -> (1 x : %World) -> IORes ()%extern prim__readLine : FilePtr -> (1 x : %World) -> IORes (Either Int String)%extern prim__writeLine : FilePtr -> String -> (1 x : %World) -> IORes (Either Int ())%extern prim__eof : FilePtr -> (1 x : %World) -> IORes Int %extern prim__fileModifiedTime : FilePtr -> (1 x : %World) ->                                 IORes (Either Int Integer) %extern prim__stdin : FilePtr%extern prim__stdout : FilePtr%extern prim__stderr : FilePtr modeStr : Mode -> StringmodeStr Read              = "r"modeStr WriteTruncate     = "w"modeStr Append            = "a"modeStr ReadWrite         = "r+"modeStr ReadWriteTruncate = "w+"modeStr ReadAppend        = "a+" public exportdata FileError = GenericFileError Int -- errno               | FileReadError               | FileWriteError               | FileNotFound               | PermissionDenied               | FileExists exportShow FileError where  show (GenericFileError errno) = "File error: " ++ show errno  show FileReadError = "File Read Error"  show FileWriteError = "File Write Error"  show FileNotFound = "File Not Found"  show PermissionDenied = "Permission Denied"  show FileExists = "File Exists" toFileError : Int -> FileErrortoFileError 1 = FileReadErrortoFileError 2 = FileWriteErrortoFileError 3 = FileNotFoundtoFileError 4 = PermissionDeniedtoFileError x = GenericFileError (x - 256) fpure : Either Int a -> IO (Either FileError a)fpure (Left err) = pure (Left (toFileError err))fpure (Right x) = pure (Right x) public exportdata FileT : Bool -> Type where     FHandle : FilePtr -> FileT bin public exportFile : TypeFile = FileT False public exportBinaryFile : TypeBinaryFile = FileT True exportstdin : Filestdin = FHandle prim__stdin exportstdout : Filestdout = FHandle prim__stdout exportstderr : Filestderr = FHandle prim__stderr exportopenFile : String -> Mode -> IO (Either FileError File)openFile f m    = do res <- primIO (prim__open f (modeStr m) 0)         fpure (map FHandle res) exportopenBinaryFile : String -> Mode -> IO (Either FileError BinaryFile)openBinaryFile f m    = do res <- primIO (prim__open f (modeStr m) 1)         fpure (map FHandle res) exportcloseFile : FileT t -> IO ()closeFile (FHandle f) = primIO (prim__close f) exportfGetLine : (h : File) -> IO (Either FileError String)fGetLine (FHandle f)    = do res <- primIO (prim__readLine f)         fpure res exportfPutStr : (h : File) -> String -> IO (Either FileError ())fPutStr (FHandle f) str    = do res <- primIO (prim__writeLine f str)         fpure res exportfPutStrLn : (h : File) -> String -> IO (Either FileError ())fPutStrLn f str = fPutStr f (str ++ "\n") exportfEOF : (h : File) -> IO BoolfEOF (FHandle f)    = do res <- primIO (prim__eof f)         pure (res /= 0) exportfileModifiedTime : (h : File) -> IO (Either FileError Integer)fileModifiedTime (FHandle f)    = do res <- primIO (prim__fileModifiedTime f)         fpure res exportreadFile : String -> IO (Either FileError String)readFile file  = do Right h <- openFile file Read          | Left err => pure (Left err)       Right content <- read [] h          | Left err => do closeFile h                           pure (Left err)       closeFile h       pure (Right (fastAppend content))  where    read : List String -> File -> IO (Either FileError (List String))    read acc h        = do eof <- fEOF h             if eof                then pure (Right (reverse acc))                else                  do Right str <- fGetLine h                        | Left err => pure (Left err)                     read (str :: acc) h ||| Write a string to a fileexportwriteFile : (filepath : String) -> (contents : String) ->            IO (Either FileError ())writeFile fn contents = do     Right h  <- openFile fn WriteTruncate        | Left err => pure (Left err)     Right () <- fPutStr h contents        | Left err => do closeFile h                         pure (Left err)     closeFile h     pure (Right ())