oxilean_kernel/subst/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::{Expr, FVarId};
6use std::collections::HashMap;
7
8use super::types::{
9    ConfigNode, DecisionNode, Either2, FlatSubstitution, FocusStack, LabelSet, NonEmptyVec,
10    PathBuf, RewriteRule, RewriteRuleSet, SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc,
11    StatSummary, Stopwatch, StringPool, SubstStats, Substitution, TokenBucket, TransformStat,
12    TransitiveClosure, VersionedRecord, WindowIterator, WriteOnce,
13};
14
15/// Instantiate BVar(0) with arg in body, shifting down all other BVars.
16///
17/// This is the core operation for β-reduction: `(λx.body) arg → body[arg/x]`.
18pub fn instantiate(body: &Expr, arg: &Expr) -> Expr {
19    instantiate_at(body, arg, 0)
20}
21fn instantiate_at(expr: &Expr, arg: &Expr, depth: u32) -> Expr {
22    match expr {
23        Expr::BVar(n) => {
24            if *n == depth {
25                arg.clone()
26            } else if *n > depth {
27                Expr::BVar(*n - 1)
28            } else {
29                expr.clone()
30            }
31        }
32        Expr::Sort(_) | Expr::FVar(_) | Expr::Const(_, _) | Expr::Lit(_) => expr.clone(),
33        Expr::App(f, a) => {
34            let f_new = instantiate_at(f, arg, depth);
35            let a_new = instantiate_at(a, arg, depth);
36            Expr::App(Box::new(f_new), Box::new(a_new))
37        }
38        Expr::Lam(bi, name, ty, body) => {
39            let ty_new = instantiate_at(ty, arg, depth);
40            let body_new = instantiate_at(body, arg, depth + 1);
41            Expr::Lam(*bi, name.clone(), Box::new(ty_new), Box::new(body_new))
42        }
43        Expr::Pi(bi, name, ty, body) => {
44            let ty_new = instantiate_at(ty, arg, depth);
45            let body_new = instantiate_at(body, arg, depth + 1);
46            Expr::Pi(*bi, name.clone(), Box::new(ty_new), Box::new(body_new))
47        }
48        Expr::Let(name, ty, val, body) => {
49            let ty_new = instantiate_at(ty, arg, depth);
50            let val_new = instantiate_at(val, arg, depth);
51            let body_new = instantiate_at(body, arg, depth + 1);
52            Expr::Let(
53                name.clone(),
54                Box::new(ty_new),
55                Box::new(val_new),
56                Box::new(body_new),
57            )
58        }
59        Expr::Proj(name, idx, e) => {
60            let e_new = instantiate_at(e, arg, depth);
61            Expr::Proj(name.clone(), *idx, Box::new(e_new))
62        }
63    }
64}
65/// Replace FVar with BVar(0), shifting up all existing BVars.
66///
67/// This is the inverse of instantiation, used when forming binders.
68pub fn abstract_expr(expr: &Expr, fvar: FVarId) -> Expr {
69    abstract_at(expr, fvar, 0)
70}
71fn abstract_at(expr: &Expr, fvar: FVarId, depth: u32) -> Expr {
72    match expr {
73        Expr::FVar(id) if *id == fvar => Expr::BVar(depth),
74        Expr::BVar(n) => Expr::BVar(*n + 1),
75        Expr::Sort(_) | Expr::FVar(_) | Expr::Const(_, _) | Expr::Lit(_) => expr.clone(),
76        Expr::App(f, a) => {
77            let f_new = abstract_at(f, fvar, depth);
78            let a_new = abstract_at(a, fvar, depth);
79            Expr::App(Box::new(f_new), Box::new(a_new))
80        }
81        Expr::Lam(bi, name, ty, body) => {
82            let ty_new = abstract_at(ty, fvar, depth);
83            let body_new = abstract_at(body, fvar, depth + 1);
84            Expr::Lam(*bi, name.clone(), Box::new(ty_new), Box::new(body_new))
85        }
86        Expr::Pi(bi, name, ty, body) => {
87            let ty_new = abstract_at(ty, fvar, depth);
88            let body_new = abstract_at(body, fvar, depth + 1);
89            Expr::Pi(*bi, name.clone(), Box::new(ty_new), Box::new(body_new))
90        }
91        Expr::Let(name, ty, val, body) => {
92            let ty_new = abstract_at(ty, fvar, depth);
93            let val_new = abstract_at(val, fvar, depth);
94            let body_new = abstract_at(body, fvar, depth + 1);
95            Expr::Let(
96                name.clone(),
97                Box::new(ty_new),
98                Box::new(val_new),
99                Box::new(body_new),
100            )
101        }
102        Expr::Proj(name, idx, e) => {
103            let e_new = abstract_at(e, fvar, depth);
104            Expr::Proj(name.clone(), *idx, Box::new(e_new))
105        }
106    }
107}
108#[cfg(test)]
109mod tests {
110    use super::*;
111    #[test]
112    fn test_instantiate_simple() {
113        let bvar0 = Expr::BVar(0);
114        let fvar = Expr::FVar(FVarId(1));
115        let result = instantiate(&bvar0, &fvar);
116        assert_eq!(result, fvar);
117    }
118    #[test]
119    fn test_instantiate_shift_down() {
120        let bvar1 = Expr::BVar(1);
121        let arg = Expr::FVar(FVarId(1));
122        let result = instantiate(&bvar1, &arg);
123        assert_eq!(result, Expr::BVar(0));
124    }
125    #[test]
126    fn test_abstract_roundtrip() {
127        let fvar_id = FVarId(42);
128        let fvar = Expr::FVar(fvar_id);
129        let abstracted = abstract_expr(&fvar, fvar_id);
130        let back = instantiate(&abstracted, &fvar);
131        assert_eq!(back, fvar);
132    }
133    #[test]
134    fn test_instantiate_app() {
135        let app = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(1)));
136        let arg = Expr::FVar(FVarId(99));
137        let result = instantiate(&app, &arg);
138        match result {
139            Expr::App(f, a) => {
140                assert_eq!(*f, arg);
141                assert_eq!(*a, Expr::BVar(0));
142            }
143            _ => panic!("Expected App"),
144        }
145    }
146}
147/// A finite mapping from free-variable identifiers to expressions.
148pub type SubstMap = HashMap<FVarId, Expr>;
149/// Simultaneously substitute `BVar(0)..BVar(k-1)` with `args[0]..args[k-1]`.
150pub fn instantiate_many(expr: &Expr, args: &[Expr]) -> Expr {
151    let k = args.len() as u32;
152    if k == 0 {
153        return expr.clone();
154    }
155    instantiate_many_at(expr, args, k, 0)
156}
157fn instantiate_many_at(expr: &Expr, args: &[Expr], k: u32, offset: u32) -> Expr {
158    match expr {
159        Expr::BVar(n) => {
160            let idx = *n;
161            if idx >= offset && idx < offset + k {
162                args[(idx - offset) as usize].clone()
163            } else if idx >= offset + k {
164                Expr::BVar(idx - k)
165            } else {
166                expr.clone()
167            }
168        }
169        Expr::Sort(_) | Expr::FVar(_) | Expr::Const(_, _) | Expr::Lit(_) => expr.clone(),
170        Expr::App(f, a) => Expr::App(
171            Box::new(instantiate_many_at(f, args, k, offset)),
172            Box::new(instantiate_many_at(a, args, k, offset)),
173        ),
174        Expr::Lam(bi, name, ty, body) => Expr::Lam(
175            *bi,
176            name.clone(),
177            Box::new(instantiate_many_at(ty, args, k, offset)),
178            Box::new(instantiate_many_at(body, args, k, offset + 1)),
179        ),
180        Expr::Pi(bi, name, ty, body) => Expr::Pi(
181            *bi,
182            name.clone(),
183            Box::new(instantiate_many_at(ty, args, k, offset)),
184            Box::new(instantiate_many_at(body, args, k, offset + 1)),
185        ),
186        Expr::Let(name, ty, val, body) => Expr::Let(
187            name.clone(),
188            Box::new(instantiate_many_at(ty, args, k, offset)),
189            Box::new(instantiate_many_at(val, args, k, offset)),
190            Box::new(instantiate_many_at(body, args, k, offset + 1)),
191        ),
192        Expr::Proj(name, idx, e) => Expr::Proj(
193            name.clone(),
194            *idx,
195            Box::new(instantiate_many_at(e, args, k, offset)),
196        ),
197    }
198}
199/// Apply a parallel substitution: replace each `FVar(id)` with the corresponding
200/// expression in `map`.
201pub fn parallel_subst(expr: &Expr, map: &SubstMap) -> Expr {
202    if map.is_empty() {
203        return expr.clone();
204    }
205    parallel_subst_impl(expr, map)
206}
207fn parallel_subst_impl(expr: &Expr, map: &SubstMap) -> Expr {
208    match expr {
209        Expr::FVar(id) => {
210            if let Some(replacement) = map.get(id) {
211                replacement.clone()
212            } else {
213                expr.clone()
214            }
215        }
216        Expr::BVar(_) | Expr::Sort(_) | Expr::Const(_, _) | Expr::Lit(_) => expr.clone(),
217        Expr::App(f, a) => Expr::App(
218            Box::new(parallel_subst_impl(f, map)),
219            Box::new(parallel_subst_impl(a, map)),
220        ),
221        Expr::Lam(bi, name, ty, body) => Expr::Lam(
222            *bi,
223            name.clone(),
224            Box::new(parallel_subst_impl(ty, map)),
225            Box::new(parallel_subst_impl(body, map)),
226        ),
227        Expr::Pi(bi, name, ty, body) => Expr::Pi(
228            *bi,
229            name.clone(),
230            Box::new(parallel_subst_impl(ty, map)),
231            Box::new(parallel_subst_impl(body, map)),
232        ),
233        Expr::Let(name, ty, val, body) => Expr::Let(
234            name.clone(),
235            Box::new(parallel_subst_impl(ty, map)),
236            Box::new(parallel_subst_impl(val, map)),
237            Box::new(parallel_subst_impl(body, map)),
238        ),
239        Expr::Proj(name, idx, e) => {
240            Expr::Proj(name.clone(), *idx, Box::new(parallel_subst_impl(e, map)))
241        }
242    }
243}
244/// Shift all `BVar(i)` with `i >= cutoff` up by `amount`.
245pub fn shift_bvars(expr: &Expr, amount: u32, cutoff: u32) -> Expr {
246    match expr {
247        Expr::BVar(i) => {
248            if *i >= cutoff {
249                Expr::BVar(*i + amount)
250            } else {
251                expr.clone()
252            }
253        }
254        Expr::Sort(_) | Expr::FVar(_) | Expr::Const(_, _) | Expr::Lit(_) => expr.clone(),
255        Expr::App(f, a) => Expr::App(
256            Box::new(shift_bvars(f, amount, cutoff)),
257            Box::new(shift_bvars(a, amount, cutoff)),
258        ),
259        Expr::Lam(bi, name, ty, body) => Expr::Lam(
260            *bi,
261            name.clone(),
262            Box::new(shift_bvars(ty, amount, cutoff)),
263            Box::new(shift_bvars(body, amount, cutoff + 1)),
264        ),
265        Expr::Pi(bi, name, ty, body) => Expr::Pi(
266            *bi,
267            name.clone(),
268            Box::new(shift_bvars(ty, amount, cutoff)),
269            Box::new(shift_bvars(body, amount, cutoff + 1)),
270        ),
271        Expr::Let(name, ty, val, body) => Expr::Let(
272            name.clone(),
273            Box::new(shift_bvars(ty, amount, cutoff)),
274            Box::new(shift_bvars(val, amount, cutoff)),
275            Box::new(shift_bvars(body, amount, cutoff + 1)),
276        ),
277        Expr::Proj(name, idx, e) => {
278            Expr::Proj(name.clone(), *idx, Box::new(shift_bvars(e, amount, cutoff)))
279        }
280    }
281}
282/// Collect the set of free `FVarId`s occurring in `expr`.
283pub fn free_vars(expr: &Expr) -> std::collections::HashSet<FVarId> {
284    let mut set = std::collections::HashSet::new();
285    free_vars_impl(expr, &mut set);
286    set
287}
288fn free_vars_impl(expr: &Expr, set: &mut std::collections::HashSet<FVarId>) {
289    match expr {
290        Expr::FVar(id) => {
291            set.insert(*id);
292        }
293        Expr::App(f, a) => {
294            free_vars_impl(f, set);
295            free_vars_impl(a, set);
296        }
297        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
298            free_vars_impl(ty, set);
299            free_vars_impl(body, set);
300        }
301        Expr::Let(_, ty, val, body) => {
302            free_vars_impl(ty, set);
303            free_vars_impl(val, set);
304            free_vars_impl(body, set);
305        }
306        Expr::Proj(_, _, e) => free_vars_impl(e, set),
307        _ => {}
308    }
309}
310/// Return `true` if `fvar` occurs free in `expr`.
311pub fn occurs_free(expr: &Expr, fvar: FVarId) -> bool {
312    match expr {
313        Expr::FVar(id) => *id == fvar,
314        Expr::App(f, a) => occurs_free(f, fvar) || occurs_free(a, fvar),
315        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
316            occurs_free(ty, fvar) || occurs_free(body, fvar)
317        }
318        Expr::Let(_, ty, val, body) => {
319            occurs_free(ty, fvar) || occurs_free(val, fvar) || occurs_free(body, fvar)
320        }
321        Expr::Proj(_, _, e) => occurs_free(e, fvar),
322        _ => false,
323    }
324}
325/// Count how many times `fvar` occurs free in `expr`.
326pub fn count_free_occurrences(expr: &Expr, fvar: FVarId) -> usize {
327    match expr {
328        Expr::FVar(id) => usize::from(*id == fvar),
329        Expr::App(f, a) => count_free_occurrences(f, fvar) + count_free_occurrences(a, fvar),
330        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
331            count_free_occurrences(ty, fvar) + count_free_occurrences(body, fvar)
332        }
333        Expr::Let(_, ty, val, body) => {
334            count_free_occurrences(ty, fvar)
335                + count_free_occurrences(val, fvar)
336                + count_free_occurrences(body, fvar)
337        }
338        Expr::Proj(_, _, e) => count_free_occurrences(e, fvar),
339        _ => 0,
340    }
341}
342/// Like [`instantiate`] but also fills in [`SubstStats`].
343pub fn instantiate_tracked(body: &Expr, arg: &Expr, stats: &mut SubstStats) -> Expr {
344    instantiate_tracked_at(body, arg, 0, stats)
345}
346fn instantiate_tracked_at(expr: &Expr, arg: &Expr, depth: u32, stats: &mut SubstStats) -> Expr {
347    stats.nodes_visited += 1;
348    match expr {
349        Expr::BVar(n) => {
350            if *n == depth {
351                stats.bvar_hits += 1;
352                arg.clone()
353            } else if *n > depth {
354                stats.bvar_misses += 1;
355                Expr::BVar(*n - 1)
356            } else {
357                expr.clone()
358            }
359        }
360        Expr::Sort(_) | Expr::FVar(_) | Expr::Const(_, _) | Expr::Lit(_) => expr.clone(),
361        Expr::App(f, a) => Expr::App(
362            Box::new(instantiate_tracked_at(f, arg, depth, stats)),
363            Box::new(instantiate_tracked_at(a, arg, depth, stats)),
364        ),
365        Expr::Lam(bi, name, ty, body) => Expr::Lam(
366            *bi,
367            name.clone(),
368            Box::new(instantiate_tracked_at(ty, arg, depth, stats)),
369            Box::new(instantiate_tracked_at(body, arg, depth + 1, stats)),
370        ),
371        Expr::Pi(bi, name, ty, body) => Expr::Pi(
372            *bi,
373            name.clone(),
374            Box::new(instantiate_tracked_at(ty, arg, depth, stats)),
375            Box::new(instantiate_tracked_at(body, arg, depth + 1, stats)),
376        ),
377        Expr::Let(name, ty, val, body) => Expr::Let(
378            name.clone(),
379            Box::new(instantiate_tracked_at(ty, arg, depth, stats)),
380            Box::new(instantiate_tracked_at(val, arg, depth, stats)),
381            Box::new(instantiate_tracked_at(body, arg, depth + 1, stats)),
382        ),
383        Expr::Proj(name, idx, e) => Expr::Proj(
384            name.clone(),
385            *idx,
386            Box::new(instantiate_tracked_at(e, arg, depth, stats)),
387        ),
388    }
389}
390/// Build a `SubstMap` from parallel slices of ids and replacements.
391pub fn build_subst_map(fvars: &[FVarId], replacements: &[Expr]) -> SubstMap {
392    assert_eq!(fvars.len(), replacements.len());
393    fvars
394        .iter()
395        .zip(replacements.iter())
396        .map(|(id, expr)| (*id, expr.clone()))
397        .collect()
398}
399/// Apply beta-reduction once at the top level if possible.
400pub fn try_beta_reduce(expr: &Expr) -> Option<Expr> {
401    match expr {
402        Expr::App(f, a) => {
403            if let Expr::Lam(_, _, _, body) = f.as_ref() {
404                Some(instantiate(body, a))
405            } else {
406                None
407            }
408        }
409        _ => None,
410    }
411}
412/// Repeatedly apply top-level beta reduction until no more is possible.
413pub fn beta_reduce_head(expr: Expr) -> Expr {
414    let mut curr = expr;
415    while let Some(reduced) = try_beta_reduce(&curr) {
416        curr = reduced;
417    }
418    curr
419}
420/// Substitute a single free variable with an expression.
421pub fn subst_fvar(expr: &Expr, fvar: FVarId, replacement: &Expr) -> Expr {
422    let mut map = SubstMap::new();
423    map.insert(fvar, replacement.clone());
424    parallel_subst(expr, &map)
425}
426/// Check whether `expr` is in weak head normal form with respect to beta.
427pub fn is_whnf_beta(expr: &Expr) -> bool {
428    match expr {
429        Expr::App(f, _) => match f.as_ref() {
430            Expr::Lam(_, _, _, _) => false,
431            other => is_whnf_beta(other),
432        },
433        _ => true,
434    }
435}
436/// Collect the indices of all loose bound variables.
437pub fn collect_loose_bvar_indices(expr: &Expr) -> Vec<u32> {
438    let mut indices = Vec::new();
439    collect_loose_bvar_impl(expr, 0, &mut indices);
440    indices.sort();
441    indices.dedup();
442    indices
443}
444fn collect_loose_bvar_impl(expr: &Expr, depth: u32, result: &mut Vec<u32>) {
445    match expr {
446        Expr::BVar(n) if *n >= depth => {
447            result.push(*n - depth);
448        }
449        Expr::BVar(_) => {}
450        Expr::App(f, a) => {
451            collect_loose_bvar_impl(f, depth, result);
452            collect_loose_bvar_impl(a, depth, result);
453        }
454        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
455            collect_loose_bvar_impl(ty, depth, result);
456            collect_loose_bvar_impl(body, depth + 1, result);
457        }
458        Expr::Let(_, ty, val, body) => {
459            collect_loose_bvar_impl(ty, depth, result);
460            collect_loose_bvar_impl(val, depth, result);
461            collect_loose_bvar_impl(body, depth + 1, result);
462        }
463        Expr::Proj(_, _, e) => collect_loose_bvar_impl(e, depth, result),
464        _ => {}
465    }
466}
467/// Apply a parallel substitution and collect profiling statistics.
468pub fn parallel_subst_tracked(expr: &Expr, map: &SubstMap, stats: &mut SubstStats) -> Expr {
469    if map.is_empty() {
470        return expr.clone();
471    }
472    parallel_subst_tracked_impl(expr, map, stats)
473}
474fn parallel_subst_tracked_impl(expr: &Expr, map: &SubstMap, stats: &mut SubstStats) -> Expr {
475    stats.nodes_visited += 1;
476    match expr {
477        Expr::FVar(id) => {
478            if let Some(r) = map.get(id) {
479                stats.fvar_hits += 1;
480                r.clone()
481            } else {
482                expr.clone()
483            }
484        }
485        Expr::BVar(_) | Expr::Sort(_) | Expr::Const(_, _) | Expr::Lit(_) => expr.clone(),
486        Expr::App(f, a) => Expr::App(
487            Box::new(parallel_subst_tracked_impl(f, map, stats)),
488            Box::new(parallel_subst_tracked_impl(a, map, stats)),
489        ),
490        Expr::Lam(bi, name, ty, body) => Expr::Lam(
491            *bi,
492            name.clone(),
493            Box::new(parallel_subst_tracked_impl(ty, map, stats)),
494            Box::new(parallel_subst_tracked_impl(body, map, stats)),
495        ),
496        Expr::Pi(bi, name, ty, body) => Expr::Pi(
497            *bi,
498            name.clone(),
499            Box::new(parallel_subst_tracked_impl(ty, map, stats)),
500            Box::new(parallel_subst_tracked_impl(body, map, stats)),
501        ),
502        Expr::Let(name, ty, val, body) => Expr::Let(
503            name.clone(),
504            Box::new(parallel_subst_tracked_impl(ty, map, stats)),
505            Box::new(parallel_subst_tracked_impl(val, map, stats)),
506            Box::new(parallel_subst_tracked_impl(body, map, stats)),
507        ),
508        Expr::Proj(name, idx, e) => Expr::Proj(
509            name.clone(),
510            *idx,
511            Box::new(parallel_subst_tracked_impl(e, map, stats)),
512        ),
513    }
514}
515#[cfg(test)]
516mod extended_tests {
517    use super::*;
518    use crate::{BinderInfo, Level, Literal, Name};
519    fn fvar(id: u64) -> Expr {
520        Expr::FVar(FVarId(id))
521    }
522    fn lit(n: u64) -> Expr {
523        Expr::Lit(Literal::Nat(n))
524    }
525    fn sort0() -> Expr {
526        Expr::Sort(Level::zero())
527    }
528    #[test]
529    fn test_instantiate_many_two() {
530        let app = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(1)));
531        let result = instantiate_many(&app, &[lit(10), lit(20)]);
532        match result {
533            Expr::App(f, a) => {
534                assert_eq!(*f, lit(10));
535                assert_eq!(*a, lit(20));
536            }
537            _ => panic!("Expected App"),
538        }
539    }
540    #[test]
541    fn test_parallel_subst_single() {
542        let mut map = SubstMap::new();
543        map.insert(FVarId(1), lit(99));
544        let expr = fvar(1);
545        assert_eq!(parallel_subst(&expr, &map), lit(99));
546    }
547    #[test]
548    fn test_parallel_subst_empty() {
549        let expr = fvar(5);
550        let map = SubstMap::new();
551        assert_eq!(parallel_subst(&expr, &map), expr);
552    }
553    #[test]
554    fn test_shift_bvars_above_cutoff() {
555        let e = Expr::BVar(2);
556        let shifted = shift_bvars(&e, 3, 1);
557        assert_eq!(shifted, Expr::BVar(5));
558    }
559    #[test]
560    fn test_shift_bvars_below_cutoff() {
561        let e = Expr::BVar(0);
562        let shifted = shift_bvars(&e, 2, 1);
563        assert_eq!(shifted, Expr::BVar(0));
564    }
565    #[test]
566    fn test_free_vars_single() {
567        let set = free_vars(&fvar(7));
568        assert_eq!(set.len(), 1);
569        assert!(set.contains(&FVarId(7)));
570    }
571    #[test]
572    fn test_occurs_free_true() {
573        let expr = Expr::App(Box::new(fvar(1)), Box::new(fvar(2)));
574        assert!(occurs_free(&expr, FVarId(1)));
575        assert!(!occurs_free(&expr, FVarId(3)));
576    }
577    #[test]
578    fn test_count_free_occurrences() {
579        let expr = Expr::App(Box::new(fvar(1)), Box::new(fvar(1)));
580        assert_eq!(count_free_occurrences(&expr, FVarId(1)), 2);
581    }
582    #[test]
583    fn test_subst_stats_merge() {
584        let mut a = SubstStats {
585            bvar_hits: 3,
586            bvar_misses: 1,
587            fvar_hits: 2,
588            nodes_visited: 10,
589        };
590        let b = SubstStats {
591            bvar_hits: 1,
592            bvar_misses: 0,
593            fvar_hits: 1,
594            nodes_visited: 5,
595        };
596        a.merge(&b);
597        assert_eq!(a.bvar_hits, 4);
598        assert_eq!(a.total_substs(), 7);
599    }
600    #[test]
601    fn test_instantiate_tracked() {
602        let body = Expr::BVar(0);
603        let arg = lit(42);
604        let mut stats = SubstStats::default();
605        let result = instantiate_tracked(&body, &arg, &mut stats);
606        assert_eq!(result, lit(42));
607        assert_eq!(stats.bvar_hits, 1);
608    }
609    #[test]
610    fn test_build_subst_map() {
611        let fvars = vec![FVarId(1), FVarId(2)];
612        let replacements = vec![lit(10), lit(20)];
613        let map = build_subst_map(&fvars, &replacements);
614        assert_eq!(map.get(&FVarId(1)), Some(&lit(10)));
615    }
616    #[test]
617    fn test_try_beta_reduce_success() {
618        let lam = Expr::Lam(
619            BinderInfo::Default,
620            Name::str("x"),
621            Box::new(sort0()),
622            Box::new(Expr::BVar(0)),
623        );
624        let app = Expr::App(Box::new(lam), Box::new(lit(42)));
625        let result = try_beta_reduce(&app).expect("result should be present");
626        assert_eq!(result, lit(42));
627    }
628    #[test]
629    fn test_try_beta_reduce_fail() {
630        let app = Expr::App(Box::new(fvar(1)), Box::new(lit(42)));
631        assert!(try_beta_reduce(&app).is_none());
632    }
633    #[test]
634    fn test_beta_reduce_head() {
635        let lam = Expr::Lam(
636            BinderInfo::Default,
637            Name::str("x"),
638            Box::new(sort0()),
639            Box::new(Expr::BVar(0)),
640        );
641        let app = Expr::App(Box::new(lam), Box::new(lit(7)));
642        let result = beta_reduce_head(app);
643        assert_eq!(result, lit(7));
644    }
645    #[test]
646    fn test_subst_fvar() {
647        let expr = fvar(1);
648        let result = subst_fvar(&expr, FVarId(1), &lit(99));
649        assert_eq!(result, lit(99));
650    }
651    #[test]
652    fn test_is_whnf_beta_lam() {
653        let lam = Expr::Lam(
654            BinderInfo::Default,
655            Name::str("x"),
656            Box::new(sort0()),
657            Box::new(Expr::BVar(0)),
658        );
659        assert!(is_whnf_beta(&lam));
660    }
661    #[test]
662    fn test_is_whnf_beta_app_not_whnf() {
663        let lam = Expr::Lam(
664            BinderInfo::Default,
665            Name::str("x"),
666            Box::new(sort0()),
667            Box::new(Expr::BVar(0)),
668        );
669        let app = Expr::App(Box::new(lam), Box::new(lit(1)));
670        assert!(!is_whnf_beta(&app));
671    }
672    #[test]
673    fn test_collect_loose_bvar_indices() {
674        let e = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(2)));
675        let indices = collect_loose_bvar_indices(&e);
676        assert!(indices.contains(&0));
677        assert!(indices.contains(&2));
678    }
679    #[test]
680    fn test_parallel_subst_tracked() {
681        let expr = Expr::App(Box::new(fvar(1)), Box::new(fvar(2)));
682        let mut map = SubstMap::new();
683        map.insert(FVarId(1), lit(10));
684        map.insert(FVarId(2), lit(20));
685        let mut stats = SubstStats::default();
686        let result = parallel_subst_tracked(&expr, &map, &mut stats);
687        assert_eq!(stats.fvar_hits, 2);
688        match result {
689            Expr::App(f, a) => {
690                assert_eq!(*f, lit(10));
691                assert_eq!(*a, lit(20));
692            }
693            _ => panic!("Expected App"),
694        }
695    }
696}
697/// Apply a list of arguments to a function expression via beta reduction.
698///
699/// Given `f` and `[a1, a2, ..., an]`, returns `((...((f a1) a2) ...) an)`
700/// after instantiating each lambda body with the corresponding argument.
701pub fn apply_args(f: &Expr, args: &[Expr]) -> Expr {
702    let mut result = f.clone();
703    for arg in args {
704        if let Expr::Lam(_, _, _, body) = result {
705            result = instantiate(&body, arg);
706        } else {
707            result = Expr::App(Box::new(result), Box::new(arg.clone()));
708        }
709    }
710    result
711}
712/// Check if an expression is a lambda abstraction.
713#[inline]
714pub fn is_lambda(e: &Expr) -> bool {
715    matches!(e, Expr::Lam(_, _, _, _))
716}
717/// Peel off `n` leading lambda binders, collecting binder info.
718///
719/// Returns `(binders, body)` where `binders` is a vector of `(name, binder_info, type)`
720/// tuples and `body` is the inner expression with `n` fewer lambdas.
721#[allow(clippy::type_complexity)]
722pub fn peel_lambdas(
723    e: &Expr,
724    n: usize,
725) -> (Vec<(crate::Name, crate::BinderInfo, Box<Expr>)>, &Expr) {
726    let mut binders = Vec::new();
727    let mut cur = e;
728    for _ in 0..n {
729        if let Expr::Lam(bi, _, ty, body) = cur {
730            binders.push((crate::Name::Anonymous, *bi, ty.clone()));
731            cur = body;
732        } else {
733            break;
734        }
735    }
736    (binders, cur)
737}
738/// Count the number of leading lambda binders.
739pub fn count_lambdas(e: &Expr) -> usize {
740    let mut n = 0;
741    let mut cur = e;
742    while let Expr::Lam(_, _, _, body) = cur {
743        n += 1;
744        cur = body;
745    }
746    n
747}
748/// Count the number of leading pi binders.
749pub fn count_pis(e: &Expr) -> usize {
750    let mut n = 0;
751    let mut cur = e;
752    while let Expr::Pi(_, _, _, body) = cur {
753        n += 1;
754        cur = body;
755    }
756    n
757}
758#[cfg(test)]
759mod extended2_tests {
760    use super::*;
761    use crate::{BinderInfo, Expr, FVarId, Literal, Name};
762    fn lit(n: u64) -> Expr {
763        Expr::Lit(Literal::Nat(n))
764    }
765    fn fvar(id: u64) -> Expr {
766        Expr::FVar(FVarId(id))
767    }
768    #[test]
769    fn test_apply_args_lam() {
770        let body = Expr::BVar(0);
771        let lam = Expr::Lam(
772            BinderInfo::Default,
773            Name::str("_"),
774            Box::new(lit(0)),
775            Box::new(body),
776        );
777        let result = apply_args(&lam, &[lit(42)]);
778        assert_eq!(result, lit(42));
779    }
780    #[test]
781    fn test_apply_args_non_lam() {
782        let f = fvar(1);
783        let result = apply_args(&f, &[lit(1), lit(2)]);
784        match &result {
785            Expr::App(outer, arg2) => {
786                assert_eq!(**arg2, lit(2));
787                match outer.as_ref() {
788                    Expr::App(inner_f, arg1) => {
789                        assert_eq!(**inner_f, fvar(1));
790                        assert_eq!(**arg1, lit(1));
791                    }
792                    _ => panic!("Expected App"),
793                }
794            }
795            _ => panic!("Expected App"),
796        }
797    }
798    #[test]
799    fn test_is_lambda() {
800        let lam = Expr::Lam(
801            BinderInfo::Default,
802            Name::str("_"),
803            Box::new(lit(0)),
804            Box::new(lit(1)),
805        );
806        assert!(is_lambda(&lam));
807        assert!(!is_lambda(&lit(0)));
808    }
809    #[test]
810    fn test_count_lambdas() {
811        let inner = lit(0);
812        let lam1 = Expr::Lam(
813            BinderInfo::Default,
814            Name::str("_"),
815            Box::new(lit(0)),
816            Box::new(inner),
817        );
818        let lam2 = Expr::Lam(
819            BinderInfo::Default,
820            Name::str("_"),
821            Box::new(lit(0)),
822            Box::new(lam1),
823        );
824        assert_eq!(count_lambdas(&lam2), 2);
825        assert_eq!(count_lambdas(&lit(0)), 0);
826    }
827    #[test]
828    fn test_count_pis() {
829        let inner = lit(0);
830        let pi1 = Expr::Pi(
831            BinderInfo::Default,
832            Name::str("_"),
833            Box::new(lit(0)),
834            Box::new(inner),
835        );
836        let pi2 = Expr::Pi(
837            BinderInfo::Default,
838            Name::str("_"),
839            Box::new(lit(0)),
840            Box::new(pi1),
841        );
842        assert_eq!(count_pis(&pi2), 2);
843        assert_eq!(count_pis(&lit(0)), 0);
844    }
845    #[test]
846    fn test_peel_lambdas_two() {
847        let body = Expr::BVar(0);
848        let lam1 = Expr::Lam(
849            BinderInfo::Default,
850            Name::str("_"),
851            Box::new(lit(0)),
852            Box::new(body),
853        );
854        let lam2 = Expr::Lam(
855            BinderInfo::Implicit,
856            Name::str("_"),
857            Box::new(lit(0)),
858            Box::new(lam1),
859        );
860        let (binders, inner) = peel_lambdas(&lam2, 2);
861        assert_eq!(binders.len(), 2);
862        assert_eq!(binders[0].1, BinderInfo::Implicit);
863        assert_eq!(binders[1].1, BinderInfo::Default);
864        assert_eq!(*inner, Expr::BVar(0));
865    }
866    #[test]
867    fn test_apply_args_empty() {
868        let e = lit(5);
869        let result = apply_args(&e, &[]);
870        assert_eq!(result, e);
871    }
872}
873/// Apply a substitution list (as parallel arrays) to an expression.
874#[allow(dead_code)]
875pub fn substitute_fvars(expr: &Expr, fvars: &[FVarId], replacements: &[Expr]) -> Expr {
876    assert_eq!(fvars.len(), replacements.len());
877    let mut subst = Substitution::new();
878    for (fvar, rep) in fvars.iter().zip(replacements.iter()) {
879        subst.insert(*fvar, rep.clone());
880    }
881    subst.apply(expr)
882}
883/// Check if an expression contains any free variable in the given set.
884#[allow(dead_code)]
885pub fn expr_contains_fvar(expr: &Expr, fvars: &[FVarId]) -> bool {
886    match expr {
887        Expr::FVar(id) => fvars.contains(id),
888        Expr::App(f, a) => expr_contains_fvar(f, fvars) || expr_contains_fvar(a, fvars),
889        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
890            expr_contains_fvar(ty, fvars) || expr_contains_fvar(body, fvars)
891        }
892        Expr::Let(_, ty, val, body) => {
893            expr_contains_fvar(ty, fvars)
894                || expr_contains_fvar(val, fvars)
895                || expr_contains_fvar(body, fvars)
896        }
897        Expr::Proj(_, _, inner) => expr_contains_fvar(inner, fvars),
898        _ => false,
899    }
900}
901/// Replace the outermost `BVar(0)` of a body with `FVar(id)` (open a binder).
902///
903/// This is the "open" operation in locally nameless representation.
904#[allow(dead_code)]
905pub fn open_binder(body: &Expr, id: FVarId) -> Expr {
906    open_binder_at(body, &Expr::FVar(id), 0)
907}
908fn open_binder_at(expr: &Expr, fvar_expr: &Expr, depth: u32) -> Expr {
909    match expr {
910        Expr::BVar(n) => {
911            if *n == depth {
912                fvar_expr.clone()
913            } else {
914                expr.clone()
915            }
916        }
917        Expr::App(f, a) => {
918            let f2 = open_binder_at(f, fvar_expr, depth);
919            let a2 = open_binder_at(a, fvar_expr, depth);
920            Expr::App(Box::new(f2), Box::new(a2))
921        }
922        Expr::Lam(bi, name, ty, body) => {
923            let ty2 = open_binder_at(ty, fvar_expr, depth);
924            let body2 = open_binder_at(body, fvar_expr, depth + 1);
925            Expr::Lam(*bi, name.clone(), Box::new(ty2), Box::new(body2))
926        }
927        Expr::Pi(bi, name, ty, body) => {
928            let ty2 = open_binder_at(ty, fvar_expr, depth);
929            let body2 = open_binder_at(body, fvar_expr, depth + 1);
930            Expr::Pi(*bi, name.clone(), Box::new(ty2), Box::new(body2))
931        }
932        Expr::Let(name, ty, val, body) => {
933            let ty2 = open_binder_at(ty, fvar_expr, depth);
934            let val2 = open_binder_at(val, fvar_expr, depth);
935            let body2 = open_binder_at(body, fvar_expr, depth + 1);
936            Expr::Let(name.clone(), Box::new(ty2), Box::new(val2), Box::new(body2))
937        }
938        Expr::Proj(name, idx, inner) => {
939            let inner2 = open_binder_at(inner, fvar_expr, depth);
940            Expr::Proj(name.clone(), *idx, Box::new(inner2))
941        }
942        _ => expr.clone(),
943    }
944}
945#[cfg(test)]
946mod extended3_subst_tests {
947    use super::*;
948    use crate::{BinderInfo, Expr, FVarId, Literal, Name};
949    fn lit(n: u64) -> Expr {
950        Expr::Lit(Literal::Nat(n))
951    }
952    fn fvar(id: u64) -> Expr {
953        Expr::FVar(FVarId(id))
954    }
955    #[test]
956    fn test_substitution_insert_and_get() {
957        let mut s = Substitution::new();
958        s.insert(FVarId(0), lit(42));
959        assert_eq!(s.get(FVarId(0)), Some(&lit(42)));
960        assert_eq!(s.get(FVarId(1)), None);
961    }
962    #[test]
963    fn test_substitution_len() {
964        let mut s = Substitution::new();
965        assert_eq!(s.len(), 0);
966        s.insert(FVarId(0), lit(1));
967        assert_eq!(s.len(), 1);
968    }
969    #[test]
970    fn test_substitution_apply_fvar() {
971        let mut s = Substitution::new();
972        s.insert(FVarId(1), lit(99));
973        let expr = fvar(1);
974        assert_eq!(s.apply(&expr), lit(99));
975    }
976    #[test]
977    fn test_substitution_apply_no_match() {
978        let s = Substitution::new();
979        let expr = fvar(5);
980        assert_eq!(s.apply(&expr), fvar(5));
981    }
982    #[test]
983    fn test_substitution_remove() {
984        let mut s = Substitution::new();
985        s.insert(FVarId(0), lit(1));
986        s.remove(FVarId(0));
987        assert_eq!(s.len(), 0);
988    }
989    #[test]
990    fn test_substitution_restrict() {
991        let mut s = Substitution::new();
992        s.insert(FVarId(0), lit(1));
993        s.insert(FVarId(1), lit(2));
994        let r = s.restrict(&[FVarId(0)]);
995        assert_eq!(r.len(), 1);
996        assert!(r.get(FVarId(0)).is_some());
997        assert!(r.get(FVarId(1)).is_none());
998    }
999    #[test]
1000    fn test_substitute_fvars_parallel() {
1001        let expr = Expr::App(Box::new(fvar(0)), Box::new(fvar(1)));
1002        let result = substitute_fvars(&expr, &[FVarId(0), FVarId(1)], &[lit(10), lit(20)]);
1003        match result {
1004            Expr::App(f, a) => {
1005                assert_eq!(*f, lit(10));
1006                assert_eq!(*a, lit(20));
1007            }
1008            _ => panic!("Expected App"),
1009        }
1010    }
1011    #[test]
1012    fn test_expr_contains_fvar_true() {
1013        let expr = Expr::App(Box::new(fvar(3)), Box::new(lit(0)));
1014        assert!(expr_contains_fvar(&expr, &[FVarId(3)]));
1015    }
1016    #[test]
1017    fn test_expr_contains_fvar_false() {
1018        let expr = lit(5);
1019        assert!(!expr_contains_fvar(&expr, &[FVarId(0)]));
1020    }
1021    #[test]
1022    fn test_open_binder_simple() {
1023        let body = Expr::BVar(0);
1024        let result = open_binder(&body, FVarId(7));
1025        assert_eq!(result, fvar(7));
1026    }
1027    #[test]
1028    fn test_open_binder_nested() {
1029        let inner_body = Expr::BVar(0);
1030        let inner_lam = Expr::Lam(
1031            BinderInfo::Default,
1032            Name::str("_"),
1033            Box::new(Expr::Const(Name::str("Nat"), vec![])),
1034            Box::new(inner_body),
1035        );
1036        let outer_body = Expr::App(Box::new(inner_lam), Box::new(Expr::BVar(0)));
1037        let opened = open_binder(&outer_body, FVarId(99));
1038        match opened {
1039            Expr::App(f, arg) => {
1040                assert!(matches!(*f, Expr::Lam(_, _, _, _)));
1041                assert_eq!(*arg, fvar(99));
1042            }
1043            _ => panic!("Expected App"),
1044        }
1045    }
1046    #[test]
1047    fn test_substitution_compose() {
1048        let mut s1 = Substitution::new();
1049        s1.insert(FVarId(0), lit(10));
1050        let mut s2 = Substitution::new();
1051        s2.insert(FVarId(1), lit(20));
1052        let composed = s1.compose(&s2);
1053        assert_eq!(composed.get(FVarId(0)), Some(&lit(10)));
1054        assert_eq!(composed.get(FVarId(1)), Some(&lit(20)));
1055    }
1056    #[test]
1057    fn test_substitution_insert_replace() {
1058        let mut s = Substitution::new();
1059        s.insert(FVarId(0), lit(1));
1060        s.insert(FVarId(0), lit(2));
1061        assert_eq!(s.len(), 1);
1062        assert_eq!(s.get(FVarId(0)), Some(&lit(2)));
1063    }
1064}
1065#[cfg(test)]
1066mod tests_padding_infra {
1067    use super::*;
1068    #[test]
1069    fn test_stat_summary() {
1070        let mut ss = StatSummary::new();
1071        ss.record(10.0);
1072        ss.record(20.0);
1073        ss.record(30.0);
1074        assert_eq!(ss.count(), 3);
1075        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
1076        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
1077        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
1078    }
1079    #[test]
1080    fn test_transform_stat() {
1081        let mut ts = TransformStat::new();
1082        ts.record_before(100.0);
1083        ts.record_after(80.0);
1084        let ratio = ts.mean_ratio().expect("ratio should be present");
1085        assert!((ratio - 0.8).abs() < 1e-9);
1086    }
1087    #[test]
1088    fn test_small_map() {
1089        let mut m: SmallMap<u32, &str> = SmallMap::new();
1090        m.insert(3, "three");
1091        m.insert(1, "one");
1092        m.insert(2, "two");
1093        assert_eq!(m.get(&2), Some(&"two"));
1094        assert_eq!(m.len(), 3);
1095        let keys = m.keys();
1096        assert_eq!(*keys[0], 1);
1097        assert_eq!(*keys[2], 3);
1098    }
1099    #[test]
1100    fn test_label_set() {
1101        let mut ls = LabelSet::new();
1102        ls.add("foo");
1103        ls.add("bar");
1104        ls.add("foo");
1105        assert_eq!(ls.count(), 2);
1106        assert!(ls.has("bar"));
1107        assert!(!ls.has("baz"));
1108    }
1109    #[test]
1110    fn test_config_node() {
1111        let mut root = ConfigNode::section("root");
1112        let child = ConfigNode::leaf("key", "value");
1113        root.add_child(child);
1114        assert_eq!(root.num_children(), 1);
1115    }
1116    #[test]
1117    fn test_versioned_record() {
1118        let mut vr = VersionedRecord::new(0u32);
1119        vr.update(1);
1120        vr.update(2);
1121        assert_eq!(*vr.current(), 2);
1122        assert_eq!(vr.version(), 2);
1123        assert!(vr.has_history());
1124        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
1125    }
1126    #[test]
1127    fn test_simple_dag() {
1128        let mut dag = SimpleDag::new(4);
1129        dag.add_edge(0, 1);
1130        dag.add_edge(1, 2);
1131        dag.add_edge(2, 3);
1132        assert!(dag.can_reach(0, 3));
1133        assert!(!dag.can_reach(3, 0));
1134        let order = dag.topological_sort().expect("order should be present");
1135        assert_eq!(order, vec![0, 1, 2, 3]);
1136    }
1137    #[test]
1138    fn test_focus_stack() {
1139        let mut fs: FocusStack<&str> = FocusStack::new();
1140        fs.focus("a");
1141        fs.focus("b");
1142        assert_eq!(fs.current(), Some(&"b"));
1143        assert_eq!(fs.depth(), 2);
1144        fs.blur();
1145        assert_eq!(fs.current(), Some(&"a"));
1146    }
1147}
1148#[cfg(test)]
1149mod tests_extra_iterators {
1150    use super::*;
1151    #[test]
1152    fn test_window_iterator() {
1153        let data = vec![1u32, 2, 3, 4, 5];
1154        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
1155        assert_eq!(windows.len(), 3);
1156        assert_eq!(windows[0], &[1, 2, 3]);
1157        assert_eq!(windows[2], &[3, 4, 5]);
1158    }
1159    #[test]
1160    fn test_non_empty_vec() {
1161        let mut nev = NonEmptyVec::singleton(10u32);
1162        nev.push(20);
1163        nev.push(30);
1164        assert_eq!(nev.len(), 3);
1165        assert_eq!(*nev.first(), 10);
1166        assert_eq!(*nev.last(), 30);
1167    }
1168}
1169#[cfg(test)]
1170mod tests_padding2 {
1171    use super::*;
1172    #[test]
1173    fn test_sliding_sum() {
1174        let mut ss = SlidingSum::new(3);
1175        ss.push(1.0);
1176        ss.push(2.0);
1177        ss.push(3.0);
1178        assert!((ss.sum() - 6.0).abs() < 1e-9);
1179        ss.push(4.0);
1180        assert!((ss.sum() - 9.0).abs() < 1e-9);
1181        assert_eq!(ss.count(), 3);
1182    }
1183    #[test]
1184    fn test_path_buf() {
1185        let mut pb = PathBuf::new();
1186        pb.push("src");
1187        pb.push("main");
1188        assert_eq!(pb.as_str(), "src/main");
1189        assert_eq!(pb.depth(), 2);
1190        pb.pop();
1191        assert_eq!(pb.as_str(), "src");
1192    }
1193    #[test]
1194    fn test_string_pool() {
1195        let mut pool = StringPool::new();
1196        let s = pool.take();
1197        assert!(s.is_empty());
1198        pool.give("hello".to_string());
1199        let s2 = pool.take();
1200        assert!(s2.is_empty());
1201        assert_eq!(pool.free_count(), 0);
1202    }
1203    #[test]
1204    fn test_transitive_closure() {
1205        let mut tc = TransitiveClosure::new(4);
1206        tc.add_edge(0, 1);
1207        tc.add_edge(1, 2);
1208        tc.add_edge(2, 3);
1209        assert!(tc.can_reach(0, 3));
1210        assert!(!tc.can_reach(3, 0));
1211        let r = tc.reachable_from(0);
1212        assert_eq!(r.len(), 4);
1213    }
1214    #[test]
1215    fn test_token_bucket() {
1216        let mut tb = TokenBucket::new(100, 10);
1217        assert_eq!(tb.available(), 100);
1218        assert!(tb.try_consume(50));
1219        assert_eq!(tb.available(), 50);
1220        assert!(!tb.try_consume(60));
1221        assert_eq!(tb.capacity(), 100);
1222    }
1223    #[test]
1224    fn test_rewrite_rule_set() {
1225        let mut rrs = RewriteRuleSet::new();
1226        rrs.add(RewriteRule::unconditional(
1227            "beta",
1228            "App(Lam(x, b), v)",
1229            "b[x:=v]",
1230        ));
1231        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
1232        assert_eq!(rrs.len(), 2);
1233        assert_eq!(rrs.unconditional_rules().len(), 1);
1234        assert_eq!(rrs.conditional_rules().len(), 1);
1235        assert!(rrs.get("beta").is_some());
1236        let disp = rrs
1237            .get("beta")
1238            .expect("element at \'beta\' should exist")
1239            .display();
1240        assert!(disp.contains("→"));
1241    }
1242}
1243#[cfg(test)]
1244mod tests_padding3 {
1245    use super::*;
1246    #[test]
1247    fn test_decision_node() {
1248        let tree = DecisionNode::Branch {
1249            key: "x".into(),
1250            val: "1".into(),
1251            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
1252            no_branch: Box::new(DecisionNode::Leaf("no".into())),
1253        };
1254        let mut ctx = std::collections::HashMap::new();
1255        ctx.insert("x".into(), "1".into());
1256        assert_eq!(tree.evaluate(&ctx), "yes");
1257        ctx.insert("x".into(), "2".into());
1258        assert_eq!(tree.evaluate(&ctx), "no");
1259        assert_eq!(tree.depth(), 1);
1260    }
1261    #[test]
1262    fn test_flat_substitution() {
1263        let mut sub = FlatSubstitution::new();
1264        sub.add("foo", "bar");
1265        sub.add("baz", "qux");
1266        assert_eq!(sub.apply("foo and baz"), "bar and qux");
1267        assert_eq!(sub.len(), 2);
1268    }
1269    #[test]
1270    fn test_stopwatch() {
1271        let mut sw = Stopwatch::start();
1272        sw.split();
1273        sw.split();
1274        assert_eq!(sw.num_splits(), 2);
1275        assert!(sw.elapsed_ms() >= 0.0);
1276        for &s in sw.splits() {
1277            assert!(s >= 0.0);
1278        }
1279    }
1280    #[test]
1281    fn test_either2() {
1282        let e: Either2<i32, &str> = Either2::First(42);
1283        assert!(e.is_first());
1284        let mapped = e.map_first(|x| x * 2);
1285        assert_eq!(mapped.first(), Some(84));
1286        let e2: Either2<i32, &str> = Either2::Second("hello");
1287        assert!(e2.is_second());
1288        assert_eq!(e2.second(), Some("hello"));
1289    }
1290    #[test]
1291    fn test_write_once() {
1292        let wo: WriteOnce<u32> = WriteOnce::new();
1293        assert!(!wo.is_written());
1294        assert!(wo.write(42));
1295        assert!(!wo.write(99));
1296        assert_eq!(wo.read(), Some(42));
1297    }
1298    #[test]
1299    fn test_sparse_vec() {
1300        let mut sv: SparseVec<i32> = SparseVec::new(100);
1301        sv.set(5, 10);
1302        sv.set(50, 20);
1303        assert_eq!(*sv.get(5), 10);
1304        assert_eq!(*sv.get(50), 20);
1305        assert_eq!(*sv.get(0), 0);
1306        assert_eq!(sv.nnz(), 2);
1307        sv.set(5, 0);
1308        assert_eq!(sv.nnz(), 1);
1309    }
1310    #[test]
1311    fn test_stack_calc() {
1312        let mut calc = StackCalc::new();
1313        calc.push(3);
1314        calc.push(4);
1315        calc.add();
1316        assert_eq!(calc.peek(), Some(7));
1317        calc.push(2);
1318        calc.mul();
1319        assert_eq!(calc.peek(), Some(14));
1320    }
1321}
oxilean_kernel/subst/functions.rs

oxilean_kernel/subst/
functions.rs
