System.File.ReadWrite

Reexports

Definitions

fSeekLine : HasIO io => File -> io (Either FileError ())

  Seek through the next newline.
  This is @fGetLine@ without the overhead of copying
  any characters.
  
  @ h the file handle to seek through

Visibility: export

getStringAndFree : HasIO io => File -> Ptr String -> io (Either FileError String)

  Get a garbage collected String from a Ptr String and and free the original

Totality: total
Visibility: export

fGetLine : HasIO io => File -> io (Either FileError String)

  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 : HasIO io => File -> Int -> io (Either FileError String)

  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 : HasIO io => File -> io (Either FileError Char)

  Get the next character from the given file handle.
  
  @ h the file handle to read from

Totality: total
Visibility: export

fPutStr : HasIO io => File -> String -> io (Either FileError ())

  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 : HasIO io => File -> String -> io (Either FileError ())

  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 : HasIO io => File -> io Bool

  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 : HasIO io => File -> io (Either FileError String)

  Read all the remaining contents of a file handle

Visibility: export

removeFile : HasIO io => String -> io (Either FileError ())

  Delete the file at the given name.
  
  @ fname the file to delete

Totality: total
Visibility: export

readFilePage : HasIO io => Nat -> Fuel -> String -> io (Either FileError (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.
  
  @ 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 : HasIO io => String -> io (Either FileError String)

  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 : HasIO io => String -> String -> io (Either FileError ())

  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 : HasIO io => String -> String -> io (Either FileError ())

  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