Move network support to libidris2_support

This makes the support stuff much simpler, and also makes the racket
bootstrap process easier
This commit is contained in:
Edwin Brady 2020-05-23 15:52:33 +01:00
parent 561123d49d
commit e17f66244a
13 changed files with 51 additions and 215 deletions

View File

@ -35,11 +35,11 @@ endif
ifeq ($(OS), windows)
IDRIS2_PREFIX := $(shell cygpath -m ${PREFIX})
IDRIS2_CURDIR := $(shell cygpath -m ${CURDIR})
export IDRIS2_BOOT_PATH = "${IDRIS2_CURDIR}/libs/prelude/build/ttc;${IDRIS2_CURDIR}/libs/base/build/ttc;${IDRIS2_CURDIR}/libs/network/build/ttc"
export IDRIS2_BOOT_PATH = "${IDRIS2_CURDIR}/libs/prelude/build/ttc;${IDRIS2_CURDIR}/libs/base/build/ttc"
else
IDRIS2_PREFIX := ${PREFIX}
IDRIS2_CURDIR := ${CURDIR}
export IDRIS2_BOOT_PATH = ${IDRIS2_CURDIR}/libs/prelude/build/ttc:${IDRIS2_CURDIR}/libs/base/build/ttc:${IDRIS2_CURDIR}/libs/network/build/ttc
export IDRIS2_BOOT_PATH = ${IDRIS2_CURDIR}/libs/prelude/build/ttc:${IDRIS2_CURDIR}/libs/base/build/ttc
endif
@ -127,7 +127,7 @@ install-support: support
install-libs: libs
${MAKE} -C libs/prelude install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/base install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_VERSION=${IDRIS2_VERSION}
${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
@ -145,11 +145,11 @@ endif
bootstrap-racket: support
cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
cp bootstrap/idris2.rkt bootstrap/idris2boot.rkt
cp bootstrap/idris2_app/idris2.rkt bootstrap/idris2_app/idris2-boot.rkt
ifeq ($(OS), darwin)
sed -i '' 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2boot.rkt
sed -i '' 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt
else
sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2boot.rkt
sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt
endif
sh ./bootstrap-rkt.sh

View File

@ -4,11 +4,13 @@
cd bootstrap
echo "Building idris2boot from idris2boot.rkt"
raco exe idris2boot.rkt
raco exe idris2_app/idris2-boot.rkt
# Put the result in the usual place where the target goes
mkdir -p ../build/exec
install idris2boot ../build/exec/idris2
mkdir -p ../build/exec/idris2_app
install idris2-rktboot ../build/exec/idris2
install idris2_app/* ../build/exec/idris2_app
cd ..

View File

@ -27,13 +27,13 @@ if [ ${OS} = "windows" ]; then
IDRIS2_BOOT_PATH="${IDRIS_PREFIX}/idris2-0.2.0/prelude;${IDRIS_PREFIX}/idris2-0.2.0/base;${IDRIS_PREFIX}/idris2-0.2.0/contrib;${IDRIS_PREFIX}/idris2-0.2.0/network"
NEW_PREFIX=$(cygpath -m $(dirname "$DIR"))
IDRIS2_NEW_PATH="${NEW_PREFIX}/libs/prelude/build/ttc;${NEW_PREFIX}/libs/base/build/ttc;${NEW_PREFIX}/libs/network/build/ttc"
IDRIS2_TEST_LIBS="${IDRIS_PREFIX}/idris2-0.2.0/lib;${IDRIS_PREFIX}/idris2-0.2.0/network/lib"
IDRIS2_TEST_LIBS="${IDRIS_PREFIX}/idris2-0.2.0/lib"
IDRIS2_TEST_DATA=${IDRIS_PREFIX}/idris2-0.2.0/support
else
IDRIS2_BOOT_PATH="${PREFIX}/idris2-0.2.0/prelude:${PREFIX}/idris2-0.2.0/base:${PREFIX}/idris2-0.2.0/contrib:${PREFIX}/idris2-0.2.0/network"
NEWPREFIX="`dirname $DIR`"
IDRIS2_NEW_PATH="${NEWPREFIX}/libs/prelude/build/ttc:${NEWPREFIX}/libs/base/build/ttc:${NEWPREFIX}/libs/network/build/ttc"
IDRIS2_TEST_LIBS="${PREFIX}/idris2-0.2.0/lib:${PREFIX}/idris2-0.2.0/network/lib" IDRIS2_TEST_DATA=${PREFIX}/idris2-0.2.0/support
IDRIS2_TEST_LIBS="${PREFIX}/idris2-0.2.0/lib" IDRIS2_TEST_DATA=${PREFIX}/idris2-0.2.0/support
fi
# Now rebuild everything properly

View File

@ -7124,5 +7124,5 @@
(define Parser-IDEMode-Idris-ideTokens (lambda () (List-Prelude-C-43C-43 'erased (Prelude-map_Functor__List 'erased 'erased (lambda (x) (vector 0 (Lexer-Text-exact x) (lambda (eta-0) (vector 6 eta-0)))) (Parser-IDEMode-Idris-symbols)) (vector 1 (vector 0 (Lexer-Text-digits) (lambda (x) (vector 2 (Prelude-cast_Cast__String_Integer x)))) (vector 1 (vector 0 (Lexer-Text-stringLit) (lambda (x) (vector 3 (String-Utils-stripQuotes x)))) (vector 1 (vector 0 (Source-Lexer-Parser-identAllowDashes) (lambda (x) (vector 0 (vector 1 x (vector 0 ))))) (vector 1 (vector 0 (Lexer-Text-space) (lambda (eta-0) (vector 9 eta-0))) (vector 0 ))))))))
(define Parser-IDEMode-Idris-ideParser (lambda (arg-0 arg-1 arg-2 arg-3) (Prelude-C-62C-62C-61_Monad__C-40EitherC-32C-36eC-41 'erased 'erased 'erased (Either-Utils-mapError 'erased 'erased 'erased (lambda (eta-0) (vector 1 eta-0)) (Parser-IDEMode-Idris-idelex arg-2)) (lambda (toks) (Prelude-C-62C-62C-61_Monad__C-40EitherC-32C-36eC-41 'erased 'erased 'erased (Either-Utils-mapError 'erased 'erased 'erased (lambda (eta-0) (Support-Parser-mapParseError eta-0)) (Core-Parser-Text-parse 'erased 'erased arg-1 arg-3 toks)) (lambda (parsed) (vector 1 (Builtin-fst 'erased 'erased parsed))))))))
(load-shared-object "libidris2_support.so")
(load-shared-object "idris_net.so")
(load-shared-object "libidris2_support.so")
(PrimIO-unsafePerformIO 'erased (lambda (eta-0) (Main-main eta-0))))

View File

@ -1,56 +0,0 @@
module Main
import System
import Network.Socket
import Network.Socket.Data
import Network.Socket.Raw
runServer : IO (Either String (Port, ThreadID))
runServer = do
Right sock <- socket AF_INET Stream 0
| Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
res <- bind sock (Just (Hostname "localhost")) 0
if res /= 0
then pure (Left $ "Failed to bind socket with error: " ++ show res)
else do
port <- getSockPort sock
res <- listen sock
if res /= 0
then pure (Left $ "Failed to listen on socket with error: " ++ show res)
else do
forked <- fork (serve port sock)
pure $ Right (port, forked)
where
serve : Port -> Socket -> IO ()
serve port sock = do
Right (s, _) <- accept sock
| Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
Right (str, _) <- recv s 1024
| Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
putStrLn ("Received: " ++ str)
Right n <- send s ("echo: " ++ str)
| Left err => putStrLn ("Server failed to send data with error: " ++ show err)
pure ()
runClient : Port -> IO ()
runClient serverPort = do
Right sock <- socket AF_INET Stream 0
| Left fail => putStrLn ("Failed to open socket: " ++ show fail)
res <- connect sock (Hostname "localhost") serverPort
if res /= 0
then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res)
else do
Right n <- send sock ("hello world!")
| Left err => putStrLn ("Client failed to send data with error: " ++ show err)
Right (str, _) <- recv sock 1024
| Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err)
-- assuming that stdout buffers get flushed in between system calls, this is "guaranteed"
-- to be printed after the server prints its own message
putStrLn ("Received: " ++ str)
main : IO ()
main = do
Right (serverPort, tid) <- runServer
| Left err => putStrLn $ "[server] " ++ err
runClient serverPort

View File

@ -1,58 +1,8 @@
include ../../config.mk
INSTALLDIR = ${PREFIX}/idris2-${IDRIS2_VERSION}/network/lib
IDRIS_SRCS = Network/Socket.idr Network/Socket/Data.idr Network/Socket/Raw.idr
TARGET = idris_net
SRCS = idris_net.c
OBJS = $(SRCS:.c=.o)
DEPS = $(OBJS:.o=.d)
ifeq ($(OS), windows)
LDFLAGS += -lws2_32
endif
all: $(TARGET)$(SHLIB_SUFFIX)
all:
${IDRIS2} --build network.ipkg
build: $(TARGET)$(SHLIB_SUFFIX) $(IDRIS_SRCS)
@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
${IDRIS2} --build network.ipkg
$(TARGET)$(SHLIB_SUFFIX): $(OBJS)
$(CC) -shared -o $@ $^ $(LDFLAGS)
-include $(DEPS)
%.d: %.c
@$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@
.PHONY: clean
clean :
$(RM) $(OBJS) $(TARGET)$(SHLIB_SUFFIX)
$(RM) -r build
cleandep: clean
$(RM) $(DEPS)
.PHONY: install
install:
@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
${IDRIS2} --install network.ipkg
@if ! [ -d $(INSTALLDIR) ]; then mkdir -p $(INSTALLDIR); fi
install $(TARGET)$(SHLIB_SUFFIX) $(wildcard *.h) $(INSTALLDIR)
test: build test.c
$(CC) -o network-tests -L. -I. test.c $(TARGET)$(SHLIB_SUFFIX)
LD_LIBRARY_PATH=. ./network-tests
@$(RM) ./network-tests test.o
clean:
$(RM) -r build

View File

@ -7,143 +7,143 @@ import Network.Socket.Data
-- From sys/socket.h
%foreign "C:close,idris_net"
%foreign "C:close,libidris2_support"
export
socket_close : (sockdes : SocketDescriptor) -> PrimIO Int
%foreign "C:listen,idris_net"
%foreign "C:listen,libidris2_support"
export
socket_listen : (sockfd : SocketDescriptor) -> (backlog : Int) -> PrimIO Int
-- From idris_net.h
%foreign "C:idrnet_socket,idris_net"
%foreign "C:idrnet_socket,libidris2_support"
export
idrnet_socket : (domain, type, protocol : Int) -> PrimIO Int
%foreign "C:idrnet_bind,idris_net"
%foreign "C:idrnet_bind,libidris2_support"
export
idrnet_bind : (sockfd : SocketDescriptor) -> (family, socket_type : Int) -> (host : String)
-> (port : Port) -> PrimIO Int
%foreign "C:idrnet_connect,idris_net"
%foreign "C:idrnet_connect,libidris2_support"
export
idrnet_connect : (sockfd : SocketDescriptor) -> (family, socket_type : Int) -> (host : String)
-> (port : Port) -> PrimIO Int
%foreign "C:idrnet_sockaddr_family,idris_net"
%foreign "C:idrnet_sockaddr_family,libidris2_support"
export
idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_sockaddr_ipv4,idris_net"
%foreign "C:idrnet_sockaddr_ipv4,libidris2_support"
export
idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String
%foreign "C:idrnet_sockaddr_ipv4_port,idris_net"
%foreign "C:idrnet_sockaddr_ipv4_port,libidris2_support"
export
idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_sockaddr_port,idris_net"
%foreign "C:idrnet_sockaddr_port,libidris2_support"
export
idrnet_sockaddr_port : (sockfd : SocketDescriptor) -> PrimIO Int
%foreign "C:idrnet_create_sockaddr,idris_net"
%foreign "C:idrnet_create_sockaddr,libidris2_support"
export
idrnet_create_sockaddr : PrimIO AnyPtr
%foreign "C:idrnet_accept,idris_net"
%foreign "C:idrnet_accept,libidris2_support"
export
idrnet_accept : (sockfd : SocketDescriptor) -> (sockaddr : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_send,idris_net"
%foreign "C:idrnet_send,libidris2_support"
export
idrnet_send : (sockfd : SocketDescriptor) -> (dataString : String) -> PrimIO Int
%foreign "C:idrnet_send_buf,idris_net"
%foreign "C:idrnet_send_buf,libidris2_support"
export
idrnet_send_buf : (sockfd : SocketDescriptor) -> (dataBuffer : AnyPtr) -> (len : Int) -> PrimIO Int
%foreign "C:idrnet_recv,idris_net"
%foreign "C:idrnet_recv,libidris2_support"
export
idrnet_recv : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
%foreign "C:idrnet_recv_buf,idris_net"
%foreign "C:idrnet_recv_buf,libidris2_support"
export
idrnet_recv_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int)
-> PrimIO Int
%foreign "C:idrnet_sendto,idris_net"
%foreign "C:idrnet_sendto,libidris2_support"
export
idrnet_sendto : (sockfd : SocketDescriptor) -> (dataString,host : String)
-> (port : Port) -> (family : Int) -> PrimIO Int
%foreign "C:idrnet_sendto_buf,idris_net"
%foreign "C:idrnet_sendto_buf,libidris2_support"
export
idrnet_sendto_buf : (sockfd : SocketDescriptor) -> (dataBuf : AnyPtr) -> (buf_len : Int)
-> (host : String) -> (port : Port) -> (family : Int) -> PrimIO Int
%foreign "C:idrnet_recvfrom,idris_net"
%foreign "C:idrnet_recvfrom,libidris2_support"
export
idrnet_recvfrom : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
%foreign "C:idrnet_recvfrom_buf,idris_net"
%foreign "C:idrnet_recvfrom_buf,libidris2_support"
export
idrnet_recvfrom_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int)
-> PrimIO AnyPtr
%foreign "C:idrnet_get_recv_res,idris_net"
%foreign "C:idrnet_get_recv_res,libidris2_support"
export
idrnet_get_recv_res : (res_struct : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_get_recv_payload,idris_net"
%foreign "C:idrnet_get_recv_payload,libidris2_support"
export
idrnet_get_recv_payload : (res_struct : AnyPtr) -> PrimIO String
%foreign "C:idrnet_free_recv_struct,idris_net"
%foreign "C:idrnet_free_recv_struct,libidris2_support"
export
idrnet_free_recv_struct : (res_struct : AnyPtr) -> PrimIO ()
%foreign "C:idrnet_get_recvfrom_res,idris_net"
%foreign "C:idrnet_get_recvfrom_res,libidris2_support"
export
idrnet_get_recvfrom_res : (res_struct : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_get_recvfrom_payload,idris_net"
%foreign "C:idrnet_get_recvfrom_payload,libidris2_support"
export
idrnet_get_recvfrom_payload : (res_struct : AnyPtr) -> PrimIO String
%foreign "C:idrnet_get_recvfrom_sockaddr,idris_net"
%foreign "C:idrnet_get_recvfrom_sockaddr,libidris2_support"
export
idrnet_get_recvfrom_sockaddr : (res_struct : AnyPtr) -> PrimIO AnyPtr
%foreign "C:idrnet_free_recvfrom_struct,idris_net"
%foreign "C:idrnet_free_recvfrom_struct,libidris2_support"
export
idrnet_free_recvfrom_struct : (res_struct : AnyPtr) -> PrimIO ()
%foreign "C:idrnet_geteagain,idris_net"
%foreign "C:idrnet_geteagain,libidris2_support"
export
idrnet_geteagain : PrimIO Int
%foreign "C:idrnet_errno,idris_net"
%foreign "C:idrnet_errno,libidris2_support"
export
idrnet_errno : PrimIO Int
%foreign "C:idrnet_malloc,idris_net"
%foreign "C:idrnet_malloc,libidris2_support"
export
idrnet_malloc : (size : Int) -> PrimIO AnyPtr
%foreign "C:idrnet_free,idris_net"
%foreign "C:idrnet_free,libidris2_support"
export
idrnet_free : (ptr : AnyPtr) -> PrimIO ()
%foreign "C:idrnet_peek,idris_net"
%foreign "C:idrnet_peek,libidris2_support"
export
idrnet_peek : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> PrimIO {-Unsigned-} Int
%foreign "C:idrnet_poke,idris_net"
%foreign "C:idrnet_poke,libidris2_support"
export
idrnet_poke : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> (val : Int {- should be Char? -})
-> PrimIO ()

View File

@ -47,7 +47,7 @@ BACKLOG : Int
BACKLOG = 20
-- Repeat to avoid a dependency cycle
%foreign "C:idrnet_geteagain,idris_net"
%foreign "C:idrnet_geteagain,libidris2_support"
idrnet_geteagain : PrimIO Int
export
@ -60,10 +60,10 @@ EAGAIN =
-- ---------------------------------------------------------------- [ Error Code ]
-- repeat without export to avoid dependency cycles
%foreign "C:idrnet_errno,idris_net"
%foreign "C:idrnet_errno,libidris2_support"
idrnet_errno : PrimIO Int
%foreign "C:isNull,idris_net"
%foreign "C:isNull,libidris2_support"
idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int

View File

@ -1,2 +0,0 @@
Received: hello world!
Received: echo: hello world!

View File

@ -1,58 +0,0 @@
#include <assert.h>
#include <stdio.h>
#ifndef _WIN32
#include <netinet/in.h>
#include <arpa/inet.h>
#endif
#include "idris_net.h"
void test_sockaddr_port_returns_random_port_when_bind_port_is_0() {
int sock = idrnet_socket(AF_INET, 1, 0);
assert(sock > 0);
int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 0);
assert(res == 0);
res = idrnet_sockaddr_port(sock);
assert(res > 0);
close(sock);
}
void test_sockaddr_port_returns_explicitly_assigned_port() {
int sock = idrnet_socket(AF_INET, 1, 0);
assert(sock > 0);
int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 34567);
assert(res == 0);
res = idrnet_sockaddr_port(sock);
assert(res == 34567);
close(sock);
}
void test_peek_and_poke_buffer() {
void *buf = idrnet_malloc(100);
assert(buf > 0);
for (int i = 0; i < 100; i++) {
idrnet_poke(buf,i,7*i);
}
for(int i = 0; i < 100; i++) {
assert (idrnet_peek(buf,i) == (0xff & 7*i));
}
idrnet_free(buf);
}
int main(void) {
test_sockaddr_port_returns_explicitly_assigned_port();
test_sockaddr_port_returns_random_port_when_bind_port_is_0();
test_peek_and_poke_buffer();
printf("network library tests SUCCESS\n");
return 0;
}