Enum GType 

pub enum GType {
    Comm {
        sender: Role,
        receiver: Role,
        msg_ty: BaseType,
        cont: Box<GType>,
    },
    Choice {
        selector: Role,
        receiver: Role,
        branches: HashMap<String, GType>,
    },
    End,
    Rec(String, Box<GType>),
    Var(String),
}

A global session type (multiparty protocol specification).

Variants

Comm

p → q : T; G — p sends T to q, continues as G.

Fields

sender: Role

Sender role.

receiver: Role

Receiver role.

msg_ty: BaseType

Communicated type.

cont: Box<GType>

Continuation.

Choice

p → q { branch₁ : G₁, branch₂ : G₂ } — p selects a branch to q.

Fields

selector: Role

The role that makes the choice.

receiver: Role

The role that receives the choice.

branches: HashMap<String, GType>

Named branches (label → continuation).

End

Protocol end.

Rec(String, Box<GType>)

Recursive global type: μX.G.

Var(String)

Recursion variable.

Implementations

impl GType

pub fn participants(&self) -> HashSet<Role>

Collect all roles participating in this global type.

pub fn project(&self, role: &Role) -> LType

Project the global type onto a specific role.

Trait Implementations

impl Clone for GType

fn clone(&self) -> GType

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for GType

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.