elicitation/primitives/
char.rs

1//! Char type implementation.
2
3use crate::{ElicitCommunicator, ElicitResult, Elicitation, Prompt, mcp};
4
5// Generate default-only style enum
6crate::default_style!(char => CharStyle);
7
8impl Prompt for char {
9    fn prompt() -> Option<&'static str> {
10        Some("Please enter a single character:")
11    }
12}
13
14impl Elicitation for char {
15    type Style = CharStyle;
16
17    #[tracing::instrument(skip(communicator))]
18    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
19        let prompt = communicator
20            .style_context()
21            .prompt_for_type::<Self>("value", "char", &crate::style::PromptContext::new(0, 1))
22            .unwrap_or(None)
23            .unwrap_or_else(|| Self::prompt().unwrap().to_string());
24        tracing::debug!(%prompt, "Eliciting char");
25
26        let params = mcp::text_params(&prompt);
27        let result = communicator
28            .call_tool(
29                rmcp::model::CallToolRequestParams::new(mcp::tool_names::elicit_text())
30                    .with_arguments(params),
31            )
32            .await?;
33
34        let value = mcp::extract_value(result)?;
35        let string = mcp::parse_string(value)?;
36
37        // Get first character from string
38        string.chars().next().ok_or_else(|| {
39            crate::ElicitError::new(crate::ElicitErrorKind::InvalidFormat {
40                expected: "non-empty string with at least one character".to_string(),
41                received: "empty string".to_string(),
42            })
43        })
44    }
45
46    fn kani_proof() -> proc_macro2::TokenStream {
47        crate::verification::proof_helpers::kani_char()
48    }
49
50    fn verus_proof() -> proc_macro2::TokenStream {
51        crate::verification::proof_helpers::verus_char()
52    }
53
54    fn creusot_proof() -> proc_macro2::TokenStream {
55        crate::verification::proof_helpers::creusot_char()
56    }
57}
58
59impl crate::ElicitIntrospect for char {
60    fn pattern() -> crate::ElicitationPattern {
61        crate::ElicitationPattern::Primitive
62    }
63    fn metadata() -> crate::TypeMetadata {
64        crate::TypeMetadata {
65            type_name: "char",
66            description: <char as crate::Prompt>::prompt(),
67            details: crate::PatternDetails::Primitive,
68        }
69    }
70}
elicitation/primitives/char.rs

elicitation/primitives/
char.rs
