Idris2Doc : System.File.ReadWrite

System.File.ReadWrite

Reexports

importpublic Data.Fuel
importpublic System.File.Error
importpublic System.File.Types

Definitions

fSeekLine : HasIOio=>File->io (EitherFileError ())
  Seek through the next newline.
This is @fGetLine@ without the overhead of copying
any characters.

@ h the file handle to seek through

Visibility: export
fGetLine : HasIOio=>File->io (EitherFileErrorString)
  Get the next line from the given file handle, returning the empty string if
nothing was read.

@ h the file handle to get the line from

Visibility: export
fGetChars : HasIOio=>File->Int->io (EitherFileErrorString)
  Get a number of characters from the given file handle.

@ h the file handle to read from
@ max the number of characters to read

Totality: total
Visibility: export
fGetChar : HasIOio=>File->io (EitherFileErrorChar)
  Get the next character from the given file handle.

@ h the file handle to read from

Totality: total
Visibility: export
fPutStr : HasIOio=>File->String->io (EitherFileError ())
  Write the given string to the file handle.

@ h the file handle to write to
@ str the string to write

Totality: total
Visibility: export
fPutStrLn : HasIOio=>File->String->io (EitherFileError ())
  Write the given string, followed by a newline, to the file handle.

@ fh the file handle to write to
@ str the string to write

Totality: total
Visibility: export
fEOF : HasIOio=>File->ioBool
  Check whether the end-of-file indicator for the given file handle is set.

@ h the file handle to check

Totality: total
Visibility: export
fRead : HasIOio=>File->io (EitherFileErrorString)
  Read all the remaining contents of a file handle

Visibility: export
removeFile : HasIOio=>String->io (EitherFileError ())
  Delete the file at the given name.

@ fname the file to delete

Totality: total
Visibility: export
readFilePage : HasIOio=>Nat->Fuel->String->io (EitherFileError (Bool, ListString))
  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.

@ offset the offset to start reading at
@ until the `Fuel` limiting how far we can read
@ fname the name of the file to read

Totality: total
Visibility: export
readFile : HasIOio=>String->io (EitherFileErrorString)
  Read the entire file at the given name. This function is `partial` since
there is no guarantee that the given file isn't infinite.

@ fname the name of the file to read

Visibility: export
writeFile : HasIOio=>String->String->io (EitherFileError ())
  Write the given string to the file at the specified name. Opens the file
with the `WriteTruncate` mode.
(If you have a file handle (a `File`), you may be looking for `fPutStr`.)

@ filePath the file to write to
@ contents the string to write to the file

Totality: total
Visibility: export
appendFile : HasIOio=>String->String->io (EitherFileError ())
  Append the given string to the file at the specified name. Opens the file in
with the `Append` mode.

@ filePath the file to write to
@ contents the string to write to the file

Totality: total
Visibility: export