6536663 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3103 from ericqweinstein/fix/master/network-socket

6536663Ahmad Salim Al-Sibahi11 years ago

libs/contrib/Network/Socket.idr+41−23

compare with master

unifiedsplit

@@ -8,9 +8,11 @@ module Network.Socket

8%include C "sys/socket.h"

9%include C "netdb.h"

11+public export

11−public export ByteLength : Type

12+ByteLength : Type

12ByteLength = Int

13ByteLength = Int

15+export

14interface ToCode a where

16interface ToCode a where

15 toCode : a -> Int

17 toCode : a -> Int

@@ -18,6 +20,7 @@ interface ToCode a where

18|||

20|||

19||| The ones that people might actually use. We're not going to need US

21||| The ones that people might actually use. We're not going to need US

20||| Government proprietary ones.

22||| Government proprietary ones.

23+public export

21data SocketFamily =

24data SocketFamily =

22 ||| Unspecified

25 ||| Unspecified

23 AF_UNSPEC |

26 AF_UNSPEC |

@@ -26,11 +29,13 @@ data SocketFamily =

26 ||| IP / UDP etc. IPv6

29 ||| IP / UDP etc. IPv6

27 AF_INET6

30 AF_INET6

32+export

29implementation Show SocketFamily where

33implementation Show SocketFamily where

30 show AF_UNSPEC = "AF_UNSPEC"

34 show AF_UNSPEC = "AF_UNSPEC"

31 show AF_INET = "AF_INET"

35 show AF_INET = "AF_INET"

32 show AF_INET6 = "AF_INET6"

36 show AF_INET6 = "AF_INET6"

38+export

34implementation ToCode SocketFamily where

39implementation ToCode SocketFamily where

35 toCode AF_UNSPEC = 0

40 toCode AF_UNSPEC = 0

36 toCode AF_INET = 2

41 toCode AF_INET = 2

@@ -40,6 +45,7 @@ getSocketFamily : Int -> Maybe SocketFamily

40getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]

45getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]

42||| Socket Types.

47||| Socket Types.

48+public export

43data SocketType =

49data SocketType =

44 ||| Not a socket, used in certain operations

50 ||| Not a socket, used in certain operations

45 NotASocket |

51 NotASocket |

@@ -50,62 +56,74 @@ data SocketType =

50 ||| Raw sockets

56 ||| Raw sockets

51 RawSocket

57 RawSocket

59+export

53implementation Show SocketType where

60implementation Show SocketType where

54 show NotASocket = "Not a socket"

61 show NotASocket = "Not a socket"

55 show Stream = "Stream"

62 show Stream = "Stream"

56 show Datagram = "Datagram"

63 show Datagram = "Datagram"

57 show RawSocket = "Raw"

64 show RawSocket = "Raw"

66+export

59implementation ToCode SocketType where

67implementation ToCode SocketType where

60 toCode NotASocket = 0

68 toCode NotASocket = 0

61 toCode Stream = 1

69 toCode Stream = 1

62 toCode Datagram = 2

70 toCode Datagram = 2

63 toCode RawSocket = 3

71 toCode RawSocket = 3

65−

66data RecvStructPtr = RSPtr Ptr

73data RecvStructPtr = RSPtr Ptr

67data RecvfromStructPtr = RFPtr Ptr

74data RecvfromStructPtr = RFPtr Ptr

76+export

69−export data BufPtr = BPtr Ptr

77+data BufPtr = BPtr Ptr

78+export

70−export data SockaddrPtr = SAPtr Ptr

79+data SockaddrPtr = SAPtr Ptr

72||| Protocol Number.

81||| Protocol Number.

73|||

82|||

74||| Generally good enough to just set it to 0.

83||| Generally good enough to just set it to 0.

84+public export

75ProtocolNumber : Type

85ProtocolNumber : Type

76ProtocolNumber = Int

86ProtocolNumber = Int

78||| SocketError: Error thrown by a socket operation

88||| SocketError: Error thrown by a socket operation

89+public export

79SocketError : Type

90SocketError : Type

80SocketError = Int

91SocketError = Int

82||| SocketDescriptor: Native C Socket Descriptor

93||| SocketDescriptor: Native C Socket Descriptor

94+public export

83SocketDescriptor : Type

95SocketDescriptor : Type

84SocketDescriptor = Int

96SocketDescriptor = Int

98+public export

86data SocketAddress = IPv4Addr Int Int Int Int

99data SocketAddress = IPv4Addr Int Int Int Int

87 | IPv6Addr -- Not implemented (yet)

100 | IPv6Addr -- Not implemented (yet)

88 | Hostname String

101 | Hostname String

89 | InvalidAddress -- Used when there's a parse error

102 | InvalidAddress -- Used when there's a parse error

103

104+export

91implementation Show SocketAddress where

105implementation Show SocketAddress where

92 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])

106 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])

93 show IPv6Addr = "NOT IMPLEMENTED YET"

107 show IPv6Addr = "NOT IMPLEMENTED YET"

94 show (Hostname host) = host

108 show (Hostname host) = host

95 show InvalidAddress = "Invalid"

109 show InvalidAddress = "Invalid"

110

111+public export

97Port : Type

112Port : Type

98Port = Int

113Port = Int

114

100||| Backlog used within listen() call -- number of incoming calls

115||| Backlog used within listen() call -- number of incoming calls

116+public export

101BACKLOG : Int

117BACKLOG : Int

102BACKLOG = 20

118BACKLOG = 20

103

119

104-- FIXME: This *must* be pulled in from C

120-- FIXME: This *must* be pulled in from C

121+public export

105−EAGAIN : Int

122+EAGAIN : Int

106EAGAIN = 11

123EAGAIN = 11

107

124

108-- TODO: Expand to non-string payloads

125-- TODO: Expand to non-string payloads

126+export

109record UDPRecvData where

127record UDPRecvData where

110 constructor MkUDPRecvData

128 constructor MkUDPRecvData

111 remote_addr : SocketAddress

129 remote_addr : SocketAddress

@@ -113,6 +131,7 @@ record UDPRecvData where

113 recv_data : String

131 recv_data : String

114 data_len : Int

132 data_len : Int

115

133

134+export

116record UDPAddrInfo where

135record UDPAddrInfo where

117 constructor MkUDPAddrInfo

136 constructor MkUDPAddrInfo

118 remote_addr : SocketAddress

137 remote_addr : SocketAddress

@@ -135,6 +154,7 @@ sock_alloc : ByteLength -> IO BufPtr

135sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl

154sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl

136

155

137||| The metadata about a socket

156||| The metadata about a socket

157+export

138record Socket where

158record Socket where

139 constructor MkSocket

159 constructor MkSocket

140 descriptor : SocketDescriptor

160 descriptor : SocketDescriptor

@@ -144,6 +164,7 @@ record Socket where

144

164

145||| Creates a UNIX socket with the given family, socket type and protocol

165||| Creates a UNIX socket with the given family, socket type and protocol

146||| number. Returns either a socket or an error.

166||| number. Returns either a socket or an error.

167+export

147socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)

168socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)

148socket sf st pn = do

169socket sf st pn = do

149 socket_res <- foreign FFI_C "socket" (Int -> Int -> Int -> IO Int) (toCode sf) (toCode st) pn

170 socket_res <- foreign FFI_C "socket" (Int -> Int -> Int -> IO Int) (toCode sf) (toCode st) pn

@@ -153,6 +174,7 @@ socket sf st pn = do

153 return $ Right (MkSocket socket_res sf st pn)

174 return $ Right (MkSocket socket_res sf st pn)

154

175

155||| Close a socket

176||| Close a socket

177+export

156close : Socket -> IO ()

178close : Socket -> IO ()

157close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock)

179close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock)

158

180

@@ -163,11 +185,12 @@ saString Nothing = ""

163

185

164||| Binds a socket to the given socket address and port.

186||| Binds a socket to the given socket address and port.

165||| Returns 0 on success, an error code otherwise.

187||| Returns 0 on success, an error code otherwise.

188+export

166bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int

189bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int

167bind sock addr port = do

190bind sock addr port = do

168− bind_res <- foreign FFI_C "idrnet_bind"

191+ bind_res <- foreign FFI_C "idrnet_bind"

169 (Int -> Int -> Int -> String -> Int -> IO Int)

192 (Int -> Int -> Int -> String -> Int -> IO Int)

170− (descriptor sock) (toCode $ family sock)

193+ (descriptor sock) (toCode $ family sock)

171 (toCode $ socketType sock) (saString addr) port

194 (toCode $ socketType sock) (saString addr) port

172 if bind_res == (-1) then -- error

195 if bind_res == (-1) then -- error

173 getErrno

196 getErrno

@@ -175,6 +198,7 @@ bind sock addr port = do

175

198

176||| Connects to a given address and port.

199||| Connects to a given address and port.

177||| Returns 0 on success, and an error number on error.

200||| Returns 0 on success, and an error number on error.

201+export

178connect : Socket -> SocketAddress -> Port -> IO Int

202connect : Socket -> SocketAddress -> Port -> IO Int

179connect sock addr port = do

203connect sock addr port = do

180 conn_res <- foreign FFI_C "idrnet_connect"

204 conn_res <- foreign FFI_C "idrnet_connect"

@@ -185,6 +209,7 @@ connect sock addr port = do

185 else return 0

209 else return 0

186

210

187||| Listens on a bound socket.

211||| Listens on a bound socket.

212+export

188listen : Socket -> IO Int

213listen : Socket -> IO Int

189listen sock = do

214listen sock = do

190 listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)

215 listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)

@@ -205,7 +230,6 @@ parseIPv4 str = case splitted of

205 splitted : List Int

230 splitted : List Int

206 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)

231 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)

207

232

208−

209||| Retrieves a socket address from a sockaddr pointer

233||| Retrieves a socket address from a sockaddr pointer

210getSockAddr : SockaddrPtr -> IO SocketAddress

234getSockAddr : SockaddrPtr -> IO SocketAddress

211getSockAddr (SAPtr ptr) = do

235getSockAddr (SAPtr ptr) = do

@@ -219,6 +243,7 @@ getSockAddr (SAPtr ptr) = do

219 Just AF_INET6 => return IPv6Addr

243 Just AF_INET6 => return IPv6Addr

220 Just AF_UNSPEC => return InvalidAddress)

244 Just AF_UNSPEC => return InvalidAddress)

221

245

246+export

222accept : Socket -> IO (Either SocketError (Socket, SocketAddress))

247accept : Socket -> IO (Either SocketError (Socket, SocketAddress))

223accept sock = do

248accept sock = do

224 -- We need a pointer to a sockaddr structure. This is then passed into

249 -- We need a pointer to a sockaddr structure. This is then passed into

@@ -233,6 +258,7 @@ accept sock = do

233 sockaddr_free (SAPtr sockaddr_ptr)

258 sockaddr_free (SAPtr sockaddr_ptr)

234 return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)

259 return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)

235

260

261+export

236send : Socket -> String -> IO (Either SocketError ByteLength)

262send : Socket -> String -> IO (Either SocketError ByteLength)

237send sock dat = do

263send sock dat = do

238 send_res <- foreign FFI_C "idrnet_send" (Int -> String -> IO Int) (descriptor sock) dat

264 send_res <- foreign FFI_C "idrnet_send" (Int -> String -> IO Int) (descriptor sock) dat

@@ -241,7 +267,6 @@ send sock dat = do

241 else

267 else

242 return $ Right send_res

268 return $ Right send_res

243

269

244−

245freeRecvStruct : RecvStructPtr -> IO ()

270freeRecvStruct : RecvStructPtr -> IO ()

246freeRecvStruct (RSPtr p) = foreign FFI_C "idrnet_free_recv_struct" (Ptr -> IO ()) p

271freeRecvStruct (RSPtr p) = foreign FFI_C "idrnet_free_recv_struct" (Ptr -> IO ()) p

247

272

@@ -258,7 +283,7 @@ recv sock len = do

258 errno <- getErrno

283 errno <- getErrno

259 freeRecvStruct (RSPtr recv_struct_ptr)

284 freeRecvStruct (RSPtr recv_struct_ptr)

260 return $ Left errno

285 return $ Left errno

261− else

286+ else

262 if recv_res == 0 then do

287 if recv_res == 0 then do

263 freeRecvStruct (RSPtr recv_struct_ptr)

288 freeRecvStruct (RSPtr recv_struct_ptr)

264 return $ Left 0

289 return $ Left 0

@@ -267,7 +292,6 @@ recv sock len = do

267 freeRecvStruct (RSPtr recv_struct_ptr)

292 freeRecvStruct (RSPtr recv_struct_ptr)

268 return $ Right (payload, recv_res)

293 return $ Right (payload, recv_res)

269

294

270−

271||| Sends the data in a given memory location

295||| Sends the data in a given memory location

272sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

296sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

273sendBuf sock (BPtr ptr) len = do

297sendBuf sock (BPtr ptr) len = do

@@ -287,28 +311,26 @@ recvBuf sock (BPtr ptr) len = do

287

311

288sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)

312sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)

289sendTo sock addr p dat = do

313sendTo sock addr p dat = do

290− sendto_res <- foreign FFI_C "idrnet_sendto"

314+ sendto_res <- foreign FFI_C "idrnet_sendto"

291− (Int -> String -> String -> Int -> Int -> IO Int)

315+ (Int -> String -> String -> Int -> Int -> IO Int)

292 (descriptor sock) dat (show addr) p (toCode $ family sock)

316 (descriptor sock) dat (show addr) p (toCode $ family sock)

293 if sendto_res == (-1) then

317 if sendto_res == (-1) then

294 map Left getErrno

318 map Left getErrno

295 else

319 else

296 return $ Right sendto_res

320 return $ Right sendto_res

297

321

298−

299sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

322sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)

300sendToBuf sock addr p (BPtr dat) len = do

323sendToBuf sock addr p (BPtr dat) len = do

301− sendto_res <- foreign FFI_C "idrnet_sendto_buf"

324+ sendto_res <- foreign FFI_C "idrnet_sendto_buf"

302− (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)

325+ (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)

303 (descriptor sock) dat len (show addr) p (toCode $ family sock)

326 (descriptor sock) dat len (show addr) p (toCode $ family sock)

304 if sendto_res == (-1) then

327 if sendto_res == (-1) then

305 map Left getErrno

328 map Left getErrno

306 else

329 else

307 return $ Right sendto_res

330 return $ Right sendto_res

308

331

309−

310foreignGetRecvfromPayload : RecvfromStructPtr -> IO String

332foreignGetRecvfromPayload : RecvfromStructPtr -> IO String

311−foreignGetRecvfromPayload (RFPtr p)

333+foreignGetRecvfromPayload (RFPtr p)

312 = foreign FFI_C "idrnet_get_recvfrom_payload" (Ptr -> IO String) p

334 = foreign FFI_C "idrnet_get_recvfrom_payload" (Ptr -> IO String) p

313

335

314foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress

336foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress

@@ -316,7 +338,6 @@ foreignGetRecvfromAddr (RFPtr p) = do

316 sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p

338 sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p

317 getSockAddr sockaddr_ptr

339 getSockAddr sockaddr_ptr

318

340

319−

320foreignGetRecvfromPort : RecvfromStructPtr -> IO Port

341foreignGetRecvfromPort : RecvfromStructPtr -> IO Port

321foreignGetRecvfromPort (RFPtr p) = do

342foreignGetRecvfromPort (RFPtr p) = do

322 sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p

343 sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr" (Ptr -> IO Ptr) p

@@ -325,7 +346,7 @@ foreignGetRecvfromPort (RFPtr p) = do

325

346

326recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))

347recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))

327recvFrom sock bl = do

348recvFrom sock bl = do

328− recv_ptr <- foreign FFI_C "idrnet_recvfrom" (Int -> Int -> IO Ptr)

349+ recv_ptr <- foreign FFI_C "idrnet_recvfrom" (Int -> Int -> IO Ptr)

329 (descriptor sock) bl

350 (descriptor sock) bl

330 let recv_ptr' = RFPtr recv_ptr

351 let recv_ptr' = RFPtr recv_ptr

331 if !(nullPtr recv_ptr) then

352 if !(nullPtr recv_ptr) then

@@ -342,7 +363,6 @@ recvFrom sock bl = do

342 freeRecvfromStruct recv_ptr'

363 freeRecvfromStruct recv_ptr'

343 return $ Right (MkUDPAddrInfo addr port, payload, result)

364 return $ Right (MkUDPAddrInfo addr port, payload, result)

344

365

345−

346recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))

366recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))

347recvFromBuf sock (BPtr ptr) bl = do

367recvFromBuf sock (BPtr ptr) bl = do

348 recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf" (Int -> Ptr -> Int -> IO Ptr) (descriptor sock) ptr bl

368 recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf" (Int -> Ptr -> Int -> IO Ptr) (descriptor sock) ptr bl

@@ -359,5 +379,3 @@ recvFromBuf sock (BPtr ptr) bl = do

359 addr <- foreignGetRecvfromAddr recv_ptr'

379 addr <- foreignGetRecvfromAddr recv_ptr'

360 freeRecvfromStruct recv_ptr'

380 freeRecvfromStruct recv_ptr'

361 return $ Right (MkUDPAddrInfo addr port, result + 1)

381 return $ Right (MkUDPAddrInfo addr port, result + 1)

362−

363−