Skip to main content

assura_stdlib/
lib.rs

1//! Assura standard library contracts and prelude types.
2//!
3//! This crate provides:
4//! - Standard library `.assura` contract files (math, string, collections)
5//! - The prelude: types and contracts auto-imported into every Assura file
6//! - A stable API for querying stdlib definitions
7
8use assura_parser::ast::{Decl, SourceFile};
9
10/// Embedded standard library contract source files.
11pub struct StdlibSources;
12
13impl StdlibSources {
14    /// Return the math module source.
15    pub fn math() -> &'static str {
16        include_str!("../std/math.assura")
17    }
18
19    /// Return the string module source.
20    pub fn string() -> &'static str {
21        include_str!("../std/string.assura")
22    }
23
24    /// Return the collections module source.
25    pub fn collections() -> &'static str {
26        include_str!("../std/collections.assura")
27    }
28
29    /// Return the option module source.
30    pub fn option() -> &'static str {
31        include_str!("../std/option.assura")
32    }
33
34    /// Return the result module source.
35    pub fn results() -> &'static str {
36        include_str!("../std/result.assura")
37    }
38
39    /// Return the io module source.
40    pub fn io() -> &'static str {
41        include_str!("../std/io.assura")
42    }
43
44    /// Return the fs module source.
45    pub fn fs() -> &'static str {
46        include_str!("../std/fs.assura")
47    }
48
49    /// Return the net module source.
50    pub fn net() -> &'static str {
51        include_str!("../std/net.assura")
52    }
53
54    /// Return the crypto module source.
55    pub fn crypto() -> &'static str {
56        include_str!("../std/crypto.assura")
57    }
58
59    /// Return the iter module source.
60    pub fn iter() -> &'static str {
61        include_str!("../std/iter.assura")
62    }
63
64    /// Return the bytes module source.
65    pub fn bytes() -> &'static str {
66        include_str!("../std/bytes.assura")
67    }
68
69    /// Return the time module source.
70    pub fn time() -> &'static str {
71        include_str!("../std/time.assura")
72    }
73
74    /// Return all standard library sources with their module names.
75    pub fn all() -> Vec<(&'static str, &'static str)> {
76        vec![
77            ("std.math", Self::math()),
78            ("std.string", Self::string()),
79            ("std.collections", Self::collections()),
80            ("std.option", Self::option()),
81            ("std.results", Self::results()),
82            ("std.io", Self::io()),
83            ("std.fs", Self::fs()),
84            ("std.net", Self::net()),
85            ("std.crypto", Self::crypto()),
86            ("std.iter", Self::iter()),
87            ("std.bytes", Self::bytes()),
88            ("std.time", Self::time()),
89        ]
90    }
91}
92
93/// A parsed standard library contract.
94#[derive(Debug, Clone)]
95pub struct StdlibContract {
96    /// The contract name (e.g., "abs", "min", "list_get").
97    pub name: String,
98    /// The module it belongs to (e.g., "std.math").
99    pub module: String,
100}
101
102/// Parse all standard library modules and extract contract names.
103pub fn stdlib_contracts() -> Vec<StdlibContract> {
104    let mut contracts = Vec::new();
105    for (module_name, source) in StdlibSources::all() {
106        let (parsed, _errors) = assura_parser::parse(source);
107        if let Some(file) = parsed {
108            for decl in &file.decls {
109                if let Decl::Contract(c) = &decl.node {
110                    contracts.push(StdlibContract {
111                        name: c.name.clone(),
112                        module: module_name.to_string(),
113                    });
114                }
115            }
116        }
117    }
118    contracts
119}
120
121/// Parse all standard library modules and return their ASTs.
122pub fn parse_stdlib() -> Vec<(String, SourceFile)> {
123    let mut modules = Vec::new();
124    for (module_name, source) in StdlibSources::all() {
125        let (parsed, _errors) = assura_parser::parse(source);
126        if let Some(file) = parsed {
127            modules.push((module_name.to_string(), file));
128        }
129    }
130    modules
131}
132
133/// Prelude type names that are available without explicit import.
134///
135/// These types are injected into the type environment at the start
136/// of type checking, so users can write `List<Int>` without
137/// `import std.collections`.
138pub fn prelude_type_names() -> Vec<&'static str> {
139    vec![
140        "Int",
141        "Nat",
142        "Float",
143        "Bool",
144        "String",
145        "Bytes",
146        "Unit",
147        "List",
148        "Map",
149        "Set",
150        "Option",
151        "Result",
152        // Refinement types from the existing stdlib
153        "Pos",
154        "NonNeg",
155        "Email",
156        "Uuid",
157        "Port",
158        "Percentage",
159    ]
160}
161
162/// Prelude contract names that are available without explicit import.
163pub fn prelude_contract_names() -> Vec<&'static str> {
164    vec!["abs", "min", "max", "clamp"]
165}
166
167#[cfg(test)]
168mod tests {
169    use super::*;
170
171    #[test]
172    fn math_source_parses() {
173        let source = StdlibSources::math();
174        let (parsed, errors) = assura_parser::parse(source);
175        assert!(errors.is_empty(), "math.assura parse errors: {errors:?}");
176        let file = parsed.expect("math.assura should parse");
177        assert!(file.module.is_some(), "should have module declaration");
178        assert!(!file.decls.is_empty(), "should have declarations");
179    }
180
181    #[test]
182    fn string_source_parses() {
183        let source = StdlibSources::string();
184        let (parsed, errors) = assura_parser::parse(source);
185        assert!(errors.is_empty(), "string.assura parse errors: {errors:?}");
186        let file = parsed.expect("string.assura should parse");
187        file.module.unwrap();
188        assert!(!file.decls.is_empty());
189    }
190
191    #[test]
192    fn collections_source_parses() {
193        let source = StdlibSources::collections();
194        let (parsed, errors) = assura_parser::parse(source);
195        assert!(
196            errors.is_empty(),
197            "collections.assura parse errors: {errors:?}"
198        );
199        let file = parsed.expect("collections.assura should parse");
200        file.module.unwrap();
201        assert!(!file.decls.is_empty());
202    }
203
204    #[test]
205    fn stdlib_has_at_least_ten_contracts() {
206        let contracts = stdlib_contracts();
207        assert!(
208            contracts.len() >= 10,
209            "stdlib should have at least 10 contracts, got {}",
210            contracts.len()
211        );
212    }
213
214    #[test]
215    fn stdlib_contracts_have_expected_names() {
216        let contracts = stdlib_contracts();
217        let names: Vec<&str> = contracts.iter().map(|c| c.name.as_str()).collect();
218        assert!(names.contains(&"abs"), "missing abs");
219        assert!(names.contains(&"min"), "missing min");
220        assert!(names.contains(&"max"), "missing max");
221        assert!(names.contains(&"clamp"), "missing clamp");
222        assert!(names.contains(&"string_length"), "missing string_length");
223        assert!(names.contains(&"contains"), "missing contains");
224        assert!(names.contains(&"list_get"), "missing list_get");
225        assert!(names.contains(&"list_push"), "missing list_push");
226        assert!(names.contains(&"map_get"), "missing map_get");
227        assert!(names.contains(&"set_contains"), "missing set_contains");
228    }
229
230    #[test]
231    fn stdlib_contracts_have_modules() {
232        let contracts = stdlib_contracts();
233        for c in &contracts {
234            assert!(
235                c.module.starts_with("std."),
236                "contract {} should be in std.* module, got {}",
237                c.name,
238                c.module
239            );
240        }
241    }
242
243    #[test]
244    fn parse_stdlib_returns_all_modules() {
245        let modules = parse_stdlib();
246        assert_eq!(modules.len(), 12, "should have 12 stdlib modules");
247        let names: Vec<&str> = modules.iter().map(|(n, _)| n.as_str()).collect();
248        assert!(names.contains(&"std.math"));
249        assert!(names.contains(&"std.string"));
250        assert!(names.contains(&"std.collections"));
251        assert!(names.contains(&"std.option"));
252        assert!(names.contains(&"std.results"));
253        assert!(names.contains(&"std.io"));
254        assert!(names.contains(&"std.fs"));
255        assert!(names.contains(&"std.net"));
256        assert!(names.contains(&"std.crypto"));
257        assert!(names.contains(&"std.iter"));
258        assert!(names.contains(&"std.bytes"));
259        assert!(names.contains(&"std.time"));
260    }
261
262    #[test]
263    fn prelude_includes_core_types() {
264        let types = prelude_type_names();
265        assert!(types.contains(&"Int"));
266        assert!(types.contains(&"Bool"));
267        assert!(types.contains(&"List"));
268        assert!(types.contains(&"Map"));
269        assert!(types.contains(&"Set"));
270        assert!(types.contains(&"Nat"));
271    }
272
273    #[test]
274    fn prelude_includes_refinement_types() {
275        let types = prelude_type_names();
276        assert!(types.contains(&"Pos"));
277        assert!(types.contains(&"NonNeg"));
278        assert!(types.contains(&"Port"));
279    }
280
281    #[test]
282    fn all_sources_returns_twelve_modules() {
283        let all = StdlibSources::all();
284        assert_eq!(all.len(), 12);
285    }
286
287    #[test]
288    fn math_has_four_contracts() {
289        let (parsed, _) = assura_parser::parse(StdlibSources::math());
290        let file = parsed.unwrap();
291        let count = file
292            .decls
293            .iter()
294            .filter(|d| matches!(&d.node, Decl::Contract(_)))
295            .count();
296        assert_eq!(count, 9, "math should have 9 contracts");
297    }
298
299    #[test]
300    fn string_has_three_contracts() {
301        let (parsed, _) = assura_parser::parse(StdlibSources::string());
302        let file = parsed.unwrap();
303        let count = file
304            .decls
305            .iter()
306            .filter(|d| matches!(&d.node, Decl::Contract(_)))
307            .count();
308        assert_eq!(count, 12, "string should have 12 contracts");
309    }
310
311    #[test]
312    fn collections_has_six_contracts() {
313        let (parsed, _) = assura_parser::parse(StdlibSources::collections());
314        let file = parsed.unwrap();
315        let count = file
316            .decls
317            .iter()
318            .filter(|d| matches!(&d.node, Decl::Contract(_)))
319            .count();
320        assert_eq!(count, 14, "collections should have 14 contracts");
321    }
322
323    #[test]
324    fn option_contracts_are_generic() {
325        let (parsed, errors) = assura_parser::parse(StdlibSources::option());
326        assert!(errors.is_empty(), "option.assura parse errors: {errors:?}");
327        let file = parsed.unwrap();
328        for decl in &file.decls {
329            if let Decl::Contract(c) = &decl.node {
330                assert!(
331                    !c.type_params.is_empty(),
332                    "contract {} should have type params",
333                    c.name
334                );
335            }
336        }
337    }
338
339    #[test]
340    fn result_contracts_are_generic() {
341        let (parsed, errors) = assura_parser::parse(StdlibSources::results());
342        assert!(errors.is_empty(), "result.assura parse errors: {errors:?}");
343        let file = parsed.unwrap();
344        for decl in &file.decls {
345            if let Decl::Contract(c) = &decl.node {
346                assert!(
347                    !c.type_params.is_empty(),
348                    "contract {} should have type params",
349                    c.name
350                );
351            }
352        }
353    }
354
355    #[test]
356    fn collections_contracts_are_generic() {
357        let (parsed, errors) = assura_parser::parse(StdlibSources::collections());
358        assert!(
359            errors.is_empty(),
360            "collections.assura parse errors: {errors:?}"
361        );
362        let file = parsed.unwrap();
363        for decl in &file.decls {
364            if let Decl::Contract(c) = &decl.node {
365                assert!(
366                    !c.type_params.is_empty(),
367                    "contract {} should have type params",
368                    c.name
369                );
370            }
371        }
372    }
373
374    #[test]
375    fn generic_contracts_have_ensures_clauses() {
376        let key_contracts = ["list_push", "list_get", "map_insert", "map_get", "unwrap"];
377        let modules = parse_stdlib();
378        for (_, file) in &modules {
379            for decl in &file.decls {
380                if let Decl::Contract(c) = &decl.node {
381                    if key_contracts.contains(&c.name.as_str()) {
382                        let has_ensures = c
383                            .clauses
384                            .iter()
385                            .any(|cl| cl.kind == assura_parser::ast::ClauseKind::Ensures);
386                        assert!(
387                            has_ensures,
388                            "contract {} should have at least one ensures clause",
389                            c.name
390                        );
391                    }
392                }
393            }
394        }
395    }
396
397    #[test]
398    fn result_module_name_is_std_results() {
399        // Module uses plural "results" because "result" is a keyword in Assura
400        let (parsed, _) = assura_parser::parse(StdlibSources::results());
401        let file = parsed.unwrap();
402        let module_path = file.module.as_ref().map(|m| m.path.join("."));
403        assert_eq!(
404            module_path.as_deref(),
405            Some("std.results"),
406            "module name should be std.results (result is a keyword)"
407        );
408    }
409}