git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/base/Network/Socket.idr
363 lines 12 kB history raw
1-- Time to do this properly.
2-- Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
3-- (C) SimonJF, MIT Licensed, 2014
4module IdrisNet.Socket
6%include C "idris_net.h"
7%include C "sys/types.h"
8%include C "sys/socket.h"
9%include C "netdb.h"
11%access public
13ByteLength : Type
14ByteLength = Int
16class ToCode a where
17 toCode : a -> Int
19||| Socket Families
20|||
21||| The ones that people might actually use. We're not going to need US
22||| Government proprietary ones.
23data SocketFamily =
24 ||| Unspecified
25 AF_UNSPEC |
26 ||| IP / UDP etc. IPv4
27 AF_INET |
28 ||| IP / UDP etc. IPv6
29 AF_INET6
31instance Show SocketFamily where
32 show AF_UNSPEC = "AF_UNSPEC"
33 show AF_INET = "AF_INET"
34 show AF_INET6 = "AF_INET4"
36instance ToCode SocketFamily where
37 toCode AF_UNSPEC = 0
38 toCode AF_INET = 2
39 toCode AF_INET6 = 10
41getSocketFamily : Int -> Maybe SocketFamily
42getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
44||| Socket Types.
45data SocketType =
46 ||| Not a socket, used in certain operations
47 NotASocket |
48 ||| TCP
49 Stream |
50 ||| UDP
51 Datagram |
52 ||| Raw sockets
53 RawSocket
55instance Show SocketType where
56 show NotASocket = "Not a socket"
57 show Stream = "Stream"
58 show Datagram = "Datagram"
59 show Raw = "Raw"
61instance ToCode SocketType where
62 toCode NotASocket = 0
63 toCode Stream = 1
64 toCode Datagram = 2
65 toCode Raw = 3
68data RecvStructPtr = RSPtr Ptr
69data RecvfromStructPtr = RFPtr Ptr
70data BufPtr = BPtr Ptr
71data SockaddrPtr = SAPtr Ptr
73||| Protocol Number.
74|||
75||| Generally good enough to just set it to 0.
76ProtocolNumber : Type
77ProtocolNumber = Int
79||| SocketError: Error thrown by a socket operation
80SocketError : Type
81SocketError = Int
83||| SocketDescriptor: Native C Socket Descriptor
84SocketDescriptor : Type
85SocketDescriptor = Int
87data SocketAddress = IPv4Addr Int Int Int Int
88 | IPv6Addr -- Not implemented (yet)
89 | Hostname String
90 | InvalidAddress -- Used when there's a parse error
92instance Show SocketAddress where
93 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
94 show IPv6Addr = "NOT IMPLEMENTED YET"
95 show (Hostname host) = host
96 show InvalidAddress = "Invalid"
98Port : Type
99Port = Int
101||| Backlog used within listen() call -- number of incoming calls
102BACKLOG : Int
103BACKLOG = 20
105-- FIXME: This *must* be pulled in from C
106EAGAIN : Int
107EAGAIN = 11
109-- TODO: Expand to non-string payloads
110record UDPRecvData : Type where
111 MkUDPRecvData :
112 (remote_addr : SocketAddress) ->
113 (remote_port : Port) ->
114 (recv_data : String) ->
115 (data_len : Int) ->
116 UDPRecvData
118record UDPAddrInfo : Type where
119 MkUDPAddrInfo :
120 (remote_addr : SocketAddress) ->
121 (remote_port : Port) ->
122 UDPAddrInfo
124||| Frees a given pointer
125public
126sock_free : BufPtr -> IO ()
127sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
129public
130sockaddr_free : SockaddrPtr -> IO ()
131sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
133||| Allocates an amount of memory given by the ByteLength parameter.
134|||
135||| Used to allocate a mutable pointer to be given to the Recv functions.
136public
137sock_alloc : ByteLength -> IO BufPtr
138sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
140||| The metadata about a socket
141record Socket : Type where
142 MkSocket : (descriptor : SocketDescriptor) ->
143 (family : SocketFamily) ->
144 (socketType : SocketType) ->
145 (protocolNumber : ProtocolNumber) ->
146 Socket
148||| Get the C error number
149getErrno : IO Int
150getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
152||| Creates a UNIX socket with the given family, socket type and protocol
153||| number. Returns either a socket or an error.
154socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
155socket sf st pn = do
156 socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
157 if socket_res == -1 then -- error
158 map Left getErrno
159 else
160 return $ Right (MkSocket socket_res sf st pn)
162||| Close a socket
163close : Socket -> IO ()
164close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
166private
167saString : (Maybe SocketAddress) -> String
168saString (Just sa) = show sa
169saString Nothing = ""
171||| Binds a socket to the given socket address and port.
172||| Returns 0 on success, an error code otherwise.
173bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
174bind sock addr port = do
175 bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)
176 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
177 if bind_res == (-1) then -- error
178 getErrno
179 else return 0 -- Success
181||| Connects to a given address and port.
182||| Returns 0 on success, and an error number on error.
183connect : Socket -> SocketAddress -> Port -> IO Int
184connect sock addr port = do
185 conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
186 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)
187 if conn_res == (-1) then
188 getErrno
189 else return 0
191||| Listens on a bound socket.
192listen : Socket -> IO Int
193listen sock = do
194 listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
195 if listen_res == (-1) then
196 getErrno
197 else return 0
199||| Parses a textual representation of an IPv4 address into a SocketAddress
200parseIPv4 : String -> SocketAddress
201parseIPv4 str = case splitted of
202 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
203 _ => InvalidAddress
204 where toInt' : String -> Integer
205 toInt' = cast
206 toInt : String -> Int
207 toInt s = fromInteger $ toInt' s
208 splitted : List Int
209 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
212||| Retrieves a socket address from a sockaddr pointer
213getSockAddr : SockaddrPtr -> IO SocketAddress
214getSockAddr (SAPtr ptr) = do
215 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
216 -- putStrLn $ "Addr family int: " ++ (show addr_family_int)
217 -- ASSUMPTION: Foreign call returns a valid int
218 assert_total (case getSocketFamily addr_family_int of
219 Just AF_INET => do
220 ipv4_addr <- mkForeign (FFun "idrnet_sockaddr_ipv4" [FPtr] FString) ptr
221 return $ parseIPv4 ipv4_addr
222 Just AF_INET6 => return IPv6Addr
223 Just AF_UNSPEC => return InvalidAddress)
225accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
226accept sock = do
227 -- We need a pointer to a sockaddr structure. This is then passed into
228 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
229 sockaddr_ptr <- mkForeign (FFun "idrnet_create_sockaddr" [] FPtr)
230 accept_res <- mkForeign (FFun "idrnet_accept" [FInt, FPtr] FInt) (descriptor sock) sockaddr_ptr
231 if accept_res == (-1) then
232 map Left getErrno
233 else do
234 let (MkSocket _ fam ty p_num) = sock
235 sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
236 sockaddr_free (SAPtr sockaddr_ptr)
237 return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
239send : Socket -> String -> IO (Either SocketError ByteLength)
240send sock dat = do
241 send_res <- mkForeign (FFun "idrnet_send" [FInt, FString] FInt) (descriptor sock) dat
242 if send_res == (-1) then
243 map Left getErrno
244 else
245 return $ Right send_res
248freeRecvStruct : RecvStructPtr -> IO ()
249freeRecvStruct (RSPtr p) = mkForeign (FFun "idrnet_free_recv_struct" [FPtr] FUnit) p
251freeRecvfromStruct : RecvfromStructPtr -> IO ()
252freeRecvfromStruct (RFPtr p) = mkForeign (FFun "idrnet_free_recvfrom_struct" [FPtr] FUnit) p
254recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
255recv sock len = do
256 -- Firstly make the request, get some kind of recv structure which
257 -- contains the result of the recv and possibly the retrieved payload
258 recv_struct_ptr <- mkForeign (FFun "idrnet_recv" [FInt, FInt] FPtr) (descriptor sock) len
259 recv_res <- mkForeign (FFun "idrnet_get_recv_res" [FPtr] FInt) recv_struct_ptr
260 if recv_res == (-1) then do
261 errno <- getErrno
262 freeRecvStruct (RSPtr recv_struct_ptr)
263 return $ Left errno
264 else
265 if recv_res == 0 then do
266 freeRecvStruct (RSPtr recv_struct_ptr)
267 return $ Left 0
268 else do
269 payload <- mkForeign (FFun "idrnet_get_recv_payload" [FPtr] FString) recv_struct_ptr
270 freeRecvStruct (RSPtr recv_struct_ptr)
271 return $ Right (payload, recv_res)
274||| Sends the data in a given memory location
275sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
276sendBuf sock (BPtr ptr) len = do
277 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
278 if send_res == (-1) then
279 map Left getErrno
280 else
281 return $ Right send_res
283recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
284recvBuf sock (BPtr ptr) len = do
285 recv_res <- mkForeign (FFun "idrnet_recv_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
286 if (recv_res == (-1)) then
287 map Left getErrno
288 else
289 return $ Right recv_res
291sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)
292sendTo sock addr p dat = do
293 sendto_res <- mkForeign (FFun "idrnet_sendto" [FInt, FString, FString, FInt, FInt] FInt)
294 (descriptor sock) dat (show addr) p (toCode $ family sock)
295 if sendto_res == (-1) then
296 map Left getErrno
297 else
298 return $ Right sendto_res
301sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
302sendToBuf sock addr p (BPtr dat) len = do
303 sendto_res <- mkForeign (FFun "idrnet_sendto_buf" [FInt, FPtr, FInt, FString, FInt, FInt] FInt)
304 (descriptor sock) dat len (show addr) p (toCode $ family sock)
305 if sendto_res == (-1) then
306 map Left getErrno
307 else
308 return $ Right sendto_res
311foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
312foreignGetRecvfromPayload (RFPtr p) = mkForeign (FFun "idrnet_get_recvfrom_payload" [FPtr] FString) p
314foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
315foreignGetRecvfromAddr (RFPtr p) = do
316 sockaddr_ptr <- map SAPtr $ mkForeign (FFun "idrnet_get_recvfrom_sockaddr" [FPtr] FPtr) p
317 getSockAddr sockaddr_ptr
320foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
321foreignGetRecvfromPort (RFPtr p) = do
322 sockaddr_ptr <- mkForeign (FFun "idrnet_get_recvfrom_sockaddr" [FPtr] FPtr) p
323 port <- mkForeign (FFun "idrnet_sockaddr_ipv4_port" [FPtr] FInt) sockaddr_ptr
324 return port
326recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))
327recvFrom sock bl = do
328 recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
329 (descriptor sock) bl
330 let recv_ptr' = RFPtr recv_ptr
331 if !(nullPtr recv_ptr) then
332 map Left getErrno
333 else do
334 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
335 if result == -1 then do
336 freeRecvfromStruct recv_ptr'
337 map Left getErrno
338 else do
339 payload <- foreignGetRecvfromPayload recv_ptr'
340 port <- foreignGetRecvfromPort recv_ptr'
341 addr <- foreignGetRecvfromAddr recv_ptr'
342 freeRecvfromStruct recv_ptr'
343 return $ Right (MkUDPAddrInfo addr port, payload, result)
346recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))
347recvFromBuf sock (BPtr ptr) bl = do
348 recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
349 let recv_ptr' = RFPtr recv_ptr
350 if !(nullPtr recv_ptr) then
351 map Left getErrno
352 else do
353 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
354 if result == -1 then do
355 freeRecvfromStruct recv_ptr'
356 map Left getErrno
357 else do
358 port <- foreignGetRecvfromPort recv_ptr'
359 addr <- foreignGetRecvfromAddr recv_ptr'
360 freeRecvfromStruct recv_ptr'
361 return $ Right (MkUDPAddrInfo addr port, result + 1)