git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3216 from jfdm/network-cleanup
28ece38Jan de Muijnck-Hughes
libs/contrib/Network/Socket.idr+401−174
compare with master
unifiedsplit
@@ -1,6 +1,7 @@
1−||| Time to do this properly.
2||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
1||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
2+|||
3−||| (C) SimonJF, MIT Licensed, 2014
3+||| Original (C) SimonJF, MIT Licensed, 2014
4+||| Modified (C) The Idris Community, 2015, 2016
4module Network.Socket
5module Network.Socket
5
6
6%include C "idris_net.h"
7%include C "idris_net.h"
@@ -8,119 +9,155 @@ module Network.Socket
8%include C "sys/socket.h"
9%include C "sys/socket.h"
9%include C "netdb.h"
10%include C "netdb.h"
10
11
12+-- ------------------------------------------------------------ [ Type Aliases ]
13+
11public export
14public export
12ByteLength : Type
15ByteLength : Type
13ByteLength = Int
16ByteLength = Int
14
17
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+
15export
57export
16interface ToCode a where
58interface ToCode a where
17 toCode : a -> Int
59 toCode : a -> Int
18
60
61+-- --------------------------------------------------------- [ Socket Families ]
62+
19||| Socket Families
63||| Socket Families
20|||
64|||
21||| The ones that people might actually use. We're not going to need US
65||| The ones that people might actually use. We're not going to need US
22||| Government proprietary ones.
66||| Government proprietary ones.
23public export
67public export
24−data SocketFamily =
68+data SocketFamily : Type where
25 ||| Unspecified
69 ||| Unspecified
26− AF_UNSPEC |
70+ AF_UNSPEC : SocketFamily
71+
27 ||| IP / UDP etc. IPv4
72 ||| IP / UDP etc. IPv4
28− AF_INET |
73+ AF_INET : SocketFamily
74+
29 ||| IP / UDP etc. IPv6
75 ||| IP / UDP etc. IPv6
30− AF_INET6
76+ AF_INET6 : SocketFamily
31
77
32export
78export
33−implementation Show SocketFamily where
79+Show SocketFamily where
34 show AF_UNSPEC = "AF_UNSPEC"
80 show AF_UNSPEC = "AF_UNSPEC"
35 show AF_INET = "AF_INET"
81 show AF_INET = "AF_INET"
36 show AF_INET6 = "AF_INET6"
82 show AF_INET6 = "AF_INET6"
37
83
38export
84export
39−implementation ToCode SocketFamily where
85+ToCode SocketFamily where
40 toCode AF_UNSPEC = 0
86 toCode AF_UNSPEC = 0
41 toCode AF_INET = 2
87 toCode AF_INET = 2
42 toCode AF_INET6 = 10
88 toCode AF_INET6 = 10
43
89
44getSocketFamily : Int -> Maybe SocketFamily
90getSocketFamily : Int -> Maybe SocketFamily
91+getSocketFamily i =
45−getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
92+ Prelude.List.lookup i [ (0, AF_UNSPEC)
93+ , (2, AF_INET)
94+ , (10, AF_INET6)
95+ ]
46
96
97+-- ------------------------------------------------------------ [ Socket Types ]
47||| Socket Types.
98||| Socket Types.
48public export
99public export
49−data SocketType =
100+data SocketType : Type where
50 ||| Not a socket, used in certain operations
101 ||| Not a socket, used in certain operations
51− NotASocket |
102+ NotASocket : SocketType
103+
52 ||| TCP
104 ||| TCP
53− Stream |
105+ Stream : SocketType
106+
54 ||| UDP
107 ||| UDP
55− Datagram |
108+ Datagram : SocketType
109+
56 ||| Raw sockets
110 ||| Raw sockets
57− RawSocket
111+ RawSocket : SocketType
58
112
59export
113export
60−implementation Show SocketType where
114+Show SocketType where
61 show NotASocket = "Not a socket"
115 show NotASocket = "Not a socket"
62 show Stream = "Stream"
116 show Stream = "Stream"
63 show Datagram = "Datagram"
117 show Datagram = "Datagram"
64 show RawSocket = "Raw"
118 show RawSocket = "Raw"
65
119
66export
120export
67−implementation ToCode SocketType where
121+ToCode SocketType where
68 toCode NotASocket = 0
122 toCode NotASocket = 0
69 toCode Stream = 1
123 toCode Stream = 1
70 toCode Datagram = 2
124 toCode Datagram = 2
71 toCode RawSocket = 3
125 toCode RawSocket = 3
72
126
127+-- ---------------------------------------------------------------- [ Pointers ]
128+
73data RecvStructPtr = RSPtr Ptr
129data RecvStructPtr = RSPtr Ptr
74data RecvfromStructPtr = RFPtr Ptr
130data RecvfromStructPtr = RFPtr Ptr
75
131
76export
132export
77data BufPtr = BPtr Ptr
133data BufPtr = BPtr Ptr
134+
78export
135export
79data SockaddrPtr = SAPtr Ptr
136data SockaddrPtr = SAPtr Ptr
80
137
81−||| Protocol Number.
138+-- --------------------------------------------------------------- [ Addresses ]
82−|||
83−||| Generally good enough to just set it to 0.
84−public export
85−ProtocolNumber : Type
86−ProtocolNumber = Int
87
139
88−||| SocketError: Error thrown by a socket operation
140+||| Network Addresses
89public export
141public export
90−SocketError : Type
142+data SocketAddress : Type where
91−SocketError = Int
143+ IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
92
144
93−||| SocketDescriptor: Native C Socket Descriptor
145+ ||| Not implemented (yet)
94−public export
146+ IPv6Addr : SocketAddress
95−SocketDescriptor : Type
96−SocketDescriptor = Int
97
147
98−public export
99−data SocketAddress = IPv4Addr Int Int Int Int
100− | IPv6Addr -- Not implemented (yet)
101− | Hostname String
148+ Hostname : String -> SocketAddress
149+
102− | InvalidAddress -- Used when there's a parse error
150+ ||| Used when there's a parse error
151+ InvalidAddress : SocketAddress
103
152
104export
153export
105−implementation Show SocketAddress where
154+Show SocketAddress where
106 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
155 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
107− show IPv6Addr = "NOT IMPLEMENTED YET"
156+ show IPv6Addr = "NOT IMPLEMENTED YET"
108− show (Hostname host) = host
157+ show (Hostname host) = host
109− show InvalidAddress = "Invalid"
158+ show InvalidAddress = "Invalid"
110
159
111−public export
160+-- --------------------------------------------------------- [ UDP Information ]
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
124
161
125-- TODO: Expand to non-string payloads
162-- TODO: Expand to non-string payloads
126export
163export
@@ -128,8 +165,8 @@ record UDPRecvData where
128 constructor MkUDPRecvData
165 constructor MkUDPRecvData
129 remote_addr : SocketAddress
166 remote_addr : SocketAddress
130 remote_port : Port
167 remote_port : Port
131− recv_data : String
168+ recv_data : String
132− data_len : Int
169+ data_len : Int
133
170
134export
171export
135record UDPAddrInfo where
172record UDPAddrInfo where
@@ -137,6 +174,8 @@ record UDPAddrInfo where
137 remote_addr : SocketAddress
174 remote_addr : SocketAddress
138 remote_port : Port
175 remote_port : Port
139
176
177+-- ---------------------------------------------------------- [ Socket Utilies ]
178+
140||| Frees a given pointer
179||| Frees a given pointer
141export
180export
142sock_free : BufPtr -> IO ()
181sock_free : BufPtr -> IO ()
@@ -153,25 +192,34 @@ export
153sock_alloc : ByteLength -> IO BufPtr
192sock_alloc : ByteLength -> IO BufPtr
154sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
193sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
155
194
195+-- ----------------------------------------------------------------- [ Sockets ]
156||| The metadata about a socket
196||| The metadata about a socket
157export
197export
158record Socket where
198record Socket where
159 constructor MkSocket
199 constructor MkSocket
160− descriptor : SocketDescriptor
200+ descriptor : SocketDescriptor
161− family : SocketFamily
201+ family : SocketFamily
162− socketType : SocketType
202+ socketType : SocketType
163 protocolNumber : ProtocolNumber
203 protocolNumber : ProtocolNumber
164
204
205+
206+-- ----------------------------------------------------- [ Network Socket API. ]
207+
165||| Creates a UNIX socket with the given family, socket type and protocol
208||| Creates a UNIX socket with the given family, socket type and protocol
166||| number. Returns either a socket or an error.
209||| number. Returns either a socket or an error.
167export
210export
211+socket : (fam : SocketFamily)
212+ -> (ty : SocketType)
213+ -> (pnum : ProtocolNumber)
168−socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
214+ -> IO (Either SocketError Socket)
169socket sf st pn = do
215socket sf st pn = do
170− socket_res <- foreign FFI_C "socket" (Int -> Int -> Int -> IO Int) (toCode sf) (toCode st) pn
216+ socket_res <- foreign FFI_C "socket"
217+ (Int -> Int -> Int -> IO Int)
218+ (toCode sf) (toCode st) pn
219+
171− if socket_res == -1 then -- error
220+ if socket_res == -1
172− map Left getErrno
221+ then map Left getErrno
173− else
174− return $ Right (MkSocket socket_res sf st pn)
222+ else return $ Right (MkSocket socket_res sf st pn)
175
223
176||| Close a socket
224||| Close a socket
177export
225export
@@ -186,199 +234,378 @@ saString Nothing = ""
186||| Binds a socket to the given socket address and port.
234||| Binds a socket to the given socket address and port.
187||| Returns 0 on success, an error code otherwise.
235||| Returns 0 on success, an error code otherwise.
188export
236export
237+bind : (sock : Socket)
189−bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
238+ -> (addr : Maybe SocketAddress)
239+ -> (port : Port)
240+ -> IO Int
190bind sock addr port = do
241bind sock addr port = do
191 bind_res <- foreign FFI_C "idrnet_bind"
242 bind_res <- foreign FFI_C "idrnet_bind"
192 (Int -> Int -> Int -> String -> Int -> IO Int)
243 (Int -> Int -> Int -> String -> Int -> IO Int)
193 (descriptor sock) (toCode $ family sock)
244 (descriptor sock) (toCode $ family sock)
194 (toCode $ socketType sock) (saString addr) port
245 (toCode $ socketType sock) (saString addr) port
195− if bind_res == (-1) then -- error
246+ if bind_res == (-1)
196− getErrno
247+ then getErrno
197− else return 0 -- Success
248+ else return 0
198
249
199||| Connects to a given address and port.
250||| Connects to a given address and port.
200||| Returns 0 on success, and an error number on error.
251||| Returns 0 on success, and an error number on error.
201export
252export
202−connect : Socket -> SocketAddress -> Port -> IO Int
253+connect : (sock : Socket)
254+ -> (addr : SocketAddress)
255+ -> (port : Port)
256+ -> IO ResultCode
203connect sock addr port = do
257connect sock addr port = do
204 conn_res <- foreign FFI_C "idrnet_connect"
258 conn_res <- foreign FFI_C "idrnet_connect"
205 (Int -> Int -> Int -> String -> Int -> IO Int)
259 (Int -> Int -> Int -> String -> Int -> IO Int)
206 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port
260 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port
261+
207− if conn_res == (-1) then
262+ if conn_res == (-1)
208− getErrno
263+ then getErrno
209− else return 0
264+ else return 0
210
265
211||| Listens on a bound socket.
266||| Listens on a bound socket.
267+|||
268+||| @sock The socket to listen on.
212export
269export
213−listen : Socket -> IO Int
270+listen : (sock : Socket) -> IO Int
214listen sock = do
271listen sock = do
215 listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)
272 listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)
216 (descriptor sock) BACKLOG
273 (descriptor sock) BACKLOG
217− if listen_res == (-1) then
274+ if listen_res == (-1)
218− getErrno
275+ then getErrno
219− else return 0
276+ else return 0
220
277
221||| Parses a textual representation of an IPv4 address into a SocketAddress
278||| Parses a textual representation of an IPv4 address into a SocketAddress
222parseIPv4 : String -> SocketAddress
279parseIPv4 : String -> SocketAddress
280+parseIPv4 str =
223−parseIPv4 str = case splitted of
281+ case splitted of
224− (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
282+ (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
225− _ => InvalidAddress
283+ otherwise => InvalidAddress
284+ where
226− where toInt' : String -> Integer
285+ toInt' : String -> Integer
227− toInt' = cast
286+ toInt' = cast
287+
228− toInt : String -> Int
288+ toInt : String -> Int
229− toInt s = fromInteger $ toInt' s
289+ toInt s = fromInteger $ toInt' s
290+
230− splitted : List Int
291+ splitted : List Int
231− splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
292+ splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
232
293
233||| Retrieves a socket address from a sockaddr pointer
294||| Retrieves a socket address from a sockaddr pointer
234getSockAddr : SockaddrPtr -> IO SocketAddress
295getSockAddr : SockaddrPtr -> IO SocketAddress
235getSockAddr (SAPtr ptr) = do
296getSockAddr (SAPtr ptr) = do
236− addr_family_int <- foreign FFI_C "idrnet_sockaddr_family" (Ptr -> IO Int) ptr
297+ addr_family_int <- foreign FFI_C "idrnet_sockaddr_family"
237− -- putStrLn $ "Addr family int: " ++ (show addr_family_int)
298+ (Ptr -> IO Int)
299+ ptr
300+
238 -- ASSUMPTION: Foreign call returns a valid int
301 -- ASSUMPTION: Foreign call returns a valid int
239 assert_total (case getSocketFamily addr_family_int of
302 assert_total (case getSocketFamily addr_family_int of
240 Just AF_INET => do
303 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+
242 return $ parseIPv4 ipv4_addr
308 return $ parseIPv4 ipv4_addr
243 Just AF_INET6 => return IPv6Addr
309 Just AF_INET6 => return IPv6Addr
244 Just AF_UNSPEC => return InvalidAddress)
310 Just AF_UNSPEC => return InvalidAddress)
245
311
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.
246export
320export
321+accept : (sock : Socket)
247−accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
322+ -> IO (Either SocketError (Socket, SocketAddress))
248accept sock = do
323accept sock = do
324+
249 -- We need a pointer to a sockaddr structure. This is then passed into
325 -- We need a pointer to a sockaddr structure. This is then passed into
250 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
326 -- 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)
260
327
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.
261export
349export
350+send : (sock : Socket)
351+ -> (msg : String)
262−send : Socket -> String -> IO (Either SocketError ByteLength)
352+ -> IO (Either SocketError ResultCode)
263send sock dat = do
353send sock dat = do
264− send_res <- foreign FFI_C "idrnet_send" (Int -> String -> IO Int) (descriptor sock) dat
354+ send_res <- foreign FFI_C "idrnet_send"
355+ (Int -> String -> IO Int)
356+ (descriptor sock) dat
357+
265− if send_res == (-1) then
358+ if send_res == (-1)
266− map Left getErrno
359+ then map Left getErrno
267− else
268− return $ Right send_res
360+ else return $ Right send_res
269
361
270freeRecvStruct : RecvStructPtr -> IO ()
362freeRecvStruct : RecvStructPtr -> IO ()
363+freeRecvStruct (RSPtr p) =
271−freeRecvStruct (RSPtr p) = foreign FFI_C "idrnet_free_recv_struct" (Ptr -> IO ()) p
364+ foreign FFI_C "idrnet_free_recv_struct"
365+ (Ptr -> IO ())
366+ p
272
367
368+||| Utility to extract data.
273freeRecvfromStruct : RecvfromStructPtr -> IO ()
369freeRecvfromStruct : RecvfromStructPtr -> IO ()
370+freeRecvfromStruct (RFPtr p) =
274−freeRecvfromStruct (RFPtr p) = foreign FFI_C "idrnet_free_recvfrom_struct" (Ptr -> IO ()) p
371+ foreign FFI_C "idrnet_free_recvfrom_struct"
372+ (Ptr -> IO ())
373+ p
275
374
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.
276export
385export
386+recv : (sock : Socket)
387+ -> (len : ByteLength)
277−recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
388+ -> IO (Either SocketError (String, ResultCode))
278recv sock len = do
389recv sock len = do
279 -- Firstly make the request, get some kind of recv structure which
390 -- Firstly make the request, get some kind of recv structure which
280 -- contains the result of the recv and possibly the retrieved payload
391 -- 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
392+ recv_struct_ptr <- foreign FFI_C "idrnet_recv"
393+ (Int -> Int -> IO Ptr)
394+ (descriptor sock) len
282− recv_res <- foreign FFI_C "idrnet_get_recv_res" (Ptr -> IO Int) recv_struct_ptr
395+ recv_res <- foreign FFI_C "idrnet_get_recv_res"
396+ (Ptr -> IO Int)
397+ recv_struct_ptr
398+
283− if recv_res == (-1) then do
399+ if recv_res == (-1)
400+ then do
284− errno <- getErrno
401+ errno <- getErrno
285− freeRecvStruct (RSPtr recv_struct_ptr)
402+ freeRecvStruct (RSPtr recv_struct_ptr)
286− return $ Left errno
403+ return $ Left errno
287− else
404+ else
288− if recv_res == 0 then do
405+ if recv_res == 0
406+ then do
289− freeRecvStruct (RSPtr recv_struct_ptr)
407+ freeRecvStruct (RSPtr recv_struct_ptr)
290− return $ Left 0
408+ return $ Left 0
291− else do
409+ else do
292− payload <- foreign FFI_C "idrnet_get_recv_payload" (Ptr -> IO String) recv_struct_ptr
410+ payload <- foreign FFI_C "idrnet_get_recv_payload"
411+ (Ptr -> IO String)
412+ recv_struct_ptr
293− freeRecvStruct (RSPtr recv_struct_ptr)
413+ freeRecvStruct (RSPtr recv_struct_ptr)
294− return $ Right (payload, recv_res)
414+ return $ Right (payload, recv_res)
295
415
296||| Sends the data in a given memory location
416||| Sends the data in a given memory location
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)
297−sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
427+ -> IO (Either SocketError ResultCode)
298sendBuf sock (BPtr ptr) len = do
428sendBuf sock (BPtr ptr) len = do
299− send_res <- foreign FFI_C "idrnet_send_buf" (Int -> Ptr -> Int -> IO Int) (descriptor sock) ptr len
429+ send_res <- foreign FFI_C "idrnet_send_buf"
300− if send_res == (-1) then
430+ (Int -> Ptr -> Int -> IO Int)
301− map Left getErrno
431+ (descriptor sock) ptr len
302− else
303− return $ Right send_res
304
432
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)
305−recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
448+ -> IO (Either SocketError ResultCode)
306recvBuf sock (BPtr ptr) len = do
449recvBuf sock (BPtr ptr) len = do
307− recv_res <- foreign FFI_C "idrnet_recv_buf" (Int -> Ptr -> Int -> IO Int) (descriptor sock) ptr len
450+ recv_res <- foreign FFI_C "idrnet_recv_buf"
451+ (Int -> Ptr -> Int -> IO Int)
452+ (descriptor sock) ptr len
453+
308− if (recv_res == (-1)) then
454+ if (recv_res == (-1))
309− map Left getErrno
455+ then map Left getErrno
310− else
311− return $ Right recv_res
456+ else return $ Right recv_res
312
457
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.
313export
467export
468+sendTo : (sock : Socket)
469+ -> (addr : SocketAddress)
470+ -> (port : Port)
471+ -> (msg : String)
314−sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)
472+ -> IO (Either SocketError ByteLength)
315sendTo sock addr p dat = do
473sendTo sock addr p dat = do
316 sendto_res <- foreign FFI_C "idrnet_sendto"
474 sendto_res <- foreign FFI_C "idrnet_sendto"
317 (Int -> String -> String -> Int -> Int -> IO Int)
475 (Int -> String -> String -> Int -> Int -> IO Int)
318 (descriptor sock) dat (show addr) p (toCode $ family sock)
476 (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
323
477
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)
325sendToBuf sock addr p (BPtr dat) len = do
498sendToBuf sock addr p (BPtr dat) len = do
326 sendto_res <- foreign FFI_C "idrnet_sendto_buf"
499 sendto_res <- foreign FFI_C "idrnet_sendto_buf"
327 (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)
500 (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)
328 (descriptor sock) dat len (show addr) p (toCode $ family sock)
501 (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
333
502
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`.
334foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
508foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
335−foreignGetRecvfromPayload (RFPtr p)
509+foreignGetRecvfromPayload (RFPtr p) =
336− = foreign FFI_C "idrnet_get_recvfrom_payload" (Ptr -> IO String) p
510+ foreign FFI_C "idrnet_get_recvfrom_payload"
511+ (Ptr -> IO String)
512+ p
337
513
514+||| Utility function to return senders socket address.
338foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
515foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
339foreignGetRecvfromAddr (RFPtr p) = do
516foreignGetRecvfromAddr (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
341 getSockAddr sockaddr_ptr
520 getSockAddr sockaddr_ptr
342
521
522+||| Utility function to return sender's IPV4 port.
343foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
523foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
344foreignGetRecvfromPort (RFPtr p) = do
524foreignGetRecvfromPort (RFPtr p) = do
345− sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p
525+ sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr"
526+ (Ptr -> IO Ptr)
527+ p
346− port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" (Ptr -> IO Int) sockaddr_ptr
528+ port <- foreign FFI_C "idrnet_sockaddr_ipv4_port"
529+ (Ptr -> IO Int)
530+ sockaddr_ptr
347 return port
531 return port
348
532
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+|||
349export
545export
546+recvFrom : (sock : Socket)
547+ -> (len : ByteLength)
350−recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))
548+ -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))
351recvFrom sock bl = do
549recvFrom 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)
353 (descriptor sock) bl
552 (descriptor sock) bl
553+
354 let recv_ptr' = RFPtr recv_ptr
554 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)
368
555
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)
369−recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))
587+ -> IO (Either SocketError (UDPAddrInfo, ResultCode))
370recvFromBuf sock (BPtr ptr) bl = do
588recvFromBuf 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+
372 let recv_ptr' = RFPtr recv_ptr
593 let recv_ptr' = RFPtr recv_ptr
594+
373− if !(nullPtr recv_ptr) then
595+ if !(nullPtr recv_ptr)
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
596+ then map Left getErrno
380 else do
597 else do
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
381− port <- foreignGetRecvfromPort recv_ptr'
606+ port <- foreignGetRecvfromPort recv_ptr'
382− addr <- foreignGetRecvfromAddr recv_ptr'
607+ addr <- foreignGetRecvfromAddr recv_ptr'
383− freeRecvfromStruct recv_ptr'
608+ freeRecvfromStruct recv_ptr'
384− return $ Right (MkUDPAddrInfo addr port, result + 1)
609+ return $ Right (MkUDPAddrInfo addr port, result + 1)
610+
611+-- --------------------------------------------------------------------- [ EOF ]