oxilean_kernel/level/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::Name;
6
7use super::types::{
8    ConfigNode, ConstraintSet, DecisionNode, Either2, Fixture, FlatSubstitution, FocusStack,
9    LabelSet, Level, LevelConstraint, LevelMVarId, MinHeap, NonEmptyVec, PathBuf, PrefixCounter,
10    RewriteRule, RewriteRuleSet, SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc,
11    StatSummary, Stopwatch, StringPool, TokenBucket, TransformStat, TransitiveClosure,
12    VersionedRecord, WindowIterator, WriteOnce,
13};
14
15/// Decompose a level into `(base, offset)` where level = succ^offset(base).
16///
17/// Strips all Succ wrappers. E.g., `succ(succ(param u))` -> `(param u, 2)`.
18pub fn to_offset(l: &Level) -> (&Level, u32) {
19    match l {
20        Level::Succ(inner) => {
21            let (base, k) = to_offset(inner);
22            (base, k + 1)
23        }
24        _ => (l, 0),
25    }
26}
27/// Reconstruct a level from `(base, offset)` as `succ^offset(base)`.
28pub(super) fn from_offset(base: Level, offset: u32) -> Level {
29    let mut result = base;
30    for _ in 0..offset {
31        result = Level::succ(result);
32    }
33    result
34}
35/// Collect all arguments of a nested max expression into a flat list.
36pub(super) fn push_max_args(l: &Level, args: &mut Vec<Level>) {
37    match l {
38        Level::Max(l1, l2) => {
39            push_max_args(l1, args);
40            push_max_args(l2, args);
41        }
42        _ => args.push(l.clone()),
43    }
44}
45/// Total order on levels for normalization.
46///
47/// This ordering ensures that normalization produces a canonical form.
48pub(super) fn is_norm_lt(l1: &Level, l2: &Level) -> bool {
49    let (b1, k1) = to_offset(l1);
50    let (b2, k2) = to_offset(l2);
51    fn kind_ord(l: &Level) -> u8 {
52        match l {
53            Level::Zero => 0,
54            Level::Param(_) => 1,
55            Level::MVar(_) => 2,
56            Level::Max(_, _) => 3,
57            Level::IMax(_, _) => 4,
58            Level::Succ(_) => 5,
59        }
60    }
61    let k1_ord = kind_ord(b1);
62    let k2_ord = kind_ord(b2);
63    if k1_ord != k2_ord {
64        return k1_ord < k2_ord;
65    }
66    match (b1, b2) {
67        (Level::Param(n1), Level::Param(n2)) => {
68            let s1 = n1.to_string();
69            let s2 = n2.to_string();
70            if s1 != s2 {
71                return s1 < s2;
72            }
73        }
74        (Level::MVar(m1), Level::MVar(m2)) => {
75            if m1.0 != m2.0 {
76                return m1.0 < m2.0;
77            }
78        }
79        (Level::Max(a1, a2), Level::Max(b1_inner, b2_inner))
80        | (Level::IMax(a1, a2), Level::IMax(b1_inner, b2_inner)) => {
81            if a1 != b1_inner {
82                return is_norm_lt(a1, b1_inner);
83            }
84            if a2 != b2_inner {
85                return is_norm_lt(a2, b2_inner);
86            }
87        }
88        _ => {}
89    }
90    k1 < k2
91}
92/// Normalize a universe level to canonical form.
93///
94/// Follows LEAN 4's normalization algorithm:
95/// 1. Flatten nested max expressions
96/// 2. Normalize each argument recursively
97/// 3. Sort arguments
98/// 4. Merge duplicates (keep larger offsets)
99/// 5. Remove subsumed explicit levels
100pub fn normalize(l: &Level) -> Level {
101    let (base, k) = to_offset(l);
102    match base {
103        Level::Zero | Level::Param(_) | Level::MVar(_) => l.clone(),
104        Level::Succ(_) => l.clone(),
105        Level::IMax(l1, l2) => {
106            let l1_norm = normalize(l1);
107            let l2_norm = normalize(l2);
108            if l2_norm.is_zero() {
109                return from_offset(Level::Zero, k);
110            }
111            if l2_norm.is_not_zero() {
112                return from_offset(normalize(&Level::max(l1_norm, l2_norm)), k);
113            }
114            if l1_norm.is_zero() {
115                return from_offset(l2_norm, k);
116            }
117            from_offset(Level::imax(l1_norm, l2_norm), k)
118        }
119        Level::Max(_, _) => {
120            let mut args = Vec::new();
121            push_max_args(base, &mut args);
122            let mut normed: Vec<Level> = args
123                .into_iter()
124                .map(|a| normalize(&from_offset(a, k)))
125                .collect();
126            normed.sort_by(|a, b| {
127                if is_norm_lt(a, b) {
128                    std::cmp::Ordering::Less
129                } else if a == b {
130                    std::cmp::Ordering::Equal
131                } else {
132                    std::cmp::Ordering::Greater
133                }
134            });
135            let mut merged: Vec<Level> = Vec::new();
136            for arg in normed {
137                let dominated = if let Some(last) = merged.last() {
138                    let (base_last, k_last) = to_offset(last);
139                    let (base_arg, k_arg) = to_offset(&arg);
140                    if base_last == base_arg {
141                        if k_arg > k_last {
142                            merged.pop();
143                            false
144                        } else {
145                            true
146                        }
147                    } else {
148                        false
149                    }
150                } else {
151                    false
152                };
153                if !dominated {
154                    merged.push(arg);
155                }
156            }
157            if merged.len() > 1 {
158                let has_nonzero = merged.iter().any(|a| a.is_not_zero());
159                if has_nonzero {
160                    merged.retain(|a| !a.is_zero());
161                }
162            }
163            if merged.is_empty() {
164                Level::Zero
165            } else if merged.len() == 1 {
166                merged
167                    .into_iter()
168                    .next()
169                    .expect("merged set must be non-empty")
170            } else {
171                let mut result = merged.pop().expect("merged set must be non-empty");
172                while let Some(arg) = merged.pop() {
173                    result = Level::max(arg, result);
174                }
175                result
176            }
177        }
178    }
179}
180/// Check if two levels are semantically equivalent.
181///
182/// First tries structural equality, then falls back to normalization.
183pub fn is_equivalent(l1: &Level, l2: &Level) -> bool {
184    l1 == l2 || normalize(l1) == normalize(l2)
185}
186/// Check if `l1 >= l2` (level ordering).
187///
188/// Returns true if level `l1` is guaranteed to be >= `l2`
189/// for all possible assignments to parameters and metavariables.
190pub fn is_geq(l1: &Level, l2: &Level) -> bool {
191    is_geq_core(&normalize(l1), &normalize(l2))
192}
193pub(super) fn is_geq_core(l1: &Level, l2: &Level) -> bool {
194    if l1 == l2 {
195        return true;
196    }
197    if l2.is_zero() {
198        return true;
199    }
200    if let Level::Max(a, b) = l1 {
201        if is_geq_core(a, l2) || is_geq_core(b, l2) {
202            return true;
203        }
204    }
205    if let Level::Max(b, c) = l2 {
206        if is_geq_core(l1, b) && is_geq_core(l1, c) {
207            return true;
208        }
209    }
210    if let Level::IMax(b, c) = l2 {
211        if is_geq_core(l1, b) && is_geq_core(l1, c) {
212            return true;
213        }
214    }
215    if let Level::IMax(_, b) = l1 {
216        if is_geq_core(b, l2) {
217            return true;
218        }
219    }
220    let (b1, k1) = to_offset(l1);
221    let (b2, k2) = to_offset(l2);
222    if b1 == b2 {
223        return k1 >= k2;
224    }
225    false
226}
227/// Check if `l1 <= l2` (level ordering).
228pub fn is_leq(l1: &Level, l2: &Level) -> bool {
229    is_geq(l2, l1)
230}
231/// Instantiate level parameters using a substitution.
232///
233/// Replaces `Param(name)` with the corresponding level if `name` is found
234/// in `param_names`.
235pub fn instantiate_level(level: &Level, param_names: &[Name], levels: &[Level]) -> Level {
236    if param_names.is_empty() {
237        return level.clone();
238    }
239    match level {
240        Level::Param(name) => {
241            for (i, pn) in param_names.iter().enumerate() {
242                if pn == name {
243                    if let Some(l) = levels.get(i) {
244                        return l.clone();
245                    }
246                }
247            }
248            level.clone()
249        }
250        Level::Succ(l) => Level::succ(instantiate_level(l, param_names, levels)),
251        Level::Max(l1, l2) => Level::max(
252            instantiate_level(l1, param_names, levels),
253            instantiate_level(l2, param_names, levels),
254        ),
255        Level::IMax(l1, l2) => Level::imax(
256            instantiate_level(l1, param_names, levels),
257            instantiate_level(l2, param_names, levels),
258        ),
259        Level::Zero | Level::MVar(_) => level.clone(),
260    }
261}
262/// Collect all parameter names used in a level.
263pub fn collect_level_params(l: &Level, params: &mut Vec<Name>) {
264    match l {
265        Level::Param(name) => {
266            if !params.contains(name) {
267                params.push(name.clone());
268            }
269        }
270        Level::Succ(l) => collect_level_params(l, params),
271        Level::Max(l1, l2) | Level::IMax(l1, l2) => {
272            collect_level_params(l1, params);
273            collect_level_params(l2, params);
274        }
275        Level::Zero | Level::MVar(_) => {}
276    }
277}
278/// Collect all metavariable IDs used in a level.
279pub fn collect_level_mvars(l: &Level, mvars: &mut Vec<LevelMVarId>) {
280    match l {
281        Level::MVar(id) => {
282            if !mvars.contains(id) {
283                mvars.push(*id);
284            }
285        }
286        Level::Succ(l) => collect_level_mvars(l, mvars),
287        Level::Max(l1, l2) | Level::IMax(l1, l2) => {
288            collect_level_mvars(l1, mvars);
289            collect_level_mvars(l2, mvars);
290        }
291        Level::Zero | Level::Param(_) => {}
292    }
293}
294/// Replace level metavariables using a substitution function.
295pub fn instantiate_level_mvars(
296    level: &Level,
297    subst: &dyn Fn(LevelMVarId) -> Option<Level>,
298) -> Level {
299    match level {
300        Level::MVar(id) => {
301            if let Some(l) = subst(*id) {
302                instantiate_level_mvars(&l, subst)
303            } else {
304                level.clone()
305            }
306        }
307        Level::Succ(l) => Level::succ(instantiate_level_mvars(l, subst)),
308        Level::Max(l1, l2) => Level::max(
309            instantiate_level_mvars(l1, subst),
310            instantiate_level_mvars(l2, subst),
311        ),
312        Level::IMax(l1, l2) => Level::imax(
313            instantiate_level_mvars(l1, subst),
314            instantiate_level_mvars(l2, subst),
315        ),
316        Level::Zero | Level::Param(_) => level.clone(),
317    }
318}
319#[cfg(test)]
320mod tests {
321    use super::*;
322    #[test]
323    fn test_level_construction() {
324        let l0 = Level::zero();
325        let l1 = Level::succ(Level::zero());
326        let l_param = Level::param(Name::str("u"));
327        let l_max = Level::max(l1.clone(), l_param.clone());
328        assert!(l0.is_zero());
329        assert!(l_param.is_param());
330        assert!(!l_max.is_zero());
331    }
332    #[test]
333    fn test_level_display() {
334        let l0 = Level::zero();
335        let l1 = Level::succ(Level::zero());
336        let l_max = Level::max(l0.clone(), l1.clone());
337        let l_imax = Level::imax(l0, l1);
338        assert_eq!(l_max.to_string(), "max(0, 1)");
339        assert_eq!(l_imax.to_string(), "imax(0, 1)");
340    }
341    #[test]
342    fn test_level_mvar() {
343        let mv = Level::mvar(LevelMVarId(42));
344        assert!(mv.is_mvar());
345        assert!(mv.has_mvar());
346        assert!(!mv.has_param());
347        assert_eq!(mv.to_string(), "?u_42");
348    }
349    #[test]
350    fn test_is_not_zero() {
351        assert!(!Level::zero().is_not_zero());
352        assert!(Level::succ(Level::zero()).is_not_zero());
353        assert!(Level::succ(Level::param(Name::str("u"))).is_not_zero());
354        assert!(!Level::param(Name::str("u")).is_not_zero());
355        let m = Level::max(Level::zero(), Level::succ(Level::param(Name::str("u"))));
356        assert!(m.is_not_zero());
357    }
358    #[test]
359    fn test_to_offset() {
360        let l = Level::succ(Level::succ(Level::param(Name::str("u"))));
361        let (base, k) = to_offset(&l);
362        assert_eq!(*base, Level::param(Name::str("u")));
363        assert_eq!(k, 2);
364        let zero = Level::zero();
365        let (base0, k0) = to_offset(&zero);
366        assert_eq!(*base0, Level::zero());
367        assert_eq!(k0, 0);
368    }
369    #[test]
370    fn test_from_nat_to_nat() {
371        for n in 0..5 {
372            let l = Level::from_nat(n);
373            assert_eq!(l.to_nat(), Some(n));
374        }
375        assert_eq!(Level::param(Name::str("u")).to_nat(), None);
376    }
377    #[test]
378    fn test_normalize_zero() {
379        assert_eq!(normalize(&Level::zero()), Level::zero());
380    }
381    #[test]
382    fn test_normalize_succ() {
383        let l = Level::succ(Level::succ(Level::zero()));
384        assert_eq!(normalize(&l), l);
385    }
386    #[test]
387    fn test_normalize_max_same() {
388        let u = Level::param(Name::str("u"));
389        let m = Level::max(u.clone(), u.clone());
390        assert_eq!(normalize(&m), u);
391    }
392    #[test]
393    fn test_normalize_max_zero() {
394        let u = Level::param(Name::str("u"));
395        let m = Level::max(u.clone(), Level::zero());
396        let n = normalize(&m);
397        assert!(is_equivalent(&n, &u) || is_equivalent(&n, &m));
398    }
399    #[test]
400    fn test_normalize_max_ordering() {
401        let u = Level::param(Name::str("u"));
402        let v = Level::param(Name::str("v"));
403        let m1 = Level::max(u.clone(), v.clone());
404        let m2 = Level::max(v, u);
405        assert_eq!(normalize(&m1), normalize(&m2));
406    }
407    #[test]
408    fn test_normalize_imax_zero() {
409        let u = Level::param(Name::str("u"));
410        let im = Level::imax(u, Level::zero());
411        assert_eq!(normalize(&im), Level::zero());
412    }
413    #[test]
414    fn test_normalize_imax_succ() {
415        let u = Level::param(Name::str("u"));
416        let v = Level::param(Name::str("v"));
417        let im = Level::imax(u.clone(), Level::succ(v.clone()));
418        let expected = normalize(&Level::max(u, Level::succ(v)));
419        assert_eq!(normalize(&im), expected);
420    }
421    #[test]
422    fn test_is_equivalent() {
423        let u = Level::param(Name::str("u"));
424        let v = Level::param(Name::str("v"));
425        assert!(is_equivalent(
426            &Level::max(u.clone(), v.clone()),
427            &Level::max(v, u),
428        ));
429        assert!(!is_equivalent(
430            &Level::param(Name::str("u")),
431            &Level::param(Name::str("v")),
432        ));
433        assert!(is_equivalent(
434            &Level::succ(Level::zero()),
435            &Level::succ(Level::zero()),
436        ));
437    }
438    #[test]
439    fn test_is_geq() {
440        let u = Level::param(Name::str("u"));
441        let l0 = Level::zero();
442        let l1 = Level::succ(Level::zero());
443        let l2 = Level::succ(Level::succ(Level::zero()));
444        assert!(is_geq(&u, &l0));
445        assert!(is_geq(&l2, &l1));
446        assert!(!is_geq(&l1, &l2));
447        assert!(is_geq(&Level::succ(u.clone()), &u));
448        let v = Level::param(Name::str("v"));
449        assert!(is_geq(&Level::max(u.clone(), v.clone()), &u));
450        assert!(is_geq(&Level::max(u.clone(), v.clone()), &v));
451    }
452    #[test]
453    fn test_instantiate_level() {
454        let l = Level::max(
455            Level::param(Name::str("u")),
456            Level::succ(Level::param(Name::str("v"))),
457        );
458        let result = instantiate_level(
459            &l,
460            &[Name::str("u"), Name::str("v")],
461            &[Level::zero(), Level::succ(Level::zero())],
462        );
463        let expected = Level::max(Level::zero(), Level::succ(Level::succ(Level::zero())));
464        assert_eq!(result, expected);
465    }
466    #[test]
467    fn test_collect_level_params() {
468        let l = Level::max(
469            Level::param(Name::str("u")),
470            Level::succ(Level::param(Name::str("v"))),
471        );
472        let mut params = Vec::new();
473        collect_level_params(&l, &mut params);
474        assert_eq!(params.len(), 2);
475        assert!(params.contains(&Name::str("u")));
476        assert!(params.contains(&Name::str("v")));
477    }
478    #[test]
479    fn test_instantiate_level_mvars() {
480        let l = Level::max(
481            Level::mvar(LevelMVarId(0)),
482            Level::succ(Level::mvar(LevelMVarId(1))),
483        );
484        let result = instantiate_level_mvars(&l, &|id| {
485            if id.0 == 0 {
486                Some(Level::zero())
487            } else if id.0 == 1 {
488                Some(Level::param(Name::str("u")))
489            } else {
490                None
491            }
492        });
493        let expected = Level::max(Level::zero(), Level::succ(Level::param(Name::str("u"))));
494        assert_eq!(result, expected);
495    }
496    #[test]
497    fn test_depth() {
498        assert_eq!(Level::zero().depth(), 0);
499        assert_eq!(Level::succ(Level::zero()).depth(), 1);
500        assert_eq!(
501            Level::max(Level::param(Name::str("u")), Level::succ(Level::zero())).depth(),
502            2
503        );
504    }
505}
506/// Compute the minimum of two levels: min(l1, l2).
507///
508/// Defined as `imax(l1, succ(l2))` is NOT min; instead use:
509/// min(l1, l2) = l1 if l1 <= l2, else l2. This is approximate
510/// (returns a conservative lower bound for polymorphic levels).
511#[allow(dead_code)]
512pub fn level_min(l1: &Level, l2: &Level) -> Level {
513    if l1.is_zero() || l2.is_zero() {
514        return Level::Zero;
515    }
516    if is_leq(l1, l2) {
517        return l1.clone();
518    }
519    if is_leq(l2, l1) {
520        return l2.clone();
521    }
522    Level::Zero
523}
524/// Create `max(max(l1, l2), l3)` and normalize.
525#[allow(dead_code)]
526pub fn level_max3(l1: Level, l2: Level, l3: Level) -> Level {
527    normalize(&Level::max(Level::max(l1, l2), l3))
528}
529/// Bump a level by `n` successor applications.
530///
531/// `level_add(l, n)` = `succ^n(l)`.
532#[allow(dead_code)]
533pub fn level_add(l: Level, n: u32) -> Level {
534    let mut result = l;
535    for _ in 0..n {
536        result = Level::succ(result);
537    }
538    result
539}
540/// The universe level for `Type n` (= succ^(n+1)(0)).
541#[allow(dead_code)]
542pub fn type_level(n: u32) -> Level {
543    Level::from_nat(n + 1)
544}
545/// Check if `l` is definitely a successor (non-zero) level.
546/// Returns true for `succ(anything)`.
547#[allow(dead_code)]
548pub fn is_definitely_succ(l: &Level) -> bool {
549    matches!(l, Level::Succ(_))
550}
551/// Collect all levels appearing in a `Vec<Level>`, deduplicating by structural equality.
552#[allow(dead_code)]
553pub fn dedup_levels(levels: Vec<Level>) -> Vec<Level> {
554    let mut seen: Vec<Level> = Vec::new();
555    for l in levels {
556        if !seen.contains(&l) {
557            seen.push(l);
558        }
559    }
560    seen
561}
562#[cfg(test)]
563mod extra_level_tests {
564    use super::*;
565    #[test]
566    fn test_level_min_zeros() {
567        assert_eq!(
568            level_min(&Level::zero(), &Level::succ(Level::zero())),
569            Level::zero()
570        );
571    }
572    #[test]
573    fn test_level_min_equal() {
574        let l1 = Level::succ(Level::zero());
575        let l2 = Level::succ(Level::zero());
576        assert_eq!(level_min(&l1, &l2), l1);
577    }
578    #[test]
579    fn test_level_max3() {
580        let l0 = Level::zero();
581        let l1 = Level::succ(Level::zero());
582        let l2 = Level::succ(Level::succ(Level::zero()));
583        let result = level_max3(l0, l1, l2.clone());
584        assert!(is_equivalent(&result, &l2));
585    }
586    #[test]
587    fn test_level_add_zero_times() {
588        let l = Level::param(Name::str("u"));
589        assert_eq!(level_add(l.clone(), 0), l);
590    }
591    #[test]
592    fn test_level_add_two_times() {
593        let l = Level::zero();
594        let result = level_add(l, 2);
595        assert_eq!(result.to_nat(), Some(2));
596    }
597    #[test]
598    fn test_type_level_zero() {
599        assert_eq!(type_level(0), Level::succ(Level::zero()));
600    }
601    #[test]
602    fn test_type_level_two() {
603        assert_eq!(type_level(2).to_nat(), Some(3));
604    }
605    #[test]
606    fn test_is_definitely_succ_true() {
607        assert!(is_definitely_succ(&Level::succ(Level::zero())));
608    }
609    #[test]
610    fn test_is_definitely_succ_false() {
611        assert!(!is_definitely_succ(&Level::zero()));
612        assert!(!is_definitely_succ(&Level::param(Name::str("u"))));
613    }
614    #[test]
615    fn test_dedup_levels() {
616        let l0 = Level::zero();
617        let l1 = Level::succ(Level::zero());
618        let levels = vec![l0.clone(), l0.clone(), l1.clone(), l1.clone()];
619        let deduped = dedup_levels(levels);
620        assert_eq!(deduped.len(), 2);
621    }
622    #[test]
623    fn test_collect_level_mvars_multiple() {
624        let l = Level::max(Level::mvar(LevelMVarId(0)), Level::mvar(LevelMVarId(1)));
625        let mut mvars = Vec::new();
626        collect_level_mvars(&l, &mut mvars);
627        assert_eq!(mvars.len(), 2);
628    }
629    #[test]
630    fn test_level_is_leq() {
631        let l0 = Level::zero();
632        let l1 = Level::succ(Level::zero());
633        assert!(is_leq(&l0, &l1));
634        assert!(!is_leq(&l1, &l0));
635        assert!(is_leq(&l0, &l0));
636    }
637}
638/// Flatten a level to a list of `(base, offset)` pairs representing max arguments.
639///
640/// E.g., `max(max(u, v+1), w+2)` → `[(u,0), (v,1), (w,2)]`.
641#[allow(dead_code)]
642pub fn flatten_max(l: &Level) -> Vec<(Level, u32)> {
643    let norm = normalize(l);
644    let mut result = Vec::new();
645    push_flat(&norm, &mut result);
646    result
647}
648pub(super) fn push_flat(l: &Level, acc: &mut Vec<(Level, u32)>) {
649    match l {
650        Level::Max(l1, l2) => {
651            push_flat(l1, acc);
652            push_flat(l2, acc);
653        }
654        _ => {
655            let (base, k) = to_offset(l);
656            acc.push((base.clone(), k));
657        }
658    }
659}
660/// Check if the level is a concrete numeral (succ^n(zero)).
661#[allow(dead_code)]
662pub fn is_numeral(l: &Level) -> bool {
663    l.to_nat().is_some()
664}
665/// Check if a level expression is ground (no parameters, no mvars).
666#[allow(dead_code)]
667pub fn is_ground(l: &Level) -> bool {
668    !l.has_param() && !l.has_mvar()
669}
670/// Evaluate a ground (no params, no mvars) level to a concrete `u32`.
671///
672/// Returns `None` if the level has parameters or metavariables.
673#[allow(dead_code)]
674pub fn eval_ground_level(l: &Level) -> Option<u32> {
675    if !is_ground(l) {
676        return None;
677    }
678    let norm = normalize(l);
679    norm.to_nat()
680}
681/// Create a level that is the `max` of a slice of levels.
682///
683/// Returns `Level::Zero` for an empty slice.
684#[allow(dead_code)]
685pub fn max_of_slice(levels: &[Level]) -> Level {
686    let mut iter = levels.iter();
687    match iter.next() {
688        None => Level::Zero,
689        Some(first) => iter.fold(first.clone(), |acc, l| Level::max(acc, l.clone())),
690    }
691}
692/// Create a level that is the `imax` of a slice of levels, left-folded.
693///
694/// Useful for computing the sort level of Pi types.
695#[allow(dead_code)]
696pub fn imax_fold(levels: &[Level]) -> Level {
697    let mut iter = levels.iter();
698    match iter.next() {
699        None => Level::Zero,
700        Some(first) => iter.fold(first.clone(), |acc, l| Level::imax(acc, l.clone())),
701    }
702}
703/// Level of `Prop` (= 0).
704#[allow(dead_code)]
705pub const PROP_LEVEL: Level = Level::Zero;
706/// Level of `Type 0` (= 1).
707#[allow(dead_code)]
708pub fn type0_level() -> Level {
709    Level::succ(Level::Zero)
710}
711/// Level of `Type 1` (= 2).
712#[allow(dead_code)]
713pub fn type1_level() -> Level {
714    Level::succ(Level::succ(Level::Zero))
715}
716#[cfg(test)]
717mod extra2_level_tests {
718    use super::*;
719    #[test]
720    fn test_level_constraint_leq_satisfied() {
721        let l0 = Level::zero();
722        let l1 = Level::succ(Level::zero());
723        let c = LevelConstraint::Leq(l0, l1);
724        assert!(c.is_satisfied());
725    }
726    #[test]
727    fn test_level_constraint_leq_violated() {
728        let l1 = Level::succ(Level::zero());
729        let l0 = Level::zero();
730        let c = LevelConstraint::Leq(l1, l0);
731        assert!(!c.is_satisfied());
732    }
733    #[test]
734    fn test_level_constraint_eq_satisfied() {
735        let l = Level::succ(Level::zero());
736        let c = LevelConstraint::Eq(l.clone(), l);
737        assert!(c.is_satisfied());
738    }
739    #[test]
740    fn test_constraint_set_all_satisfied() {
741        let mut cs = ConstraintSet::new();
742        cs.add_leq(Level::zero(), Level::succ(Level::zero()));
743        cs.add_eq(Level::zero(), Level::zero());
744        assert!(cs.all_satisfied());
745    }
746    #[test]
747    fn test_constraint_set_unsatisfied() {
748        let mut cs = ConstraintSet::new();
749        cs.add_leq(Level::succ(Level::zero()), Level::zero());
750        assert!(!cs.all_satisfied());
751        assert_eq!(cs.unsatisfied().len(), 1);
752    }
753    #[test]
754    fn test_flatten_max_single() {
755        let l = Level::param(Name::str("u"));
756        let flat = flatten_max(&l);
757        assert_eq!(flat.len(), 1);
758    }
759    #[test]
760    fn test_flatten_max_binary() {
761        let u = Level::param(Name::str("u"));
762        let v = Level::param(Name::str("v"));
763        let m = Level::max(u, v);
764        let flat = flatten_max(&m);
765        assert_eq!(flat.len(), 2);
766    }
767    #[test]
768    fn test_is_numeral_true() {
769        assert!(is_numeral(&Level::zero()));
770        assert!(is_numeral(&Level::succ(Level::zero())));
771        assert!(is_numeral(&Level::from_nat(5)));
772    }
773    #[test]
774    fn test_is_numeral_false() {
775        assert!(!is_numeral(&Level::param(Name::str("u"))));
776    }
777    #[test]
778    fn test_is_ground_zero() {
779        assert!(is_ground(&Level::zero()));
780    }
781    #[test]
782    fn test_is_ground_param() {
783        assert!(!is_ground(&Level::param(Name::str("u"))));
784    }
785    #[test]
786    fn test_eval_ground_level_numeral() {
787        let l = Level::from_nat(3);
788        assert_eq!(eval_ground_level(&l), Some(3));
789    }
790    #[test]
791    fn test_eval_ground_level_param() {
792        let l = Level::param(Name::str("u"));
793        assert_eq!(eval_ground_level(&l), None);
794    }
795    #[test]
796    fn test_max_of_slice_empty() {
797        let result = max_of_slice(&[]);
798        assert_eq!(result, Level::zero());
799    }
800    #[test]
801    fn test_max_of_slice_single() {
802        let l = Level::succ(Level::zero());
803        let result = max_of_slice(std::slice::from_ref(&l));
804        assert_eq!(result, l);
805    }
806    #[test]
807    fn test_max_of_slice_multiple() {
808        let l0 = Level::zero();
809        let l1 = Level::succ(Level::zero());
810        let l2 = Level::succ(Level::succ(Level::zero()));
811        let result = max_of_slice(&[l0, l1, l2.clone()]);
812        assert!(is_equivalent(&normalize(&result), &l2));
813    }
814    #[test]
815    fn test_imax_fold_empty() {
816        assert_eq!(imax_fold(&[]), Level::zero());
817    }
818    #[test]
819    fn test_type0_level() {
820        assert_eq!(type0_level().to_nat(), Some(1));
821    }
822    #[test]
823    fn test_type1_level() {
824        assert_eq!(type1_level().to_nat(), Some(2));
825    }
826    #[test]
827    fn test_constraint_set_len() {
828        let mut cs = ConstraintSet::new();
829        cs.add_leq(Level::zero(), Level::succ(Level::zero()));
830        assert_eq!(cs.len(), 1);
831        assert!(!cs.is_empty());
832    }
833}
834#[cfg(test)]
835mod tests_padding_infra {
836    use super::*;
837    #[test]
838    fn test_stat_summary() {
839        let mut ss = StatSummary::new();
840        ss.record(10.0);
841        ss.record(20.0);
842        ss.record(30.0);
843        assert_eq!(ss.count(), 3);
844        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
845        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
846        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
847    }
848    #[test]
849    fn test_transform_stat() {
850        let mut ts = TransformStat::new();
851        ts.record_before(100.0);
852        ts.record_after(80.0);
853        let ratio = ts.mean_ratio().expect("ratio should be present");
854        assert!((ratio - 0.8).abs() < 1e-9);
855    }
856    #[test]
857    fn test_small_map() {
858        let mut m: SmallMap<u32, &str> = SmallMap::new();
859        m.insert(3, "three");
860        m.insert(1, "one");
861        m.insert(2, "two");
862        assert_eq!(m.get(&2), Some(&"two"));
863        assert_eq!(m.len(), 3);
864        let keys = m.keys();
865        assert_eq!(*keys[0], 1);
866        assert_eq!(*keys[2], 3);
867    }
868    #[test]
869    fn test_label_set() {
870        let mut ls = LabelSet::new();
871        ls.add("foo");
872        ls.add("bar");
873        ls.add("foo");
874        assert_eq!(ls.count(), 2);
875        assert!(ls.has("bar"));
876        assert!(!ls.has("baz"));
877    }
878    #[test]
879    fn test_config_node() {
880        let mut root = ConfigNode::section("root");
881        let child = ConfigNode::leaf("key", "value");
882        root.add_child(child);
883        assert_eq!(root.num_children(), 1);
884    }
885    #[test]
886    fn test_versioned_record() {
887        let mut vr = VersionedRecord::new(0u32);
888        vr.update(1);
889        vr.update(2);
890        assert_eq!(*vr.current(), 2);
891        assert_eq!(vr.version(), 2);
892        assert!(vr.has_history());
893        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
894    }
895    #[test]
896    fn test_simple_dag() {
897        let mut dag = SimpleDag::new(4);
898        dag.add_edge(0, 1);
899        dag.add_edge(1, 2);
900        dag.add_edge(2, 3);
901        assert!(dag.can_reach(0, 3));
902        assert!(!dag.can_reach(3, 0));
903        let order = dag.topological_sort().expect("order should be present");
904        assert_eq!(order, vec![0, 1, 2, 3]);
905    }
906    #[test]
907    fn test_focus_stack() {
908        let mut fs: FocusStack<&str> = FocusStack::new();
909        fs.focus("a");
910        fs.focus("b");
911        assert_eq!(fs.current(), Some(&"b"));
912        assert_eq!(fs.depth(), 2);
913        fs.blur();
914        assert_eq!(fs.current(), Some(&"a"));
915    }
916}
917#[cfg(test)]
918mod tests_extra_iterators {
919    use super::*;
920    #[test]
921    fn test_window_iterator() {
922        let data = vec![1u32, 2, 3, 4, 5];
923        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
924        assert_eq!(windows.len(), 3);
925        assert_eq!(windows[0], &[1, 2, 3]);
926        assert_eq!(windows[2], &[3, 4, 5]);
927    }
928    #[test]
929    fn test_non_empty_vec() {
930        let mut nev = NonEmptyVec::singleton(10u32);
931        nev.push(20);
932        nev.push(30);
933        assert_eq!(nev.len(), 3);
934        assert_eq!(*nev.first(), 10);
935        assert_eq!(*nev.last(), 30);
936    }
937}
938#[cfg(test)]
939mod tests_padding2 {
940    use super::*;
941    #[test]
942    fn test_sliding_sum() {
943        let mut ss = SlidingSum::new(3);
944        ss.push(1.0);
945        ss.push(2.0);
946        ss.push(3.0);
947        assert!((ss.sum() - 6.0).abs() < 1e-9);
948        ss.push(4.0);
949        assert!((ss.sum() - 9.0).abs() < 1e-9);
950        assert_eq!(ss.count(), 3);
951    }
952    #[test]
953    fn test_path_buf() {
954        let mut pb = PathBuf::new();
955        pb.push("src");
956        pb.push("main");
957        assert_eq!(pb.as_str(), "src/main");
958        assert_eq!(pb.depth(), 2);
959        pb.pop();
960        assert_eq!(pb.as_str(), "src");
961    }
962    #[test]
963    fn test_string_pool() {
964        let mut pool = StringPool::new();
965        let s = pool.take();
966        assert!(s.is_empty());
967        pool.give("hello".to_string());
968        let s2 = pool.take();
969        assert!(s2.is_empty());
970        assert_eq!(pool.free_count(), 0);
971    }
972    #[test]
973    fn test_transitive_closure() {
974        let mut tc = TransitiveClosure::new(4);
975        tc.add_edge(0, 1);
976        tc.add_edge(1, 2);
977        tc.add_edge(2, 3);
978        assert!(tc.can_reach(0, 3));
979        assert!(!tc.can_reach(3, 0));
980        let r = tc.reachable_from(0);
981        assert_eq!(r.len(), 4);
982    }
983    #[test]
984    fn test_token_bucket() {
985        let mut tb = TokenBucket::new(100, 10);
986        assert_eq!(tb.available(), 100);
987        assert!(tb.try_consume(50));
988        assert_eq!(tb.available(), 50);
989        assert!(!tb.try_consume(60));
990        assert_eq!(tb.capacity(), 100);
991    }
992    #[test]
993    fn test_rewrite_rule_set() {
994        let mut rrs = RewriteRuleSet::new();
995        rrs.add(RewriteRule::unconditional(
996            "beta",
997            "App(Lam(x, b), v)",
998            "b[x:=v]",
999        ));
1000        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
1001        assert_eq!(rrs.len(), 2);
1002        assert_eq!(rrs.unconditional_rules().len(), 1);
1003        assert_eq!(rrs.conditional_rules().len(), 1);
1004        assert!(rrs.get("beta").is_some());
1005        let disp = rrs
1006            .get("beta")
1007            .expect("element at \'beta\' should exist")
1008            .display();
1009        assert!(disp.contains("→"));
1010    }
1011}
1012#[cfg(test)]
1013mod tests_padding3 {
1014    use super::*;
1015    #[test]
1016    fn test_decision_node() {
1017        let tree = DecisionNode::Branch {
1018            key: "x".into(),
1019            val: "1".into(),
1020            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
1021            no_branch: Box::new(DecisionNode::Leaf("no".into())),
1022        };
1023        let mut ctx = std::collections::HashMap::new();
1024        ctx.insert("x".into(), "1".into());
1025        assert_eq!(tree.evaluate(&ctx), "yes");
1026        ctx.insert("x".into(), "2".into());
1027        assert_eq!(tree.evaluate(&ctx), "no");
1028        assert_eq!(tree.depth(), 1);
1029    }
1030    #[test]
1031    fn test_flat_substitution() {
1032        let mut sub = FlatSubstitution::new();
1033        sub.add("foo", "bar");
1034        sub.add("baz", "qux");
1035        assert_eq!(sub.apply("foo and baz"), "bar and qux");
1036        assert_eq!(sub.len(), 2);
1037    }
1038    #[test]
1039    fn test_stopwatch() {
1040        let mut sw = Stopwatch::start();
1041        sw.split();
1042        sw.split();
1043        assert_eq!(sw.num_splits(), 2);
1044        assert!(sw.elapsed_ms() >= 0.0);
1045        for &s in sw.splits() {
1046            assert!(s >= 0.0);
1047        }
1048    }
1049    #[test]
1050    fn test_either2() {
1051        let e: Either2<i32, &str> = Either2::First(42);
1052        assert!(e.is_first());
1053        let mapped = e.map_first(|x| x * 2);
1054        assert_eq!(mapped.first(), Some(84));
1055        let e2: Either2<i32, &str> = Either2::Second("hello");
1056        assert!(e2.is_second());
1057        assert_eq!(e2.second(), Some("hello"));
1058    }
1059    #[test]
1060    fn test_write_once() {
1061        let wo: WriteOnce<u32> = WriteOnce::new();
1062        assert!(!wo.is_written());
1063        assert!(wo.write(42));
1064        assert!(!wo.write(99));
1065        assert_eq!(wo.read(), Some(42));
1066    }
1067    #[test]
1068    fn test_sparse_vec() {
1069        let mut sv: SparseVec<i32> = SparseVec::new(100);
1070        sv.set(5, 10);
1071        sv.set(50, 20);
1072        assert_eq!(*sv.get(5), 10);
1073        assert_eq!(*sv.get(50), 20);
1074        assert_eq!(*sv.get(0), 0);
1075        assert_eq!(sv.nnz(), 2);
1076        sv.set(5, 0);
1077        assert_eq!(sv.nnz(), 1);
1078    }
1079    #[test]
1080    fn test_stack_calc() {
1081        let mut calc = StackCalc::new();
1082        calc.push(3);
1083        calc.push(4);
1084        calc.add();
1085        assert_eq!(calc.peek(), Some(7));
1086        calc.push(2);
1087        calc.mul();
1088        assert_eq!(calc.peek(), Some(14));
1089    }
1090}
1091#[cfg(test)]
1092mod tests_final_padding {
1093    use super::*;
1094    #[test]
1095    fn test_min_heap() {
1096        let mut h = MinHeap::new();
1097        h.push(5u32);
1098        h.push(1u32);
1099        h.push(3u32);
1100        assert_eq!(h.peek(), Some(&1));
1101        assert_eq!(h.pop(), Some(1));
1102        assert_eq!(h.pop(), Some(3));
1103        assert_eq!(h.pop(), Some(5));
1104        assert!(h.is_empty());
1105    }
1106    #[test]
1107    fn test_prefix_counter() {
1108        let mut pc = PrefixCounter::new();
1109        pc.record("hello");
1110        pc.record("help");
1111        pc.record("world");
1112        assert_eq!(pc.count_with_prefix("hel"), 2);
1113        assert_eq!(pc.count_with_prefix("wor"), 1);
1114        assert_eq!(pc.count_with_prefix("xyz"), 0);
1115    }
1116    #[test]
1117    fn test_fixture() {
1118        let mut f = Fixture::new();
1119        f.set("key1", "val1");
1120        f.set("key2", "val2");
1121        assert_eq!(f.get("key1"), Some("val1"));
1122        assert_eq!(f.get("key3"), None);
1123        assert_eq!(f.len(), 2);
1124    }
1125}
oxilean_kernel/level/functions.rs

oxilean_kernel/level/
functions.rs
