Enum sesstype::global::Type

pub enum Type {
    Interact {
        p: Rc<Role>,
        q: Rc<Role>,
        g: HashMap<Message, Box<Type>>,
    },
    Recur {
        t: String,
        g: Box<Type>,
    },
    TypeVar {
        t: String,
    },
    End,
}

Global session types.

Definition 2.17

G ::= p → q : { lᵢ(Uᵢ).Gᵢ } where i ∈ I | μt.G | t | end

Variants

Interact

Interaction Type between two Roles.

G ::= p → q : { lᵢ(Uᵢ).Gᵢ } where i ∈ I

p and q are sender and receiver Roles respectively, and g is a mapping from Message to continuation Type.

Each map entry represents a Message sent by p to q, then the interaction proceeds as the continuation Type.

The Message should be distinct across in this Interaction Type.

Fields of Interact

p: Rc<Role>
q: Rc<Role>
g: HashMap<Message, Box<Type>>

Recur

Recursive Type for representing infinite behaviour.

G ::= μt.G

t is the type variable for identifying the recursion, and g is the Type for the continuation.

Fields of Recur

t: String
g: Box<Type>

TypeVar

Type Variable for use with Recur to represent infinite behaviour.

G ::= t

t is the previously defined type variable in Recur.

Fields of TypeVar

t: String

End

Terminated Type with no continuation.

G ::= end

Methods

impl Type

fn interaction(p: &Rc<Role>, q: &Rc<Role>) -> Box<Type>

Returns a heap-allocated Type::Interact with no interactions.

p and q are the sender and receiver Roles respectively.

fn add_message(
    interact_type: Box<Type>,
    m_i: Message,
    g_i: Box<Type>
) -> Box<Type>

Adds a message m_i (and its continuation g_i) to a Type::Interact and returns the updated Interact Type.

interact_type is the input Type, if it is not a Type::Interact it is returned unmodified.

fn recur(name: &str, body: Box<Type>) -> Box<Type>

Returns a heap-allocated Type::Recur.

name is the name given to the recursion scope. body is the recursion body.

fn typevar(name: &str) -> Box<Type>

Returns a heap-allocated Type::TypeVar.

name is the (previously defined) name of the recursion scope.

fn end() -> Box<Type>

Returns a heap-allocated Type::End.

All types should end in an instance of this.

Trait Implementations

impl Debug for Type

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl ToString for Type

fn to_string(&self) -> String

Converts the given value to a String.