diff --git a/.github/workflows/workflow.yml b/.github/workflows/workflow.yml index 4c8801f..deabdab 100644 --- a/.github/workflows/workflow.yml +++ b/.github/workflows/workflow.yml @@ -32,4 +32,9 @@ jobs: - run: opam install . --deps-only --with-test - - run: opam exec -- dune build + - run: opam exec -- dune build --profile=dev --only-packages mpst,mpst-basic + + - run: opam exec -- dune build tests/ examples/ + + - run: opam exec -- dune runtest + diff --git a/.gitignore b/.gitignore index c004e09..e34302c 100644 --- a/.gitignore +++ b/.gitignore @@ -42,3 +42,4 @@ ppx_tools/ppx_tools.install _opam +.vscode \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json deleted file mode 100644 index 545db9d..0000000 --- a/.vscode/settings.json +++ /dev/null @@ -1,6 +0,0 @@ -{ - "ocaml.sandbox": { - "kind": "opam", - "switch": "4.12.1" - } -} \ No newline at end of file diff --git a/README.md b/README.md index 429ed5f..a0308ed 100644 --- a/README.md +++ b/README.md @@ -66,8 +66,7 @@ dune exec examples/mpst/calc.exe 1. Declare the name of participants (__roles__) and __labels__: ``` -open Mpst.BasicCombinators -open Mpst.Unicast +open Mpst_basic [%%declare_roles_prefixed a, b, c] (* note that the order matters *) [%%declare_labels msg] diff --git a/lib/bare/chan.ml b/basic/bare/chan.ml similarity index 100% rename from lib/bare/chan.ml rename to basic/bare/chan.ml diff --git a/lib/bare/chan.mli b/basic/bare/chan.mli similarity index 100% rename from lib/bare/chan.mli rename to basic/bare/chan.mli diff --git a/lib/bare/monitor.ml b/basic/bare/monitor.ml similarity index 100% rename from lib/bare/monitor.ml rename to basic/bare/monitor.ml diff --git a/lib/bare/monitor.mli b/basic/bare/monitor.mli similarity index 100% rename from lib/bare/monitor.mli rename to basic/bare/monitor.mli diff --git a/basic/dune b/basic/dune new file mode 100644 index 0000000..0d1c26a --- /dev/null +++ b/basic/dune @@ -0,0 +1,6 @@ +(library + (name mpst_basic) + (public_name mpst-basic) + (libraries mpst hlist rows threads compiler-libs.common)) + +(include_subdirs unqualified) diff --git a/lib/dynChan.ml b/basic/dynChan.ml similarity index 98% rename from lib/dynChan.ml rename to basic/dynChan.ml index 97797de..8fb68dd 100644 --- a/lib/dynChan.ml +++ b/basic/dynChan.ml @@ -6,7 +6,7 @@ module type S = sig val new_endpoint : unit -> 'a endpoint end -type chan = (module S) +type t = (module S) let rec path_compression n = match !n with diff --git a/basic/dynChan.mli b/basic/dynChan.mli new file mode 100644 index 0000000..1f7825c --- /dev/null +++ b/basic/dynChan.mli @@ -0,0 +1 @@ +include Mpst.S.CHANNEL diff --git a/basic/mpst_basic.ml b/basic/mpst_basic.ml new file mode 100644 index 0000000..98f4031 --- /dev/null +++ b/basic/mpst_basic.ml @@ -0,0 +1,4 @@ +module DynChan = DynChan +include Mpst.BasicCombinators +include Mpst.Unicast.Make(DynChan) +include Mpst.Multicast.Make(DynChan) diff --git a/examples/calc/calc.ml b/examples/calc/calc.ml index 0028b0a..b6cfa58 100644 --- a/examples/calc/calc.ml +++ b/examples/calc/calc.ml @@ -1,5 +1,4 @@ -open Mpst.BasicCombinators -open Mpst.Unicast +open Mpst_basic type op = Add | Sub | Mul | Div diff --git a/examples/calc/dune b/examples/calc/dune index 43ba5ce..237159a 100644 --- a/examples/calc/dune +++ b/examples/calc/dune @@ -3,4 +3,4 @@ (modules calc) (preprocess (staged_pps mpst.ppx.ty)) - (libraries mpst)) + (libraries mpst-basic)) diff --git a/examples/mixed_choice/dune b/examples/mixed_choice/dune index 1e6f178..1c8a97d 100644 --- a/examples/mixed_choice/dune +++ b/examples/mixed_choice/dune @@ -3,4 +3,4 @@ (modules mixed1) (preprocess (staged_pps mpst.ppx.ty)) - (libraries mpst)) + (libraries mpst-basic)) diff --git a/examples/mixed_choice/mixed1.ml b/examples/mixed_choice/mixed1.ml index fd3b703..68d16da 100644 --- a/examples/mixed_choice/mixed1.ml +++ b/examples/mixed_choice/mixed1.ml @@ -1,5 +1,4 @@ -open Mpst.BasicCombinators -open Mpst.Unicast +open Mpst_basic [%%declare_roles a, b, c] [%%declare_labels req, resp, timeout] diff --git a/lib/dynChan.mli b/lib/dynChan.mli deleted file mode 100644 index db2522e..0000000 --- a/lib/dynChan.mli +++ /dev/null @@ -1,9 +0,0 @@ -type chan -type 'a endpoint - -val make : unit -> chan -val new_endpoint : chan -> 'a endpoint -val unify : 'a endpoint -> 'a endpoint -> unit -val finalise : 'a endpoint -> 'a endpoint -val send : 'a endpoint -> 'a -> unit -val receive : 'a endpoint -> 'a diff --git a/lib/multicast/actionGather.ml b/lib/multicast/actionGather.ml index b624038..bcff410 100644 --- a/lib/multicast/actionGather.ml +++ b/lib/multicast/actionGather.ml @@ -1,91 +1,99 @@ module Context = State.Context type tag = int -type 'var gather_ = (tag DynChan.endpoint list * 'var InpChoice.t list) lazy_t -type 'var gather = 'var gather_ Lin.lin - -let gather_op0 (type b) : b gather_ State.op = - let module M = struct - type nonrec a = b gather_ - - let determinise ctx gthr = - lazy - begin - let names, exts = Lazy.force gthr in - (names, List.map (InpChoice.determinise ctx) exts) - end - - let merge ctx g1 g2 = - lazy - begin - let names1, exts1 = Lazy.force g1 and names2, exts2 = Lazy.force g2 in - List.iter2 DynChan.unify names1 names2; - (names1, InpChoice.merge ctx exts1 exts2) - end - - let force ctx s = - let (names : int DynChan.endpoint list), extcs = Lazy.force s in - ignore (List.map DynChan.finalise names); - extcs |> List.iter (InpChoice.force ctx) - - let to_string ctx s = - "?{" - ^ (if Lazy.is_val s then - String.concat "," - (List.map (fun e -> InpChoice.to_string ctx e) (snd (Lazy.force s))) - else "") - ^ "}" - end in - (module M) - -let gather_op role = - LinState.gen_op @@ State.obj_op role @@ LinState.lin_op @@ gather_op0 - -let make_gather0 constr names s = - Lazy.from_val (names, [ InpChoice.make constr s ]) - -open Rows - -let make_gather role constr (names : _ DynChan.endpoint list) s = - let st = - (role.make_obj |> Lin.map_gen) @@ Lin.declare @@ make_gather0 constr names s - in - PowState.make (gather_op role) st - -let gather (inp : _ gather) = - let names, items = Lazy.force @@ Lin.use inp in - let tags = - List.map (fun name -> DynChan.receive (DynChan.finalise name)) names - in - let tag = match tags with tag :: _ -> tag | [] -> failwith "impossible" in - assert (List.for_all (fun t -> t = tag) tags); - items |> List.map InpChoice.match_item |> List.assoc tag |> Lazy.force - -type ('v, 's) gather_val_ = 'v DynChan.endpoint list * 's LinState.t -type ('v, 's) gather_val = ('v, 's) gather_val_ Lin.lin - -let gather_val_op0 (type v s) : (v, s) gather_val_ State.op = - let module M = struct - type a = (v, s) gather_val_ - - let determinise ctx (ch, s) = (ch, PowState.determinise ctx s) - - let merge ctx (ch1, s1) (ch2, s2) = - List.iter2 DynChan.unify ch1 ch2; - (ch1, PowState.merge ctx s1 s2) - - let force ctx (_, s) = PowState.force ctx s - let to_string ctx (_, s) = "?." ^ PowState.to_string ctx s - end in - (module M) - -let gather_val_op role = State.obj_op role @@ LinState.lin_op gather_val_op0 - -let make_gather_val role names cont = - let st = (role.make_obj |> Lin.map_gen) @@ Lin.declare (names, cont) in - PowState.make (LinState.gen_op (gather_val_op role)) st - -let gather_val (type v s) (gthrv : (v, s) gather_val) = - let chs, cont = Lin.use gthrv in - ( List.map (fun ch -> DynChan.receive (DynChan.finalise ch)) chs, - Lin.fresh (PowState.ensure_determinised cont) ) + +module Make (DynChan : S.CHANNEL) = struct + type 'var gather_ = (tag DynChan.endpoint list * 'var InpChoice.t list) lazy_t + type 'var gather = 'var gather_ Lin.lin + + let gather_op0 (type b) : b gather_ State.op = + let module M = struct + type nonrec a = b gather_ + + let determinise ctx gthr = + lazy + begin + let names, exts = Lazy.force gthr in + (names, List.map (InpChoice.determinise ctx) exts) + end + + let merge ctx g1 g2 = + lazy + begin + let names1, exts1 = Lazy.force g1 + and names2, exts2 = Lazy.force g2 in + List.iter2 DynChan.unify names1 names2; + (names1, InpChoice.merge ctx exts1 exts2) + end + + let force ctx s = + let (names : int DynChan.endpoint list), extcs = Lazy.force s in + ignore (List.map DynChan.finalise names); + extcs |> List.iter (InpChoice.force ctx) + + let to_string ctx s = + "?{" + ^ (if Lazy.is_val s then + String.concat "," + (List.map + (fun e -> InpChoice.to_string ctx e) + (snd (Lazy.force s))) + else "") + ^ "}" + end in + (module M) + + let gather_op role = + LinState.gen_op @@ State.obj_op role @@ LinState.lin_op @@ gather_op0 + + let make_gather0 constr names s = + Lazy.from_val (names, [ InpChoice.make constr s ]) + + open Rows + + let make_gather role constr (names : _ DynChan.endpoint list) s = + let st = + (role.make_obj |> Lin.map_gen) + @@ Lin.declare + @@ make_gather0 constr names s + in + PowState.make (gather_op role) st + + let gather (inp : _ gather) = + let names, items = Lazy.force @@ Lin.use inp in + let tags = + List.map (fun name -> DynChan.receive (DynChan.finalise name)) names + in + let tag = match tags with tag :: _ -> tag | [] -> failwith "impossible" in + assert (List.for_all (fun t -> t = tag) tags); + items |> List.map InpChoice.match_item |> List.assoc tag |> Lazy.force + + type ('v, 's) gather_val_ = 'v DynChan.endpoint list * 's LinState.t + type ('v, 's) gather_val = ('v, 's) gather_val_ Lin.lin + + let gather_val_op0 (type v s) : (v, s) gather_val_ State.op = + let module M = struct + type a = (v, s) gather_val_ + + let determinise ctx (ch, s) = (ch, PowState.determinise ctx s) + + let merge ctx (ch1, s1) (ch2, s2) = + List.iter2 DynChan.unify ch1 ch2; + (ch1, PowState.merge ctx s1 s2) + + let force ctx (_, s) = PowState.force ctx s + let to_string ctx (_, s) = "?." ^ PowState.to_string ctx s + end in + (module M) + + let gather_val_op role = State.obj_op role @@ LinState.lin_op gather_val_op0 + + let make_gather_val role names cont = + let st = (role.make_obj |> Lin.map_gen) @@ Lin.declare (names, cont) in + PowState.make (LinState.gen_op (gather_val_op role)) st + + let gather_val (type v s) (gthrv : (v, s) gather_val) = + let chs, cont = Lin.use gthrv in + ( List.map (fun ch -> DynChan.receive (DynChan.finalise ch)) chs, + Lin.fresh (PowState.ensure_determinised cont) ) +end diff --git a/lib/multicast/actionGather.mli b/lib/multicast/actionGather.mli index f7d6815..4852cd0 100644 --- a/lib/multicast/actionGather.mli +++ b/lib/multicast/actionGather.mli @@ -1,18 +1,20 @@ -type 'var gather -type ('v, 's) gather_val +module Make (C : S.CHANNEL) : sig + type 'var gather + type ('v, 's) gather_val -val make_gather : - ('a, 'var gather) Rows.method_ -> - ('var, 's) Rows.constr -> - int DynChan.endpoint list -> - 's LinState.t -> - 'a LinState.t + val make_gather : + ('a, 'var gather) Rows.method_ -> + ('var, 's) Rows.constr -> + int C.endpoint list -> + 's LinState.t -> + 'a LinState.t -val make_gather_val : - ('a, ('v, 's) gather_val) Rows.method_ -> - 'v DynChan.endpoint list -> - 's LinState.t -> - 'a LinState.t + val make_gather_val : + ('a, ('v, 's) gather_val) Rows.method_ -> + 'v C.endpoint list -> + 's LinState.t -> + 'a LinState.t -val gather : 'a gather -> 'a -val gather_val : ('v, 's) gather_val -> 'v list * 's + val gather : 'a gather -> 'a + val gather_val : ('v, 's) gather_val -> 'v list * 's +end diff --git a/lib/multicast/actionMany.ml b/lib/multicast/actionMany.ml index 5dea529..6f619e6 100644 --- a/lib/multicast/actionMany.ml +++ b/lib/multicast/actionMany.ml @@ -1,56 +1,64 @@ type 'a many = 'a LinState.t list -let get_many ss = List.map (fun s -> Lin.fresh @@ PowState.do_determinise s) ss - -let list_op (type b) : b many State.op = - let module M = struct - type nonrec a = b many - - let determinise _ctx s = s - let merge _ctx s1 s2 = List.map2 PowState.make_merge s1 s2 - let force _ctx _ss = () - let to_string _ctx _s = "" - end in - (module M) - -let units ~count = - PowState.make - (LinState.gen_op @@ list_op) - (Lin.declare_unlimited @@ List.init count (fun _i -> LinState.unit)) - -let make_many ~count (names : 'v DynChan.endpoint list) (ss : 's many LinState.t) - (f : 'v DynChan.endpoint -> 's LinState.t -> 'a LinState.t) : 'a many LinState.t - = - let ss = - lazy - (let ss = - Lin.fresh @@ PowState.do_determinise ss (* FIXME this needs context *) - in - ss) - in - let ss = - List.init count (fun i -> - PowState.make_lazy (lazy (List.nth (Lazy.force ss) i))) - in - PowState.make_raw (State.Context.new_key ()) - (lazy - State. - { - st = Lin.declare_unlimited @@ List.map2 f names ss; - st_op = LinState.gen_op @@ list_op; - }) - -let make_selects ~count role lab names (ss : _ many LinState.t) : - _ many LinState.t = - make_many ~count names ss (fun name s -> - ActionOut.make_select role lab name s) - -let make_branches ~count role constr names (ss : _ many LinState.t) = - make_many ~count names ss (fun name s -> - ActionInp.make_branch role constr name s) - -let make_outs ~count role names ss = - make_many ~count names ss (fun name s -> ActionOut.make_out role name s) - -let make_inps ~count role names ss = - make_many ~count names ss (fun name s -> ActionInp.make_inp role name s) +module Make (DynChan : S.CHANNEL) = struct + module ActionOut = ActionOut.Make (DynChan) + module ActionInp = ActionInp.Make (DynChan) + + let get_many ss = + List.map (fun s -> Lin.fresh @@ PowState.do_determinise s) ss + + let list_op (type b) : b many State.op = + let module M = struct + type nonrec a = b many + + let determinise _ctx s = s + let merge _ctx s1 s2 = List.map2 PowState.make_merge s1 s2 + let force _ctx _ss = () + let to_string _ctx _s = "" + end in + (module M) + + let units ~count = + PowState.make + (LinState.gen_op @@ list_op) + (Lin.declare_unlimited @@ List.init count (fun _i -> LinState.unit)) + + let make_many ~count (names : 'v DynChan.endpoint list) + (ss : 's many LinState.t) + (f : 'v DynChan.endpoint -> 's LinState.t -> 'a LinState.t) : + 'a many LinState.t = + let ss = + lazy + (let ss = + Lin.fresh + @@ PowState.do_determinise ss (* FIXME this needs context *) + in + ss) + in + let ss = + List.init count (fun i -> + PowState.make_lazy (lazy (List.nth (Lazy.force ss) i))) + in + PowState.make_raw (State.Context.new_key ()) + (lazy + State. + { + st = Lin.declare_unlimited @@ List.map2 f names ss; + st_op = LinState.gen_op @@ list_op; + }) + + let make_selects ~count role lab names (ss : _ many LinState.t) : + _ many LinState.t = + make_many ~count names ss (fun name s -> + ActionOut.make_select role lab name s) + + let make_branches ~count role constr names (ss : _ many LinState.t) = + make_many ~count names ss (fun name s -> + ActionInp.make_branch role constr name s) + + let make_outs ~count role names ss = + make_many ~count names ss (fun name s -> ActionOut.make_out role name s) + + let make_inps ~count role names ss = + make_many ~count names ss (fun name s -> ActionInp.make_inp role name s) +end \ No newline at end of file diff --git a/lib/multicast/actionMany.mli b/lib/multicast/actionMany.mli index c3c9ba4..cf43f73 100644 --- a/lib/multicast/actionMany.mli +++ b/lib/multicast/actionMany.mli @@ -1,34 +1,36 @@ type 'a many -val get_many : 'a many -> 'a list -val units : count:int -> unit many LinState.t +module Make (C : S.CHANNEL) : sig + val get_many : 'a many -> 'a list + val units : count:int -> unit many LinState.t -val make_selects : - count:int -> - ('a, 'b) Rows.method_ -> - ('b, 'c ActionOut.select) Rows.method_ -> - int DynChan.endpoint list -> - 'c many LinState.t -> - 'a many LinState.t + val make_selects : + count:int -> + ('a, 'b) Rows.method_ -> + ('b, 'c ActionOut.Make(C).select) Rows.method_ -> + int C.endpoint list -> + 'c many LinState.t -> + 'a many LinState.t -val make_branches : - count:int -> - ('a, 'b ActionInp.branch) Rows.method_ -> - ('b, 'c) Rows.constr -> - int DynChan.endpoint list -> - 'c many LinState.t -> - 'a many LinState.t + val make_branches : + count:int -> + ('a, 'b ActionInp.Make(C).branch) Rows.method_ -> + ('b, 'c) Rows.constr -> + int C.endpoint list -> + 'c many LinState.t -> + 'a many LinState.t -val make_outs : - count:int -> - ('a, ('v, 'c) ActionOut.out) Rows.method_ -> - 'v DynChan.endpoint list -> - 'c many LinState.t -> - 'a many LinState.t + val make_outs : + count:int -> + ('a, ('v, 'c) ActionOut.Make(C).out) Rows.method_ -> + 'v C.endpoint list -> + 'c many LinState.t -> + 'a many LinState.t -val make_inps : - count:int -> - ('a, ('v, 'c) ActionInp.inp) Rows.method_ -> - 'v DynChan.endpoint list -> - 'c many LinState.t -> - 'a many LinState.t + val make_inps : + count:int -> + ('a, ('v, 'c) ActionInp.Make(C).inp) Rows.method_ -> + 'v C.endpoint list -> + 'c many LinState.t -> + 'a many LinState.t +end diff --git a/lib/multicast/actionScatter.ml b/lib/multicast/actionScatter.ml index 6f14a1d..3ada823 100644 --- a/lib/multicast/actionScatter.ml +++ b/lib/multicast/actionScatter.ml @@ -3,76 +3,78 @@ module Context = State.Context type tag = int -type ('v, 's) scatter_val_ = - string * 'v DynChan.endpoint list * 's LinState.t lazy_t +module Make (DynChan : S.CHANNEL) = struct + type ('v, 's) scatter_val_ = + string * 'v DynChan.endpoint list * 's LinState.t lazy_t -type ('v, 's) scatter_val = ('v, 's) scatter_val_ Lin.lin -type 'a scatter = (tag, 'a) scatter_val + type ('v, 's) scatter_val = ('v, 's) scatter_val_ Lin.lin + type 'a scatter = (tag, 'a) scatter_val -let scatter_op0 (type v b) : (v, b) scatter_val_ State.op = - let module M = struct - type nonrec a = (v, b) scatter_val_ + let scatter_op0 (type v b) : (v, b) scatter_val_ State.op = + let module M = struct + type nonrec a = (v, b) scatter_val_ - let determinise ctx (tag, name, cont) = - (tag, name, lazy (PowState.determinise ctx (Lazy.force cont))) + let determinise ctx (tag, name, cont) = + (tag, name, lazy (PowState.determinise ctx (Lazy.force cont))) - let merge ctx (tag1, names1, cont1) (tag2, names2, cont2) = - assert (tag1 = tag2); - List.iter2 DynChan.unify names1 names2; + let merge ctx (tag1, names1, cont1) (tag2, names2, cont2) = + assert (tag1 = tag2); + List.iter2 DynChan.unify names1 names2; - ( tag1, - names1, - lazy (PowState.merge ctx (Lazy.force cont1) (Lazy.force cont2)) ) + ( tag1, + names1, + lazy (PowState.merge ctx (Lazy.force cont1) (Lazy.force cont2)) ) - let force ctx (_, names, cont) = - ignore (List.map DynChan.finalise names); - PowState.force ctx (Lazy.force cont) + let force ctx (_, names, cont) = + ignore (List.map DynChan.finalise names); + PowState.force ctx (Lazy.force cont) - let to_string ctx (_, _, cont) = - "." - ^ - if Lazy.is_val cont then - let cont = Lazy.force cont in - PowState.to_string ctx cont - else "" - end in - (module M) + let to_string ctx (_, _, cont) = + "." + ^ + if Lazy.is_val cont then + let cont = Lazy.force cont in + PowState.to_string ctx cont + else "" + end in + (module M) -let scatter_op role lab = - LinState.gen_op - @@ State.obj_op role - @@ State.obj_op lab - @@ LinState.lin_op - @@ scatter_op0 + let scatter_op role lab = + LinState.gen_op + @@ State.obj_op role + @@ State.obj_op lab + @@ LinState.lin_op + @@ scatter_op0 -let scatter_val_op role = - LinState.gen_op @@ State.obj_op role @@ LinState.lin_op @@ scatter_op0 + let scatter_val_op role = + LinState.gen_op @@ State.obj_op role @@ LinState.lin_op @@ scatter_op0 -let make_scatter role lab name s = - let st = - Lin.map_gen (fun t -> role.make_obj @@ lab.make_obj t) - @@ Lin.declare - @@ (lab.method_name, name, Lazy.from_val s) - in - PowState.make (scatter_op role lab) st + let make_scatter role lab name s = + let st = + Lin.map_gen (fun t -> role.make_obj @@ lab.make_obj t) + @@ Lin.declare + @@ (lab.method_name, name, Lazy.from_val s) + in + PowState.make (scatter_op role lab) st -let make_scatter_val role name s = - let st = - (role.make_obj |> Lin.map_gen) - @@ Lin.declare - @@ ("_out" (*FIXME*), name, Lazy.from_val s) - in - PowState.make (scatter_val_op role) st + let make_scatter_val role name s = + let st = + (role.make_obj |> Lin.map_gen) + @@ Lin.declare + @@ ("_out" (*FIXME*), name, Lazy.from_val s) + in + PowState.make (scatter_val_op role) st -let scatter s = - let labname, names, cont = Lin.use s in - let tag = Btype.hash_variant labname in - let cont = PowState.ensure_determinised (Lazy.force cont) in - List.iter (fun name -> DynChan.send (DynChan.finalise name) tag) names; - Lin.fresh cont + let scatter s = + let labname, names, cont = Lin.use s in + let tag = Btype.hash_variant labname in + let cont = PowState.ensure_determinised (Lazy.force cont) in + List.iter (fun name -> DynChan.send (DynChan.finalise name) tag) names; + Lin.fresh cont -let scatter_val s vs = - let _, names, cont = Lin.use s in - let cont = PowState.ensure_determinised (Lazy.force cont) in - List.iter2 (fun name v -> DynChan.send (DynChan.finalise name) v) names vs; - Lin.fresh cont + let scatter_val s vs = + let _, names, cont = Lin.use s in + let cont = PowState.ensure_determinised (Lazy.force cont) in + List.iter2 (fun name v -> DynChan.send (DynChan.finalise name) v) names vs; + Lin.fresh cont +end diff --git a/lib/multicast/actionScatter.mli b/lib/multicast/actionScatter.mli index 38f68fc..e57781e 100644 --- a/lib/multicast/actionScatter.mli +++ b/lib/multicast/actionScatter.mli @@ -1,18 +1,20 @@ -type _ scatter -type (_, _) scatter_val +module Make (C : S.CHANNEL) : sig + type _ scatter + type (_, _) scatter_val -val make_scatter : - ('a, 'b) Rows.method_ -> - ('b, 'c scatter) Rows.method_ -> - int DynChan.endpoint list -> - 'c LinState.t -> - 'a LinState.t + val make_scatter : + ('a, 'b) Rows.method_ -> + ('b, 'c scatter) Rows.method_ -> + int C.endpoint list -> + 'c LinState.t -> + 'a LinState.t -val make_scatter_val : - ('a, ('v, 'c) scatter_val) Rows.method_ -> - 'v DynChan.endpoint list -> - 'c LinState.t -> - 'a LinState.t + val make_scatter_val : + ('a, ('v, 'c) scatter_val) Rows.method_ -> + 'v C.endpoint list -> + 'c LinState.t -> + 'a LinState.t -val scatter : 'a scatter -> 'a -val scatter_val : ('v, 'a) scatter_val -> 'v list -> 'a + val scatter : 'a scatter -> 'a + val scatter_val : ('v, 'a) scatter_val -> 'v list -> 'a +end diff --git a/lib/multicast/multicast.ml b/lib/multicast/multicast.ml index b7881b0..17af5b4 100644 --- a/lib/multicast/multicast.ml +++ b/lib/multicast/multicast.ml @@ -2,142 +2,152 @@ open BasicCombinators module Sessions = Hlist.Make (LinState) open Sessions -type 's scatter = 's ActionScatter.scatter -type 's gather = 's ActionGather.gather -type ('v, 's) scatter_val = ('v, 's) ActionScatter.scatter_val -type ('v, 's) gather_val = ('v, 's) ActionGather.gather_val -type 's many = 's ActionMany.many - -type chan_table = { - process_count : (string, int) Hashtbl.t; - table : (string * string, DynChan.chan list) Hashtbl.t; -} - -type param += P : ((_, _, _, _, _, _) role * int) -> param - -module MulticastEnv : EnvSpec with type entry = chan_table = struct - type entry = chan_table - type env_entry += E of entry - - let name = "multicast" - - let make_default () = - { process_count = Hashtbl.create 42; table = Hashtbl.create 42 } - - let update param t = - match param with - | P (role, cnt) -> - Hashtbl.replace t.process_count role.role_label.method_name cnt - | _ -> () +module Make (DynChan : S.CHANNEL) = struct + module ActionScatter = ActionScatter.Make (DynChan) + module ActionGather = ActionGather.Make (DynChan) + module ActionMany0 = ActionMany + module ActionMany = ActionMany0.Make (DynChan) + + type 's scatter = 's ActionScatter.scatter + type 's gather = 's ActionGather.gather + type ('v, 's) scatter_val = ('v, 's) ActionScatter.scatter_val + type ('v, 's) gather_val = ('v, 's) ActionGather.gather_val + type 's many = 's ActionMany0.many + + type chan_table = { + process_count : (string, int) Hashtbl.t; + table : (string * string, DynChan.t list) Hashtbl.t; + } + + type param += P : ((_, _, _, _, _, _) role * int) -> param + + module MulticastEnv : EnvSpec with type entry = chan_table = struct + type entry = chan_table + type env_entry += E of entry + + let name = "multicast" + + let make_default () = + { process_count = Hashtbl.create 42; table = Hashtbl.create 42 } + + let update param t = + match param with + | P (role, cnt) -> + Hashtbl.replace t.process_count role.role_label.method_name cnt + | _ -> () + end + + module Lookup = RegisterEnvSpec (MulticastEnv) + + let get_process_count (t : chan_table) role = + Option.value ~default:1 (Hashtbl.find_opt t.process_count role) + + let get_chan (t : chan_table) (key : string * string) = + match Hashtbl.find_opt t.table key with + | Some ch -> ch + | None -> + let from, to_ = key in + let from_count = get_process_count t from in + let to_count = get_process_count t to_ in + let ch = + List.init (from_count * to_count) (fun _i -> DynChan.make ()) + in + Hashtbl.add t.table key ch; + ch + + (* scatter *) + let ( -->@@ ) ra rb lab g env = + let g = g env in + let env = Lookup.lookup env in + let to_count = get_process_count env rb.role_label.method_name in + let chs = + get_chan env (ra.role_label.method_name, rb.role_label.method_name) + in + let keys = List.map DynChan.new_endpoint chs in + let b = seq_get rb.role_index g in + let g = + seq_put rb.role_index g + (ActionMany.make_branches ~count:to_count ra.role_label lab.var keys b) + in + let a = seq_get ra.role_index g in + let g = + seq_put ra.role_index g + (ActionScatter.make_scatter rb.role_label lab.obj keys a) + in + g + + (** gather *) + let ( @@--> ) ra rb lab g env = + let g = g env in + let env = Lookup.lookup env in + let from_count = get_process_count env ra.role_label.method_name in + let chs = + get_chan env (ra.role_label.method_name, rb.role_label.method_name) + in + let keys = List.map DynChan.new_endpoint chs in + let b = seq_get rb.role_index g in + let g = + seq_put rb.role_index g + (ActionGather.make_gather ra.role_label lab.var keys b) + in + let a = seq_get ra.role_index g in + let g = + seq_put ra.role_index g + (ActionMany.make_selects ~count:from_count rb.role_label lab.obj keys a) + in + g + + (* scatter (value) *) + let ( ==>@@ ) ra rb g env = + let g = g env in + let env = Lookup.lookup env in + let to_count = get_process_count env rb.role_label.method_name in + let chs = + get_chan env (ra.role_label.method_name, rb.role_label.method_name) + in + let keys = List.map DynChan.new_endpoint chs in + let b = seq_get rb.role_index g in + let g = + seq_put rb.role_index g + (ActionMany.make_inps ~count:to_count ra.role_label keys b) + in + let a = seq_get ra.role_index g in + let g = + seq_put ra.role_index g + (ActionScatter.make_scatter_val rb.role_label keys a) + in + g + + (** gather (val) *) + let ( @@==> ) ra rb g env = + let g = g env in + let env = Lookup.lookup env in + let from_count = get_process_count env ra.role_label.method_name in + let chs = + get_chan env (ra.role_label.method_name, rb.role_label.method_name) + in + let keys = List.map DynChan.new_endpoint chs in + let b = seq_get rb.role_index g in + let g = + seq_put rb.role_index g + (ActionGather.make_gather_val ra.role_label keys b) + in + let a = seq_get ra.role_index g in + let g = + seq_put ra.role_index g + (ActionMany.make_outs ~count:from_count rb.role_label keys a) + in + g + + let many_at role g env = + let g = g env in + let env = Lookup.lookup env in + let count = get_process_count env role.role_label.method_name in + seq_put role.role_index g (ActionMany.units ~count) + + let get_many = ActionMany.get_many + let scatter = ActionScatter.scatter + let gather = ActionGather.gather + let scatter_val = ActionScatter.scatter_val + let gather_val = ActionGather.gather_val end - -module Lookup = RegisterEnvSpec (MulticastEnv) - -let get_process_count (t : chan_table) role = - Option.value ~default:1 (Hashtbl.find_opt t.process_count role) - -let get_chan (t : chan_table) (key : string * string) = - match Hashtbl.find_opt t.table key with - | Some ch -> ch - | None -> - let from, to_ = key in - let from_count = get_process_count t from in - let to_count = get_process_count t to_ in - let ch = List.init (from_count * to_count) (fun _i -> DynChan.make ()) in - Hashtbl.add t.table key ch; - ch - -(* scatter *) -let ( -->@@ ) ra rb lab g env = - let g = g env in - let env = Lookup.lookup env in - let to_count = get_process_count env rb.role_label.method_name in - let chs = - get_chan env (ra.role_label.method_name, rb.role_label.method_name) - in - let keys = List.map DynChan.new_endpoint chs in - let b = seq_get rb.role_index g in - let g = - seq_put rb.role_index g - (ActionMany.make_branches ~count:to_count ra.role_label lab.var keys b) - in - let a = seq_get ra.role_index g in - let g = - seq_put ra.role_index g - (ActionScatter.make_scatter rb.role_label lab.obj keys a) - in - g - -(** gather *) -let ( @@--> ) ra rb lab g env = - let g = g env in - let env = Lookup.lookup env in - let from_count = get_process_count env ra.role_label.method_name in - let chs = - get_chan env (ra.role_label.method_name, rb.role_label.method_name) - in - let keys = List.map DynChan.new_endpoint chs in - let b = seq_get rb.role_index g in - let g = - seq_put rb.role_index g - (ActionGather.make_gather ra.role_label lab.var keys b) - in - let a = seq_get ra.role_index g in - let g = - seq_put ra.role_index g - (ActionMany.make_selects ~count:from_count rb.role_label lab.obj keys a) - in - g - -(* scatter (value) *) -let ( ==>@@ ) ra rb g env = - let g = g env in - let env = Lookup.lookup env in - let to_count = get_process_count env rb.role_label.method_name in - let chs = - get_chan env (ra.role_label.method_name, rb.role_label.method_name) - in - let keys = List.map DynChan.new_endpoint chs in - let b = seq_get rb.role_index g in - let g = - seq_put rb.role_index g - (ActionMany.make_inps ~count:to_count ra.role_label keys b) - in - let a = seq_get ra.role_index g in - let g = - seq_put ra.role_index g - (ActionScatter.make_scatter_val rb.role_label keys a) - in - g - -(** gather (val) *) -let ( @@==> ) ra rb g env = - let g = g env in - let env = Lookup.lookup env in - let from_count = get_process_count env ra.role_label.method_name in - let chs = - get_chan env (ra.role_label.method_name, rb.role_label.method_name) - in - let keys = List.map DynChan.new_endpoint chs in - let b = seq_get rb.role_index g in - let g = - seq_put rb.role_index g (ActionGather.make_gather_val ra.role_label keys b) - in - let a = seq_get ra.role_index g in - let g = - seq_put ra.role_index g - (ActionMany.make_outs ~count:from_count rb.role_label keys a) - in - g - -let many_at role g env = - let g = g env in - let env = Lookup.lookup env in - let count = get_process_count env role.role_label.method_name in - seq_put role.role_index g (ActionMany.units ~count) - -let get_many = ActionMany.get_many -let scatter = ActionScatter.scatter -let gather = ActionGather.gather -let scatter_val = ActionScatter.scatter_val -let gather_val = ActionGather.gather_val diff --git a/lib/multicast/multicast.mli b/lib/multicast/multicast.mli index 4cb0cf0..3298098 100644 --- a/lib/multicast/multicast.mli +++ b/lib/multicast/multicast.mli @@ -1,46 +1,48 @@ open BasicCombinators -type 's scatter -type 's gather -type ('v, 's) scatter_val -type ('v, 's) gather_val -type 's many - -val ( -->@@ ) : - ('a, 'b, 'c, 'd, 'e, 'f Unicast.branch) BasicCombinators.role -> - ('g many, 'e many, 'h, 'c, 'b, 'i) BasicCombinators.role -> - ('i, 'a scatter, 'f, 'g) BasicCombinators.label -> - 'h global -> - 'd global - -val ( @@--> ) : - ('a many, 'b many, 'c, 'd, 'e, 'f gather) BasicCombinators.role -> - ('g, 'e, 'h, 'c, 'b, 'i) BasicCombinators.role -> - ('i, 'a Unicast.select, 'f, 'g) BasicCombinators.label -> - 'h global -> - 'd global - -val ( ==>@@ ) : - ('a, 'b, 'c, 'd, 'e, ('f, 'g) ActionInp.inp) role -> - ('g many, 'e many, 'h, 'c, 'b, ('f, 'a) ActionScatter.scatter_val) role -> - 'h global -> - 'd global - -val ( @@==> ) : - ('a many, 'b many, 'c, 'd, 'e, ('f, 'g) ActionGather.gather_val) role -> - ('g, 'e, 'h, 'c, 'b, ('f, 'a) ActionOut.out) role -> - 'h global -> - 'd global - -val many_at : - (unit, unit many, 'b, 'c, 'd, 'e) BasicCombinators.role -> - 'b global -> - 'c global - -type param += P : ((_, _, _, _, _, _) role * int) -> param - -val get_many : 'a many -> 'a list -val scatter : 'a scatter -> 'a -val gather : 'a gather -> 'a -val scatter_val : ('v, 'a) scatter_val -> 'v list -> 'a -val gather_val : ('v, 'a) gather_val -> 'v list * 'a +module Make (C : S.CHANNEL) : sig + type 's scatter + type 's gather + type ('v, 's) scatter_val + type ('v, 's) gather_val + type 's many + + val ( -->@@ ) : + ('a, 'b, 'c, 'd, 'e, 'f Unicast.Make(C).branch) BasicCombinators.role -> + ('g many, 'e many, 'h, 'c, 'b, 'i) BasicCombinators.role -> + ('i, 'a scatter, 'f, 'g) BasicCombinators.label -> + 'h global -> + 'd global + + val ( @@--> ) : + ('a many, 'b many, 'c, 'd, 'e, 'f gather) BasicCombinators.role -> + ('g, 'e, 'h, 'c, 'b, 'i) BasicCombinators.role -> + ('i, 'a Unicast.Make(C).select, 'f, 'g) BasicCombinators.label -> + 'h global -> + 'd global + + val ( ==>@@ ) : + ('a, 'b, 'c, 'd, 'e, ('f, 'g) Unicast.Make(C).inp) role -> + ('g many, 'e many, 'h, 'c, 'b, ('f, 'a) ActionScatter.Make(C).scatter_val) role -> + 'h global -> + 'd global + + val ( @@==> ) : + ('a many, 'b many, 'c, 'd, 'e, ('f, 'g) ActionGather.Make(C).gather_val) role -> + ('g, 'e, 'h, 'c, 'b, ('f, 'a) Unicast.Make(C).out) role -> + 'h global -> + 'd global + + val many_at : + (unit, unit many, 'b, 'c, 'd, 'e) BasicCombinators.role -> + 'b global -> + 'c global + + type param += P : ((_, _, _, _, _, _) role * int) -> param + + val get_many : 'a many -> 'a list + val scatter : 'a scatter -> 'a + val gather : 'a gather -> 'a + val scatter_val : ('v, 'a) scatter_val -> 'v list -> 'a + val gather_val : ('v, 'a) gather_val -> 'v list * 'a +end diff --git a/lib/s.ml b/lib/s.ml new file mode 100644 index 0000000..c5aa3db --- /dev/null +++ b/lib/s.ml @@ -0,0 +1,11 @@ +module type CHANNEL = sig + type t + type 'a endpoint + + val make : unit -> t + val new_endpoint : t -> 'a endpoint + val unify : 'a endpoint -> 'a endpoint -> unit + val finalise : 'a endpoint -> 'a endpoint + val send : 'a endpoint -> 'a -> unit + val receive : 'a endpoint -> 'a +end diff --git a/lib/unicast/actionInp.ml b/lib/unicast/actionInp.ml index 509cae5..255bb86 100644 --- a/lib/unicast/actionInp.ml +++ b/lib/unicast/actionInp.ml @@ -2,87 +2,90 @@ module Context = State.Context open Rows type tag = int -type 'var branch_ = (tag DynChan.endpoint * 'var InpChoice.t list) Lazy.t -type 'var branch = 'var branch_ Lin.lin - -let make_branch0 constr name s = - Lazy.from_val (name, [ InpChoice.make constr s ]) - -let branch_op0 (type vars) : vars branch_ State.op = - let module M = struct - type nonrec a = vars branch_ - - let determinise ctx inp = - lazy - begin - let (lazy (name, exts)) = inp in - (name, List.map (InpChoice.determinise ctx) exts) - end - - let merge ctx inp1 inp2 = - lazy - begin - let (lazy (name1, exts1)), (lazy (name2, exts2)) = (inp1, inp2) in - DynChan.unify name1 name2; - (name1, InpChoice.merge ctx exts1 exts2) - end - - let force ctx inp = - let (lazy (name, exts)) = inp in - ignore (DynChan.finalise name); - exts |> List.iter (InpChoice.force ctx) - - let to_string ctx s = - "?{" - ^ (if Lazy.is_val s then - String.concat "," - (List.map (InpChoice.to_string ctx) (snd (Lazy.force s))) - else "") - ^ "}" - end in - (module M) - -let branch_op role = - LinState.gen_op @@ State.obj_op role @@ LinState.lin_op branch_op0 - -let make_branch role constr name (s : _ LinState.t) = - let st = - (role.make_obj |> Lin.map_gen) @@ Lin.declare (make_branch0 constr name s) - in - PowState.make (branch_op role) st - -let branch (inp : _ branch) = - let name, items = Lazy.force @@ Lin.use inp in - items - |> List.map InpChoice.match_item - |> List.assoc (DynChan.receive (DynChan.finalise name)) - |> Lazy.force - -type ('v, 's) inp_ = 'v DynChan.endpoint * 's LinState.t -type ('v, 's) inp = ('v, 's) inp_ Lin.lin - -let inp_op0 (type v s) : (v, s) inp_ State.op = - let module M = struct - type a = (v, s) inp_ - - let determinise ctx (ch, s) = (ch, PowState.determinise ctx s) - - let merge ctx (ch1, s1) (ch2, s2) = - DynChan.unify ch1 ch2; - (ch1, PowState.merge ctx s1 s2) - - let force ctx (_, s) = PowState.force ctx s - let to_string ctx (_, s) = "?." ^ PowState.to_string ctx s - end in - (module M) - -let inp_op role = State.obj_op role @@ LinState.lin_op inp_op0 - -let make_inp role chan cont = - let st = (role.make_obj |> Lin.map_gen) @@ Lin.declare (chan, cont) in - PowState.make (LinState.gen_op (inp_op role)) st - -let receive inp = - let ch, cont = Lin.use inp in - ( DynChan.receive (DynChan.finalise ch), - Lin.fresh (PowState.ensure_determinised cont) ) + +module Make (DynChan : S.CHANNEL) = struct + type 'var branch_ = (tag DynChan.endpoint * 'var InpChoice.t list) Lazy.t + type 'var branch = 'var branch_ Lin.lin + + let make_branch0 constr name s = + Lazy.from_val (name, [ InpChoice.make constr s ]) + + let branch_op0 (type vars) : vars branch_ State.op = + let module M = struct + type nonrec a = vars branch_ + + let determinise ctx inp = + lazy + begin + let (lazy (name, exts)) = inp in + (name, List.map (InpChoice.determinise ctx) exts) + end + + let merge ctx inp1 inp2 = + lazy + begin + let (lazy (name1, exts1)), (lazy (name2, exts2)) = (inp1, inp2) in + DynChan.unify name1 name2; + (name1, InpChoice.merge ctx exts1 exts2) + end + + let force ctx inp = + let (lazy (name, exts)) = inp in + ignore (DynChan.finalise name); + exts |> List.iter (InpChoice.force ctx) + + let to_string ctx s = + "?{" + ^ (if Lazy.is_val s then + String.concat "," + (List.map (InpChoice.to_string ctx) (snd (Lazy.force s))) + else "") + ^ "}" + end in + (module M) + + let branch_op role = + LinState.gen_op @@ State.obj_op role @@ LinState.lin_op branch_op0 + + let make_branch role constr name (s : _ LinState.t) = + let st = + (role.make_obj |> Lin.map_gen) @@ Lin.declare (make_branch0 constr name s) + in + PowState.make (branch_op role) st + + let branch (inp : _ branch) = + let name, items = Lazy.force @@ Lin.use inp in + items + |> List.map InpChoice.match_item + |> List.assoc (DynChan.receive (DynChan.finalise name)) + |> Lazy.force + + type ('v, 's) inp_ = 'v DynChan.endpoint * 's LinState.t + type ('v, 's) inp = ('v, 's) inp_ Lin.lin + + let inp_op0 (type v s) : (v, s) inp_ State.op = + let module M = struct + type a = (v, s) inp_ + + let determinise ctx (ch, s) = (ch, PowState.determinise ctx s) + + let merge ctx (ch1, s1) (ch2, s2) = + DynChan.unify ch1 ch2; + (ch1, PowState.merge ctx s1 s2) + + let force ctx (_, s) = PowState.force ctx s + let to_string ctx (_, s) = "?." ^ PowState.to_string ctx s + end in + (module M) + + let inp_op role = State.obj_op role @@ LinState.lin_op inp_op0 + + let make_inp role chan cont = + let st = (role.make_obj |> Lin.map_gen) @@ Lin.declare (chan, cont) in + PowState.make (LinState.gen_op (inp_op role)) st + + let receive inp = + let ch, cont = Lin.use inp in + ( DynChan.receive (DynChan.finalise ch), + Lin.fresh (PowState.ensure_determinised cont) ) +end diff --git a/lib/unicast/actionInp.mli b/lib/unicast/actionInp.mli index 6605b8a..0b1a160 100644 --- a/lib/unicast/actionInp.mli +++ b/lib/unicast/actionInp.mli @@ -1,18 +1,20 @@ -type 'var branch -type ('v, 's) inp +module Make (C : S.CHANNEL) : sig + type 'var branch + type ('v, 's) inp -val make_branch : - ('a, 'c branch) Rows.method_ -> - ('c, 'd) Rows.constr -> - int DynChan.endpoint -> - 'd LinState.t -> - 'a LinState.t + val make_branch : + ('a, 'c branch) Rows.method_ -> + ('c, 'd) Rows.constr -> + int C.endpoint -> + 'd LinState.t -> + 'a LinState.t -val make_inp : - ('a, ('v, 'c) inp) Rows.method_ -> - 'v DynChan.endpoint -> - 'c LinState.t -> - 'a LinState.t + val make_inp : + ('a, ('v, 'c) inp) Rows.method_ -> + 'v C.endpoint -> + 'c LinState.t -> + 'a LinState.t -val branch : 'var branch -> 'var -val receive : ('v, 's) inp -> 'v * 's + val branch : 'var branch -> 'var + val receive : ('v, 's) inp -> 'v * 's +end diff --git a/lib/unicast/actionOut.ml b/lib/unicast/actionOut.ml index 3507798..0a730fa 100644 --- a/lib/unicast/actionOut.ml +++ b/lib/unicast/actionOut.ml @@ -2,67 +2,70 @@ open Rows module Context = State.Context type tag = int -type ('v, 's) out_ = string * 'v DynChan.endpoint * 's LinState.t lazy_t -type ('v, 'a) out = ('v, 'a) out_ Lin.lin -type 's select = (tag, 's) out -let out_op0 (type v cont) : (v, cont) out_ State.op = - let module M = struct - type nonrec a = (v, cont) out_ +module Make (DynChan : S.CHANNEL) = struct + type ('v, 's) out_ = string * 'v DynChan.endpoint * 's LinState.t lazy_t + type ('v, 'a) out = ('v, 'a) out_ Lin.lin + type 's select = (tag, 's) out - let determinise ctx (tag, name, (lazy cont)) = - (tag, name, lazy (PowState.determinise ctx cont)) + let out_op0 (type v cont) : (v, cont) out_ State.op = + let module M = struct + type nonrec a = (v, cont) out_ - let merge ctx (tag1, name1, cont1) (tag2, name2, cont2) = - assert (tag1 = tag2); - DynChan.unify name1 name2; - ( tag1, - name1, - lazy (PowState.merge ctx (Lazy.force cont1) (Lazy.force cont2)) ) + let determinise ctx (tag, name, (lazy cont)) = + (tag, name, lazy (PowState.determinise ctx cont)) - let force ctx (_, name, cont) = - ignore (DynChan.finalise name); - PowState.force ctx (Lazy.force cont) + let merge ctx (tag1, name1, cont1) (tag2, name2, cont2) = + assert (tag1 = tag2); + DynChan.unify name1 name2; + ( tag1, + name1, + lazy (PowState.merge ctx (Lazy.force cont1) (Lazy.force cont2)) ) - let to_string ctx (_, _, cont) = - (*FIXME:use label*) - if Lazy.is_val cont then - let cont = Lazy.force cont in - PowState.to_string ctx cont - else "" - end in - (module M) + let force ctx (_, name, cont) = + ignore (DynChan.finalise name); + PowState.force ctx (Lazy.force cont) -let out_op role = State.obj_op role @@ LinState.lin_op out_op0 + let to_string ctx (_, _, cont) = + (*FIXME:use label*) + if Lazy.is_val cont then + let cont = Lazy.force cont in + PowState.to_string ctx cont + else "" + end in + (module M) -let select_op role label = - State.obj_op role @@ State.obj_op label @@ LinState.lin_op out_op0 + let out_op role = State.obj_op role @@ LinState.lin_op out_op0 -let make_out role name s : _ LinState.t = - let st = - (role.make_obj |> Lin.map_gen) - @@ Lin.declare ("_out" (* FIXME *), name, Lazy.from_val s) - in - let op = LinState.gen_op (out_op role) in - PowState.make op st + let select_op role label = + State.obj_op role @@ State.obj_op label @@ LinState.lin_op out_op0 -let make_select role label name s : _ LinState.t = - let st = - Lin.map_gen (fun t -> role.make_obj @@ label.make_obj t) - @@ Lin.declare (label.method_name, name, Lazy.from_val s) - in - let op = LinState.gen_op @@ select_op role label in - PowState.make op st + let make_out role name s : _ LinState.t = + let st = + (role.make_obj |> Lin.map_gen) + @@ Lin.declare ("_out" (* FIXME *), name, Lazy.from_val s) + in + let op = LinState.gen_op (out_op role) in + PowState.make op st -let select out = - let labname, name, cont = Lin.use out in - let tag = Btype.hash_variant labname in - let cont = PowState.ensure_determinised (Lazy.force cont) in - DynChan.send (DynChan.finalise name) tag; - Lin.fresh cont + let make_select role label name s : _ LinState.t = + let st = + Lin.map_gen (fun t -> role.make_obj @@ label.make_obj t) + @@ Lin.declare (label.method_name, name, Lazy.from_val s) + in + let op = LinState.gen_op @@ select_op role label in + PowState.make op st -let send out v = - let _, name, cont = Lin.use out in - let cont = PowState.ensure_determinised (Lazy.force cont) in - DynChan.send (DynChan.finalise name) v; - Lin.fresh cont + let select out = + let labname, name, cont = Lin.use out in + let tag = Btype.hash_variant labname in + let cont = PowState.ensure_determinised (Lazy.force cont) in + DynChan.send (DynChan.finalise name) tag; + Lin.fresh cont + + let send out v = + let _, name, cont = Lin.use out in + let cont = PowState.ensure_determinised (Lazy.force cont) in + DynChan.send (DynChan.finalise name) v; + Lin.fresh cont +end diff --git a/lib/unicast/actionOut.mli b/lib/unicast/actionOut.mli index 3060dc1..20274e3 100644 --- a/lib/unicast/actionOut.mli +++ b/lib/unicast/actionOut.mli @@ -1,19 +1,21 @@ -type 'a select -type ('v, 'a) out +module Make (C : S.CHANNEL) : sig + type 'a select + type ('v, 'a) out -val make_select : - ('a, 'b) Rows.method_ -> - ('b, 'c select) Rows.method_ -> - int DynChan.endpoint -> - 'c LinState.t -> - 'a LinState.t + val make_select : + ('a, 'b) Rows.method_ -> + ('b, 'c select) Rows.method_ -> + int C.endpoint -> + 'c LinState.t -> + 'a LinState.t -val select : 's select -> 's + val select : 's select -> 's -val make_out : - ('a, ('v, 'c) out) Rows.method_ -> - 'v DynChan.endpoint -> - 'c LinState.t -> - 'a LinState.t + val make_out : + ('a, ('v, 'c) out) Rows.method_ -> + 'v C.endpoint -> + 'c LinState.t -> + 'a LinState.t -val send : ('v, 's) out -> 'v -> 's + val send : ('v, 's) out -> 'v -> 's +end diff --git a/lib/unicast/unicast.ml b/lib/unicast/unicast.ml index a1cc2bc..4f60853 100644 --- a/lib/unicast/unicast.ml +++ b/lib/unicast/unicast.ml @@ -2,68 +2,72 @@ open BasicCombinators module Sessions = Hlist.Make (LinState) open Sessions -type 's select = 's ActionOut.select -type 's branch = 's ActionInp.branch -type ('v, 's) out = ('v, 's) ActionOut.out -type ('v, 's) inp = ('v, 's) ActionInp.inp -type chan = DynChan.chan +module Make (DynChan : S.CHANNEL) = struct + module ActionOut = ActionOut.Make (DynChan) + module ActionInp = ActionInp.Make (DynChan) -let close () = () + type 's select = 's ActionOut.select + type 's branch = 's ActionInp.branch + type ('v, 's) out = ('v, 's) ActionOut.out + type ('v, 's) inp = ('v, 's) ActionInp.inp -type chan_table = (string * string, DynChan.chan) Hashtbl.t + let close () = () -module UnicastEnv : EnvSpec with type entry = chan_table = struct - type entry = chan_table - type env_entry += E of entry + type chan_table = (string * string, DynChan.t) Hashtbl.t - let name = "unicast" - let make_default () = Hashtbl.create 42 - let update _param _tbl = () -end + module UnicastEnv : EnvSpec with type entry = chan_table = struct + type entry = chan_table + type env_entry += E of entry + + let name = "unicast" + let make_default () = Hashtbl.create 42 + let update _param _tbl = () + end -module Lookup = RegisterEnvSpec (UnicastEnv) + module Lookup = RegisterEnvSpec (UnicastEnv) -let lookup (t : chan_table) (key : string * string) = - match Hashtbl.find_opt t key with - | Some ch -> ch - | None -> - let ch = DynChan.make () in - Hashtbl.add t key ch; - ch + let lookup (t : chan_table) (key : string * string) = + match Hashtbl.find_opt t key with + | Some ch -> ch + | None -> + let ch = DynChan.make () in + Hashtbl.add t key ch; + ch -let ( --> ) ra rb lab g env = - let g = g env in - let ch = - lookup (Lookup.lookup env) - (ra.role_label.method_name, rb.role_label.method_name) - in - let key = DynChan.new_endpoint ch in - let b = seq_get rb.role_index g in - let g = - seq_put rb.role_index g (ActionInp.make_branch ra.role_label lab.var key b) - in - let a = seq_get ra.role_index g in - let g = - seq_put ra.role_index g (ActionOut.make_select rb.role_label lab.obj key a) - in - g + let ( --> ) ra rb lab g env = + let g = g env in + let ch = + lookup (Lookup.lookup env) + (ra.role_label.method_name, rb.role_label.method_name) + in + let key = DynChan.new_endpoint ch in + let b = seq_get rb.role_index g in + let g = + seq_put rb.role_index g + (ActionInp.make_branch ra.role_label lab.var key b) + in + let a = seq_get ra.role_index g in + let g = + seq_put ra.role_index g + (ActionOut.make_select rb.role_label lab.obj key a) + in + g -let ( ==> ) ra rb g env = - let g = g env in - let ch = - lookup (Lookup.lookup env) - (ra.role_label.method_name, rb.role_label.method_name) - in - let key = DynChan.new_endpoint ch in - let b = seq_get rb.role_index g in - let g = seq_put rb.role_index g (ActionInp.make_inp ra.role_label key b) in - let a = seq_get ra.role_index g in - let g = - seq_put ra.role_index g (ActionOut.make_out rb.role_label key a) - in - g + let ( ==> ) ra rb g env = + let g = g env in + let ch = + lookup (Lookup.lookup env) + (ra.role_label.method_name, rb.role_label.method_name) + in + let key = DynChan.new_endpoint ch in + let b = seq_get rb.role_index g in + let g = seq_put rb.role_index g (ActionInp.make_inp ra.role_label key b) in + let a = seq_get ra.role_index g in + let g = seq_put ra.role_index g (ActionOut.make_out rb.role_label key a) in + g -let select = ActionOut.select -let branch = ActionInp.branch -let send = ActionOut.send -let receive = ActionInp.receive + let select = ActionOut.select + let branch = ActionInp.branch + let send = ActionOut.send + let receive = ActionInp.receive +end diff --git a/lib/unicast/unicast.mli b/lib/unicast/unicast.mli index e94863a..5d3b004 100644 --- a/lib/unicast/unicast.mli +++ b/lib/unicast/unicast.mli @@ -1,26 +1,27 @@ open BasicCombinators -type 's select = 's ActionOut.select -type 's branch = 's ActionInp.branch -type ('v, 's) out = ('v, 's) ActionOut.out -type ('v, 's) inp = ('v, 's) ActionInp.inp -type chan +module Make (C : S.CHANNEL) : sig + type 's select = 's ActionOut.Make(C).select + type 's branch = 's ActionInp.Make(C).branch + type ('v, 's) out = ('v, 's) ActionOut.Make(C).out + type ('v, 's) inp = ('v, 's) ActionInp.Make(C).inp -val select : 'a select -> 'a -val branch : 'a branch -> 'a -val send : ('v, 'a) out -> 'v -> 'a -val receive : ('v, 'a) inp -> 'v * 'a -val close : unit -> unit + val select : 'a select -> 'a + val branch : 'a branch -> 'a + val send : ('v, 'a) out -> 'v -> 'a + val receive : ('v, 'a) inp -> 'v * 'a + val close : unit -> unit -val ( --> ) : - ('a, 'b, 'c, 'd, 'e, 'f branch) role -> - ('g, 'e, 'h, 'c, 'b, 'i) role -> - ('i, 'a select, 'f, 'g) label -> - 'h global -> - 'd global + val ( --> ) : + ('a, 'b, 'c, 'd, 'e, 'f branch) role -> + ('g, 'e, 'h, 'c, 'b, 'i) role -> + ('i, 'a select, 'f, 'g) label -> + 'h global -> + 'd global -val ( ==> ) : - ('a, 'b, 'c, 'd, 'e, ('f, 'g) inp) role -> - ('g, 'e, 'h, 'c, 'b, ('f, 'a) out) role -> - 'h global -> - 'd global + val ( ==> ) : + ('a, 'b, 'c, 'd, 'e, ('f, 'g) inp) role -> + ('g, 'e, 'h, 'c, 'b, ('f, 'a) out) role -> + 'h global -> + 'd global +end diff --git a/mpst-basic.opam b/mpst-basic.opam new file mode 100644 index 0000000..ba9d094 --- /dev/null +++ b/mpst-basic.opam @@ -0,0 +1,38 @@ +opam-version: "2.0" +version: "0.0.1" +synopsis: "OCaml-MPST basic library [WIP]" +description: "OCaml-MPST basic library [WIP]" +maintainer: ["keigo.imai@gmail.com"] +authors: ["Keigo Imai"] +homepage: "https://github.com/keigoi/ocaml-mpst" +doc: "https://github.com/keigoi/ocaml-mpst" +bug-reports: "https://github.com/keigoi/ocaml-mpst/issues" +depends: [ + "ocaml" {>= "4.12.0"} + "dune" {>= "2.8"} + "mpst" + "hlist" + "rows" + "ppxlib" {>= "0.19.0"} + "ounit" {with-test} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/keigoi/ocaml-mpst.git" +pin-depends: [ + [ "hlist.dev" "git+https://github.com/keigoi/hlist-ocaml.git"] + [ "rows.dev" "git+https://github.com/keigoi/rows-ocaml.git"] +] diff --git a/tests/dune b/tests/dune index 6145f93..90facd7 100644 --- a/tests/dune +++ b/tests/dune @@ -3,51 +3,51 @@ (modules test_protocols_mergefail) (preprocess (pps mpst.ppx)) - (libraries mpst oUnit)) + (libraries mpst-basic oUnit)) (test (name test_protocols_merge) (modules test_protocols_merge) (preprocess (pps mpst.ppx)) - (libraries mpst oUnit)) + (libraries mpst-basic oUnit)) (test (name test_run_loop) (modules test_run_loop) (preprocess (pps mpst.ppx)) - (libraries mpst oUnit)) + (libraries mpst-basic oUnit)) (test (name test_protocols_multicast) (modules test_protocols_multicast) (preprocess (pps mpst.ppx)) - (libraries mpst oUnit)) + (libraries mpst-basic oUnit)) (test (name test_run_multicast) (modules test_run_multicast) (preprocess (pps mpst.ppx)) - (libraries mpst oUnit)) + (libraries mpst-basic oUnit)) (test (name test_linearity_fail) (modules test_linearity_fail) (preprocess (staged_pps mpst.ppx.ty)) - (libraries mpst oUnit)) + (libraries mpst-basic oUnit)) (test (name test_ppx_ty) (modules test_ppx_ty) (preprocess (staged_pps mpst.ppx.ty)) - (libraries mpst oUnit)) + (libraries mpst-basic oUnit)) (test (name test_dynChan) (modules test_dynChan) - (libraries mpst oUnit)) + (libraries mpst-basic oUnit)) diff --git a/tests/test_dynChan.ml b/tests/test_dynChan.ml index ae46d33..17dbf84 100644 --- a/tests/test_dynChan.ml +++ b/tests/test_dynChan.ml @@ -1,4 +1,4 @@ -module DynChan = Mpst.DynChan +module DynChan = Mpst_basic.DynChan open OUnit let test_unify () = diff --git a/tests/test_linearity_fail.ml b/tests/test_linearity_fail.ml index dabdaf7..f313e17 100644 --- a/tests/test_linearity_fail.ml +++ b/tests/test_linearity_fail.ml @@ -1,5 +1,4 @@ -open Mpst.BasicCombinators -open Mpst.Unicast +open Mpst_basic open Rows open OUnit diff --git a/tests/test_ppx_ty.ml b/tests/test_ppx_ty.ml index a1119c2..32c63a9 100644 --- a/tests/test_ppx_ty.ml +++ b/tests/test_ppx_ty.ml @@ -1,5 +1,4 @@ -open Mpst.BasicCombinators -open Mpst.Unicast +open Mpst_basic open Rows open OUnit diff --git a/tests/test_protocols_merge.ml b/tests/test_protocols_merge.ml index 3237d90..d854876 100644 --- a/tests/test_protocols_merge.ml +++ b/tests/test_protocols_merge.ml @@ -1,5 +1,4 @@ -open Mpst.BasicCombinators -open Mpst.Unicast +open Mpst_basic open Rows open OUnit diff --git a/tests/test_protocols_mergefail.ml b/tests/test_protocols_mergefail.ml index 8c5a3df..dbe1840 100644 --- a/tests/test_protocols_mergefail.ml +++ b/tests/test_protocols_mergefail.ml @@ -1,5 +1,4 @@ -open Mpst.BasicCombinators -open Mpst.Unicast +open Mpst_basic open Rows open OUnit diff --git a/tests/test_protocols_multicast.ml b/tests/test_protocols_multicast.ml index c6ce593..f9156ed 100644 --- a/tests/test_protocols_multicast.ml +++ b/tests/test_protocols_multicast.ml @@ -1,6 +1,4 @@ -open Mpst.BasicCombinators -open Mpst.Unicast -open Mpst.Multicast +open Mpst_basic open Rows open OUnit @@ -13,7 +11,7 @@ open Util let extract_b_many g = let `cons(_,`cons(b,_)) = extract g in - ignore (Mpst.Multicast.get_many b) + ignore (get_many b) let test_multicast_projection_success () = let finish = many_at a Mpst.BasicCombinators.finish in diff --git a/tests/test_run_loop.ml b/tests/test_run_loop.ml index 9394797..2751a74 100644 --- a/tests/test_run_loop.ml +++ b/tests/test_run_loop.ml @@ -1,5 +1,4 @@ -open Mpst.BasicCombinators -open Mpst.Unicast +open Mpst_basic open Rows open OUnit diff --git a/tests/test_run_multicast.ml b/tests/test_run_multicast.ml index bf9b028..c0b1f4e 100644 --- a/tests/test_run_multicast.ml +++ b/tests/test_run_multicast.ml @@ -1,6 +1,4 @@ -open Mpst.BasicCombinators -open Mpst.Unicast -open Mpst.Multicast +open Mpst_basic open Rows open OUnit