git.iko.soy/Idris-dev
on master help sign in
export socket internals in Network.Socket.Raw
b817debPoroCYon
libs/contrib/Network/Socket.idr+3−194
compare with master
unifiedsplit
@@ -4,205 +4,14 @@
4||| Modified (C) The Idris Community, 2015, 2016
4||| Modified (C) The Idris Community, 2015, 2016
5module Network.Socket
5module Network.Socket
6
6
7+import public Network.Socket.Types
8+import Network.Socket.Raw
9+
7%include C "idris_net.h"
10%include C "idris_net.h"
8%include C "sys/types.h"
11%include C "sys/types.h"
9%include C "sys/socket.h"
12%include C "sys/socket.h"
10%include C "netdb.h"
13%include C "netdb.h"
11
14
12−-- ------------------------------------------------------------ [ Type Aliases ]
13−
14−public export
15−ByteLength : Type
16−ByteLength = Int
17−
18−public export
19−ResultCode : Type
20−ResultCode = Int
21−
22−||| Protocol Number.
23−|||
24−||| Generally good enough to just set it to 0.
25−public export
26−ProtocolNumber : Type
27−ProtocolNumber = Int
28−
29−||| SocketError: Error thrown by a socket operation
30−public export
31−SocketError : Type
32−SocketError = Int
33−
34−||| SocketDescriptor: Native C Socket Descriptor
35−public export
36−SocketDescriptor : Type
37−SocketDescriptor = Int
38−
39−public export
40−Port : Type
41−Port = Int
42−
43−-- --------------------------------------------------------------- [ Constants ]
44−
45−||| Backlog used within listen() call -- number of incoming calls
46−public export
47−BACKLOG : Int
48−BACKLOG = 20
49−
50−-- FIXME: This *must* be pulled in from C
51−public export
52−EAGAIN : Int
53−EAGAIN = 11
54−
55−-- -------------------------------------------------------------- [ Interfaces ]
56−
57−export
58−interface ToCode a where
59− toCode : a -> Int
60−
61−-- --------------------------------------------------------- [ Socket Families ]
62−
63−||| Socket Families
64−|||
65−||| The ones that people might actually use. We're not going to need US
66−||| Government proprietary ones.
67−public export
68−data SocketFamily : Type where
69− ||| Unspecified
70− AF_UNSPEC : SocketFamily
71−
72− ||| IP / UDP etc. IPv4
73− AF_INET : SocketFamily
74−
75− ||| IP / UDP etc. IPv6
76− AF_INET6 : SocketFamily
77−
78−export
79−Show SocketFamily where
80− show AF_UNSPEC = "AF_UNSPEC"
81− show AF_INET = "AF_INET"
82− show AF_INET6 = "AF_INET6"
83−
84−export
85−ToCode SocketFamily where
86− toCode AF_UNSPEC = 0
87− toCode AF_INET = 2
88− toCode AF_INET6 = 10
89−
90−getSocketFamily : Int -> Maybe SocketFamily
91−getSocketFamily i =
92− Prelude.List.lookup i [ (0, AF_UNSPEC)
93− , (2, AF_INET)
94− , (10, AF_INET6)
95− ]
96−
97−-- ------------------------------------------------------------ [ Socket Types ]
98−||| Socket Types.
99−public export
100−data SocketType : Type where
101− ||| Not a socket, used in certain operations
102− NotASocket : SocketType
103−
104− ||| TCP
105− Stream : SocketType
106−
107− ||| UDP
108− Datagram : SocketType
109−
110− ||| Raw sockets
111− RawSocket : SocketType
112−
113−export
114−Show SocketType where
115− show NotASocket = "Not a socket"
116− show Stream = "Stream"
117− show Datagram = "Datagram"
118− show RawSocket = "Raw"
119−
120−export
121−ToCode SocketType where
122− toCode NotASocket = 0
123− toCode Stream = 1
124− toCode Datagram = 2
125− toCode RawSocket = 3
126−
127−-- ---------------------------------------------------------------- [ Pointers ]
128−
129−data RecvStructPtr = RSPtr Ptr
130−data RecvfromStructPtr = RFPtr Ptr
131−
132−export
133−data BufPtr = BPtr Ptr
134−
135−export
136−data SockaddrPtr = SAPtr Ptr
137−
138−-- --------------------------------------------------------------- [ Addresses ]
139−
140−||| Network Addresses
141−public export
142−data SocketAddress : Type where
143− IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
144−
145− ||| Not implemented (yet)
146− IPv6Addr : SocketAddress
147−
148− Hostname : String -> SocketAddress
149−
150− ||| Used when there's a parse error
151− InvalidAddress : SocketAddress
152−
153−export
154−Show SocketAddress where
155− show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
156− show IPv6Addr = "NOT IMPLEMENTED YET"
157− show (Hostname host) = host
158− show InvalidAddress = "Invalid"
159−
160−-- --------------------------------------------------------- [ UDP Information ]
161−
162−-- TODO: Expand to non-string payloads
163−export
164−record UDPRecvData where
165− constructor MkUDPRecvData
166− remote_addr : SocketAddress
167− remote_port : Port
168− recv_data : String
169− data_len : Int
170−
171−export
172−record UDPAddrInfo where
173− constructor MkUDPAddrInfo
174− remote_addr : SocketAddress
175− remote_port : Port
176−
177−-- ---------------------------------------------------------- [ Socket Utilies ]
178−
179−||| Frees a given pointer
180−export
181−sock_free : BufPtr -> IO ()
182−sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
183−
184−export
185−sockaddr_free : SockaddrPtr -> IO ()
186−sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
187−
188−||| Allocates an amount of memory given by the ByteLength parameter.
189−|||
190−||| Used to allocate a mutable pointer to be given to the Recv functions.
191−export
192−sock_alloc : ByteLength -> IO BufPtr
193−sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
194−
195−-- ----------------------------------------------------------------- [ Sockets ]
196−||| The metadata about a socket
197−export
198−record Socket where
199− constructor MkSocket
200− descriptor : SocketDescriptor
201− family : SocketFamily
202− socketType : SocketType
203− protocolNumber : ProtocolNumber
204−
205−
206-- ----------------------------------------------------- [ Network Socket API. ]
15-- ----------------------------------------------------- [ Network Socket API. ]
207
16
208||| Creates a UNIX socket with the given family, socket type and protocol
17||| Creates a UNIX socket with the given family, socket type and protocol
libs/contrib/Network/Socket/Raw.idrnew file+45
@@ -0,0 +1,45 @@
1+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
2+||| Type-unsafe parts. Use Network.Socket for a safe variant.
3+|||
4+||| Original (C) SimonJF, MIT Licensed, 2014
5+||| Modified (C) The Idris Community, 2015, 2016
6+module Network.Socket.Raw
7+
8+import public Network.Socket.Types
9+
10+%include C "idris_net.h"
11+%include C "sys/types.h"
12+%include C "sys/socket.h"
13+%include C "netdb.h"
14+
15+-- ---------------------------------------------------------------- [ Pointers ]
16+
17+public export
18+data RecvStructPtr = RSPtr Ptr
19+public export
20+data RecvfromStructPtr = RFPtr Ptr
21+
22+public export
23+data BufPtr = BPtr Ptr
24+
25+public export
26+data SockaddrPtr = SAPtr Ptr
27+
28+-- ---------------------------------------------------------- [ Socket Utilies ]
29+
30+||| Frees a given pointer
31+public export
32+sock_free : BufPtr -> IO ()
33+sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
34+
35+public export
36+sockaddr_free : SockaddrPtr -> IO ()
37+sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
38+
39+||| Allocates an amount of memory given by the ByteLength parameter.
40+|||
41+||| Used to allocate a mutable pointer to be given to the Recv functions.
42+public export
43+sock_alloc : ByteLength -> IO BufPtr
44+sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
45+
libs/contrib/Network/Socket/Types.idrnew file+173
@@ -0,0 +1,173 @@
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,
23
23
24 Decidable.Decidable, Decidable.Order,
24 Decidable.Decidable, Decidable.Order,
25
25
26− Network.Cgi, Network.Socket,
26+ Network.Cgi, Network.Socket.Types, Network.Socket.Raw, Network.Socket,
27
27
28 System.Concurrency.Process,
28 System.Concurrency.Process,
29
29