Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion .github/workflows/workflow.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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

1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -42,3 +42,4 @@ ppx_tools/ppx_tools.install

_opam

.vscode
6 changes: 0 additions & 6 deletions .vscode/settings.json

This file was deleted.

3 changes: 1 addition & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
6 changes: 6 additions & 0 deletions basic/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
(library
(name mpst_basic)
(public_name mpst-basic)
(libraries mpst hlist rows threads compiler-libs.common))

(include_subdirs unqualified)
2 changes: 1 addition & 1 deletion lib/dynChan.ml → basic/dynChan.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions basic/dynChan.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
include Mpst.S.CHANNEL
4 changes: 4 additions & 0 deletions basic/mpst_basic.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
module DynChan = DynChan
include Mpst.BasicCombinators
include Mpst.Unicast.Make(DynChan)
include Mpst.Multicast.Make(DynChan)
3 changes: 1 addition & 2 deletions examples/calc/calc.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
open Mpst.BasicCombinators
open Mpst.Unicast
open Mpst_basic

type op = Add | Sub | Mul | Div

Expand Down
2 changes: 1 addition & 1 deletion examples/calc/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@
(modules calc)
(preprocess
(staged_pps mpst.ppx.ty))
(libraries mpst))
(libraries mpst-basic))
2 changes: 1 addition & 1 deletion examples/mixed_choice/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@
(modules mixed1)
(preprocess
(staged_pps mpst.ppx.ty))
(libraries mpst))
(libraries mpst-basic))
3 changes: 1 addition & 2 deletions examples/mixed_choice/mixed1.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
open Mpst.BasicCombinators
open Mpst.Unicast
open Mpst_basic

[%%declare_roles a, b, c]
[%%declare_labels req, resp, timeout]
Expand Down
9 changes: 0 additions & 9 deletions lib/dynChan.mli

This file was deleted.

184 changes: 96 additions & 88 deletions lib/multicast/actionGather.ml
Original file line number Diff line number Diff line change
@@ -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 "<lazy_inp>")
^ "}"
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 "<lazy_inp>")
^ "}"
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
32 changes: 17 additions & 15 deletions lib/multicast/actionGather.mli
Original file line number Diff line number Diff line change
@@ -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
Loading