telltale_types/
action.rs

1//! Actions in Session Types
2//!
3//! Actions represent the basic communication primitives in session types.
4//! These correspond to the Lean definitions in `lean/SessionTypes/Core.lean`.
5
6use crate::Label;
7use serde::{Deserialize, Serialize};
8
9/// Basic action type (send or receive).
10///
11/// Corresponds to Lean's action polarity.
12#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
13pub enum Action {
14    /// Send action (internal choice, output)
15    Send,
16    /// Receive action (external choice, input)
17    Recv,
18}
19
20impl Action {
21    /// Get the dual action
22    #[must_use]
23    pub fn dual(&self) -> Self {
24        match self {
25            Action::Send => Action::Recv,
26            Action::Recv => Action::Send,
27        }
28    }
29
30    /// Check if this is a send action
31    #[must_use]
32    pub fn is_send(&self) -> bool {
33        matches!(self, Action::Send)
34    }
35
36    /// Check if this is a receive action
37    #[must_use]
38    pub fn is_recv(&self) -> bool {
39        matches!(self, Action::Recv)
40    }
41}
42
43impl std::fmt::Display for Action {
44    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
45        match self {
46            Action::Send => write!(f, "!"),
47            Action::Recv => write!(f, "?"),
48        }
49    }
50}
51
52/// A complete local action with role and label.
53///
54/// Represents a single communication step: action + partner + message.
55/// Corresponds to Lean's action representation in traces.
56///
57/// # Examples
58///
59/// ```
60/// use telltale_types::{LocalAction, Action, Label};
61///
62/// // Send "hello" to role B
63/// let action = LocalAction::new(Action::Send, "B", Label::new("hello"));
64/// assert!(action.is_send());
65/// assert_eq!(action.partner(), "B");
66/// ```
67#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
68pub struct LocalAction {
69    /// The action type (send or receive)
70    action: Action,
71    /// The communication partner
72    partner: String,
73    /// The message label
74    label: Label,
75}
76
77impl LocalAction {
78    /// Create a new local action
79    #[must_use]
80    pub fn new(action: Action, partner: impl Into<String>, label: Label) -> Self {
81        Self {
82            action,
83            partner: partner.into(),
84            label,
85        }
86    }
87
88    /// Create a send action
89    #[must_use]
90    pub fn send(partner: impl Into<String>, label: Label) -> Self {
91        Self::new(Action::Send, partner, label)
92    }
93
94    /// Create a receive action
95    #[must_use]
96    pub fn recv(partner: impl Into<String>, label: Label) -> Self {
97        Self::new(Action::Recv, partner, label)
98    }
99
100    /// Get the action type
101    #[must_use]
102    pub fn action(&self) -> Action {
103        self.action
104    }
105
106    /// Get the partner role
107    #[must_use]
108    pub fn partner(&self) -> &str {
109        &self.partner
110    }
111
112    /// Get the message label
113    #[must_use]
114    pub fn label(&self) -> &Label {
115        &self.label
116    }
117
118    /// Check if this is a send action
119    #[must_use]
120    pub fn is_send(&self) -> bool {
121        self.action.is_send()
122    }
123
124    /// Check if this is a receive action
125    #[must_use]
126    pub fn is_recv(&self) -> bool {
127        self.action.is_recv()
128    }
129
130    /// Get the dual action (swap send/recv, keep partner and label)
131    #[must_use]
132    pub fn dual(&self) -> Self {
133        Self {
134            action: self.action.dual(),
135            partner: self.partner.clone(),
136            label: self.label.clone(),
137        }
138    }
139}
140
141impl std::fmt::Display for LocalAction {
142    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
143        write!(f, "{}{}{{{}}}", self.action, self.partner, self.label)
144    }
145}
146
147#[cfg(test)]
148mod tests {
149    use super::*;
150
151    #[test]
152    fn test_action_dual() {
153        assert_eq!(Action::Send.dual(), Action::Recv);
154        assert_eq!(Action::Recv.dual(), Action::Send);
155    }
156
157    #[test]
158    fn test_action_display() {
159        assert_eq!(format!("{}", Action::Send), "!");
160        assert_eq!(format!("{}", Action::Recv), "?");
161    }
162
163    #[test]
164    fn test_local_action_new() {
165        let action = LocalAction::new(Action::Send, "B", Label::new("msg"));
166        assert!(action.is_send());
167        assert_eq!(action.partner(), "B");
168        assert_eq!(action.label().name, "msg");
169    }
170
171    #[test]
172    fn test_local_action_send_recv() {
173        let send = LocalAction::send("B", Label::new("hello"));
174        let recv = LocalAction::recv("A", Label::new("world"));
175
176        assert!(send.is_send());
177        assert!(!send.is_recv());
178        assert!(recv.is_recv());
179        assert!(!recv.is_send());
180    }
181
182    #[test]
183    fn test_local_action_dual() {
184        let send = LocalAction::send("B", Label::new("msg"));
185        let recv = send.dual();
186
187        assert!(recv.is_recv());
188        assert_eq!(recv.partner(), "B");
189        assert_eq!(recv.label().name, "msg");
190    }
191
192    #[test]
193    fn test_local_action_display() {
194        let action = LocalAction::send("B", Label::new("hello"));
195        assert_eq!(format!("{}", action), "!B{hello}");
196
197        let recv = LocalAction::recv("A", Label::new("data"));
198        assert_eq!(format!("{}", recv), "?A{data}");
199    }
200}
telltale_types/action.rs

telltale_types/
action.rs
