System.Linux.File

Definitions

interface FileDesc : Type -> Type

Parameters: a
Methods:

fileDesc : a -> Bits32

Implementations:

FileDesc EventFD

FileDesc Bits32

FileDesc StdFile

fileDesc : FileDesc a => a -> Bits32

Totality: total
Visibility: public export

data ReadRes : Type

  Result of reading from a file descriptor

Totality: total
Visibility: public export
Constructors:

EOF : ReadRes

  End of file has been reached

Again : ReadRes

  This occurs when reading from a file descriptor in non-blocking mode
  and there is currently no data ready.

Bytes : (n : Nat) -> IBuffer n -> ReadRes

  The given numbers have been read into an immutable buffer

Err : EpollErr -> ReadRes

  An error occured

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

  Close a file descriptor.

Totality: total
Visibility: export

read : FileDesc a => a -> Buffer -> Nat -> Nat -> PrimIO (Either EpollErr Nat)

  Low-level reading of at most `max` bytes from a file into a buffer
  starting at buffer offset `offset`.
  
  See `readBytes` for a higher-level function that allocates a new buffer and
  correctly interprets the result.

Totality: total
Visibility: export

write : FileDesc a => a -> Buffer -> Nat -> Nat -> PrimIO (Either EpollErr Nat)

Totality: total
Visibility: export

readBytes : FileDesc a => a -> Nat -> PrimIO ReadRes

  A higher-level alternative to `read`: It allocates a new buffer of the
  given size and returns it wrapped in a `ReadRes`.
  
  Use `read` if you want to avoid allocating a new buffer for every
  data package.

Totality: total
Visibility: export

setNonBlocking : FileDesc a => a -> PrimIO ()

  Changes a file descriptor's mode to `O_NONBLOCK`.
  
  This will not block when trying to read from a stream such as a pipe, socket, or
  stdin. Instead, `readBytes` will return `Again` in case no data is currently
  available. Use this in combination with `EPOLLET` to keep reading from a data
  source until it is temporarily exhausted.

Totality: total
Visibility: export

data StdFile : Type

Totality: total
Visibility: public export
Constructors:

StdIn : StdFile

StdOut : StdFile

StdErr : StdFile

Hints:

Eq StdFile

FileDesc StdFile

Finite StdFile

Ord StdFile

Show StdFile