Enum LocalTypeR 

pub enum LocalTypeR {
    End,
    Send {
        partner: String,
        branches: Vec<(Label, Option<ValType>, LocalTypeR)>,
    },
    Recv {
        partner: String,
        branches: Vec<(Label, Option<ValType>, 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 telltale_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, Option<ValType>, LocalTypeR)>

Recv

External choice: receive from partner with offered continuations

Fields

partner: String

branches: Vec<(Label, Option<ValType>, 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) -> Self

Create a simple send with one label

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

Create a send with multiple branches

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

Create a simple recv with one label

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

Create a recv with multiple branches

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

Create a recursive type

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

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 mu_height(&self) -> usize

Count nested recursion binders at the current head position.

Corresponds to Lean’s LocalTypeR.muHeight.

pub fn full_unfold(&self) -> LocalTypeR

Fully unfold leading recursion until a non-Mu head is exposed.

Corresponds to Lean’s LocalTypeR.fullUnfold.

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 unique_branch_labels(&self) -> bool

Check if all send/recv nodes have unique branch label names.

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 reaches_communication(&self) -> bool

Check whether full unfolding exposes a communication head.

Corresponds to Lean’s LocalTypeR.reachesCommunication.

pub fn regular_practical_fragment(&self) -> bool

Mechanically characterized practical fragment that needs no manual ReachesComm.

Corresponds to Lean’s LocalTypeR.regularPracticalFragment.

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 is_var_guarded(&self, var: &str) -> bool

Check if a specific recursion variable is guarded in this local type.

A variable v is guarded if it does not appear “bare” (i.e., every occurrence is under a send or recv). Corresponds to Lean’s LocalTypeR.isGuarded v.

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

Extract labels from the outermost visible choice node.

For recursive terms (Mu), this inspects the wrapped body.

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

Extract all labels that appear anywhere in the local type.

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 to_template_bytes(&self) -> Result<Vec<u8>, ContentableError>

Serialize to template bytes, allowing open terms with explicit free-variable interfaces when supported by the implementation.

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

Deserialize from JSON bytes.

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

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

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

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

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

Compute content ID using explicit BLAKE3 (from JSON bytes).

fn template_id<H: Hasher>(&self) -> Result<ContentId<H>, ContentableError>

Compute a template ID using the specified hasher (from template bytes).

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

Compute a template ID using the central default content hasher.

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

Compute a template ID using explicit BLAKE3.

impl Debug for LocalTypeR

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

Formats the value using the given formatter.

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

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl From<&LocalTypeR> for LocalTypeRDB

fn from(t: &LocalTypeR) -> Self

Converts to this type from the input type.

impl Hash for LocalTypeR

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

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::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for LocalTypeR

impl StructuralPartialEq for LocalTypeR