
  0 | module IO.Async.Socket
  1 | 
  2 | import public IO.Async.Posix
  3 | import public System.Posix.Socket
  4 | 
  5 | %default total
  6 | 
  7 | parameters {auto has : Has Errno es}
  8 |            {auto ep  : PollH e}
  9 | 
 10 |   ||| Creates a new endpoint for communication returning a file descriptor
 11 |   ||| referring to that endpoint.
 12 |   |||
 13 |   ||| Unlike `System.Posix.Socket`, this will open the socket in
 14 |   ||| non-blocking mode (with the `O_NONBLOCK` flag set)
 15 |   export %inline
 16 |   socketnb : (d : Domain) -> SockType -> Async e es (Socket d)
 17 |   socketnb d t = do
 18 |     sock <- socket d t
 19 |     addFlags sock O_NONBLOCK
 20 |     pure sock
 21 | 
 22 |   ||| Listens on the given socket for incoming connections without blocking.
 23 |   export
 24 |   acceptnb : Socket d -> Async e es (Socket d)
 25 |   acceptnb sock = do
 26 |     assert_total $ attempt (accept {es = [Errno]} sock) >>= \case
 27 |       Right peer    => pure peer
 28 |       Left (Here x) =>
 29 |         if x == EINPROGRESS || x == EAGAIN
 30 |            then ignore (poll sock POLLIN) >> acceptnb sock
 31 |            else throw x
 32 | 
 33 |   ||| Connects a socket to the given address.
 34 |   export
 35 |   connectnb : {d : _} -> Socket d -> Addr d -> Async e es ()
 36 |   connectnb sock addr =
 37 |     attempt (connect {es = [Errno]} sock addr) >>= \case
 38 |       Left (Here x) =>
 39 |         if x == EINPROGRESS || x == EAGAIN
 40 |            then ignore $ poll sock POLLOUT
 41 |            else throw x
 42 |       Right ()      => pure ()
 43 | 
 44 |   ||| Reads at most `n` bytes from a socket.
 45 |   export %inline
 46 |   recvnb :
 47 |        Socket d
 48 |     -> (0 r : Type)
 49 |     -> {auto frb : FromBuf r}
 50 |     -> (n : Bits32)
 51 |     -> SockFlags
 52 |     -> Async e es (ReadRes r)
 53 |   recvnb sock r n fs = do
 54 |     _ <- poll sock POLLIN
 55 |     recv sock r n fs
 56 |