Skip to main content

elicitation/primitives/ratatui_types/
trenchcoats.rs

1//! Select-trenchcoat wrappers for ratatui types.
2//!
3//! Each wrapper adds `JsonSchema` to the corresponding ratatui type,
4//! enabling [`ElicitComplete`](crate::ElicitComplete).
5//!
6//! [`BordersSelect`] wraps the bitflags [`ratatui::widgets::Borders`]
7//! with common preset combinations. [`ScrollbarOrientationSelect`]
8//! wraps [`ratatui::widgets::ScrollbarOrientation`] with serde delegation.
9
10use crate::{
11    ElicitCommunicator, ElicitError, ElicitErrorKind, ElicitIntrospect, ElicitResult, Elicitation,
12    ElicitationPattern, PatternDetails, Prompt, Select, TypeMetadata, VariantMetadata, mcp,
13};
14use ratatui::widgets::{Borders, ScrollbarOrientation};
15
16// ---------------------------------------------------------------------------
17// Borders (bitflags — manual wrapper with common presets)
18// ---------------------------------------------------------------------------
19
20/// Select wrapper for [`ratatui::widgets::Borders`].
21///
22/// Provides common border combinations as selectable presets.
23/// Use `into_inner()` to unwrap back to `Borders`.
24#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
25pub struct BordersSelect(Borders);
26
27impl BordersSelect {
28    /// Unwrap to the inner `Borders` value.
29    pub fn into_inner(self) -> Borders {
30        self.0
31    }
32}
33
34impl From<Borders> for BordersSelect {
35    fn from(b: Borders) -> Self {
36        Self(b)
37    }
38}
39
40impl std::ops::Deref for BordersSelect {
41    type Target = Borders;
42    fn deref(&self) -> &Self::Target {
43        &self.0
44    }
45}
46
47impl schemars::JsonSchema for BordersSelect {
48    fn schema_name() -> std::borrow::Cow<'static, str> {
49        "BordersSelect".into()
50    }
51
52    fn json_schema(_gen: &mut schemars::SchemaGenerator) -> schemars::Schema {
53        let labels = <Borders as Select>::labels();
54        let enum_values: Vec<serde_json::Value> =
55            labels.into_iter().map(serde_json::Value::String).collect();
56        serde_json::from_value(serde_json::json!({
57            "type": "string",
58            "enum": enum_values
59        }))
60        .expect("valid schema")
61    }
62}
63
64impl Prompt for Borders {
65    fn prompt() -> Option<&'static str> {
66        Some("Choose which borders to show:")
67    }
68}
69
70impl Select for Borders {
71    fn options() -> Vec<Self> {
72        vec![
73            Borders::NONE,
74            Borders::ALL,
75            Borders::TOP,
76            Borders::BOTTOM,
77            Borders::LEFT,
78            Borders::RIGHT,
79            Borders::TOP | Borders::BOTTOM,
80            Borders::LEFT | Borders::RIGHT,
81        ]
82    }
83
84    fn labels() -> Vec<String> {
85        vec![
86            "None".to_string(),
87            "All".to_string(),
88            "Top".to_string(),
89            "Bottom".to_string(),
90            "Left".to_string(),
91            "Right".to_string(),
92            "Top + Bottom".to_string(),
93            "Left + Right".to_string(),
94        ]
95    }
96
97    fn from_label(label: &str) -> Option<Self> {
98        match label {
99            "None" => Some(Borders::NONE),
100            "All" => Some(Borders::ALL),
101            "Top" => Some(Borders::TOP),
102            "Bottom" => Some(Borders::BOTTOM),
103            "Left" => Some(Borders::LEFT),
104            "Right" => Some(Borders::RIGHT),
105            "Top + Bottom" => Some(Borders::TOP | Borders::BOTTOM),
106            "Left + Right" => Some(Borders::LEFT | Borders::RIGHT),
107            _ => None,
108        }
109    }
110}
111
112crate::default_style!(ratatui::widgets::Borders => BordersStyle);
113
114impl Elicitation for Borders {
115    type Style = BordersStyle;
116
117    #[tracing::instrument(skip(communicator))]
118    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
119        tracing::debug!("Eliciting ratatui::widgets::Borders");
120        let params =
121            mcp::select_params(Self::prompt().unwrap_or("Choose borders:"), &Self::labels());
122        let result = communicator
123            .call_tool(
124                rmcp::model::CallToolRequestParams::new(mcp::tool_names::elicit_select())
125                    .with_arguments(params),
126            )
127            .await?;
128        let value = mcp::extract_value(result)?;
129        let label = mcp::parse_string(value)?;
130        Self::from_label(&label).ok_or_else(|| {
131            ElicitError::new(ElicitErrorKind::ParseError(format!(
132                "Invalid ratatui::widgets::Borders: {label}"
133            )))
134        })
135    }
136
137    fn kani_proof() -> proc_macro2::TokenStream {
138        crate::verification::proof_helpers::kani_select_wrapper("ratatui::widgets::Borders", "All")
139    }
140
141    fn verus_proof() -> proc_macro2::TokenStream {
142        crate::verification::proof_helpers::verus_select_wrapper("ratatui::widgets::Borders", "All")
143    }
144
145    fn creusot_proof() -> proc_macro2::TokenStream {
146        crate::verification::proof_helpers::creusot_select_wrapper(
147            "ratatui::widgets::Borders",
148            "All",
149        )
150    }
151}
152
153impl ElicitIntrospect for Borders {
154    fn pattern() -> ElicitationPattern {
155        ElicitationPattern::Select
156    }
157
158    fn metadata() -> TypeMetadata {
159        TypeMetadata {
160            type_name: "ratatui::widgets::Borders",
161            description: Self::prompt(),
162            details: PatternDetails::Select {
163                variants: Self::labels()
164                    .into_iter()
165                    .map(|label| VariantMetadata {
166                        label,
167                        fields: vec![],
168                    })
169                    .collect(),
170            },
171        }
172    }
173}
174
175impl Prompt for BordersSelect {
176    fn prompt() -> Option<&'static str> {
177        <Borders as Prompt>::prompt()
178    }
179}
180
181impl ElicitIntrospect for BordersSelect {
182    fn pattern() -> ElicitationPattern {
183        <Borders as ElicitIntrospect>::pattern()
184    }
185
186    fn metadata() -> TypeMetadata {
187        <Borders as ElicitIntrospect>::metadata()
188    }
189}
190
191impl Elicitation for BordersSelect {
192    type Style = <Borders as Elicitation>::Style;
193
194    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
195        <Borders as Elicitation>::elicit(communicator)
196            .await
197            .map(Self)
198    }
199
200    fn kani_proof() -> proc_macro2::TokenStream {
201        <Borders as Elicitation>::kani_proof()
202    }
203
204    fn verus_proof() -> proc_macro2::TokenStream {
205        <Borders as Elicitation>::verus_proof()
206    }
207
208    fn creusot_proof() -> proc_macro2::TokenStream {
209        <Borders as Elicitation>::creusot_proof()
210    }
211}
212
213impl crate::emit_code::ToCodeLiteral for BordersSelect {
214    fn to_code_literal(&self) -> proc_macro2::TokenStream {
215        let bits = self.0.bits();
216        quote::quote! {
217            BordersSelect::from(ratatui::widgets::Borders::from_bits_truncate(#bits))
218        }
219    }
220
221    fn type_tokens() -> proc_macro2::TokenStream {
222        quote::quote! { BordersSelect }
223    }
224}
225
226// ---------------------------------------------------------------------------
227// ScrollbarOrientation (regular enum with serde)
228// ---------------------------------------------------------------------------
229
230crate::select_trenchcoat!(ratatui::widgets::ScrollbarOrientation, as ScrollbarOrientationSelect, serde);
231crate::select_trenchcoat_traits!(
232    ScrollbarOrientationSelect,
233    ratatui::widgets::ScrollbarOrientation,
234    [eq, hash]
235);
236
237impl Prompt for ScrollbarOrientation {
238    fn prompt() -> Option<&'static str> {
239        Some("Choose scrollbar orientation:")
240    }
241}
242
243impl Select for ScrollbarOrientation {
244    fn options() -> Vec<Self> {
245        vec![
246            ScrollbarOrientation::VerticalRight,
247            ScrollbarOrientation::VerticalLeft,
248            ScrollbarOrientation::HorizontalBottom,
249            ScrollbarOrientation::HorizontalTop,
250        ]
251    }
252
253    fn labels() -> Vec<String> {
254        vec![
255            "VerticalRight".to_string(),
256            "VerticalLeft".to_string(),
257            "HorizontalBottom".to_string(),
258            "HorizontalTop".to_string(),
259        ]
260    }
261
262    fn from_label(label: &str) -> Option<Self> {
263        match label {
264            "VerticalRight" => Some(ScrollbarOrientation::VerticalRight),
265            "VerticalLeft" => Some(ScrollbarOrientation::VerticalLeft),
266            "HorizontalBottom" => Some(ScrollbarOrientation::HorizontalBottom),
267            "HorizontalTop" => Some(ScrollbarOrientation::HorizontalTop),
268            _ => None,
269        }
270    }
271}
272
273crate::default_style!(ratatui::widgets::ScrollbarOrientation => ScrollbarOrientationStyle);
274
275impl Elicitation for ScrollbarOrientation {
276    type Style = ScrollbarOrientationStyle;
277
278    #[tracing::instrument(skip(communicator))]
279    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
280        tracing::debug!("Eliciting ratatui::widgets::ScrollbarOrientation");
281        let params = mcp::select_params(
282            Self::prompt().unwrap_or("Choose scrollbar orientation:"),
283            &Self::labels(),
284        );
285        let result = communicator
286            .call_tool(
287                rmcp::model::CallToolRequestParams::new(mcp::tool_names::elicit_select())
288                    .with_arguments(params),
289            )
290            .await?;
291        let value = mcp::extract_value(result)?;
292        let label = mcp::parse_string(value)?;
293        Self::from_label(&label).ok_or_else(|| {
294            ElicitError::new(ElicitErrorKind::ParseError(format!(
295                "Invalid ratatui::widgets::ScrollbarOrientation: {label}"
296            )))
297        })
298    }
299
300    fn kani_proof() -> proc_macro2::TokenStream {
301        crate::verification::proof_helpers::kani_select_wrapper(
302            "ratatui::widgets::ScrollbarOrientation",
303            "VerticalRight",
304        )
305    }
306
307    fn verus_proof() -> proc_macro2::TokenStream {
308        crate::verification::proof_helpers::verus_select_wrapper(
309            "ratatui::widgets::ScrollbarOrientation",
310            "VerticalRight",
311        )
312    }
313
314    fn creusot_proof() -> proc_macro2::TokenStream {
315        crate::verification::proof_helpers::creusot_select_wrapper(
316            "ratatui::widgets::ScrollbarOrientation",
317            "VerticalRight",
318        )
319    }
320}
321
322impl ElicitIntrospect for ScrollbarOrientation {
323    fn pattern() -> ElicitationPattern {
324        ElicitationPattern::Select
325    }
326
327    fn metadata() -> TypeMetadata {
328        TypeMetadata {
329            type_name: "ratatui::widgets::ScrollbarOrientation",
330            description: Self::prompt(),
331            details: PatternDetails::Select {
332                variants: Self::labels()
333                    .into_iter()
334                    .map(|label| VariantMetadata {
335                        label,
336                        fields: vec![],
337                    })
338                    .collect(),
339            },
340        }
341    }
342}
343
344// ---------------------------------------------------------------------------
345// Alignment (regular enum with serde — trenchcoat adds JsonSchema)
346// ---------------------------------------------------------------------------
347
348crate::select_trenchcoat!(ratatui::layout::Alignment, as AlignmentSelect, serde);
349crate::select_trenchcoat_traits!(
350    AlignmentSelect,
351    ratatui::layout::Alignment,
352    [copy, eq, hash]
353);
354
355// ---------------------------------------------------------------------------
356// Direction (regular enum with serde — trenchcoat adds JsonSchema)
357// ---------------------------------------------------------------------------
358
359crate::select_trenchcoat!(ratatui::layout::Direction, as RatatuiDirectionSelect, serde);
360crate::select_trenchcoat_traits!(
361    RatatuiDirectionSelect,
362    ratatui::layout::Direction,
363    [copy, eq, hash]
364);
365
366// ---------------------------------------------------------------------------
367// BorderType (regular enum with serde — trenchcoat adds JsonSchema)
368// ---------------------------------------------------------------------------
369
370crate::select_trenchcoat!(ratatui::widgets::BorderType, as BorderTypeSelect, serde);
371crate::select_trenchcoat_traits!(
372    BorderTypeSelect,
373    ratatui::widgets::BorderType,
374    [copy, eq, hash]
375);
376
377// ---------------------------------------------------------------------------
378// Color (custom serde via Display/FromStr — trenchcoat adds JsonSchema)
379// ---------------------------------------------------------------------------
380
381crate::select_trenchcoat!(ratatui::style::Color, as ColorSelect, serde);
382crate::select_trenchcoat_traits!(ColorSelect, ratatui::style::Color, [copy, eq, hash]);