openFile : Has Errno es => EIO1 f => String -> Flags -> Mode -> f es Fd Tries to open a file with the given flags and mode.
Totality: total
Visibility: exportclose' : FileDesc a => HasIO io => a -> io () Convenience version of `close` that fails silently.
Totality: total
Visibility: exportclose : FileDesc a => a -> Has Errno es => EIO1 f => f es () Closes a file descriptor.
Totality: total
Visibility: exportreadPtr : FileDesc a => a -> Has Errno es => EIO1 f => (0 r : Type) -> FromPtr r => CPtr -> f es r Reads at most `n` bytes from a file into a pre-allocated pointer.
Totality: total
Visibility: exportreadPtrRes : FileDesc a => a -> Has Errno es => EIO1 f => (0 r : Type) -> FromPtr r => CPtr -> f es (ReadRes r) Reads at most `n` bytes from a file into a pre-allocated pointer.
Totality: total
Visibility: exportread : FileDesc a => a -> Has Errno es => EIO1 f => (0 r : Type) -> FromBuf r => Bits32 -> f es r Reads at most `n` bytes from a file into a bytestring.
Totality: total
Visibility: exportreadRaw : FileDesc a => a -> Has Errno es => EIO1 f => Buf -> f es EMBuffer Reads data from a file into a preallocated buffer
Totality: total
Visibility: exportreadres : FileDesc a => a -> Has Errno es => EIO1 f => (0 r : Type) -> FromBuf r => Bits32 -> f es (ReadRes r) Reads at most `n` bytes from a file into a bytestring.
This is a more convenient version of `read` that gives detailed
information about why a read might fail. It is especially useful
when reading from - possibly non-blocking - pipes or sockets.
Totality: total
Visibility: exportpread : FileDesc a => a -> Has Errno es => EIO1 f => (0 r : Type) -> FromBuf r => Bits32 -> OffT -> f es r Atomically reads up to `n` bytes from the given file at
the given file offset.
Notes: This will only work with seekable files but not with
arbitrary data streams such as pipes or sockets.
Also, it will not change the position of the open file description.
Totality: total
Visibility: exportwrite : FileDesc a => a -> Has Errno es => EIO1 f => ToBuf r => r -> f es Bits32 Writes up to the number of bytes in the bytestring
to the given file.
Note: This is an atomic operation if `fd` is a regular file that
was opened in "append" mode (with the `O_APPEND` flag).
Totality: total
Visibility: exportfwrite : FileDesc a => a -> Has Errno es => EIO1 f => ToBuf r => r -> f es () Iteratively writes a value to a file descriptor making sure
that the whole value is written. Use this, if a single call to
`write` might not write the complete data (for instance, when
writing to a pipe or socket).
Totality: total
Visibility: exportpwrite : FileDesc a => a -> Has Errno es => EIO1 f => ToBuf r => r -> OffT -> f es Bits32 Atomically writes up to the number of bytes in the bytestring
to the given file at the given file offset.
Notes: This will only work with seekable files but not with
arbitrary data streams such as pipes or sockets.
Also, it will not change the position of the open file description.
Totality: total
Visibility: exportlseek : FileDesc a => HasIO io => a -> OffT -> Whence -> io OffT Moves the file pointer to the given offset relative to the
`Whence` value.
Totality: total
Visibility: exportdup : FileDesc a => a -> Has Errno es => EIO1 f => f es Fd Duplicates the given open file descriptor.
The duplicate is guaranteed to be given the smallest available
file descriptor.
Totality: total
Visibility: exportdup2 : FileDesc a => a -> Has Errno es => EIO1 f => FileDesc b => b -> f es Fd Duplicates the given open file descriptor.
The new file descriptor vill have the integer value of `fd2`.
This is an atomic operation that will close `fd2` if it is still open.
Totality: total
Visibility: exportdupfd : FileDesc a => a -> Has Errno es => EIO1 f => Bits32 -> f es Fd Duplicates the given open file descriptor.
The new file descriptor vill have the integer value of `fd2`.
This is an atomic operation that will close `fd2` if it is still open.
Totality: total
Visibility: exportgetFlags : FileDesc a => a -> Has Errno es => EIO1 f => f es Flags Gets the flags set at an open file descriptor.
Totality: total
Visibility: exportsetFlags : FileDesc a => a -> Has Errno es => EIO1 f => Flags -> f es () Sets the flags of an open file descriptor.
Note: This replaces the currently set flags. See also `addFlags`.
Totality: total
Visibility: exportaddFlags : FileDesc a => a -> Has Errno es => EIO1 f => Flags -> f es () Adds the given flags to the flags set for an open
file descriptor by ORing them with the currently set flags.
Totality: total
Visibility: exportftruncate : FileDesc a => a -> Has Errno es => EIO1 f => OffT -> f es () Truncates a file to the given length.
Totality: total
Visibility: exporttruncate : Has Errno es => EIO1 f => String -> OffT -> f es () Truncates a file to the given length.
Totality: total
Visibility: exportmkstemp : Has Errno es => EIO1 f => String -> f es (Fd, String) Atomically creates and opens a temporary, unique file.
Totality: total
Visibility: exportlink : Has Errno es => EIO1 f => String -> String -> f es () Creates a (hard) link to a file.
Totality: total
Visibility: exportsymlink : Has Errno es => EIO1 f => String -> String -> f es () Creates a (hard) link to a file.
Totality: total
Visibility: exportunlink : Has Errno es => EIO1 f => String -> f es () Deletes a (hard) link to a file.
If this is the last link to the file, the file is removed.
Note: Files with open file descriptors will only be deleted after the last
open file descriptor is closed, but the file name will already
disapper from the file system before that.
Totality: total
Visibility: exportremove : Has Errno es => EIO1 f => String -> f es () Removes a file or (empty) directory calling `unlink` or `rmdir`
internally.
Totality: total
Visibility: exportrename : Has Errno es => EIO1 f => String -> String -> f es () Renames a file within a file system.
Note: This will fail if the two paths point to different file systems.
In that case, the file needs to be copied from one FS to the other.
Totality: total
Visibility: exportreadlink : Has Errno es => EIO1 f => String -> f es ByteString Returns the path of a file a symbolic link points to
This allocates a buffer of 4096 bytes for the byte array holding
the result.
Totality: total
Visibility: exportstdout : HasIO io => String -> io ()- Totality: total
Visibility: export stdoutLn : HasIO io => String -> io ()- Totality: total
Visibility: export prnt : HasIO io => Show a => a -> io ()- Totality: total
Visibility: export prntLn : HasIO io => Show a => a -> io ()- Totality: total
Visibility: export stderr : HasIO io => String -> io ()- Totality: total
Visibility: export stderrLn : HasIO io => String -> io ()- Totality: total
Visibility: export