From 8715374a52ab3598aa6723a83adc5e013533cfda Mon Sep 17 00:00:00 2001 From: Keigo Imai Date: Fri, 6 Apr 2018 18:40:12 +0900 Subject: [PATCH] up to date with the journal revision --- README.md | 45 ++----- examples/dbserver.ml | 36 ++++++ examples/ex_multi1.ml | 30 ----- examples/ex_multi2.ml | 14 --- examples/ex_single1.ml | 22 ---- examples/ex_single2.ml | 41 ------- examples/example_journal1.ml | 14 +++ examples/example_journal2.ml | 27 ++++ examples/example_journal3.ml | 38 ++++++ examples/smtp2.ml | 2 +- lib/lsession.ml | 118 +++++++++--------- lib/lsession.mli | 62 +++++----- lib/session.ml | 230 +++++++++++++++++------------------ lib/session.mli | 192 +++++++++++------------------ lib/unixAdapter.ml | 18 +-- net/dsession.ml | 30 ++--- net/dsession.mli | 32 ++--- ppx/ppx_session.ml | 6 - 18 files changed, 432 insertions(+), 525 deletions(-) create mode 100644 examples/dbserver.ml delete mode 100644 examples/ex_multi1.ml delete mode 100644 examples/ex_multi2.ml delete mode 100644 examples/ex_single1.ml delete mode 100644 examples/ex_single2.ml create mode 100644 examples/example_journal1.ml create mode 100644 examples/example_journal2.ml create mode 100644 examples/example_journal3.ml diff --git a/README.md b/README.md index 9c624fd..240c965 100644 --- a/README.md +++ b/README.md @@ -6,12 +6,12 @@ Session-ocaml is an implementation of session types in OCaml. ## How to try it -Prepare OCaml 4.02.1 or later and install ```findlib```, ```ocamlbuild```, ```ppx_tools```. -We recommend to use ```opam``` and OCaml 4.03.0. +Prepare OCaml __4.05__ and install ```findlib```, ```ocamlbuild```, ```ppx_tools```. +We recommend to use ```opam``` -Install the compiler and prerequisite libraries. +Install the compiler and prerequisite libraries. (__NOTE__: the version number has changed: 4.03 ==> __4.05__) - opam switch 4.03.0 + opam switch 4.05.0 eval `opam config env` opam install ocamlfind ocamlbuild ppx_tools @@ -46,12 +46,11 @@ Also, you can uninstall manually by ```ocamlfind remove session-ocaml```. # Macro for branching / selection -For branching on arbitrary labels, we provide a macro ```match%branch0``` and ```match%branch```. - -Single-channel case (```open Session0```): +For branching on arbitrary labels, we provide a macro ```match%branch```. ```ocaml - match%branch0 () with + open Session + match%branch s with | `apple -> send 100 | `banana -> recv () | `orange -> send "Hello!" @@ -66,39 +65,11 @@ Its protocol type will be: | `orange of [`msg of req * string * 'a]] ``` -Multi-channel case (```open SessionN```): - -```ocaml - match%branch _2 with - | `batman -> [%select _2 `goodbye] - | `ironman -> let%s x = recv _2 in send _2 x - | `hulk -> send _2 "foobar" -``` - -Protocol type: - -``` - [ `branch of resp * - [ `batman of [ `branch of req * _[> `goodbye of '_e ] ] - | `hulk of [ `msg of req * string * '_e ] - | `ironman of [ `msg of resp * '_f * [ `msg of req * '_f * '_e ] ] ] ] -``` - Similarly, we have a macro for selection, like ```ocaml - [%select0 `label] -``` - -or - + [%select s `label] ``` - [%select _n `bark] -``` - -## TODO - -* Better error reporting inside %branch0 and %branch ---- author: Keigo IMAI (@keigoi on Twitter / keigoi __AT__ gifu-u.ac.jp) diff --git a/examples/dbserver.ml b/examples/dbserver.ml new file mode 100644 index 0000000..f23ce42 --- /dev/null +++ b/examples/dbserver.ml @@ -0,0 +1,36 @@ +open Session + +type result = Result (*stub*) +type credential = Cred (*stub*) +let bad_credential Cred = false (*stub*) +let do_query (query:string) : result = Result (*stub*) + +let db_ch = new_channel () +and worker_ch = new_channel () + +let rec main () = + accept db_ch ~bindto:_0 >> + recv _0 >>= fun cred -> + if bad_credential cred then + select_left _0 >> + close _0 + else + select_right _0 >> + connect worker_ch ~bindto:_1 >> + deleg_send _1 ~release:_0 >> + close _1 >>= + main + +let rec worker () = + accept worker_ch ~bindto:_0 >> + deleg_recv _0 ~bindto:_1 >> + close _0 >> + let rec loop () = + branch + ~left:(_1, fun () -> close _1) + ~right:(_1, fun () -> + recv _1 >>= fun query -> + let res = do_query query in + send _1 res >>= + loop) + in loop () >>= worker diff --git a/examples/ex_multi1.ml b/examples/ex_multi1.ml deleted file mode 100644 index 308ef82..0000000 --- a/examples/ex_multi1.ml +++ /dev/null @@ -1,30 +0,0 @@ -(* Multi-session example with slots and lenses *) -open Session -open SessionN -open Ex_single2 - -open Session;; - -(* The service channel between the main thread and workers *) -let deleg_ch = new_channel ();; - -(* The main thread *) -let rec main_thread () = - accept arith_ch ~bindto:_0 >> connect deleg_ch ~bindto:_1 >> - deleg_send _1 ~release:_0 >> - close _1 >>= main_thread;; - -(* The worker thread *) -let rec worker_thread i () = - let%s _ = accept deleg_ch ~bindto:_1 >> deleg_recv _1 ~bindto:_0 in - (Printf.printf "worker %d\n" i; - close _1) >> - arith_server () >>= worker_thread i;; - -(* Invokation of threads *) -for i = 0 to 5 do ignore @@ Thread.create (run @@ worker_thread i) () done; -Thread.create (run main_thread) ();; - -for i = 0 to 10 do - Session0.connect_ arith_ch arith_client () -done;; diff --git a/examples/ex_multi2.ml b/examples/ex_multi2.ml deleted file mode 100644 index 5e6b3d6..0000000 --- a/examples/ex_multi2.ml +++ /dev/null @@ -1,14 +0,0 @@ - -open Lsession -;; - - -let ch = new_channel () -;; -let s = _0 - -let f () = - let%lin #s = accept ch in - let%lin #s = send 100 s in - close s - diff --git a/examples/ex_single1.ml b/examples/ex_single1.ml deleted file mode 100644 index 78c1c42..0000000 --- a/examples/ex_single1.ml +++ /dev/null @@ -1,22 +0,0 @@ -(* Single-session example *) -open Session -open Session0 - -let neg_server () = - let%s x = recv () in - send (-x) >> - close () - -let neg_client () = - send 12345 >> - let%s x = recv () in - Printf.printf "Negated: %d\n" x; (* prints "-12345" *) - close () - -let neg_ch = new_channel () - -let _ = - ignore @@ Thread.create - (accept_ neg_ch neg_server) (); - connect_ neg_ch neg_client () - diff --git a/examples/ex_single2.ml b/examples/ex_single2.ml deleted file mode 100644 index 27ddc26..0000000 --- a/examples/ex_single2.ml +++ /dev/null @@ -1,41 +0,0 @@ -(* Single-session example with branching and selection on arbitrary labels. *) - -(* This will be rewritten with macros ```match%branch0``` and ```[%select]```. See README.md *) - -open Session -open Session0 - -type binop = Add | Sub | Mul | Div - -let eval_binop = function - | Add -> (+) | Sub -> (-) - | Mul -> ( * ) | Div -> (/) - -let rec arith_server () = - match%branch0 () with - | `neg -> Ex_single1.neg_server () - | `bin -> binop_server () - | `fin -> close () - -and binop_server () = - let%s op = recv () in - let%s (x,y) = recv () in - send (eval_binop op x y) >> - arith_server () - -let arith_client () = - [%select0 `bin] >> - send Add >> - send (150, 250) >> - let%s ans = recv () in - Printf.printf "Answer: %d\n" ans; - [%select0 `fin] >> - close () >> - return () - -let arith_ch = new_channel () - -let _ = - ignore @@ Thread.create - (accept_ arith_ch arith_server) (); - connect_ arith_ch arith_client () diff --git a/examples/example_journal1.ml b/examples/example_journal1.ml new file mode 100644 index 0000000..a39cffb --- /dev/null +++ b/examples/example_journal1.ml @@ -0,0 +1,14 @@ +open Session +let xor : bool -> bool -> bool = (<>) +let print_bool = Printf.printf "%B" +let xor_ch = new_channel ();; +Thread.create + (accept_ xor_ch (fun () -> + recv s >>= fun (x,y) -> + send s (xor x y) >> + close s)) ();; +connect_ xor_ch (fun () -> + send s (false,true) >> + recv s >>= fun b -> + print_bool b; + close s) () diff --git a/examples/example_journal2.ml b/examples/example_journal2.ml new file mode 100644 index 0000000..03cf295 --- /dev/null +++ b/examples/example_journal2.ml @@ -0,0 +1,27 @@ +open Session +let xor : bool -> bool -> bool = (<>) +let print_bool = Printf.printf "%B" +type binop = And | Or | Xor | Imp +let log_ch = new_channel () +let eval_op = function + | And -> (&&) + | Or -> (||) + | Xor -> xor + | Imp -> (fun a b -> not a || b) +let rec logic_server () = + branch ~left:(s, fun () -> + recv s >>= fun op -> + recv s >>= fun (x,y) -> + send s (eval_op op x y) >>= fun () -> + logic_server ()) + ~right:(s, fun () -> close s);; +Thread.create + (accept_ log_ch logic_server) ();; +connect_ log_ch (fun () -> + select_left s >> + send s And >> + send s (true, false) >> + recv s >>= fun ans -> + (print_bool ans; + select_right s >> + close s)) () diff --git a/examples/example_journal3.ml b/examples/example_journal3.ml new file mode 100644 index 0000000..7342437 --- /dev/null +++ b/examples/example_journal3.ml @@ -0,0 +1,38 @@ +open Session +open Example_journal2 +let worker_ch = new_channel () +let rec main () = + accept log_ch ~bindto:_0 >> + connect worker_ch ~bindto:_1 >> + deleg_send _1 ~release:_0 >> + close _1 >>= fun () -> + main () +let rec worker () = + accept worker_ch ~bindto:_1 >> + deleg_recv _1 ~bindto:_0 >> + close _1 >> + logic_server () >>= fun () -> + worker ();; +for i = 0 to 5 do + Thread.create (run worker) () +done;; +Thread.create (run main) ();; +connect_ log_ch (fun () -> + select_left s >> + send s Or >> + send s (true, false) >> + recv s >>= fun ans -> + print_bool ans; print_newline (); + select_left s >> + send s And >> + send s (true, false) >> + recv s >>= fun ans -> + print_bool ans; print_newline (); + select_left s >> + send s Xor >> + send s (true, false) >> + recv s >>= fun ans -> + print_bool ans; print_newline (); + select_right s >> + close s) () + diff --git a/examples/smtp2.ml b/examples/smtp2.ml index b3abc7a..eeddc6f 100644 --- a/examples/smtp2.ml +++ b/examples/smtp2.ml @@ -137,7 +137,7 @@ open Tcp let s = _0 -let sendmail host port from to_ mailbody () : ((smtp,cli,stream) dsess * empty_three, empty_four, unit lin) lmonad = +let sendmail host port from to_ mailbody () : ((smtp,cli,stream) dsess * empty_three, empty_four, unit) lmonad = let%lin `_200(msg,#s) = branch s in List.iter print_endline msg; let%lin #s = select (fun x -> `EHLO("me.example.com",x)) s in diff --git a/lib/lsession.ml b/lib/lsession.ml index 2e3d0ec..c124bd3 100644 --- a/lib/lsession.ml +++ b/lib/lsession.ml @@ -1,10 +1,7 @@ -type 'a lin = L of 'a type 'a data = W of 'a type ('pre, 'post, 'a) lmonad = 'pre -> 'post * 'a type 'f lbind = 'f -let unlin (L v) = v - type ('a,'b,'ss,'tt) slot = ('ss -> 'a) * ('ss -> 'b -> 'tt) let _0 = (fun (a,_) -> a), (fun (_,ss) b -> (b,ss)) @@ -15,7 +12,7 @@ let _3 = (fun (_,(_,(_,(a,_)))) -> a), (fun (s0,(s1,(s2,(_,ss)))) b -> (s0,(s1,( type empty = Empty type all_empty = empty * 'a as 'a -let return a pre = pre, L a +let return a pre = pre, a let (>>=) f g pre = let mid, la = f pre in g la mid let (>>) f g pre = let mid, _ = f pre in g mid @@ -35,111 +32,109 @@ module type S = sig val new_channel : unit -> 'p channel type ('p,'q) sess - type ('p, 'q) lsess = ('p, 'q) sess lin - val accept : 'p channel -> ('pre, 'pre, ('p, serv) lsess) lmonad + val accept : 'p channel -> ('pre, 'pre, ('p, serv) sess) lmonad - val connect : 'p channel -> ('pre, 'pre, ('p, cli) lsess) lmonad + val connect : 'p channel -> ('pre, 'pre, ('p, cli) sess) lmonad - val close : (([`close], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, unit lin) lmonad + val close : (([`close], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, unit) lmonad - val send : 'v -> (([`msg of 'r1 * 'v * 'p], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('p, 'r1*'r2) lsess) lmonad + val send : 'v -> (([`msg of 'r1 * 'v * 'p], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, ('p, 'r1*'r2) sess) lmonad - val receive : (([`msg of 'r2 * 'v * 'p], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('v data * ('p, 'r1*'r2) lsess) lin) lmonad + val receive : (([`msg of 'r2 * 'v * 'p], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, 'v data * ('p, 'r1*'r2) sess) lmonad - val select : (('p,'r2*'r1) lsess -> ([>] as 'br)) - -> (([`branch of 'r1 * 'br],'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('p,'r1*'r2) lsess) lmonad + val select : (('p,'r2*'r1) sess -> ([>] as 'br)) + -> (([`branch of 'r1 * 'br],'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, ('p,'r1*'r2) sess) lmonad - val branch : (([`branch of 'r2 * [>] as 'br], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, 'br lin) lmonad + val branch : (([`branch of 'r2 * [>] as 'br], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, 'br) lmonad - val deleg_send : (('pp, 'qq) lsess, empty, 'mid, 'post) slot - -> (([`deleg of 'r1 * ('pp, 'qq) lsess * 'p], 'r1*'r2) lsess, empty, 'pre, 'mid) slot - -> ('pre, 'post, ('p, 'r1*'r2) lsess) lmonad + val deleg_send : (('pp, 'qq) sess, empty, 'mid, 'post) slot + -> (([`deleg of 'r1 * ('pp, 'qq) sess * 'p], 'r1*'r2) sess, empty, 'pre, 'mid) slot + -> ('pre, 'post, ('p, 'r1*'r2) sess) lmonad val deleg_recv : - (([`deleg of 'r2 * ('pp, 'qq) lsess * 'p], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, (('pp,'qq) lsess * ('p,'r1*'r2) lsess) lin) lmonad + (([`deleg of 'r2 * ('pp, 'qq) sess * 'p], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, ('pp,'qq) sess * ('p,'r1*'r2) sess) lmonad end module Make(U : UnsafeChannel) : S = struct type ('p,'q) sess = U.t type 'p channel = U.t Schannel.t - type ('p, 'q) lsess = ('p, 'q) sess lin let new_channel = Schannel.create - let accept : 'p 'pre. 'p channel -> ('pre, 'pre, ('p, serv) lsess) lmonad = + let accept : 'p 'pre. 'p channel -> ('pre, 'pre, ('p, serv) sess) lmonad = fun ch pre -> let s = Schannel.receive ch in - pre, L s + pre, s - let connect : 'p 'pre. 'p channel -> ('pre, 'pre, ('p, cli) lsess) lmonad = + let connect : 'p 'pre. 'p channel -> ('pre, 'pre, ('p, cli) sess) lmonad = fun ch pre -> let s = U.create () in Schannel.send ch (U.reverse s); - pre, L s + pre, s let close : 'pre 'r1 'r2 'post. - (([`close], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, unit lin) lmonad = + (([`close], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, unit) lmonad = fun (_,set) pre -> - set pre Empty, L () + set pre Empty, () let send : 'v 'r1 'p 'r2 'pre 'post. - 'v -> (([`msg of 'r1 * 'v * 'p], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('p, 'r1*'r2) lsess) lmonad = + 'v -> (([`msg of 'r1 * 'v * 'p], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, ('p, 'r1*'r2) sess) lmonad = fun v (get,set) pre -> - let s = unlin @@ get pre in + let s = get pre in U.send s v; - set pre Empty, L s + set pre Empty, s let receive : 'r2 'v 'p 'r1 'pre 'post. - (([`msg of 'r2 * 'v * 'p], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('v data * ('p, 'r1*'r2) lsess) lin) lmonad = + (([`msg of 'r2 * 'v * 'p], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, 'v data * ('p, 'r1*'r2) sess) lmonad = fun (get,set) pre -> - let s = unlin @@ get pre in - set pre Empty, L (W (U.receive s), L s) + let s = get pre in + set pre Empty, (W (U.receive s), s) let select : 'p 'r2 'r1 'pre 'post. - (('p,'r2*'r1) lsess -> ([>] as 'br)) - -> (([`branch of 'r1 * 'br],'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('p,'r1*'r2) lsess) lmonad = + (('p,'r2*'r1) sess -> ([>] as 'br)) + -> (([`branch of 'r1 * 'br],'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, ('p,'r1*'r2) sess) lmonad = fun f (get,set) pre -> - let s = unlin @@ get pre in - U.send s (f (L (U.reverse s))); - set pre Empty, L s + let s = get pre in + U.send s (f (U.reverse s)); + set pre Empty, s let branch : 'r2 'r1 'pre 'post. - (([`branch of 'r2 * [>] as 'br], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, 'br lin) lmonad = + (([`branch of 'r2 * [>] as 'br], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, 'br) lmonad = fun (get,set) pre -> - let s = unlin @@ get pre in - set pre Empty, L (U.receive s) + let s = get pre in + set pre Empty, (U.receive s) let deleg_send : 'pp 'qq 'mid 'post 'r1 'r2 'pre. - (('pp, 'qq) lsess, empty, 'mid, 'post) slot - -> (([`deleg of 'r1 * ('pp, 'qq) lsess * 'p], 'r1*'r2) lsess, empty, 'pre, 'mid) slot - -> ('pre, 'post, ('p, 'r1*'r2) lsess) lmonad = + (('pp, 'qq) sess, empty, 'mid, 'post) slot + -> (([`deleg of 'r1 * ('pp, 'qq) sess * 'p], 'r1*'r2) sess, empty, 'pre, 'mid) slot + -> ('pre, 'post, ('p, 'r1*'r2) sess) lmonad = fun (get1,set1) (get2,set2) pre -> - let s = unlin @@ get2 pre in + let s = get2 pre in let mid = set2 pre Empty in - let t = unlin @@ get1 mid in + let t = get1 mid in U.send s t; - set1 mid Empty, L s + set1 mid Empty, s let deleg_recv : 'r2 'p 'r1 'pre 'post 'pp 'qq. - (([`deleg of 'r2 * ('pp, 'qq) lsess * 'p], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, (('pp,'qq) lsess * ('p,'r1*'r2) lsess) lin) lmonad = + (([`deleg of 'r2 * ('pp, 'qq) sess * 'p], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, ('pp,'qq) sess * ('p,'r1*'r2) sess) lmonad = fun (get,set) pre -> - let s = unlin @@ get pre in + let s = get pre in let t = U.receive s in - set pre Empty, L (L t, L s) + set pre Empty, (t, s) end @@ -159,13 +154,12 @@ module Syntax = struct let __bind_raw = fun m f pre -> match m pre with (mid,x) -> f x mid let __putval_raw = fun (_,set) v pre -> - set pre (L v), () + set pre v, () let __takeval_raw (get,set) pre = - set pre Empty, match get pre with L a -> a + set pre Empty, get pre let __mkbindfun f = f - let __run m pre = (>>=) (m pre) (fun (_,L a) -> a) let __dispose_env m pre = (>>=) (m pre) (fun (_,a) -> return (Empty, a)) end diff --git a/lib/lsession.mli b/lib/lsession.mli index 202f166..aefc159 100644 --- a/lib/lsession.mli +++ b/lib/lsession.mli @@ -1,4 +1,3 @@ -type 'a lin = L of 'a type 'a data = W of 'a type ('pre, 'post, 'a) lmonad type 'f lbind @@ -12,13 +11,13 @@ val _3 : ('a, 'b, ('s0 * ('s1 * ('s2 * ('a * 'ss)))), ('s0 * ('s1 * ('s2 * ('b * type empty type all_empty = empty * 'a as 'a -val return : 'a -> ('pre, 'pre, 'a lin) lmonad -val (>>=) : ('pre, 'mid, 'a lin) lmonad - -> ('a lin -> ('mid, 'post, 'b lin) lmonad) lbind - -> ('pre, 'post, 'b lin) lmonad -val (>>) : ('pre, 'mid, unit lin) lmonad - -> ('mid, 'post, 'b lin) lmonad - -> ('pre, 'post, 'b lin) lmonad +val return : 'a -> ('pre, 'pre, 'a) lmonad +val (>>=) : ('pre, 'mid, 'a) lmonad + -> ('a -> ('mid, 'post, 'b) lmonad) lbind + -> ('pre, 'post, 'b) lmonad +val (>>) : ('pre, 'mid, unit) lmonad + -> ('mid, 'post, 'b) lmonad + -> ('pre, 'post, 'b) lmonad module type UnsafeChannel = sig type t @@ -36,35 +35,34 @@ module type S = sig val new_channel : unit -> 'p channel type ('p,'q) sess - type ('p, 'q) lsess = ('p, 'q) sess lin - val accept : 'p channel -> ('pre, 'pre, ('p, serv) lsess) lmonad + val accept : 'p channel -> ('pre, 'pre, ('p, serv) sess) lmonad - val connect : 'p channel -> ('pre, 'pre, ('p, cli) lsess) lmonad + val connect : 'p channel -> ('pre, 'pre, ('p, cli) sess) lmonad - val close : (([`close], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, unit lin) lmonad + val close : (([`close], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, unit) lmonad - val send : 'v -> (([`msg of 'r1 * 'v * 'p], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('p, 'r1*'r2) lsess) lmonad + val send : 'v -> (([`msg of 'r1 * 'v * 'p], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, ('p, 'r1*'r2) sess) lmonad - val receive : (([`msg of 'r2 * 'v * 'p], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('v data * ('p, 'r1*'r2) lsess) lin) lmonad + val receive : (([`msg of 'r2 * 'v * 'p], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, 'v data * ('p, 'r1*'r2) sess) lmonad - val select : (('p,'r2*'r1) lsess -> ([>] as 'br)) - -> (([`branch of 'r1 * 'br],'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('p,'r1*'r2) lsess) lmonad + val select : (('p,'r2*'r1) sess -> ([>] as 'br)) + -> (([`branch of 'r1 * 'br],'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, ('p,'r1*'r2) sess) lmonad - val branch : (([`branch of 'r2 * [>] as 'br], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, 'br lin) lmonad + val branch : (([`branch of 'r2 * [>] as 'br], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, 'br) lmonad - val deleg_send : (('pp, 'qq) lsess, empty, 'mid, 'post) slot - -> (([`deleg of 'r1 * ('pp, 'qq) lsess * 'p], 'r1*'r2) lsess, empty, 'pre, 'mid) slot - -> ('pre, 'post, ('p, 'r1*'r2) lsess) lmonad + val deleg_send : (('pp, 'qq) sess, empty, 'mid, 'post) slot + -> (([`deleg of 'r1 * ('pp, 'qq) sess * 'p], 'r1*'r2) sess, empty, 'pre, 'mid) slot + -> ('pre, 'post, ('p, 'r1*'r2) sess) lmonad val deleg_recv : - (([`deleg of 'r2 * ('pp, 'qq) lsess * 'p], 'r1*'r2) lsess, empty, 'pre, 'post) slot - -> ('pre, 'post, (('pp,'qq) lsess * ('p,'r1*'r2) lsess) lin) lmonad + (([`deleg of 'r2 * ('pp, 'qq) sess * 'p], 'r1*'r2) sess, empty, 'pre, 'post) slot + -> ('pre, 'post, ('pp,'qq) sess * ('p,'r1*'r2) sess) lmonad end @@ -73,9 +71,9 @@ module Make(U : UnsafeChannel) : S include S module Syntax : sig - val bind : ('pre, 'mid, 'a lin) lmonad - -> ('a lin -> ('mid, 'post, 'b lin) lmonad) lbind - -> ('pre, 'post, 'b lin) lmonad + val bind : ('pre, 'mid, 'a) lmonad + -> ('a -> ('mid, 'post, 'b) lmonad) lbind + -> ('pre, 'post, 'b) lmonad module Internal : sig val __bind_raw : ('pre,'mid,'a) lmonad -> ('a -> ('mid,'post,'b) lmonad) -> ('pre,'post,'b) lmonad @@ -83,7 +81,7 @@ module Syntax : sig val __mkbindfun : ('a -> ('pre,'post,'b) lmonad) -> ('a -> ('pre, 'post, 'b) lmonad) lbind - val __putval_raw : (empty,'a lin,'pre,'post) slot -> 'a -> ('pre,'post,unit) lmonad - val __takeval_raw : ('a lin,empty,'pre,'post) slot -> ('pre,'post,'a) lmonad + val __putval_raw : (empty,'a,'pre,'post) slot -> 'a -> ('pre,'post,unit) lmonad + val __takeval_raw : ('a,empty,'pre,'post) slot -> ('pre,'post,'a) lmonad end end diff --git a/lib/session.ml b/lib/session.ml index 46efae9..9e665b9 100644 --- a/lib/session.ml +++ b/lib/session.ml @@ -1,25 +1,27 @@ (* slots and lenses *) type empty = Empty type all_empty = empty * 'a as 'a +let rec all_empty = Empty, all_empty -type ('a,'b,'ss,'tt) slot = ('ss -> 'a) * ('ss -> 'b -> 'tt) +type ('a,'b,'pre,'post) slot = ('pre -> 'a) * ('pre -> 'b -> 'post) +let s = (fun (a,_) -> a), (fun (_,ss) b -> (b,ss)) let _0 = (fun (a,_) -> a), (fun (_,ss) b -> (b,ss)) let _1 = (fun (_,(a,_)) -> a), (fun (s0,(_,ss)) b -> (s0,(b,ss))) let _2 = (fun (_,(_,(a,_))) -> a), (fun (s0,(s1,(_,ss))) b -> (s0,(s1,(b,ss)))) let _3 = (fun (_,(_,(_,(a,_)))) -> a), (fun (s0,(s1,(s2,(_,ss)))) b -> (s0,(s1,(s2,(b,ss))))) +let _4 = (fun (_,(_,(_,(_,(a,_))))) -> a), (fun (s0,(s1,(s2,(s3,(_,ss))))) b -> (s0,(s1,(s2,(s3,(b,ss)))))) -let rec all_empty = Empty, all_empty let _run_internal a f x = snd (f x a) -let run f x = _run_internal all_empty f x -let run_ m = _run_internal all_empty (fun () -> m) () +let run f x = snd (f x all_empty) +let run_ m = snd (m all_empty) -(* monads *) -type ('ss,'tt,'v) monad = 'ss -> 'tt * 'v +(* sessions *) +type ('pre,'post,'a) session = 'pre -> 'post * 'a -let return x p = p, x -let (>>=) m f p = let q,v = m p in f v q -let (>>) m n p = let q,_ = m p in n q +let return x = fun pre -> pre, x +let (>>=) m f = fun pre -> let mid,a = m pre in f a mid +let (>>) m n = fun pre -> let mid,_ = m pre in n mid (* polarized session types *) type req = Req @@ -28,109 +30,106 @@ type resp = Resp type cli = req * resp type serv = resp * req -type 'p cont = - Msg : ('v * 'p cont Channel.t) -> [`msg of 'r * 'v * 'p] cont -| Branch : 'br -> [`branch of 'r * 'br] cont -| Chan : (('pp, 'rr) sess * 'p cont Channel.t) -> [`deleg of 'r * ('pp, 'rr) sess * 'p] cont -and ('p, 'r) sess = 'p cont Channel.t * 'r +type 'p wrap = + Msg : ('v * 'p wrap Channel.t) -> [`msg of 'r * 'v * 'p] wrap +| Branch : 'br -> [`branch of 'r * 'br] wrap +| Chan : (('pp, 'rr) sess * 'p wrap Channel.t) -> [`deleg of 'r * ('pp, 'rr) sess * 'p] wrap +and ('p, 'q) sess = 'p wrap Channel.t * 'q (* service channels *) -type 'p channel = 'p cont Channel.t Channel.t +type 'p channel = 'p wrap Channel.t Channel.t let new_channel = Channel.create - -module SessionN = struct - let new_channel = Channel.create - - let close (get,set) ss = set ss Empty, () - - let send (get,set) v ss = - let ch,q = get ss and ch' = Channel.create () in - Channel.send ch (Msg(v,ch')); set ss (ch',q), () - - let recv (get,set) ss = - let (ch,q) = get ss in let Msg(v,ch') = Channel.receive ch in - set ss (ch',q), v - - let deleg_send (get0,set0) ~release:(get1,set1) ss = - let ch0,q1 = get0 ss and ch0' = Channel.create () in - let tt = set0 ss (ch0',q1) in - let ch1,q2 = get1 tt in - Channel.send ch0 (Chan((ch1,q2),ch0')); - set1 tt Empty, () - - let deleg_recv (get0,set0) ~bindto:(get1,set1) ss = - let ch0,q0 = get0 ss in - let Chan((ch1',q1),ch0') = Channel.receive ch0 in - let tt = set0 ss (ch0',q0) in - set1 tt (ch1',q1), () - - let accept ch ~bindto:(_,set) ss = - let ch' = Channel.receive ch in set ss (ch',(Resp,Req)), () - - let connect ch ~bindto:(_,set) ss = - let ch' = Channel.create () in Channel.send ch ch'; set ss (ch',(Req,Resp)), () - - - let inp : 'p 'r. 'p -> 'r -> ('p,'r) sess = fun x _ -> Obj.magic x - let out : 'p 'r. ('p,'r) sess -> 'p = Obj.magic - - let _branch_start : type br. - (([`branch of 'r2 * br], 'r1*'r2) sess, 'x, 'ss, 'xx) slot - -> (br * ('r1*'r2) -> ('ss, 'uu,'v) monad) - -> ('ss, 'uu, 'v) monad - = fun (get0,set0) f ss -> - let (ch,p) = get0 ss in - match Channel.receive ch with - | Branch(br) -> f (br,p) ss - - let _branch : - (([`branch of 'r2 * 'br], 'r1*'r2) sess, ('p,'r1*'r2) sess, 'ss, 'tt1) slot - -> 'p * ('r1*'r2) - -> ('tt1,'uu,'v) monad - -> ('ss, 'uu, 'v) monad - = fun (_,set1) (c,p) m ss -> - let tt1 = set1 ss (inp c p) - in m tt1 - - - let _select : type br p. - (([`branch of 'r1 * br],'r1*'r2) sess, (p,'r1*'r2) sess, 'ss, 'tt) slot - -> (p -> br) - -> ('ss, 'tt, 'v) monad = fun (get0,set0) f ss -> - let ch,p = get0 ss in - let k = Channel.create () in - Channel.send ch (Branch(f (out (k,p)))); - set0 ss (k,p), () - - let branch2 (s1,f1) (s2,f2) = - _branch_start s1 (function - | `left(p1),q -> _branch s1 (p1,q) (f1 ()) - | `right(p2),q -> _branch s2 (p2,q) (f2 ()) - : [`left of 'p1 | `right of 'p2] * 'x -> 'y) - - let select_left s = _select s (fun x -> `left(x)) - - let select_right s = _select s (fun x -> `right(x)) -end - -module Session0 = struct - let accept_ ch f v = run (fun v -> SessionN.accept ch ~bindto:_0 >> f v) v - let connect_ ch f v = run (fun v -> SessionN.connect ch ~bindto:_0 >> f v) v - - let close () = SessionN.close _0 - let recv () = SessionN.recv _0 - let send v = SessionN.send _0 v - - let branch2 = fun f g -> SessionN.branch2 (_0,f) (_0,g) - let select_left () = SessionN.select_left _0 - let select_right () = SessionN.select_right _0 - - let _select f = SessionN._select _0 f - let _branch_start f = SessionN._branch_start _0 f - let _branch wit m = SessionN._branch _0 wit m - -end +let accept_ ch f x = + let ch' = Channel.receive ch in + let ch' = (ch',(Resp,Req)) in + _run_internal (ch',all_empty) f x + +let connect_ ch f x = + let ch' = Channel.create () in + Channel.send ch ch'; + let ch' = (ch',(Req,Resp)) in + _run_internal (ch',all_empty) f x + +let close (get,set) = fun pre -> + set pre Empty, () + +let send (get,set) v = fun pre -> + let ch,q = get pre + and ch' = Channel.create () in + Channel.send ch (Msg(v,ch')); + set pre (ch',q), () + +let recv (get,set) = fun pre -> + let (ch,q) = get pre in + let Msg(v,ch') = Channel.receive ch in + set pre (ch',q), v + +let deleg_send (get0,set0) ~release:(get1,set1) = fun pre -> + let ch0,q1 = get0 pre + and ch0' = Channel.create () in + let mid = set0 pre (ch0',q1) in + let ch1,q2 = get1 mid in + Channel.send ch0 (Chan((ch1,q2),ch0')); + set1 mid Empty, () + +let deleg_recv (get0,set0) ~bindto:(get1,set1) = fun pre -> + let ch0,q0 = get0 pre in + let Chan((ch1',q1),ch0') = Channel.receive ch0 in + let mid = set0 pre (ch0',q0) in + set1 mid (ch1',q1), () + +let accept ch ~bindto:(_,set) = fun pre -> + let ch' = Channel.receive ch in + set pre (ch',(Resp,Req)), () + +let connect ch ~bindto:(_,set) = fun pre -> + let ch' = Channel.create () in + Channel.send ch ch'; + set pre (ch',(Req,Resp)), () + + +let inp : 'p 'r. 'p -> 'p wrap Channel.t = Obj.magic +let out : 'p 'r. 'p wrap Channel.t -> 'p = Obj.magic + +let _branch : type br. + (([`branch of 'r2 * br], 'r1*'r2) sess, empty, 'pre, 'mid) slot + -> (br * ('r1*'r2) -> ('mid, 'post,'v) session) + -> ('pre, 'post, 'v) session + = fun (get0,set0) f pre -> + let (ch,p) = get0 pre in + let mid = set0 pre Empty in + match Channel.receive ch with + | Branch(br) -> f (br,p) mid + +let _set_sess : + (empty, ('p,'r1*'r2) sess, 'pre, 'mid) slot + -> 'p * ('r1*'r2) + -> ('mid,'post,'v) session + -> ('pre, 'post, 'v) session + = fun (_,set1) (c,p) m ss -> + let tt1 = set1 ss ((inp c), p) + in m tt1 + + +let _select : type br p. + (([`branch of 'r1 * br],'r1*'r2) sess, (p,'r1*'r2) sess, 'ss, 'tt) slot + -> (p -> br) + -> ('ss, 'tt, 'v) session = fun (get0,set0) f ss -> + let ch,p = get0 ss in + let k = Channel.create () in + Channel.send ch (Branch(f (out k))); + set0 ss (k,p), () + +let branch ~left:((get1,set1),f1) ~right:((get2,set2),f2) = fun pre -> + let (ch,p) = get1 pre in + match Channel.receive ch with + | Branch(`left(ch')) -> f1 () (set1 pre (inp ch', p)) + | Branch(`right(ch')) -> f2 () (set2 pre (inp ch', p)) + +let select_left s = _select s (fun x -> `left(x)) + +let select_right s = _select s (fun x -> `right(x)) type 'a parse_result = [`Partial of (string option -> 'a parse_result) @@ -139,7 +138,7 @@ type 'a parse_result = module type Adapter = sig type raw_chan - type 'p net = raw_chan -> (('p, serv) sess * all_empty, all_empty, unit) monad + type 'p net = raw_chan -> (('p, serv) sess * all_empty, all_empty, unit) session val req : ('v -> string) -> 'p net -> [`msg of req * 'v * 'p] net val resp : (string -> 'v parse_result) -> 'p net -> [`msg of resp * 'v * 'p] net val sel : left:'p1 net -> right:'p2 net -> @@ -151,14 +150,7 @@ end module Syntax = struct let bind = (>>=) - module Session0 = struct - let _select = Session0._select - let _branch_start = Session0._branch_start - let _branch = Session0._branch - end - module SessionN = struct - let _select = SessionN._select - let _branch_start = SessionN._branch_start - let _branch = SessionN._branch - end + let _select = _select + let _branch = _branch + let _set_sess = _set_sess end diff --git a/lib/session.mli b/lib/session.mli index 9deb80a..c21eeec 100644 --- a/lib/session.mli +++ b/lib/session.mli @@ -1,25 +1,26 @@ (* empty slots *) -type empty = Empty +type empty type all_empty = empty * 'a as 'a (* lenses on slots *) -type ('a,'b,'ss,'tt) slot = ('ss -> 'a) * ('ss -> 'b -> 'tt) +type ('a,'b,'pre,'post) slot = ('pre -> 'a) * ('pre -> 'b -> 'post) -val _0 : ('a, 'b, ('a * 'ss), ('b * 'ss)) slot -val _1 : ('a, 'b, ('s0 * ('a * 'ss)), ('s0 * ('b * 'ss))) slot -val _2 : ('a, 'b, ('s0 * ('s1 * ('a * 'ss))), ('s0 * ('s1 * ('b * 'ss)))) slot -val _3 : ('a, 'b, ('s0 * ('s1 * ('s2 * ('a * 'ss)))), ('s0 * ('s1 * ('s2 * ('b * 'ss))))) slot +val s : ('a, 'b, ('a * 'pre), ('b * 'pre)) slot +val _0 : ('a, 'b, ('a * 'pre), ('b * 'pre)) slot +val _1 : ('a, 'b, ('s0 * ('a * 'pre)), ('s0 * ('b * 'pre))) slot +val _2 : ('a, 'b, ('s0 * ('s1 * ('a * 'pre))), ('s0 * ('s1 * ('b * 'pre)))) slot +val _3 : ('a, 'b, ('s0 * ('s1 * ('s2 * ('a * 'pre)))), ('s0 * ('s1 * ('s2 * ('b * 'pre))))) slot -(* parameterized monads *) -type ('x,'y,'a) monad +(* parameterized sessions *) +type ('x,'y,'a) session -val return : 'v -> ('x,'x,'v) monad -val (>>=) : ('x,'y,'a) monad -> ('a -> ('y, 'z, 'b) monad) -> ('x,'z,'b) monad -val (>>) : ('x,'y,'a) monad -> ('y,'z,'b) monad -> ('x,'z,'b) monad +val return : 'a -> ('pre,'pre,'a) session +val (>>=) : ('pre,'mid,'a) session -> ('a -> ('mid,'post,'b) session) -> ('pre,'post,'b) session +val (>>) : ('pre,'mid,'a) session -> ('mid,'post,'b) session -> ('pre,'post,'b) session -val run : ('a -> (all_empty, all_empty, 'b) monad) -> 'a -> 'b -val run_ : ((all_empty, all_empty, 'b) monad) -> 'b -val _run_internal : 'a -> ('b -> ('a, 'a, 'c) monad) -> 'b -> 'c +val run_ : (all_empty,all_empty,unit) session -> unit +val run : ('a -> (all_empty,all_empty,'b) session) -> 'a -> 'b +val _run_internal : 'a -> ('b -> ('a, 'a, 'c) session) -> 'b -> 'c (* channels *) type 'p channel @@ -34,92 +35,57 @@ type serv = resp * req type ('p, 'q) sess -module Session0 : sig - val accept_ : 'p channel -> ('v -> (('p,serv) sess * all_empty, all_empty, 'w) monad) -> 'v -> 'w - val connect_ : 'p channel -> ('v -> (('p,cli) sess * all_empty, all_empty, 'w) monad) -> 'v -> 'w +val accept_ : 'p channel -> ('a -> (('p,serv) sess * all_empty, all_empty, 'b) session) -> 'a -> 'b +val connect_ : 'p channel -> ('a -> (('p,cli) sess * all_empty, all_empty, 'b) session) -> 'a -> 'b - val close : unit -> (([`close], 'r1*'r2) sess * 'ss, empty * 'ss, unit) monad - val send : 'v -> (([`msg of 'r1 * 'v * 'p], 'r1*'r2) sess * 'ss, ('p, 'r1*'r2) sess * 'ss, unit) monad - val recv : unit -> (([`msg of 'r2 * 'v * 'p], 'r1*'r2) sess * 'ss, ('p, 'r1*'r2) sess * 'ss, 'v) monad +val accept : 'p channel -> bindto:(empty, ('p,serv) sess, 'pre, 'post) slot -> ('pre, 'post, unit) session +val connect : 'p channel -> bindto:(empty, ('p,cli) sess, 'pre, 'post) slot -> ('pre, 'post, unit) session - val branch2 - : (unit -> (('p1, 'r1*'r2) sess * 'ss, 'uu, 'a) monad) - -> (unit -> (('p2, 'r1*'r2) sess * 'ss, 'uu, 'a) monad) - -> (([`branch of 'r2 * [`left of 'p1 | `right of 'p2]], 'r1*'r2) sess * 'ss, 'uu, 'a) monad +val close : (([`close], 'r1*'r2) sess, empty, 'pre, 'post) slot -> ('pre, 'post, unit) session +val send : (([`msg of 'r1 * 'v * 'p], 'r1*'r2) sess, ('p, 'r1*'r2) sess, 'pre, 'post) slot -> 'v -> ('pre, 'post, unit) session +val recv : (([`msg of 'r2 * 'v * 'p], 'r1*'r2) sess, ('p, 'r1*'r2) sess, 'pre, 'post) slot -> ('pre, 'post, 'v) session - val select_left - : unit -> (([`branch of 'r1 * [>`left of 's1]], 'r1*'r2) sess * 'ss, ('s1, 'r1*'r2) sess * 'ss, unit) monad +val branch + : left:(([`branch of 'r2 * [`left of 'p1 | `right of 'p2]], 'r1*'r2) sess, ('p1, 'r1*'r2) sess, 'pre, 'mid1) slot * (unit -> ('mid1, 'post, 'a) session) + -> right:(([`branch of 'r2 * [`left of 'p1 | `right of 'p2]], 'r1*'r2) sess, ('p2, 'r1*'r2) sess, 'pre, 'mid2) slot * (unit -> ('mid2, 'post, 'a) session) + -> ('pre, 'post, 'a) session - val select_right - : unit -> (([`branch of 'r1 * [>`right of 's2]], 'r1*'r2) sess * 'ss, ('s2, 'r1*'r2) sess * 'ss, unit) monad +val select_left + : (([`branch of 'r1 * [>`left of 'p1]], 'r1*'r2) sess, + ('p1, 'r1*'r2) sess, 'pre, 'post) slot + -> ('pre, 'post, unit) session - val _select - : ('p -> 'br) - -> (([`branch of 'r1 * 'br],'r1*'r2) sess * 'ss, ('p,'r1*'r2) sess * 'ss, unit) monad - - val _branch_start - : ('br * ('r1*'r2) -> (([`branch of 'r2 * 'br], 'r1*'r2) sess * 'ss, 'uu,'v) monad) - -> (([`branch of 'r2 * 'br], 'r1*'r2) sess * 'ss, 'uu, 'v) monad - - val _branch - : 'p * ('r1*'r2) - -> (('p,'r1*'r2) sess * 'ss, 'uu, 'v) monad - -> (([`branch of 'r2 * 'br], 'r1*'r2) sess * 'ss, 'uu, 'v) monad -end - - -module SessionN : sig - - val accept : 'p channel -> bindto:(empty, ('p,serv) sess, 'ss, 'tt) slot -> ('ss, 'tt, unit) monad - val connect : 'p channel -> bindto:(empty, ('p,cli) sess, 'ss, 'tt) slot -> ('ss, 'tt, unit) monad - - val close : (([`close], 'r1*'r2) sess, empty, 'ss, 'tt) slot -> ('ss, 'tt, unit) monad - val send : (([`msg of 'r1 * 'v * 'p], 'r1*'r2) sess, ('p, 'r1*'r2) sess, 'ss, 'tt) slot -> 'v -> ('ss, 'tt, unit) monad - val recv : (([`msg of 'r2 * 'v * 'p], 'r1*'r2) sess, ('p, 'r1*'r2) sess, 'ss, 'tt) slot -> ('ss, 'tt, 'v) monad - - val branch2 - : (([`branch of 'r2 * [`left of 'p1 | `right of 'p2]], 'r1*'r2) sess, ('p1, 'r1*'r2) sess, 'ss, 'tt1) slot * (unit -> ('tt1, 'uu, 'a) monad) - -> (([`branch of 'r2 * [`left of 'p1 | `right of 'p2]], 'r1*'r2) sess, ('p2, 'r1*'r2) sess, 'ss, 'tt2) slot * (unit -> ('tt2, 'uu, 'a) monad) - -> ('ss, 'uu, 'a) monad - - val select_left - : (([`branch of 'r1 * [>`left of 's1]], 'r1*'r2) sess, - ('s1, 'r1*'r2) sess, 'ss, 'tt) slot - -> ('ss, 'tt, unit) monad - - val select_right - : (([`branch of 'r1 * [>`right of 's2]], 'r1*'r2) sess, - ('s2, 'r1*'r2) sess, 'ss, 'tt) slot - -> ('ss, 'tt, unit) monad +val select_right + : (([`branch of 'r1 * [>`right of 'p2]], 'r1*'r2) sess, + ('p2, 'r1*'r2) sess, 'pre, 'post) slot + -> ('pre, 'post, unit) session - val _select - : (([`branch of 'r1 * 'br],'r1*'r2) sess, ('p,'r1*'r2) sess, 'ss, 'tt) slot - -> ('p -> 'br) - -> ('ss, 'tt, unit) monad - - val _branch_start - : (([`branch of 'r2 * 'br], 'r1*'r2) sess, 'x, 'ss, 'xx) slot - -> ('br * ('r1*'r2) -> ('ss, 'uu,'v) monad) - -> ('ss, 'uu, 'v) monad +val _select + : (([`branch of 'r1 * 'br],'r1*'r2) sess, ('p,'r1*'r2) sess, 'pre, 'post) slot + -> ('p -> ([>] as 'br)) + -> ('pre, 'post, unit) session - val _branch - : (([`branch of 'r2 * 'br], 'r1*'r2) sess, ('p,'r1*'r2) sess, 'ss, 'tt1) slot - -> 'p * ('r1*'r2) - -> ('tt1, 'uu, 'v) monad - -> ('ss, 'uu, 'v) monad +val _branch + : (([`branch of 'r2 * 'br], 'r1*'r2) sess, empty, 'pre, 'mid) slot + -> ('br * ('r1*'r2) -> ('mid, 'post,'v) session) + -> ('pre, 'post, 'v) session - val deleg_send - : (([`deleg of 'r1 * ('pp, 'rr) sess * 'p], 'r1*'r2) sess, ('p, 'r1*'r2) sess, 'ss, 'tt) slot - -> release:(('pp, 'rr) sess, empty, 'tt, 'uu) slot - -> ('ss, 'uu, unit) monad +val _set_sess + : (empty, ('p,'r1*'r2) sess, 'pre, 'mid) slot + -> 'p * ('r1*'r2) + -> ('mid, 'post, 'v) session + -> ('pre, 'post, 'v) session - val deleg_recv - : (([`deleg of 'r2 * ('pp, 'rr) sess * 'p], 'r1*'r2) sess, ('p, 'r1*'r2) sess, 'ss, 'tt) slot - -> bindto:(empty, ('pp, 'rr) sess, 'tt, 'uu) slot - -> ('ss, 'uu, unit) monad +val deleg_send + : (([`deleg of 'r1 * ('pp, 'qq) sess * 'p], 'r1*'r2) sess, ('p, 'r1*'r2) sess, 'pre, 'mid) slot + -> release:(('pp, 'qq) sess, empty, 'mid, 'post) slot + -> ('pre, 'post, unit) session -end +val deleg_recv + : (([`deleg of 'r2 * ('pp, 'qq) sess * 'p], 'r1*'r2) sess, ('p, 'r1*'r2) sess, 'pre, 'mid) slot + -> bindto:(empty, ('pp, 'qq) sess, 'mid, 'post) slot + -> ('pre, 'post, unit) session type 'a parse_result = [`Partial of (string option -> 'a parse_result) (* `Partial f. invariant: (f None) may not return Partial *) @@ -128,7 +94,7 @@ type 'a parse_result = module type Adapter = sig type raw_chan - type 'p net = raw_chan -> (('p, serv) sess * all_empty, all_empty, unit) monad + type 'p net = raw_chan -> (('p, serv) sess * all_empty, all_empty, unit) session val req : ('v -> string) -> 'p net -> [`msg of req * 'v * 'p] net val resp : (string -> 'v parse_result) -> 'p net -> [`msg of resp * 'v * 'p] net val sel : left:'p1 net -> right:'p2 net -> @@ -139,36 +105,20 @@ module type Adapter = sig end module Syntax : sig - val bind : ('x,'y,'a) monad -> ('a -> ('y, 'z, 'b) monad) -> ('x,'z,'b) monad - module Session0 : sig - val _select - : ('p -> 'br) - -> (([`branch of 'r1 * 'br],'r1*'r2) sess * 'ss, ('p,'r1*'r2) sess * 'ss, unit) monad - - val _branch_start - : ('br * ('r1*'r2) -> (([`branch of 'r2 * 'br], 'r1*'r2) sess * 'ss, 'uu,'v) monad) - -> (([`branch of 'r2 * 'br], 'r1*'r2) sess * 'ss, 'uu, 'v) monad - - val _branch - : 'p * ('r1*'r2) - -> (('p,'r1*'r2) sess * 'ss, 'uu, 'v) monad - -> (([`branch of 'r2 * 'br], 'r1*'r2) sess * 'ss, 'uu, 'v) monad - end - module SessionN : sig - val _select - : (([`branch of 'r1 * 'br],'r1*'r2) sess, ('p,'r1*'r2) sess, 'ss, 'tt) slot - -> ('p -> 'br) - -> ('ss, 'tt, unit) monad - - val _branch_start - : (([`branch of 'r2 * 'br], 'r1*'r2) sess, 'x, 'ss, 'xx) slot - -> ('br * ('r1*'r2) -> ('ss, 'uu,'v) monad) - -> ('ss, 'uu, 'v) monad + val bind : ('x,'y,'a) session -> ('a -> ('y, 'z, 'b) session) -> ('x,'z,'b) session + val _select + : (([`branch of 'r1 * 'br],'r1*'r2) sess, ('p,'r1*'r2) sess, 'pre, 'post) slot + -> ('p -> ([>] as 'br)) + -> ('pre, 'post, unit) session + + val _branch + : (([`branch of 'r2 * 'br], 'r1*'r2) sess, empty, 'pre, 'mid) slot + -> ('br * ('r1*'r2) -> ('mid, 'post,'v) session) + -> ('pre, 'post, 'v) session - val _branch - : (([`branch of 'r2 * 'br], 'r1*'r2) sess, ('p,'r1*'r2) sess, 'ss, 'tt1) slot - -> 'p * ('r1*'r2) - -> ('tt1, 'uu, 'v) monad - -> ('ss, 'uu, 'v) monad - end + val _set_sess + : (empty, ('p,'r1*'r2) sess, 'pre, 'mid) slot + -> 'p * ('r1*'r2) + -> ('mid, 'post, 'v) session + -> ('pre, 'post, 'v) session end diff --git a/lib/unixAdapter.ml b/lib/unixAdapter.ml index acdffb1..7997934 100644 --- a/lib/unixAdapter.ml +++ b/lib/unixAdapter.ml @@ -3,7 +3,7 @@ open Session let bufsize = 4096 type raw_chan = {in_ch:in_channel; in_buf:string; out_ch:out_channel} -type 'p net = raw_chan -> (('p, serv) sess * all_empty, all_empty, unit) monad +type 'p net = raw_chan -> (('p, serv) sess * all_empty, all_empty, unit) session let consume (read:string->'v parse_result) {in_ch;in_buf} = let consume_buf : string -> 'v parse_result = function @@ -25,7 +25,7 @@ let consume (read:string->'v parse_result) {in_ch;in_buf} = let req : 'v 'p . ('v -> string) -> 'p net -> [`msg of req * 'v * 'p] net = fun print cont ({out_ch} as ch) -> - Session0.recv () >>= fun v -> + recv _0 >>= fun v -> (output_string out_ch (print v); flush out_ch; cont ch) let resp @@ -35,29 +35,29 @@ let resp match v with | None -> assert false (*FIXME:EOF*) | Some(v) -> - Session0.send v >> + send _0 v >> cont ch let sel : 'p1 'p2. left:'p1 net -> right:'p2 net -> [`branch of req * [`left of 'p1|`right of 'p2]] net = fun ~left ~right ch -> - Session0.branch2 (fun () -> left ch) - (fun () -> right ch) + branch (_0, fun () -> left ch) + (_0, fun () -> right ch) let bra = fun ~left:(read,left) ~right ({in_ch;in_buf} as ch) -> let v, in_buf = consume read ch in let ch = {ch with in_buf} in match v with - | Some v -> Session0.select_left () >> Session0.send v >> left ch - | None -> Session0.select_right () >> right ch + | Some v -> select_left _0 >> send _0 v >> left ch + | None -> select_right _0 >> right ch let cls : [`close] net = fun {in_ch;out_ch;in_buf} -> close_in_noerr in_ch; close_out_noerr out_ch; (* assert in_buf="" *) - Session0.close () + close _0 module TcpSession = struct let new_channel adapter hostport = @@ -75,6 +75,6 @@ module TcpSession = struct in let in_ch,out_ch = connect () in let ch = Session.new_channel () in - ignore @@ Thread.create (Session0.accept_ ch adapter) {in_ch;out_ch;in_buf=""}; + ignore @@ Thread.create (fun () -> run_ (accept ch ~bindto:_0 >> adapter {in_ch;out_ch;in_buf=""})) (); ch end diff --git a/net/dsession.ml b/net/dsession.ml index 7fcec7f..75f0b22 100644 --- a/net/dsession.ml +++ b/net/dsession.ml @@ -16,11 +16,11 @@ type empty = Empty type empty_three = empty * (empty * (empty * empty)) type empty_four = empty * empty_three -let return a pre = pre, L a +let return a pre = pre, a let (>>=) f g pre = let mid, la = f pre in g la mid let (>>) f g pre = let mid, _ = f pre in g mid -let run f = unlin @@ snd @@ f () (Empty, (Empty, (Empty, (Empty, Empty)))) +let run f = snd @@ f () (Empty, (Empty, (Empty, (Empty, Empty)))) type req and resp type cli = req * resp and serv = resp * req @@ -68,7 +68,7 @@ module type S = sig val close : ?_closer:'c Closer.t -> (([`close], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, unit lin) lmonad + -> ('pre, 'post, unit) lmonad val send : ?_sender:('c, 'v) Sender.t @@ -78,7 +78,7 @@ module type S = sig val receive : ?_receiver:('c, 'v) Receiver.t -> (([`msg of 'r2 * 'v * 'p], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('v data * ('p, 'r1*'r2, 'c) dsess) lin) lmonad + -> ('pre, 'post, 'v data * ('p, 'r1*'r2, 'c) dsess) lmonad val select : ?_sender:('c, [>] as 'br) Sender.t @@ -89,7 +89,7 @@ module type S = sig val branch : ?_receiver:('c, [>] as 'br) Receiver.t -> (([`branch of 'r2 * 'br], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, 'br lin) lmonad + -> ('pre, 'post, 'br) lmonad val deleg_send : ?_sender:('c , ('pp,'qq,'cc) sess) Sender.t @@ -100,7 +100,7 @@ module type S = sig val deleg_recv : ?_receiver:('c, ('pp, 'qq, 'cc) sess) Receiver.t -> (([`deleg of 'r2 * ('pp, 'qq, 'cc) dsess * 'p], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, (('pp,'qq,'cc) dsess * ('p,'r1*'r2,'c) dsess) lin) lmonad + -> ('pre, 'post, ('pp,'qq,'cc) dsess * ('p,'r1*'r2,'c) dsess) lmonad end @@ -179,10 +179,10 @@ end) : S = struct let close : 'pre 'r1 'r2 'c 'post. ?_closer:'c Closer.t -> (([`close], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, unit lin) lmonad = + -> ('pre, 'post, unit) lmonad = fun ?_closer (get,set) pre -> Closer.unpack (instance _closer) (unlin @@ get pre); - set pre Empty, L () + set pre Empty, () let send : 'v 'r1 'p 'r2 'c 'pre 'post. ?_sender:('c,'v) Sender.t @@ -196,10 +196,10 @@ end) : S = struct let receive : 'r2 'v 'p 'r1 'c 'pre 'post. ?_receiver:('c,'v) Receiver.t -> (([`msg of 'r2 * 'v * 'p], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('v data * ('p, 'r1*'r2, 'c) dsess) lin) lmonad = + -> ('pre, 'post, 'v data * ('p, 'r1*'r2, 'c) dsess) lmonad = fun ?_receiver (get,set) pre -> let s = unlin @@ get pre in - set pre Empty, L (W (Receiver.unpack (instance _receiver) s), L s) + set pre Empty, (W (Receiver.unpack (instance _receiver) s), L s) let select : 'p 'r2 'r1 'c 'pre 'post. ?_sender:('c, [>] as 'br) Sender.t @@ -214,10 +214,10 @@ end) : S = struct let branch : 'r2 'r1 'c 'pre 'post. ?_receiver:('c,[>] as 'br) Receiver.t -> (([`branch of 'r2 * 'br], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, 'br lin) lmonad = + -> ('pre, 'post, 'br) lmonad = fun ?_receiver (get,set) pre -> let s = unlin @@ get pre in - set pre Empty, L (Receiver.unpack (instance _receiver) s) + set pre Empty, (Receiver.unpack (instance _receiver) s) let deleg_send : 'pp 'qq 'cc 'mid 'post 'r1 'r2 'c 'pre. ?_sender:('c, ('pp, 'qq, 'cc) sess) Sender.t @@ -234,11 +234,11 @@ end) : S = struct let deleg_recv : 'r2 'p 'r1 'c 'pre 'post 'pp 'qq 'cc. ?_receiver:('c, ('pp, 'qq, 'cc) sess) Receiver.t -> (([`deleg of 'r2 * ('pp, 'qq, 'cc) dsess * 'p], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, (('pp,'qq,'cc) dsess * ('p,'r1*'r2,'c) dsess) lin) lmonad = + -> ('pre, 'post, ('pp,'qq,'cc) dsess * ('p,'r1*'r2,'c) dsess) lmonad = fun ?_receiver (get,set) pre -> let s = unlin @@ get pre in let t = Receiver.unpack (instance _receiver) s in - set pre Empty, L (L t, L s) + set pre Empty, (L t, L s) end @@ -261,7 +261,7 @@ module Syntax = struct set pre (L v), () let __takeval_raw (get,set) pre = - set pre Empty, match get pre with L a -> a + set pre Empty, get pre let __mkbindfun f = f let __run m pre = (>>=) (m pre) (fun (_,L a) -> a) diff --git a/net/dsession.mli b/net/dsession.mli index 0c4a5cb..39295cc 100644 --- a/net/dsession.mli +++ b/net/dsession.mli @@ -13,15 +13,15 @@ type empty type empty_three = empty * (empty * (empty * empty)) type empty_four = empty * empty_three -val return : 'a -> ('pre, 'pre, 'a lin) lmonad -val (>>=) : ('pre, 'mid, 'a lin) lmonad - -> ('a lin -> ('mid, 'post, 'b lin) lmonad) lbind - -> ('pre, 'post, 'b lin) lmonad -val (>>) : ('pre, 'mid, unit lin) lmonad - -> ('mid, 'post, 'b lin) lmonad - -> ('pre, 'post, 'b lin) lmonad +val return : 'a -> ('pre, 'pre, 'a) lmonad +val (>>=) : ('pre, 'mid, 'a) lmonad + -> ('a -> ('mid, 'post, 'b) lmonad) lbind + -> ('pre, 'post, 'b) lmonad +val (>>) : ('pre, 'mid, unit) lmonad + -> ('mid, 'post, 'b) lmonad + -> ('pre, 'post, 'b) lmonad -val run : (unit -> (empty_four, empty_four, unit lin) lmonad) -> unit +val run : (unit -> (empty_four, empty_four, unit) lmonad) -> unit type req and resp type cli = req * resp and serv = resp * req @@ -69,7 +69,7 @@ module type S = sig val close : ?_closer:'c Closer.t -> (([`close], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, unit lin) lmonad + -> ('pre, 'post, unit) lmonad val send : ?_sender:('c, 'v) Sender.t @@ -79,7 +79,7 @@ module type S = sig val receive : ?_receiver:('c, 'v) Receiver.t -> (([`msg of 'r2 * 'v * 'p], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, ('v data * ('p, 'r1*'r2, 'c) dsess) lin) lmonad + -> ('pre, 'post, 'v data * ('p, 'r1*'r2, 'c) dsess) lmonad val select : ?_sender:('c, [>] as 'br) Sender.t @@ -90,7 +90,7 @@ module type S = sig val branch : ?_receiver:('c, [>] as 'br) Receiver.t -> (([`branch of 'r2 * 'br], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, 'br lin) lmonad + -> ('pre, 'post, 'br) lmonad val deleg_send : ?_sender:('c , ('pp,'qq,'cc) sess) Sender.t @@ -101,7 +101,7 @@ module type S = sig val deleg_recv : ?_receiver:('c, ('pp, 'qq, 'cc) sess) Receiver.t -> (([`deleg of 'r2 * ('pp, 'qq, 'cc) dsess * 'p], 'r1*'r2, 'c) dsess, empty, 'pre, 'post) slot - -> ('pre, 'post, (('pp,'qq,'cc) dsess * ('p,'r1*'r2,'c) dsess) lin) lmonad + -> ('pre, 'post, ('pp,'qq,'cc) dsess * ('p,'r1*'r2,'c) dsess) lmonad end @@ -116,9 +116,9 @@ end include S module Syntax : sig - val bind : ('pre, 'mid, 'a lin) lmonad - -> ('a lin -> ('mid, 'post, 'b lin) lmonad) lbind - -> ('pre, 'post, 'b lin) lmonad + val bind : ('pre, 'mid, 'a) lmonad + -> ('a -> ('mid, 'post, 'b) lmonad) lbind + -> ('pre, 'post, 'b) lmonad module Internal : sig val __bind_raw : ('pre,'mid,'a) lmonad -> ('a -> ('mid,'post,'b) lmonad) -> ('pre,'post,'b) lmonad @@ -127,7 +127,7 @@ module Syntax : sig val __mkbindfun : ('a -> ('pre,'post,'b) lmonad) -> ('a -> ('pre, 'post, 'b) lmonad) lbind val __putval_raw : (empty,'a lin,'pre,'post) slot -> 'a -> ('pre,'post,unit) lmonad - val __takeval_raw : ('a lin,empty,'pre,'post) slot -> ('pre,'post,'a) lmonad + val __takeval_raw : ('a,empty,'pre,'post) slot -> ('pre,'post,'a) lmonad end end diff --git a/ppx/ppx_session.ml b/ppx/ppx_session.ml index 8f3b787..f717c92 100644 --- a/ppx/ppx_session.ml +++ b/ppx/ppx_session.ml @@ -123,12 +123,6 @@ let lin_pattern oldpat = pconstr ~loc:ppat_loc "W" [pat] in let newpat = traverse wrap_datapat replace_linpat oldpat in - let newpat = - if is_linpat oldpat then - newpat (* not to duplicate Lin pattern *) - else - pconstr ~loc:ppat_loc "L" [newpat] - in newpat, List.rev !lin_vars in let newpat,lin_vars = wrap oldpat in