git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3583 from PoroCYon/master
c90347fEdwin Brady
libs/contrib/Network/Socket.idr+15−396
compare with master
unifiedsplit
@@ -4,210 +4,20 @@
4||| Modified (C) The Idris Community, 2015, 2016
4||| Modified (C) The Idris Community, 2015, 2016
5module Network.Socket
5module Network.Socket
6
6
7+import public Network.Socket.Data
8+import Network.Socket.Raw
9+
7%include C "idris_net.h"
10%include C "idris_net.h"
8%include C "sys/types.h"
11%include C "sys/types.h"
9%include C "sys/socket.h"
12%include C "sys/socket.h"
10%include C "netdb.h"
13%include C "netdb.h"
11
14
12−-- ------------------------------------------------------------ [ Type Aliases ]
13−
14−public export
15+%access export
15−ByteLength : Type
16−ByteLength = Int
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−
57−export
58−interface ToCode a where
59− toCode : a -> Int
60−
61−-- --------------------------------------------------------- [ Socket Families ]
62−
63−||| Socket Families
64−|||
65−||| The ones that people might actually use. We're not going to need US
66−||| Government proprietary ones.
67−public export
68−data SocketFamily : Type where
69− ||| Unspecified
70− AF_UNSPEC : SocketFamily
71−
72− ||| IP / UDP etc. IPv4
73− AF_INET : SocketFamily
74−
75− ||| IP / UDP etc. IPv6
76− AF_INET6 : SocketFamily
77−
78−export
79−Show SocketFamily where
80− show AF_UNSPEC = "AF_UNSPEC"
81− show AF_INET = "AF_INET"
82− show AF_INET6 = "AF_INET6"
83−
84−export
85−ToCode SocketFamily where
86− toCode AF_UNSPEC = 0
87− toCode AF_INET = 2
88− toCode AF_INET6 = 10
89−
90−getSocketFamily : Int -> Maybe SocketFamily
91−getSocketFamily i =
92− Prelude.List.lookup i [ (0, AF_UNSPEC)
93− , (2, AF_INET)
94− , (10, AF_INET6)
95− ]
96−
97−-- ------------------------------------------------------------ [ Socket Types ]
98−||| Socket Types.
99−public export
100−data SocketType : Type where
101− ||| Not a socket, used in certain operations
102− NotASocket : SocketType
103−
104− ||| TCP
105− Stream : SocketType
106−
107− ||| UDP
108− Datagram : SocketType
109−
110− ||| Raw sockets
111− RawSocket : SocketType
112−
113−export
114−Show SocketType where
115− show NotASocket = "Not a socket"
116− show Stream = "Stream"
117− show Datagram = "Datagram"
118− show RawSocket = "Raw"
119−
120−export
121−ToCode SocketType where
122− toCode NotASocket = 0
123− toCode Stream = 1
124− toCode Datagram = 2
125− toCode RawSocket = 3
126−
127−-- ---------------------------------------------------------------- [ Pointers ]
128−
129−data RecvStructPtr = RSPtr Ptr
130−data RecvfromStructPtr = RFPtr Ptr
131−
132−export
133−data BufPtr = BPtr Ptr
134−
135−export
136−data SockaddrPtr = SAPtr Ptr
137−
138−-- --------------------------------------------------------------- [ Addresses ]
139−
140−||| Network Addresses
141−public export
142−data SocketAddress : Type where
143− IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
144−
145− ||| Not implemented (yet)
146− IPv6Addr : SocketAddress
147−
148− Hostname : String -> SocketAddress
149−
150− ||| Used when there's a parse error
151− InvalidAddress : SocketAddress
152−
153−export
154−Show SocketAddress where
155− show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
156− show IPv6Addr = "NOT IMPLEMENTED YET"
157− show (Hostname host) = host
158− show InvalidAddress = "Invalid"
159−
160−-- --------------------------------------------------------- [ UDP Information ]
161−
162−-- TODO: Expand to non-string payloads
163−export
164−record UDPRecvData where
165− constructor MkUDPRecvData
166− remote_addr : SocketAddress
167− remote_port : Port
168− recv_data : String
169− data_len : Int
170−
171−export
172−record UDPAddrInfo where
173− constructor MkUDPAddrInfo
174− remote_addr : SocketAddress
175− remote_port : Port
176−
177−-- ---------------------------------------------------------- [ Socket Utilies ]
178−
179−||| Frees a given pointer
180−export
181−sock_free : BufPtr -> IO ()
182−sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
183−
184−export
185−sockaddr_free : SockaddrPtr -> IO ()
186−sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
187−
188−||| Allocates an amount of memory given by the ByteLength parameter.
189−|||
190−||| Used to allocate a mutable pointer to be given to the Recv functions.
191−export
192−sock_alloc : ByteLength -> IO BufPtr
193−sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
194−
195−-- ----------------------------------------------------------------- [ Sockets ]
196−||| The metadata about a socket
197−export
198−record Socket where
199− constructor MkSocket
200− descriptor : SocketDescriptor
201− family : SocketFamily
202− socketType : SocketType
203− protocolNumber : ProtocolNumber
204−
205
16
206-- ----------------------------------------------------- [ Network Socket API. ]
17-- ----------------------------------------------------- [ Network Socket API. ]
207
18
208||| Creates a UNIX socket with the given family, socket type and protocol
19||| Creates a UNIX socket with the given family, socket type and protocol
209||| number. Returns either a socket or an error.
20||| number. Returns either a socket or an error.
210−export
211socket : (fam : SocketFamily)
21socket : (fam : SocketFamily)
212 -> (ty : SocketType)
22 -> (ty : SocketType)
213 -> (pnum : ProtocolNumber)
23 -> (pnum : ProtocolNumber)
@@ -222,34 +32,30 @@ socket sf st pn = do
222 else pure $ Right (MkSocket socket_res sf st pn)
32 else pure $ Right (MkSocket socket_res sf st pn)
223
33
224||| Close a socket
34||| Close a socket
225−export
226close : Socket -> IO ()
35close : Socket -> IO ()
227close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock)
36close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock)
228
37
229−private
230−saString : (Maybe SocketAddress) -> String
231−saString (Just sa) = show sa
232−saString Nothing = ""
233−
234||| Binds a socket to the given socket address and port.
38||| Binds a socket to the given socket address and port.
235||| Returns 0 on success, an error code otherwise.
39||| Returns 0 on success, an error code otherwise.
236−export
237bind : (sock : Socket)
40bind : (sock : Socket)
238 -> (addr : Maybe SocketAddress)
41 -> (addr : Maybe SocketAddress)
239 -> (port : Port)
42 -> (port : Port)
240 -> IO Int
43 -> IO Int
241bind sock addr port = do
44bind sock addr port = do
242− bind_res <- foreign FFI_C "idrnet_bind"
45+ bind_res <- foreign FFI_C "idrnet_bind"
243− (Int -> Int -> Int -> String -> Int -> IO Int)
46+ (Int -> Int -> Int -> String -> Int -> IO Int)
244− (descriptor sock) (toCode $ family sock)
47+ (descriptor sock) (toCode $ family sock)
245− (toCode $ socketType sock) (saString addr) port
48+ (toCode $ socketType sock) (saString addr) port
246− if bind_res == (-1)
49+ if bind_res == (-1)
247− then getErrno
50+ then getErrno
248− else pure 0
51+ else pure 0
52+ where
53+ saString : Maybe SocketAddress -> String
54+ saString (Just sa) = show sa
55+ saString Nothing = ""
249
56
250||| Connects to a given address and port.
57||| Connects to a given address and port.
251||| Returns 0 on success, and an error number on error.
58||| Returns 0 on success, and an error number on error.
252−export
253connect : (sock : Socket)
59connect : (sock : Socket)
254 -> (addr : SocketAddress)
60 -> (addr : SocketAddress)
255 -> (port : Port)
61 -> (port : Port)
@@ -266,7 +72,6 @@ connect sock addr port = do
266||| Listens on a bound socket.
72||| Listens on a bound socket.
267|||
73|||
268||| @sock The socket to listen on.
74||| @sock The socket to listen on.
269−export
270listen : (sock : Socket) -> IO Int
75listen : (sock : Socket) -> IO Int
271listen sock = do
76listen sock = do
272 listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)
77 listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)
@@ -275,40 +80,6 @@ listen sock = do
275 then getErrno
80 then getErrno
276 else pure 0
81 else pure 0
277
82
278−||| Parses a textual representation of an IPv4 address into a SocketAddress
279−parseIPv4 : String -> SocketAddress
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)
293−
294−||| Retrieves a socket address from a sockaddr pointer
295−getSockAddr : SockaddrPtr -> IO SocketAddress
296−getSockAddr (SAPtr ptr) = do
297− addr_family_int <- foreign FFI_C "idrnet_sockaddr_family"
298− (Ptr -> IO Int)
299− ptr
300−
301− -- ASSUMPTION: Foreign call returns a valid int
302− assert_total (case getSocketFamily addr_family_int of
303− Just AF_INET => do
304− ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4"
305− (Ptr -> IO String)
306− ptr
307−
308− pure $ parseIPv4 ipv4_addr
309− Just AF_INET6 => pure IPv6Addr
310− Just AF_UNSPEC => pure InvalidAddress)
311−
312||| Accept a connection on the provided socket.
83||| Accept a connection on the provided socket.
313|||
84|||
314||| Returns on failure a `SocketError`
85||| Returns on failure a `SocketError`
@@ -317,7 +88,6 @@ getSockAddr (SAPtr ptr) = do
317||| + `SocketAddress` :: The
88||| + `SocketAddress` :: The
318|||
89|||
319||| @sock The socket used to establish connection.
90||| @sock The socket used to establish connection.
320−export
321accept : (sock : Socket)
91accept : (sock : Socket)
322 -> IO (Either SocketError (Socket, SocketAddress))
92 -> IO (Either SocketError (Socket, SocketAddress))
323accept sock = do
93accept sock = do
@@ -346,7 +116,6 @@ accept sock = do
346|||
116|||
347||| @sock The socket on which to send the message.
117||| @sock The socket on which to send the message.
348||| @msg The data to send.
118||| @msg The data to send.
349−export
350send : (sock : Socket)
119send : (sock : Socket)
351 -> (msg : String)
120 -> (msg : String)
352 -> IO (Either SocketError ResultCode)
121 -> IO (Either SocketError ResultCode)
@@ -359,20 +128,6 @@ send sock dat = do
359 then map Left getErrno
128 then map Left getErrno
360 else pure $ Right send_res
129 else pure $ Right send_res
361
130
362−freeRecvStruct : RecvStructPtr -> IO ()
363−freeRecvStruct (RSPtr p) =
364− foreign FFI_C "idrnet_free_recv_struct"
365− (Ptr -> IO ())
366− p
367−
368−||| Utility to extract data.
369−freeRecvfromStruct : RecvfromStructPtr -> IO ()
370−freeRecvfromStruct (RFPtr p) =
371− foreign FFI_C "idrnet_free_recvfrom_struct"
372− (Ptr -> IO ())
373− p
374−
375−
376||| Receive data on the specified socket.
131||| Receive data on the specified socket.
377|||
132|||
378||| Returns on failure a `SocketError`
133||| Returns on failure a `SocketError`
@@ -382,7 +137,6 @@ freeRecvfromStruct (RFPtr p) =
382|||
137|||
383||| @sock The socket on which to receive the message.
138||| @sock The socket on which to receive the message.
384||| @len How much of the data to send.
139||| @len How much of the data to send.
385−export
386recv : (sock : Socket)
140recv : (sock : Socket)
387 -> (len : ByteLength)
141 -> (len : ByteLength)
388 -> IO (Either SocketError (String, ResultCode))
142 -> IO (Either SocketError (String, ResultCode))
@@ -413,48 +167,6 @@ recv sock len = do
413 freeRecvStruct (RSPtr recv_struct_ptr)
167 freeRecvStruct (RSPtr recv_struct_ptr)
414 pure $ Right (payload, recv_res)
168 pure $ Right (payload, recv_res)
415
169
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)
427− -> IO (Either SocketError ResultCode)
428−sendBuf sock (BPtr ptr) len = do
429− send_res <- foreign FFI_C "idrnet_send_buf"
430− (Int -> Ptr -> Int -> IO Int)
431− (descriptor sock) ptr len
432−
433− if send_res == (-1)
434− then map Left getErrno
435− else pure $ 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)
449−recvBuf sock (BPtr ptr) len = do
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 pure $ Right recv_res
457−
458||| Send a message.
170||| Send a message.
459|||
171|||
460||| Returns on failure a `SocketError`
172||| Returns on failure a `SocketError`
@@ -464,7 +176,6 @@ recvBuf sock (BPtr ptr) len = do
464||| @addr Address of the recipient.
176||| @addr Address of the recipient.
465||| @port The port on which to send the message.
177||| @port The port on which to send the message.
466||| @msg The message to send.
178||| @msg The message to send.
467−export
468sendTo : (sock : Socket)
179sendTo : (sock : Socket)
469 -> (addr : SocketAddress)
180 -> (addr : SocketAddress)
470 -> (port : Port)
181 -> (port : Port)
@@ -479,58 +190,6 @@ sendTo sock addr p dat = do
479 then map Left getErrno
190 then map Left getErrno
480 else pure $ Right sendto_res
191 else pure $ Right sendto_res
481
192
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)
498−sendToBuf sock addr p (BPtr dat) len = do
499− sendto_res <- foreign FFI_C "idrnet_sendto_buf"
500− (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)
501− (descriptor sock) dat len (show addr) p (toCode $ family sock)
502−
503− if sendto_res == (-1)
504− then map Left getErrno
505− else pure $ Right sendto_res
506−
507−||| Utility function to get the payload of the sent message as a `String`.
508−foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
509−foreignGetRecvfromPayload (RFPtr p) =
510− foreign FFI_C "idrnet_get_recvfrom_payload"
511− (Ptr -> IO String)
512− p
513−
514−||| Utility function to return senders socket address.
515−foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
516−foreignGetRecvfromAddr (RFPtr p) = do
517− sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr"
518− (Ptr -> IO Ptr)
519− p
520− getSockAddr sockaddr_ptr
521−
522−||| Utility function to return sender's IPV4 port.
523−foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
524−foreignGetRecvfromPort (RFPtr p) = do
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
531− pure port
532−
533−
534||| Receive a message.
193||| Receive a message.
535|||
194|||
536||| Returns on failure a `SocketError`.
195||| Returns on failure a `SocketError`.
@@ -542,7 +201,6 @@ foreignGetRecvfromPort (RFPtr p) = do
542||| @sock The channel on which to receive.
201||| @sock The channel on which to receive.
543||| @len Size of the expected message.
202||| @len Size of the expected message.
544|||
203|||
545−export
546recvFrom : (sock : Socket)
204recvFrom : (sock : Socket)
547 -> (len : ByteLength)
205 -> (len : ByteLength)
548 -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))
206 -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))
@@ -570,42 +228,3 @@ recvFrom sock bl = do
570 freeRecvfromStruct recv_ptr'
228 freeRecvfromStruct recv_ptr'
571 pure $ Right (MkUDPAddrInfo addr port, payload, result)
229 pure $ Right (MkUDPAddrInfo addr port, payload, result)
572
230
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))
588−recvFromBuf sock (BPtr ptr) bl = do
589− recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf"
590− (Int -> Ptr -> Int -> IO Ptr)
591− (descriptor sock) ptr bl
592−
593− let recv_ptr' = RFPtr recv_ptr
594−
595− if !(nullPtr recv_ptr)
596− then map Left getErrno
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
606− port <- foreignGetRecvfromPort recv_ptr'
607− addr <- foreignGetRecvfromAddr recv_ptr'
608− freeRecvfromStruct recv_ptr'
609− pure $ Right (MkUDPAddrInfo addr port, result + 1)
610−
611−-- --------------------------------------------------------------------- [ EOF ]
libs/contrib/Network/Socket/Data.idrnew file+172
@@ -0,0 +1,172 @@
1+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
2+||| Types used by Network.Socket.Raw and Network.Socket.
3+|||
4+||| Original (C) SimonJF, MIT Licensed, 2014
5+||| Modified (C) The Idris Community, 2015, 2016
6+module Network.Socket.Data
7+
8+%access public export
9+
10+-- ------------------------------------------------------------ [ Type Aliases ]
11+
12+ByteLength : Type
13+ByteLength = Int
14+
15+ResultCode : Type
16+ResultCode = Int
17+
18+||| Protocol Number.
19+|||
20+||| Generally good enough to just set it to 0.
21+ProtocolNumber : Type
22+ProtocolNumber = Int
23+
24+||| SocketError: Error thrown by a socket operation
25+SocketError : Type
26+SocketError = Int
27+
28+||| SocketDescriptor: Native C Socket Descriptor
29+SocketDescriptor : Type
30+SocketDescriptor = Int
31+
32+Port : Type
33+Port = Int
34+
35+-- --------------------------------------------------------------- [ Constants ]
36+
37+||| Backlog used within listen() call -- number of incoming calls
38+BACKLOG : Int
39+BACKLOG = 20
40+
41+EAGAIN : Int
42+EAGAIN =
43+ -- I'm sorry
44+ -- maybe
45+ unsafePerformIO $ foreign FFI_C "idrnet_geteagain" (() -> IO Int) ()
46+
47+-- -------------------------------------------------------------- [ Interfaces ]
48+
49+interface ToCode a where
50+ toCode : a -> Int
51+
52+-- --------------------------------------------------------- [ Socket Families ]
53+
54+||| Socket Families
55+|||
56+||| The ones that people might actually use. We're not going to need US
57+||| Government proprietary ones.
58+data SocketFamily : Type where
59+ ||| Unspecified
60+ AF_UNSPEC : SocketFamily
61+
62+ ||| IP / UDP etc. IPv4
63+ AF_INET : SocketFamily
64+
65+ ||| IP / UDP etc. IPv6
66+ AF_INET6 : SocketFamily
67+
68+Show SocketFamily where
69+ show AF_UNSPEC = "AF_UNSPEC"
70+ show AF_INET = "AF_INET"
71+ show AF_INET6 = "AF_INET6"
72+
73+ToCode SocketFamily where
74+ toCode AF_UNSPEC = 0
75+ toCode AF_INET = 2
76+ toCode AF_INET6 = 10
77+
78+getSocketFamily : Int -> Maybe SocketFamily
79+getSocketFamily i =
80+ Prelude.List.lookup i [ (0, AF_UNSPEC)
81+ , (2, AF_INET)
82+ , (10, AF_INET6)
83+ ]
84+
85+-- ------------------------------------------------------------ [ Socket Types ]
86+
87+||| Socket Types.
88+data SocketType : Type where
89+ ||| Not a socket, used in certain operations
90+ NotASocket : SocketType
91+
92+ ||| TCP
93+ Stream : SocketType
94+
95+ ||| UDP
96+ Datagram : SocketType
97+
98+ ||| Raw sockets
99+ RawSocket : SocketType
100+
101+Show SocketType where
102+ show NotASocket = "Not a socket"
103+ show Stream = "Stream"
104+ show Datagram = "Datagram"
105+ show RawSocket = "Raw"
106+
107+ToCode SocketType where
108+ toCode NotASocket = 0
109+ toCode Stream = 1
110+ toCode Datagram = 2
111+ toCode RawSocket = 3
112+
113+-- --------------------------------------------------------------- [ Addresses ]
114+
115+||| Network Addresses
116+data SocketAddress : Type where
117+ IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
118+
119+ ||| Not implemented (yet)
120+ IPv6Addr : SocketAddress
121+
122+ Hostname : String -> SocketAddress
123+
124+ ||| Used when there's a parse error
125+ InvalidAddress : SocketAddress
126+
127+Show SocketAddress where
128+ show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
129+ show IPv6Addr = "NOT IMPLEMENTED YET"
130+ show (Hostname host) = host
131+ show InvalidAddress = "Invalid"
132+
133+||| Parses a textual representation of an IPv4 address into a SocketAddress
134+parseIPv4 : String -> SocketAddress
135+parseIPv4 str =
136+ case splitted of
137+ (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
138+ otherwise => InvalidAddress
139+ where
140+ toInt' : String -> Integer
141+ toInt' = cast
142+
143+ toInt : String -> Int
144+ toInt s = fromInteger $ toInt' s
145+
146+ splitted : List Int
147+ splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
148+
149+-- --------------------------------------------------------- [ UDP Information ]
150+
151+-- TODO: Expand to non-string payloads
152+record UDPRecvData where
153+ constructor MkUDPRecvData
154+ remote_addr : SocketAddress
155+ remote_port : Port
156+ recv_data : String
157+ data_len : Int
158+
159+record UDPAddrInfo where
160+ constructor MkUDPAddrInfo
161+ remote_addr : SocketAddress
162+ remote_port : Port
163+
164+-- ----------------------------------------------------------------- [ Sockets ]
165+||| The metadata about a socket
166+record Socket where
167+ constructor MkSocket
168+ descriptor : SocketDescriptor
169+ family : SocketFamily
170+ socketType : SocketType
171+ protocolNumber : ProtocolNumber
172+
libs/contrib/Network/Socket/Raw.idrnew file+202
@@ -0,0 +1,202 @@
1+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
2+||| Type-unsafe parts. Use Network.Socket for a safe variant.
3+|||
4+||| Original (C) SimonJF, MIT Licensed, 2014
5+||| Modified (C) The Idris Community, 2015, 2016
6+module Network.Socket.Raw
7+
8+import public Network.Socket.Data
9+
10+%include C "idris_net.h"
11+%include C "sys/types.h"
12+%include C "sys/socket.h"
13+%include C "netdb.h"
14+
15+%access public export
16+
17+-- ---------------------------------------------------------------- [ Pointers ]
18+
19+data RecvStructPtr = RSPtr Ptr
20+data RecvfromStructPtr = RFPtr Ptr
21+
22+data BufPtr = BPtr Ptr
23+
24+data SockaddrPtr = SAPtr Ptr
25+
26+-- ---------------------------------------------------------- [ Socket Utilies ]
27+
28+||| Frees a given pointer
29+sock_free : BufPtr -> IO ()
30+sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
31+
32+sockaddr_free : SockaddrPtr -> IO ()
33+sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
34+
35+||| Allocates an amount of memory given by the ByteLength parameter.
36+|||
37+||| Used to allocate a mutable pointer to be given to the Recv functions.
38+sock_alloc : ByteLength -> IO BufPtr
39+sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
40+
41+||| Retrieves a socket address from a sockaddr pointer
42+getSockAddr : SockaddrPtr -> IO SocketAddress
43+getSockAddr (SAPtr ptr) = do
44+ addr_family_int <- foreign FFI_C "idrnet_sockaddr_family"
45+ (Ptr -> IO Int)
46+ ptr
47+
48+ -- ASSUMPTION: Foreign call returns a valid int
49+ assert_total (case getSocketFamily addr_family_int of
50+ Just AF_INET => do
51+ ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4"
52+ (Ptr -> IO String)
53+ ptr
54+
55+ pure $ parseIPv4 ipv4_addr
56+ Just AF_INET6 => pure IPv6Addr
57+ Just AF_UNSPEC => pure InvalidAddress)
58+
59+freeRecvStruct : RecvStructPtr -> IO ()
60+freeRecvStruct (RSPtr p) =
61+ foreign FFI_C "idrnet_free_recv_struct"
62+ (Ptr -> IO ())
63+ p
64+
65+||| Utility to extract data.
66+freeRecvfromStruct : RecvfromStructPtr -> IO ()
67+freeRecvfromStruct (RFPtr p) =
68+ foreign FFI_C "idrnet_free_recvfrom_struct"
69+ (Ptr -> IO ())
70+ p
71+
72+||| Sends the data in a given memory location
73+|||
74+||| Returns on failure a `SocketError`
75+||| Returns on success the `ResultCode`
76+|||
77+||| @sock The socket on which to send the message.
78+||| @ptr The location containing the data to send.
79+||| @len How much of the data to send.
80+sendBuf : (sock : Socket)
81+ -> (ptr : BufPtr)
82+ -> (len : ByteLength)
83+ -> IO (Either SocketError ResultCode)
84+sendBuf sock (BPtr ptr) len = do
85+ send_res <- foreign FFI_C "idrnet_send_buf"
86+ (Int -> Ptr -> Int -> IO Int)
87+ (descriptor sock) ptr len
88+
89+ if send_res == (-1)
90+ then map Left getErrno
91+ else pure $ Right send_res
92+
93+||| Receive data from a given memory location.
94+|||
95+||| Returns on failure a `SocketError`
96+||| Returns on success the `ResultCode`
97+|||
98+||| @sock The socket on which to receive the message.
99+||| @ptr The location containing the data to receive.
100+||| @len How much of the data to receive.
101+recvBuf : (sock : Socket)
102+ -> (ptr : BufPtr)
103+ -> (len : ByteLength)
104+ -> IO (Either SocketError ResultCode)
105+recvBuf sock (BPtr ptr) len = do
106+ recv_res <- foreign FFI_C "idrnet_recv_buf"
107+ (Int -> Ptr -> Int -> IO Int)
108+ (descriptor sock) ptr len
109+
110+ if (recv_res == (-1))
111+ then map Left getErrno
112+ else pure $ Right recv_res
113+
114+||| Send a message stored in some buffer.
115+|||
116+||| Returns on failure a `SocketError`
117+||| Returns on success the `ResultCode`
118+|||
119+||| @sock The socket on which to send the message.
120+||| @addr Address of the recipient.
121+||| @port The port on which to send the message.
122+||| @ptr A Pointer to the buffer containing the message.
123+||| @len The size of the message.
124+sendToBuf : (sock : Socket)
125+ -> (addr : SocketAddress)
126+ -> (port : Port)
127+ -> (ptr : BufPtr)
128+ -> (len : ByteLength)
129+ -> IO (Either SocketError ResultCode)
130+sendToBuf sock addr p (BPtr dat) len = do
131+ sendto_res <- foreign FFI_C "idrnet_sendto_buf"
132+ (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)
133+ (descriptor sock) dat len (show addr) p (toCode $ family sock)
134+
135+ if sendto_res == (-1)
136+ then map Left getErrno
137+ else pure $ Right sendto_res
138+
139+||| Utility function to get the payload of the sent message as a `String`.
140+foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
141+foreignGetRecvfromPayload (RFPtr p) =
142+ foreign FFI_C "idrnet_get_recvfrom_payload"
143+ (Ptr -> IO String)
144+ p
145+
146+||| Utility function to return senders socket address.
147+foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
148+foreignGetRecvfromAddr (RFPtr p) = do
149+ sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr"
150+ (Ptr -> IO Ptr)
151+ p
152+ getSockAddr sockaddr_ptr
153+
154+||| Utility function to return sender's IPV4 port.
155+foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
156+foreignGetRecvfromPort (RFPtr p) = do
157+ sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr"
158+ (Ptr -> IO Ptr)
159+ p
160+ port <- foreign FFI_C "idrnet_sockaddr_ipv4_port"
161+ (Ptr -> IO Int)
162+ sockaddr_ptr
163+ pure port
164+
165+||| Receive a message placed on a 'known' buffer.
166+|||
167+||| Returns on failure a `SocketError`.
168+||| Returns on success a pair of
169+||| + `UDPAddrInfo` :: The address of the sender.
170+||| + `Int` :: Result value from underlying function.
171+|||
172+||| @sock The channel on which to receive.
173+||| @ptr Pointer to the buffer to place the message.
174+||| @len Size of the expected message.
175+|||
176+recvFromBuf : (sock : Socket)
177+ -> (ptr : BufPtr)
178+ -> (len : ByteLength)
179+ -> IO (Either SocketError (UDPAddrInfo, ResultCode))
180+recvFromBuf sock (BPtr ptr) bl = do
181+ recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf"
182+ (Int -> Ptr -> Int -> IO Ptr)
183+ (descriptor sock) ptr bl
184+
185+ let recv_ptr' = RFPtr recv_ptr
186+
187+ if !(nullPtr recv_ptr)
188+ then map Left getErrno
189+ else do
190+ result <- foreign FFI_C "idrnet_get_recvfrom_res"
191+ (Ptr -> IO Int)
192+ recv_ptr
193+ if result == -1
194+ then do
195+ freeRecvfromStruct recv_ptr'
196+ map Left getErrno
197+ else do
198+ port <- foreignGetRecvfromPort recv_ptr'
199+ addr <- foreignGetRecvfromAddr recv_ptr'
200+ freeRecvfromStruct recv_ptr'
201+ pure $ Right (MkUDPAddrInfo addr port, result + 1)
202+
libs/contrib/contrib.ipkg+1−1
@@ -25,7 +25,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
25
25
26 Decidable.Decidable, Decidable.Order,
26 Decidable.Decidable, Decidable.Order,
27
27
28− Network.Cgi, Network.Socket,
28+ Network.Cgi, Network.Socket.Data, Network.Socket.Raw, Network.Socket,
29
29
30 System.Concurrency.Process,
30 System.Concurrency.Process,
31
31
rts/idris_net.c+5
@@ -315,3 +315,8 @@ void idrnet_free_recvfrom_struct(void* res_struct) {
315 }
315 }
316 }
316 }
317}
317}
318+
319+int idrnet_geteagain() {
320+ return EAGAIN;
321+}
322+
rts/idris_net.h+1
@@ -73,5 +73,6 @@ void idrnet_free_recvfrom_struct(void* res_struct);
73int idrnet_getaddrinfo(struct addrinfo** address_res, char* host,
73int idrnet_getaddrinfo(struct addrinfo** address_res, char* host,
74 int port, int family, int socket_type);
74 int port, int family, int socket_type);
75
75
76+int idrnet_geteagain();
76
77
77#endif
78#endif
rts/windows/idris_net.c+5
@@ -193,3 +193,8 @@ void idrnet_free_recv_struct(void* res_struct) {
193int idrnet_errno() {
193int idrnet_errno() {
194 return errno;
194 return errno;
195}
195}
196+
197+int idrnet_geteagain() {
198+ return EAGAIN;
199+}
200+