elicitation 0.10.0

//! Char contract types.

use super::ValidationError;
use crate::{ElicitCommunicator, ElicitResult, Elicitation, Prompt};
use anodized::spec;
#[cfg(not(kani))]
use elicitation_macros::instrumented_impl;

// ============================================================================

/// Contract type for alphabetic char values.
///
/// Validates on construction, then can unwrap to stdlib char via `into_inner()`.
#[derive(
    Debug,
    Clone,
    Copy,
    PartialEq,
    Eq,
    Hash,
    serde::Serialize,
    serde::Deserialize,
    schemars::JsonSchema,
)]
#[schemars(description = "An alphabetic character (a-z, A-Z)")]
pub struct CharAlphabetic(char);

#[cfg_attr(not(kani), instrumented_impl)]
impl CharAlphabetic {
    /// Constructs an alphabetic char.
    ///
    /// # Errors
    ///
    /// Returns `ValidationError::NotAlphabetic` if char is not alphabetic.
    #[cfg(not(kani))]
    #[spec(requires: [value.is_alphabetic()])]
    pub fn new(value: char) -> Result<Self, ValidationError> {
        if value.is_alphabetic() {
            Ok(Self(value))
        } else {
            Err(ValidationError::NotAlphabetic(value))
        }
    }

    /// Kani version: trust stdlib, verify wrapper logic.
    #[cfg(kani)]
    pub fn new(value: char) -> Result<Self, ValidationError> {
        // Symbolic boolean represents is_alphabetic() result
        // We verify our wrapper logic, not Unicode table implementation
        let is_alpha: bool = kani::any();
        if is_alpha {
            Ok(Self(value))
        } else {
            Err(ValidationError::NotAlphabetic(value))
        }
    }

    /// Gets the wrapped value.
    pub fn get(&self) -> char {
        self.0
    }

    /// Unwraps to stdlib char (trenchcoat off).
    pub fn into_inner(self) -> char {
        self.0
    }
}

crate::default_style!(CharAlphabetic => CharAlphabeticStyle);

impl Prompt for CharAlphabetic {
    fn prompt() -> Option<&'static str> {
        Some("Please enter an alphabetic character:")
    }
}

impl Elicitation for CharAlphabetic {
    type Style = CharAlphabeticStyle;

    #[tracing::instrument(skip(communicator), fields(type_name = "CharAlphabetic"))]
    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
        tracing::debug!("Eliciting CharAlphabetic (alphabetic char)");

        loop {
            let value = char::elicit(communicator).await?;

            match Self::new(value) {
                Ok(alphabetic) => {
                    tracing::debug!(value = %value, "Valid CharAlphabetic constructed");
                    return Ok(alphabetic);
                }
                Err(e) => {
                    tracing::warn!(value = %value, error = %e, "Invalid CharAlphabetic, re-prompting");
                }
            }
        }
    }

    fn kani_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::kani_char_alphabetic()
    }

    fn verus_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::verus_char()
    }

    fn creusot_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::creusot_char()
    }
}

/// Contract type for numeric char values.
///
/// Validates on construction, then can unwrap to stdlib char via `into_inner()`.
#[derive(
    Debug,
    Clone,
    Copy,
    PartialEq,
    Eq,
    Hash,
    serde::Serialize,
    serde::Deserialize,
    schemars::JsonSchema,
)]
#[schemars(description = "A numeric character (0-9)")]
pub struct CharNumeric(char);

impl CharNumeric {
    /// Constructs a numeric char.
    ///
    /// # Errors
    ///
    /// Returns `ValidationError::NotNumeric` if char is not numeric.
    #[cfg(not(kani))]
    #[spec(requires: [value.is_numeric()])]
    pub fn new(value: char) -> Result<Self, ValidationError> {
        if value.is_numeric() {
            Ok(Self(value))
        } else {
            Err(ValidationError::NotNumeric(value))
        }
    }

    /// Kani version: trust stdlib, verify wrapper logic.
    #[cfg(kani)]
    pub fn new(value: char) -> Result<Self, ValidationError> {
        // Symbolic boolean represents is_numeric() result
        let is_numeric: bool = kani::any();
        if is_numeric {
            Ok(Self(value))
        } else {
            Err(ValidationError::NotNumeric(value))
        }
    }

    /// Gets the wrapped value.
    pub fn get(&self) -> char {
        self.0
    }

    /// Unwraps to stdlib char (trenchcoat off).
    pub fn into_inner(self) -> char {
        self.0
    }
}

crate::default_style!(CharNumeric => CharNumericStyle);

impl Prompt for CharNumeric {
    fn prompt() -> Option<&'static str> {
        Some("Please enter a numeric character:")
    }
}

impl Elicitation for CharNumeric {
    type Style = CharNumericStyle;

    #[tracing::instrument(skip(communicator), fields(type_name = "CharNumeric"))]
    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
        tracing::debug!("Eliciting CharNumeric (numeric char)");

        loop {
            let value = char::elicit(communicator).await?;

            match Self::new(value) {
                Ok(numeric) => {
                    tracing::debug!(value = %value, "Valid CharNumeric constructed");
                    return Ok(numeric);
                }
                Err(e) => {
                    tracing::warn!(value = %value, error = %e, "Invalid CharNumeric, re-prompting");
                }
            }
        }
    }

    fn kani_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::kani_char_numeric()
    }

    fn verus_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::verus_char()
    }

    fn creusot_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::creusot_char()
    }
}

/// Contract type for alphanumeric char values.
///
/// Validates on construction, then can unwrap to stdlib char via `into_inner()`.
#[derive(
    Debug,
    Clone,
    Copy,
    PartialEq,
    Eq,
    Hash,
    serde::Serialize,
    serde::Deserialize,
    schemars::JsonSchema,
)]
#[schemars(description = "An alphanumeric character (a-z, A-Z, 0-9)")]
pub struct CharAlphanumeric(char);

#[cfg_attr(not(kani), instrumented_impl)]
impl CharAlphanumeric {
    /// Constructs an alphanumeric char.
    ///
    /// # Errors
    ///
    /// Returns `ValidationError::NotAlphanumeric` if char is not alphanumeric.
    #[spec(requires: [value.is_alphanumeric()])]
    pub fn new(value: char) -> Result<Self, ValidationError> {
        #[cfg(kani)]
        {
            // Under Kani: symbolic validation (trust stdlib char handling)
            let is_alphanumeric: bool = kani::any();
            if is_alphanumeric {
                Ok(Self(value))
            } else {
                Err(ValidationError::NotAlphanumeric(value))
            }
        }
        #[cfg(not(kani))]
        {
            // Production: actual validation
            if value.is_alphanumeric() {
                Ok(Self(value))
            } else {
                Err(ValidationError::NotAlphanumeric(value))
            }
        }
    }

    /// Gets the wrapped value.
    pub fn get(&self) -> char {
        self.0
    }

    /// Unwraps to stdlib char (trenchcoat off).
    pub fn into_inner(self) -> char {
        self.0
    }
}

crate::default_style!(CharAlphanumeric => CharAlphanumericStyle);

impl Prompt for CharAlphanumeric {
    fn prompt() -> Option<&'static str> {
        Some("Please enter an alphanumeric character:")
    }
}

impl Elicitation for CharAlphanumeric {
    type Style = CharAlphanumericStyle;

    #[tracing::instrument(skip(communicator), fields(type_name = "CharAlphanumeric"))]
    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
        tracing::debug!("Eliciting CharAlphanumeric (alphanumeric char)");

        loop {
            let value = char::elicit(communicator).await?;

            match Self::new(value) {
                Ok(alphanumeric) => {
                    tracing::debug!(value = %value, "Valid CharAlphanumeric constructed");
                    return Ok(alphanumeric);
                }
                Err(e) => {
                    tracing::warn!(value = %value, error = %e, "Invalid CharAlphanumeric, re-prompting");
                }
            }
        }
    }

    fn kani_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::kani_char_alphanumeric()
    }

    fn verus_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::verus_char()
    }

    fn creusot_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::creusot_char()
    }
}

#[cfg(test)]
mod char_alphabetic_tests {
    use super::*;

    #[test]
    fn char_alphabetic_new_valid() {
        let result = CharAlphabetic::new('a');
        assert!(result.is_ok());
        assert_eq!(result.unwrap().get(), 'a');
    }

    #[test]
    fn char_alphabetic_new_digit_invalid() {
        let result = CharAlphabetic::new('5');
        assert!(result.is_err());
    }

    #[test]
    fn char_alphabetic_into_inner() {
        let alphabetic = CharAlphabetic::new('z').unwrap();
        let value: char = alphabetic.into_inner();
        assert_eq!(value, 'z');
    }
}

#[cfg(test)]
mod char_numeric_tests {
    use super::*;

    #[test]
    fn char_numeric_new_valid() {
        let result = CharNumeric::new('5');
        assert!(result.is_ok());
        assert_eq!(result.unwrap().get(), '5');
    }

    #[test]
    fn char_numeric_new_letter_invalid() {
        let result = CharNumeric::new('a');
        assert!(result.is_err());
    }

    #[test]
    fn char_numeric_into_inner() {
        let numeric = CharNumeric::new('9').unwrap();
        let value: char = numeric.into_inner();
        assert_eq!(value, '9');
    }
}

#[cfg(test)]
mod char_alphanumeric_tests {
    use super::*;

    #[test]
    fn char_alphanumeric_new_valid_letter() {
        let result = CharAlphanumeric::new('a');
        assert!(result.is_ok());
        assert_eq!(result.unwrap().get(), 'a');
    }

    #[test]
    fn char_alphanumeric_new_valid_digit() {
        let result = CharAlphanumeric::new('5');
        assert!(result.is_ok());
        assert_eq!(result.unwrap().get(), '5');
    }

    #[test]
    fn char_alphanumeric_new_symbol_invalid() {
        let result = CharAlphanumeric::new('!');
        assert!(result.is_err());
    }

    #[test]
    fn char_alphanumeric_into_inner() {
        let alphanumeric = CharAlphanumeric::new('x').unwrap();
        let value: char = alphanumeric.into_inner();
        assert_eq!(value, 'x');
    }
}

// ── ToCodeLiteral impls ───────────────────────────────────────────────────────

mod emit_impls {
    use super::*;
    use crate::emit_code::ToCodeLiteral;
    use proc_macro2::TokenStream;

    impl ToCodeLiteral for CharAlphabetic {
        fn to_code_literal(&self) -> TokenStream {
            let c = self.get();
            quote::quote! { elicitation::CharAlphabetic::new(#c).expect("valid CharAlphabetic") }
        }
    }

    impl ToCodeLiteral for CharNumeric {
        fn to_code_literal(&self) -> TokenStream {
            let c = self.get();
            quote::quote! { elicitation::CharNumeric::new(#c).expect("valid CharNumeric") }
        }
    }

    impl ToCodeLiteral for CharAlphanumeric {
        fn to_code_literal(&self) -> TokenStream {
            let c = self.get();
            quote::quote! { elicitation::CharAlphanumeric::new(#c).expect("valid CharAlphanumeric") }
        }
    }
}

// ── ElicitIntrospect impls ────────────────────────────────────────────────────

macro_rules! impl_primitive_introspect {
    ($($ty:ty => $name:literal),+ $(,)?) => {
        $(
            impl crate::ElicitIntrospect for $ty {
                fn pattern() -> crate::ElicitationPattern {
                    crate::ElicitationPattern::Primitive
                }
                fn metadata() -> crate::TypeMetadata {
                    crate::TypeMetadata {
                        type_name: $name,
                        description: <$ty as crate::Prompt>::prompt(),
                        details: crate::PatternDetails::Primitive,
                    }
                }
            }
        )+
    };
}

impl_primitive_introspect!(
    CharAlphabetic => "CharAlphabetic",
    CharNumeric => "CharNumeric",
    CharAlphanumeric => "CharAlphanumeric",
);