elicitation/primitives/ratatui_types/
trenchcoats.rs1use crate::{
11 ElicitCommunicator, ElicitError, ElicitErrorKind, ElicitIntrospect, ElicitResult, Elicitation,
12 ElicitationPattern, PatternDetails, Prompt, Select, TypeMetadata, VariantMetadata, mcp,
13};
14use ratatui::widgets::{Borders, ScrollbarOrientation};
15
16#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
25pub struct BordersSelect(Borders);
26
27impl BordersSelect {
28 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
226crate::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
344crate::select_trenchcoat!(ratatui::layout::Alignment, as AlignmentSelect, serde);
349crate::select_trenchcoat_traits!(
350 AlignmentSelect,
351 ratatui::layout::Alignment,
352 [copy, eq, hash]
353);
354
355crate::select_trenchcoat!(ratatui::layout::Direction, as RatatuiDirectionSelect, serde);
360crate::select_trenchcoat_traits!(
361 RatatuiDirectionSelect,
362 ratatui::layout::Direction,
363 [copy, eq, hash]
364);
365
366crate::select_trenchcoat!(ratatui::widgets::BorderType, as BorderTypeSelect, serde);
371crate::select_trenchcoat_traits!(
372 BorderTypeSelect,
373 ratatui::widgets::BorderType,
374 [copy, eq, hash]
375);
376
377crate::select_trenchcoat!(ratatui::style::Color, as ColorSelect, serde);
382crate::select_trenchcoat_traits!(ColorSelect, ratatui::style::Color, [copy, eq, hash]);