elicitation/type_spec/
collection_contracts.rs

1//! [`ElicitSpec`](crate::ElicitSpec) implementations for collection contract types.
2
3use crate::verification::types::{
4    BTreeMapNonEmpty, BTreeSetNonEmpty, HashMapNonEmpty, HashSetNonEmpty, LinkedListNonEmpty,
5    OptionSome, ResultOk, VecDequeNonEmpty, VecNonEmpty,
6};
7use crate::{
8    ElicitSpec, SpecCategoryBuilder, SpecEntryBuilder, TypeSpec, TypeSpecBuilder,
9    TypeSpecInventoryKey,
10};
11
12macro_rules! impl_nonempty_spec {
13    (
14        type    = $ty:ty,
15        name    = $name:literal,
16        item    = $item:literal,
17        summary = $summary:literal $(,)?
18    ) => {
19        impl ElicitSpec for $ty {
20            fn type_spec() -> TypeSpec {
21                let requires = SpecCategoryBuilder::default()
22                    .name("requires".to_string())
23                    .entries(vec![
24                        SpecEntryBuilder::default()
25                            .label("non_empty".to_string())
26                            .description(
27                                concat!($item, " must contain at least one element.").to_string(),
28                            )
29                            .expression(Some(concat!("!", $item, ".is_empty()").to_string()))
30                            .build()
31                            .expect("valid SpecEntry"),
32                    ])
33                    .build()
34                    .expect("valid SpecCategory");
35                TypeSpecBuilder::default()
36                    .type_name($name.to_string())
37                    .summary($summary.to_string())
38                    .categories(vec![requires])
39                    .build()
40                    .expect("valid TypeSpec")
41            }
42        }
43
44        inventory::submit!(TypeSpecInventoryKey::new(
45            $name,
46            <$ty as ElicitSpec>::type_spec,
47            std::any::TypeId::of::<$ty>
48        ));
49    };
50}
51
52// Marker types for generic collections (inventory needs concrete types)
53// These are the ElicitSpec implementations for generic types using i32 as the
54// concrete monomorphization for inventory registration.
55
56// ── Non-empty collections ─────────────────────────────────────────────────────
57
58impl_nonempty_spec!(
59    type    = VecNonEmpty<i32>,
60    name    = "VecNonEmpty",
61    item    = "vec",
62    summary = "A Vec guaranteed to contain at least one element.",
63);
64
65impl_nonempty_spec!(
66    type    = HashMapNonEmpty<String, i32>,
67    name    = "HashMapNonEmpty",
68    item    = "map",
69    summary = "A HashMap guaranteed to contain at least one key-value pair.",
70);
71
72impl_nonempty_spec!(
73    type    = BTreeMapNonEmpty<String, i32>,
74    name    = "BTreeMapNonEmpty",
75    item    = "map",
76    summary = "A BTreeMap guaranteed to contain at least one key-value pair.",
77);
78
79impl_nonempty_spec!(
80    type    = HashSetNonEmpty<i32>,
81    name    = "HashSetNonEmpty",
82    item    = "set",
83    summary = "A HashSet guaranteed to contain at least one element.",
84);
85
86impl_nonempty_spec!(
87    type    = BTreeSetNonEmpty<i32>,
88    name    = "BTreeSetNonEmpty",
89    item    = "set",
90    summary = "A BTreeSet guaranteed to contain at least one element.",
91);
92
93impl_nonempty_spec!(
94    type    = VecDequeNonEmpty<i32>,
95    name    = "VecDequeNonEmpty",
96    item    = "deque",
97    summary = "A VecDeque guaranteed to contain at least one element.",
98);
99
100impl_nonempty_spec!(
101    type    = LinkedListNonEmpty<i32>,
102    name    = "LinkedListNonEmpty",
103    item    = "list",
104    summary = "A LinkedList guaranteed to contain at least one element.",
105);
106
107// ── Option and Result contract types ─────────────────────────────────────────
108
109impl ElicitSpec for OptionSome<i32> {
110    fn type_spec() -> TypeSpec {
111        let requires = SpecCategoryBuilder::default()
112            .name("requires".to_string())
113            .entries(vec![
114                SpecEntryBuilder::default()
115                    .label("is_some".to_string())
116                    .description("Option must be Some, not None.".to_string())
117                    .expression(Some("opt.is_some()".to_string()))
118                    .build()
119                    .expect("valid SpecEntry"),
120            ])
121            .build()
122            .expect("valid SpecCategory");
123        TypeSpecBuilder::default()
124            .type_name("OptionSome".to_string())
125            .summary("An Option<T> guaranteed to be Some(T), never None.".to_string())
126            .categories(vec![requires])
127            .build()
128            .expect("valid TypeSpec")
129    }
130}
131
132inventory::submit!(TypeSpecInventoryKey::new(
133    "OptionSome",
134    OptionSome::<i32>::type_spec,
135    std::any::TypeId::of::<OptionSome<i32>>
136));
137
138impl ElicitSpec for ResultOk<i32> {
139    fn type_spec() -> TypeSpec {
140        let requires = SpecCategoryBuilder::default()
141            .name("requires".to_string())
142            .entries(vec![
143                SpecEntryBuilder::default()
144                    .label("is_ok".to_string())
145                    .description("Result must be Ok, not Err.".to_string())
146                    .expression(Some("result.is_ok()".to_string()))
147                    .build()
148                    .expect("valid SpecEntry"),
149            ])
150            .build()
151            .expect("valid SpecCategory");
152        TypeSpecBuilder::default()
153            .type_name("ResultOk".to_string())
154            .summary("A Result<T, E> guaranteed to be Ok(T), never Err(E).".to_string())
155            .categories(vec![requires])
156            .build()
157            .expect("valid TypeSpec")
158    }
159}
160
161inventory::submit!(TypeSpecInventoryKey::new(
162    "ResultOk",
163    ResultOk::<i32>::type_spec,
164    std::any::TypeId::of::<ResultOk<i32>>
165));
elicitation/type_spec/collection_contracts.rs

elicitation/type_spec/
collection_contracts.rs
