oxilean_kernel/alpha/
functions.rs

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

oxilean_kernel/alpha/
functions.rs
