oxilean_kernel/beta/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::{instantiate, BinderInfo, Expr, Name};
6
7use super::types::{
8    BetaStats, ConfigNode, DecisionNode, Either2, FlatSubstitution, FocusStack, LabelSet,
9    NonEmptyVec, PathBuf, RewriteRule, RewriteRuleSet, SimpleDag, SlidingSum, SmallMap, SparseVec,
10    StackCalc, StatSummary, Stopwatch, StringPool, TokenBucket, TransformStat, TransitiveClosure,
11    VersionedRecord, WindowIterator, WriteOnce,
12};
13
14/// Perform one step of beta reduction.
15///
16/// If the expression is an application of a lambda to an argument,
17/// substitute the argument for the bound variable in the lambda body.
18pub fn beta_step(expr: &Expr) -> Option<Expr> {
19    match expr {
20        Expr::App(f, a) => {
21            if let Expr::Lam(_bi, _n, _ty, body) = f.as_ref() {
22                Some(instantiate(body, a))
23            } else {
24                None
25            }
26        }
27        _ => None,
28    }
29}
30/// Perform beta reduction to normal form.
31///
32/// Repeatedly apply beta reduction until no more reductions are possible.
33pub fn beta_normalize(expr: &Expr) -> Expr {
34    beta_normalize_impl(expr, 1000)
35}
36fn beta_normalize_impl(expr: &Expr, fuel: u32) -> Expr {
37    if fuel == 0 {
38        return expr.clone();
39    }
40    match expr {
41        Expr::App(f, a) => {
42            if let Expr::Lam(_bi, _n, _ty, body) = f.as_ref() {
43                let reduced = instantiate(body, a);
44                beta_normalize_impl(&reduced, fuel - 1)
45            } else {
46                let f_norm = beta_normalize_impl(f, fuel - 1);
47                let a_norm = beta_normalize_impl(a, fuel - 1);
48                if let Expr::Lam(_bi, _n, _ty, body) = &f_norm {
49                    let reduced = instantiate(body, &a_norm);
50                    beta_normalize_impl(&reduced, fuel - 1)
51                } else {
52                    Expr::App(Box::new(f_norm), Box::new(a_norm))
53                }
54            }
55        }
56        Expr::Lam(bi, n, ty, body) => {
57            let ty_norm = beta_normalize_impl(ty, fuel - 1);
58            let body_norm = beta_normalize_impl(body, fuel - 1);
59            Expr::Lam(*bi, n.clone(), Box::new(ty_norm), Box::new(body_norm))
60        }
61        Expr::Pi(bi, n, ty, body) => {
62            let ty_norm = beta_normalize_impl(ty, fuel - 1);
63            let body_norm = beta_normalize_impl(body, fuel - 1);
64            Expr::Pi(*bi, n.clone(), Box::new(ty_norm), Box::new(body_norm))
65        }
66        Expr::Let(n, ty, val, body) => {
67            let ty_norm = beta_normalize_impl(ty, fuel - 1);
68            let val_norm = beta_normalize_impl(val, fuel - 1);
69            let body_norm = beta_normalize_impl(body, fuel - 1);
70            Expr::Let(
71                n.clone(),
72                Box::new(ty_norm),
73                Box::new(val_norm),
74                Box::new(body_norm),
75            )
76        }
77        Expr::Proj(n, i, s) => {
78            let s_norm = beta_normalize_impl(s, fuel - 1);
79            Expr::Proj(n.clone(), *i, Box::new(s_norm))
80        }
81        e => e.clone(),
82    }
83}
84/// Check if an expression is in beta normal form.
85pub fn is_beta_normal(expr: &Expr) -> bool {
86    match expr {
87        Expr::App(f, _) => {
88            if matches!(f.as_ref(), Expr::Lam(..)) {
89                return false;
90            }
91            is_beta_normal(f) && is_beta_normal(f)
92        }
93        Expr::Lam(_, _, ty, body) => is_beta_normal(ty) && is_beta_normal(body),
94        Expr::Pi(_, _, ty, body) => is_beta_normal(ty) && is_beta_normal(body),
95        Expr::Let(_, ty, val, body) => {
96            is_beta_normal(ty) && is_beta_normal(val) && is_beta_normal(body)
97        }
98        Expr::Proj(_, _, s) => is_beta_normal(s),
99        Expr::BVar(_) | Expr::FVar(_) | Expr::Sort(_) | Expr::Const(..) | Expr::Lit(_) => true,
100    }
101}
102/// Beta reduce under a specific variable binding.
103pub fn beta_under_binder(body: &Expr, arg: &Expr) -> Expr {
104    instantiate(body, arg)
105}
106/// Create a beta redex (lambda application that can be reduced).
107pub fn mk_beta_redex(ty: Expr, body: Expr, arg: Expr) -> Expr {
108    Expr::App(
109        Box::new(Expr::Lam(
110            crate::BinderInfo::Default,
111            Name::str("x"),
112            Box::new(ty),
113            Box::new(body),
114        )),
115        Box::new(arg),
116    )
117}
118#[cfg(test)]
119mod tests {
120    use super::*;
121    use crate::{BinderInfo, Literal};
122    #[test]
123    fn test_beta_step_simple() {
124        let nat = Expr::Const(Name::str("Nat"), vec![]);
125        let body = Expr::BVar(0);
126        let arg = Expr::Lit(Literal::Nat(42));
127        let lam = Expr::Lam(
128            BinderInfo::Default,
129            Name::str("x"),
130            Box::new(nat),
131            Box::new(body),
132        );
133        let app = Expr::App(Box::new(lam), Box::new(arg.clone()));
134        let result = beta_step(&app);
135        assert!(result.is_some());
136        assert_eq!(result.expect("result should be valid"), arg);
137    }
138    #[test]
139    fn test_beta_step_no_redex() {
140        let e = Expr::BVar(0);
141        assert!(beta_step(&e).is_none());
142    }
143    #[test]
144    fn test_beta_normalize() {
145        let nat = Expr::Const(Name::str("Nat"), vec![]);
146        let body = Expr::BVar(0);
147        let arg = Expr::Lit(Literal::Nat(42));
148        let lam = Expr::Lam(
149            BinderInfo::Default,
150            Name::str("x"),
151            Box::new(nat),
152            Box::new(body),
153        );
154        let app = Expr::App(Box::new(lam), Box::new(arg.clone()));
155        let result = beta_normalize(&app);
156        assert_eq!(result, arg);
157    }
158    #[test]
159    fn test_is_beta_normal() {
160        let e = Expr::Lit(Literal::Nat(42));
161        assert!(is_beta_normal(&e));
162        let nat = Expr::Const(Name::str("Nat"), vec![]);
163        let lam = Expr::Lam(
164            BinderInfo::Default,
165            Name::str("x"),
166            Box::new(nat.clone()),
167            Box::new(Expr::BVar(0)),
168        );
169        assert!(is_beta_normal(&lam));
170        let app = Expr::App(Box::new(lam), Box::new(Expr::Lit(Literal::Nat(42))));
171        assert!(!is_beta_normal(&app));
172    }
173    #[test]
174    fn test_mk_beta_redex() {
175        let nat = Expr::Const(Name::str("Nat"), vec![]);
176        let body = Expr::BVar(0);
177        let arg = Expr::Lit(Literal::Nat(42));
178        let redex = mk_beta_redex(nat, body, arg.clone());
179        let result = beta_normalize(&redex);
180        assert_eq!(result, arg);
181    }
182}
183/// Perform one step of beta reduction at the outermost position.
184///
185/// Returns (reduced_expr, true) if a reduction was performed,
186/// or (expr.clone(), false) if the expression is already in WHNF.
187pub fn beta_step_with_flag(expr: &Expr) -> (Expr, bool) {
188    match expr {
189        Expr::App(f, a) => {
190            if let Expr::Lam(_bi, _n, _ty, body) = f.as_ref() {
191                (instantiate(body, a), true)
192            } else {
193                (expr.clone(), false)
194            }
195        }
196        _ => (expr.clone(), false),
197    }
198}
199/// Reduce an application spine.
200///
201/// Given head and a list of arguments, applies them sequentially,
202/// reducing whenever head is a lambda.
203pub fn reduce_app_spine(head: &Expr, args: &[Expr]) -> Expr {
204    let mut result = head.clone();
205    for arg in args {
206        result = match result {
207            Expr::Lam(_bi, _n, _ty, body) => instantiate(&body, arg),
208            other => Expr::App(Box::new(other), Box::new(arg.clone())),
209        };
210    }
211    result
212}
213/// Collect the application spine of an expression.
214///
215/// Returns (head, args) such that e = head args\[0\] ... args\[n-1\].
216pub fn collect_app_spine(e: &Expr) -> (&Expr, Vec<&Expr>) {
217    let mut args = Vec::new();
218    let mut current = e;
219    while let Expr::App(f, a) = current {
220        args.push(a.as_ref());
221        current = f;
222    }
223    args.reverse();
224    (current, args)
225}
226/// Eta-expand an expression of a known function type.
227///
228/// Given f : A -> B, produces lambda x : A. f x.
229pub fn eta_expand(f: Expr, domain_ty: Expr) -> Expr {
230    let var = Expr::BVar(0);
231    let body = Expr::App(Box::new(f), Box::new(var));
232    Expr::Lam(
233        BinderInfo::Default,
234        Name::str("x"),
235        Box::new(domain_ty),
236        Box::new(body),
237    )
238}
239/// Check if an expression is eta-reducible.
240///
241/// An expression lambda x. f x is eta-reducible to f if x does not appear in f.
242pub fn is_eta_reducible(expr: &Expr) -> bool {
243    if let Expr::Lam(_, _, _, body) = expr {
244        if let Expr::App(f, arg) = body.as_ref() {
245            if let Expr::BVar(0) = arg.as_ref() {
246                return !has_loose_bvar_aux(f, 0);
247            }
248        }
249    }
250    false
251}
252fn has_loose_bvar_aux(expr: &Expr, idx: u32) -> bool {
253    match expr {
254        Expr::BVar(i) => *i == idx,
255        Expr::App(f, a) => has_loose_bvar_aux(f, idx) || has_loose_bvar_aux(a, idx),
256        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
257            has_loose_bvar_aux(ty, idx) || has_loose_bvar_aux(body, idx + 1)
258        }
259        Expr::Let(_, ty, val, body) => {
260            has_loose_bvar_aux(ty, idx)
261                || has_loose_bvar_aux(val, idx)
262                || has_loose_bvar_aux(body, idx + 1)
263        }
264        Expr::Proj(_, _, s) => has_loose_bvar_aux(s, idx),
265        _ => false,
266    }
267}
268/// Count the number of beta reduction steps to normalize an expression.
269pub fn count_reduction_steps(expr: &Expr) -> usize {
270    count_steps_impl(expr, 100)
271}
272fn count_steps_impl(expr: &Expr, fuel: usize) -> usize {
273    if fuel == 0 {
274        return 0;
275    }
276    match expr {
277        Expr::App(f, a) => {
278            if let Expr::Lam(_bi, _n, _ty, body) = f.as_ref() {
279                let reduced = instantiate(body, a);
280                1 + count_steps_impl(&reduced, fuel - 1)
281            } else {
282                count_steps_impl(f, fuel - 1) + count_steps_impl(a, fuel - 1)
283            }
284        }
285        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
286            count_steps_impl(ty, fuel - 1) + count_steps_impl(body, fuel - 1)
287        }
288        Expr::Let(_, ty, val, body) => {
289            count_steps_impl(ty, fuel - 1)
290                + count_steps_impl(val, fuel - 1)
291                + count_steps_impl(body, fuel - 1)
292        }
293        Expr::Proj(_, _, s) => count_steps_impl(s, fuel - 1),
294        _ => 0,
295    }
296}
297/// Create a K combinator: lambda x. lambda y. x.
298pub fn mk_k_combinator(ty_x: Expr, ty_y: Expr) -> Expr {
299    let inner = Expr::Lam(
300        BinderInfo::Default,
301        Name::str("y"),
302        Box::new(ty_y),
303        Box::new(Expr::BVar(1)),
304    );
305    Expr::Lam(
306        BinderInfo::Default,
307        Name::str("x"),
308        Box::new(ty_x),
309        Box::new(inner),
310    )
311}
312/// Apply the K combinator: K x y = x.
313pub fn apply_k(x: Expr, y: Expr, ty_x: Expr, ty_y: Expr) -> Expr {
314    let k = mk_k_combinator(ty_x, ty_y);
315    let kx = Expr::App(Box::new(k), Box::new(x));
316    Expr::App(Box::new(kx), Box::new(y))
317}
318/// Create an I combinator: lambda x. x.
319pub fn mk_i_combinator(ty: Expr) -> Expr {
320    Expr::Lam(
321        BinderInfo::Default,
322        Name::str("x"),
323        Box::new(ty),
324        Box::new(Expr::BVar(0)),
325    )
326}
327/// Beta reduce with statistics collection.
328pub fn beta_normalize_with_stats(expr: &Expr, stats: &mut BetaStats) -> Expr {
329    beta_stats_impl(expr, 1000, stats, 0)
330}
331fn beta_stats_impl(expr: &Expr, fuel: u32, stats: &mut BetaStats, depth: u32) -> Expr {
332    stats.update_depth(depth);
333    if fuel == 0 {
334        stats.record_fuel_exhaustion();
335        return expr.clone();
336    }
337    match expr {
338        Expr::App(f, a) => {
339            if let Expr::Lam(_bi, _n, _ty, body) = f.as_ref() {
340                let reduced = instantiate(body, a);
341                stats.record_reduction();
342                beta_stats_impl(&reduced, fuel - 1, stats, depth)
343            } else {
344                let f_norm = beta_stats_impl(f, fuel - 1, stats, depth + 1);
345                let a_norm = beta_stats_impl(a, fuel - 1, stats, depth + 1);
346                if let Expr::Lam(_bi, _n, _ty, body) = &f_norm {
347                    let reduced = instantiate(body, &a_norm);
348                    stats.record_reduction();
349                    beta_stats_impl(&reduced, fuel - 1, stats, depth)
350                } else {
351                    Expr::App(Box::new(f_norm), Box::new(a_norm))
352                }
353            }
354        }
355        Expr::Lam(bi, n, ty, body) => {
356            let ty_n = beta_stats_impl(ty, fuel - 1, stats, depth + 1);
357            let body_n = beta_stats_impl(body, fuel - 1, stats, depth + 1);
358            Expr::Lam(*bi, n.clone(), Box::new(ty_n), Box::new(body_n))
359        }
360        Expr::Pi(bi, n, ty, body) => {
361            let ty_n = beta_stats_impl(ty, fuel - 1, stats, depth + 1);
362            let body_n = beta_stats_impl(body, fuel - 1, stats, depth + 1);
363            Expr::Pi(*bi, n.clone(), Box::new(ty_n), Box::new(body_n))
364        }
365        Expr::Let(n, ty, val, body) => {
366            let ty_n = beta_stats_impl(ty, fuel - 1, stats, depth + 1);
367            let val_n = beta_stats_impl(val, fuel - 1, stats, depth + 1);
368            let body_n = beta_stats_impl(body, fuel - 1, stats, depth + 1);
369            Expr::Let(n.clone(), Box::new(ty_n), Box::new(val_n), Box::new(body_n))
370        }
371        Expr::Proj(n, i, s) => {
372            let s_n = beta_stats_impl(s, fuel - 1, stats, depth + 1);
373            Expr::Proj(n.clone(), *i, Box::new(s_n))
374        }
375        e => e.clone(),
376    }
377}
378/// Check if an expression is in weak head normal form.
379///
380/// An expression is in WHNF if its outermost form is not a beta redex.
381pub fn is_whnf(expr: &Expr) -> bool {
382    match expr {
383        Expr::App(f, _) => !matches!(f.as_ref(), Expr::Lam(_, _, _, _)),
384        Expr::Let(_, _, _, _) => false,
385        _ => true,
386    }
387}
388/// Reduce an expression to weak head normal form.
389///
390/// Only reduces the outermost redex; does not reduce under binders.
391pub fn beta_whnf(expr: &Expr) -> Expr {
392    beta_whnf_impl(expr, 1000)
393}
394fn beta_whnf_impl(expr: &Expr, fuel: u32) -> Expr {
395    if fuel == 0 {
396        return expr.clone();
397    }
398    match expr {
399        Expr::App(f, a) => {
400            let f_whnf = beta_whnf_impl(f, fuel - 1);
401            if let Expr::Lam(_bi, _n, _ty, body) = &f_whnf {
402                let reduced = instantiate(body, a);
403                beta_whnf_impl(&reduced, fuel - 1)
404            } else {
405                Expr::App(Box::new(f_whnf), a.clone())
406            }
407        }
408        Expr::Let(_n, _ty, val, body) => {
409            let reduced = instantiate(body, val);
410            beta_whnf_impl(&reduced, fuel - 1)
411        }
412        e => e.clone(),
413    }
414}
415/// Perform fueled beta normalization.
416///
417/// Returns `(normalized_expr, remaining_fuel)`.
418pub fn beta_normalize_fueled(expr: &Expr, fuel: u32) -> (Expr, u32) {
419    beta_fueled_impl(expr, fuel)
420}
421fn beta_fueled_impl(expr: &Expr, fuel: u32) -> (Expr, u32) {
422    if fuel == 0 {
423        return (expr.clone(), 0);
424    }
425    match expr {
426        Expr::App(f, a) => {
427            let (f_norm, f_fuel) = beta_fueled_impl(f, fuel - 1);
428            if let Expr::Lam(_bi, _n, _ty, body) = &f_norm {
429                let reduced = instantiate(body, a);
430                beta_fueled_impl(&reduced, f_fuel)
431            } else {
432                let (a_norm, a_fuel) = beta_fueled_impl(a, f_fuel);
433                if let Expr::Lam(_bi, _n, _ty, body) = &f_norm {
434                    let reduced = instantiate(body, &a_norm);
435                    beta_fueled_impl(&reduced, a_fuel)
436                } else {
437                    (Expr::App(Box::new(f_norm), Box::new(a_norm)), a_fuel)
438                }
439            }
440        }
441        Expr::Lam(bi, n, ty, body) => {
442            let (ty_n, t_fuel) = beta_fueled_impl(ty, fuel - 1);
443            let (body_n, b_fuel) = beta_fueled_impl(body, t_fuel);
444            (
445                Expr::Lam(*bi, n.clone(), Box::new(ty_n), Box::new(body_n)),
446                b_fuel,
447            )
448        }
449        Expr::Pi(bi, n, ty, body) => {
450            let (ty_n, t_fuel) = beta_fueled_impl(ty, fuel - 1);
451            let (body_n, b_fuel) = beta_fueled_impl(body, t_fuel);
452            (
453                Expr::Pi(*bi, n.clone(), Box::new(ty_n), Box::new(body_n)),
454                b_fuel,
455            )
456        }
457        Expr::Let(_n, _ty, val, body) => {
458            let reduced = instantiate(body, val);
459            beta_fueled_impl(&reduced, fuel - 1)
460        }
461        Expr::Proj(n, i, s) => {
462            let (s_n, s_fuel) = beta_fueled_impl(s, fuel - 1);
463            (Expr::Proj(n.clone(), *i, Box::new(s_n)), s_fuel)
464        }
465        e => (e.clone(), fuel),
466    }
467}
468/// Eta-reduce `lambda x. f x` to `f` when `x` is not free in `f`.
469pub fn eta_reduce(expr: &Expr) -> Option<Expr> {
470    if let Expr::Lam(_, _, _, body) = expr {
471        if let Expr::App(f, arg) = body.as_ref() {
472            if let Expr::BVar(0) = arg.as_ref() {
473                if !has_loose_bvar_aux(f, 0) {
474                    return Some(*f.clone());
475                }
476            }
477        }
478    }
479    None
480}
481/// Head beta normalization: reduce only the head of an application spine.
482pub fn beta_head_normalize(expr: &Expr) -> Expr {
483    beta_head_impl(expr, 100)
484}
485fn beta_head_impl(expr: &Expr, fuel: u32) -> Expr {
486    if fuel == 0 {
487        return expr.clone();
488    }
489    match expr {
490        Expr::App(f, a) => {
491            let f_head = beta_head_impl(f, fuel - 1);
492            if let Expr::Lam(_bi, _n, _ty, body) = &f_head {
493                let reduced = instantiate(body, a);
494                beta_head_impl(&reduced, fuel - 1)
495            } else {
496                Expr::App(Box::new(f_head), a.clone())
497            }
498        }
499        e => e.clone(),
500    }
501}
502/// Count the number of redexes at the outermost position.
503pub fn count_redexes(expr: &Expr) -> usize {
504    match expr {
505        Expr::App(f, _) => {
506            if matches!(f.as_ref(), Expr::Lam(_, _, _, _)) {
507                1
508            } else {
509                0
510            }
511        }
512        _ => 0,
513    }
514}
515/// Estimate how many steps are needed to normalize an expression.
516pub fn estimate_reduction_depth(expr: &Expr) -> usize {
517    match expr {
518        Expr::App(f, a) => {
519            let base = if matches!(f.as_ref(), Expr::Lam(_, _, _, _)) {
520                1
521            } else {
522                0
523            };
524            base + estimate_reduction_depth(f) + estimate_reduction_depth(a)
525        }
526        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
527            estimate_reduction_depth(ty) + estimate_reduction_depth(body)
528        }
529        Expr::Let(_, ty, val, body) => {
530            1 + estimate_reduction_depth(ty)
531                + estimate_reduction_depth(val)
532                + estimate_reduction_depth(body)
533        }
534        Expr::Proj(_, _, s) => estimate_reduction_depth(s),
535        _ => 0,
536    }
537}
538/// Create an identity function for a given type: `lambda x : ty. x`.
539pub fn mk_identity(ty: Expr) -> Expr {
540    Expr::Lam(
541        BinderInfo::Default,
542        Name::str("x"),
543        Box::new(ty),
544        Box::new(Expr::BVar(0)),
545    )
546}
547/// Create a constant function: `lambda _ : dom. val`.
548pub fn mk_const_fn(dom: Expr, val: Expr) -> Expr {
549    Expr::Lam(
550        BinderInfo::Default,
551        Name::str("_"),
552        Box::new(dom),
553        Box::new(val),
554    )
555}
556/// Compose two functions: `lambda x : dom. f (g x)`.
557pub fn mk_compose(f: Expr, g: Expr, dom: Expr) -> Expr {
558    let var = Expr::BVar(0);
559    let g_app = Expr::App(Box::new(g), Box::new(var));
560    let f_app = Expr::App(Box::new(f), Box::new(g_app));
561    Expr::Lam(
562        BinderInfo::Default,
563        Name::str("x"),
564        Box::new(dom),
565        Box::new(f_app),
566    )
567}
568/// Create a multi-argument beta redex.
569pub fn mk_multi_beta_redex(tys: &[Expr], body: Expr, args: &[Expr]) -> Expr {
570    assert_eq!(tys.len(), args.len());
571    let mut lam = body;
572    for (i, ty) in tys.iter().enumerate().rev() {
573        lam = Expr::Lam(
574            BinderInfo::Default,
575            Name::str(format!("x{}", i)),
576            Box::new(ty.clone()),
577            Box::new(lam),
578        );
579    }
580    let mut result = lam;
581    for arg in args {
582        result = Expr::App(Box::new(result), Box::new(arg.clone()));
583    }
584    result
585}
586#[cfg(test)]
587mod extra_beta_tests {
588    use super::*;
589    use crate::Literal;
590    fn nat() -> Expr {
591        Expr::Const(Name::str("Nat"), vec![])
592    }
593    fn lit(n: u64) -> Expr {
594        Expr::Lit(Literal::Nat(n))
595    }
596    #[test]
597    fn test_beta_step_with_flag_redex() {
598        let id = Expr::Lam(
599            BinderInfo::Default,
600            Name::str("x"),
601            Box::new(nat()),
602            Box::new(Expr::BVar(0)),
603        );
604        let app = Expr::App(Box::new(id), Box::new(lit(42)));
605        let (result, reduced) = beta_step_with_flag(&app);
606        assert!(reduced);
607        assert_eq!(result, lit(42));
608    }
609    #[test]
610    fn test_beta_step_with_flag_no_redex() {
611        let e = Expr::Const(Name::str("f"), vec![]);
612        let (_, reduced) = beta_step_with_flag(&e);
613        assert!(!reduced);
614    }
615    #[test]
616    fn test_collect_app_spine() {
617        let f = Expr::Const(Name::str("f"), vec![]);
618        let a = lit(1);
619        let b = lit(2);
620        let app = Expr::App(
621            Box::new(Expr::App(Box::new(f.clone()), Box::new(a))),
622            Box::new(b),
623        );
624        let (head, args) = collect_app_spine(&app);
625        assert_eq!(head, &f);
626        assert_eq!(args.len(), 2);
627    }
628    #[test]
629    fn test_reduce_app_spine() {
630        let id = Expr::Lam(
631            BinderInfo::Default,
632            Name::str("x"),
633            Box::new(nat()),
634            Box::new(Expr::BVar(0)),
635        );
636        let result = reduce_app_spine(&id, &[lit(99)]);
637        assert_eq!(result, lit(99));
638    }
639    #[test]
640    fn test_is_eta_reducible_true() {
641        let f = Expr::Const(Name::str("f"), vec![]);
642        let body = Expr::App(Box::new(f), Box::new(Expr::BVar(0)));
643        let lam = Expr::Lam(
644            BinderInfo::Default,
645            Name::str("x"),
646            Box::new(nat()),
647            Box::new(body),
648        );
649        assert!(is_eta_reducible(&lam));
650    }
651    #[test]
652    fn test_is_eta_reducible_false() {
653        let lam = Expr::Lam(
654            BinderInfo::Default,
655            Name::str("x"),
656            Box::new(nat()),
657            Box::new(Expr::BVar(0)),
658        );
659        assert!(!is_eta_reducible(&lam));
660    }
661    #[test]
662    fn test_eta_expand_then_apply() {
663        let f = Expr::Const(Name::str("f"), vec![]);
664        let expanded = eta_expand(f.clone(), nat());
665        let result = beta_normalize(&Expr::App(Box::new(expanded), Box::new(lit(5))));
666        let expected = Expr::App(Box::new(f), Box::new(lit(5)));
667        assert_eq!(result, expected);
668    }
669    #[test]
670    fn test_mk_k_combinator() {
671        let k = mk_k_combinator(nat(), nat());
672        let kxy = Expr::App(
673            Box::new(Expr::App(Box::new(k), Box::new(lit(10)))),
674            Box::new(lit(20)),
675        );
676        assert_eq!(beta_normalize(&kxy), lit(10));
677    }
678    #[test]
679    fn test_apply_k() {
680        let kxy = apply_k(lit(10), lit(20), nat(), nat());
681        assert_eq!(beta_normalize(&kxy), lit(10));
682    }
683    #[test]
684    fn test_mk_i_combinator() {
685        let i = mk_i_combinator(nat());
686        let result = beta_normalize(&Expr::App(Box::new(i), Box::new(lit(7))));
687        assert_eq!(result, lit(7));
688    }
689    #[test]
690    fn test_count_reduction_steps() {
691        let id = Expr::Lam(
692            BinderInfo::Default,
693            Name::str("x"),
694            Box::new(nat()),
695            Box::new(Expr::BVar(0)),
696        );
697        let app = Expr::App(Box::new(id), Box::new(lit(1)));
698        let steps = count_reduction_steps(&app);
699        assert!(steps >= 1);
700    }
701    #[test]
702    fn test_beta_stats_tracking() {
703        let mut stats = BetaStats::new();
704        let id = Expr::Lam(
705            BinderInfo::Default,
706            Name::str("x"),
707            Box::new(nat()),
708            Box::new(Expr::BVar(0)),
709        );
710        let app = Expr::App(Box::new(id), Box::new(lit(3)));
711        let result = beta_normalize_with_stats(&app, &mut stats);
712        assert_eq!(result, lit(3));
713        assert!(stats.total_reductions >= 1);
714    }
715    #[test]
716    fn test_beta_stats_max_depth() {
717        let mut stats = BetaStats::new();
718        let e = Expr::Sort(crate::Level::zero());
719        beta_normalize_with_stats(&e, &mut stats);
720        assert_eq!(stats.max_depth, 0);
721    }
722}
723/// Normal-order beta reduction.
724///
725/// Reduces the leftmost, outermost redex first.
726/// This strategy is guaranteed to terminate if any strategy terminates.
727pub fn beta_normal_order(expr: &Expr) -> Expr {
728    beta_normal_order_impl(expr, 200)
729}
730fn beta_normal_order_impl(expr: &Expr, fuel: u32) -> Expr {
731    if fuel == 0 {
732        return expr.clone();
733    }
734    match expr {
735        Expr::App(f, a) => {
736            if let Expr::Lam(_bi, _n, _ty, body) = f.as_ref() {
737                let reduced = instantiate(body, a);
738                beta_normal_order_impl(&reduced, fuel - 1)
739            } else {
740                let f_norm = beta_normal_order_impl(f, fuel - 1);
741                if let Expr::Lam(_bi, _n, _ty, body) = &f_norm {
742                    let reduced = instantiate(body, a);
743                    beta_normal_order_impl(&reduced, fuel - 1)
744                } else {
745                    let a_norm = beta_normal_order_impl(a, fuel - 1);
746                    Expr::App(Box::new(f_norm), Box::new(a_norm))
747                }
748            }
749        }
750        Expr::Lam(bi, n, ty, body) => {
751            let ty_norm = beta_normal_order_impl(ty, fuel - 1);
752            let body_norm = beta_normal_order_impl(body, fuel - 1);
753            Expr::Lam(*bi, n.clone(), Box::new(ty_norm), Box::new(body_norm))
754        }
755        Expr::Pi(bi, n, ty, body) => {
756            let ty_norm = beta_normal_order_impl(ty, fuel - 1);
757            let body_norm = beta_normal_order_impl(body, fuel - 1);
758            Expr::Pi(*bi, n.clone(), Box::new(ty_norm), Box::new(body_norm))
759        }
760        Expr::Let(n, ty, val, body) => {
761            let ty_n = beta_normal_order_impl(ty, fuel - 1);
762            let val_n = beta_normal_order_impl(val, fuel - 1);
763            let body_n = beta_normal_order_impl(body, fuel - 1);
764            Expr::Let(n.clone(), Box::new(ty_n), Box::new(val_n), Box::new(body_n))
765        }
766        Expr::Proj(n, i, s) => {
767            Expr::Proj(n.clone(), *i, Box::new(beta_normal_order_impl(s, fuel - 1)))
768        }
769        e => e.clone(),
770    }
771}
772/// Applicative-order beta reduction.
773///
774/// Reduces arguments before the function body. Evaluates eagerly.
775pub fn beta_applicative_order(expr: &Expr) -> Expr {
776    beta_applicative_impl(expr, 200)
777}
778fn beta_applicative_impl(expr: &Expr, fuel: u32) -> Expr {
779    if fuel == 0 {
780        return expr.clone();
781    }
782    match expr {
783        Expr::App(f, a) => {
784            let f_norm = beta_applicative_impl(f, fuel - 1);
785            let a_norm = beta_applicative_impl(a, fuel - 1);
786            if let Expr::Lam(_bi, _n, _ty, body) = &f_norm {
787                let reduced = instantiate(body, &a_norm);
788                beta_applicative_impl(&reduced, fuel - 1)
789            } else {
790                Expr::App(Box::new(f_norm), Box::new(a_norm))
791            }
792        }
793        Expr::Lam(bi, n, ty, body) => {
794            let ty_norm = beta_applicative_impl(ty, fuel - 1);
795            let body_norm = beta_applicative_impl(body, fuel - 1);
796            Expr::Lam(*bi, n.clone(), Box::new(ty_norm), Box::new(body_norm))
797        }
798        Expr::Pi(bi, n, ty, body) => {
799            let ty_norm = beta_applicative_impl(ty, fuel - 1);
800            let body_norm = beta_applicative_impl(body, fuel - 1);
801            Expr::Pi(*bi, n.clone(), Box::new(ty_norm), Box::new(body_norm))
802        }
803        Expr::Let(n, ty, val, body) => {
804            let ty_n = beta_applicative_impl(ty, fuel - 1);
805            let val_n = beta_applicative_impl(val, fuel - 1);
806            let body_n = beta_applicative_impl(body, fuel - 1);
807            Expr::Let(n.clone(), Box::new(ty_n), Box::new(val_n), Box::new(body_n))
808        }
809        Expr::Proj(n, i, s) => {
810            Expr::Proj(n.clone(), *i, Box::new(beta_applicative_impl(s, fuel - 1)))
811        }
812        e => e.clone(),
813    }
814}
815/// Check if two expressions are beta-equivalent.
816///
817/// Two expressions are beta-equivalent if they have the same normal form.
818pub fn beta_equivalent(e1: &Expr, e2: &Expr) -> bool {
819    let n1 = beta_normalize(e1);
820    let n2 = beta_normalize(e2);
821    n1 == n2
822}
823/// Reduce all let-bindings by substitution.
824///
825/// Converts  to .
826pub fn reduce_lets(expr: &Expr) -> Expr {
827    match expr {
828        Expr::Let(_, _, val, body) => {
829            let val_reduced = reduce_lets(val);
830            let body_with_val = instantiate(body, &val_reduced);
831            reduce_lets(&body_with_val)
832        }
833        Expr::App(f, a) => Expr::App(Box::new(reduce_lets(f)), Box::new(reduce_lets(a))),
834        Expr::Lam(bi, n, ty, body) => Expr::Lam(
835            *bi,
836            n.clone(),
837            Box::new(reduce_lets(ty)),
838            Box::new(reduce_lets(body)),
839        ),
840        Expr::Pi(bi, n, ty, body) => Expr::Pi(
841            *bi,
842            n.clone(),
843            Box::new(reduce_lets(ty)),
844            Box::new(reduce_lets(body)),
845        ),
846        Expr::Proj(n, i, s) => Expr::Proj(n.clone(), *i, Box::new(reduce_lets(s))),
847        e => e.clone(),
848    }
849}
850/// Check if an expression contains any let-bindings.
851pub fn has_let(expr: &Expr) -> bool {
852    match expr {
853        Expr::Let(_, _, _, _) => true,
854        Expr::App(f, a) => has_let(f) || has_let(a),
855        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => has_let(ty) || has_let(body),
856        Expr::Proj(_, _, s) => has_let(s),
857        _ => false,
858    }
859}
860#[cfg(test)]
861mod strategy_tests {
862    use super::*;
863    use crate::Literal;
864    fn nat() -> Expr {
865        Expr::Const(Name::str("Nat"), vec![])
866    }
867    fn lit(n: u64) -> Expr {
868        Expr::Lit(Literal::Nat(n))
869    }
870    fn identity() -> Expr {
871        Expr::Lam(
872            BinderInfo::Default,
873            Name::str("x"),
874            Box::new(nat()),
875            Box::new(Expr::BVar(0)),
876        )
877    }
878    #[test]
879    fn test_normal_order_simple() {
880        let app = Expr::App(Box::new(identity()), Box::new(lit(5)));
881        assert_eq!(beta_normal_order(&app), lit(5));
882    }
883    #[test]
884    fn test_applicative_order_simple() {
885        let app = Expr::App(Box::new(identity()), Box::new(lit(5)));
886        assert_eq!(beta_applicative_order(&app), lit(5));
887    }
888    #[test]
889    fn test_beta_equivalent() {
890        let id = identity();
891        let e1 = Expr::App(Box::new(id.clone()), Box::new(lit(7)));
892        let e2 = lit(7);
893        assert!(beta_equivalent(&e1, &e2));
894    }
895    #[test]
896    fn test_beta_not_equivalent() {
897        assert!(!beta_equivalent(&lit(1), &lit(2)));
898    }
899    #[test]
900    fn test_reduce_lets_basic() {
901        let body = Expr::BVar(0);
902        let val = lit(42);
903        let let_expr = Expr::Let(
904            Name::str("x"),
905            Box::new(nat()),
906            Box::new(val.clone()),
907            Box::new(body),
908        );
909        let result = reduce_lets(&let_expr);
910        assert_eq!(result, val);
911    }
912    #[test]
913    fn test_has_let_true() {
914        let let_expr = Expr::Let(
915            Name::str("x"),
916            Box::new(nat()),
917            Box::new(lit(1)),
918            Box::new(Expr::BVar(0)),
919        );
920        assert!(has_let(&let_expr));
921    }
922    #[test]
923    fn test_has_let_false() {
924        assert!(!has_let(&lit(42)));
925        assert!(!has_let(&nat()));
926    }
927    #[test]
928    fn test_reduce_lets_nested() {
929        let inner_let = Expr::Let(
930            Name::str("y"),
931            Box::new(nat()),
932            Box::new(lit(2)),
933            Box::new(Expr::BVar(1)),
934        );
935        let outer_let = Expr::Let(
936            Name::str("x"),
937            Box::new(nat()),
938            Box::new(lit(1)),
939            Box::new(inner_let),
940        );
941        let result = reduce_lets(&outer_let);
942        assert_eq!(result, lit(1));
943    }
944}
945#[cfg(test)]
946mod extra_beta_tests2 {
947    use super::*;
948    use crate::Literal;
949    fn nat() -> Expr {
950        Expr::Const(Name::str("Nat"), vec![])
951    }
952    fn lit(n: u64) -> Expr {
953        Expr::Lit(Literal::Nat(n))
954    }
955    #[test]
956    fn test_normal_order_reduces_id() {
957        let id = Expr::Lam(
958            crate::BinderInfo::Default,
959            Name::str("x"),
960            Box::new(nat()),
961            Box::new(Expr::BVar(0)),
962        );
963        let app = Expr::App(Box::new(id), Box::new(lit(5)));
964        assert_eq!(beta_normal_order(&app), lit(5));
965    }
966    #[test]
967    fn test_applicative_order_reduces_id() {
968        let id = Expr::Lam(
969            crate::BinderInfo::Default,
970            Name::str("x"),
971            Box::new(nat()),
972            Box::new(Expr::BVar(0)),
973        );
974        let app = Expr::App(Box::new(id.clone()), Box::new(lit(7)));
975        assert_eq!(beta_applicative_order(&app), lit(7));
976    }
977    #[test]
978    fn test_both_strategies_agree_on_id() {
979        let id = Expr::Lam(
980            crate::BinderInfo::Default,
981            Name::str("x"),
982            Box::new(nat()),
983            Box::new(Expr::BVar(0)),
984        );
985        let app = Expr::App(Box::new(id), Box::new(lit(3)));
986        assert_eq!(beta_normal_order(&app), beta_applicative_order(&app));
987    }
988    #[test]
989    fn test_beta_equivalent_same_normal_form() {
990        let id = Expr::Lam(
991            crate::BinderInfo::Default,
992            Name::str("x"),
993            Box::new(nat()),
994            Box::new(Expr::BVar(0)),
995        );
996        let app = Expr::App(Box::new(id), Box::new(lit(3)));
997        assert!(beta_equivalent(&app, &lit(3)));
998    }
999    #[test]
1000    fn test_beta_equivalent_different() {
1001        assert!(!beta_equivalent(&lit(1), &lit(2)));
1002    }
1003    #[test]
1004    fn test_reduce_lets_identity() {
1005        let val = lit(42);
1006        let body = Expr::BVar(0);
1007        let let_expr = Expr::Let(
1008            Name::str("x"),
1009            Box::new(nat()),
1010            Box::new(val.clone()),
1011            Box::new(body),
1012        );
1013        assert_eq!(reduce_lets(&let_expr), val);
1014    }
1015    #[test]
1016    fn test_has_let_none() {
1017        assert!(!has_let(&lit(42)));
1018        assert!(!has_let(&nat()));
1019    }
1020    #[test]
1021    fn test_has_let_some() {
1022        let let_expr = Expr::Let(
1023            Name::str("x"),
1024            Box::new(nat()),
1025            Box::new(lit(1)),
1026            Box::new(Expr::BVar(0)),
1027        );
1028        assert!(has_let(&let_expr));
1029    }
1030    #[test]
1031    fn test_beta_normal_order_no_redex() {
1032        let e = lit(42);
1033        assert_eq!(beta_normal_order(&e), e);
1034    }
1035    #[test]
1036    fn test_beta_applicative_order_no_redex() {
1037        let e = lit(42);
1038        assert_eq!(beta_applicative_order(&e), e);
1039    }
1040    #[test]
1041    fn test_is_whnf_sort() {
1042        let s = Expr::Sort(crate::Level::zero());
1043        assert!(is_whnf(&s));
1044    }
1045    #[test]
1046    fn test_is_whnf_let_is_not() {
1047        let let_expr = Expr::Let(
1048            Name::str("x"),
1049            Box::new(nat()),
1050            Box::new(lit(1)),
1051            Box::new(Expr::BVar(0)),
1052        );
1053        assert!(!is_whnf(&let_expr));
1054    }
1055    #[test]
1056    fn test_beta_whnf_simple() {
1057        let id = Expr::Lam(
1058            crate::BinderInfo::Default,
1059            Name::str("x"),
1060            Box::new(nat()),
1061            Box::new(Expr::BVar(0)),
1062        );
1063        let app = Expr::App(Box::new(id), Box::new(lit(9)));
1064        assert_eq!(beta_whnf(&app), lit(9));
1065    }
1066    #[test]
1067    fn test_beta_whnf_const() {
1068        let c = Expr::Const(Name::str("Nat"), vec![]);
1069        assert_eq!(beta_whnf(&c), c);
1070    }
1071    #[test]
1072    fn test_beta_normalize_fueled_uses_fuel() {
1073        let id = Expr::Lam(
1074            crate::BinderInfo::Default,
1075            Name::str("x"),
1076            Box::new(nat()),
1077            Box::new(Expr::BVar(0)),
1078        );
1079        let app = Expr::App(Box::new(id), Box::new(lit(5)));
1080        let (result, remaining) = beta_normalize_fueled(&app, 10);
1081        assert_eq!(result, lit(5));
1082        assert!(remaining < 10);
1083    }
1084    #[test]
1085    fn test_eta_reduce_simple() {
1086        let f = Expr::Const(Name::str("f"), vec![]);
1087        let body = Expr::App(Box::new(f.clone()), Box::new(Expr::BVar(0)));
1088        let lam = Expr::Lam(
1089            crate::BinderInfo::Default,
1090            Name::str("x"),
1091            Box::new(nat()),
1092            Box::new(body),
1093        );
1094        assert_eq!(eta_reduce(&lam), Some(f));
1095    }
1096    #[test]
1097    fn test_eta_reduce_non_eta() {
1098        let body = Expr::BVar(0);
1099        let lam = Expr::Lam(
1100            crate::BinderInfo::Default,
1101            Name::str("x"),
1102            Box::new(nat()),
1103            Box::new(body),
1104        );
1105        assert!(eta_reduce(&lam).is_none());
1106    }
1107    #[test]
1108    fn test_mk_identity_reduces_correctly() {
1109        let id = mk_identity(nat());
1110        let app = Expr::App(Box::new(id), Box::new(lit(42)));
1111        assert_eq!(beta_normalize(&app), lit(42));
1112    }
1113    #[test]
1114    fn test_mk_const_fn_ignores_arg() {
1115        let c = mk_const_fn(nat(), lit(99));
1116        let app = Expr::App(Box::new(c), Box::new(lit(0)));
1117        assert_eq!(beta_normalize(&app), lit(99));
1118    }
1119    #[test]
1120    fn test_beta_head_normalize_basic() {
1121        let id = Expr::Lam(
1122            crate::BinderInfo::Default,
1123            Name::str("x"),
1124            Box::new(nat()),
1125            Box::new(Expr::BVar(0)),
1126        );
1127        let app = Expr::App(Box::new(id), Box::new(lit(77)));
1128        assert_eq!(beta_head_normalize(&app), lit(77));
1129    }
1130    #[test]
1131    fn test_count_redexes_redex() {
1132        let id = Expr::Lam(
1133            crate::BinderInfo::Default,
1134            Name::str("x"),
1135            Box::new(nat()),
1136            Box::new(Expr::BVar(0)),
1137        );
1138        let app = Expr::App(Box::new(id), Box::new(lit(1)));
1139        assert_eq!(count_redexes(&app), 1);
1140    }
1141    #[test]
1142    fn test_estimate_reduction_depth_zero() {
1143        assert_eq!(estimate_reduction_depth(&lit(42)), 0);
1144    }
1145    #[test]
1146    fn test_estimate_reduction_depth_redex() {
1147        let id = Expr::Lam(
1148            crate::BinderInfo::Default,
1149            Name::str("x"),
1150            Box::new(nat()),
1151            Box::new(Expr::BVar(0)),
1152        );
1153        let app = Expr::App(Box::new(id), Box::new(lit(1)));
1154        assert!(estimate_reduction_depth(&app) >= 1);
1155    }
1156    #[test]
1157    fn test_mk_multi_beta_redex_single() {
1158        let body = Expr::BVar(0);
1159        let redex = mk_multi_beta_redex(&[nat()], body, &[lit(55)]);
1160        assert_eq!(beta_normalize(&redex), lit(55));
1161    }
1162    #[test]
1163    fn test_mk_compose_applies() {
1164        let id1 = mk_identity(nat());
1165        let id2 = mk_identity(nat());
1166        let composed = mk_compose(id1, id2, nat());
1167        let app = Expr::App(Box::new(composed), Box::new(lit(5)));
1168        assert_eq!(beta_normalize(&app), lit(5));
1169    }
1170}
1171#[cfg(test)]
1172mod tests_padding_infra {
1173    use super::*;
1174    #[test]
1175    fn test_stat_summary() {
1176        let mut ss = StatSummary::new();
1177        ss.record(10.0);
1178        ss.record(20.0);
1179        ss.record(30.0);
1180        assert_eq!(ss.count(), 3);
1181        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
1182        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
1183        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
1184    }
1185    #[test]
1186    fn test_transform_stat() {
1187        let mut ts = TransformStat::new();
1188        ts.record_before(100.0);
1189        ts.record_after(80.0);
1190        let ratio = ts.mean_ratio().expect("ratio should be present");
1191        assert!((ratio - 0.8).abs() < 1e-9);
1192    }
1193    #[test]
1194    fn test_small_map() {
1195        let mut m: SmallMap<u32, &str> = SmallMap::new();
1196        m.insert(3, "three");
1197        m.insert(1, "one");
1198        m.insert(2, "two");
1199        assert_eq!(m.get(&2), Some(&"two"));
1200        assert_eq!(m.len(), 3);
1201        let keys = m.keys();
1202        assert_eq!(*keys[0], 1);
1203        assert_eq!(*keys[2], 3);
1204    }
1205    #[test]
1206    fn test_label_set() {
1207        let mut ls = LabelSet::new();
1208        ls.add("foo");
1209        ls.add("bar");
1210        ls.add("foo");
1211        assert_eq!(ls.count(), 2);
1212        assert!(ls.has("bar"));
1213        assert!(!ls.has("baz"));
1214    }
1215    #[test]
1216    fn test_config_node() {
1217        let mut root = ConfigNode::section("root");
1218        let child = ConfigNode::leaf("key", "value");
1219        root.add_child(child);
1220        assert_eq!(root.num_children(), 1);
1221    }
1222    #[test]
1223    fn test_versioned_record() {
1224        let mut vr = VersionedRecord::new(0u32);
1225        vr.update(1);
1226        vr.update(2);
1227        assert_eq!(*vr.current(), 2);
1228        assert_eq!(vr.version(), 2);
1229        assert!(vr.has_history());
1230        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
1231    }
1232    #[test]
1233    fn test_simple_dag() {
1234        let mut dag = SimpleDag::new(4);
1235        dag.add_edge(0, 1);
1236        dag.add_edge(1, 2);
1237        dag.add_edge(2, 3);
1238        assert!(dag.can_reach(0, 3));
1239        assert!(!dag.can_reach(3, 0));
1240        let order = dag.topological_sort().expect("order should be present");
1241        assert_eq!(order, vec![0, 1, 2, 3]);
1242    }
1243    #[test]
1244    fn test_focus_stack() {
1245        let mut fs: FocusStack<&str> = FocusStack::new();
1246        fs.focus("a");
1247        fs.focus("b");
1248        assert_eq!(fs.current(), Some(&"b"));
1249        assert_eq!(fs.depth(), 2);
1250        fs.blur();
1251        assert_eq!(fs.current(), Some(&"a"));
1252    }
1253}
1254#[cfg(test)]
1255mod tests_extra_iterators {
1256    use super::*;
1257    #[test]
1258    fn test_window_iterator() {
1259        let data = vec![1u32, 2, 3, 4, 5];
1260        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
1261        assert_eq!(windows.len(), 3);
1262        assert_eq!(windows[0], &[1, 2, 3]);
1263        assert_eq!(windows[2], &[3, 4, 5]);
1264    }
1265    #[test]
1266    fn test_non_empty_vec() {
1267        let mut nev = NonEmptyVec::singleton(10u32);
1268        nev.push(20);
1269        nev.push(30);
1270        assert_eq!(nev.len(), 3);
1271        assert_eq!(*nev.first(), 10);
1272        assert_eq!(*nev.last(), 30);
1273    }
1274}
1275#[cfg(test)]
1276mod tests_padding2 {
1277    use super::*;
1278    #[test]
1279    fn test_sliding_sum() {
1280        let mut ss = SlidingSum::new(3);
1281        ss.push(1.0);
1282        ss.push(2.0);
1283        ss.push(3.0);
1284        assert!((ss.sum() - 6.0).abs() < 1e-9);
1285        ss.push(4.0);
1286        assert!((ss.sum() - 9.0).abs() < 1e-9);
1287        assert_eq!(ss.count(), 3);
1288    }
1289    #[test]
1290    fn test_path_buf() {
1291        let mut pb = PathBuf::new();
1292        pb.push("src");
1293        pb.push("main");
1294        assert_eq!(pb.as_str(), "src/main");
1295        assert_eq!(pb.depth(), 2);
1296        pb.pop();
1297        assert_eq!(pb.as_str(), "src");
1298    }
1299    #[test]
1300    fn test_string_pool() {
1301        let mut pool = StringPool::new();
1302        let s = pool.take();
1303        assert!(s.is_empty());
1304        pool.give("hello".to_string());
1305        let s2 = pool.take();
1306        assert!(s2.is_empty());
1307        assert_eq!(pool.free_count(), 0);
1308    }
1309    #[test]
1310    fn test_transitive_closure() {
1311        let mut tc = TransitiveClosure::new(4);
1312        tc.add_edge(0, 1);
1313        tc.add_edge(1, 2);
1314        tc.add_edge(2, 3);
1315        assert!(tc.can_reach(0, 3));
1316        assert!(!tc.can_reach(3, 0));
1317        let r = tc.reachable_from(0);
1318        assert_eq!(r.len(), 4);
1319    }
1320    #[test]
1321    fn test_token_bucket() {
1322        let mut tb = TokenBucket::new(100, 10);
1323        assert_eq!(tb.available(), 100);
1324        assert!(tb.try_consume(50));
1325        assert_eq!(tb.available(), 50);
1326        assert!(!tb.try_consume(60));
1327        assert_eq!(tb.capacity(), 100);
1328    }
1329    #[test]
1330    fn test_rewrite_rule_set() {
1331        let mut rrs = RewriteRuleSet::new();
1332        rrs.add(RewriteRule::unconditional(
1333            "beta",
1334            "App(Lam(x, b), v)",
1335            "b[x:=v]",
1336        ));
1337        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
1338        assert_eq!(rrs.len(), 2);
1339        assert_eq!(rrs.unconditional_rules().len(), 1);
1340        assert_eq!(rrs.conditional_rules().len(), 1);
1341        assert!(rrs.get("beta").is_some());
1342        let disp = rrs
1343            .get("beta")
1344            .expect("element at \'beta\' should exist")
1345            .display();
1346        assert!(disp.contains("→"));
1347    }
1348}
1349#[cfg(test)]
1350mod tests_padding3 {
1351    use super::*;
1352    #[test]
1353    fn test_decision_node() {
1354        let tree = DecisionNode::Branch {
1355            key: "x".into(),
1356            val: "1".into(),
1357            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
1358            no_branch: Box::new(DecisionNode::Leaf("no".into())),
1359        };
1360        let mut ctx = std::collections::HashMap::new();
1361        ctx.insert("x".into(), "1".into());
1362        assert_eq!(tree.evaluate(&ctx), "yes");
1363        ctx.insert("x".into(), "2".into());
1364        assert_eq!(tree.evaluate(&ctx), "no");
1365        assert_eq!(tree.depth(), 1);
1366    }
1367    #[test]
1368    fn test_flat_substitution() {
1369        let mut sub = FlatSubstitution::new();
1370        sub.add("foo", "bar");
1371        sub.add("baz", "qux");
1372        assert_eq!(sub.apply("foo and baz"), "bar and qux");
1373        assert_eq!(sub.len(), 2);
1374    }
1375    #[test]
1376    fn test_stopwatch() {
1377        let mut sw = Stopwatch::start();
1378        sw.split();
1379        sw.split();
1380        assert_eq!(sw.num_splits(), 2);
1381        assert!(sw.elapsed_ms() >= 0.0);
1382        for &s in sw.splits() {
1383            assert!(s >= 0.0);
1384        }
1385    }
1386    #[test]
1387    fn test_either2() {
1388        let e: Either2<i32, &str> = Either2::First(42);
1389        assert!(e.is_first());
1390        let mapped = e.map_first(|x| x * 2);
1391        assert_eq!(mapped.first(), Some(84));
1392        let e2: Either2<i32, &str> = Either2::Second("hello");
1393        assert!(e2.is_second());
1394        assert_eq!(e2.second(), Some("hello"));
1395    }
1396    #[test]
1397    fn test_write_once() {
1398        let wo: WriteOnce<u32> = WriteOnce::new();
1399        assert!(!wo.is_written());
1400        assert!(wo.write(42));
1401        assert!(!wo.write(99));
1402        assert_eq!(wo.read(), Some(42));
1403    }
1404    #[test]
1405    fn test_sparse_vec() {
1406        let mut sv: SparseVec<i32> = SparseVec::new(100);
1407        sv.set(5, 10);
1408        sv.set(50, 20);
1409        assert_eq!(*sv.get(5), 10);
1410        assert_eq!(*sv.get(50), 20);
1411        assert_eq!(*sv.get(0), 0);
1412        assert_eq!(sv.nnz(), 2);
1413        sv.set(5, 0);
1414        assert_eq!(sv.nnz(), 1);
1415    }
1416    #[test]
1417    fn test_stack_calc() {
1418        let mut calc = StackCalc::new();
1419        calc.push(3);
1420        calc.push(4);
1421        calc.add();
1422        assert_eq!(calc.peek(), Some(7));
1423        calc.push(2);
1424        calc.mul();
1425        assert_eq!(calc.peek(), Some(14));
1426    }
1427}
oxilean_kernel/beta/functions.rs

oxilean_kernel/beta/
functions.rs
