module System.File import Data.Listimport Data.Strings public exportdata Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend public exportFilePtr : TypeFilePtr = AnyPtr support : String -> Stringsupport fn = "C:" ++ fn ++ ", libidris2_support" libc : String -> Stringlibc fn = "C:" ++ fn ++ ", libc 6" %foreign support "idris2_openFile"prim__open : String -> String -> Int -> PrimIO FilePtr%foreign support "idris2_closeFile"prim__close : FilePtr -> PrimIO () %foreign support "idris2_fileError"prim_error : FilePtr -> PrimIO Int%foreign support "idris2_fileErrno"prim_fileErrno : PrimIO Int %foreign support "idris2_readLine"prim__readLine : FilePtr -> PrimIO (Ptr String)%foreign support "idris2_readChars"prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)%foreign support "fgetc"prim__readChar : FilePtr -> PrimIO Char%foreign support "idris2_writeLine"prim__writeLine : FilePtr -> String -> PrimIO Int%foreign support "idris2_eof"prim__eof : FilePtr -> PrimIO Int%foreign "C:fflush,libc 6"prim__flush : FilePtr -> PrimIO Int %foreign support "idris2_fileRemove"prim__fileRemove : String -> PrimIO Int%foreign support "idris2_fileSize"prim__fileSize : FilePtr -> PrimIO Int%foreign support "idris2_fileSize"prim__fPoll : FilePtr -> PrimIO Int %foreign support "idris2_fileAccessTime"prim__fileAccessTime : FilePtr -> PrimIO Int%foreign support "idris2_fileModifiedTime"prim__fileModifiedTime : FilePtr -> PrimIO Int%foreign support "idris2_fileStatusTime"prim__fileStatusTime : FilePtr -> PrimIO Int %foreign support "idris2_stdin"prim__stdin : FilePtr%foreign support "idris2_stdout"prim__stdout : FilePtr%foreign support "idris2_stderr"prim__stderr : FilePtr %foreign libc "chmod"prim__chmod : String -> Int -> PrimIO Int 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 returnError : IO (Either FileError a)returnError    = do err <- primIO prim_fileErrno         case err of              0 => pure $ Left FileReadError              1 => pure $ Left FileWriteError              2 => pure $ Left FileNotFound              3 => pure $ Left PermissionDenied              4 => pure $ Left FileExists              _ => pure $ Left (GenericFileError (err-5)) 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" ok : a -> IO (Either FileError a)ok x = pure (Right x) public exportdata File : Type where     FHandle : FilePtr -> File 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)         if prim__nullAnyPtr res /= 0            then returnError            else ok (FHandle res) exportcloseFile : File -> IO ()closeFile (FHandle f) = primIO (prim__close f) exportfileError : File -> IO BoolfileError (FHandle f)    = do x <- primIO $ prim_error f         pure (x /= 0) exportfGetLine : (h : File) -> IO (Either FileError String)fGetLine (FHandle f)    = do res <- primIO (prim__readLine f)         if prim__nullPtr res /= 0            then returnError            else ok (prim__getString res) exportfGetChars : (h : File) -> Int -> IO (Either FileError String)fGetChars (FHandle f) max    = do res <- primIO (prim__readChars max f)         if prim__nullPtr res /= 0            then returnError            else ok (prim__getString res) exportfGetChar : (h : File) -> IO (Either FileError Char)fGetChar (FHandle h)    = do c <- primIO (prim__readChar h)         ferr <- primIO (prim_error h)         if (ferr /= 0)            then returnError            else ok c exportfPutStr : (h : File) -> String -> IO (Either FileError ())fPutStr (FHandle f) str    = do res <- primIO (prim__writeLine f str)         if res == 0            then returnError            else ok () 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) exportfflush : (h : File) -> IO ()fflush (FHandle f)    = do primIO (prim__flush f)         pure () exportfileAccessTime : (h : File) -> IO (Either FileError Int)fileAccessTime (FHandle f)    = do res <- primIO (prim__fileAccessTime f)         if res > 0            then ok res            else returnError exportfileModifiedTime : (h : File) -> IO (Either FileError Int)fileModifiedTime (FHandle f)    = do res <- primIO (prim__fileModifiedTime f)         if res > 0            then ok res            else returnError exportfileStatusTime : (h : File) -> IO (Either FileError Int)fileStatusTime (FHandle f)    = do res <- primIO (prim__fileStatusTime f)         if res > 0            then ok res            else returnError exportfileRemove : String -> IO (Either FileError ())fileRemove fname    = do res <- primIO (prim__fileRemove fname)         if res == 0            then ok ()            else returnError exportfileSize : (h : File) -> IO (Either FileError Int)fileSize (FHandle f)    = do res <- primIO (prim__fileSize f)         if res >= 0            then ok res            else returnError exportfPoll : File -> IO BoolfPoll (FHandle f)    = do p <- primIO (prim__fPoll f)         pure (p > 0) exportreadFile : String -> IO (Either FileError String)readFile file  = do Right h <- openFile file Read          | Left err => returnError       Right content <- read [] h          | Left err => do closeFile h                           returnError       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 => returnError                     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 ()) namespace FileMode   public export  data FileMode = Read | Write | Execute public exportrecord Permissions where  constructor MkPermissions  user   : List FileMode  group  : List FileMode  others : List FileMode mkMode : Permissions -> IntmkMode p    = getMs (user p) * 64 + getMs (group p) * 8 + getMs (others p)  where    getM : FileMode -> Int    getM Read = 4    getM Write = 2    getM Execute = 1     getMs : List FileMode -> Int    getMs = sum . map getM exportchmodRaw : String -> Int -> IO (Either FileError ())chmodRaw fname p    = do ok <- primIO $ prim__chmod fname p         if ok == 0            then pure (Right ())            else returnError exportchmod : String -> Permissions -> IO (Either FileError ())chmod fname p = chmodRaw fname (mkMode p)