2383614 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

rearrange stuff

2383614PoroCYon10 years ago

libs/contrib/Network/Socket.idr+14−204

compare with master

unifiedsplit

@@ -4,7 +4,7 @@

4||| Modified (C) The Idris Community, 2015, 2016

5module Network.Socket

7−import public Network.Socket.Types

7+import public Network.Socket.Data

8import Network.Socket.Raw

10%include C "idris_net.h"

@@ -12,11 +12,12 @@ import Network.Socket.Raw

12%include C "sys/socket.h"

13%include C "netdb.h"

15+%access export

16+

15-- ----------------------------------------------------- [ Network Socket API. ]

17-- ----------------------------------------------------- [ Network Socket API. ]

17||| 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

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

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

19−export

20socket : (fam : SocketFamily)

21socket : (fam : SocketFamily)

21 -> (ty : SocketType)

22 -> (ty : SocketType)

22 -> (pnum : ProtocolNumber)

23 -> (pnum : ProtocolNumber)

@@ -31,34 +32,30 @@ socket sf st pn = do

31 else pure $ Right (MkSocket socket_res sf st pn)

32 else pure $ Right (MkSocket socket_res sf st pn)

33||| Close a socket

34||| Close a socket

34−export

35close : Socket -> IO ()

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

38−private

39−saString : (Maybe SocketAddress) -> String

40−saString (Just sa) = show sa

41−saString Nothing = ""

42−

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

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

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

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

45−export

46bind : (sock : Socket)

40bind : (sock : Socket)

47 -> (addr : Maybe SocketAddress)

41 -> (addr : Maybe SocketAddress)

48 -> (port : Port)

42 -> (port : Port)

49 -> IO Int

43 -> IO Int

50bind sock addr port = do

44bind sock addr port = do

51− bind_res <- foreign FFI_C "idrnet_bind"

45+ bind_res <- foreign FFI_C "idrnet_bind"

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

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

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

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

54− (toCode $ socketType sock) (saString addr) port

48+ (toCode $ socketType sock) (saString addr) port

55− if bind_res == (-1)

49+ if bind_res == (-1)

56− then getErrno

50+ then getErrno

57− else pure 0

51+ else pure 0

52+ where

53+ saString : Maybe SocketAddress -> String

54+ saString (Just sa) = show sa

55+ saString Nothing = ""

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

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

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

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

61−export

62connect : (sock : Socket)

59connect : (sock : Socket)

63 -> (addr : SocketAddress)

60 -> (addr : SocketAddress)

64 -> (port : Port)

61 -> (port : Port)

@@ -75,7 +72,6 @@ connect sock addr port = do

75||| Listens on a bound socket.

72||| Listens on a bound socket.

76|||

73|||

77||| @sock The socket to listen on.

74||| @sock The socket to listen on.

78−export

79listen : (sock : Socket) -> IO Int

75listen : (sock : Socket) -> IO Int

80listen sock = do

76listen sock = do

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

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

@@ -84,40 +80,6 @@ listen sock = do

84 then getErrno

80 then getErrno

85 else pure 0

81 else pure 0

87−||| Parses a textual representation of an IPv4 address into a SocketAddress

88−parseIPv4 : String -> SocketAddress

89−parseIPv4 str =

90− case splitted of

91− (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4

92− otherwise => InvalidAddress

93− where

94− toInt' : String -> Integer

95− toInt' = cast

96−

97− toInt : String -> Int

98− toInt s = fromInteger $ toInt' s

99−

100− splitted : List Int

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

102−

103−||| Retrieves a socket address from a sockaddr pointer

104−getSockAddr : SockaddrPtr -> IO SocketAddress

105−getSockAddr (SAPtr ptr) = do

106− addr_family_int <- foreign FFI_C "idrnet_sockaddr_family"

107− (Ptr -> IO Int)

108− ptr

109−

110− -- ASSUMPTION: Foreign call returns a valid int

111− assert_total (case getSocketFamily addr_family_int of

112− Just AF_INET => do

113− ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4"

114− (Ptr -> IO String)

115− ptr

116−

117− pure $ parseIPv4 ipv4_addr

118− Just AF_INET6 => pure IPv6Addr

119− Just AF_UNSPEC => pure InvalidAddress)

120−

121||| Accept a connection on the provided socket.

83||| Accept a connection on the provided socket.

122|||

84|||

123||| Returns on failure a `SocketError`

85||| Returns on failure a `SocketError`

@@ -126,7 +88,6 @@ getSockAddr (SAPtr ptr) = do

126||| + `SocketAddress` :: The

88||| + `SocketAddress` :: The

127|||

89|||

128||| @sock The socket used to establish connection.

90||| @sock The socket used to establish connection.

129−export

130accept : (sock : Socket)

91accept : (sock : Socket)

131 -> IO (Either SocketError (Socket, SocketAddress))

92 -> IO (Either SocketError (Socket, SocketAddress))

132accept sock = do

93accept sock = do

@@ -155,7 +116,6 @@ accept sock = do

155|||

116|||

156||| @sock The socket on which to send the message.

117||| @sock The socket on which to send the message.

157||| @msg The data to send.

118||| @msg The data to send.

158−export

159send : (sock : Socket)

119send : (sock : Socket)

160 -> (msg : String)

120 -> (msg : String)

161 -> IO (Either SocketError ResultCode)

121 -> IO (Either SocketError ResultCode)

@@ -168,20 +128,6 @@ send sock dat = do

168 then map Left getErrno

128 then map Left getErrno

169 else pure $ Right send_res

129 else pure $ Right send_res

170

130

171−freeRecvStruct : RecvStructPtr -> IO ()

172−freeRecvStruct (RSPtr p) =

173− foreign FFI_C "idrnet_free_recv_struct"

174− (Ptr -> IO ())

175− p

176−

177−||| Utility to extract data.

178−freeRecvfromStruct : RecvfromStructPtr -> IO ()

179−freeRecvfromStruct (RFPtr p) =

180− foreign FFI_C "idrnet_free_recvfrom_struct"

181− (Ptr -> IO ())

182− p

183−

184−

185||| Receive data on the specified socket.

131||| Receive data on the specified socket.

186|||

132|||

187||| Returns on failure a `SocketError`

133||| Returns on failure a `SocketError`

@@ -191,7 +137,6 @@ freeRecvfromStruct (RFPtr p) =

191|||

137|||

192||| @sock The socket on which to receive the message.

138||| @sock The socket on which to receive the message.

193||| @len How much of the data to send.

139||| @len How much of the data to send.

194−export

195recv : (sock : Socket)

140recv : (sock : Socket)

196 -> (len : ByteLength)

141 -> (len : ByteLength)

197 -> IO (Either SocketError (String, ResultCode))

142 -> IO (Either SocketError (String, ResultCode))

@@ -222,48 +167,6 @@ recv sock len = do

222 freeRecvStruct (RSPtr recv_struct_ptr)

167 freeRecvStruct (RSPtr recv_struct_ptr)

223 pure $ Right (payload, recv_res)

168 pure $ Right (payload, recv_res)

224

169

225−||| Sends the data in a given memory location

226−|||

227−||| Returns on failure a `SocketError`

228−||| Returns on success the `ResultCode`

229−|||

230−||| @sock The socket on which to send the message.

231−||| @ptr The location containing the data to send.

232−||| @len How much of the data to send.

233−sendBuf : (sock : Socket)

234− -> (ptr : BufPtr)

235− -> (len : ByteLength)

236− -> IO (Either SocketError ResultCode)

237−sendBuf sock (BPtr ptr) len = do

238− send_res <- foreign FFI_C "idrnet_send_buf"

239− (Int -> Ptr -> Int -> IO Int)

240− (descriptor sock) ptr len

241−

242− if send_res == (-1)

243− then map Left getErrno

244− else pure $ Right send_res

245−

246−||| Receive data from a given memory location.

247−|||

248−||| Returns on failure a `SocketError`

249−||| Returns on success the `ResultCode`

250−|||

251−||| @sock The socket on which to receive the message.

252−||| @ptr The location containing the data to receive.

253−||| @len How much of the data to receive.

254−recvBuf : (sock : Socket)

255− -> (ptr : BufPtr)

256− -> (len : ByteLength)

257− -> IO (Either SocketError ResultCode)

258−recvBuf sock (BPtr ptr) len = do

259− recv_res <- foreign FFI_C "idrnet_recv_buf"

260− (Int -> Ptr -> Int -> IO Int)

261− (descriptor sock) ptr len

262−

263− if (recv_res == (-1))

264− then map Left getErrno

265− else pure $ Right recv_res

266−

267||| Send a message.

170||| Send a message.

268|||

171|||

269||| Returns on failure a `SocketError`

172||| Returns on failure a `SocketError`

@@ -273,7 +176,6 @@ recvBuf sock (BPtr ptr) len = do

273||| @addr Address of the recipient.

176||| @addr Address of the recipient.

274||| @port The port on which to send the message.

177||| @port The port on which to send the message.

275||| @msg The message to send.

178||| @msg The message to send.

276−export

277sendTo : (sock : Socket)

179sendTo : (sock : Socket)

278 -> (addr : SocketAddress)

180 -> (addr : SocketAddress)

279 -> (port : Port)

181 -> (port : Port)

@@ -288,58 +190,6 @@ sendTo sock addr p dat = do

288 then map Left getErrno

190 then map Left getErrno

289 else pure $ Right sendto_res

191 else pure $ Right sendto_res

290

192

291−||| Send a message stored in some buffer.

292−|||

293−||| Returns on failure a `SocketError`

294−||| Returns on success the `ResultCode`

295−|||

296−||| @sock The socket on which to send the message.

297−||| @addr Address of the recipient.

298−||| @port The port on which to send the message.

299−||| @ptr A Pointer to the buffer containing the message.

300−||| @len The size of the message.

301−sendToBuf : (sock : Socket)

302− -> (addr : SocketAddress)

303− -> (port : Port)

304− -> (ptr : BufPtr)

305− -> (len : ByteLength)

306− -> IO (Either SocketError ResultCode)

307−sendToBuf sock addr p (BPtr dat) len = do

308− sendto_res <- foreign FFI_C "idrnet_sendto_buf"

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

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

311−

312− if sendto_res == (-1)

313− then map Left getErrno

314− else pure $ Right sendto_res

315−

316−||| Utility function to get the payload of the sent message as a `String`.

317−foreignGetRecvfromPayload : RecvfromStructPtr -> IO String

318−foreignGetRecvfromPayload (RFPtr p) =

319− foreign FFI_C "idrnet_get_recvfrom_payload"

320− (Ptr -> IO String)

321− p

322−

323−||| Utility function to return senders socket address.

324−foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress

325−foreignGetRecvfromAddr (RFPtr p) = do

326− sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr"

327− (Ptr -> IO Ptr)

328− p

329− getSockAddr sockaddr_ptr

330−

331−||| Utility function to return sender's IPV4 port.

332−foreignGetRecvfromPort : RecvfromStructPtr -> IO Port

333−foreignGetRecvfromPort (RFPtr p) = do

334− sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr"

335− (Ptr -> IO Ptr)

336− p

337− port <- foreign FFI_C "idrnet_sockaddr_ipv4_port"

338− (Ptr -> IO Int)

339− sockaddr_ptr

340− pure port

341−

342−

343||| Receive a message.

193||| Receive a message.

344|||

194|||

345||| Returns on failure a `SocketError`.

195||| Returns on failure a `SocketError`.

@@ -351,7 +201,6 @@ foreignGetRecvfromPort (RFPtr p) = do

351||| @sock The channel on which to receive.

201||| @sock The channel on which to receive.

352||| @len Size of the expected message.

202||| @len Size of the expected message.

353|||

203|||

354−export

355recvFrom : (sock : Socket)

204recvFrom : (sock : Socket)

356 -> (len : ByteLength)

205 -> (len : ByteLength)

357 -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))

206 -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))

@@ -379,42 +228,3 @@ recvFrom sock bl = do

379 freeRecvfromStruct recv_ptr'

228 freeRecvfromStruct recv_ptr'

380 pure $ Right (MkUDPAddrInfo addr port, payload, result)

229 pure $ Right (MkUDPAddrInfo addr port, payload, result)

381

230

382−||| Receive a message placed on a 'known' buffer.

383−|||

384−||| Returns on failure a `SocketError`.

385−||| Returns on success a pair of

386−||| + `UDPAddrInfo` :: The address of the sender.

387−||| + `Int` :: Result value from underlying function.

388−|||

389−||| @sock The channel on which to receive.

390−||| @ptr Pointer to the buffer to place the message.

391−||| @len Size of the expected message.

392−|||

393−recvFromBuf : (sock : Socket)

394− -> (ptr : BufPtr)

395− -> (len : ByteLength)

396− -> IO (Either SocketError (UDPAddrInfo, ResultCode))

397−recvFromBuf sock (BPtr ptr) bl = do

398− recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf"

399− (Int -> Ptr -> Int -> IO Ptr)

400− (descriptor sock) ptr bl

401−

402− let recv_ptr' = RFPtr recv_ptr

403−

404− if !(nullPtr recv_ptr)

405− then map Left getErrno

406− else do

407− result <- foreign FFI_C "idrnet_get_recvfrom_res"

408− (Ptr -> IO Int)

409− recv_ptr

410− if result == -1

411− then do

412− freeRecvfromStruct recv_ptr'

413− map Left getErrno

414− else do

415− port <- foreignGetRecvfromPort recv_ptr'

416− addr <- foreignGetRecvfromAddr recv_ptr'

417− freeRecvfromStruct recv_ptr'

418− pure $ Right (MkUDPAddrInfo addr port, result + 1)

419−

420−-- --------------------------------------------------------------------- [ EOF ]

libs/contrib/Network/Socket/Raw.idr+166−9

@@ -5,41 +5,198 @@

5||| Modified (C) The Idris Community, 2015, 2016

6module Network.Socket.Raw

8−import public Network.Socket.Types

8+import public Network.Socket.Data

10%include C "idris_net.h"

11%include C "sys/types.h"

12%include C "sys/socket.h"

13%include C "netdb.h"

15+%access public export

16+

15-- ---------------------------------------------------------------- [ Pointers ]

17-- ---------------------------------------------------------------- [ Pointers ]

17−public export

18−data RecvStructPtr = RSPtr Ptr

19+data RecvStructPtr = RSPtr Ptr

19−public export

20data RecvfromStructPtr = RFPtr Ptr

22−public export

23data BufPtr = BPtr Ptr

22data BufPtr = BPtr Ptr

25−public export

26data SockaddrPtr = SAPtr Ptr

24data SockaddrPtr = SAPtr Ptr

28-- ---------------------------------------------------------- [ Socket Utilies ]

26-- ---------------------------------------------------------- [ Socket Utilies ]

30||| Frees a given pointer

28||| Frees a given pointer

31−public export

32sock_free : BufPtr -> IO ()

29sock_free : BufPtr -> IO ()

33sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr

30sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr

35−public export

36sockaddr_free : SockaddrPtr -> IO ()

32sockaddr_free : SockaddrPtr -> IO ()

37sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr

33sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr

39||| Allocates an amount of memory given by the ByteLength parameter.

35||| Allocates an amount of memory given by the ByteLength parameter.

40|||

36|||

41||| Used to allocate a mutable pointer to be given to the Recv functions.

37||| Used to allocate a mutable pointer to be given to the Recv functions.

42−public export

43sock_alloc : ByteLength -> IO BufPtr

38sock_alloc : ByteLength -> IO BufPtr

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

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

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/Network/Socket/Types.idrdeleted−173

@@ -1,173 +0,0 @@

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.Types

7−

8−-- ------------------------------------------------------------ [ Type Aliases ]

9−

10−public export

11−ByteLength : Type

12−ByteLength = Int

13−

14−public export

15−ResultCode : Type

16−ResultCode = Int

17−

18−||| Protocol Number.

19−|||

20−||| Generally good enough to just set it to 0.

21−public export

22−ProtocolNumber : Type

23−ProtocolNumber = Int

24−

25−||| SocketError: Error thrown by a socket operation

26−public export

27−SocketError : Type

28−SocketError = Int

29−

30−||| SocketDescriptor: Native C Socket Descriptor

31−public export

32−SocketDescriptor : Type

33−SocketDescriptor = Int

34−

35−public export

36−Port : Type

37−Port = Int

38−

39−-- --------------------------------------------------------------- [ Constants ]

40−

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

42−public export

43−BACKLOG : Int

44−BACKLOG = 20

45−

46−-- FIXME: This *must* be pulled in from C

47−public export

48−EAGAIN : Int

49−EAGAIN = 11

50−

51−-- -------------------------------------------------------------- [ Interfaces ]

52−

53−public export

54−interface ToCode a where

55− toCode : a -> Int

56−

57−-- --------------------------------------------------------- [ Socket Families ]

58−

59−||| Socket Families

60−|||

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

62−||| Government proprietary ones.

63−public export

64−data SocketFamily : Type where

65− ||| Unspecified

66− AF_UNSPEC : SocketFamily

67−

68− ||| IP / UDP etc. IPv4

69− AF_INET : SocketFamily

70−

71− ||| IP / UDP etc. IPv6

72− AF_INET6 : SocketFamily

73−

74−public export

75−Show SocketFamily where

76− show AF_UNSPEC = "AF_UNSPEC"

77− show AF_INET = "AF_INET"

78− show AF_INET6 = "AF_INET6"

79−

80−public export

81−ToCode SocketFamily where

82− toCode AF_UNSPEC = 0

83− toCode AF_INET = 2

84− toCode AF_INET6 = 10

85−

86−public export

87−getSocketFamily : Int -> Maybe SocketFamily

88−getSocketFamily i =

89− Prelude.List.lookup i [ (0, AF_UNSPEC)

90− , (2, AF_INET)

91− , (10, AF_INET6)

92− ]

93−

94−-- ------------------------------------------------------------ [ Socket Types ]

95−

96−||| Socket Types.

97−public export

98−data SocketType : Type where

99− ||| Not a socket, used in certain operations

100− NotASocket : SocketType

101−

102− ||| TCP

103− Stream : SocketType

104−

105− ||| UDP

106− Datagram : SocketType

107−

108− ||| Raw sockets

109− RawSocket : SocketType

110−

111−public export

112−Show SocketType where

113− show NotASocket = "Not a socket"

114− show Stream = "Stream"

115− show Datagram = "Datagram"

116− show RawSocket = "Raw"

117−

118−public export

119−ToCode SocketType where

120− toCode NotASocket = 0

121− toCode Stream = 1

122− toCode Datagram = 2

123− toCode RawSocket = 3

124−

125−-- --------------------------------------------------------------- [ Addresses ]

126−

127−||| Network Addresses

128−public export

129−data SocketAddress : Type where

130− IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress

131−

132− ||| Not implemented (yet)

133− IPv6Addr : SocketAddress

134−

135− Hostname : String -> SocketAddress

136−

137− ||| Used when there's a parse error

138− InvalidAddress : SocketAddress

139−

140−public export

141−Show SocketAddress where

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

143− show IPv6Addr = "NOT IMPLEMENTED YET"

144− show (Hostname host) = host

145− show InvalidAddress = "Invalid"

146−

147−-- --------------------------------------------------------- [ UDP Information ]

148−

149−-- TODO: Expand to non-string payloads

150−public export

151−record UDPRecvData where

152− constructor MkUDPRecvData

153− remote_addr : SocketAddress

154− remote_port : Port

155− recv_data : String

156− data_len : Int

157−

158−public export

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−public export

167−record Socket where

168− constructor MkSocket

169− descriptor : SocketDescriptor

170− family : SocketFamily

171− socketType : SocketType

172− protocolNumber : ProtocolNumber

173−

libs/contrib/contrib.ipkg+1−1

@@ -23,7 +23,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,

24 Decidable.Decidable, Decidable.Order,

26− Network.Cgi, Network.Socket.Types, Network.Socket.Raw, Network.Socket,

26+ Network.Cgi, Network.Socket.Data, Network.Socket.Raw, Network.Socket,

28 System.Concurrency.Process,

rts/idris_net.c+5

@@ -315,3 +315,8 @@ void idrnet_free_recvfrom_struct(void* res_struct) {

315 }

316 }

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,

74 int port, int family, int socket_type);

76+int idrnet_geteagain();

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() {

194 return errno;

195}

196+

197+int idrnet_geteagain() {

198+ return EAGAIN;

199+}

200+