Session type implementation with Janestreet Async. https://github.com/janestreet/async/
Last active
January 1, 2016 19:29
-
-
Save keigoi/8190749 to your computer and use it in GitHub Desktop.
Session type implementation using Janestreet Async
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
session.cmi : | |
example.cmo : session.cmi | |
example.cmx : session.cmx | |
session.cmo : session.cmi | |
session.cmx : session.cmi |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
*.cm[ioxat] | |
*.cmxa | |
*.cmti | |
*.o | |
*.annot | |
test.* | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
include Session;; | |
let p () = | |
send _0 1234 >> | |
recv _0 >>= fun str -> | |
print_endline str; | |
close _0 >> | |
ret () | |
(* | |
val p : | |
unit -> | |
((('a, 'b, ('a, int, ('b, string, finish) shot) shot) chan, 'c) cons, | |
(empty, 'c) cons, unit) | |
monad = <fun> | |
*) | |
(* | |
val p : | |
unit -> | |
(((int, (string, 'a) recv) send, 'b) cons, ('a, 'b) cons, unit) monad | |
*) | |
let q () = | |
recv _0 >>= fun i -> | |
send _0 (string_of_int (i*2)) >> | |
close _0 >> | |
ret () | |
(* | |
val q : | |
unit -> | |
((('a, 'b, ('b, int, ('a, string, finish) shot) shot) chan, 'c) cons, | |
(empty, 'c) cons, unit) | |
monad | |
*) | |
let r () = | |
fork _0 (q ()) >> | |
p () | |
(* | |
val r : | |
unit -> | |
((empty, (empty, 'a) cons) cons, (empty, (empty, 'a) cons) cons, unit) | |
monad | |
*) | |
(* output: | |
2468 | |
*) | |
let p2 () = | |
send _0 7777 >> | |
recv_slot _0 _1 >> | |
recv _1 >>= fun str -> | |
print_endline str; | |
close _0 >> | |
close _1 | |
let q2 () = | |
recv _0 >>= fun v -> | |
send_new_chan _0 _1 >> | |
send _1 (string_of_int (v - 1111)) >> | |
close _0 >> | |
close _1 | |
let r2 () = | |
fork _0 (q2 ()) >> | |
p2 () | |
(* output: | |
6666 | |
*) | |
let rec p3 n = | |
if n>10 then | |
select_right _0 >> close _0 | |
else | |
select_left _0 >> | |
send _0 n >> | |
recv _0 >>= fun str -> | |
print_endline str; | |
p3 (n+1) | |
let rec q3 () = | |
branch _0 | |
(_0,fun _ -> | |
recv _0 >>= fun x -> | |
send _0 (string_of_int x) >> | |
q3 ()) | |
(_0,fun _ -> | |
close _0) | |
let r3 () = | |
fork _0 (q3 ()) >> | |
p3 1 | |
(* output: | |
1 | |
2 | |
3 | |
4 | |
5 | |
6 | |
7 | |
8 | |
9 | |
10 | |
*) | |
let r4 () = | |
run_routine | |
_0 | |
Routine.(send "Hello, " >> recv >>= fun x -> print_endline x; close) >> | |
recv _0 >>= fun x -> | |
send _0 (x ^ "World!") >> | |
close _0 | |
(* output: | |
Hello, World! | |
*) | |
let r5 () = | |
let proc = | |
recv _0 >>= fun i -> | |
Printf.printf "My no. is %d.\n" i; | |
flush_all(); | |
close _0 | |
in | |
let rec duplicate = function | |
| 0 -> ret () | |
| n -> | |
fork _1 proc >> | |
LinList.put _0 _1 >> | |
duplicate (n-1) | |
in | |
let rec send_repeat cnt = | |
LinList.take | |
(_0, _1, fun _ -> | |
send _1 cnt >> | |
close _1 >> | |
send_repeat (cnt+1)) | |
(_0, fun _ -> | |
ret ()) | |
in | |
LinList.nil _0 >> | |
duplicate 10 >> | |
send_repeat 0 | |
let _ = run (r () >> r2 () >> r3 () >> r4 () >> r5 ()) | |
let _ = Async.Std.Scheduler.go() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
OCAMLC=ocamlfind ocamlc -g -rectypes -thread -package async | |
OCAMLOPT=ocamlfind ocamlopt -g -rectypes -thread -package async | |
OCAMLMKTOP=ocamlfind ocamlmktop -g -rectypes -thread -package async | |
OCAMLDEP=ocamlfind ocamldep | |
INCLUDES= # all relevant -I options here | |
OCAMLFLAGS=$(INCLUDES) # add other options for ocamlc here | |
OCAMLOPTFLAGS=$(INCLUDES) # add other options for ocamlopt here | |
CMI=session.cmi | |
BYTE_OBJS=session.cmo example.cmo | |
NATIVE_OBJS=$(BYTE_OBJS:%.cmo=%.cmx) | |
all: test.byte | |
test.native: $(NATIVE_OBJS) $(CMI) | |
$(OCAMLOPT) -linkpkg -o test.native $(OCAMLFLAGS) $(NATIVE_OBJS) | |
test.byte: $(BYTE_OBJS) $(CMI) | |
$(OCAMLC) -linkpkg -o test.byte $(OCAMLFLAGS) $(BYTE_OBJS) | |
test.top: $(BYTE_OBJS) $(CMI) | |
$(OCAMLMKTOP) -linkpkg -o test.top $(OCAMLFLAGS) $(BYTE_OBJS) | |
# Common rules | |
.SUFFIXES: .ml .mli .cmo .cmi .cmx | |
.ml.cmo: | |
$(OCAMLC) $(OCAMLFLAGS) -c $< | |
.mli.cmi: | |
$(OCAMLC) $(OCAMLFLAGS) -c $< | |
.ml.cmx: | |
$(OCAMLOPT) $(OCAMLOPTFLAGS) -c $< | |
# Clean up | |
clean: | |
rm -f test.byte test.native | |
rm -f *.cm[ioaxt] *.cmax *.cmti *.o *.annot | |
# Dependencies | |
depend: | |
$(OCAMLDEP) $(INCLUDES) *.mli *.ml > .depend | |
include .depend | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Ivar = Async_core.Raw_ivar | |
module Scheduler = Async.Std.Scheduler | |
type ('a,'b,'p,'q) idx = ('p -> 'a) * ('p -> 'b -> 'q) | |
type ('hd, 'tl) cons = 'hd * 'tl | |
type empty = Empty | |
type all_empty = empty * all_empty | |
let _0 = (fun (a0,_) -> a0), (fun (_,a) b0 -> (b0,a)) | |
let _1 = (fun (_,(a1,_)) -> a1), (fun (a0,(_,a)) b1 -> (a0,(b1,a))) | |
let _2 = (fun (_,(_,(a2,_))) -> a2), (fun (a0,(a1,(_,a))) b2 -> (a0,(a1,(b2,a)))) | |
let _3 = (fun (_,(_,(_,(a3,_)))) -> a3), (fun (a0,(a1,(a2,(_,a)))) b3 -> (a0,(a1,(a2,(b3,a))))) | |
let succ (get,set) = (fun (_,a) -> get a), (fun (a0,a) bn -> (a0,set a bn)) | |
type ('p,'q,'a) monad = 'p -> ('q * 'a) Ivar.t | |
let ret a p = Ivar.create_full (p, a) | |
let (>>=) m f p = | |
let ret = Ivar.create () in | |
Ivar.upon (m p) (fun (q, x) -> Ivar.connect ~bind_rhs:(f x q) ~bind_result:ret); | |
ret | |
let (>>) m n = m >>= (fun _ -> n) | |
let slide m (p0,p) = | |
let ret = Ivar.create () in | |
Ivar.upon (m p) (fun (q, x) -> Ivar.fill ret ((p0,q),x)); | |
ret | |
let rec all_empty = Empty, all_empty | |
let run m = | |
Async.Std.Deferred.create | |
(fun iv -> Ivar.upon (m all_empty) (fun (_, x) -> Async.Std.Ivar.fill iv x)) | |
type pos = Pos and neg = Neg | |
type ('s,'v,'k) shot = Shot of 's * 'v * 'k Ivar.t | |
type ('s,'c,'k) pass = Pass of 's * 'c * 'k Ivar.t | |
type ('s,'k1,'k2) branch = BranchLeft of 's * 'k1 Ivar.t | BranchRight of 's * 'k2 Ivar.t | |
type finish = unit | |
type ('s,'t,'v,'w,'k) yield = ('s,'v,('t,'w,'k)shot)shot | |
type ('s,'t,'k) channel = Chan of 's * 't * 'k Ivar.t | |
let send (get,set) v p = | |
let Chan(s,t,c) = get p in | |
let c' = Ivar.create () in | |
Ivar.fill c (Shot(s,v,c')); | |
Ivar.create_full (set p (Chan(s,t,c')), ()) | |
let recv (get,set) p = | |
let Chan(s,t,c) = get p in | |
let ret = Ivar.create () in | |
Ivar.upon c (fun (Shot(_, v, c')) -> Ivar.fill ret (set p (Chan(s,t,c')), v)); | |
ret | |
let close (get,set) p = | |
Ivar.create_full (set p Empty, ()) | |
let send_slot (get0,set0) (get1,set1) p = | |
let e, q = get1 p, set1 p Empty in | |
let Chan(s,t,c) = get0 q in | |
let c' = Ivar.create () in | |
Ivar.fill c (Pass(s,e,c')); | |
Ivar.create_full (set0 q (Chan(s,t,c')), ()) | |
let send_chan = send_slot | |
let recv_slot (get0,set0) (get1,set1) p = | |
let Chan(s,t,c) = get0 p in | |
let ret = Ivar.create () in | |
Ivar.upon c (fun (Pass(_,e,c')) -> Ivar.fill ret (set1 (set0 p (Chan(s,t,c'))) e, ())); | |
ret | |
let recv_chan = recv_slot | |
let send_new_chan (get0,set0) (get1,set1) p = | |
let Chan(s,t,c) = get0 p in | |
let c' = Ivar.create () in | |
let cc = Ivar.create () in | |
let e = Pass(s,Chan(t,s,cc),c') in | |
Ivar.fill c e; | |
Ivar.create_full (set1 (set0 p (Chan(s,t,c'))) (Chan(s,t,cc)), ()) | |
let select_left (get,set) p = | |
let Chan(s,t,c) = get p in | |
let c' = Ivar.create () in | |
Ivar.fill c (BranchLeft(s,c')); | |
Ivar.create_full (set p (Chan(s,t,c')), ()) | |
let select_right (get,set) p = | |
let Chan(s,t,c) = get p in | |
let c' = Ivar.create () in | |
Ivar.fill c (BranchRight(s,c')); | |
Ivar.create_full (set p (Chan(s,t,c')), ()) | |
let branch (get0,set0) ((get1,set1),f1) ((get2,set2),f2) p = | |
let Chan(s,t,c), q = get0 p, set0 p Empty in | |
let ret = Ivar.create () in | |
Ivar.upon c | |
(function | |
| BranchLeft(_,c') -> | |
Ivar.connect ~bind_rhs:(f1 () (set1 q (Chan(s,t,c')))) ~bind_result:ret | |
| BranchRight(_,c') -> | |
Ivar.connect ~bind_rhs:(f2 () (set2 q (Chan(s,t,c')))) ~bind_result:ret | |
); | |
ret | |
let fork (get,set) m p = | |
let ivar = Ivar.create () in | |
Scheduler.within (fun _ -> ignore (m (Chan(Neg,Pos,ivar),all_empty))); | |
Ivar.create_full (set p (Chan(Pos,Neg,ivar)), ()) | |
module LinList = struct | |
let nil (_,set) p = Ivar.create_full (set p [], ()) | |
let put (get0,set0) (get1,set1) p = | |
let q = set1 p Empty in | |
Ivar.create_full (set0 q (get1 p::get0 q), ()) | |
let take ((get0,set0),(get1,set1),f0) ((_,set2),f2) p = | |
match get0 p with | |
| x::xs -> | |
let ret = Ivar.create () in | |
Ivar.upon (f0 () (set1 (set0 p xs) x)) (Ivar.fill ret); | |
ret | |
| [] -> f2 () (set2 p Empty) | |
end | |
module Routine = struct | |
let send v (Chan(s,t,c)) = | |
let c' = Ivar.create () in | |
Ivar.fill c (Shot(s,v,c')); | |
Ivar.create_full (Chan(s,t,c'),()) | |
let recv (Chan(s,t,c)) = | |
let ret = Ivar.create () in | |
Ivar.upon c (fun (Shot(_,v,c')) -> Ivar.fill ret (Chan(s,t,c'),v)); | |
ret | |
let close (Chan(_,_,_)) = | |
Ivar.create_full (Empty, ()) | |
let yield v = send v >> recv | |
end | |
let run_routine (get,set) m p = | |
let c = Ivar.create () in | |
m (Chan(Neg,Pos,c)); | |
Ivar.create_full (set p (Chan(Pos,Neg,c)), ()) | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
type ('an,'bn,'a,'b) idx | |
type (+'hd, +'tl) cons | |
type empty | |
type all_empty = (empty, 'a) cons as 'a | |
val _0 : ('a0, 'b0, ('a0,'a) cons, ('b0,'a) cons) idx | |
val _1 : ('a1, 'b1, ('a0,('a1,'a) cons) cons, ('a0,('b1,'a) cons) cons) idx | |
val _2 : ('a2, 'b2, ('a0,('a1,('a2,'a) cons) cons) cons, ('a0,('a1,('b2,'a) cons) cons) cons) idx | |
val _3 : ('a3, 'b3, ('a0,('a1,('a2,('a3,'a) cons) cons) cons) cons, ('a0,('a1,('a2,('b3,'a) cons) cons) cons) cons) idx | |
val succ : ('an, 'bn, 'a, 'b) idx -> ('an, 'bn, ('a0,'a) cons, ('a0,'b) cons) idx | |
type ('p,'q,'a) monad | |
val ret : 'a -> ('p, 'p, 'a) monad | |
val (>>=) : ('p,'q,'a) monad -> ('a -> ('q,'r,'b) monad) -> ('p,'r,'b) monad | |
val (>>) : ('p,'q,'a) monad -> ('q,'r,'b) monad -> ('p,'r,'b) monad | |
val slide : ('p,'q,'a) monad -> (('p0,'p)cons,('p0,'q)cons,'a) monad | |
val run : (all_empty,all_empty,'a) monad -> 'a Async.Std.Deferred.t | |
type ('s, 'v, 'k) shot | |
type ('s, 'c, 'k) pass | |
type ('s, 'k1, 'k2) branch | |
type finish | |
type ('s,'t,'v,'w,'k) yield = ('s,'v,('t,'w,'k)shot)shot | |
type pos and neg | |
type ('s, 't, 'k) channel | |
val send : (('s,'t,('s,'a,'k)shot)channel , ('s,'t,'k) channel, 'p, 'q) idx -> 'a -> ('p,'q,unit) monad | |
val recv : (('s,'t,('t,'a,'k)shot)channel, ('s,'t,'k) channel, 'p, 'q) idx -> ('p,'q,'a) monad | |
val close : (('s,'t,finish)channel, empty, 'p, 'q) idx -> ('p, 'q, unit) monad | |
val send_slot : | |
(('s,'t,('s,'c,'k) pass) channel, ('s,'t,'k) channel, 'q, 'r) idx -> | |
('c, empty, 'p, 'q) idx -> | |
('p,'r,unit) monad | |
val recv_slot : | |
(('s,'t,('t,'c,'k) pass) channel, ('s,'t,'k) channel, 'p, 'q) idx -> | |
(empty, 'c, 'q, 'r) idx -> | |
('p,'r,unit) monad | |
val send_chan : | |
(('s,'t,('s,('ss,'tt,'kk)channel,'k) pass) channel, ('s,'t,'k) channel, 'q, 'r) idx -> | |
(('ss,'tt,'kk)channel, empty, 'p, 'q) idx -> | |
('p,'r,unit) monad | |
val recv_chan : | |
(('s,'t,('t,('ss,'tt,'kk)channel,'k) pass) channel, ('s,'t,'k) channel, 'p, 'q) idx -> | |
(empty, ('ss,'tt,'kk)channel, 'q, 'r) idx -> | |
('p,'r,unit) monad | |
val send_new_chan : | |
(('s,'t,('s,('t,'s,'kk)channel,'k) pass) channel, ('s,'t,'k) channel, 'p, 'q) idx -> | |
(empty,('s,'t,'kk)channel, 'q, 'r) idx -> | |
('p,'r,unit) monad | |
val select_left : | |
(('s,'t,('s,'k1,'k2)branch)channel, ('s,'t,'k1)channel, 'p, 'q) idx -> | |
('p,'q,unit) monad | |
val select_right : | |
(('s,'t,('s,'k1,'k2)branch)channel, ('s,'t,'k2)channel, 'p, 'q) idx -> | |
('p,'q,unit) monad | |
val branch : | |
(('s,'t,('t,'k1,'k2)branch)channel, empty, 'p, 'q) idx -> | |
(empty,('s,'t,'k1)channel, 'q,'q1) idx * (unit -> ('q1,'r,'a) monad) -> | |
(empty,('s,'t,'k2)channel, 'q,'q2) idx * (unit -> ('q2,'r,'a) monad) -> | |
('p,'r,'a) monad | |
val fork : | |
(empty, (pos,neg,'k)channel, 'p, 'q) idx -> | |
(((neg,pos,'k)channel, all_empty) cons, all_empty, unit) monad -> | |
('p,'q,unit) monad | |
module LinList : sig | |
val nil : (empty,'a list,'p,'q) idx -> ('p,'q,unit) monad | |
val put : ('a list,'a list,'q,'r) idx -> ('a,empty,'p,'q) idx -> ('p,'r,unit)monad | |
val take : ('a list,'a list,'p,'p) idx * (empty,'a,'p,'q1) idx * (unit -> ('q1,'r,'b) monad) -> | |
('a list,empty,'p,'q2) idx * (unit -> ('q2,'r,'b) monad) -> | |
('p,'r,'b) monad | |
(*val map : ('a list,'b list,'p,'q) idx -> ('c -> (('a,all_empty)cons,('b,all_empty)cons,'c)monad) -> 'c -> ('p,'q,'c) monad*) | |
end | |
module Routine : sig | |
val send : 'v -> (('s,'t,('s,'v,'k)shot)channel, ('s,'t,'k) channel, unit) monad | |
val recv : (('s,'t,('t,'v,'k)shot)channel, ('s,'t,'k) channel, 'v) monad | |
val close : (('s,'t,finish)channel, empty, unit) monad | |
val yield : 'v -> (('s,'t,('s,'t,'v,'w,'k)yield)channel, ('s,'t,'k)channel, 'w) monad | |
end | |
val run_routine : | |
(empty, (pos,neg,'k)channel, 'p, 'q) idx -> | |
((neg,pos,'k)channel, empty, unit) monad -> | |
('p,'q,unit) monad |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* compile with OCaml 3.10.0+varunion *) | |
module type SESSION = sig | |
(* slots *) | |
type (+'hd, +'tl) cons | |
(* empty slot(s) *) | |
type empty | |
type all_empty = (empty, 'a) cons as 'a | |
(* | |
* index to specify usage-tracked `slots'. | |
* the type is to read | |
* "in the slot a, replace the n-th content of type an with that of type bn. | |
* the resulting slot is b." | |
*) | |
type ('an,'bn,'a,'b) idx | |
val _0 : ('a0, 'b0, ('a0,'a) cons, ('b0,'a) cons) idx | |
val _1 : ('a1, 'b1, ('a0,('a1,'a) cons) cons, ('a0,('b1,'a) cons) cons) idx | |
val _2 : ('a2, 'b2, ('a0,('a1,('a2,'a) cons) cons) cons, ('a0,('a1,('b2,'a) cons) cons) cons) idx | |
val _3 : ('a3, 'b3, ('a0,('a1,('a2,('a3,'a) cons) cons) cons) cons, ('a0,('a1,('a2,('b3,'a) cons) cons) cons) cons) idx | |
val succ : ('an, 'bn, 'a, 'b) idx -> ('an, 'bn, ('a0,'a) cons, ('a0,'b) cons) idx | |
(* variable-type-state monad *) | |
type ('p,'q,'a) monad | |
val ret : 'a -> ('p, 'p, 'a) monad | |
val (>>=) : ('p,'q,'a) monad -> ('a -> ('q,'r,'b) monad) -> ('p,'r,'b) monad | |
val (>>) : ('p,'q,'a) monad -> ('q,'r,'b) monad -> ('p,'r,'b) monad | |
(* these tags are used to express 'polarity' (indicating an endpoint of a channel) *) | |
type pos and neg | |
(* | |
* the type of channels, which are embedded in slots and not escaped outside the monad. | |
* pair of 's and 't shows polarity ('s != 't). | |
* every channels have type of either: | |
* (pos, neg, 'k) channel (i.e. 'positive'-side) | |
* or | |
* (neg, pos, 'k) channel (i.e. 'negative'-side) | |
*) | |
type ('s, 't, 'k) channel | |
type 'k cont | |
(* | |
* a session type associated to a channel is represented in a symmetric manner. | |
* the type of sending an integer twice has either: | |
* <for positive side> | |
* (pos, neg, [`Shot of pos * int * 'k cont]) channel | |
* or | |
* <for negative side> | |
* (neg, pos, [`Shot of neg * int * 'k cont]) channel | |
* | |
* symmetrically, channel receiving of an int has the type of either | |
* (pos, neg, [`Shot of neg * int * 'k cont]) channel | |
* or | |
* (neg, pos, [`Shot of pos * int * 'k cont]) channel | |
*) | |
val send : (('s,'t,[>`Shot of 's * 'a * 'k cont])channel , ('s,'t,'k) channel, 'p, 'q) idx -> 'a -> ('p,'q,unit) monad | |
val recv : (('s,'t,[`Shot of 't * 'a * 'k cont])channel, ('s,'t,'k) channel, 'p, 'q) idx -> ('p,'q,'a) monad | |
val close : (('s,'t,[>`Finish])channel, empty, 'p, 'q) idx -> ('p, 'q, unit) monad | |
val send_slot : | |
(('s,'t,[>`Pass of 's * 'c * 'k cont]) channel, ('s,'t,'k) channel, 'q, 'r) idx -> | |
('c, empty, 'p, 'q) idx -> | |
('p,'r,unit) monad | |
val recv_slot : | |
(('s,'t,[`Pass of 't * 'c * 'k cont]) channel, ('s,'t,'k) channel, 'p, 'q) idx -> | |
(empty, 'c, 'q, 'r) idx -> | |
('p,'r,unit) monad | |
val send_chan : | |
(('s,'t,[>`Pass of 's * ('ss,'tt,'kk)channel * 'k cont]) channel, ('s,'t,'k) channel, 'q, 'r) idx -> | |
(('ss,'tt,'kk)channel, empty, 'p, 'q) idx -> | |
('p,'r,unit) monad | |
val recv_chan : | |
(('s,'t,[`Pass of 't * ('ss,'tt,'kk)channel * 'k cont]) channel, ('s,'t,'k) channel, 'p, 'q) idx -> | |
(empty, ('ss,'tt,'kk)channel, 'q, 'r) idx -> | |
('p,'r,unit) monad | |
val send_new_chan : | |
(('s,'t,[>`Pass of 's * ('t,'s,'kk)channel * 'k cont]) channel, ('s,'t,'k) channel, 'p, 'q) idx -> | |
(empty,('s,'t,'kk)channel, 'q, 'r) idx -> | |
('p,'r,unit) monad | |
val fork : | |
(empty, (pos,neg,'k)channel, 'p, 'q) idx -> | |
(((neg,pos,'k)channel, all_empty) cons, all_empty, unit) monad -> | |
('p,'q,unit) monad | |
(* | |
* synthesize branching on arbitrary-many `tags | |
* here after we need union of abstract poly-variants | |
*) | |
(* | |
* Basic signature of the synthesis | |
*) | |
module type BRANCH = sig | |
(* session *) | |
type 't from = private [> ] | |
(* type of the branch *) | |
type ('s,'t,'q,'r,'a) branch | |
(* used internally *) | |
val cont_ : 's -> 'q -> ('r * 'a) cont -> ('s,'t,'q,'r,'a) branch -> 't from -> unit | |
(* synthesized branch *) | |
val branch : (('s,'t,'t from)channel,empty,'p,'q) idx -> | |
('s,'t,'q,'r,'a) branch -> | |
('p,'r,'a) monad | |
end | |
(* branch `Finish *) | |
module BranchFinish : | |
BRANCH with | |
type 't from = [`Finish] and | |
type ('s,'t,'q,'r,'a) branch = unit -> ('q,'r,'a) monad | |
type ('s,'t,'v,'k,'q,'r,'a) on_receive = | |
{on_receive:'q1. (empty,('s,'t,'k)channel, 'q,'q1) idx * ('v -> ('q1,'r,'a) monad)} | |
(* FAIL: we need 'q1 to be existential, not universal. *) | |
module type SHOT = sig | |
type 'a polyvar = private [> ] | |
type v | |
type k | |
val ext : 'a polyvar -> 'a | |
end | |
(* Receiving (`SomeTag of 't * 'v * 'k) *) | |
module BranchRecv : | |
functor (X:SHOT) -> | |
BRANCH with | |
type 't from = [< ('t * X.v * X.k cont) X.polyvar] and (* '<' is strange but compiles for now *) | |
type ('s,'t,'q,'r,'a) branch = ('s, 't,X.v,X.k,'q,'r,'a) on_receive | |
(* adding another tag. HERE WE USE UNION OF ABSTRACT VARIANTS *) | |
module BranchAddRecv : | |
functor (M:BRANCH) -> functor (X:SHOT with type 'a polyvar = private [> ]~[M.from]) -> | |
BRANCH with | |
type 't from = ['t M.from | ('t * X.v * X.k cont) X.polyvar] and (* HERE *) | |
type ('s,'t,'q,'r,'a) branch = ('s,'t,'q,'r,'a) M.branch * ('s,'t,X.v,X.k,'q,'r,'a) on_receive | |
end | |
(* signature of Ivar in Janestreet Async *) | |
module type IVAR = sig | |
type 'a t | |
val create : unit -> _ t | |
val create_full : 'a -> 'a t | |
val peek : 'a t -> 'a option | |
val is_empty : _ t -> bool | |
val is_full : _ t -> bool | |
val equal : 'a t -> 'a t -> bool | |
val connect : bind_result:'a t -> bind_rhs:'a t -> unit | |
val fill : 'a t -> 'a -> unit | |
val upon : 'a t -> ('a -> unit) -> unit | |
end | |
module Session(Ivar:IVAR) : SESSION = struct | |
type ('a,'b,'p,'q) idx = ('p -> 'a) * ('p -> 'b -> 'q) | |
type ('hd, 'tl) cons = 'hd * 'tl | |
type empty = Empty | |
type all_empty = empty * all_empty | |
let _0 = (fun (a0,_) -> a0), (fun (_,a) b0 -> (b0,a)) | |
let _1 = (fun (_,(a1,_)) -> a1), (fun (a0,(_,a)) b1 -> (a0,(b1,a))) | |
let _2 = (fun (_,(_,(a2,_))) -> a2), (fun (a0,(a1,(_,a))) b2 -> (a0,(a1,(b2,a)))) | |
let _3 = (fun (_,(_,(_,(a3,_)))) -> a3), (fun (a0,(a1,(a2,(_,a)))) b3 -> (a0,(a1,(a2,(b3,a))))) | |
let succ (get,set) = (fun (_,a) -> get a), (fun (a0,a) bn -> (a0,set a bn)) | |
type ('p,'q,'a) monad = 'p -> ('q * 'a) Ivar.t | |
let ret a p = Ivar.create_full (p, a) | |
let (>>=) m f p = | |
let ret = Ivar.create () in | |
Ivar.upon (m p) (fun (q, x) -> Ivar.connect ~bind_rhs:(f x q) ~bind_result:ret); | |
ret | |
let (>>) m n = m >>= (fun _ -> n) | |
let rec all_empty = Empty, all_empty | |
type pos = Pos and neg = Neg | |
type ('s,'v,'k) shot = Shot of 's * 'v * 'k Ivar.t | |
type ('s,'c,'k) pass = Pass of 's * 'c * 'k Ivar.t | |
type ('s,'k1,'k2) branch = BranchLeft of 's * 'k1 Ivar.t | BranchRight of 's * 'k2 Ivar.t | |
type finish = unit | |
type ('s,'t,'v,'w,'k) yield = ('s,'v,('t,'w,'k)shot)shot | |
type ('s,'t,'k) channel = Chan of 's * 't * 'k Ivar.t | |
type 'k cont = 'k Ivar.t | |
let send (get,set) v p = | |
let Chan(s,t,c) = get p in | |
let c' = Ivar.create () in | |
Ivar.fill c (`Shot(s,v,c')); | |
Ivar.create_full (set p (Chan(s,t,c')), ()) | |
let recv (get,set) p = | |
let Chan(s,t,c) = get p in | |
let ret = Ivar.create () in | |
Ivar.upon c (fun (`Shot(_, v, c')) -> Ivar.fill ret (set p (Chan(s,t,c')), v)); | |
ret | |
let close (get,set) p = | |
Ivar.create_full (set p Empty, ()) | |
let send_slot (get0,set0) (get1,set1) p = | |
let e, q = get1 p, set1 p Empty in | |
let Chan(s,t,c) = get0 q in | |
let c' = Ivar.create () in | |
Ivar.fill c (`Pass(s,e,c')); | |
Ivar.create_full (set0 q (Chan(s,t,c')), ()) | |
let send_chan = send_slot | |
let recv_slot (get0,set0) (get1,set1) p = | |
let Chan(s,t,c) = get0 p in | |
let ret = Ivar.create () in | |
Ivar.upon c (fun (`Pass(_,e,c')) -> Ivar.fill ret (set1 (set0 p (Chan(s,t,c'))) e, ())); | |
ret | |
let recv_chan = recv_slot | |
let send_new_chan (get0,set0) (get1,set1) p = | |
let Chan(s,t,c) = get0 p in | |
let c' = Ivar.create () in | |
let cc = Ivar.create () in | |
let e = `Pass(s,Chan(t,s,cc),c') in | |
Ivar.fill c e; | |
Ivar.create_full (set1 (set0 p (Chan(s,t,c'))) (Chan(s,t,cc)), ()) | |
let branch (get0,set0) ((get1,set1),f1) ((get2,set2),f2) p = | |
let Chan(s,t,c), q = get0 p, set0 p Empty in | |
let ret = Ivar.create () in | |
Ivar.upon c | |
(function | |
| BranchLeft(_,c') -> | |
Ivar.connect ~bind_rhs:(f1 () (set1 q (Chan(s,t,c')))) ~bind_result:ret | |
| BranchRight(_,c') -> | |
Ivar.connect ~bind_rhs:(f2 () (set2 q (Chan(s,t,c')))) ~bind_result:ret | |
); | |
ret | |
let fork (get,set) m p = | |
let ivar = Ivar.create () in | |
ignore (m (Chan(Neg,Pos,ivar),all_empty)); | |
Ivar.create_full (set p (Chan(Pos,Neg,ivar)), ()) | |
module type BRANCH = sig | |
type 't from = private [> ] | |
type ('s,'t,'q,'r,'a) branch | |
val cont_ : 's -> 'q -> ('r * 'a) cont -> ('s,'t,'q,'r,'a) branch -> 't from -> unit | |
val branch : (('s,'t,'t from)channel,empty,'p,'q) idx -> | |
('s,'t,'q,'r,'a) branch -> | |
('p,'r,'a) monad | |
end | |
module BranchFinish = struct | |
type 't from = [`Finish] | |
type ('s,'t,'q,'r,'a) branch = unit -> ('q,'r,'a) monad | |
let cont_ s q ret on_close `Finish = | |
Ivar.connect ~bind_rhs:(on_close () q) ~bind_result:ret | |
let branch (get0,set0) go p = | |
let Chan(s,t,c), q = get0 p, set0 p Empty | |
and ret = Ivar.create () | |
in | |
Ivar.upon c (cont_ s q ret go); | |
ret | |
end | |
module type SHOT = sig | |
type 'a polyvar = private [> ] | |
type v | |
type k | |
val ext : 'a polyvar -> 'a | |
end | |
type ('s,'t,'v,'k,'q,'r,'a) on_receive = | |
{on_receive:'q1. (empty,('s,'t,'k)channel, 'q,'q1) idx * ('v -> ('q1,'r,'a) monad)} | |
module BranchRecv = functor (X:SHOT) -> struct | |
type 't from = [< ('t * X.v * X.k cont) X.polyvar] | |
type ('s,'t,'q,'r,'a) branch = ('s, 't, X.v, X.k, 'q, 'r, 'a) on_receive | |
let cont_ s q ret go (#X.polyvar as x) = | |
let (t,v,c') = X.ext x | |
and (get1,set1), go = go.on_receive | |
in | |
Ivar.connect ~bind_rhs:(go v (set1 q (Chan(s,t,c')))) ~bind_result:ret | |
let branch (get0,set0) go p = | |
let Chan(s,t,c), q = get0 p, set0 p Empty | |
and ret = Ivar.create () | |
in | |
Ivar.upon c (cont_ s q ret go); | |
ret | |
end | |
module BranchAddRecv(M:BRANCH)(X:SHOT with type 'a polyvar = private [> ]~[M.from]) = struct | |
type 't from = ['t M.from | ('t * X.v * X.k cont) X.polyvar] | |
type ('s,'t,'q,'r,'a) branch = ('s,'t,'q,'r,'a) M.branch * ('s,'t,X.v,X.k,'q,'r,'a) on_receive | |
let cont_ s q ret (go1,go2) = function | |
| #M.from as x -> | |
M.cont_ s q ret go1 x | |
| #X.polyvar as x -> | |
let (t,v,c') = X.ext x | |
and (get1,set1), go2 = go2.on_receive | |
in | |
Ivar.connect ~bind_rhs:(go2 v (set1 q (Chan(s,t,c')))) ~bind_result:ret | |
let branch (get0,set0) go p = | |
let Chan(s,t,c), q = get0 p, set0 p Empty | |
and ret = Ivar.create () | |
in | |
Ivar.upon c (cont_ s q ret go); | |
ret | |
end | |
end | |
module BranchSynthesisExample(Ivar:IVAR) = struct | |
module S = Session(Ivar) | |
open S | |
let branch_close_or_shot1 () = | |
let module Shot1 = struct | |
type 'a polyvar = [`Shot1 of 'a] | |
type v = int | |
type k = [`Finish] | |
let ext (`Shot1(x)) = x | |
end in | |
let module M = | |
BranchAddRecv(BranchFinish)(Shot1) | |
in M.branch | |
let branch_shot1_or_shot2 () = | |
let module Shot1 = struct | |
type 'a polyvar = [`Shot1 of 'a] | |
type v = int | |
type k = [`Finish] | |
let ext (`Shot1(x)) = x | |
end in | |
let module Shot2 = struct | |
type 'a polyvar = [`Shot2 of 'a] | |
type v = string | |
type k = [`Finish] | |
let ext (`Shot2(x)) = x | |
end in | |
let module M = BranchAddRecv(BranchRecv(Shot1))(Shot2) | |
in M.branch | |
end | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment