IdrisDoc: Prelude.File

# Prelude.File

writeFile : (filepath : String) -> (contents : String) -> IO (Either FileError ())

  Write a string to a file

validFile : File -> IO Bool

  Check whether a file handle is actually a null pointer

stdout : File

  Standard output

stdin : File

  Standard input

stderr : File

  Standard output

readFile : (filepath : String) -> IO (Either FileError String)

  Read the contents of a file into a string
  This checks the size of the file before beginning to read, and only
  reads that many bytes, to ensure that it remains a total function if
  the file is appended to while being read.
  Returns an error if filepath is not a normal file.

popen : String -> Mode -> IO (Either FileError File)
pclose : File -> IO ()
openFileX : (f : String) -> (m : Mode) -> IO (Either FileError File)

  Open a file using C11 extended modes.

  f

    the filename

  m

    the mode; either Read, WriteTruncate, Append, ReadWrite, ReadWriteTruncate, or ReadAppend

openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)

  Open a file

  f

    the filename

  m

    the mode; either Read, WriteTruncate, Append, ReadWrite, ReadWriteTruncate, or ReadAppend

modeStr : Mode -> String
getFileError : IO FileError
fwrite : File -> String -> IO (Either FileError ())
fread : File -> IO (Either FileError String)
fpoll : File -> IO Bool
fopen : (f : String) -> (m : String) -> IO (Either FileError File)

  Open a file

  f

    the filename

  m

    the mode as a String (`"r"`, `"w"`, or `"r+"`)

fileSize : File -> IO (Either FileError Int)

  Return the size of a File
  Returns an error if the File is not an ordinary file (e.g. a directory)
  Also note that this currently returns an Int, which may overflow if the
  file is very big

fgetc : File -> IO (Either FileError Char)
fflush : File -> IO ()
ferror : File -> IO Bool
feof : File -> IO Bool

  Check if a file handle has reached the end

fPutStrLn : File -> String -> IO (Either FileError ())
fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())

  Write a line to a file

  h

    a file handle which must be open for writing

  str

    the line to write to the file

fGetLine : (h : File) -> IO (Either FileError String)

  Read a line from a file

  h

    a file handle which must be open for reading

fEOF : File -> IO Bool

  Check if a file handle has reached the end

closeFile : File -> IO ()
Write : Mode
data Mode : Type

  Modes for opening files

  Read : Mode
  WriteTruncate : Mode
  Append : Mode
  ReadWrite : Mode
  ReadWriteTruncate : Mode
  ReadAppend : Mode
data FileError : Type

  An error from a file operation

  GenericFileError : Int -> FileError
  FileReadError : FileError
  FileWriteError : FileError
  FileNotFound : FileError
  PermissionDenied : FileError
data File : Type

  A file handle

  FHandle : (p : Ptr) -> File