Idris2Doc : System.File

System.File

File : Type
Totality: total
Constructor: 
FHandle : FilePtr -> File
FileError : Type
Totality: total
Constructors:
GenericFileError : Int -> FileError
FileReadError : FileError
FileWriteError : FileError
FileNotFound : FileError
PermissionDenied : FileError
FileExists : FileError
FilePtr : Type
Totality: total
Mode : Type
Totality: total
Constructors:
Read : Mode
WriteTruncate : Mode
Append : Mode
ReadWrite : Mode
ReadWriteTruncate : Mode
ReadAppend : Mode
Permissions : Type
Totality: total
Constructor: 
chmod : HasIOio => String -> Permissions -> io (EitherFileErrorUnit)
Totality: total
chmodRaw : HasIOio => String -> Int -> io (EitherFileErrorUnit)
Totality: total
closeFile : HasIOio => File -> ioUnit
Totality: total
exists : HasIOio => String -> ioBool
Check if a file exists for reading.
Totality: total
fEOF : HasIOio => File -> ioBool
Totality: total
fGetChar : HasIOio => File -> io (EitherFileError Char)
Totality: total
fGetChars : HasIOio => File -> Int -> io (EitherFileError String)
Totality: total
fGetLine : HasIOio => File -> io (EitherFileError String)
Totality: total
fPoll : HasIOio => File -> ioBool
Totality: total
fPutStr : HasIOio => File -> String -> io (EitherFileErrorUnit)
Totality: total
fPutStrLn : HasIOio => File -> String -> io (EitherFileErrorUnit)
Totality: total
fSeekLine : HasIOio => File -> io (EitherFileErrorUnit)
Seek through the next newline.
This is @fGetLine@ without the overhead of copying
any characters.
Totality: total
fflush : HasIOio => File -> ioUnit
Totality: total
fileAccessTime : HasIOio => File -> io (EitherFileError Int)
Totality: total
fileError : HasIOio => File -> ioBool
Totality: total
fileModifiedTime : HasIOio => File -> io (EitherFileError Int)
Totality: total
fileSize : HasIOio => File -> io (EitherFileError Int)
Totality: total
fileStatusTime : HasIOio => File -> io (EitherFileError Int)
Totality: total
firstExists : HasIOio => List String -> io (Maybe String)
Pick the first existing file
Totality: total
openFile : HasIOio => String -> Mode -> io (EitherFileErrorFile)
Totality: total
pclose : HasIOio => File -> ioUnit
Totality: total
popen : HasIOio => String -> Mode -> io (EitherFileErrorFile)
Totality: total
readFile : HasIOio => String -> io (EitherFileError String)
readFilePage : HasIOio => Nat -> Fuel -> String -> io (EitherFileError (Bool, List String))
Read a chunk of a file in a line-delimited fashion.
You can use this function to read an entire file
as with @readFile@ by reading until @forever@ or by
iterating through pages until hitting the end of
the file.

The @limit@ function can provide you with enough
fuel to read exactly a given number of lines.

On success, returns a tuple of whether the end of
the file was reached or not and the lines read in
from the file.

Note that each line will still have a newline
character at the end.

Important: because we are chunking by lines, this
function's totality depends on the assumption that
no single line in the input file is infinite.
Totality: total
removeFile : HasIOio => String -> io (EitherFileErrorUnit)
Totality: total
stderr : File
Totality: total
stdin : File
Totality: total
stdout : File
Totality: total
withFile : HasIOio => String -> Mode -> (FileError -> ioa) -> (File -> io (Eitherab)) -> io (Eitherab)
Perform a given operation on successful file open
and ensure the file is closed afterwards or perform
a different operation if the file fails to open.
Totality: total
writeFile : HasIOio => String -> String -> io (EitherFileErrorUnit)
Write a string to a file
Totality: total