oxilean_kernel/universe/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::level;
6use crate::{Level, Name};
7use std::collections::{HashMap, HashSet};
8
9use super::types::{
10    ConfigNode, DecisionNode, Either2, FlatSubstitution, FocusStack, LabelSet,
11    LevelComparisonTable, LevelNormalForm, NonEmptyVec, PathBuf, RewriteRule, RewriteRuleSet,
12    SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch, StringPool,
13    TokenBucket, TransformStat, TransitiveClosure, UnivChecker, UnivConstraint, UnivConstraintSet,
14    UnivPolySignature, UnivSatChecker, UniverseInstantiation, VersionedRecord, WindowIterator,
15    WriteOnce,
16};
17
18#[cfg(test)]
19mod tests {
20    use super::*;
21    #[test]
22    fn test_create_checker() {
23        let checker = UnivChecker::new();
24        assert_eq!(checker.all_constraints().len(), 0);
25        assert_eq!(checker.all_univ_vars().len(), 0);
26    }
27    #[test]
28    fn test_add_univ_var() {
29        let mut checker = UnivChecker::new();
30        checker.add_univ_var(Name::str("u"));
31        assert_eq!(checker.all_univ_vars().len(), 1);
32    }
33    #[test]
34    fn test_satisfiable_lt() {
35        let mut checker = UnivChecker::new();
36        checker.add_constraint(UnivConstraint::Lt(
37            Level::zero(),
38            Level::succ(Level::zero()),
39        ));
40        assert!(checker.check().is_ok());
41    }
42    #[test]
43    fn test_unsatisfiable_lt() {
44        let mut checker = UnivChecker::new();
45        let u = Level::succ(Level::zero());
46        checker.add_constraint(UnivConstraint::Lt(u.clone(), u));
47        assert!(checker.check().is_err());
48    }
49    #[test]
50    fn test_satisfiable_eq() {
51        let mut checker = UnivChecker::new();
52        let u = Level::zero();
53        checker.add_constraint(UnivConstraint::Eq(u.clone(), u));
54        assert!(checker.check().is_ok());
55    }
56    #[test]
57    fn test_le_constraint() {
58        let mut checker = UnivChecker::new();
59        checker.add_constraint(UnivConstraint::Le(
60            Level::zero(),
61            Level::succ(Level::zero()),
62        ));
63        assert!(checker.check().is_ok());
64    }
65    #[test]
66    fn test_le_equal() {
67        let mut checker = UnivChecker::new();
68        let l = Level::succ(Level::zero());
69        checker.add_constraint(UnivConstraint::Le(l.clone(), l));
70        assert!(checker.check().is_ok());
71    }
72    #[test]
73    fn test_le_violation() {
74        let mut checker = UnivChecker::new();
75        checker.add_constraint(UnivConstraint::Le(
76            Level::succ(Level::succ(Level::zero())),
77            Level::succ(Level::zero()),
78        ));
79        assert!(checker.check().is_err());
80    }
81    #[test]
82    fn test_level_def_eq_normalized() {
83        let checker = UnivChecker::new();
84        let l1 = Level::max(Level::param(Name::str("u")), Level::param(Name::str("v")));
85        let l2 = Level::max(Level::param(Name::str("v")), Level::param(Name::str("u")));
86        assert!(checker.is_level_def_eq(&l1, &l2));
87    }
88    #[test]
89    fn test_level_mvar_assignment() {
90        let mut checker = UnivChecker::new();
91        let m = checker.fresh_level_mvar();
92        let one = Level::succ(Level::zero());
93        if let Level::MVar(id) = &m {
94            checker.assign_mvar(*id, one.clone());
95        }
96        checker.add_constraint(UnivConstraint::Eq(m, one));
97        assert!(checker.check().is_ok());
98    }
99    #[test]
100    fn test_solve_simple() {
101        let mut checker = UnivChecker::new();
102        let m = checker.fresh_level_mvar();
103        let two = Level::succ(Level::succ(Level::zero()));
104        checker.add_constraint(UnivConstraint::Eq(m.clone(), two.clone()));
105        assert!(checker.solve_simple());
106        if let Level::MVar(id) = &m {
107            assert_eq!(checker.get_mvar_assignment(id), Some(&two));
108        }
109    }
110    #[test]
111    fn test_is_geq() {
112        let checker = UnivChecker::new();
113        assert!(checker.is_geq(&Level::succ(Level::zero()), &Level::zero()));
114        assert!(checker.is_geq(&Level::zero(), &Level::zero()));
115        assert!(!checker.is_geq(&Level::zero(), &Level::succ(Level::zero())));
116    }
117    #[test]
118    fn test_is_gt() {
119        let checker = UnivChecker::new();
120        assert!(checker.is_gt(&Level::succ(Level::zero()), &Level::zero()));
121        assert!(!checker.is_gt(&Level::zero(), &Level::zero()));
122    }
123    #[test]
124    fn test_clear() {
125        let mut checker = UnivChecker::new();
126        checker.add_constraint(UnivConstraint::Eq(Level::zero(), Level::zero()));
127        let m = checker.fresh_level_mvar();
128        if let Level::MVar(id) = &m {
129            checker.assign_mvar(*id, Level::zero());
130        }
131        checker.clear();
132        assert_eq!(checker.all_constraints().len(), 0);
133    }
134}
135/// Compute the maximum of two universe levels.
136pub fn level_max(l1: Level, l2: Level) -> Level {
137    Level::max(l1, l2)
138}
139/// Compute succ(l).
140pub fn level_succ(l: Level) -> Level {
141    Level::succ(l)
142}
143/// Compute imax(l1, l2).
144pub fn level_imax(l1: Level, l2: Level) -> Level {
145    Level::imax(l1, l2)
146}
147/// The type of Sort(l) is Sort(succ(l)).
148pub fn sort_type_level(l: &Level) -> Level {
149    Level::succ(l.clone())
150}
151/// The Pi type level: imax(domain, codomain).
152pub fn pi_type_level(domain: &Level, codomain: &Level) -> Level {
153    Level::imax(domain.clone(), codomain.clone())
154}
155/// Convert a concrete level to a natural number.
156pub fn level_to_nat(l: &Level) -> Option<u32> {
157    match l {
158        Level::Zero => Some(0),
159        Level::Succ(inner) => level_to_nat(inner).map(|n| n + 1),
160        Level::Max(a, b) => {
161            let a_n = level_to_nat(a)?;
162            let b_n = level_to_nat(b)?;
163            Some(a_n.max(b_n))
164        }
165        Level::IMax(a, b) => {
166            let b_n = level_to_nat(b)?;
167            if b_n == 0 {
168                Some(0)
169            } else {
170                let a_n = level_to_nat(a)?;
171                Some(a_n.max(b_n))
172            }
173        }
174        Level::Param(_) | Level::MVar(_) => None,
175    }
176}
177/// Prop = Sort 0.
178pub fn prop_level() -> Level {
179    Level::zero()
180}
181/// Type 0 = Sort 1.
182pub fn type0_level() -> Level {
183    Level::succ(Level::zero())
184}
185/// Type 1 = Sort 2.
186pub fn type1_level() -> Level {
187    Level::succ(Level::succ(Level::zero()))
188}
189/// Check if a level is definitionally Prop.
190pub fn is_prop_level(l: &Level) -> bool {
191    level::is_equivalent(l, &Level::zero())
192}
193/// Count succ constructors in a concrete level.
194pub fn count_succs(l: &Level) -> Option<u32> {
195    match l {
196        Level::Zero => Some(0),
197        Level::Succ(inner) => count_succs(inner).map(|n| n + 1),
198        _ => None,
199    }
200}
201/// Peel off n succ constructors.
202pub fn peel_succs(l: &Level, n: u32) -> Option<Level> {
203    if n == 0 {
204        return Some(l.clone());
205    }
206    match l {
207        Level::Succ(inner) => peel_succs(inner, n - 1),
208        _ => None,
209    }
210}
211/// Add n succ constructors to a level.
212pub fn add_succs(l: Level, n: u32) -> Level {
213    let mut r = l;
214    for _ in 0..n {
215        r = Level::succ(r);
216    }
217    r
218}
219/// Collect universe parameters in a level expression.
220pub fn collect_level_params(l: &Level) -> Vec<Name> {
221    let mut params = std::collections::HashSet::new();
222    collect_level_params_impl(l, &mut params);
223    let mut result: Vec<Name> = params.into_iter().collect();
224    result.sort_by(|a, b| format!("{}", a).cmp(&format!("{}", b)));
225    result
226}
227fn collect_level_params_impl(l: &Level, params: &mut std::collections::HashSet<Name>) {
228    match l {
229        Level::Param(name) => {
230            params.insert(name.clone());
231        }
232        Level::Succ(inner) => collect_level_params_impl(inner, params),
233        Level::Max(a, b) | Level::IMax(a, b) => {
234            collect_level_params_impl(a, params);
235            collect_level_params_impl(b, params);
236        }
237        Level::Zero | Level::MVar(_) => {}
238    }
239}
240/// Substitute a universe parameter.
241pub fn substitute_level_param(l: &Level, param_name: &Name, replacement: &Level) -> Level {
242    match l {
243        Level::Param(name) if name == param_name => replacement.clone(),
244        Level::Succ(inner) => Level::succ(substitute_level_param(inner, param_name, replacement)),
245        Level::Max(a, b) => Level::max(
246            substitute_level_param(a, param_name, replacement),
247            substitute_level_param(b, param_name, replacement),
248        ),
249        Level::IMax(a, b) => Level::imax(
250            substitute_level_param(a, param_name, replacement),
251            substitute_level_param(b, param_name, replacement),
252        ),
253        Level::Zero | Level::Param(_) | Level::MVar(_) => l.clone(),
254    }
255}
256/// Format a level as a string.
257pub fn format_level(l: &Level) -> String {
258    match l {
259        Level::Zero => "0".to_string(),
260        Level::Succ(_) => {
261            if let Some(n) = count_succs(l) {
262                if n <= 4 {
263                    return n.to_string();
264                }
265            }
266            if let Level::Succ(inner) = l {
267                format!("succ({})", format_level(inner))
268            } else {
269                "?".to_string()
270            }
271        }
272        Level::Max(a, b) => format!("max({}, {})", format_level(a), format_level(b)),
273        Level::IMax(a, b) => format!("imax({}, {})", format_level(a), format_level(b)),
274        Level::Param(name) => format!("{}", name),
275        Level::MVar(id) => format!("?u{}", id.0),
276    }
277}
278/// Parse a simple level from string.
279pub fn parse_level_str(s: &str) -> Option<Level> {
280    match s.trim() {
281        "0" => Some(Level::zero()),
282        "1" => Some(Level::succ(Level::zero())),
283        "2" => Some(Level::succ(Level::succ(Level::zero()))),
284        "Prop" => Some(Level::zero()),
285        "Type" => Some(Level::succ(Level::zero())),
286        s if s.starts_with("succ(") && s.ends_with(')') => {
287            parse_level_str(&s[5..s.len() - 1]).map(Level::succ)
288        }
289        s if s
290            .chars()
291            .all(|c| c.is_alphanumeric() || c == '_' || c == '.') =>
292        {
293            Some(Level::param(Name::str(s)))
294        }
295        _ => None,
296    }
297}
298pub(super) fn collect_nf_comps(l: &Level, offset: u32, comps: &mut Vec<(Option<Name>, u32)>) {
299    match l {
300        Level::Zero => comps.push((None, offset)),
301        Level::Param(name) => comps.push((Some(name.clone()), offset)),
302        Level::Succ(inner) => collect_nf_comps(inner, offset + 1, comps),
303        Level::Max(a, b) => {
304            collect_nf_comps(a, offset, comps);
305            collect_nf_comps(b, offset, comps);
306        }
307        Level::IMax(a, b) => {
308            collect_nf_comps(a, offset, comps);
309            collect_nf_comps(b, offset, comps);
310        }
311        Level::MVar(_) => {}
312    }
313}
314#[cfg(test)]
315mod universe_arith_tests {
316    use super::*;
317    #[test]
318    fn test_level_to_nat_zero() {
319        assert_eq!(level_to_nat(&Level::zero()), Some(0));
320    }
321    #[test]
322    fn test_level_to_nat_succ() {
323        assert_eq!(level_to_nat(&Level::succ(Level::zero())), Some(1));
324        assert_eq!(
325            level_to_nat(&Level::succ(Level::succ(Level::zero()))),
326            Some(2)
327        );
328    }
329    #[test]
330    fn test_level_to_nat_param() {
331        assert_eq!(level_to_nat(&Level::param(Name::str("u"))), None);
332    }
333    #[test]
334    fn test_is_prop_level() {
335        assert!(is_prop_level(&Level::zero()));
336        assert!(!is_prop_level(&Level::succ(Level::zero())));
337    }
338    #[test]
339    fn test_pi_type_level() {
340        let pi_l = pi_type_level(&Level::zero(), &Level::succ(Level::zero()));
341        assert!(level::is_equivalent(&pi_l, &Level::succ(Level::zero())));
342    }
343    #[test]
344    fn test_collect_level_params() {
345        let l = Level::max(
346            Level::param(Name::str("u")),
347            Level::succ(Level::param(Name::str("v"))),
348        );
349        let params = collect_level_params(&l);
350        assert!(params.contains(&Name::str("u")));
351        assert!(params.contains(&Name::str("v")));
352    }
353    #[test]
354    fn test_substitute_level_param() {
355        let l = Level::succ(Level::param(Name::str("u")));
356        let result = substitute_level_param(&l, &Name::str("u"), &Level::zero());
357        assert_eq!(result, Level::succ(Level::zero()));
358    }
359    #[test]
360    fn test_add_succs() {
361        let result = add_succs(Level::zero(), 3);
362        assert_eq!(level_to_nat(&result), Some(3));
363    }
364    #[test]
365    fn test_peel_succs() {
366        let l = Level::succ(Level::succ(Level::succ(Level::zero())));
367        assert_eq!(peel_succs(&l, 3), Some(Level::zero()));
368        assert_eq!(peel_succs(&l, 4), None);
369    }
370    #[test]
371    fn test_parse_level_str() {
372        assert_eq!(parse_level_str("0"), Some(Level::zero()));
373        assert_eq!(parse_level_str("1"), Some(Level::succ(Level::zero())));
374        assert_eq!(parse_level_str("u"), Some(Level::param(Name::str("u"))));
375    }
376    #[test]
377    fn test_format_level() {
378        assert_eq!(format_level(&Level::zero()), "0");
379        assert_eq!(format_level(&Level::succ(Level::zero())), "1");
380    }
381    #[test]
382    fn test_sat_checker() {
383        let mut checker = UnivSatChecker::new();
384        checker.add_lower_bound(Name::str("u"), 1);
385        checker.add_upper_bound(Name::str("u"), 3);
386        assert!(checker.is_satisfiable());
387    }
388    #[test]
389    fn test_sat_checker_unsat() {
390        let mut checker = UnivSatChecker::new();
391        checker.add_lower_bound(Name::str("u"), 5);
392        checker.add_upper_bound(Name::str("u"), 3);
393        assert!(!checker.is_satisfiable());
394    }
395    #[test]
396    fn test_sort_type_level() {
397        assert_eq!(sort_type_level(&Level::zero()), Level::succ(Level::zero()));
398    }
399    #[test]
400    fn test_prop_level() {
401        assert_eq!(prop_level(), Level::zero());
402    }
403    #[test]
404    fn test_count_succs() {
405        assert_eq!(count_succs(&Level::zero()), Some(0));
406        assert_eq!(count_succs(&Level::succ(Level::zero())), Some(1));
407    }
408    #[test]
409    fn test_level_normal_form() {
410        let l = Level::max(Level::succ(Level::zero()), Level::zero());
411        let nf = LevelNormalForm::from_level(&l);
412        assert!(!nf.components.is_empty());
413    }
414    #[test]
415    fn test_type0_type1() {
416        assert_eq!(level_to_nat(&type0_level()), Some(1));
417        assert_eq!(level_to_nat(&type1_level()), Some(2));
418    }
419    #[test]
420    fn test_level_max_fn() {
421        let l = level_max(Level::zero(), Level::succ(Level::zero()));
422        assert!(level::is_equivalent(&l, &Level::succ(Level::zero())));
423    }
424    #[test]
425    fn test_level_succ_fn() {
426        assert_eq!(level_succ(Level::zero()), Level::succ(Level::zero()));
427    }
428}
429/// Compute the maximum of a list of levels.
430///
431/// Returns `Level::Zero` for an empty list.
432#[allow(dead_code)]
433pub fn level_max_many(levels: &[Level]) -> Level {
434    levels
435        .iter()
436        .fold(Level::zero(), |acc, l| level_max(acc, l.clone()))
437}
438/// Check whether a level is *structurally* a max-expression.
439#[allow(dead_code)]
440pub fn is_max_level(l: &Level) -> bool {
441    matches!(l, Level::Max(_, _))
442}
443/// Check whether a level is *structurally* an imax-expression.
444#[allow(dead_code)]
445pub fn is_imax_level(l: &Level) -> bool {
446    matches!(l, Level::IMax(_, _))
447}
448/// Return the depth of nesting of `Succ` constructors.
449///
450/// `count_succs(succ(succ(zero))) == 2`
451#[allow(dead_code)]
452pub fn count_succ_depth(l: &Level) -> u32 {
453    let mut depth = 0u32;
454    let mut cur = l;
455    while let Level::Succ(inner) = cur {
456        depth += 1;
457        cur = inner;
458    }
459    depth
460}
461/// Compute the `n`-th successor of a level.
462///
463/// `add_succ_n(zero, 3) == succ(succ(succ(zero)))`
464#[allow(dead_code)]
465pub fn add_succ_n(l: Level, n: u32) -> Level {
466    (0..n).fold(l, |acc, _| Level::succ(acc))
467}
468/// Attempt to evaluate a closed level to a concrete `u32`.
469///
470/// Returns `None` if the level contains `Param` or `MVar` nodes.
471#[allow(dead_code)]
472pub fn eval_closed_level(l: &Level) -> Option<u32> {
473    level_to_nat(l)
474}
475/// Check whether two levels have the same structural shape (ignoring parameters).
476#[allow(dead_code)]
477pub fn same_level_shape(l1: &Level, l2: &Level) -> bool {
478    match (l1, l2) {
479        (Level::Zero, Level::Zero) => true,
480        (Level::Succ(a), Level::Succ(b)) => same_level_shape(a, b),
481        (Level::Max(a1, b1), Level::Max(a2, b2)) => {
482            same_level_shape(a1, a2) && same_level_shape(b1, b2)
483        }
484        (Level::IMax(a1, b1), Level::IMax(a2, b2)) => {
485            same_level_shape(a1, a2) && same_level_shape(b1, b2)
486        }
487        (Level::Param(_), Level::Param(_)) => true,
488        (Level::MVar(_), Level::MVar(_)) => true,
489        _ => false,
490    }
491}
492/// Check if an instantiation is valid for a given list of universe parameters.
493pub fn is_valid_instantiation(params: &[Name], inst: &UniverseInstantiation) -> bool {
494    params.iter().all(|p| inst.subst.contains_key(p))
495}
496/// Instantiate a list of levels using the given substitution map.
497pub fn instantiate_levels(levels: &[Level], params: &[Name], args: &[Level]) -> Vec<Level> {
498    let mut inst = UniverseInstantiation::new();
499    for (p, l) in params.iter().zip(args.iter()) {
500        inst.add(p.clone(), l.clone());
501    }
502    levels.iter().map(|l| inst.apply(l)).collect()
503}
504#[cfg(test)]
505mod poly_tests {
506    use super::*;
507    #[test]
508    fn test_universe_instantiation_apply() {
509        let mut inst = UniverseInstantiation::new();
510        inst.add(Name::str("u"), Level::succ(Level::zero()));
511        let l = Level::param(Name::str("u"));
512        let result = inst.apply(&l);
513        assert_eq!(result, Level::succ(Level::zero()));
514    }
515    #[test]
516    fn test_universe_instantiation_compose() {
517        let mut inst1 = UniverseInstantiation::new();
518        inst1.add(Name::str("v"), Level::zero());
519        let mut inst2 = UniverseInstantiation::new();
520        inst2.add(Name::str("u"), Level::param(Name::str("v")));
521        let composed = inst1.compose(&inst2);
522        let l = Level::param(Name::str("u"));
523        let result = composed.apply(&l);
524        assert_eq!(result, Level::zero());
525    }
526    #[test]
527    fn test_is_valid_instantiation() {
528        let mut inst = UniverseInstantiation::new();
529        inst.add(Name::str("u"), Level::zero());
530        let params = vec![Name::str("u")];
531        assert!(is_valid_instantiation(&params, &inst));
532        let params2 = vec![Name::str("u"), Name::str("v")];
533        assert!(!is_valid_instantiation(&params2, &inst));
534    }
535    #[test]
536    fn test_instantiate_levels() {
537        let levels = vec![
538            Level::param(Name::str("u")),
539            Level::succ(Level::param(Name::str("u"))),
540        ];
541        let params = vec![Name::str("u")];
542        let args = vec![Level::zero()];
543        let result = instantiate_levels(&levels, &params, &args);
544        assert_eq!(result[0], Level::zero());
545        assert_eq!(result[1], Level::succ(Level::zero()));
546    }
547    #[test]
548    fn test_univ_constraint_set_dedup() {
549        let mut s = UnivConstraintSet::new();
550        s.add(UnivConstraint::Eq(Level::zero(), Level::zero()));
551        s.add(UnivConstraint::Eq(Level::zero(), Level::zero()));
552        s.dedup();
553        assert_eq!(s.len(), 1);
554    }
555    #[test]
556    fn test_univ_constraint_set_merge() {
557        let mut s1 = UnivConstraintSet::new();
558        s1.add(UnivConstraint::Le(
559            Level::zero(),
560            Level::succ(Level::zero()),
561        ));
562        let mut s2 = UnivConstraintSet::new();
563        s2.add(UnivConstraint::Eq(Level::zero(), Level::zero()));
564        s1.merge(&s2);
565        assert_eq!(s1.len(), 2);
566    }
567    #[test]
568    fn test_univ_poly_signature_instantiate() {
569        let sig = UnivPolySignature::new(vec![Name::str("u"), Name::str("v")]);
570        let args = vec![Level::zero(), Level::succ(Level::zero())];
571        let inst = sig.instantiate(&args).expect("inst should be present");
572        assert_eq!(inst.apply(&Level::param(Name::str("u"))), Level::zero());
573        assert_eq!(
574            inst.apply(&Level::param(Name::str("v"))),
575            Level::succ(Level::zero())
576        );
577    }
578    #[test]
579    fn test_univ_poly_signature_wrong_arity() {
580        let sig = UnivPolySignature::new(vec![Name::str("u")]);
581        assert!(sig.instantiate(&[]).is_none());
582    }
583    #[test]
584    fn test_univ_poly_signature_check_ok() {
585        let mut sig = UnivPolySignature::new(vec![Name::str("u")]);
586        sig.add_constraint(UnivConstraint::Le(
587            Level::param(Name::str("u")),
588            Level::succ(Level::param(Name::str("u"))),
589        ));
590        let args = vec![Level::zero()];
591        let inst = sig.instantiate(&args).expect("inst should be present");
592        assert!(sig.check_instantiation(&inst).is_ok());
593    }
594    #[test]
595    fn test_univ_constraint_display() {
596        let c = UnivConstraint::Lt(Level::zero(), Level::succ(Level::zero()));
597        let s = format!("{}", c);
598        assert!(s.contains('<'));
599    }
600    #[test]
601    fn test_level_comparison_table() {
602        let levels = vec![
603            Level::zero(),
604            Level::succ(Level::zero()),
605            Level::succ(Level::succ(Level::zero())),
606        ];
607        let table = LevelComparisonTable::new(levels);
608        assert_eq!(table.len(), 3);
609        assert_eq!(table.geq(1, 0), Some(true));
610        assert_eq!(table.geq(0, 1), Some(false));
611    }
612    #[test]
613    fn test_level_comparison_table_max() {
614        let levels = vec![Level::zero(), Level::succ(Level::zero())];
615        let table = LevelComparisonTable::new(levels);
616        let max = table.max_idx();
617        assert_eq!(max, Some(1));
618    }
619    #[test]
620    fn test_same_level_shape_max() {
621        let l1 = Level::max(Level::param(Name::str("u")), Level::param(Name::str("v")));
622        let l2 = Level::max(Level::param(Name::str("a")), Level::param(Name::str("b")));
623        assert!(same_level_shape(&l1, &l2));
624    }
625    #[test]
626    fn test_count_succ_depth() {
627        assert_eq!(count_succ_depth(&Level::zero()), 0);
628        assert_eq!(
629            count_succ_depth(&Level::succ(Level::succ(Level::zero()))),
630            2
631        );
632    }
633    #[test]
634    fn test_add_succ_n() {
635        let result = add_succ_n(Level::zero(), 4);
636        assert_eq!(level_to_nat(&result), Some(4));
637    }
638    #[test]
639    fn test_eval_closed_level_param() {
640        let l = Level::param(Name::str("u"));
641        assert!(eval_closed_level(&l).is_none());
642    }
643    #[test]
644    fn test_is_max_level() {
645        let l = Level::max(Level::zero(), Level::zero());
646        assert!(is_max_level(&l));
647        assert!(!is_imax_level(&l));
648    }
649    #[test]
650    fn test_is_imax_level() {
651        let l = Level::imax(Level::zero(), Level::zero());
652        assert!(is_imax_level(&l));
653        assert!(!is_max_level(&l));
654    }
655    #[test]
656    fn test_level_max_many_empty() {
657        let result = level_max_many(&[]);
658        assert_eq!(result, Level::zero());
659    }
660    #[test]
661    fn test_level_max_many_one() {
662        let l = Level::succ(Level::zero());
663        let result = level_max_many(std::slice::from_ref(&l));
664        assert!(crate::level::is_equivalent(&result, &l));
665    }
666    #[test]
667    fn test_univ_instantiation_len() {
668        let mut inst = UniverseInstantiation::new();
669        assert_eq!(inst.len(), 0);
670        inst.add(Name::str("u"), Level::zero());
671        assert_eq!(inst.len(), 1);
672    }
673}
674#[cfg(test)]
675mod tests_padding_infra {
676    use super::*;
677    #[test]
678    fn test_stat_summary() {
679        let mut ss = StatSummary::new();
680        ss.record(10.0);
681        ss.record(20.0);
682        ss.record(30.0);
683        assert_eq!(ss.count(), 3);
684        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
685        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
686        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
687    }
688    #[test]
689    fn test_transform_stat() {
690        let mut ts = TransformStat::new();
691        ts.record_before(100.0);
692        ts.record_after(80.0);
693        let ratio = ts.mean_ratio().expect("ratio should be present");
694        assert!((ratio - 0.8).abs() < 1e-9);
695    }
696    #[test]
697    fn test_small_map() {
698        let mut m: SmallMap<u32, &str> = SmallMap::new();
699        m.insert(3, "three");
700        m.insert(1, "one");
701        m.insert(2, "two");
702        assert_eq!(m.get(&2), Some(&"two"));
703        assert_eq!(m.len(), 3);
704        let keys = m.keys();
705        assert_eq!(*keys[0], 1);
706        assert_eq!(*keys[2], 3);
707    }
708    #[test]
709    fn test_label_set() {
710        let mut ls = LabelSet::new();
711        ls.add("foo");
712        ls.add("bar");
713        ls.add("foo");
714        assert_eq!(ls.count(), 2);
715        assert!(ls.has("bar"));
716        assert!(!ls.has("baz"));
717    }
718    #[test]
719    fn test_config_node() {
720        let mut root = ConfigNode::section("root");
721        let child = ConfigNode::leaf("key", "value");
722        root.add_child(child);
723        assert_eq!(root.num_children(), 1);
724    }
725    #[test]
726    fn test_versioned_record() {
727        let mut vr = VersionedRecord::new(0u32);
728        vr.update(1);
729        vr.update(2);
730        assert_eq!(*vr.current(), 2);
731        assert_eq!(vr.version(), 2);
732        assert!(vr.has_history());
733        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
734    }
735    #[test]
736    fn test_simple_dag() {
737        let mut dag = SimpleDag::new(4);
738        dag.add_edge(0, 1);
739        dag.add_edge(1, 2);
740        dag.add_edge(2, 3);
741        assert!(dag.can_reach(0, 3));
742        assert!(!dag.can_reach(3, 0));
743        let order = dag.topological_sort().expect("order should be present");
744        assert_eq!(order, vec![0, 1, 2, 3]);
745    }
746    #[test]
747    fn test_focus_stack() {
748        let mut fs: FocusStack<&str> = FocusStack::new();
749        fs.focus("a");
750        fs.focus("b");
751        assert_eq!(fs.current(), Some(&"b"));
752        assert_eq!(fs.depth(), 2);
753        fs.blur();
754        assert_eq!(fs.current(), Some(&"a"));
755    }
756}
757#[cfg(test)]
758mod tests_extra_iterators {
759    use super::*;
760    #[test]
761    fn test_window_iterator() {
762        let data = vec![1u32, 2, 3, 4, 5];
763        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
764        assert_eq!(windows.len(), 3);
765        assert_eq!(windows[0], &[1, 2, 3]);
766        assert_eq!(windows[2], &[3, 4, 5]);
767    }
768    #[test]
769    fn test_non_empty_vec() {
770        let mut nev = NonEmptyVec::singleton(10u32);
771        nev.push(20);
772        nev.push(30);
773        assert_eq!(nev.len(), 3);
774        assert_eq!(*nev.first(), 10);
775        assert_eq!(*nev.last(), 30);
776    }
777}
778#[cfg(test)]
779mod tests_padding2 {
780    use super::*;
781    #[test]
782    fn test_sliding_sum() {
783        let mut ss = SlidingSum::new(3);
784        ss.push(1.0);
785        ss.push(2.0);
786        ss.push(3.0);
787        assert!((ss.sum() - 6.0).abs() < 1e-9);
788        ss.push(4.0);
789        assert!((ss.sum() - 9.0).abs() < 1e-9);
790        assert_eq!(ss.count(), 3);
791    }
792    #[test]
793    fn test_path_buf() {
794        let mut pb = PathBuf::new();
795        pb.push("src");
796        pb.push("main");
797        assert_eq!(pb.as_str(), "src/main");
798        assert_eq!(pb.depth(), 2);
799        pb.pop();
800        assert_eq!(pb.as_str(), "src");
801    }
802    #[test]
803    fn test_string_pool() {
804        let mut pool = StringPool::new();
805        let s = pool.take();
806        assert!(s.is_empty());
807        pool.give("hello".to_string());
808        let s2 = pool.take();
809        assert!(s2.is_empty());
810        assert_eq!(pool.free_count(), 0);
811    }
812    #[test]
813    fn test_transitive_closure() {
814        let mut tc = TransitiveClosure::new(4);
815        tc.add_edge(0, 1);
816        tc.add_edge(1, 2);
817        tc.add_edge(2, 3);
818        assert!(tc.can_reach(0, 3));
819        assert!(!tc.can_reach(3, 0));
820        let r = tc.reachable_from(0);
821        assert_eq!(r.len(), 4);
822    }
823    #[test]
824    fn test_token_bucket() {
825        let mut tb = TokenBucket::new(100, 10);
826        assert_eq!(tb.available(), 100);
827        assert!(tb.try_consume(50));
828        assert_eq!(tb.available(), 50);
829        assert!(!tb.try_consume(60));
830        assert_eq!(tb.capacity(), 100);
831    }
832    #[test]
833    fn test_rewrite_rule_set() {
834        let mut rrs = RewriteRuleSet::new();
835        rrs.add(RewriteRule::unconditional(
836            "beta",
837            "App(Lam(x, b), v)",
838            "b[x:=v]",
839        ));
840        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
841        assert_eq!(rrs.len(), 2);
842        assert_eq!(rrs.unconditional_rules().len(), 1);
843        assert_eq!(rrs.conditional_rules().len(), 1);
844        assert!(rrs.get("beta").is_some());
845        let disp = rrs
846            .get("beta")
847            .expect("element at \'beta\' should exist")
848            .display();
849        assert!(disp.contains("→"));
850    }
851}
852#[cfg(test)]
853mod tests_padding3 {
854    use super::*;
855    #[test]
856    fn test_decision_node() {
857        let tree = DecisionNode::Branch {
858            key: "x".into(),
859            val: "1".into(),
860            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
861            no_branch: Box::new(DecisionNode::Leaf("no".into())),
862        };
863        let mut ctx = std::collections::HashMap::new();
864        ctx.insert("x".into(), "1".into());
865        assert_eq!(tree.evaluate(&ctx), "yes");
866        ctx.insert("x".into(), "2".into());
867        assert_eq!(tree.evaluate(&ctx), "no");
868        assert_eq!(tree.depth(), 1);
869    }
870    #[test]
871    fn test_flat_substitution() {
872        let mut sub = FlatSubstitution::new();
873        sub.add("foo", "bar");
874        sub.add("baz", "qux");
875        assert_eq!(sub.apply("foo and baz"), "bar and qux");
876        assert_eq!(sub.len(), 2);
877    }
878    #[test]
879    fn test_stopwatch() {
880        let mut sw = Stopwatch::start();
881        sw.split();
882        sw.split();
883        assert_eq!(sw.num_splits(), 2);
884        assert!(sw.elapsed_ms() >= 0.0);
885        for &s in sw.splits() {
886            assert!(s >= 0.0);
887        }
888    }
889    #[test]
890    fn test_either2() {
891        let e: Either2<i32, &str> = Either2::First(42);
892        assert!(e.is_first());
893        let mapped = e.map_first(|x| x * 2);
894        assert_eq!(mapped.first(), Some(84));
895        let e2: Either2<i32, &str> = Either2::Second("hello");
896        assert!(e2.is_second());
897        assert_eq!(e2.second(), Some("hello"));
898    }
899    #[test]
900    fn test_write_once() {
901        let wo: WriteOnce<u32> = WriteOnce::new();
902        assert!(!wo.is_written());
903        assert!(wo.write(42));
904        assert!(!wo.write(99));
905        assert_eq!(wo.read(), Some(42));
906    }
907    #[test]
908    fn test_sparse_vec() {
909        let mut sv: SparseVec<i32> = SparseVec::new(100);
910        sv.set(5, 10);
911        sv.set(50, 20);
912        assert_eq!(*sv.get(5), 10);
913        assert_eq!(*sv.get(50), 20);
914        assert_eq!(*sv.get(0), 0);
915        assert_eq!(sv.nnz(), 2);
916        sv.set(5, 0);
917        assert_eq!(sv.nnz(), 1);
918    }
919    #[test]
920    fn test_stack_calc() {
921        let mut calc = StackCalc::new();
922        calc.push(3);
923        calc.push(4);
924        calc.add();
925        assert_eq!(calc.peek(), Some(7));
926        calc.push(2);
927        calc.mul();
928        assert_eq!(calc.peek(), Some(14));
929    }
930}
oxilean_kernel/universe/functions.rs

oxilean_kernel/universe/
functions.rs
