Enum sesstype::local::Type

pub enum Type {
    Branch {
        p: Rc<Role>,
        s: HashMap<Message, Box<Type>>,
    },
    Select {
        p: Rc<Role>,
        s: HashMap<Message, Box<Type>>,
    },
    Recur {
        t: String,
        s: Box<Type>,
    },
    TypeVar {
        t: String,
    },
    End,
}

Local session types.

Definition 2.5

S ::= p &ᵢ ? lᵢ(Uᵢ).Sᵢ where i ∈ I | p ⊕ᵢ ! lᵢ(Uᵢ).Sᵢ where i ∈ I | μt.S | t | end

Variants

Branch

Branching Type receives a Message chosen by a Role.

S ::= p &ᵢ ? lᵢ(Uᵢ).Sᵢ where i ∈ I

p is the receiver Role, and s is the mapping of Message to continuation Type choices.

Each map entry represents a choice received by q, where the key of s (a Message) is the message expected, and the value is the continuation Type of the Branching Type.

Fields of Branch

p: Rc<Role>
s: HashMap<Message, Box<Type>>

Select

Selection Type sends a Message chosen by a Role.

S ::= p ⊕ᵢ ! lᵢ(Uᵢ).Sᵢ where i ∈ I

p is the sender Role, and s is the mapping of Message to continuation Type choices.

Each map entry represents a choice sent by p, where the key of s (a Message) is the message to send, and the value is the continuation Type of the Selection Type.

Fields of Select

p: Rc<Role>
s: HashMap<Message, Box<Type>>

Recur

Recursive Type for representing infinite behaviour.

S ::= μt.S

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

Fields of Recur

t: String
s: Box<Type>

TypeVar

Type Variable for use with Recur to represent infinite behaviour.

S ::= 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 branch(p: &Rc<Role>) -> Box<Type>

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

p is the receiver Role.

fn select(p: &Rc<Role>) -> Box<Type>

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

p is the sender Role.

fn add_message(selbr_type: Box<Type>, m_i: Message, s_i: Box<Type>) -> Box<Type>

Adds a message m_i (and its continuation s_i) to a Type::Branch or Type::Select and returns the updated Branch Type or Select Type respectively.

selbr_type is the input Type, if it is not a Type::Branch or Type::Select it is returned unmodified.

fn len(&self) -> usize

Returns the number of branches/selects for the Type::Branch/Type::Select.

Returns 1 for other Type variants (1 continuation).

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 (or TypeVar).

fn deep_eq(&self, other: &Type) -> bool

Deep-compares two local types.

This compare considers two types the same if the role names (references) are identical, and Type is structurally equivalent.

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.

impl PartialEq for Type

fn eq(&self, other: &Type) -> bool

Returns true if two local::Type are structurally equivalent.

Roles are considered the same if their String name are equal, as this is the more common use of equality in this library. For equality where Roles are identical references, use the deep_eq() method.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=.