oxilean_kernel/beta/
functions.rs

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

oxilean_kernel/beta/
functions.rs
