System.Posix.File.Prim

Reexports

Definitions

allocRead : FromBuf a => Bits32 -> (Buffer -> Bits32 -> PrimIO SsizeT) -> EPrim a

  Converts a number of bytes read into a buffer to a suitable result.

Totality: total
Visibility: export

toRes : FromBuf a => Bits32 -> (Buffer -> Bits32 -> PrimIO SsizeT) -> EPrim (ReadRes a)

  Like `allocRead` but treats certain errors as valid results.

Totality: total
Visibility: export

ptrRead : FromPtr a => AnyPtr -> PrimIO SsizeT -> EPrim a

  Converts a number of bytes read into a C-ptr to a suitable result.

Totality: total
Visibility: export

ptrToRes : FromPtr a => AnyPtr -> PrimIO SsizeT -> EPrim (ReadRes a)

  Like `ptrRead` but treats certain errors as valid results.

Totality: total
Visibility: export

toFD : PrimIO CInt -> EPrim Fd

Totality: total
Visibility: export

openFile : String -> Flags -> Mode -> EPrim Fd

  Tries to open a file with the given flags and mode.

Totality: total
Visibility: export

close : FileDesc a => a -> EPrim ()

  Closes a file descriptor.

Totality: total
Visibility: export

close' : FileDesc a => a -> PrimIO ()

  Convenience version of `close` that fails silently.

Totality: total
Visibility: export

readPtr : FileDesc a => a -> (0 r : Type) -> FromPtr r => CPtr -> EPrim r

  Reads at most `n` bytes from a file into a pre-allocated pointer.

Totality: total
Visibility: export

readPtrRes : FileDesc a => a -> (0 r : Type) -> FromPtr r => CPtr -> EPrim (ReadRes r)

  Reads at most `n` bytes from a file into a pre-allocated pointer.
  
  This is similar to `readres`, but it allows us to efficiently stream
  data into a large pointer, even in case the chunks of data are much smaller.

Totality: total
Visibility: export

read : FileDesc a => a -> (0 r : Type) -> FromBuf r => Bits32 -> EPrim r

  Reads at most `n` bytes from a file into a suitable result type.

Totality: total
Visibility: export

readRaw : FileDesc a => a -> Buf -> EPrim EMBuffer

  Reads data from a file into a preallocated buffer

Totality: total
Visibility: export

readres : FileDesc a => a -> (0 r : Type) -> FromBuf r => Bits32 -> EPrim (ReadRes r)

  Reads at most `n` bytes from a file into a suitable result type.
  
  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: export

pread : FileDesc a => a -> (0 r : Type) -> FromBuf r => Bits32 -> OffT -> EPrim 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: export

write : FileDesc a => a -> ToBuf r => r -> EPrim 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: export

fwrite : FileDesc a => a -> ToBuf r => r -> EPrim ()

  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: export

pwrite : FileDesc a => a -> ToBuf r => r -> OffT -> EPrim 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: export

lseek : FileDesc a => a -> OffT -> Whence -> PrimIO OffT

  Moves the file pointer to the given offset relative to the
  `Whence` value.

Totality: total
Visibility: export

dup : FileDesc a => a -> EPrim Fd

  Duplicates the given open file descriptor.
  
  The duplicate is guaranteed to be given the smallest available
  file descriptor.

Totality: total
Visibility: export

dup2 : FileDesc a => a -> FileDesc b => b -> EPrim 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: export

dupfd : FileDesc a => a -> Bits32 -> EPrim 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: export

getFlags : FileDesc a => a -> EPrim Flags

  Gets the flags set at an open file descriptor.

Totality: total
Visibility: export

setFlags : FileDesc a => a -> Flags -> EPrim ()

  Sets the flags of an open file descriptor.
  
  Note: This replaces the currently set flags. See also `addFlags`.

Totality: total
Visibility: export

addFlags : FileDesc a => a -> Flags -> EPrim ()

  Adds the given flags to the flags set for an open
  file descriptor by ORing them with the currently set flags.

Totality: total
Visibility: export

ftruncate : FileDesc a => a -> OffT -> EPrim ()

  Truncates a file to the given length.

Totality: total
Visibility: export

truncate : String -> OffT -> EPrim ()

  Truncates a file to the given length.

Totality: total
Visibility: export

mkstemp : String -> EPrim (Fd, String)

  Atomically creates and opens a temporary, unique file.

Totality: total
Visibility: export

link : String -> String -> EPrim ()

  Creates a (hard) link to a file.

Totality: total
Visibility: export

symlink : String -> String -> EPrim ()

  Creates a (hard) link to a file.

Totality: total
Visibility: export

unlink : String -> EPrim ()

  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: export

remove : String -> EPrim ()

  Removes a file or (empty) directory calling `unlink` or `rmdir`
  internally.

Totality: total
Visibility: export

rename : String -> String -> EPrim ()

  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: export

readlink : FromBuf a => String -> EPrim a

  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: export

stdout : String -> PrimIO ()

Totality: total
Visibility: export

stdoutLn : String -> PrimIO ()

Totality: total
Visibility: export

prnt : Show a => a -> PrimIO ()

Totality: total
Visibility: export

prntLn : Show a => a -> PrimIO ()

Totality: total
Visibility: export

stderr : String -> PrimIO ()

Totality: total
Visibility: export

stderrLn : String -> PrimIO ()

Totality: total
Visibility: export