Skip to content

Instantly share code, notes, and snippets.

@keigoi keigoi/.depend
Last active Jan 1, 2016

Embed
What would you like to do?
Session type implementation using Janestreet Async
session.cmi :
example.cmo : session.cmi
example.cmx : session.cmx
session.cmo : session.cmi
session.cmx : session.cmi
*.cm[ioxat]
*.cmxa
*.cmti
*.o
*.annot
test.*
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()
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
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)), ())
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
(* 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
You can’t perform that action at this time.