git.iko.soy/Idris-dev
on master help sign in
Added Network.Sockets
5a1d646Edwin Brady
libs/base/Network/Socket.idrnew file+246
compare with master
unifiedsplit
@@ -0,0 +1,246 @@
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
4+module Network.Socket
5+
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"
10+
11+%access public
12+
13+ByteLength : Type
14+ByteLength = Int
15+
16+class ToCode a where
17+ toCode : a -> Int
18+
19+-- Socket Families.
20+-- The ones that people might actually use. We're not going to need US Government
21+-- proprietary ones...
22+data SocketFamily = AF_UNSPEC -- Unspecified
23+ | AF_INET -- IP / UDP etc. IPv4
24+ | AF_INET6 -- IP / UDP etc. IPv6
25+
26+instance Show SocketFamily where
27+ show AF_UNSPEC = "AF_UNSPEC"
28+ show AF_INET = "AF_INET"
29+ show AF_INET6 = "AF_INET4"
30+
31+instance ToCode SocketFamily where
32+ toCode AF_UNSPEC = 0
33+ toCode AF_INET = 2
34+ toCode AF_INET6 = 10
35+
36+getSocketFamily : Int -> Maybe SocketFamily
37+getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
38+
39+-- Socket Types.
40+data SocketType = NotASocket -- Not a socket, used in certain operations
41+ | Stream -- TCP
42+ | Datagram -- UDP
43+ | RawSocket -- Raw sockets. A guy can dream.
44+
45+instance Show SocketType where
46+ show NotASocket = "Not a socket"
47+ show Stream = "Stream"
48+ show Datagram = "Datagram"
49+ show Raw = "Raw"
50+
51+instance ToCode SocketType where
52+ toCode NotASocket = 0
53+ toCode Stream = 1
54+ toCode Datagram = 2
55+ toCode Raw = 3
56+
57+-- Protocol Number. Generally good enough to just set it to 0.
58+ProtocolNumber : Type
59+ProtocolNumber = Int
60+
61+-- SocketError: Error thrown by a socket operation
62+SocketError : Type
63+SocketError = Int
64+
65+-- SocketDescriptor: Native C Socket Descriptor
66+SocketDescriptor : Type
67+SocketDescriptor = Int
68+
69+data SocketAddress = IPv4Addr Int Int Int Int
70+ | IPv6Addr -- Not implemented (yet)
71+ | Hostname String
72+ | InvalidAddress -- Used when there's a parse error
73+
74+instance 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"
79+
80+Port : Type
81+Port = Int
82+
83+-- Backlog used within listen() call -- number of incoming calls
84+BACKLOG : Int
85+BACKLOG = 20
86+
87+-- FIXME: This *must* be pulled in from C
88+EAGAIN : Int
89+EAGAIN = 11
90+
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.
93+private
94+alloc : ByteLength -> IO Ptr
95+alloc bl = mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
96+
97+-- Frees a given pointer
98+private
99+free : Ptr -> IO ()
100+free ptr = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
101+
102+record Socket : Type where
103+ MkSocket : (descriptor : SocketDescriptor) ->
104+ (family : SocketFamily) ->
105+ (socketType : SocketType) ->
106+ (protocolNumber : ProtocolNumber) ->
107+ Socket
108+
109+getErrno : IO Int
110+getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
111+
112+-- Creates a UNIX socket with the given family, socket type and protocol number.
113+-- Returns either a socket or an error.
114+socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
115+socket 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)
121+
122+
123+close : Socket -> IO ()
124+close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
125+
126+-- Binds a socket to the given socket address and port.
127+-- Returns 0 on success, an error code otherwise.
128+bind : Socket -> SocketAddress -> Port -> IO Int
129+bind 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
135+
136+-- Connects to a given address and port.
137+-- Returns 0 on success, and an error number on error.
138+connect : Socket -> SocketAddress -> Port -> IO Int
139+connect 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
145+
146+-- Listens on a bound socket.
147+listen : Socket -> IO Int
148+listen 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
153+
154+-- Parses a textual representation of an IPv4 address into a SocketAddress
155+private
156+parseIPv4 : String -> SocketAddress
157+parseIPv4 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)
166+
167+
168+-- Retrieves a socket address from a sockaddr pointer
169+private
170+getSockAddr : Ptr -> IO SocketAddress
171+getSockAddr 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
181+
182+-- Accepts a connection from a listening socket.
183+accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
184+accept 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)
196+
197+send : Socket -> String -> IO (Either SocketError ByteLength)
198+send 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
204+
205+private
206+freeRecvStruct : Ptr -> IO ()
207+freeRecvStruct p = mkForeign (FFun "idrnet_free_recv_struct" [FPtr] FUnit) p
208+
209+
210+recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
211+recv 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)
228+
229+
230+-- Sends the data in a given memory location
231+sendBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)
232+sendBuf 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
238+
239+recvBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)
240+recvBuf 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
246+
libs/base/base.ipkg+1−1
@@ -3,7 +3,7 @@ package base
3opts = "--nobasepkgs --total -i ../prelude"
3opts = "--nobasepkgs --total -i ../prelude"
4modules = System,
4modules = System,
5
5
6− Network.Cgi,
6+ Network.Cgi, Network.Socket,
7 Debug.Trace,
7 Debug.Trace,
8
8
9 System.Concurrency.Raw, System.Concurrency.Process,
9 System.Concurrency.Raw, System.Concurrency.Process,
libs/neweffects/Effects.idr+1−1
@@ -22,10 +22,10 @@ class Handler (e : Effect) (m : Type -> Type) where
22-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
22-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
23-- up to a small number of parameters...)
23-- up to a small number of parameters...)
24
24
25+syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
25syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
26syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
26 = eff inst (\b => outst)
27 = eff inst (\b => outst)
27syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
28syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
28−syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
29
29
30---- Properties and proof construction
30---- Properties and proof construction
31
31
rts/Makefile+2−2
@@ -1,9 +1,9 @@
1include ../config.mk
1include ../config.mk
2
2
3OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_stdfgn.o \
3OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_stdfgn.o \
4− idris_bitstring.o idris_opts.o idris_stats.o mini-gmp.o
4+ idris_bitstring.o idris_net.o idris_opts.o idris_stats.o mini-gmp.o
5HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h \
5HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h \
6− idris_bitstring.h idris_opts.h idris_stats.h mini-gmp.h
6+ idris_bitstring.h idris_net.h idris_opts.h idris_stats.h mini-gmp.h
7CFLAGS:=-fPIC $(CFLAGS)
7CFLAGS:=-fPIC $(CFLAGS)
8CFLAGS += $(GMP_INCLUDE_DIR) $(GMP)
8CFLAGS += $(GMP_INCLUDE_DIR) $(GMP)
9
9
rts/idris_net.cnew file+143
@@ -0,0 +1,143 @@
1+// C-Side of the Idris network library
2+// (C) Simon Fowler, 2014
3+// MIT Licensed. Have fun!
4+#include "idris_net.h"
5+#include <arpa/inet.h>
6+
7+void* idrnet_malloc(int size) {
8+ return malloc(size);
9+}
10+
11+void idrnet_free(void* ptr) {
12+ free(ptr);
13+}
14+
15+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {
16+ struct addrinfo hints;
17+ struct addrinfo* address_res;
18+ // Convert port into string
19+ char str_port[8];
20+ sprintf(str_port, "%d", port);
21+
22+ // Set up hints structure
23+ memset(&hints, 0, sizeof(hints)); // zero out hints
24+ hints.ai_family = family;
25+ hints.ai_socktype = socket_type;
26+
27+ // If the length of the hostname is 0 (i.e, it was set to Nothing in Idris)
28+ // then we want to instruct the C library to fill in the IP automatically
29+ if (strlen(host) == 0) {
30+ hints.ai_flags = AI_PASSIVE; // fill in IP automatically
31+ }
32+
33+ int addr_res = getaddrinfo(host, str_port, &hints, &address_res);
34+ if (addr_res == -1) {
35+ return -1;
36+ }
37+
38+ int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen);
39+ if (bind_res == -1) {
40+ return -1;
41+ }
42+
43+ return 0;
44+}
45+
46+int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port) {
47+ char str_port[8];
48+ sprintf(str_port, "%d", port);
49+ struct addrinfo hints;
50+ struct addrinfo* remote_host;
51+
52+ // Set up hints structure for getaddrinfo
53+ memset(&hints, 0, sizeof(hints));
54+ hints.ai_family = family;
55+ hints.ai_socktype = socket_type;
56+
57+ // Get info about the remote host (DNS lookup etc)
58+ int addr_res = getaddrinfo(host, str_port, &hints, &remote_host);
59+ if (addr_res == -1) {
60+ return -1;
61+ }
62+
63+ int connect_res = connect(sockfd, remote_host->ai_addr, remote_host->ai_addrlen);
64+ if (connect_res == -1) {
65+ return -1;
66+ }
67+
68+ return 0;
69+}
70+
71+
72+int idrnet_sockaddr_family(void* sockaddr) {
73+ struct sockaddr* addr = (struct sockaddr*) sockaddr;
74+ return (int) addr->sa_family;
75+}
76+
77+char* idrnet_sockaddr_ipv4(void* sockaddr) {
78+ struct sockaddr_in* addr = (struct sockaddr_in*) addr;
79+ char* ip_addr = (char*) malloc(sizeof(char) * INET_ADDRSTRLEN);
80+ inet_ntop(AF_INET, &(addr->sin_addr), ip_addr, INET_ADDRSTRLEN);
81+ return ip_addr;
82+}
83+
84+void* idrnet_create_sockaddr() {
85+ return malloc(sizeof(struct sockaddr_storage));
86+}
87+
88+
89+int idrnet_accept(int sockfd, void* sockaddr) {
90+ struct sockaddr* addr = (struct sockaddr*) sockaddr;
91+ socklen_t addr_size = 0;
92+ return accept(sockfd, addr, &addr_size);
93+}
94+
95+int idrnet_send(int sockfd, char* data) {
96+ int len = strlen(data); // For now.
97+ return send(sockfd, (void*) data, len, 0);
98+}
99+
100+int idrnet_send_buf(int sockfd, void* data, int len) {
101+ return send(sockfd, data, len, 0);
102+}
103+
104+void* idrnet_recv(int sockfd, int len) {
105+ idrnet_recv_result* res_struct =
106+ (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));
107+
108+ char* buf = malloc(len + 1);
109+ int recv_res = recv(sockfd, buf, len, 0);
110+ res_struct->result = recv_res;
111+
112+ if (recv_res > 0) { // Data was received
113+ buf[recv_res + 1] = 0x00; // Null-term, so Idris can interpret it
114+ }
115+ res_struct->payload = (void*) buf;
116+ return (void*) res_struct;
117+}
118+
119+int idrnet_recv_buf(int sockfd, void* buf, int len) {
120+ return recv(sockfd, buf, len, 0);
121+}
122+
123+int idrnet_get_recv_res(void* res_struct) {
124+ return (((idrnet_recv_result*) res_struct)->result);
125+}
126+
127+void* idrnet_get_recv_payload(void* res_struct) {
128+ return (((idrnet_recv_result*) res_struct)->payload);
129+}
130+
131+void idrnet_free_recv_struct(void* res_struct) {
132+ idrnet_recv_result* i_res_struct =
133+ (idrnet_recv_result*) res_struct;
134+ if (i_res_struct->payload != NULL) {
135+ free(i_res_struct->payload);
136+ }
137+ free(res_struct);
138+}
139+
140+int idrnet_errno() {
141+ return errno;
142+}
143+
rts/idris_net.hnew file+53
@@ -0,0 +1,53 @@
1+#ifndef IDRISNET_H
2+#define IDRISNET_H
3+
4+#include <errno.h>
5+#include <netdb.h>
6+#include <stdbool.h>
7+#include <stdlib.h>
8+#include <stdio.h>
9+#include <string.h>
10+#include <sys/types.h>
11+#include <sys/socket.h>
12+
13+typedef struct idrnet_recv_result {
14+ int result;
15+ void* payload;
16+} idrnet_recv_result;
17+
18+// Memory management functions
19+void* idrnet_malloc(int size);
20+void idrnet_free(void* ptr);
21+
22+// Gets value of errno
23+int idrnet_errno();
24+
25+// Bind
26+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port);
27+
28+// Connect
29+int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port);
30+
31+// Accessor functions for struct_sockaddr
32+int idrnet_sockaddr_family(void* sockaddr);
33+char* idrnet_sockaddr_ipv4(void* sockaddr);
34+void* idrnet_create_sockaddr();
35+
36+// Accept
37+int idrnet_accept(int sockfd, void* sockaddr);
38+
39+// Send
40+int idrnet_send(int sockfd, char* data);
41+int idrnet_send_buf(int sockfd, void* data, int len);
42+
43+// Receive
44+// Creates a result structure containing result and payload
45+void* idrnet_recv(int sockfd, int len);
46+// Receives directly into a buffer
47+int idrnet_recv_buf(int sockfd, void* buf, int len);
48+
49+// Receive structure accessors
50+int idrnet_get_recv_res(void* res_struct);
51+void* idrnet_get_recv_payload(void* res_struct);
52+void idrnet_free_recv_struct(void* res_struct);
53+#endif
src/Idris/ParseExpr.hs+8−2
@@ -70,8 +70,14 @@ Expr' ::= "External (User-defined) Syntax"
70 | InternalExpr;
70 | InternalExpr;
71@
71@
72 -}
72 -}
73+expr' syn = doexpr' syn
74+-- = do l <- restOfLine
75+-- f <- getFC
76+-- e <- trace (show (f, l)) $ doexpr' syn
77+-- return e
78+
73−expr' :: SyntaxInfo -> IdrisParser PTerm
79+doexpr' :: SyntaxInfo -> IdrisParser PTerm
74−expr' syn = try (externalExpr syn)
80+doexpr' syn = try (externalExpr syn)
75 <|> internalExpr syn
81 <|> internalExpr syn
76 <?> "expression"
82 <?> "expression"
77
83