Enum LocalTypeR 

pub enum LocalTypeR {
    End,
    Send {
        partner: String,
        branches: Vec<(Label, LocalTypeR)>,
    },
    Recv {
        partner: String,
        branches: Vec<(Label, LocalTypeR)>,
    },
    Mu {
        var: String,
        body: Box<LocalTypeR>,
    },
    Var(String),
}

Core local type matching Lean’s LocalTypeR.

This is the minimal type used for validation and correspondence proofs. For code generation, see the extended LocalType in the DSL crate.

Examples

use rumpsteak_types::{LocalTypeR, Label};

// Simple send: !B{msg.end}
let lt = LocalTypeR::send("B", Label::new("msg"), LocalTypeR::End);
assert!(lt.well_formed());

// Recursive type: μt. !B{msg.t}
let rec = LocalTypeR::mu(
    "t",
    LocalTypeR::send("B", Label::new("msg"), LocalTypeR::var("t")),
);
assert!(rec.well_formed());

Variants

End

Protocol termination

Send

Internal choice: send to partner with choice of continuations

Fields

partner: String

branches: Vec<(Label, LocalTypeR)>

Recv

External choice: receive from partner with offered continuations

Fields

partner: String

branches: Vec<(Label, LocalTypeR)>

Mu

Recursive type: μt.T binds variable t in body T

Fields

var: String

body: Box<LocalTypeR>

Var(String)

Type variable: reference to enclosing μ-binder

Implementations

impl LocalTypeR

pub fn send( partner: impl Into<String>, label: Label, cont: LocalTypeR, ) -> LocalTypeR

Create a simple send with one label

pub fn send_choice( partner: impl Into<String>, branches: Vec<(Label, LocalTypeR)>, ) -> LocalTypeR

Create a send with multiple branches

pub fn recv( partner: impl Into<String>, label: Label, cont: LocalTypeR, ) -> LocalTypeR

Create a simple recv with one label

pub fn recv_choice( partner: impl Into<String>, branches: Vec<(Label, LocalTypeR)>, ) -> LocalTypeR

Create a recv with multiple branches

pub fn mu(var: impl Into<String>, body: LocalTypeR) -> LocalTypeR

Create a recursive type

pub fn var(name: impl Into<String>) -> LocalTypeR

Create a type variable

pub fn free_vars(&self) -> Vec<String>

Extract free type variables from a local type.

Corresponds to Lean’s LocalTypeR.freeVars.

pub fn substitute(&self, var_name: &str, replacement: &LocalTypeR) -> LocalTypeR

Substitute a local type for a variable.

Corresponds to Lean’s LocalTypeR.substitute.

pub fn unfold(&self) -> LocalTypeR

Unfold one level of recursion: μt.T ↦ T[μt.T/t]

Corresponds to Lean’s LocalTypeR.unfold.

pub fn dual(&self) -> LocalTypeR

Compute the dual of a local type (swap send/recv).

The dual of role A’s view is role B’s view when A and B are the only participants. Corresponds to Lean’s LocalTypeR.dual.

pub fn all_vars_bound(&self) -> bool

Check if all recursion variables are bound.

Corresponds to Lean’s LocalTypeR.allVarsBound.

pub fn all_choices_non_empty(&self) -> bool

Check if each choice has at least one branch.

Corresponds to Lean’s LocalTypeR.allChoicesNonEmpty.

pub fn well_formed(&self) -> bool

Well-formedness predicate for local types.

Corresponds to Lean’s LocalTypeR.wellFormed. A local type is well-formed if:

1. All recursion variables are bound
2. Each choice has at least one branch
3. All recursion is guarded (no immediate recursion without communication)

pub fn depth(&self) -> usize

Count the depth of a local type (for termination proofs).

Corresponds to Lean’s LocalTypeR.depth.

pub fn is_guarded(&self) -> bool

Check if a local type is guarded (no immediate recursion).

Corresponds to Lean’s LocalTypeR.isGuarded.

pub fn labels(&self) -> Vec<String>

Extract all labels from a local type.

Corresponds to Lean’s LocalTypeR.labels.

pub fn partners(&self) -> Vec<String>

Extract all partners from a local type.

Corresponds to Lean’s LocalTypeR.partners.

pub fn mentions_partner(&self, role: &str) -> bool

Check if a local type mentions a specific partner.

pub fn is_send(&self) -> bool

Check if this is an internal choice (send)

pub fn is_recv(&self) -> bool

Check if this is an external choice (recv)

pub fn is_end(&self) -> bool

Check if this is a terminated type

Trait Implementations

impl Clone for LocalTypeR

fn clone(&self) -> LocalTypeR

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Contentable for LocalTypeR

fn to_bytes(&self) -> Result<Vec<u8>, ContentableError>

Serialize to canonical byte representation (JSON format).

fn from_bytes(bytes: &[u8]) -> Result<LocalTypeR, ContentableError>

Deserialize from JSON bytes.

fn content_id<H>(&self) -> Result<ContentId<H>, ContentableError>

where H: Hasher,

Compute content ID using the specified hasher (from JSON bytes).

fn content_id_sha256(&self) -> Result<ContentId, ContentableError>

Compute content ID using default SHA-256 hasher (from JSON bytes).

impl Debug for LocalTypeR

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for LocalTypeR

fn deserialize<__D>( __deserializer: __D, ) -> Result<LocalTypeR, <__D as Deserializer<'de>>::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Hash for LocalTypeR

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for LocalTypeR

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for LocalTypeR

fn serialize<__S>( &self, __serializer: __S, ) -> Result<<__S as Serializer>::Ok, <__S as Serializer>::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for LocalTypeR

impl StructuralPartialEq for LocalTypeR