Idris2Doc : System.Posix.Socket.Prim

System.Posix.Socket.Prim

(source)

Reexports

import public Data.Buffer
import public Data.Buffer.Core
import public Data.ByteString
import public Data.ByteVect
import public Data.C.Ptr
import public System.Posix.Errno
import public System.Posix.File.FileDesc
import public System.Posix.File.ReadRes
import public System.Posix.Socket.Struct
import public System.Posix.Socket.Types

Definitions

socket : (d : Domain) -> SockType -> EPrim (Socket d)
  Creates a new endpoint for communication returning a file descriptor
referring to that endpoint.

Totality: total
Visibility: export
listen : Socket d -> Bits32 -> EPrim ()
  Listen for connections on a socket.

This marks the socket as the *passive* part that will then wait
for incoming connections using calles to `accept`.

Totality: total
Visibility: export
accept : Socket d -> EPrim (Socket d)
  Accept connections on a socket.

Incoming connections are returned as new `Socket` file descriptors.

Totality: total
Visibility: export
bind_ : Socket d -> Sockaddr d -> EPrim ()
  Binds a socket to the given address. See also `bind` for a more
convenient version of this function.

Totality: total
Visibility: export
connect_ : Socket d -> Sockaddr d -> EPrim ()
  Connects a socket to the given address. See also `connect` for a more
convenient version of this function.

Totality: total
Visibility: export
recvPtr : Socket d -> (0 r : Type) -> FromPtr r => CPtr -> SockFlags -> EPrim (ReadRes r)
  Reads at most `n` bytes from a file into an allocated pointer.

Totality: total
Visibility: export
recv : Socket d -> (0 r : Type) -> FromBuf r => Bits32 -> SockFlags -> EPrim (ReadRes r)
  Reads at most `n` bytes from a file into a bytestring.

Totality: total
Visibility: export
recvFromPtr : Socket d -> (0 r : Type) -> FromPtr r => CPtr -> SockFlags -> Sockaddr d -> EPrim r
  Reads at most `n` bytes from a file into an allocated pointer.

Totality: total
Visibility: export
recvFrom : Socket d -> (0 r : Type) -> FromBuf r => Bits32 -> SockFlags -> Sockaddr d -> EPrim r
  Reads at most `n` bytes from a file into an allocated pointer.

Totality: total
Visibility: export
sendto : ToBuf r => Socket d -> r -> SockFlags -> Sockaddr d -> EPrim Bits32
  Sends the given byte string via the given socket to the peer at the
given address.

Totality: total
Visibility: export
bind : Socket d -> Addr d -> EPrim ()
  Convenience alias for `bind_`.

Totality: total
Visibility: export
connect : Socket d -> Addr d -> EPrim ()
  Convenience alias for `connect_`.

Totality: total
Visibility: export
getpeername_ : Socket d -> Sockaddr d -> EPrim ()
  Returns the address of the peer connected to a socket.
The given Sockaddr buffer will be filled with the peer address.

Totality: total
Visibility: export
getsockname_ : Socket d -> Sockaddr d -> EPrim ()
  Returns the current address to which the socket is bound.
The given Sockaddr buffer will be filled with the socket's address.

Totality: total
Visibility: export
getpeername : Socket d -> EPrim (Addr d)
  Returns the address of the peer connected to a socket.

Totality: total
Visibility: export
getsockname : Socket d -> EPrim (Addr d)
  Returns the current address to which the socket is bound.

Totality: total
Visibility: export
setNoDelay : Socket d -> Bool -> EPrim ()
  Enables or disables the Nagle algorithm.

Totality: total
Visibility: export
setReuseAddress : Socket d -> Bool -> EPrim ()
  Allows binding to an address/port before the expiry of the TIME_WAIT state.

Totality: total
Visibility: export
setLinger : Socket d -> Maybe Bits32 -> EPrim ()
  Sets the linger option for a socket.

`Nothing` disables lingering (close returns immediately).
`Just 0` enables a hard close (RST sent, data discarded).
`Just n` for n > 0 waits up to n seconds for data to be sent before closing.

Totality: total
Visibility: export