#![allow(clippy::needless_range_loop)]

//! Property-based tests for type extraction functions in adze-common.
//!
//! Tests `try_extract_inner_type`, `filter_inner_type`, and `wrap_leaf_type`
//! with random inputs to verify no-panic guarantees, idempotency, composition,
//! and output validity properties.

use adze_common::{filter_inner_type, try_extract_inner_type, wrap_leaf_type};
use proptest::prelude::*;
use quote::ToTokens;
use std::collections::HashSet;
use syn::{Type, parse_str};

// ---------------------------------------------------------------------------
// Strategies
// ---------------------------------------------------------------------------

/// Simple leaf type names that are never container names.
fn leaf_type_name() -> impl Strategy<Value = &'static str> {
    prop::sample::select(
        &[
            "i8", "i16", "i32", "i64", "u8", "u16", "u32", "u64", "f32", "f64", "bool", "char",
            "String", "usize", "isize", "Token", "Expr", "Stmt", "Node", "Leaf",
        ][..],
    )
}

/// Container type names used for wrapping.
fn container_name() -> impl Strategy<Value = &'static str> {
    prop::sample::select(&["Box", "Vec", "Option", "Arc", "Rc"][..])
}

/// Random subsets of container names for skip-over sets.
fn skip_set_strategy() -> impl Strategy<Value = HashSet<&'static str>> {
    prop::collection::hash_set(container_name(), 0..=5)
}

/// Type strings of varying nesting depth.
fn type_string_strategy() -> impl Strategy<Value = String> {
    prop_oneof![
        // Leaf
        leaf_type_name().prop_map(|s| s.to_string()),
        // Container<Leaf>
        (container_name(), leaf_type_name()).prop_map(|(c, l)| format!("{c}<{l}>")),
        // Container<Container<Leaf>>
        (container_name(), container_name(), leaf_type_name())
            .prop_map(|(c1, c2, l)| format!("{c1}<{c2}<{l}>>")),
    ]
}

/// Non-path type strings (references, tuples, arrays, slices).
fn non_path_type_string() -> impl Strategy<Value = String> {
    prop_oneof![
        leaf_type_name().prop_map(|l| format!("& {l}")),
        (leaf_type_name(), leaf_type_name()).prop_map(|(a, b)| format!("({a} , {b})")),
        leaf_type_name().prop_map(|l| format!("[{l} ; 4]")),
        leaf_type_name().prop_map(|l| format!("& [{l}]")),
    ]
}

// ---------------------------------------------------------------------------
// Helper
// ---------------------------------------------------------------------------

fn ty_str(ty: &Type) -> String {
    ty.to_token_stream().to_string()
}

// ---------------------------------------------------------------------------
// Property tests
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(100))]

    // ===== try_extract_inner_type: no-panic & correctness =====

    // 1. Tuple types are non-path and never cause extraction.
    #[test]
    fn extract_tuple_never_extracts(
        a in leaf_type_name(),
        b in leaf_type_name(),
        target in container_name(),
    ) {
        let ty: Type = parse_str(&format!("({a}, {b})")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (_result, extracted) = try_extract_inner_type(&ty, target, &skip);
        prop_assert!(!extracted);
    }

    // 2. Array types are non-path and never cause extraction.
    #[test]
    fn extract_array_never_extracts(
        leaf in leaf_type_name(),
        target in container_name(),
    ) {
        let ty: Type = parse_str(&format!("[{leaf}; 4]")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (_result, extracted) = try_extract_inner_type(&ty, target, &skip);
        prop_assert!(!extracted);
    }

    // 3. When extraction fails on a leaf, result equals original.
    #[test]
    fn extract_fail_preserves_original(
        leaf in leaf_type_name(),
        target in container_name(),
    ) {
        let ty: Type = parse_str(leaf).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, target, &skip);
        prop_assert!(!extracted);
        prop_assert_eq!(ty_str(&result), ty_str(&ty));
    }

    // 4. Direct match on container always succeeds and returns the inner type.
    #[test]
    fn extract_direct_match_returns_inner(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, container, &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), inner);
    }

    // 5. Successful extraction produces a result with strictly fewer characters.
    #[test]
    fn extract_success_shrinks_output(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, container, &skip);
        prop_assert!(extracted);
        prop_assert!(ty_str(&result).len() < ty_str(&ty).len());
    }

    // 6. Double extraction peels two identical container layers.
    #[test]
    fn extract_double_layer(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{container}<{inner}>>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (first, ok1) = try_extract_inner_type(&ty, container, &skip);
        prop_assert!(ok1);
        let (second, ok2) = try_extract_inner_type(&first, container, &skip);
        prop_assert!(ok2);
        prop_assert_eq!(ty_str(&second), inner);
    }

    // 7. Extraction with disjoint skip set still extracts a direct top-level match.
    #[test]
    fn extract_disjoint_skip_still_extracts(inner in leaf_type_name()) {
        let ty: Type = parse_str(&format!("Vec<{inner}>")).unwrap();
        let skip: HashSet<&str> = ["Box", "Arc"].into_iter().collect();
        let (result, extracted) = try_extract_inner_type(&ty, "Vec", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), inner);
    }

    // 8. Extraction through a skip wrapper reaches nested target.
    #[test]
    fn extract_through_skip_wrapper(
        wrapper in prop::sample::select(&["Box", "Arc"][..]),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{wrapper}<Option<{inner}>>")).unwrap();
        let skip: HashSet<&str> = [wrapper].into_iter().collect();
        let (result, extracted) = try_extract_inner_type(&ty, "Option", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), inner);
    }

    // 9. Non-path types return the exact original on extraction.
    #[test]
    fn extract_non_path_returns_original(
        non_path in non_path_type_string(),
        target in container_name(),
    ) {
        let ty: Type = parse_str(&non_path).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, target, &skip);
        prop_assert!(!extracted);
        prop_assert_eq!(ty_str(&result), ty_str(&ty));
    }

    // 10. Extraction result is always a parseable Type.
    #[test]
    fn extract_result_is_parseable(
        ty_s in type_string_strategy(),
        target in container_name(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let (result, _) = try_extract_inner_type(&ty, target, &skip);
        let s = ty_str(&result);
        prop_assert!(parse_str::<Type>(&s).is_ok(), "unparseable: {s}");
    }

    // 11. Extraction is deterministic.
    #[test]
    fn extract_deterministic(
        ty_s in type_string_strategy(),
        target in container_name(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let (r1, e1) = try_extract_inner_type(&ty, target, &skip);
        let (r2, e2) = try_extract_inner_type(&ty, target, &skip);
        prop_assert_eq!(e1, e2);
        prop_assert_eq!(ty_str(&r1), ty_str(&r2));
    }

    // ===== filter_inner_type: identity, idempotency, validity =====

    // 12. Filtering a tuple type is always identity.
    #[test]
    fn filter_tuple_is_identity(
        a in leaf_type_name(),
        b in leaf_type_name(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&format!("({a}, {b})")).unwrap();
        let filtered = filter_inner_type(&ty, &skip);
        prop_assert_eq!(ty_str(&filtered), ty_str(&ty));
    }

    // 13. Filtering an array type is always identity.
    #[test]
    fn filter_array_is_identity(
        leaf in leaf_type_name(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&format!("[{leaf}; 4]")).unwrap();
        let filtered = filter_inner_type(&ty, &skip);
        prop_assert_eq!(ty_str(&filtered), ty_str(&ty));
    }

    // 14. Filtering any non-path type is identity.
    #[test]
    fn filter_non_path_is_identity(
        non_path in non_path_type_string(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&non_path).unwrap();
        let filtered = filter_inner_type(&ty, &skip);
        prop_assert_eq!(ty_str(&filtered), ty_str(&ty));
    }

    // 15. filter_inner_type is idempotent on arbitrary valid types.
    #[test]
    fn filter_idempotent(
        ty_s in type_string_strategy(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let once = filter_inner_type(&ty, &skip);
        let twice = filter_inner_type(&once, &skip);
        prop_assert_eq!(ty_str(&once), ty_str(&twice));
    }

    // 16. Filtering with a superset skip set produces same-or-smaller output.
    #[test]
    fn filter_superset_skip_no_larger(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let small_skip: HashSet<&str> = HashSet::new();
        let big_skip: HashSet<&str> = [container].into_iter().collect();
        let small_len = ty_str(&filter_inner_type(&ty, &small_skip)).len();
        let big_len = ty_str(&filter_inner_type(&ty, &big_skip)).len();
        prop_assert!(big_len <= small_len);
    }

    // 17. Filtered output is always parseable.
    #[test]
    fn filter_output_parseable(
        ty_s in type_string_strategy(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let s = ty_str(&filter_inner_type(&ty, &skip));
        prop_assert!(parse_str::<Type>(&s).is_ok(), "unparseable: {s}");
    }

    // 18. filter_inner_type is deterministic.
    #[test]
    fn filter_deterministic(
        ty_s in type_string_strategy(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let f1 = ty_str(&filter_inner_type(&ty, &skip));
        let f2 = ty_str(&filter_inner_type(&ty, &skip));
        prop_assert_eq!(f1, f2);
    }

    // ===== wrap_leaf_type: wrapping, preservation, validity =====

    // 19. Wrapping a leaf type always produces output containing WithLeaf.
    #[test]
    fn wrap_leaf_contains_with_leaf(leaf in leaf_type_name()) {
        let ty: Type = parse_str(leaf).unwrap();
        let s = ty_str(&wrap_leaf_type(&ty, &HashSet::new()));
        prop_assert!(s.contains("adze :: WithLeaf"), "expected WithLeaf: {s}");
    }

    // 20. Wrapping a non-path type always produces output containing WithLeaf.
    #[test]
    fn wrap_non_path_contains_with_leaf(non_path in non_path_type_string()) {
        let ty: Type = parse_str(&non_path).unwrap();
        let s = ty_str(&wrap_leaf_type(&ty, &HashSet::new()));
        prop_assert!(s.contains("adze :: WithLeaf"), "expected WithLeaf: {s}");
    }

    // 21. Wrapping a leaf type increases character count.
    #[test]
    fn wrap_leaf_increases_length(leaf in leaf_type_name()) {
        let ty: Type = parse_str(leaf).unwrap();
        let orig_len = ty_str(&ty).len();
        let wrapped_len = ty_str(&wrap_leaf_type(&ty, &HashSet::new())).len();
        prop_assert!(wrapped_len > orig_len);
    }

    // 22. Wrapping with a skip set preserves the container name at the front.
    #[test]
    fn wrap_preserves_skip_container_name(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let skip: HashSet<&str> = [container].into_iter().collect();
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let s = ty_str(&wrap_leaf_type(&ty, &skip));
        prop_assert!(
            s.starts_with(&format!("{container} <")),
            "expected {container} at front: {s}"
        );
    }

    // 23. Wrapping without a skip set wraps the entire container.
    #[test]
    fn wrap_no_skip_wraps_entirely(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let s = ty_str(&wrap_leaf_type(&ty, &HashSet::new()));
        prop_assert!(
            s.starts_with("adze :: WithLeaf"),
            "expected adze::WithLeaf at front: {s}"
        );
    }

    // 24. Wrapped output is always parseable.
    #[test]
    fn wrap_output_parseable(
        ty_s in type_string_strategy(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let s = ty_str(&wrap_leaf_type(&ty, &skip));
        prop_assert!(parse_str::<Type>(&s).is_ok(), "unparseable: {s}");
    }

    // 25. wrap_leaf_type is deterministic.
    #[test]
    fn wrap_deterministic(
        ty_s in type_string_strategy(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let w1 = ty_str(&wrap_leaf_type(&ty, &skip));
        let w2 = ty_str(&wrap_leaf_type(&ty, &skip));
        prop_assert_eq!(w1, w2);
    }

    // ===== Composition properties =====

    // 26. filter(extract_fail.0) equals original when extraction did not succeed.
    #[test]
    fn filter_after_failed_extract_is_identity(
        leaf in leaf_type_name(),
        target in container_name(),
    ) {
        let ty: Type = parse_str(leaf).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, target, &skip);
        prop_assert!(!extracted);
        let filtered = filter_inner_type(&result, &skip);
        prop_assert_eq!(ty_str(&filtered), ty_str(&ty));
    }

    // 27. wrap(filter(C<T>, {C})) equals wrap(T) for single-layer containers.
    #[test]
    fn wrap_of_filtered_equals_wrap_of_inner(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let skip: HashSet<&str> = [container].into_iter().collect();
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let filtered = filter_inner_type(&ty, &skip);
        let wrapped_filtered = wrap_leaf_type(&filtered, &HashSet::new());
        let inner_ty: Type = parse_str(inner).unwrap();
        let wrapped_inner = wrap_leaf_type(&inner_ty, &HashSet::new());
        prop_assert_eq!(ty_str(&wrapped_filtered), ty_str(&wrapped_inner));
    }

    // 28. extract then wrap gives adze::WithLeaf<inner> for single-layer targets.
    #[test]
    fn extract_then_wrap_gives_with_leaf(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (extracted, ok) = try_extract_inner_type(&ty, container, &skip);
        prop_assert!(ok);
        let wrapped = wrap_leaf_type(&extracted, &HashSet::new());
        prop_assert_eq!(ty_str(&wrapped), format!("adze :: WithLeaf < {inner} >"));
    }

    // 29. Extracting through skip then wrapping produces adze::WithLeaf<inner>.
    #[test]
    fn extract_through_skip_then_wrap(
        wrapper in prop::sample::select(&["Box", "Arc"][..]),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{wrapper}<Option<{inner}>>")).unwrap();
        let skip: HashSet<&str> = [wrapper].into_iter().collect();
        let (extracted, ok) = try_extract_inner_type(&ty, "Option", &skip);
        prop_assert!(ok);
        let wrapped = wrap_leaf_type(&extracted, &HashSet::new());
        prop_assert_eq!(ty_str(&wrapped), format!("adze :: WithLeaf < {inner} >"));
    }

    // 30. All three functions handle slice references without panicking.
    #[test]
    fn slice_ref_no_panic_all_functions(
        leaf in leaf_type_name(),
        target in container_name(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&format!("&[{leaf}]")).unwrap();
        let _ = try_extract_inner_type(&ty, target, &skip);
        let _ = filter_inner_type(&ty, &skip);
        let _ = wrap_leaf_type(&ty, &skip);
    }

    // 31. Wrapping nested skip containers wraps only the innermost leaf.
    #[test]
    fn wrap_nested_skips_wraps_leaf_only(inner in leaf_type_name()) {
        let skip: HashSet<&str> = ["Option", "Vec"].into_iter().collect();
        let ty: Type = parse_str(&format!("Option<Vec<{inner}>>")).unwrap();
        let s = ty_str(&wrap_leaf_type(&ty, &skip));
        prop_assert!(s.starts_with("Option <"), "outer preserved: {s}");
        prop_assert!(s.contains("Vec <"), "middle preserved: {s}");
        prop_assert!(s.contains("adze :: WithLeaf"), "leaf wrapped: {s}");
        // Exactly one WithLeaf occurrence
        let count = s.matches("WithLeaf").count();
        prop_assert!(count == 1, "expected 1 WithLeaf, got {} in: {}", count, s);
    }

    // 32. filter(ty) with empty skip equals identity for any type_string.
    #[test]
    fn filter_empty_skip_is_identity(ty_s in type_string_strategy()) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let filtered = filter_inner_type(&ty, &HashSet::new());
        prop_assert_eq!(ty_str(&filtered), ty_str(&ty));
    }

    // 33. Extracting a mismatched target from a container returns the container unchanged.
    #[test]
    fn extract_mismatch_returns_container_unchanged(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        // Only test when container != "Option"
        prop_assume!(container != "Option");
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, "Option", &skip);
        prop_assert!(!extracted);
        prop_assert_eq!(ty_str(&result), ty_str(&ty));
    }

    // 34. filter then filter then filter = filter (triple idempotency).
    #[test]
    fn filter_triple_idempotent(ty_s in type_string_strategy(), skip in skip_set_strategy()) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let f1 = filter_inner_type(&ty, &skip);
        let f2 = filter_inner_type(&f1, &skip);
        let f3 = filter_inner_type(&f2, &skip);
        prop_assert_eq!(ty_str(&f1), ty_str(&f2));
        prop_assert_eq!(ty_str(&f2), ty_str(&f3));
    }
}

// ---------------------------------------------------------------------------
// Additional targeted tests (35–64)
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(100))]

    // === Extract inner type from Option<T> ===

    // 35. Option<T> extraction always succeeds for leaf T.
    #[test]
    fn extract_option_leaf(inner in leaf_type_name()) {
        let ty: Type = parse_str(&format!("Option<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, "Option", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), inner);
    }

    // 36. Option<Container<T>> extraction yields Container<T>.
    #[test]
    fn extract_option_of_container(
        wrapper in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("Option<{wrapper}<{inner}>>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, "Option", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), format!("{wrapper} < {inner} >"));
    }

    // === Extract inner type from Vec<T> ===

    // 37. Vec<T> extraction always succeeds for leaf T.
    #[test]
    fn extract_vec_leaf(inner in leaf_type_name()) {
        let ty: Type = parse_str(&format!("Vec<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, "Vec", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), inner);
    }

    // 38. Vec<Container<T>> extraction yields Container<T>.
    #[test]
    fn extract_vec_of_container(
        wrapper in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("Vec<{wrapper}<{inner}>>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, "Vec", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), format!("{wrapper} < {inner} >"));
    }

    // === Extract inner type from Box<T> ===

    // 39. Box<T> extraction always succeeds for leaf T.
    #[test]
    fn extract_box_leaf(inner in leaf_type_name()) {
        let ty: Type = parse_str(&format!("Box<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, "Box", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), inner);
    }

    // 40. Box in skip set allows reaching Vec target inside.
    #[test]
    fn extract_box_skip_to_vec(inner in leaf_type_name()) {
        let ty: Type = parse_str(&format!("Box<Vec<{inner}>>")).unwrap();
        let skip: HashSet<&str> = ["Box"].into_iter().collect();
        let (result, extracted) = try_extract_inner_type(&ty, "Vec", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), inner);
    }

    // === Nested containers (Option<Vec<T>>) ===

    // 41. Option<Vec<T>> — extract Option yields Vec<T>.
    #[test]
    fn extract_option_vec_gets_vec(inner in leaf_type_name()) {
        let ty: Type = parse_str(&format!("Option<Vec<{inner}>>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, "Option", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), format!("Vec < {inner} >"));
    }

    // 42. Vec<Option<T>> — extract Vec yields Option<T>.
    #[test]
    fn extract_vec_option_gets_option(inner in leaf_type_name()) {
        let ty: Type = parse_str(&format!("Vec<Option<{inner}>>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, "Vec", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), format!("Option < {inner} >"));
    }

    // 43. Option<Vec<T>> — skip Option, extract Vec yields T.
    #[test]
    fn extract_option_skip_to_vec(inner in leaf_type_name()) {
        let ty: Type = parse_str(&format!("Option<Vec<{inner}>>")).unwrap();
        let skip: HashSet<&str> = ["Option"].into_iter().collect();
        let (result, extracted) = try_extract_inner_type(&ty, "Vec", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), inner);
    }

    // 44. Box<Option<Vec<T>>> — skip Box+Option, extract Vec yields T.
    #[test]
    fn extract_triple_nested_skip_two(inner in leaf_type_name()) {
        let ty: Type = parse_str(&format!("Box<Option<Vec<{inner}>>>")).unwrap();
        let skip: HashSet<&str> = ["Box", "Option"].into_iter().collect();
        let (result, extracted) = try_extract_inner_type(&ty, "Vec", &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), inner);
    }

    // === Plain types pass through unchanged ===

    // 45. Primitive types always pass through extract unchanged.
    #[test]
    fn extract_plain_primitive_passthrough(
        leaf in leaf_type_name(),
        target in container_name(),
    ) {
        let ty: Type = parse_str(leaf).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, target, &skip);
        prop_assert!(!extracted);
        prop_assert_eq!(ty_str(&result), leaf);
    }

    // 46. Plain types pass through filter unchanged with any skip set.
    #[test]
    fn filter_plain_type_passthrough(
        leaf in leaf_type_name(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(leaf).unwrap();
        let filtered = filter_inner_type(&ty, &skip);
        prop_assert_eq!(ty_str(&filtered), leaf);
    }

    // 47. Tuple types pass through extract, filter, and wrap without panic.
    #[test]
    fn all_functions_on_tuple(
        a in leaf_type_name(),
        b in leaf_type_name(),
        target in container_name(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&format!("({a}, {b})")).unwrap();
        let (_, ext) = try_extract_inner_type(&ty, target, &skip);
        prop_assert!(!ext);
        let filt = filter_inner_type(&ty, &skip);
        prop_assert_eq!(ty_str(&filt), ty_str(&ty));
        let w = wrap_leaf_type(&ty, &skip);
        prop_assert!(ty_str(&w).contains("adze :: WithLeaf"));
    }

    // === Complex generic types ===

    // 48. Container wrapping another container: inner container returned intact.
    #[test]
    fn extract_returns_inner_container_intact(
        outer in container_name(),
        inner_c in container_name(),
        leaf in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{outer}<{inner_c}<{leaf}>>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, outer, &skip);
        prop_assert!(extracted);
        prop_assert_eq!(ty_str(&result), format!("{inner_c} < {leaf} >"));
    }

    // 49. filter strips all matching skip layers from nested containers.
    #[test]
    fn filter_strips_multiple_matching_layers(
        container in container_name(),
        leaf in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{container}<{leaf}>>")).unwrap();
        let skip: HashSet<&str> = [container].into_iter().collect();
        let filtered = filter_inner_type(&ty, &skip);
        prop_assert_eq!(ty_str(&filtered), leaf);
    }

    // 50. wrap with two-level skip set wraps only the innermost leaf.
    #[test]
    fn wrap_two_level_skip(
        c1 in container_name(),
        c2 in container_name(),
        leaf in leaf_type_name(),
    ) {
        let skip: HashSet<&str> = [c1, c2].into_iter().collect();
        let ty: Type = parse_str(&format!("{c1}<{c2}<{leaf}>>")).unwrap();
        let s = ty_str(&wrap_leaf_type(&ty, &skip));
        let wl_count = s.matches("WithLeaf").count();
        prop_assert!(wl_count == 1, "expected 1 WithLeaf, got {} in: {}", wl_count, s);
    }

    // === Reference types handling ===

    // 51. &T — extraction never succeeds on reference types.
    #[test]
    fn extract_ref_never_succeeds(
        leaf in leaf_type_name(),
        target in container_name(),
    ) {
        let ty: Type = parse_str(&format!("& {leaf}")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (_, extracted) = try_extract_inner_type(&ty, target, &skip);
        prop_assert!(!extracted);
    }

    // 52. &mut T — extraction never succeeds on mutable references.
    #[test]
    fn extract_ref_mut_never_succeeds(
        leaf in leaf_type_name(),
        target in container_name(),
    ) {
        let ty: Type = parse_str(&format!("& mut {leaf}")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (_, extracted) = try_extract_inner_type(&ty, target, &skip);
        prop_assert!(!extracted);
    }

    // 53. &T — filter on reference returns identical type.
    #[test]
    fn filter_ref_identity(leaf in leaf_type_name(), skip in skip_set_strategy()) {
        let ty: Type = parse_str(&format!("& {leaf}")).unwrap();
        let filtered = filter_inner_type(&ty, &skip);
        prop_assert_eq!(ty_str(&filtered), ty_str(&ty));
    }

    // 54. &mut T — filter on mutable reference returns identical type.
    #[test]
    fn filter_ref_mut_identity(leaf in leaf_type_name(), skip in skip_set_strategy()) {
        let ty: Type = parse_str(&format!("& mut {leaf}")).unwrap();
        let filtered = filter_inner_type(&ty, &skip);
        prop_assert_eq!(ty_str(&filtered), ty_str(&ty));
    }

    // 55. Reference types are wrapped entirely by wrap_leaf_type.
    #[test]
    fn wrap_ref_wraps_entirely(leaf in leaf_type_name()) {
        let ty: Type = parse_str(&format!("& {leaf}")).unwrap();
        let s = ty_str(&wrap_leaf_type(&ty, &HashSet::new()));
        prop_assert!(s.starts_with("adze :: WithLeaf"), "expected full wrap: {s}");
    }

    // === Type extraction determinism ===

    // 56. Five repeated extractions produce identical results.
    #[test]
    fn extract_five_times_deterministic(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let results: Vec<_> = (0..5)
            .map(|_| {
                let (r, e) = try_extract_inner_type(&ty, container, &skip);
                (ty_str(&r), e)
            })
            .collect();
        for i in 1..results.len() {
            prop_assert_eq!(&results[0], &results[i]);
        }
    }

    // 57. Five repeated filters produce identical results.
    #[test]
    fn filter_five_times_deterministic(
        ty_s in type_string_strategy(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let results: Vec<_> = (0..5)
            .map(|_| ty_str(&filter_inner_type(&ty, &skip)))
            .collect();
        for i in 1..results.len() {
            prop_assert_eq!(&results[0], &results[i]);
        }
    }

    // 58. Five repeated wraps produce identical results.
    #[test]
    fn wrap_five_times_deterministic(
        ty_s in type_string_strategy(),
        skip in skip_set_strategy(),
    ) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let results: Vec<_> = (0..5)
            .map(|_| ty_str(&wrap_leaf_type(&ty, &skip)))
            .collect();
        for i in 1..results.len() {
            prop_assert_eq!(&results[0], &results[i]);
        }
    }

    // === Additional composition and edge-case properties ===

    // 59. When container is both target and in skip set, target match wins (peels one layer).
    #[test]
    fn extract_target_priority_over_skip(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{container}<{inner}>>")).unwrap();
        let skip: HashSet<&str> = [container].into_iter().collect();
        let (result, extracted) = try_extract_inner_type(&ty, container, &skip);
        prop_assert!(extracted);
        // Target match wins over skip — only one layer peeled
        prop_assert_eq!(ty_str(&result), format!("{container} < {inner} >"));
    }

    // 60. filter_inner_type on a leaf type is always identity regardless of skip set.
    #[test]
    fn filter_leaf_always_identity(leaf in leaf_type_name(), skip in skip_set_strategy()) {
        let ty: Type = parse_str(leaf).unwrap();
        let filtered = filter_inner_type(&ty, &skip);
        prop_assert_eq!(ty_str(&filtered), leaf);
    }

    // 61. Wrapping then stringifying always contains exactly one "adze :: WithLeaf" for leaves.
    #[test]
    fn wrap_leaf_exactly_one_with_leaf(leaf in leaf_type_name()) {
        let ty: Type = parse_str(leaf).unwrap();
        let s = ty_str(&wrap_leaf_type(&ty, &HashSet::new()));
        let count = s.matches("WithLeaf").count();
        prop_assert!(count == 1, "expected 1 WithLeaf, got {} in: {}", count, s);
    }

    // 62. extract(Container<T>, Container) then filter(T, {}) is identity on inner T.
    #[test]
    fn extract_then_filter_empty_is_inner(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (extracted, ok) = try_extract_inner_type(&ty, container, &skip);
        prop_assert!(ok);
        let filtered = filter_inner_type(&extracted, &skip);
        prop_assert_eq!(ty_str(&filtered), inner);
    }

    // 63. Filtered output never grows longer than the original.
    #[test]
    fn filter_never_grows(ty_s in type_string_strategy(), skip in skip_set_strategy()) {
        let ty: Type = parse_str(&ty_s).unwrap();
        let orig_len = ty_str(&ty).len();
        let filt_len = ty_str(&filter_inner_type(&ty, &skip)).len();
        prop_assert!(filt_len <= orig_len, "filter grew: {} > {}", filt_len, orig_len);
    }

    // 64. Extracting from a non-matching single-segment path is always no-op.
    #[test]
    fn extract_non_matching_segment_noop(
        container in container_name(),
        inner in leaf_type_name(),
    ) {
        prop_assume!(container != "Rc");
        let ty: Type = parse_str(&format!("{container}<{inner}>")).unwrap();
        let skip: HashSet<&str> = HashSet::new();
        let (result, extracted) = try_extract_inner_type(&ty, "Rc", &skip);
        prop_assert!(!extracted);
        prop_assert_eq!(ty_str(&result), ty_str(&ty));
    }
}
