git.iko.soy/Idris-dev
on bfa343c help sign in
Idris-dev/libs/base/Network/Socket.idr
349 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-- The ones that people might actually use. We're not going to need US Government
21-- proprietary ones...
22data SocketFamily = AF_UNSPEC -- Unspecified
23 | AF_INET -- IP / UDP etc. IPv4
24 | AF_INET6 -- IP / UDP etc. IPv6
26instance Show SocketFamily where
27 show AF_UNSPEC = "AF_UNSPEC"
28 show AF_INET = "AF_INET"
29 show AF_INET6 = "AF_INET4"
31instance ToCode SocketFamily where
32 toCode AF_UNSPEC = 0
33 toCode AF_INET = 2
34 toCode AF_INET6 = 10
36getSocketFamily : Int -> Maybe SocketFamily
37getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
39-- Socket Types.
40data SocketType = NotASocket -- Not a socket, used in certain operations
41 | Stream -- TCP
42 | Datagram -- UDP
43 | RawSocket -- Raw sockets. A guy can dream.
45instance Show SocketType where
46 show NotASocket = "Not a socket"
47 show Stream = "Stream"
48 show Datagram = "Datagram"
49 show Raw = "Raw"
51instance ToCode SocketType where
52 toCode NotASocket = 0
53 toCode Stream = 1
54 toCode Datagram = 2
55 toCode Raw = 3
58data RecvStructPtr = RSPtr Ptr
59data RecvfromStructPtr = RFPtr Ptr
60data BufPtr = BPtr Ptr
61data SockaddrPtr = SAPtr Ptr
63-- Protocol Number. Generally good enough to just set it to 0.
64ProtocolNumber : Type
65ProtocolNumber = Int
67-- SocketError: Error thrown by a socket operation
68SocketError : Type
69SocketError = Int
71-- SocketDescriptor: Native C Socket Descriptor
72SocketDescriptor : Type
73SocketDescriptor = Int
75data SocketAddress = IPv4Addr Int Int Int Int
76 | IPv6Addr -- Not implemented (yet)
77 | Hostname String
78 | InvalidAddress -- Used when there's a parse error
80instance Show SocketAddress where
81 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
82 show IPv6Addr = "NOT IMPLEMENTED YET"
83 show (Hostname host) = host
84 show InvalidAddress = "Invalid"
86Port : Type
87Port = Int
89-- Backlog used within listen() call -- number of incoming calls
90BACKLOG : Int
91BACKLOG = 20
93-- FIXME: This *must* be pulled in from C
94EAGAIN : Int
95EAGAIN = 11
97-- TODO: Expand to non-string payloads
98record UDPRecvData : Type where
99 MkUDPRecvData :
100 (remote_addr : SocketAddress) ->
101 (remote_port : Port) ->
102 (recv_data : String) ->
103 (data_len : Int) ->
104 UDPRecvData
106record UDPAddrInfo : Type where
107 MkUDPAddrInfo :
108 (remote_addr : SocketAddress) ->
109 (remote_port : Port) ->
110 UDPAddrInfo
112-- Frees a given pointer
113public
114sock_free : BufPtr -> IO ()
115sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
117public
118sockaddr_free : SockaddrPtr -> IO ()
119sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
121-- Allocates an amount of memory given by the ByteLength parameter.
122-- Used to allocate a mutable pointer to be given to the Recv functions.
123public
124sock_alloc : ByteLength -> IO BufPtr
125sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
127record Socket : Type where
128 MkSocket : (descriptor : SocketDescriptor) ->
129 (family : SocketFamily) ->
130 (socketType : SocketType) ->
131 (protocolNumber : ProtocolNumber) ->
132 Socket
134getErrno : IO Int
135getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
137-- Creates a UNIX socket with the given family, socket type and protocol number.
138-- Returns either a socket or an error.
139socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
140socket sf st pn = do
141 socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
142 if socket_res == -1 then -- error
143 map Left getErrno
144 else
145 return $ Right (MkSocket socket_res sf st pn)
148close : Socket -> IO ()
149close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
151private
152saString : (Maybe SocketAddress) -> String
153saString (Just sa) = show sa
154saString Nothing = ""
156-- Binds a socket to the given socket address and port.
157-- Returns 0 on success, an error code otherwise.
158bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
159bind sock addr port = do
160 bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)
161 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
162 if bind_res == (-1) then -- error
163 getErrno
164 else return 0 -- Success
166-- Connects to a given address and port.
167-- Returns 0 on success, and an error number on error.
168connect : Socket -> SocketAddress -> Port -> IO Int
169connect sock addr port = do
170 conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
171 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)
172 if conn_res == (-1) then
173 getErrno
174 else return 0
176-- Listens on a bound socket.
177listen : Socket -> IO Int
178listen sock = do
179 listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
180 if listen_res == (-1) then
181 getErrno
182 else return 0
184-- Parses a textual representation of an IPv4 address into a SocketAddress
185parseIPv4 : String -> SocketAddress
186parseIPv4 str = case splitted of
187 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
188 _ => InvalidAddress
189 where toInt' : String -> Integer
190 toInt' = cast
191 toInt : String -> Int
192 toInt s = fromInteger $ toInt' s
193 splitted : List Int
194 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
197-- Retrieves a socket address from a sockaddr pointer
198getSockAddr : SockaddrPtr -> IO SocketAddress
199getSockAddr (SAPtr ptr) = do
200 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
201 -- putStrLn $ "Addr family int: " ++ (show addr_family_int)
202 -- ASSUMPTION: Foreign call returns a valid int
203 assert_total (case getSocketFamily addr_family_int of
204 Just AF_INET => do
205 ipv4_addr <- mkForeign (FFun "idrnet_sockaddr_ipv4" [FPtr] FString) ptr
206 return $ parseIPv4 ipv4_addr
207 Just AF_INET6 => return IPv6Addr
208 Just AF_UNSPEC => return InvalidAddress)
210accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
211accept sock = do
212 -- We need a pointer to a sockaddr structure. This is then passed into
213 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
214 sockaddr_ptr <- mkForeign (FFun "idrnet_create_sockaddr" [] FPtr)
215 accept_res <- mkForeign (FFun "idrnet_accept" [FInt, FPtr] FInt) (descriptor sock) sockaddr_ptr
216 if accept_res == (-1) then
217 map Left getErrno
218 else do
219 let (MkSocket _ fam ty p_num) = sock
220 sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
221 sockaddr_free (SAPtr sockaddr_ptr)
222 return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
224send : Socket -> String -> IO (Either SocketError ByteLength)
225send sock dat = do
226 send_res <- mkForeign (FFun "idrnet_send" [FInt, FString] FInt) (descriptor sock) dat
227 if send_res == (-1) then
228 map Left getErrno
229 else
230 return $ Right send_res
233freeRecvStruct : RecvStructPtr -> IO ()
234freeRecvStruct (RSPtr p) = mkForeign (FFun "idrnet_free_recv_struct" [FPtr] FUnit) p
236freeRecvfromStruct : RecvfromStructPtr -> IO ()
237freeRecvfromStruct (RFPtr p) = mkForeign (FFun "idrnet_free_recvfrom_struct" [FPtr] FUnit) p
239recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
240recv sock len = do
241 -- Firstly make the request, get some kind of recv structure which
242 -- contains the result of the recv and possibly the retrieved payload
243 recv_struct_ptr <- mkForeign (FFun "idrnet_recv" [FInt, FInt] FPtr) (descriptor sock) len
244 recv_res <- mkForeign (FFun "idrnet_get_recv_res" [FPtr] FInt) recv_struct_ptr
245 if recv_res == (-1) then do
246 errno <- getErrno
247 freeRecvStruct (RSPtr recv_struct_ptr)
248 return $ Left errno
249 else
250 if recv_res == 0 then do
251 freeRecvStruct (RSPtr recv_struct_ptr)
252 return $ Left 0
253 else do
254 payload <- mkForeign (FFun "idrnet_get_recv_payload" [FPtr] FString) recv_struct_ptr
255 freeRecvStruct (RSPtr recv_struct_ptr)
256 return $ Right (payload, recv_res)
259-- Sends the data in a given memory location
260sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
261sendBuf sock (BPtr ptr) len = do
262 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
263 if send_res == (-1) then
264 map Left getErrno
265 else
266 return $ Right send_res
268recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
269recvBuf sock (BPtr ptr) len = do
270 recv_res <- mkForeign (FFun "idrnet_recv_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
271 if (recv_res == (-1)) then
272 map Left getErrno
273 else
274 return $ Right recv_res
276sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)
277sendTo sock addr p dat = do
278 sendto_res <- mkForeign (FFun "idrnet_sendto" [FInt, FString, FString, FInt, FInt] FInt)
279 (descriptor sock) dat (show addr) p (toCode $ family sock)
280 if sendto_res == (-1) then
281 map Left getErrno
282 else
283 return $ Right sendto_res
286sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
287sendToBuf sock addr p (BPtr dat) len = do
288 sendto_res <- mkForeign (FFun "idrnet_sendto_buf" [FInt, FPtr, FInt, FString, FInt, FInt] FInt)
289 (descriptor sock) dat len (show addr) p (toCode $ family sock)
290 if sendto_res == (-1) then
291 map Left getErrno
292 else
293 return $ Right sendto_res
296foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
297foreignGetRecvfromPayload (RFPtr p) = mkForeign (FFun "idrnet_get_recvfrom_payload" [FPtr] FString) p
299foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
300foreignGetRecvfromAddr (RFPtr p) = do
301 sockaddr_ptr <- map SAPtr $ mkForeign (FFun "idrnet_get_recvfrom_sockaddr" [FPtr] FPtr) p
302 getSockAddr sockaddr_ptr
305foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
306foreignGetRecvfromPort (RFPtr p) = do
307 sockaddr_ptr <- mkForeign (FFun "idrnet_get_recvfrom_sockaddr" [FPtr] FPtr) p
308 port <- mkForeign (FFun "idrnet_sockaddr_ipv4_port" [FPtr] FInt) sockaddr_ptr
309 return port
311recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))
312recvFrom sock bl = do
313 recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
314 (descriptor sock) bl
315 let recv_ptr' = RFPtr recv_ptr
316 if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
317 map Left getErrno
318 else do
319 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
320 if result == -1 then do
321 freeRecvfromStruct recv_ptr'
322 map Left getErrno
323 else do
324 payload <- foreignGetRecvfromPayload recv_ptr'
325 port <- foreignGetRecvfromPort recv_ptr'
326 addr <- foreignGetRecvfromAddr recv_ptr'
327 freeRecvfromStruct recv_ptr'
328 return $ Right (MkUDPAddrInfo addr port, payload, result)
331recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))
332recvFromBuf sock (BPtr ptr) bl = do
333 recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
334 let recv_ptr' = RFPtr recv_ptr
335 if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
336 map Left getErrno
337 else do
338 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
339 if result == -1 then do
340 freeRecvfromStruct recv_ptr'
341 map Left getErrno
342 else do
343 port <- foreignGetRecvfromPort recv_ptr'
344 addr <- foreignGetRecvfromAddr recv_ptr'
345 freeRecvfromStruct recv_ptr'
346 return $ Right (MkUDPAddrInfo addr port, result + 1)