
   0 | module System.Posix.Socket
   1 | 
   2 | import System.Posix.Socket.Prim as P
   3 | 
   4 | import public System.Posix.Socket.Struct
   5 | import public System.Posix.Socket.Types
   6 | import public System.Posix.File.ReadRes
   7 | 
   8 | parameters {auto has : Has Errno es}
   9 |            {auto eio : EIO1 f}
  10 | 
  11 |   ||| Creates a new endpoint for communication returning a file descriptor
  12 |   ||| referring to that endpoint.
  13 |   export %inline
  14 |   socket : (d : Domain) -> SockType -> f es (Socket d)
  15 |   socket d t = elift1 $ P.socket d t
  16 | 
  17 |   ||| Listen for connections on a socket.
  18 |   |||
  19 |   ||| This marks the socket as the *passive* part that will then wait
  20 |   ||| for incoming connections using calles to `accept`.
  21 |   export %inline
  22 |   listen : Socket d -> (backlog : Bits32) -> f es ()
  23 |   listen s b = elift1 $ P.listen s b
  24 | 
  25 |   ||| Accept connections on a socket.
  26 |   |||
  27 |   ||| Incoming connections are returned as new `Socket` file descriptors.
  28 |   export %inline
  29 |   accept : Socket d -> f es (Socket d)
  30 |   accept s = elift1 $ P.accept s
  31 | 
  32 |   ||| Binds a socket to the given address.
  33 |   export %inline
  34 |   bind_ : {d : _} -> Socket d -> Sockaddr d -> f es ()
  35 |   bind_ s a = elift1 $ P.bind_ s a
  36 | 
  37 |   ||| Connects a socket to the given address.
  38 |   export %inline
  39 |   connect_ : {d : _} -> Socket d -> Sockaddr d -> f es ()
  40 |   connect_ s a = elift1 $ P.connect_ s a
  41 | 
  42 |   ||| Convenience alias for `bind_`.
  43 |   export
  44 |   bind : {d : _} -> Socket d -> Addr d -> f es ()
  45 |   bind s a = elift1 $ P.bind s a
  46 | 
  47 |   ||| Convenience alias for `connect_`.
  48 |   export
  49 |   connect : {d : _} -> Socket d -> Addr d -> f es ()
  50 |   connect s a = elift1 $ P.connect s a
  51 | 
  52 |   ||| Reads at most `n` bytes from a file into an allocated pointer.
  53 |   export %inline
  54 |   recvPtr :
  55 |        Socket d
  56 |     -> (0 r : Type)
  57 |     -> {auto frp : FromPtr r}
  58 |     -> CPtr
  59 |     -> SockFlags
  60 |     -> f es (ReadRes r)
  61 |   recvPtr s r cp fs = elift1 $ P.recvPtr s r cp fs
  62 | 
  63 |   ||| Reads at most `n` bytes from a file into an allocated pointer.
  64 |   export %inline
  65 |   recvFromPtr :
  66 |       {d : _}
  67 |     -> Socket d
  68 |     -> (0 r : Type)
  69 |     -> {auto frp : FromPtr r}
  70 |     -> CPtr
  71 |     -> SockFlags
  72 |     -> Sockaddr d
  73 |     -> f es r
  74 |   recvFromPtr s r cp sf a = elift1 $ P.recvFromPtr s r cp sf a
  75 | 
  76 |   ||| Reads at most `n` bytes from a file into a bytestring.
  77 |   export %inline
  78 |   recv :
  79 |        Socket d
  80 |     -> (0 r : Type)
  81 |     -> {auto frb : FromBuf r}
  82 |     -> (n : Bits32)
  83 |     -> SockFlags
  84 |     -> f es (ReadRes r)
  85 |   recv s r n fs = elift1 $ P.recv s r n fs
  86 | 
  87 |   ||| Reads at most `n` bytes from a socket into a bytestring
  88 |   export %inline
  89 |   recvFrom :
  90 |       {d : _}
  91 |     -> Socket d
  92 |     -> (0 r : Type)
  93 |     -> {auto frb : FromBuf r}
  94 |     -> (n : Bits32)
  95 |     -> SockFlags
  96 |     -> Sockaddr d
  97 |     -> f es r
  98 |   recvFrom s r n sf a = elift1 $ P.recvFrom s r n sf a
  99 | 
 100 |   export
 101 |   sendto :
 102 |        {d : _}
 103 |     -> {auto tob : ToBuf r}
 104 |     -> Socket d
 105 |     -> r
 106 |     -> SockFlags
 107 |     -> Sockaddr d
 108 |     -> f es Bits32
 109 |   sendto s r f a = elift1 $ P.sendto s r f a
 110 | 
 111 |   ||| Returns the address of the peer connected to a socket.
 112 |   ||| The given Sockaddr buffer will be filled with the peer address.
 113 |   export %inline
 114 |   getpeername_ : {d : _} -> Socket d -> Sockaddr d -> f es ()
 115 |   getpeername_ s a = elift1 $ P.getpeername_ s a
 116 | 
 117 |   ||| Returns the current address to which the socket is bound.
 118 |   ||| The given Sockaddr buffer will be filled with the socket's address.
 119 |   export %inline
 120 |   getsockname_ : {d : _} -> Socket d -> Sockaddr d -> f es ()
 121 |   getsockname_ s a = elift1 $ P.getsockname_ s a
 122 | 
 123 |   ||| Returns the address of the peer connected to a socket.
 124 |   export %inline
 125 |   getpeername : {d : _} -> Socket d -> f es (Addr d)
 126 |   getpeername s = elift1 $ P.getpeername s
 127 | 
 128 |   export %inline
 129 |   getsockname : {d : _} -> Socket d -> f es (Addr d)
 130 |   getsockname s = elift1 $ P.getsockname s
 131 | 
 132 |   ||| Enables or disables the Nagle algorithm.
 133 |   export %inline
 134 |   setNoDelay : Socket d -> Bool -> f es ()
 135 |   setNoDelay s b = elift1 $ P.setNoDelay s b
 136 | 
 137 |   ||| Allows binding to an address/port before the expiry of the TIME_WAIT state.
 138 |   export %inline
 139 |   setReuseAddress : Socket d -> Bool -> f es ()
 140 |   setReuseAddress s b = elift1 $ P.setReuseAddress s b
 141 | 
 142 |   ||| Sets the linger option for a socket.
 143 |   |||
 144 |   ||| `Nothing` disables lingering (close returns immediately).
 145 |   ||| `Just 0` enables a hard close (RST sent, data discarded).
 146 |   ||| `Just n` for n > 0 waits up to n seconds for data to be sent before closing.
 147 |   export %inline
 148 |   setLinger : Socket d -> Maybe Bits32 -> f es ()
 149 |   setLinger s t = elift1 $ P.setLinger s t
 150 |