cleanup

BACKUP/Makefile

@@ -0,0 +1,28 @@
+
+
+
+
+
+
+
+# all: test_typechecking.tc
+all: test_bitcoinpayment.tc 
+
+# z3: session.dats test_typechecking.dats
+	# patsopt -tc --constraint-export -d $< | patsolve_smt2 --printfile ./set.smt2 -i | tee ./constraints | z3 -t:2000 -smt2 -in 2>&1 | tee output | em -fgreen "^unsat" | em "^sat|^timeout|^unknown" #| grep -B1 "unknown"
+
+
+
+%.tc: %.dats
+	patsopt -tc --constraint-export -d $< | patsolve_smt2 --printfile ./set.smt2 -i | tee ./constraints | z3 -t:2000 -smt2 -in 2>&1 | tee output | em -fgreen "^unsat" | em "^sat|^timeout|^unknown" 
+
+
+constraints.xx: 
+	z3 -t:2000 -smt2 -in 2>&1 | tee output | em -fgreen "^unsat" | em "^sat|^timeout|^unknown" 
+
+
+redisd:
+	docker run --name redisd -d redis 
+
+redis-cli:
+	docker run -it --rm --link redisd:redis redis redis-cli -h redis -p 6379

BACKUP/README.md

@@ -0,0 +1,2 @@
+# ats-sessions
+Session Types Library for ATS

BACKUP/address.sats

@@ -0,0 +1,11 @@
+
+
+abstype address
+
+
+fun addr_make (string): addres s 
+
+fun print_addr (address): void 
+fun eq_addr_addr (address, address): bool
+overload print with print_addr 
+overload =     with eq_addr_addr

BACKUP/ats/Makefile

@@ -0,0 +1,16 @@
+
+PATSOPT=patsopt 
+CC=gcc
+CFLAGS += -g -std=c99 -D_GNU_SOURCE -I$(PATSHOME) -I$(PATSHOME)/ccomp/runtime -I$(PATSHOME)/contrib/atscntrb -DATS_MEMALLOC_LIBC
+
+%_dats.c: %.dats
+	$(PATSOPT) -o $@ -d $< 
+
+%_sats.c: %.sats
+	$(PATSOPT) -o $@ -s $< 
+
+a.out: json_dats.c thread_dats.c transport_dats.c main_dats.c uuid_dats.c
+	$(CC) $(CFLAGS) -ljansson -lpthread -lnng $^ -o $@
+
+clean:
+	rm -rf *ats.c

BACKUP/ats/endpoint.dats

@@ -0,0 +1,34 @@
+#define ATS_DYNLOADFLAG 0
+
+staload "./endpoint.sats"
+
+
+local (************************)
+
+#include "share/atspre_staload_libats_ML.hats"
+
+typedef list (a:t@ype) = list0 a
+typedef peer = (string (* uuid *), int (* role *))
+
+datavtype ep_t (t:transport) = Ep of (transport t, 
+	 						   		  set int (* full *), set int (* self *), 
+	 						   		  uuid (* session *), uuid (* self *),
+	 						  		  list peer)
+
+
+assume endpoint = [t:transport] ep_t t
+
+in    (************************)
+
+
+implement ep_request (ep) = let 
+	val @Ep (trans, full, self, idss, idself, peers) = ep 
+
+
+
+	val _ = fold@ep
+in 
+end
+
+
+end   (************************)

BACKUP/ats/endpoint.sats

@@ -0,0 +1,28 @@
+staload "./uuid.sats"
+staload "libats/ML/SATS/basis.sats"
+
+absvtype endpoint (transport) = ptr
+
+fun ep_make (): endpoint
+
+//fun ep_get_id (!endpoint): uuid
+//fun ep_set_id (!endpoint, uuid): void
+
+fun ep_set_roles (!endpoint, set int): void
+fun ep_get_roles (!endpoint): set int
+
+fun {t:transport} ep_set_transport (transport t): void
+
+fun ep_accept  (!endpoint, set int): bool
+fun ep_request (!endpoint): bool
+
+fun ep_close (endpoint): void
+fun ep_wait  (endpoint): void
+
+fun ep_broadcast (!endpoint, msg): void
+fun ep_receive   (!endpoint): msg
+
+fun _ep_encode (!endpoint, msg_ss): msg_ep
+fun _ep_decode (!endpoint, msg_ep): msg_ss
+
+fun ep_cut (endpoint, endpoint): endpoint

BACKUP/ats/json.dats

@@ -0,0 +1,59 @@
+#define ATS_DYNLOADFLAG 0
+
+staload "./json.sats"
+
+local (*********************)
+
+#include "share/atspre_staload.hats"
+staload JSON = "contrib/atscntrb/atscntrb-hx-libjansson/SATS/jansson.sats"
+staload _    = "contrib/atscntrb/atscntrb-hx-libjansson/DATS/jansson.dats"
+staload UN   = "prelude/SATS/unsafe.sats"
+
+macdef JSON_DECODE_ANY = $extval (int, "JSON_DECODE_ANY")
+
+assume json = $JSON.JSONptr1
+
+in    (*********************)
+
+implement json_loads (str) = let 
+	var err: $JSON.json_error_t 
+	val json = $JSON.json_loads ($UN.strptr2string str, JSON_DECODE_ANY, err)
+	val _ = assert_errmsg ($JSON.JSONptr_isnot_null json, "json_loads failed.")
+in 
+	json 
+end
+
+implement json_loadb {n} {l} (pf | buf, size) = let 
+	var err: $JSON.json_error_t
+	val json = $JSON.json_loadb (pf | buf, i2sz size, JSON_DECODE_ANY, err)
+	val _ = assert_errmsg ($JSON.JSONptr_isnot_null json, "json_loadb failed.")
+in 
+	json
+end
+
+implement json_dumps (json) = let 
+	val str = $JSON.json_dumps (json, $JSON.JSON_ENCODE_ANY)
+	val _   = assert_errmsg (isneqz str, "json_dump failed.")
+	val _   = $JSON.json_decref json
+in 
+	str
+end
+
+implement json_free (json) = $JSON.json_decref json
+
+implement to_json<string> (str) = let 
+	val json = $JSON.json_string str
+	val _    = assert_errmsg ($JSON.JSONptr_isnot_null json, "to_json<string> failed.")
+in 
+	json
+end
+
+implement from_json<cstring> (json) = let 
+	val (pf | s) = $JSON.json_string_value json
+	val str = copy s
+	prval _ = minus_addback (pf, s | json)
+in 
+	str
+end
+
+end   (*********************)

BACKUP/ats/json.sats

@@ -0,0 +1,16 @@
+/*
+ *  Simple interface for converting datatypes to json
+ */
+
+absvtype json
+
+fun {a:vt@ype} to_json   (!a): json
+fun {a:vt@ype} from_json (!json): a
+
+vtypedef cstring = [l:addr|l>null] strptr l
+
+fun json_loads (!cstring): json 
+fun json_loadb {n:nat} {l:addr|l>null} (!(@[byte][n] @ l) | ptr l, int n): json
+fun json_dumps (json): cstring
+fun json_free  (json): void
+

BACKUP/ats/main.dats

@@ -0,0 +1,95 @@
+#include "share/atspre_staload.hats"
+
+%{^
+#include <nng/nng.h>
+#include <nng/protocol/bus0/bus.h>
+#include <uuid/uuid.h>
+%}
+
+staload "./transport.sats"
+staload "./json.sats"
+staload "./thread.sats"
+staload "./uuid.sats"
+
+staload _ = "./transport.dats"
+staload _ = "./json.dats"
+staload _ = "./thread.dats"
+
+staload "libats/libc/SATS/unistd.sats"
+
+implement main0 () = let 
+
+//	val uuid1 = uuid_generate ()
+//	val uuid2 = uuid_copy uuid1
+
+//	var uuidstr: uuid_string
+//	val () = uuid_unparse (uuid2, uuidstr)
+
+//	val _ = println! ($UNSAFE.cast{string} uuidstr)
+//	val uuid3 = uuid_parse uuidstr
+
+//	val _ = println! (uuid_equal (uuid1, uuid3))
+
+//	val _ = uuid_free uuid1 
+//	val _ = uuid_free uuid2
+//	val _ = uuid_free uuid3 
+
+
+	val (tbroker, sock) = trans_nn_broker ("inproc://bus")
+
+	fun t1 (): void = let 
+		val trans = trans_make<nn> ()
+		val _     = println! "t1 connecting"
+		val _     = trans_connect (trans, "inproc://bus")
+		val _     = sleep 2
+		val json  = to_json<string> "hello"
+		val _     = println! "t1 sending"
+		val _     = trans_send<json> (trans, json)
+		val _     = println! "t1 sent"
+	in 
+		trans_term trans
+	end
+
+	fun t2 (): void = let 
+		val trans = trans_make<nn> () 
+		val _     = println! "t2 connecting"
+		val _     = trans_connect (trans, "inproc://bus")
+		val _     = println! "t2 receiving"
+		val json  = trans_recv<json> (trans)
+		val _     = println! "t2 received"
+		val resp  = from_json<cstring> json
+		val _     = println! resp
+		val _     = free resp
+		val _     = json_free json
+		val _     = sleep 1
+	in 
+		trans_term trans
+	end
+
+	fun t3 (): void = let 
+		val trans = trans_make<nn> ()
+		val _     = trans_connect (trans, "inproc://bus")
+
+		fun echo (json): void = let 
+			val resp = from_json<cstring> json 
+			val _    = println! resp 
+			val _    = free resp 
+			val _    = json_free json 
+		in 
+		end 
+
+		val _ = trans_recv<json> (trans, llam json => echo json)
+	in 
+		trans_term trans 
+	end 
+
+	val tid1 = thread_spawn (llam () => t1 ())
+	val _     = sleep 1
+	val tid2 = thread_spawn (llam () => t2 ())
+	val _ = thread_join tid1
+	val _ = thread_join tid2
+
+	val _ = trans_term sock 
+	val _ = thread_join tbroker
+in 
+end

BACKUP/ats/roles.sats

@@ -0,0 +1,5 @@
+
+
+
+abstype roles
+

BACKUP/ats/test.c

@@ -0,0 +1,87 @@
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <nng/nng.h>
+#include <nng/protocol/bus0/bus.h>
+#include <nng/supplemental/util/platform.h>
+#include <stdlib.h>
+
+void work(void* arg) {
+	nng_aio* aio = *(nng_aio**)arg;
+	int ret = nng_aio_result(aio);
+
+	if (ret != 0) {
+		printf("Error: %s\n", nng_strerror(ret));
+		return;
+	}
+
+	nng_msg* msg = nng_aio_get_msg(aio);
+	printf("Server received: %s\n", nng_msg_body(msg));
+	nng_msg_free(msg);
+
+	// this is a defered free
+	nng_aio_free(aio);
+}
+
+
+int server(const char* url) {
+
+	nng_socket sock;
+	int ret;
+
+	assert(nng_bus0_open(&sock) == 0);
+
+	nng_aio* aio;
+	assert(nng_aio_alloc(&aio, work, &aio) == 0);
+
+	assert(nng_listen(sock, url, NULL, 0) == 0);
+	printf("Server connected\n");
+
+	nng_recv_aio(sock, aio);
+	nng_aio_wait(aio);
+	// assert(nng_aio_result(aio) == 0);
+	// nng_msg* msg = nng_aio_get_msg(aio);
+
+	// printf("Server received: %s", nng_msg_body(msg));
+	// nng_msg_free(msg);
+
+	// nng_aio_free(aio);
+
+	// char* msg; 
+	// size_t size;
+
+	// nng_recv(sock, &msg, &size, NNG_FLAG_ALLOC);
+	// printf("Message received: %s\n", msg);
+	// free(msg);
+
+	nng_close(sock);
+	return 0;
+}
+
+int client(const char* url) {
+	nng_socket sock;
+	int ret;
+
+	assert(nng_bus0_open(&sock) == 0);
+	assert(nng_dial(sock, url, NULL, 0) == 0);
+	printf("Client connected\n");
+
+	char* data = "hello";
+	printf("Client sent: %s\n", data);
+	nng_send(sock, data, strlen(data), 0);
+
+	nng_msleep(1000);
+	nng_close(sock);
+	return 0;
+}
+
+int main(int argc, char** argv) {
+	assert(argc == 3);
+
+	switch (argv[1][0]) {
+		case 'c': client(argv[2]); break;
+		case 's': server(argv[2]); break;
+	}
+
+	return 0;
+}