git.iko.soy/Idris-dev
on master help sign in
add Network/Socket/Data.idr
9b372d8PoroCYon
libs/contrib/Network/Socket/Data.idrnew file+172
compare with master
unifiedsplit
@@ -0,0 +1,172 @@
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.Data
7+
8+%access public export
9+
10+-- ------------------------------------------------------------ [ Type Aliases ]
11+
12+ByteLength : Type
13+ByteLength = Int
14+
15+ResultCode : Type
16+ResultCode = Int
17+
18+||| Protocol Number.
19+|||
20+||| Generally good enough to just set it to 0.
21+ProtocolNumber : Type
22+ProtocolNumber = Int
23+
24+||| SocketError: Error thrown by a socket operation
25+SocketError : Type
26+SocketError = Int
27+
28+||| SocketDescriptor: Native C Socket Descriptor
29+SocketDescriptor : Type
30+SocketDescriptor = Int
31+
32+Port : Type
33+Port = Int
34+
35+-- --------------------------------------------------------------- [ Constants ]
36+
37+||| Backlog used within listen() call -- number of incoming calls
38+BACKLOG : Int
39+BACKLOG = 20
40+
41+EAGAIN : Int
42+EAGAIN =
43+ -- I'm sorry
44+ -- maybe
45+ unsafePerformIO $ foreign FFI_C "idrnet_geteagain" (() -> IO Int) ()
46+
47+-- -------------------------------------------------------------- [ Interfaces ]
48+
49+interface ToCode a where
50+ toCode : a -> Int
51+
52+-- --------------------------------------------------------- [ Socket Families ]
53+
54+||| Socket Families
55+|||
56+||| The ones that people might actually use. We're not going to need US
57+||| Government proprietary ones.
58+data SocketFamily : Type where
59+ ||| Unspecified
60+ AF_UNSPEC : SocketFamily
61+
62+ ||| IP / UDP etc. IPv4
63+ AF_INET : SocketFamily
64+
65+ ||| IP / UDP etc. IPv6
66+ AF_INET6 : SocketFamily
67+
68+Show SocketFamily where
69+ show AF_UNSPEC = "AF_UNSPEC"
70+ show AF_INET = "AF_INET"
71+ show AF_INET6 = "AF_INET6"
72+
73+ToCode SocketFamily where
74+ toCode AF_UNSPEC = 0
75+ toCode AF_INET = 2
76+ toCode AF_INET6 = 10
77+
78+getSocketFamily : Int -> Maybe SocketFamily
79+getSocketFamily i =
80+ Prelude.List.lookup i [ (0, AF_UNSPEC)
81+ , (2, AF_INET)
82+ , (10, AF_INET6)
83+ ]
84+
85+-- ------------------------------------------------------------ [ Socket Types ]
86+
87+||| Socket Types.
88+data SocketType : Type where
89+ ||| Not a socket, used in certain operations
90+ NotASocket : SocketType
91+
92+ ||| TCP
93+ Stream : SocketType
94+
95+ ||| UDP
96+ Datagram : SocketType
97+
98+ ||| Raw sockets
99+ RawSocket : SocketType
100+
101+Show SocketType where
102+ show NotASocket = "Not a socket"
103+ show Stream = "Stream"
104+ show Datagram = "Datagram"
105+ show RawSocket = "Raw"
106+
107+ToCode SocketType where
108+ toCode NotASocket = 0
109+ toCode Stream = 1
110+ toCode Datagram = 2
111+ toCode RawSocket = 3
112+
113+-- --------------------------------------------------------------- [ Addresses ]
114+
115+||| Network Addresses
116+data SocketAddress : Type where
117+ IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
118+
119+ ||| Not implemented (yet)
120+ IPv6Addr : SocketAddress
121+
122+ Hostname : String -> SocketAddress
123+
124+ ||| Used when there's a parse error
125+ InvalidAddress : SocketAddress
126+
127+Show SocketAddress where
128+ show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
129+ show IPv6Addr = "NOT IMPLEMENTED YET"
130+ show (Hostname host) = host
131+ show InvalidAddress = "Invalid"
132+
133+||| Parses a textual representation of an IPv4 address into a SocketAddress
134+parseIPv4 : String -> SocketAddress
135+parseIPv4 str =
136+ case splitted of
137+ (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
138+ otherwise => InvalidAddress
139+ where
140+ toInt' : String -> Integer
141+ toInt' = cast
142+
143+ toInt : String -> Int
144+ toInt s = fromInteger $ toInt' s
145+
146+ splitted : List Int
147+ splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
148+
149+-- --------------------------------------------------------- [ UDP Information ]
150+
151+-- TODO: Expand to non-string payloads
152+record UDPRecvData where
153+ constructor MkUDPRecvData
154+ remote_addr : SocketAddress
155+ remote_port : Port
156+ recv_data : String
157+ data_len : Int
158+
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+record Socket where
167+ constructor MkSocket
168+ descriptor : SocketDescriptor
169+ family : SocketFamily
170+ socketType : SocketType
171+ protocolNumber : ProtocolNumber
172+