git.iko.soy/Idris-dev
on f52eafd help sign in
Idris-dev/libs/base/Network/Socket.idr
246 lines 8.3 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 Network.Socket
6%include C "idris_net.h"
7%include C "sys/types.h" -- Pushing my luck, might need to re-export everything
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
57-- Protocol Number. Generally good enough to just set it to 0.
58ProtocolNumber : Type
59ProtocolNumber = Int
61-- SocketError: Error thrown by a socket operation
62SocketError : Type
63SocketError = Int
65-- SocketDescriptor: Native C Socket Descriptor
66SocketDescriptor : Type
67SocketDescriptor = Int
69data SocketAddress = IPv4Addr Int Int Int Int
70 | IPv6Addr -- Not implemented (yet)
71 | Hostname String
72 | InvalidAddress -- Used when there's a parse error
74instance Show SocketAddress where
75 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
76 show IPv6Addr = "NOT IMPLEMENTED YET"
77 show (Hostname host) = host
78 show InvalidAddress = "Invalid"
80Port : Type
81Port = Int
83-- Backlog used within listen() call -- number of incoming calls
84BACKLOG : Int
85BACKLOG = 20
87-- FIXME: This *must* be pulled in from C
88EAGAIN : Int
89EAGAIN = 11
91-- Allocates an amount of memory given by the ByteLength parameter.
92-- Used to allocate a mutable pointer to be given to the Recv functions.
93private
94alloc : ByteLength -> IO Ptr
95alloc bl = mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
97-- Frees a given pointer
98private
99free : Ptr -> IO ()
100free ptr = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
102record Socket : Type where
103 MkSocket : (descriptor : SocketDescriptor) ->
104 (family : SocketFamily) ->
105 (socketType : SocketType) ->
106 (protocolNumber : ProtocolNumber) ->
107 Socket
109getErrno : IO Int
110getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
112-- Creates a UNIX socket with the given family, socket type and protocol number.
113-- Returns either a socket or an error.
114socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
115socket sf st pn = do
116 socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
117 if socket_res == -1 then -- error
118 map Left getErrno
119 else
120 return $ Right (MkSocket socket_res sf st pn)
123close : Socket -> IO ()
124close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
126-- Binds a socket to the given socket address and port.
127-- Returns 0 on success, an error code otherwise.
128bind : Socket -> SocketAddress -> Port -> IO Int
129bind sock addr port = do
130 bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)
131 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)
132 if bind_res == (-1) then -- error
133 getErrno
134 else return 0 -- Success
136-- Connects to a given address and port.
137-- Returns 0 on success, and an error number on error.
138connect : Socket -> SocketAddress -> Port -> IO Int
139connect sock addr port = do
140 conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
141 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)
142 if conn_res == (-1) then
143 getErrno
144 else return 0
146-- Listens on a bound socket.
147listen : Socket -> IO Int
148listen sock = do
149 listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
150 if listen_res == (-1) then
151 getErrno
152 else return 0
154-- Parses a textual representation of an IPv4 address into a SocketAddress
155private
156parseIPv4 : String -> SocketAddress
157parseIPv4 str = case splitted of
158 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
159 _ => InvalidAddress
160 where toInt' : String -> Integer
161 toInt' = cast
162 toInt : String -> Int
163 toInt s = fromInteger $ toInt' s
164 splitted : List Int
165 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
168-- Retrieves a socket address from a sockaddr pointer
169private
170getSockAddr : Ptr -> IO SocketAddress
171getSockAddr ptr = do
172 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
173 -- FIXME: Is this really a safe assertion? Depends where the Ptr came
174 -- from!
175 assert_total $ case getSocketFamily addr_family_int of
176 Just AF_INET => do
177 ipv4_addr <- mkForeign (FFun "idrnet_sockaddr_ipv4" [FPtr] FString) ptr
178 return $ parseIPv4 ipv4_addr
179 Just AF_INET6 => return IPv6Addr
180 Just AF_UNSPEC => return IPv6Addr -- FIXME: Horrible hack
182-- Accepts a connection from a listening socket.
183accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
184accept sock = do
185 -- We need a pointer to a sockaddr structure. This is then passed into
186 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
187 sockaddr_ptr <- mkForeign (FFun "idrnet_create_sockaddr" [] FPtr)
188 accept_res <- mkForeign (FFun "idrnet_accept" [FInt, FPtr] FInt) (descriptor sock) sockaddr_ptr
189 if accept_res == (-1) then
190 map Left getErrno
191 else do
192 let (MkSocket _ fam ty p_num) = sock
193 sockaddr <- getSockAddr sockaddr_ptr
194 free sockaddr_ptr
195 return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
197send : Socket -> String -> IO (Either SocketError ByteLength)
198send sock dat = do
199 send_res <- mkForeign (FFun "idrnet_send" [FInt, FString] FInt) (descriptor sock) dat
200 if send_res == (-1) then
201 map Left getErrno
202 else
203 return $ Right send_res
205private
206freeRecvStruct : Ptr -> IO ()
207freeRecvStruct p = mkForeign (FFun "idrnet_free_recv_struct" [FPtr] FUnit) p
210recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
211recv sock len = do
212 -- Firstly make the request, get some kind of recv structure which
213 -- contains the result of the recv and possibly the retrieved payload
214 recv_struct_ptr <- mkForeign (FFun "idrnet_recv" [FInt, FInt] FPtr) (descriptor sock) len
215 recv_res <- mkForeign (FFun "idrnet_get_recv_res" [FPtr] FInt) recv_struct_ptr
216 if recv_res == (-1) then do
217 errno <- getErrno
218 freeRecvStruct recv_struct_ptr
219 return $ Left errno
220 else
221 if recv_res == 0 then do
222 freeRecvStruct recv_struct_ptr
223 return $ Left 0
224 else do
225 payload <- mkForeign (FFun "idrnet_get_recv_payload" [FPtr] FString) recv_struct_ptr
226 freeRecvStruct recv_struct_ptr
227 return $ Right (payload, recv_res)
230-- Sends the data in a given memory location
231sendBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)
232sendBuf sock ptr len = do
233 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
234 if send_res == (-1) then
235 map Left getErrno
236 else
237 return $ Right send_res
239recvBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)
240recvBuf sock ptr len = do
241 recv_res <- mkForeign (FFun "idrnet_recv_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
242 if (recv_res == (-1)) then
243 map Left getErrno
244 else
245 return $ Right recv_res