telltale_types/
label.rs

1//! Message Labels for Session Types
2//!
3//! Labels identify message types in communications between roles.
4//!
5//! # Lean Correspondence
6//!
7//! Corresponds to the `Label` structure in `lean/SessionTypes/GlobalType.lean`.
8
9use crate::PayloadSort;
10use serde::{Deserialize, Serialize};
11
12/// A message label with its payload sort.
13///
14/// Labels identify message types in communications.
15/// Each label has a name and an associated payload type.
16///
17/// # Examples
18///
19/// ```
20/// use telltale_types::{Label, PayloadSort};
21///
22/// // Simple label with unit payload
23/// let hello = Label::new("hello");
24/// assert_eq!(hello.name, "hello");
25///
26/// // Label with typed payload
27/// let data = Label::with_sort("data", PayloadSort::Nat);
28/// assert!(!data.sort.is_simple() || matches!(data.sort, PayloadSort::Nat));
29/// ```
30#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
31pub struct Label {
32    /// The label name identifying this message type
33    pub name: String,
34    /// The payload sort for this message
35    #[serde(default)]
36    pub sort: PayloadSort,
37}
38
39impl Label {
40    /// Create a new label with unit payload
41    #[must_use]
42    pub fn new(name: impl Into<String>) -> Self {
43        Self {
44            name: name.into(),
45            sort: PayloadSort::Unit,
46        }
47    }
48
49    /// Create a new label with a specific sort
50    #[must_use]
51    pub fn with_sort(name: impl Into<String>, sort: PayloadSort) -> Self {
52        Self {
53            name: name.into(),
54            sort,
55        }
56    }
57
58    /// Check if this label matches another exactly (name and sort).
59    #[must_use]
60    pub fn matches(&self, other: &Label) -> bool {
61        self == other
62    }
63
64    /// Check if this label matches a name
65    #[must_use]
66    pub fn matches_name(&self, name: &str) -> bool {
67        self.name == name
68    }
69}
70
71impl std::fmt::Display for Label {
72    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
73        write!(f, "{}", self.name)?;
74        if self.sort != PayloadSort::Unit {
75            write!(f, "({})", self.sort)?;
76        }
77        Ok(())
78    }
79}
80
81#[cfg(test)]
82mod tests {
83    use super::*;
84
85    #[test]
86    fn test_label_new() {
87        let label = Label::new("hello");
88        assert_eq!(label.name, "hello");
89        assert_eq!(label.sort, PayloadSort::Unit);
90    }
91
92    #[test]
93    fn test_label_with_sort() {
94        let label = Label::with_sort("data", PayloadSort::Nat);
95        assert_eq!(label.name, "data");
96        assert_eq!(label.sort, PayloadSort::Nat);
97    }
98
99    #[test]
100    fn test_label_matches() {
101        let l1 = Label::new("msg");
102        let l2 = Label::with_sort("msg", PayloadSort::Bool);
103        let l3 = Label::new("other");
104        let l4 = Label::new("msg");
105
106        assert!(!l1.matches(&l2)); // Same name, different sort
107        assert!(!l1.matches(&l3)); // Different name
108        assert!(l1.matches(&l4)); // Exact match
109        assert!(l1.matches_name("msg")); // Name-only helper
110    }
111
112    #[test]
113    fn test_label_display() {
114        let unit_label = Label::new("hello");
115        assert_eq!(format!("{}", unit_label), "hello");
116
117        let typed_label = Label::with_sort("data", PayloadSort::Nat);
118        assert_eq!(format!("{}", typed_label), "data(Nat)");
119    }
120}
telltale_types/label.rs

telltale_types/
label.rs
