Struct SessionSubtypeChecker 

pub struct SessionSubtypeChecker { /* private fields */ }

Behavioral subtype checker for session types.

Implements the standard coinductive subtype relation:

• Send T S₁ <: Send T S₂ when S₁ <: S₂ (covariant send)
• Recv T S₁ <: Recv T S₂ when S₁ <: S₂ (covariant receive)
• Choice S₁ S₂ <: Choice T₁ T₂ when S₁ <: T₁ and S₂ <: T₂
• Branch S₁ S₂ <: Branch T₁ T₂ when S₁ <: T₁ and S₂ <: T₂
• End <: End

Implementations

impl SessionSubtypeChecker

pub fn new() -> Self

Create a new subtype checker.

pub fn is_subtype(&mut self, sub: &SType, sup: &SType) -> bool

Check whether sub <: sup holds under the behavioral subtype relation.

Trait Implementations

impl Default for SessionSubtypeChecker

fn default() -> Self

Returns the “default value” for a type.