oxilean_kernel/alpha/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::{Expr, FVarId, Name};
6
7use super::types::{
8    AlphaCache, ConfigNode, DecisionNode, Either2, Fixture, FlatSubstitution, FocusStack, LabelSet,
9    MinHeap, NonEmptyVec, PathBuf, PrefixCounter, RewriteRule, RewriteRuleSet, SimpleDag,
10    SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch, StringPool, TokenBucket,
11    TransformStat, TransitiveClosure, VersionedRecord, WindowIterator, WriteOnce,
12};
13
14/// Check if two expressions are alpha equivalent.
15///
16/// Alpha equivalence means the expressions are structurally identical
17/// modulo renaming of bound variables.
18pub fn alpha_equiv(e1: &Expr, e2: &Expr) -> bool {
19    alpha_equiv_impl(e1, e2, &mut Vec::new(), &mut Vec::new())
20}
21/// Implementation of alpha equivalence with de Bruijn level tracking.
22pub(super) fn alpha_equiv_impl(
23    e1: &Expr,
24    e2: &Expr,
25    ctx1: &mut Vec<FVarId>,
26    ctx2: &mut Vec<FVarId>,
27) -> bool {
28    match (e1, e2) {
29        (Expr::BVar(i), Expr::BVar(j)) => i == j,
30        (Expr::FVar(f1), Expr::FVar(f2)) => {
31            match (
32                ctx1.iter().position(|f| f == f1),
33                ctx2.iter().position(|f| f == f2),
34            ) {
35                (Some(i), Some(j)) => i == j,
36                (None, None) => f1 == f2,
37                _ => false,
38            }
39        }
40        (Expr::Sort(l1), Expr::Sort(l2)) => l1 == l2,
41        (Expr::Const(n1, _), Expr::Const(n2, _)) => n1 == n2,
42        (Expr::App(f1, a1), Expr::App(f2, a2)) => {
43            alpha_equiv_impl(f1, f2, ctx1, ctx2) && alpha_equiv_impl(a1, a2, ctx1, ctx2)
44        }
45        (Expr::Lam(bi1, _n1, ty1, body1), Expr::Lam(bi2, _n2, ty2, body2)) => {
46            if bi1 != bi2 {
47                return false;
48            }
49            if !alpha_equiv_impl(ty1, ty2, ctx1, ctx2) {
50                return false;
51            }
52            let fvar1 = FVarId::new(ctx1.len() as u64);
53            let fvar2 = FVarId::new(ctx2.len() as u64);
54            ctx1.push(fvar1);
55            ctx2.push(fvar2);
56            let result = alpha_equiv_impl(body1, body2, ctx1, ctx2);
57            ctx1.pop();
58            ctx2.pop();
59            result
60        }
61        (Expr::Pi(bi1, _n1, ty1, body1), Expr::Pi(bi2, _n2, ty2, body2)) => {
62            if bi1 != bi2 {
63                return false;
64            }
65            if !alpha_equiv_impl(ty1, ty2, ctx1, ctx2) {
66                return false;
67            }
68            let fvar1 = FVarId::new(ctx1.len() as u64);
69            let fvar2 = FVarId::new(ctx2.len() as u64);
70            ctx1.push(fvar1);
71            ctx2.push(fvar2);
72            let result = alpha_equiv_impl(body1, body2, ctx1, ctx2);
73            ctx1.pop();
74            ctx2.pop();
75            result
76        }
77        (Expr::Let(_n1, ty1, val1, body1), Expr::Let(_n2, ty2, val2, body2)) => {
78            if !alpha_equiv_impl(ty1, ty2, ctx1, ctx2) {
79                return false;
80            }
81            if !alpha_equiv_impl(val1, val2, ctx1, ctx2) {
82                return false;
83            }
84            let fvar1 = FVarId::new(ctx1.len() as u64);
85            let fvar2 = FVarId::new(ctx2.len() as u64);
86            ctx1.push(fvar1);
87            ctx2.push(fvar2);
88            let result = alpha_equiv_impl(body1, body2, ctx1, ctx2);
89            ctx1.pop();
90            ctx2.pop();
91            result
92        }
93        (Expr::Proj(n1, i1, s1), Expr::Proj(n2, i2, s2)) => {
94            n1 == n2 && i1 == i2 && alpha_equiv_impl(s1, s2, ctx1, ctx2)
95        }
96        (Expr::Lit(l1), Expr::Lit(l2)) => l1 == l2,
97        _ => false,
98    }
99}
100/// Rename bound variables in an expression to canonical names.
101/// This produces a canonical form for alpha-equivalent expressions.
102pub fn canonicalize(expr: &Expr) -> Expr {
103    canonicalize_impl(expr, 0)
104}
105pub(super) fn canonicalize_impl(expr: &Expr, depth: u32) -> Expr {
106    match expr {
107        Expr::BVar(i) => Expr::BVar(*i),
108        Expr::FVar(f) => Expr::FVar(*f),
109        Expr::Sort(l) => Expr::Sort(l.clone()),
110        Expr::Const(n, ls) => Expr::Const(n.clone(), ls.clone()),
111        Expr::App(f, a) => Expr::App(
112            Box::new(canonicalize_impl(f, depth)),
113            Box::new(canonicalize_impl(a, depth)),
114        ),
115        Expr::Lam(bi, _n, ty, body) => {
116            let canonical_name = Name::str(format!("x{}", depth));
117            Expr::Lam(
118                *bi,
119                canonical_name,
120                Box::new(canonicalize_impl(ty, depth)),
121                Box::new(canonicalize_impl(body, depth + 1)),
122            )
123        }
124        Expr::Pi(bi, _n, ty, body) => {
125            let canonical_name = Name::str(format!("x{}", depth));
126            Expr::Pi(
127                *bi,
128                canonical_name,
129                Box::new(canonicalize_impl(ty, depth)),
130                Box::new(canonicalize_impl(body, depth + 1)),
131            )
132        }
133        Expr::Let(_n, ty, val, body) => {
134            let canonical_name = Name::str(format!("x{}", depth));
135            Expr::Let(
136                canonical_name,
137                Box::new(canonicalize_impl(ty, depth)),
138                Box::new(canonicalize_impl(val, depth)),
139                Box::new(canonicalize_impl(body, depth + 1)),
140            )
141        }
142        Expr::Proj(n, i, s) => Expr::Proj(n.clone(), *i, Box::new(canonicalize_impl(s, depth))),
143        Expr::Lit(l) => Expr::Lit(l.clone()),
144    }
145}
146#[cfg(test)]
147mod tests {
148    use super::*;
149    use crate::{BinderInfo, Level, Literal};
150    #[test]
151    fn test_alpha_equiv_bvar() {
152        let e1 = Expr::BVar(0);
153        let e2 = Expr::BVar(0);
154        assert!(alpha_equiv(&e1, &e2));
155        let e3 = Expr::BVar(1);
156        assert!(!alpha_equiv(&e1, &e3));
157    }
158    #[test]
159    fn test_alpha_equiv_sort() {
160        let e1 = Expr::Sort(Level::zero());
161        let e2 = Expr::Sort(Level::zero());
162        assert!(alpha_equiv(&e1, &e2));
163    }
164    #[test]
165    fn test_alpha_equiv_const() {
166        let e1 = Expr::Const(Name::str("Nat"), vec![]);
167        let e2 = Expr::Const(Name::str("Nat"), vec![]);
168        assert!(alpha_equiv(&e1, &e2));
169        let e3 = Expr::Const(Name::str("Bool"), vec![]);
170        assert!(!alpha_equiv(&e1, &e3));
171    }
172    #[test]
173    fn test_alpha_equiv_app() {
174        let f = Expr::Const(Name::str("f"), vec![]);
175        let a = Expr::Lit(Literal::Nat(42));
176        let e1 = Expr::App(Box::new(f.clone()), Box::new(a.clone()));
177        let e2 = Expr::App(Box::new(f), Box::new(a));
178        assert!(alpha_equiv(&e1, &e2));
179    }
180    #[test]
181    fn test_alpha_equiv_lambda() {
182        let nat = Expr::Const(Name::str("Nat"), vec![]);
183        let e1 = Expr::Lam(
184            BinderInfo::Default,
185            Name::str("x"),
186            Box::new(nat.clone()),
187            Box::new(Expr::BVar(0)),
188        );
189        let e2 = Expr::Lam(
190            BinderInfo::Default,
191            Name::str("y"),
192            Box::new(nat),
193            Box::new(Expr::BVar(0)),
194        );
195        assert!(alpha_equiv(&e1, &e2));
196    }
197    #[test]
198    fn test_canonicalize() {
199        let nat = Expr::Const(Name::str("Nat"), vec![]);
200        let e1 = Expr::Lam(
201            BinderInfo::Default,
202            Name::str("different_name"),
203            Box::new(nat.clone()),
204            Box::new(Expr::BVar(0)),
205        );
206        let e2 = Expr::Lam(
207            BinderInfo::Default,
208            Name::str("another_name"),
209            Box::new(nat),
210            Box::new(Expr::BVar(0)),
211        );
212        let c1 = canonicalize(&e1);
213        let c2 = canonicalize(&e2);
214        assert_eq!(c1, c2);
215    }
216}
217/// Check if two expressions are alpha equivalent modulo universe levels.
218///
219/// Unlike `alpha_equiv`, this ignores the universe level arguments to constants.
220pub fn alpha_equiv_mod_levels(e1: &Expr, e2: &Expr) -> bool {
221    alpha_equiv_mod_levels_impl(e1, e2, &mut Vec::new(), &mut Vec::new())
222}
223pub(super) fn alpha_equiv_mod_levels_impl(
224    e1: &Expr,
225    e2: &Expr,
226    ctx1: &mut Vec<FVarId>,
227    ctx2: &mut Vec<FVarId>,
228) -> bool {
229    match (e1, e2) {
230        (Expr::BVar(i), Expr::BVar(j)) => i == j,
231        (Expr::FVar(f1), Expr::FVar(f2)) => {
232            match (
233                ctx1.iter().position(|f| f == f1),
234                ctx2.iter().position(|f| f == f2),
235            ) {
236                (Some(i), Some(j)) => i == j,
237                (None, None) => f1 == f2,
238                _ => false,
239            }
240        }
241        (Expr::Sort(l1), Expr::Sort(l2)) => l1 == l2,
242        (Expr::Const(n1, _), Expr::Const(n2, _)) => n1 == n2,
243        (Expr::App(f1, a1), Expr::App(f2, a2)) => {
244            alpha_equiv_mod_levels_impl(f1, f2, ctx1, ctx2)
245                && alpha_equiv_mod_levels_impl(a1, a2, ctx1, ctx2)
246        }
247        (Expr::Lam(bi1, _n1, ty1, body1), Expr::Lam(bi2, _n2, ty2, body2)) => {
248            if bi1 != bi2 {
249                return false;
250            }
251            if !alpha_equiv_mod_levels_impl(ty1, ty2, ctx1, ctx2) {
252                return false;
253            }
254            let fvar1 = FVarId::new(ctx1.len() as u64);
255            let fvar2 = FVarId::new(ctx2.len() as u64);
256            ctx1.push(fvar1);
257            ctx2.push(fvar2);
258            let result = alpha_equiv_mod_levels_impl(body1, body2, ctx1, ctx2);
259            ctx1.pop();
260            ctx2.pop();
261            result
262        }
263        (Expr::Pi(bi1, _n1, ty1, body1), Expr::Pi(bi2, _n2, ty2, body2)) => {
264            if bi1 != bi2 {
265                return false;
266            }
267            if !alpha_equiv_mod_levels_impl(ty1, ty2, ctx1, ctx2) {
268                return false;
269            }
270            let fvar1 = FVarId::new(ctx1.len() as u64);
271            let fvar2 = FVarId::new(ctx2.len() as u64);
272            ctx1.push(fvar1);
273            ctx2.push(fvar2);
274            let result = alpha_equiv_mod_levels_impl(body1, body2, ctx1, ctx2);
275            ctx1.pop();
276            ctx2.pop();
277            result
278        }
279        (Expr::Let(_n1, ty1, val1, body1), Expr::Let(_n2, ty2, val2, body2)) => {
280            if !alpha_equiv_mod_levels_impl(ty1, ty2, ctx1, ctx2) {
281                return false;
282            }
283            if !alpha_equiv_mod_levels_impl(val1, val2, ctx1, ctx2) {
284                return false;
285            }
286            let fvar1 = FVarId::new(ctx1.len() as u64);
287            let fvar2 = FVarId::new(ctx2.len() as u64);
288            ctx1.push(fvar1);
289            ctx2.push(fvar2);
290            let result = alpha_equiv_mod_levels_impl(body1, body2, ctx1, ctx2);
291            ctx1.pop();
292            ctx2.pop();
293            result
294        }
295        (Expr::Proj(n1, i1, s1), Expr::Proj(n2, i2, s2)) => {
296            n1 == n2 && i1 == i2 && alpha_equiv_mod_levels_impl(s1, s2, ctx1, ctx2)
297        }
298        (Expr::Lit(l1), Expr::Lit(l2)) => l1 == l2,
299        _ => false,
300    }
301}
302/// Compute an alpha-equivalence class representative.
303///
304/// Maps an expression to a canonical representative where all binder names
305/// are replaced by `x0`, `x1`, etc.
306pub fn alpha_class_rep(expr: &Expr) -> Expr {
307    canonicalize(expr)
308}
309/// Check if a list of expressions are pairwise alpha-equivalent.
310pub fn all_alpha_equiv(exprs: &[Expr]) -> bool {
311    if exprs.len() <= 1 {
312        return true;
313    }
314    let first = &exprs[0];
315    exprs[1..].iter().all(|e| alpha_equiv(first, e))
316}
317/// Find the first pair of alpha-non-equivalent expressions in a list.
318///
319/// Returns `None` if all are pairwise equivalent, or `Some((i, j))` for the first differing pair.
320pub fn find_non_equiv_pair(exprs: &[Expr]) -> Option<(usize, usize)> {
321    for i in 0..exprs.len() {
322        for j in (i + 1)..exprs.len() {
323            if !alpha_equiv(&exprs[i], &exprs[j]) {
324                return Some((i, j));
325            }
326        }
327    }
328    None
329}
330/// Compute a structural hash of an expression for alpha-equivalence purposes.
331///
332/// Two alpha-equivalent expressions will have the same hash.
333/// (Note: this is not a cryptographic hash — collisions are possible.)
334pub fn alpha_hash(expr: &Expr) -> u64 {
335    alpha_hash_impl(expr, 0)
336}
337#[allow(clippy::only_used_in_recursion)]
338pub(super) fn alpha_hash_impl(expr: &Expr, depth: u32) -> u64 {
339    use std::collections::hash_map::DefaultHasher;
340    use std::hash::{Hash, Hasher};
341    let mut h = DefaultHasher::new();
342    match expr {
343        Expr::BVar(i) => {
344            0u8.hash(&mut h);
345            i.hash(&mut h);
346        }
347        Expr::FVar(id) => {
348            1u8.hash(&mut h);
349            id.0.hash(&mut h);
350        }
351        Expr::Sort(l) => {
352            2u8.hash(&mut h);
353            format!("{:?}", l).hash(&mut h);
354        }
355        Expr::Const(n, _) => {
356            3u8.hash(&mut h);
357            format!("{}", n).hash(&mut h);
358        }
359        Expr::App(f, a) => {
360            4u8.hash(&mut h);
361            alpha_hash_impl(f, depth).hash(&mut h);
362            alpha_hash_impl(a, depth).hash(&mut h);
363        }
364        Expr::Lam(bi, _, ty, body) => {
365            5u8.hash(&mut h);
366            format!("{:?}", bi).hash(&mut h);
367            alpha_hash_impl(ty, depth).hash(&mut h);
368            alpha_hash_impl(body, depth + 1).hash(&mut h);
369        }
370        Expr::Pi(bi, _, ty, body) => {
371            6u8.hash(&mut h);
372            format!("{:?}", bi).hash(&mut h);
373            alpha_hash_impl(ty, depth).hash(&mut h);
374            alpha_hash_impl(body, depth + 1).hash(&mut h);
375        }
376        Expr::Let(_, ty, val, body) => {
377            7u8.hash(&mut h);
378            alpha_hash_impl(ty, depth).hash(&mut h);
379            alpha_hash_impl(val, depth).hash(&mut h);
380            alpha_hash_impl(body, depth + 1).hash(&mut h);
381        }
382        Expr::Proj(n, i, s) => {
383            8u8.hash(&mut h);
384            format!("{}", n).hash(&mut h);
385            i.hash(&mut h);
386            alpha_hash_impl(s, depth).hash(&mut h);
387        }
388        Expr::Lit(l) => {
389            9u8.hash(&mut h);
390            format!("{:?}", l).hash(&mut h);
391        }
392    }
393    h.finish()
394}
395#[cfg(test)]
396mod alpha_extended_tests {
397    use super::*;
398    use crate::{BinderInfo, Level, Literal};
399    fn nat() -> Expr {
400        Expr::Const(Name::str("Nat"), vec![])
401    }
402    #[test]
403    fn test_alpha_equiv_mod_levels() {
404        let e1 = Expr::Const(Name::str("f"), vec![Level::zero()]);
405        let e2 = Expr::Const(Name::str("f"), vec![Level::succ(Level::zero())]);
406        assert!(alpha_equiv_mod_levels(&e1, &e2));
407        assert!(alpha_equiv(&e1, &e2));
408        let e3 = Expr::Const(Name::str("g"), vec![Level::zero()]);
409        assert!(!alpha_equiv(&e1, &e3));
410    }
411    #[test]
412    fn test_all_alpha_equiv_empty() {
413        assert!(all_alpha_equiv(&[]));
414    }
415    #[test]
416    fn test_all_alpha_equiv_single() {
417        assert!(all_alpha_equiv(&[nat()]));
418    }
419    #[test]
420    fn test_all_alpha_equiv_same() {
421        let exprs = vec![nat(), nat(), nat()];
422        assert!(all_alpha_equiv(&exprs));
423    }
424    #[test]
425    fn test_all_alpha_equiv_different() {
426        let exprs = vec![nat(), Expr::Const(Name::str("Bool"), vec![])];
427        assert!(!all_alpha_equiv(&exprs));
428    }
429    #[test]
430    fn test_find_non_equiv_pair() {
431        let exprs = vec![nat(), nat(), Expr::Sort(Level::zero())];
432        let pair = find_non_equiv_pair(&exprs);
433        assert!(pair.is_some());
434        let (i, j) = pair.expect("pair should be valid");
435        assert!(i < j);
436    }
437    #[test]
438    fn test_find_non_equiv_pair_all_equiv() {
439        let lam1 = Expr::Lam(
440            BinderInfo::Default,
441            Name::str("x"),
442            Box::new(nat()),
443            Box::new(Expr::BVar(0)),
444        );
445        let lam2 = Expr::Lam(
446            BinderInfo::Default,
447            Name::str("y"),
448            Box::new(nat()),
449            Box::new(Expr::BVar(0)),
450        );
451        assert!(find_non_equiv_pair(&[lam1, lam2]).is_none());
452    }
453    #[test]
454    fn test_alpha_hash_same_expr() {
455        let h1 = alpha_hash(&nat());
456        let h2 = alpha_hash(&nat());
457        assert_eq!(h1, h2);
458    }
459    #[test]
460    fn test_alpha_hash_alpha_equiv() {
461        let lam1 = Expr::Lam(
462            BinderInfo::Default,
463            Name::str("x"),
464            Box::new(nat()),
465            Box::new(Expr::BVar(0)),
466        );
467        let lam2 = Expr::Lam(
468            BinderInfo::Default,
469            Name::str("y"),
470            Box::new(nat()),
471            Box::new(Expr::BVar(0)),
472        );
473        assert_eq!(alpha_hash(&lam1), alpha_hash(&lam2));
474    }
475    #[test]
476    fn test_alpha_cache_basic() {
477        let mut cache = AlphaCache::new();
478        let e1 = nat();
479        let _e2 = Expr::Const(Name::str("Bool"), vec![]);
480        assert!(cache.query(&e1, &e1).is_none());
481        let result = cache.alpha_equiv_cached(&e1, &e1);
482        assert!(result);
483        assert_eq!(cache.num_equiv(), 1);
484    }
485    #[test]
486    fn test_alpha_cache_non_equiv() {
487        let mut cache = AlphaCache::new();
488        let e1 = nat();
489        let e2 = Expr::Const(Name::str("Bool"), vec![]);
490        let result = cache.alpha_equiv_cached(&e1, &e2);
491        assert!(!result);
492        assert_eq!(cache.num_non_equiv(), 1);
493        let result2 = cache.alpha_equiv_cached(&e1, &e2);
494        assert!(!result2);
495    }
496    #[test]
497    fn test_alpha_cache_clear() {
498        let mut cache = AlphaCache::new();
499        cache.alpha_equiv_cached(&nat(), &nat());
500        assert_eq!(cache.num_equiv(), 1);
501        cache.clear();
502        assert_eq!(cache.num_equiv(), 0);
503        assert_eq!(cache.num_non_equiv(), 0);
504    }
505    #[test]
506    fn test_alpha_class_rep() {
507        let e = Expr::Lam(
508            BinderInfo::Default,
509            Name::str("uniqueName"),
510            Box::new(nat()),
511            Box::new(Expr::BVar(0)),
512        );
513        let rep = alpha_class_rep(&e);
514        if let Expr::Lam(_, name, _, _) = &rep {
515            assert!(name.to_string().starts_with('x'));
516        }
517    }
518    #[test]
519    fn test_alpha_hash_lit() {
520        let h1 = alpha_hash(&Expr::Lit(Literal::Nat(42)));
521        let h2 = alpha_hash(&Expr::Lit(Literal::Nat(42)));
522        let h3 = alpha_hash(&Expr::Lit(Literal::Nat(43)));
523        assert_eq!(h1, h2);
524        assert_ne!(h1, h3);
525    }
526}
527/// Rename a specific bound variable index in an expression.
528///
529/// Replaces all occurrences of `BVar(from_idx)` with `BVar(to_idx)`.
530/// This is only safe when both indices are valid in the same context.
531pub fn rename_bvar(expr: &Expr, from_idx: u32, to_idx: u32) -> Expr {
532    rename_bvar_impl(expr, from_idx, to_idx, 0)
533}
534pub(super) fn rename_bvar_impl(expr: &Expr, from: u32, to: u32, depth: u32) -> Expr {
535    match expr {
536        Expr::BVar(i) => {
537            if *i == from + depth {
538                Expr::BVar(to + depth)
539            } else {
540                Expr::BVar(*i)
541            }
542        }
543        Expr::App(f, a) => Expr::App(
544            Box::new(rename_bvar_impl(f, from, to, depth)),
545            Box::new(rename_bvar_impl(a, from, to, depth)),
546        ),
547        Expr::Lam(bi, n, ty, body) => Expr::Lam(
548            *bi,
549            n.clone(),
550            Box::new(rename_bvar_impl(ty, from, to, depth)),
551            Box::new(rename_bvar_impl(body, from, to, depth + 1)),
552        ),
553        Expr::Pi(bi, n, ty, body) => Expr::Pi(
554            *bi,
555            n.clone(),
556            Box::new(rename_bvar_impl(ty, from, to, depth)),
557            Box::new(rename_bvar_impl(body, from, to, depth + 1)),
558        ),
559        Expr::Let(n, ty, val, body) => Expr::Let(
560            n.clone(),
561            Box::new(rename_bvar_impl(ty, from, to, depth)),
562            Box::new(rename_bvar_impl(val, from, to, depth)),
563            Box::new(rename_bvar_impl(body, from, to, depth + 1)),
564        ),
565        Expr::Proj(n, i, s) => Expr::Proj(
566            n.clone(),
567            *i,
568            Box::new(rename_bvar_impl(s, from, to, depth)),
569        ),
570        e => e.clone(),
571    }
572}
573/// Swap two bound variable indices in an expression.
574///
575/// Exchanges occurrences of `BVar(i)` with `BVar(j)` and vice versa.
576pub fn swap_bvars(expr: &Expr, i: u32, j: u32) -> Expr {
577    swap_bvars_impl(expr, i, j, 0)
578}
579pub(super) fn swap_bvars_impl(expr: &Expr, i: u32, j: u32, depth: u32) -> Expr {
580    match expr {
581        Expr::BVar(k) => {
582            let adjusted_i = i + depth;
583            let adjusted_j = j + depth;
584            if *k == adjusted_i {
585                Expr::BVar(adjusted_j)
586            } else if *k == adjusted_j {
587                Expr::BVar(adjusted_i)
588            } else {
589                Expr::BVar(*k)
590            }
591        }
592        Expr::App(f, a) => Expr::App(
593            Box::new(swap_bvars_impl(f, i, j, depth)),
594            Box::new(swap_bvars_impl(a, i, j, depth)),
595        ),
596        Expr::Lam(bi, n, ty, body) => Expr::Lam(
597            *bi,
598            n.clone(),
599            Box::new(swap_bvars_impl(ty, i, j, depth)),
600            Box::new(swap_bvars_impl(body, i, j, depth + 1)),
601        ),
602        Expr::Pi(bi, n, ty, body) => Expr::Pi(
603            *bi,
604            n.clone(),
605            Box::new(swap_bvars_impl(ty, i, j, depth)),
606            Box::new(swap_bvars_impl(body, i, j, depth + 1)),
607        ),
608        Expr::Let(n, ty, val, body) => Expr::Let(
609            n.clone(),
610            Box::new(swap_bvars_impl(ty, i, j, depth)),
611            Box::new(swap_bvars_impl(val, i, j, depth)),
612            Box::new(swap_bvars_impl(body, i, j, depth + 1)),
613        ),
614        Expr::Proj(n, k, s) => Expr::Proj(n.clone(), *k, Box::new(swap_bvars_impl(s, i, j, depth))),
615        e => e.clone(),
616    }
617}
618#[cfg(test)]
619mod rename_tests {
620    use super::*;
621    #[allow(dead_code)]
622    fn nat() -> Expr {
623        Expr::Const(Name::str("Nat"), vec![])
624    }
625    #[test]
626    fn test_rename_bvar_basic() {
627        let e = Expr::BVar(0);
628        let result = rename_bvar(&e, 0, 1);
629        assert_eq!(result, Expr::BVar(1));
630    }
631    #[test]
632    fn test_rename_bvar_no_match() {
633        let e = Expr::BVar(2);
634        let result = rename_bvar(&e, 0, 1);
635        assert_eq!(result, Expr::BVar(2));
636    }
637    #[test]
638    fn test_rename_bvar_in_app() {
639        let e = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(0)));
640        let result = rename_bvar(&e, 0, 5);
641        if let Expr::App(f, a) = result {
642            assert_eq!(*f, Expr::BVar(5));
643            assert_eq!(*a, Expr::BVar(5));
644        }
645    }
646    #[test]
647    fn test_swap_bvars() {
648        let e = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(1)));
649        let result = swap_bvars(&e, 0, 1);
650        if let Expr::App(f, a) = result {
651            assert_eq!(*f, Expr::BVar(1));
652            assert_eq!(*a, Expr::BVar(0));
653        }
654    }
655    #[test]
656    fn test_swap_same_idx_noop() {
657        let e = Expr::BVar(3);
658        let result = swap_bvars(&e, 3, 3);
659        assert_eq!(result, Expr::BVar(3));
660    }
661}
662/// Shift all free de Bruijn indices in `expr` by `amount`.
663///
664/// Indices ≥ `cutoff` are shifted; indices < `cutoff` are bound and left unchanged.
665/// Used when inserting an expression under new binders.
666pub fn shift(expr: &Expr, amount: i32, cutoff: u32) -> Expr {
667    shift_impl(expr, amount, cutoff)
668}
669pub(super) fn shift_impl(expr: &Expr, amount: i32, cutoff: u32) -> Expr {
670    match expr {
671        Expr::BVar(i) => {
672            if *i >= cutoff {
673                let new_i = (*i as i32 + amount).max(0) as u32;
674                Expr::BVar(new_i)
675            } else {
676                Expr::BVar(*i)
677            }
678        }
679        Expr::FVar(f) => Expr::FVar(*f),
680        Expr::Sort(l) => Expr::Sort(l.clone()),
681        Expr::Const(n, ls) => Expr::Const(n.clone(), ls.clone()),
682        Expr::App(f, a) => Expr::App(
683            Box::new(shift_impl(f, amount, cutoff)),
684            Box::new(shift_impl(a, amount, cutoff)),
685        ),
686        Expr::Lam(bi, n, ty, body) => Expr::Lam(
687            *bi,
688            n.clone(),
689            Box::new(shift_impl(ty, amount, cutoff)),
690            Box::new(shift_impl(body, amount, cutoff + 1)),
691        ),
692        Expr::Pi(bi, n, ty, body) => Expr::Pi(
693            *bi,
694            n.clone(),
695            Box::new(shift_impl(ty, amount, cutoff)),
696            Box::new(shift_impl(body, amount, cutoff + 1)),
697        ),
698        Expr::Let(n, ty, val, body) => Expr::Let(
699            n.clone(),
700            Box::new(shift_impl(ty, amount, cutoff)),
701            Box::new(shift_impl(val, amount, cutoff)),
702            Box::new(shift_impl(body, amount, cutoff + 1)),
703        ),
704        Expr::Proj(n, i, s) => Expr::Proj(n.clone(), *i, Box::new(shift_impl(s, amount, cutoff))),
705        Expr::Lit(l) => Expr::Lit(l.clone()),
706    }
707}
708/// Shift all free de Bruijn indices up by 1 (lift by one binder).
709pub fn lift(expr: &Expr) -> Expr {
710    shift(expr, 1, 0)
711}
712/// Shift all free de Bruijn indices down by 1 (used after substituting under a binder).
713pub fn lower(expr: &Expr) -> Expr {
714    shift(expr, -1, 0)
715}
716/// Structural equality: same as `alpha_equiv` but uses a simpler name-blind comparison.
717///
718/// Two expressions are structurally equal if they differ only in the names
719/// given to binders (which are cosmetic in de Bruijn representation).
720pub fn structurally_equal(e1: &Expr, e2: &Expr) -> bool {
721    alpha_equiv(e1, e2)
722}
723/// Perform capture-avoiding substitution: replace `BVar(0)` with `replacement`
724/// throughout `body`, adjusting de Bruijn indices appropriately.
725///
726/// This is the standard instantiation operation: `body[replacement/0]`.
727pub fn alpha_subst(body: &Expr, replacement: &Expr) -> Expr {
728    alpha_subst_impl(body, replacement, 0)
729}
730pub(super) fn alpha_subst_impl(body: &Expr, replacement: &Expr, depth: u32) -> Expr {
731    match body {
732        Expr::BVar(i) => {
733            if *i == depth {
734                shift(replacement, depth as i32, 0)
735            } else if *i > depth {
736                Expr::BVar(i - 1)
737            } else {
738                Expr::BVar(*i)
739            }
740        }
741        Expr::App(f, a) => Expr::App(
742            Box::new(alpha_subst_impl(f, replacement, depth)),
743            Box::new(alpha_subst_impl(a, replacement, depth)),
744        ),
745        Expr::Lam(bi, n, ty, b) => Expr::Lam(
746            *bi,
747            n.clone(),
748            Box::new(alpha_subst_impl(ty, replacement, depth)),
749            Box::new(alpha_subst_impl(b, replacement, depth + 1)),
750        ),
751        Expr::Pi(bi, n, ty, b) => Expr::Pi(
752            *bi,
753            n.clone(),
754            Box::new(alpha_subst_impl(ty, replacement, depth)),
755            Box::new(alpha_subst_impl(b, replacement, depth + 1)),
756        ),
757        Expr::Let(n, ty, val, b) => Expr::Let(
758            n.clone(),
759            Box::new(alpha_subst_impl(ty, replacement, depth)),
760            Box::new(alpha_subst_impl(val, replacement, depth)),
761            Box::new(alpha_subst_impl(b, replacement, depth + 1)),
762        ),
763        Expr::Proj(n, i, s) => Expr::Proj(
764            n.clone(),
765            *i,
766            Box::new(alpha_subst_impl(s, replacement, depth)),
767        ),
768        e => e.clone(),
769    }
770}
771/// Check if `FVar(id)` occurs free in `expr`.
772pub fn fvar_occurs(expr: &Expr, id: FVarId) -> bool {
773    match expr {
774        Expr::FVar(f) => *f == id,
775        Expr::App(f, a) => fvar_occurs(f, id) || fvar_occurs(a, id),
776        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
777            fvar_occurs(ty, id) || fvar_occurs(body, id)
778        }
779        Expr::Let(_, ty, val, body) => {
780            fvar_occurs(ty, id) || fvar_occurs(val, id) || fvar_occurs(body, id)
781        }
782        Expr::Proj(_, _, s) => fvar_occurs(s, id),
783        _ => false,
784    }
785}
786/// Collect all free variable IDs occurring in `expr`.
787pub fn free_fvars(expr: &Expr) -> std::collections::HashSet<FVarId> {
788    let mut set = std::collections::HashSet::new();
789    free_fvars_impl(expr, &mut set);
790    set
791}
792pub(super) fn free_fvars_impl(expr: &Expr, acc: &mut std::collections::HashSet<FVarId>) {
793    match expr {
794        Expr::FVar(f) => {
795            acc.insert(*f);
796        }
797        Expr::App(f, a) => {
798            free_fvars_impl(f, acc);
799            free_fvars_impl(a, acc);
800        }
801        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
802            free_fvars_impl(ty, acc);
803            free_fvars_impl(body, acc);
804        }
805        Expr::Let(_, ty, val, body) => {
806            free_fvars_impl(ty, acc);
807            free_fvars_impl(val, acc);
808            free_fvars_impl(body, acc);
809        }
810        Expr::Proj(_, _, s) => free_fvars_impl(s, acc),
811        _ => {}
812    }
813}
814/// Count the number of occurrences of `BVar(0)` in `expr` (at the current depth).
815pub fn count_bvar0_occurrences(expr: &Expr) -> usize {
816    count_bvar0_impl(expr, 0)
817}
818pub(super) fn count_bvar0_impl(expr: &Expr, depth: u32) -> usize {
819    match expr {
820        Expr::BVar(i) => {
821            if *i == depth {
822                1
823            } else {
824                0
825            }
826        }
827        Expr::App(f, a) => count_bvar0_impl(f, depth) + count_bvar0_impl(a, depth),
828        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
829            count_bvar0_impl(ty, depth) + count_bvar0_impl(body, depth + 1)
830        }
831        Expr::Let(_, ty, val, body) => {
832            count_bvar0_impl(ty, depth)
833                + count_bvar0_impl(val, depth)
834                + count_bvar0_impl(body, depth + 1)
835        }
836        Expr::Proj(_, _, s) => count_bvar0_impl(s, depth),
837        _ => 0,
838    }
839}
840/// Check whether `BVar(0)` occurs at all in `body`.
841///
842/// Useful for determining whether a lambda is an eta-candidate.
843pub fn bvar0_free(body: &Expr) -> bool {
844    count_bvar0_occurrences(body) == 0
845}
846/// Check alpha equivalence under a partial FVar substitution.
847///
848/// `subst` maps FVarIds to expressions; occurrences of `FVar(id)` in `e1`
849/// are replaced before comparison.
850pub fn alpha_equiv_under_subst(
851    e1: &Expr,
852    e2: &Expr,
853    subst: &std::collections::HashMap<FVarId, Expr>,
854) -> bool {
855    let e1_inst = apply_fvar_subst(e1, subst);
856    alpha_equiv(&e1_inst, e2)
857}
858/// Apply a map of FVar substitutions to an expression.
859pub fn apply_fvar_subst(expr: &Expr, subst: &std::collections::HashMap<FVarId, Expr>) -> Expr {
860    match expr {
861        Expr::FVar(id) => subst.get(id).cloned().unwrap_or_else(|| expr.clone()),
862        Expr::App(f, a) => Expr::App(
863            Box::new(apply_fvar_subst(f, subst)),
864            Box::new(apply_fvar_subst(a, subst)),
865        ),
866        Expr::Lam(bi, n, ty, body) => Expr::Lam(
867            *bi,
868            n.clone(),
869            Box::new(apply_fvar_subst(ty, subst)),
870            Box::new(apply_fvar_subst(body, subst)),
871        ),
872        Expr::Pi(bi, n, ty, body) => Expr::Pi(
873            *bi,
874            n.clone(),
875            Box::new(apply_fvar_subst(ty, subst)),
876            Box::new(apply_fvar_subst(body, subst)),
877        ),
878        Expr::Let(n, ty, val, body) => Expr::Let(
879            n.clone(),
880            Box::new(apply_fvar_subst(ty, subst)),
881            Box::new(apply_fvar_subst(val, subst)),
882            Box::new(apply_fvar_subst(body, subst)),
883        ),
884        Expr::Proj(n, i, s) => Expr::Proj(n.clone(), *i, Box::new(apply_fvar_subst(s, subst))),
885        e => e.clone(),
886    }
887}
888#[cfg(test)]
889mod shift_subst_tests {
890    use super::*;
891    use crate::BinderInfo;
892    use std::collections::HashMap;
893    fn nat() -> Expr {
894        Expr::Const(Name::str("Nat"), vec![])
895    }
896    #[test]
897    fn test_shift_bvar_above_cutoff() {
898        let e = Expr::BVar(1);
899        let shifted = shift(&e, 2, 0);
900        assert_eq!(shifted, Expr::BVar(3));
901    }
902    #[test]
903    fn test_shift_bvar_below_cutoff() {
904        let e = Expr::BVar(0);
905        let shifted = shift(&e, 5, 1);
906        assert_eq!(shifted, Expr::BVar(0));
907    }
908    #[test]
909    fn test_lift_basic() {
910        let e = Expr::BVar(0);
911        assert_eq!(lift(&e), Expr::BVar(1));
912    }
913    #[test]
914    fn test_lower_basic() {
915        let e = Expr::BVar(1);
916        assert_eq!(lower(&e), Expr::BVar(0));
917    }
918    #[test]
919    fn test_alpha_subst_simple() {
920        let body = Expr::BVar(0);
921        let result = alpha_subst(&body, &nat());
922        assert_eq!(result, nat());
923    }
924    #[test]
925    fn test_alpha_subst_no_occurrence() {
926        let body = Expr::BVar(1);
927        let result = alpha_subst(&body, &nat());
928        assert_eq!(result, Expr::BVar(0));
929    }
930    #[test]
931    fn test_fvar_occurs_true() {
932        let id = FVarId(42);
933        let e = Expr::FVar(id);
934        assert!(fvar_occurs(&e, id));
935    }
936    #[test]
937    fn test_fvar_occurs_false() {
938        let e = Expr::FVar(FVarId(1));
939        assert!(!fvar_occurs(&e, FVarId(2)));
940    }
941    #[test]
942    fn test_free_fvars_collects_all() {
943        let e = Expr::App(
944            Box::new(Expr::FVar(FVarId(1))),
945            Box::new(Expr::FVar(FVarId(2))),
946        );
947        let fvars = free_fvars(&e);
948        assert!(fvars.contains(&FVarId(1)));
949        assert!(fvars.contains(&FVarId(2)));
950        assert_eq!(fvars.len(), 2);
951    }
952    #[test]
953    fn test_count_bvar0_none() {
954        let e = nat();
955        assert_eq!(count_bvar0_occurrences(&e), 0);
956    }
957    #[test]
958    fn test_count_bvar0_one() {
959        let e = Expr::BVar(0);
960        assert_eq!(count_bvar0_occurrences(&e), 1);
961    }
962    #[test]
963    fn test_count_bvar0_in_app() {
964        let e = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(0)));
965        assert_eq!(count_bvar0_occurrences(&e), 2);
966    }
967    #[test]
968    fn test_bvar0_free_true() {
969        assert!(bvar0_free(&nat()));
970        assert!(bvar0_free(&Expr::BVar(1)));
971    }
972    #[test]
973    fn test_bvar0_free_false() {
974        assert!(!bvar0_free(&Expr::BVar(0)));
975    }
976    #[test]
977    fn test_apply_fvar_subst() {
978        let id = FVarId(0);
979        let mut subst = HashMap::new();
980        subst.insert(id, nat());
981        let e = Expr::FVar(id);
982        let result = apply_fvar_subst(&e, &subst);
983        assert_eq!(result, nat());
984    }
985    #[test]
986    fn test_alpha_equiv_under_subst_same() {
987        let id = FVarId(0);
988        let mut subst = HashMap::new();
989        subst.insert(id, nat());
990        let e1 = Expr::FVar(id);
991        let e2 = nat();
992        assert!(alpha_equiv_under_subst(&e1, &e2, &subst));
993    }
994    #[test]
995    fn test_structurally_equal() {
996        let lam1 = Expr::Lam(
997            BinderInfo::Default,
998            Name::str("x"),
999            Box::new(nat()),
1000            Box::new(Expr::BVar(0)),
1001        );
1002        let lam2 = Expr::Lam(
1003            BinderInfo::Default,
1004            Name::str("y"),
1005            Box::new(nat()),
1006            Box::new(Expr::BVar(0)),
1007        );
1008        assert!(structurally_equal(&lam1, &lam2));
1009    }
1010    #[test]
1011    fn test_shift_preserves_const() {
1012        let e = Expr::Const(Name::str("f"), vec![]);
1013        assert_eq!(shift(&e, 3, 0), e);
1014    }
1015    #[test]
1016    fn test_shift_in_lam() {
1017        let lam = Expr::Lam(
1018            BinderInfo::Default,
1019            Name::str("x"),
1020            Box::new(nat()),
1021            Box::new(Expr::BVar(1)),
1022        );
1023        let shifted = shift(&lam, 1, 0);
1024        if let Expr::Lam(_, _, _, body) = &shifted {
1025            assert_eq!(**body, Expr::BVar(2));
1026        } else {
1027            panic!("expected Lam");
1028        }
1029    }
1030}
1031#[cfg(test)]
1032mod tests_padding_infra {
1033    use super::*;
1034    #[test]
1035    fn test_stat_summary() {
1036        let mut ss = StatSummary::new();
1037        ss.record(10.0);
1038        ss.record(20.0);
1039        ss.record(30.0);
1040        assert_eq!(ss.count(), 3);
1041        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
1042        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
1043        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
1044    }
1045    #[test]
1046    fn test_transform_stat() {
1047        let mut ts = TransformStat::new();
1048        ts.record_before(100.0);
1049        ts.record_after(80.0);
1050        let ratio = ts.mean_ratio().expect("ratio should be present");
1051        assert!((ratio - 0.8).abs() < 1e-9);
1052    }
1053    #[test]
1054    fn test_small_map() {
1055        let mut m: SmallMap<u32, &str> = SmallMap::new();
1056        m.insert(3, "three");
1057        m.insert(1, "one");
1058        m.insert(2, "two");
1059        assert_eq!(m.get(&2), Some(&"two"));
1060        assert_eq!(m.len(), 3);
1061        let keys = m.keys();
1062        assert_eq!(*keys[0], 1);
1063        assert_eq!(*keys[2], 3);
1064    }
1065    #[test]
1066    fn test_label_set() {
1067        let mut ls = LabelSet::new();
1068        ls.add("foo");
1069        ls.add("bar");
1070        ls.add("foo");
1071        assert_eq!(ls.count(), 2);
1072        assert!(ls.has("bar"));
1073        assert!(!ls.has("baz"));
1074    }
1075    #[test]
1076    fn test_config_node() {
1077        let mut root = ConfigNode::section("root");
1078        let child = ConfigNode::leaf("key", "value");
1079        root.add_child(child);
1080        assert_eq!(root.num_children(), 1);
1081    }
1082    #[test]
1083    fn test_versioned_record() {
1084        let mut vr = VersionedRecord::new(0u32);
1085        vr.update(1);
1086        vr.update(2);
1087        assert_eq!(*vr.current(), 2);
1088        assert_eq!(vr.version(), 2);
1089        assert!(vr.has_history());
1090        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
1091    }
1092    #[test]
1093    fn test_simple_dag() {
1094        let mut dag = SimpleDag::new(4);
1095        dag.add_edge(0, 1);
1096        dag.add_edge(1, 2);
1097        dag.add_edge(2, 3);
1098        assert!(dag.can_reach(0, 3));
1099        assert!(!dag.can_reach(3, 0));
1100        let order = dag.topological_sort().expect("order should be present");
1101        assert_eq!(order, vec![0, 1, 2, 3]);
1102    }
1103    #[test]
1104    fn test_focus_stack() {
1105        let mut fs: FocusStack<&str> = FocusStack::new();
1106        fs.focus("a");
1107        fs.focus("b");
1108        assert_eq!(fs.current(), Some(&"b"));
1109        assert_eq!(fs.depth(), 2);
1110        fs.blur();
1111        assert_eq!(fs.current(), Some(&"a"));
1112    }
1113}
1114#[cfg(test)]
1115mod tests_extra_iterators {
1116    use super::*;
1117    #[test]
1118    fn test_window_iterator() {
1119        let data = vec![1u32, 2, 3, 4, 5];
1120        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
1121        assert_eq!(windows.len(), 3);
1122        assert_eq!(windows[0], &[1, 2, 3]);
1123        assert_eq!(windows[2], &[3, 4, 5]);
1124    }
1125    #[test]
1126    fn test_non_empty_vec() {
1127        let mut nev = NonEmptyVec::singleton(10u32);
1128        nev.push(20);
1129        nev.push(30);
1130        assert_eq!(nev.len(), 3);
1131        assert_eq!(*nev.first(), 10);
1132        assert_eq!(*nev.last(), 30);
1133    }
1134}
1135#[cfg(test)]
1136mod tests_padding2 {
1137    use super::*;
1138    #[test]
1139    fn test_sliding_sum() {
1140        let mut ss = SlidingSum::new(3);
1141        ss.push(1.0);
1142        ss.push(2.0);
1143        ss.push(3.0);
1144        assert!((ss.sum() - 6.0).abs() < 1e-9);
1145        ss.push(4.0);
1146        assert!((ss.sum() - 9.0).abs() < 1e-9);
1147        assert_eq!(ss.count(), 3);
1148    }
1149    #[test]
1150    fn test_path_buf() {
1151        let mut pb = PathBuf::new();
1152        pb.push("src");
1153        pb.push("main");
1154        assert_eq!(pb.as_str(), "src/main");
1155        assert_eq!(pb.depth(), 2);
1156        pb.pop();
1157        assert_eq!(pb.as_str(), "src");
1158    }
1159    #[test]
1160    fn test_string_pool() {
1161        let mut pool = StringPool::new();
1162        let s = pool.take();
1163        assert!(s.is_empty());
1164        pool.give("hello".to_string());
1165        let s2 = pool.take();
1166        assert!(s2.is_empty());
1167        assert_eq!(pool.free_count(), 0);
1168    }
1169    #[test]
1170    fn test_transitive_closure() {
1171        let mut tc = TransitiveClosure::new(4);
1172        tc.add_edge(0, 1);
1173        tc.add_edge(1, 2);
1174        tc.add_edge(2, 3);
1175        assert!(tc.can_reach(0, 3));
1176        assert!(!tc.can_reach(3, 0));
1177        let r = tc.reachable_from(0);
1178        assert_eq!(r.len(), 4);
1179    }
1180    #[test]
1181    fn test_token_bucket() {
1182        let mut tb = TokenBucket::new(100, 10);
1183        assert_eq!(tb.available(), 100);
1184        assert!(tb.try_consume(50));
1185        assert_eq!(tb.available(), 50);
1186        assert!(!tb.try_consume(60));
1187        assert_eq!(tb.capacity(), 100);
1188    }
1189    #[test]
1190    fn test_rewrite_rule_set() {
1191        let mut rrs = RewriteRuleSet::new();
1192        rrs.add(RewriteRule::unconditional(
1193            "beta",
1194            "App(Lam(x, b), v)",
1195            "b[x:=v]",
1196        ));
1197        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
1198        assert_eq!(rrs.len(), 2);
1199        assert_eq!(rrs.unconditional_rules().len(), 1);
1200        assert_eq!(rrs.conditional_rules().len(), 1);
1201        assert!(rrs.get("beta").is_some());
1202        let disp = rrs
1203            .get("beta")
1204            .expect("element at \'beta\' should exist")
1205            .display();
1206        assert!(disp.contains("→"));
1207    }
1208}
1209#[cfg(test)]
1210mod tests_padding3 {
1211    use super::*;
1212    #[test]
1213    fn test_decision_node() {
1214        let tree = DecisionNode::Branch {
1215            key: "x".into(),
1216            val: "1".into(),
1217            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
1218            no_branch: Box::new(DecisionNode::Leaf("no".into())),
1219        };
1220        let mut ctx = std::collections::HashMap::new();
1221        ctx.insert("x".into(), "1".into());
1222        assert_eq!(tree.evaluate(&ctx), "yes");
1223        ctx.insert("x".into(), "2".into());
1224        assert_eq!(tree.evaluate(&ctx), "no");
1225        assert_eq!(tree.depth(), 1);
1226    }
1227    #[test]
1228    fn test_flat_substitution() {
1229        let mut sub = FlatSubstitution::new();
1230        sub.add("foo", "bar");
1231        sub.add("baz", "qux");
1232        assert_eq!(sub.apply("foo and baz"), "bar and qux");
1233        assert_eq!(sub.len(), 2);
1234    }
1235    #[test]
1236    fn test_stopwatch() {
1237        let mut sw = Stopwatch::start();
1238        sw.split();
1239        sw.split();
1240        assert_eq!(sw.num_splits(), 2);
1241        assert!(sw.elapsed_ms() >= 0.0);
1242        for &s in sw.splits() {
1243            assert!(s >= 0.0);
1244        }
1245    }
1246    #[test]
1247    fn test_either2() {
1248        let e: Either2<i32, &str> = Either2::First(42);
1249        assert!(e.is_first());
1250        let mapped = e.map_first(|x| x * 2);
1251        assert_eq!(mapped.first(), Some(84));
1252        let e2: Either2<i32, &str> = Either2::Second("hello");
1253        assert!(e2.is_second());
1254        assert_eq!(e2.second(), Some("hello"));
1255    }
1256    #[test]
1257    fn test_write_once() {
1258        let wo: WriteOnce<u32> = WriteOnce::new();
1259        assert!(!wo.is_written());
1260        assert!(wo.write(42));
1261        assert!(!wo.write(99));
1262        assert_eq!(wo.read(), Some(42));
1263    }
1264    #[test]
1265    fn test_sparse_vec() {
1266        let mut sv: SparseVec<i32> = SparseVec::new(100);
1267        sv.set(5, 10);
1268        sv.set(50, 20);
1269        assert_eq!(*sv.get(5), 10);
1270        assert_eq!(*sv.get(50), 20);
1271        assert_eq!(*sv.get(0), 0);
1272        assert_eq!(sv.nnz(), 2);
1273        sv.set(5, 0);
1274        assert_eq!(sv.nnz(), 1);
1275    }
1276    #[test]
1277    fn test_stack_calc() {
1278        let mut calc = StackCalc::new();
1279        calc.push(3);
1280        calc.push(4);
1281        calc.add();
1282        assert_eq!(calc.peek(), Some(7));
1283        calc.push(2);
1284        calc.mul();
1285        assert_eq!(calc.peek(), Some(14));
1286    }
1287}
1288#[cfg(test)]
1289mod tests_final_padding {
1290    use super::*;
1291    #[test]
1292    fn test_min_heap() {
1293        let mut h = MinHeap::new();
1294        h.push(5u32);
1295        h.push(1u32);
1296        h.push(3u32);
1297        assert_eq!(h.peek(), Some(&1));
1298        assert_eq!(h.pop(), Some(1));
1299        assert_eq!(h.pop(), Some(3));
1300        assert_eq!(h.pop(), Some(5));
1301        assert!(h.is_empty());
1302    }
1303    #[test]
1304    fn test_prefix_counter() {
1305        let mut pc = PrefixCounter::new();
1306        pc.record("hello");
1307        pc.record("help");
1308        pc.record("world");
1309        assert_eq!(pc.count_with_prefix("hel"), 2);
1310        assert_eq!(pc.count_with_prefix("wor"), 1);
1311        assert_eq!(pc.count_with_prefix("xyz"), 0);
1312    }
1313    #[test]
1314    fn test_fixture() {
1315        let mut f = Fixture::new();
1316        f.set("key1", "val1");
1317        f.set("key2", "val2");
1318        assert_eq!(f.get("key1"), Some("val1"));
1319        assert_eq!(f.get("key3"), None);
1320        assert_eq!(f.len(), 2);
1321    }
1322}
oxilean_kernel/alpha/functions.rs

oxilean_kernel/alpha/
functions.rs
