Skip to content

Instantly share code, notes, and snippets.

@keigoi

keigoi/mpst.ml

Last active August 16, 2018 04:03
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save keigoi/5740db9bd83e3fed9edeaa160c16d599 to your computer and use it in GitHub Desktop.
Save keigoi/5740db9bd83e3fed9edeaa160c16d599 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
mpst.ml
module type S = sig
type _ mpst
type _ sess
type (_, _, _, _) lens
type (_, _) label
type (_, _, _, _) dlabel
type ('a, 'b, 'c, 'd, 'e, 'f) role = ('a, 'b, 'c, 'd) lens * ('e, 'f) label
type _ typ
val int : int typ
val str : string typ
val msg : 't typ -> ([`msg of 't * 'g], 'g, [`msg of 't * 'h], 'h) dlabel
val left : ([`left of 'g], 'g, [`left of 'h | `right of _], 'h) dlabel
val right : ([`right of 'g], 'g, [`left of _ | `right of 'h], 'h) dlabel
val (-->) :
([`send of 'c] sess, 'd, 't, 's, 'e, 'f1) role
-> ([`recv of 'e] sess, 'f, 'u, 't, 'c, 'd1) role
-> ('d1, 'd, 'f1, 'f) dlabel
-> 's mpst
-> 'u mpst
val (-%%->) :
([`send of 'c] sess, unit, 't, 'ss, 'e, [`left of 'f1 | `right of 'f2]) role
-> ([`recv of 'e] sess, unit, 'u, 't, 'c, [`left of 'd1 | `right of 'd2]) role
-> left:(((unit, 'd1, 't1, 's1, _, _) role * (unit, 'f1, 'ss, 't1, _, _) role) * 's1 mpst)
-> right:(((unit, 'd2, 't2, 's2, _, _) role * (unit, 'f2, 'ss, 't2, _, _) role) * 's2 mpst)
-> 'u mpst
val (-%%%->) :
([`send of 'c] sess, unit, 't, 'ss, 'e, [`left of 'f1 | `middle of 'f2 | `right of 'f3]) role
-> ([`recv of 'e] sess, unit, 'u, 't, 'c, [`left of 'd1 | `middle of 'd2 | `right of 'd3]) role
-> left:(((unit, 'd1, 't1, 's1, _, _) role * (unit, 'f1, 'ss, 't1, _, _) role) * 's1 mpst)
-> middle:(((unit, 'd2, 't2, 's2, _, _) role * (unit, 'f2, 'ss, 't2, _, _) role) * 's2 mpst)
-> right:(((unit, 'd3, 't3, 's3, _, _) role * (unit, 'f3, 'ss, 't3, _, _) role) * 's3 mpst)
-> 'u mpst
type close
module MPST3 : sig
val a : ('a1, 'a2, <a:'a1; b:'b; c:'c>, <a:'a2; b:'b; c:'c>, [`a of 'g], 'g) role
val b : ('b1, 'b2, <a:'a; b:'b1; c:'c>, <a:'a; b:'b2; c:'c>, [`b of 'g], 'g) role
val c : ('c1, 'c2, <a:'a; b:'b; c:'c1>, <a:'a; b:'b; c:'c2>, [`c of 'g], 'g) role
val finish : <a:close; b:close; c:close> mpst
end
module MPST4 : sig
val a : ('a1, 'a2, <a:'a1; b:'b; c:'c; d:'d>, <a:'a2; b:'b; c:'c; d:'d>, [`a of 'g], 'g) role
val b : ('b1, 'b2, <a:'a; b:'b1; c:'c; d:'d>, <a:'a; b:'b2; c:'c; d:'d>, [`b of 'g], 'g) role
val c : ('c1, 'c2, <a:'a; b:'b; c:'c1; d:'d>, <a:'a; b:'b; c:'c2; d:'d>, [`c of 'g], 'g) role
val d : ('d1, 'd2, <a:'a; b:'b; c:'c; d:'d1>, <a:'a; b:'b; c:'c; d:'d2>, [`c of 'g], 'g) role
val finish : <a:close; b:close; c:close; d:close> mpst
end
end
module M2(X:S) = struct
include X
open MPST4
let g () =
(c --> a) (msg int) @@
(a -%%-> b)
~left:((a,b),
(b --> c) right @@
finish)
~right:((a,b),
(b --> a) (msg int) @@
(b --> c) left @@
(c --> a) (msg str) @@
finish)
let rec g2 () =
(a -%%-> b)
~left:((a,b),
(b --> a) (msg int) @@
(b --> c) right @@
finish)
~right:((a,b),
(b --> a) (msg str) @@
(b --> c) left @@
g2 ())
(*
unit ->
< a : [ `recv of
[ `c of
[ `msg of
int *
[ `send of
[ `b of
[ `left of close
| `right of
[ `recv of
[ `b of
[ `msg of
int *
[ `recv of
[ `c of
[ `msg of string * close ] ] ]
sess ] ] ]
sess ] ] ]
sess ] ] ]
sess;
b : [ `recv of
[ `a of
[ `left of [ `send of [ `c of [ `right of close ] ] ] sess
| `right of
[ `send of
[ `a of
[ `msg of
int *
[ `send of [ `c of [ `left of close ] ] ] sess ] ] ]
sess ] ] ]
sess;
c : [ `send of
[ `a of
[ `msg of
int *
[ `recv of
[ `b of
[ `left of
[ `send of [ `a of [ `msg of string * close ] ] ]
sess
| `right of close ] ] ]
sess ] ] ]
sess;
d : close >
mpst
*)
(*
unit ->
< a : [ `send of
[ `b of
[ `left of [ `recv of [ `b of [ `msg of int * close ] ] ] sess
| `right of [ `recv of [ `b of [ `msg of string * 'a ] ] ] sess ] ] ]
sess as 'a;
b : [ `recv of
[ `a of
[ `left of
[ `send of
[ `a of
[ `msg of
int *
[ `send of [ `c of [ `right of close ] ] ] sess ] ] ]
sess
| `right of
[ `send of
[ `a of
[ `msg of
string *
[ `send of [ `c of [ `left of 'b ] ] ] sess ] ] ]
sess ] ] ]
sess as 'b;
c : [ `recv of [ `b of [ `left of 'c | `right of close ] ] ] sess as 'c;
d : close >
mpst
*)
let g3 () =
(c --> a) (msg int) @@
(a -%%%-> b)
~left:((a,b),
(b --> c) left @@
(c --> a) (msg str) @@
finish)
~middle:((a,b),
(b --> c) right @@
finish)
~right:((a,b),
(b --> a) (msg int) @@
(b --> c) left @@
(c --> a) (msg str) @@
finish)
(*
unit ->
< a : [ `recv of
[ `c of
[ `msg of
int *
[ `send of
[ `b of
[ `left of
[ `recv of [ `c of [ `msg of string * close ] ] ]
sess
| `middle of close
| `right of
[ `recv of
[ `b of
[ `msg of
int *
[ `recv of
[ `c of
[ `msg of string * close ] ] ]
sess ] ] ]
sess ] ] ]
sess ] ] ]
sess;
b : [ `recv of
[ `a of
[ `left of [ `send of [ `c of [ `left of close ] ] ] sess
| `middle of [ `send of [ `c of [ `right of close ] ] ] sess
| `right of
[ `send of
[ `a of
[ `msg of
int *
[ `send of [ `c of [ `left of close ] ] ] sess ] ] ]
sess ] ] ]
sess;
c : [ `send of
[ `a of
[ `msg of
int *
[ `recv of
[ `b of
[ `left of
[ `send of [ `a of [ `msg of string * close ] ] ]
sess
| `right of close ] ] ]
sess ] ] ]
sess;
d : close >
mpst
*)
end
Raw
session.ml
(* a binary session calculus, sequentially *)
module Try = struct
type _ sess =
| Send : ('v -> 's sess) -> [`send of 'v * 's] sess
| Recv : 'v * 's sess -> [`recv of 'v * 's] sess
| Close : [`close] sess
let send : [`send of 'v * 's] sess -> 'v -> 's sess = fun (Send f) v -> f v
let receive : [`recv of 'v * 's] sess -> 'v * 's sess = fun (Recv (v,s)) -> v, s
let close : [`close] sess -> unit = fun Close -> ()
let p () =
Send (fun x -> (Send (fun y -> Recv(x+y, Close))))
let f () =
let p = p () in
let p = send p 10 in
let p = send p 20 in
let v, p = receive p in
close p;
print_int v;
()
end
(* trial to build a mpst local endpoint. we want to have [`send of [`A of ...]] for a (parameterised) participant A *)
module Try2 = struct
type ('l,'x) label = 'x -> 'l (* use as a role label later -- ([`a of 'x], 'x) label *)
type _ sess =
| Send : (([>] as 'l, [`msg of 'v * 's sess]) label * 'v -> 's sess) -> [`send of 'l] sess
| Recv : (([>] as 'l, [`msg of 'v * 's sess]) label * 'v * 's sess) -> [`recv of 'l] sess
| SelectLeft : (([>] as 'l, [`left of 's sess]) label -> 's sess) -> [`send of 'l] sess
| SelectRight : (([>] as 'l, [`right of 's sess]) label -> 's sess) -> [`send of 'l] sess
| BranchLeftRight : ([>] as 'l, ([`left of 's1 sess | `right of 's2 sess] as 'x)) label * 'x -> [`recv of 'l] sess
| Close : [`close] sess
let a : ([`a of 'x], 'x) label = fun x -> `a(x)
let left : ([>`left of 'x], 'x) label = fun x -> `left(x)
let right : ([>`left of 'x], 'x) label = fun x -> `left(x)
let p0 () =
SelectLeft (fun l -> match l (`left(Close)) with `c(`left(s)) -> s)
(*
int ->
[ `recv of
[> `left of
[ `left of
[ `recv of [ `a of [ `msg of int * [ `close ] sess ] ] ] sess
| `right of [ `close ] sess ] ] ]
sess
*)
let p1 x =
begin
if x<>0 then
BranchLeftRight (left, `left(Recv (a, 123 / x, Close)))
else
BranchLeftRight (right, `right(Close))
end
let p2 () =
(*
unit ->
[ `send of
[< `c of
[< `msg of
'a * <== ??
[ `recv of
[> `left of
[ `left of
[ `recv of
[ `a of [ `msg of int * [ `close ] sess ] ] ]
sess
| `right of [ `close ] sess ] ] ]
sess ] ] ]
sess
*)
Send (fun (l,v) ->
match l (`msg(v,p1 v)) with
| `c(`msg(_,s)) -> s)
(* fail *)
let send : type v s. (([>] as 'l, [`msg of v * s sess]) label * v) -> [`send of 'l] sess -> s sess =
fun (l, v) (Send f) ->
f (l, v)
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment