@@ -1,6 +1,7 @@
1−||| Time to do this properly.
21||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
3−||| (C) SimonJF, MIT Licensed, 2014
2+|||
3+||| Original (C) SimonJF, MIT Licensed, 2014
4+||| Modified (C) The Idris Community, 2015, 2016
45module Network.Socket
56
67%include C "idris_net.h"
@@ -8,119 +9,155 @@ module Network.Socket
89%include C "sys/socket.h"
910%include C "netdb.h"
1011
12+-- ------------------------------------------------------------ [ Type Aliases ]
13+
1114public export
1215ByteLength : Type
1316ByteLength = Int
1417
18+public export
19+ResultCode : Type
20+ResultCode = Int
21+
22+||| Protocol Number.
23+|||
24+||| Generally good enough to just set it to 0.
25+public export
26+ProtocolNumber : Type
27+ProtocolNumber = Int
28+
29+||| SocketError: Error thrown by a socket operation
30+public export
31+SocketError : Type
32+SocketError = Int
33+
34+||| SocketDescriptor: Native C Socket Descriptor
35+public export
36+SocketDescriptor : Type
37+SocketDescriptor = Int
38+
39+public export
40+Port : Type
41+Port = Int
42+
43+-- --------------------------------------------------------------- [ Constants ]
44+
45+||| Backlog used within listen() call -- number of incoming calls
46+public export
47+BACKLOG : Int
48+BACKLOG = 20
49+
50+-- FIXME: This *must* be pulled in from C
51+public export
52+EAGAIN : Int
53+EAGAIN = 11
54+
55+-- -------------------------------------------------------------- [ Interfaces ]
56+
1557export
1658interface ToCode a where
1759 toCode : a -> Int
1860
61+-- --------------------------------------------------------- [ Socket Families ]
62+
1963||| Socket Families
2064|||
2165||| The ones that people might actually use. We're not going to need US
2266||| Government proprietary ones.
2367public export
24−data SocketFamily =
68+data SocketFamily : Type where
2569 ||| Unspecified
26− AF_UNSPEC |
70+ AF_UNSPEC : SocketFamily
71+
2772 ||| IP / UDP etc. IPv4
28− AF_INET |
73+ AF_INET : SocketFamily
74+
2975 ||| IP / UDP etc. IPv6
30− AF_INET6
76+ AF_INET6 : SocketFamily
3177
3278export
33−implementation Show SocketFamily where
79+Show SocketFamily where
3480 show AF_UNSPEC = "AF_UNSPEC"
3581 show AF_INET = "AF_INET"
3682 show AF_INET6 = "AF_INET6"
3783
3884export
39−implementation ToCode SocketFamily where
85+ToCode SocketFamily where
4086 toCode AF_UNSPEC = 0
4187 toCode AF_INET = 2
4288 toCode AF_INET6 = 10
4389
4490getSocketFamily : Int -> Maybe SocketFamily
45−getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
91+getSocketFamily i =
92+ Prelude.List.lookup i [ (0, AF_UNSPEC)
93+ , (2, AF_INET)
94+ , (10, AF_INET6)
95+ ]
4696
97+-- ------------------------------------------------------------ [ Socket Types ]
4798||| Socket Types.
4899public export
49−data SocketType =
100+data SocketType : Type where
50101 ||| Not a socket, used in certain operations
51− NotASocket |
102+ NotASocket : SocketType
103+
52104 ||| TCP
53− Stream |
105+ Stream : SocketType
106+
54107 ||| UDP
55− Datagram |
108+ Datagram : SocketType
109+
56110 ||| Raw sockets
57− RawSocket
111+ RawSocket : SocketType
58112
59113export
60−implementation Show SocketType where
114+Show SocketType where
61115 show NotASocket = "Not a socket"
62116 show Stream = "Stream"
63117 show Datagram = "Datagram"
64118 show RawSocket = "Raw"
65119
66120export
67−implementation ToCode SocketType where
121+ToCode SocketType where
68122 toCode NotASocket = 0
69123 toCode Stream = 1
70124 toCode Datagram = 2
71125 toCode RawSocket = 3
72126
127+-- ---------------------------------------------------------------- [ Pointers ]
128+
73129data RecvStructPtr = RSPtr Ptr
74130data RecvfromStructPtr = RFPtr Ptr
75131
76132export
77133data BufPtr = BPtr Ptr
134+
78135export
79136data SockaddrPtr = SAPtr Ptr
80137
81−||| Protocol Number.
82−|||
83−||| Generally good enough to just set it to 0.
84−public export
85−ProtocolNumber : Type
86−ProtocolNumber = Int
138+-- --------------------------------------------------------------- [ Addresses ]
87139
88−||| SocketError: Error thrown by a socket operation
140+||| Network Addresses
89141public export
90−SocketError : Type
91−SocketError = Int
142+data SocketAddress : Type where
143+ IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
92144
93−||| SocketDescriptor: Native C Socket Descriptor
94−public export
95−SocketDescriptor : Type
96−SocketDescriptor = Int
145+ ||| Not implemented (yet)
146+ IPv6Addr : SocketAddress
97147
98−public export
99−data SocketAddress = IPv4Addr Int Int Int Int
100− | IPv6Addr -- Not implemented (yet)
101− | Hostname String
102− | InvalidAddress -- Used when there's a parse error
148+ Hostname : String -> SocketAddress
149+
150+ ||| Used when there's a parse error
151+ InvalidAddress : SocketAddress
103152
104153export
105−implementation Show SocketAddress where
154+Show SocketAddress where
106155 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
107− show IPv6Addr = "NOT IMPLEMENTED YET"
108− show (Hostname host) = host
109− show InvalidAddress = "Invalid"
156+ show IPv6Addr = "NOT IMPLEMENTED YET"
157+ show (Hostname host) = host
158+ show InvalidAddress = "Invalid"
110159
111−public export
112−Port : Type
113−Port = Int
114−
115−||| Backlog used within listen() call -- number of incoming calls
116−public export
117−BACKLOG : Int
118−BACKLOG = 20
119−
120−-- FIXME: This *must* be pulled in from C
121−public export
122−EAGAIN : Int
123−EAGAIN = 11
160+-- --------------------------------------------------------- [ UDP Information ]
124161
125162-- TODO: Expand to non-string payloads
126163export
@@ -128,8 +165,8 @@ record UDPRecvData where
128165 constructor MkUDPRecvData
129166 remote_addr : SocketAddress
130167 remote_port : Port
131− recv_data : String
132− data_len : Int
168+ recv_data : String
169+ data_len : Int
133170
134171export
135172record UDPAddrInfo where
@@ -137,6 +174,8 @@ record UDPAddrInfo where
137174 remote_addr : SocketAddress
138175 remote_port : Port
139176
177+-- ---------------------------------------------------------- [ Socket Utilies ]
178+
140179||| Frees a given pointer
141180export
142181sock_free : BufPtr -> IO ()
@@ -153,25 +192,34 @@ export
153192sock_alloc : ByteLength -> IO BufPtr
154193sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
155194
195+-- ----------------------------------------------------------------- [ Sockets ]
156196||| The metadata about a socket
157197export
158198record Socket where
159199 constructor MkSocket
160− descriptor : SocketDescriptor
161− family : SocketFamily
162− socketType : SocketType
200+ descriptor : SocketDescriptor
201+ family : SocketFamily
202+ socketType : SocketType
163203 protocolNumber : ProtocolNumber
164204
205+
206+-- ----------------------------------------------------- [ Network Socket API. ]
207+
165208||| Creates a UNIX socket with the given family, socket type and protocol
166209||| number. Returns either a socket or an error.
167210export
168−socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
211+socket : (fam : SocketFamily)
212+ -> (ty : SocketType)
213+ -> (pnum : ProtocolNumber)
214+ -> IO (Either SocketError Socket)
169215socket sf st pn = do
170− socket_res <- foreign FFI_C "socket" (Int -> Int -> Int -> IO Int) (toCode sf) (toCode st) pn
171− if socket_res == -1 then -- error
172− map Left getErrno
173− else
174− return $ Right (MkSocket socket_res sf st pn)
216+ socket_res <- foreign FFI_C "socket"
217+ (Int -> Int -> Int -> IO Int)
218+ (toCode sf) (toCode st) pn
219+
220+ if socket_res == -1
221+ then map Left getErrno
222+ else return $ Right (MkSocket socket_res sf st pn)
175223
176224||| Close a socket
177225export
@@ -186,199 +234,378 @@ saString Nothing = ""
186234||| Binds a socket to the given socket address and port.
187235||| Returns 0 on success, an error code otherwise.
188236export
189−bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
237+bind : (sock : Socket)
238+ -> (addr : Maybe SocketAddress)
239+ -> (port : Port)
240+ -> IO Int
190241bind sock addr port = do
191242 bind_res <- foreign FFI_C "idrnet_bind"
192243 (Int -> Int -> Int -> String -> Int -> IO Int)
193244 (descriptor sock) (toCode $ family sock)
194245 (toCode $ socketType sock) (saString addr) port
195− if bind_res == (-1) then -- error
196− getErrno
197− else return 0 -- Success
246+ if bind_res == (-1)
247+ then getErrno
248+ else return 0
198249
199250||| Connects to a given address and port.
200251||| Returns 0 on success, and an error number on error.
201252export
202−connect : Socket -> SocketAddress -> Port -> IO Int
253+connect : (sock : Socket)
254+ -> (addr : SocketAddress)
255+ -> (port : Port)
256+ -> IO ResultCode
203257connect sock addr port = do
204258 conn_res <- foreign FFI_C "idrnet_connect"
205259 (Int -> Int -> Int -> String -> Int -> IO Int)
206260 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port
207− if conn_res == (-1) then
208− getErrno
209− else return 0
261+
262+ if conn_res == (-1)
263+ then getErrno
264+ else return 0
210265
211266||| Listens on a bound socket.
267+|||
268+||| @sock The socket to listen on.
212269export
213−listen : Socket -> IO Int
270+listen : (sock : Socket) -> IO Int
214271listen sock = do
215272 listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)
216273 (descriptor sock) BACKLOG
217− if listen_res == (-1) then
218− getErrno
219− else return 0
274+ if listen_res == (-1)
275+ then getErrno
276+ else return 0
220277
221278||| Parses a textual representation of an IPv4 address into a SocketAddress
222279parseIPv4 : String -> SocketAddress
223−parseIPv4 str = case splitted of
224− (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
225− _ => InvalidAddress
226− where toInt' : String -> Integer
227− toInt' = cast
228− toInt : String -> Int
229− toInt s = fromInteger $ toInt' s
230− splitted : List Int
231− splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
280+parseIPv4 str =
281+ case splitted of
282+ (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
283+ otherwise => InvalidAddress
284+ where
285+ toInt' : String -> Integer
286+ toInt' = cast
287+
288+ toInt : String -> Int
289+ toInt s = fromInteger $ toInt' s
290+
291+ splitted : List Int
292+ splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
232293
233294||| Retrieves a socket address from a sockaddr pointer
234295getSockAddr : SockaddrPtr -> IO SocketAddress
235296getSockAddr (SAPtr ptr) = do
236− addr_family_int <- foreign FFI_C "idrnet_sockaddr_family" (Ptr -> IO Int) ptr
237− -- putStrLn $ "Addr family int: " ++ (show addr_family_int)
297+ addr_family_int <- foreign FFI_C "idrnet_sockaddr_family"
298+ (Ptr -> IO Int)
299+ ptr
300+
238301 -- ASSUMPTION: Foreign call returns a valid int
239302 assert_total (case getSocketFamily addr_family_int of
240303 Just AF_INET => do
241− ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4" (Ptr -> IO String) ptr
304+ ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4"
305+ (Ptr -> IO String)
306+ ptr
307+
242308 return $ parseIPv4 ipv4_addr
243309 Just AF_INET6 => return IPv6Addr
244310 Just AF_UNSPEC => return InvalidAddress)
245311
312+||| Accept a connection on the provided socket.
313+|||
314+||| Returns on failure a `SocketError`
315+||| Returns on success a pairing of:
316+||| + `Socket` :: The socket representing the connection.
317+||| + `SocketAddress` :: The
318+|||
319+||| @sock The socket used to establish connection.
246320export
247−accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
321+accept : (sock : Socket)
322+ -> IO (Either SocketError (Socket, SocketAddress))
248323accept sock = do
324+
249325 -- We need a pointer to a sockaddr structure. This is then passed into
250326 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
251− sockaddr_ptr <- foreign FFI_C "idrnet_create_sockaddr" (IO Ptr)
252− accept_res <- foreign FFI_C "idrnet_accept" (Int -> Ptr -> IO Int) (descriptor sock) sockaddr_ptr
253− if accept_res == (-1) then
254− map Left getErrno
255− else do
256− let (MkSocket _ fam ty p_num) = sock
257− sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
258− sockaddr_free (SAPtr sockaddr_ptr)
259− return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
260327
328+ sockaddr_ptr <- foreign FFI_C "idrnet_create_sockaddr"
329+ (IO Ptr)
330+
331+ accept_res <- foreign FFI_C "idrnet_accept"
332+ (Int -> Ptr -> IO Int)
333+ (descriptor sock) sockaddr_ptr
334+ if accept_res == (-1)
335+ then map Left getErrno
336+ else do
337+ let (MkSocket _ fam ty p_num) = sock
338+ sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
339+ sockaddr_free (SAPtr sockaddr_ptr)
340+ return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
341+
342+||| Send data on the specified socket.
343+|||
344+||| Returns on failure a `SocketError`.
345+||| Returns on success the `ResultCode`.
346+|||
347+||| @sock The socket on which to send the message.
348+||| @msg The data to send.
261349export
262−send : Socket -> String -> IO (Either SocketError ByteLength)
350+send : (sock : Socket)
351+ -> (msg : String)
352+ -> IO (Either SocketError ResultCode)
263353send sock dat = do
264− send_res <- foreign FFI_C "idrnet_send" (Int -> String -> IO Int) (descriptor sock) dat
265− if send_res == (-1) then
266− map Left getErrno
267− else
268− return $ Right send_res
354+ send_res <- foreign FFI_C "idrnet_send"
355+ (Int -> String -> IO Int)
356+ (descriptor sock) dat
357+
358+ if send_res == (-1)
359+ then map Left getErrno
360+ else return $ Right send_res
269361
270362freeRecvStruct : RecvStructPtr -> IO ()
271−freeRecvStruct (RSPtr p) = foreign FFI_C "idrnet_free_recv_struct" (Ptr -> IO ()) p
363+freeRecvStruct (RSPtr p) =
364+ foreign FFI_C "idrnet_free_recv_struct"
365+ (Ptr -> IO ())
366+ p
272367
368+||| Utility to extract data.
273369freeRecvfromStruct : RecvfromStructPtr -> IO ()
274−freeRecvfromStruct (RFPtr p) = foreign FFI_C "idrnet_free_recvfrom_struct" (Ptr -> IO ()) p
370+freeRecvfromStruct (RFPtr p) =
371+ foreign FFI_C "idrnet_free_recvfrom_struct"
372+ (Ptr -> IO ())
373+ p
275374
375+
376+||| Receive data on the specified socket.
377+|||
378+||| Returns on failure a `SocketError`
379+||| Returns on success a pairing of:
380+||| + `String` :: The payload.
381+||| + `ResultCode` :: The result of the underlying function.
382+|||
383+||| @sock The socket on which to receive the message.
384+||| @len How much of the data to send.
276385export
277−recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
386+recv : (sock : Socket)
387+ -> (len : ByteLength)
388+ -> IO (Either SocketError (String, ResultCode))
278389recv sock len = do
279390 -- Firstly make the request, get some kind of recv structure which
280391 -- contains the result of the recv and possibly the retrieved payload
281− recv_struct_ptr <- foreign FFI_C "idrnet_recv" (Int -> Int -> IO Ptr) (descriptor sock) len
282− recv_res <- foreign FFI_C "idrnet_get_recv_res" (Ptr -> IO Int) recv_struct_ptr
283− if recv_res == (-1) then do
284− errno <- getErrno
285− freeRecvStruct (RSPtr recv_struct_ptr)
286− return $ Left errno
287− else
288− if recv_res == 0 then do
289− freeRecvStruct (RSPtr recv_struct_ptr)
290− return $ Left 0
291− else do
292− payload <- foreign FFI_C "idrnet_get_recv_payload" (Ptr -> IO String) recv_struct_ptr
293− freeRecvStruct (RSPtr recv_struct_ptr)
294− return $ Right (payload, recv_res)
392+ recv_struct_ptr <- foreign FFI_C "idrnet_recv"
393+ (Int -> Int -> IO Ptr)
394+ (descriptor sock) len
395+ recv_res <- foreign FFI_C "idrnet_get_recv_res"
396+ (Ptr -> IO Int)
397+ recv_struct_ptr
398+
399+ if recv_res == (-1)
400+ then do
401+ errno <- getErrno
402+ freeRecvStruct (RSPtr recv_struct_ptr)
403+ return $ Left errno
404+ else
405+ if recv_res == 0
406+ then do
407+ freeRecvStruct (RSPtr recv_struct_ptr)
408+ return $ Left 0
409+ else do
410+ payload <- foreign FFI_C "idrnet_get_recv_payload"
411+ (Ptr -> IO String)
412+ recv_struct_ptr
413+ freeRecvStruct (RSPtr recv_struct_ptr)
414+ return $ Right (payload, recv_res)
295415
296416||| Sends the data in a given memory location
297−sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
417+|||
418+||| Returns on failure a `SocketError`
419+||| Returns on success the `ResultCode`
420+|||
421+||| @sock The socket on which to send the message.
422+||| @ptr The location containing the data to send.
423+||| @len How much of the data to send.
424+sendBuf : (sock : Socket)
425+ -> (ptr : BufPtr)
426+ -> (len : ByteLength)
427+ -> IO (Either SocketError ResultCode)
298428sendBuf sock (BPtr ptr) len = do
299− send_res <- foreign FFI_C "idrnet_send_buf" (Int -> Ptr -> Int -> IO Int) (descriptor sock) ptr len
300− if send_res == (-1) then
301− map Left getErrno
302− else
303− return $ Right send_res
429+ send_res <- foreign FFI_C "idrnet_send_buf"
430+ (Int -> Ptr -> Int -> IO Int)
431+ (descriptor sock) ptr len
304432
305−recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
433+ if send_res == (-1)
434+ then map Left getErrno
435+ else return $ Right send_res
436+
437+||| Receive data from a given memory location.
438+|||
439+||| Returns on failure a `SocketError`
440+||| Returns on success the `ResultCode`
441+|||
442+||| @sock The socket on which to receive the message.
443+||| @ptr The location containing the data to receive.
444+||| @len How much of the data to receive.
445+recvBuf : (sock : Socket)
446+ -> (ptr : BufPtr)
447+ -> (len : ByteLength)
448+ -> IO (Either SocketError ResultCode)
306449recvBuf sock (BPtr ptr) len = do
307− recv_res <- foreign FFI_C "idrnet_recv_buf" (Int -> Ptr -> Int -> IO Int) (descriptor sock) ptr len
308− if (recv_res == (-1)) then
309− map Left getErrno
310− else
311− return $ Right recv_res
450+ recv_res <- foreign FFI_C "idrnet_recv_buf"
451+ (Int -> Ptr -> Int -> IO Int)
452+ (descriptor sock) ptr len
453+
454+ if (recv_res == (-1))
455+ then map Left getErrno
456+ else return $ Right recv_res
312457
458+||| Send a message.
459+|||
460+||| Returns on failure a `SocketError`
461+||| Returns on success the `ResultCode`
462+|||
463+||| @sock The socket on which to send the message.
464+||| @addr Address of the recipient.
465+||| @port The port on which to send the message.
466+||| @msg The message to send.
313467export
314−sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)
468+sendTo : (sock : Socket)
469+ -> (addr : SocketAddress)
470+ -> (port : Port)
471+ -> (msg : String)
472+ -> IO (Either SocketError ByteLength)
315473sendTo sock addr p dat = do
316474 sendto_res <- foreign FFI_C "idrnet_sendto"
317475 (Int -> String -> String -> Int -> Int -> IO Int)
318476 (descriptor sock) dat (show addr) p (toCode $ family sock)
319− if sendto_res == (-1) then
320− map Left getErrno
321− else
322− return $ Right sendto_res
323477
324−sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
478+ if sendto_res == (-1)
479+ then map Left getErrno
480+ else return $ Right sendto_res
481+
482+||| Send a message stored in some buffer.
483+|||
484+||| Returns on failure a `SocketError`
485+||| Returns on success the `ResultCode`
486+|||
487+||| @sock The socket on which to send the message.
488+||| @addr Address of the recipient.
489+||| @port The port on which to send the message.
490+||| @ptr A Pointer to the buffer containing the message.
491+||| @len The size of the message.
492+sendToBuf : (sock : Socket)
493+ -> (addr : SocketAddress)
494+ -> (port : Port)
495+ -> (ptr : BufPtr)
496+ -> (len : ByteLength)
497+ -> IO (Either SocketError ResultCode)
325498sendToBuf sock addr p (BPtr dat) len = do
326499 sendto_res <- foreign FFI_C "idrnet_sendto_buf"
327500 (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)
328501 (descriptor sock) dat len (show addr) p (toCode $ family sock)
329− if sendto_res == (-1) then
330− map Left getErrno
331− else
332− return $ Right sendto_res
333502
503+ if sendto_res == (-1)
504+ then map Left getErrno
505+ else return $ Right sendto_res
506+
507+||| Utility function to get the payload of the sent message as a `String`.
334508foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
335−foreignGetRecvfromPayload (RFPtr p)
336− = foreign FFI_C "idrnet_get_recvfrom_payload" (Ptr -> IO String) p
509+foreignGetRecvfromPayload (RFPtr p) =
510+ foreign FFI_C "idrnet_get_recvfrom_payload"
511+ (Ptr -> IO String)
512+ p
337513
514+||| Utility function to return senders socket address.
338515foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
339516foreignGetRecvfromAddr (RFPtr p) = do
340− sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p
517+ sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr"
518+ (Ptr -> IO Ptr)
519+ p
341520 getSockAddr sockaddr_ptr
342521
522+||| Utility function to return sender's IPV4 port.
343523foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
344524foreignGetRecvfromPort (RFPtr p) = do
345− sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p
346− port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" (Ptr -> IO Int) sockaddr_ptr
525+ sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr"
526+ (Ptr -> IO Ptr)
527+ p
528+ port <- foreign FFI_C "idrnet_sockaddr_ipv4_port"
529+ (Ptr -> IO Int)
530+ sockaddr_ptr
347531 return port
348532
533+
534+||| Receive a message.
535+|||
536+||| Returns on failure a `SocketError`.
537+||| Returns on success a triple of
538+||| + `UDPAddrInfo` :: The address of the sender.
539+||| + `String` :: The payload.
540+||| + `Int` :: Result value from underlying function.
541+|||
542+||| @sock The channel on which to receive.
543+||| @len Size of the expected message.
544+|||
349545export
350−recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))
546+recvFrom : (sock : Socket)
547+ -> (len : ByteLength)
548+ -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))
351549recvFrom sock bl = do
352− recv_ptr <- foreign FFI_C "idrnet_recvfrom" (Int -> Int -> IO Ptr)
550+ recv_ptr <- foreign FFI_C "idrnet_recvfrom"
551+ (Int -> Int -> IO Ptr)
353552 (descriptor sock) bl
553+
354554 let recv_ptr' = RFPtr recv_ptr
355− if !(nullPtr recv_ptr) then
356− map Left getErrno
357− else do
358− result <- foreign FFI_C "idrnet_get_recvfrom_res" (Ptr -> IO Int) recv_ptr
359− if result == -1 then do
360− freeRecvfromStruct recv_ptr'
361− map Left getErrno
362− else do
363− payload <- foreignGetRecvfromPayload recv_ptr'
364− port <- foreignGetRecvfromPort recv_ptr'
365− addr <- foreignGetRecvfromAddr recv_ptr'
366− freeRecvfromStruct recv_ptr'
367− return $ Right (MkUDPAddrInfo addr port, payload, result)
368555
369−recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))
556+ if !(nullPtr recv_ptr)
557+ then map Left getErrno
558+ else do
559+ result <- foreign FFI_C "idrnet_get_recvfrom_res"
560+ (Ptr -> IO Int)
561+ recv_ptr
562+ if result == -1
563+ then do
564+ freeRecvfromStruct recv_ptr'
565+ map Left getErrno
566+ else do
567+ payload <- foreignGetRecvfromPayload recv_ptr'
568+ port <- foreignGetRecvfromPort recv_ptr'
569+ addr <- foreignGetRecvfromAddr recv_ptr'
570+ freeRecvfromStruct recv_ptr'
571+ return $ Right (MkUDPAddrInfo addr port, payload, result)
572+
573+||| Receive a message placed on a 'known' buffer.
574+|||
575+||| Returns on failure a `SocketError`.
576+||| Returns on success a pair of
577+||| + `UDPAddrInfo` :: The address of the sender.
578+||| + `Int` :: Result value from underlying function.
579+|||
580+||| @sock The channel on which to receive.
581+||| @ptr Pointer to the buffer to place the message.
582+||| @len Size of the expected message.
583+|||
584+recvFromBuf : (sock : Socket)
585+ -> (ptr : BufPtr)
586+ -> (len : ByteLength)
587+ -> IO (Either SocketError (UDPAddrInfo, ResultCode))
370588recvFromBuf sock (BPtr ptr) bl = do
371− recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf" (Int -> Ptr -> Int -> IO Ptr) (descriptor sock) ptr bl
589+ recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf"
590+ (Int -> Ptr -> Int -> IO Ptr)
591+ (descriptor sock) ptr bl
592+
372593 let recv_ptr' = RFPtr recv_ptr
373− if !(nullPtr recv_ptr) then
374− map Left getErrno
375− else do
376− result <- foreign FFI_C "idrnet_get_recvfrom_res" (Ptr -> IO Int) recv_ptr
377− if result == -1 then do
378− freeRecvfromStruct recv_ptr'
379− map Left getErrno
594+
595+ if !(nullPtr recv_ptr)
596+ then map Left getErrno
380597 else do
381− port <- foreignGetRecvfromPort recv_ptr'
382− addr <- foreignGetRecvfromAddr recv_ptr'
383− freeRecvfromStruct recv_ptr'
384− return $ Right (MkUDPAddrInfo addr port, result + 1)
598+ result <- foreign FFI_C "idrnet_get_recvfrom_res"
599+ (Ptr -> IO Int)
600+ recv_ptr
601+ if result == -1
602+ then do
603+ freeRecvfromStruct recv_ptr'
604+ map Left getErrno
605+ else do
606+ port <- foreignGetRecvfromPort recv_ptr'
607+ addr <- foreignGetRecvfromAddr recv_ptr'
608+ freeRecvfromStruct recv_ptr'
609+ return $ Right (MkUDPAddrInfo addr port, result + 1)
610+
611+-- --------------------------------------------------------------------- [ EOF ]