oxilean_kernel/whnf/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::{BinderInfo, Environment, Expr, FVarId, Level, Literal, Name, Reducer};
6
7use super::types::{
8    ConfigNode, DecisionNode, Either2, Fixture, FlatSubstitution, FocusStack, LabelSet, MinHeap,
9    NonEmptyVec, PathBuf, PrefixCounter, ReductionBudget, RewriteRule, RewriteRuleSet, SimpleDag,
10    SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch, StringPool, StuckReason,
11    TokenBucket, TransformStat, TransitiveClosure, VersionedRecord, WhnfCache, WhnfCacheKey,
12    WhnfConfig, WhnfDepthBudget, WhnfHead, WhnfReductionOrder, WhnfStats, WindowIterator,
13    WriteOnce,
14};
15
16/// Reduce an expression to Weak Head Normal Form using the default reducer.
17pub fn whnf(expr: &Expr) -> Expr {
18    let mut reducer = Reducer::new();
19    reducer.whnf(expr)
20}
21/// Reduce an expression to WHNF in the context of an Environment.
22pub fn whnf_env(expr: &Expr, env: &Environment) -> Expr {
23    let mut reducer = Reducer::new();
24    reducer.whnf_env(expr, env)
25}
26/// Check whether an expression is already in Weak Head Normal Form.
27pub fn is_whnf(expr: &Expr) -> bool {
28    match expr {
29        Expr::Sort(_) | Expr::BVar(_) | Expr::FVar(_) | Expr::Const(_, _) | Expr::Lit(_) => true,
30        Expr::Lam(_, _, _, _) | Expr::Pi(_, _, _, _) => true,
31        Expr::App(f, _) => !matches!(f.as_ref(), Expr::Lam(_, _, _, _)),
32        Expr::Let(_, _, _, _) => false,
33        _ => true,
34    }
35}
36/// Check whether the WHNF of an expression is a Sort.
37pub fn whnf_is_sort(expr: &Expr) -> bool {
38    matches!(whnf(expr), Expr::Sort(_))
39}
40/// Check whether the WHNF of an expression is a Pi type.
41pub fn whnf_is_pi(expr: &Expr) -> bool {
42    matches!(whnf(expr), Expr::Pi(_, _, _, _))
43}
44/// Check whether the WHNF of an expression is a lambda abstraction.
45pub fn whnf_is_lambda(expr: &Expr) -> bool {
46    matches!(whnf(expr), Expr::Lam(_, _, _, _))
47}
48/// Check whether the WHNF of an expression is a named constant.
49pub fn whnf_is_const(expr: &Expr) -> Option<Name> {
50    match whnf(expr) {
51        Expr::Const(n, _) => Some(n),
52        _ => None,
53    }
54}
55/// Check whether the WHNF of an expression is a literal.
56pub fn whnf_is_lit(expr: &Expr) -> Option<Literal> {
57    match whnf(expr) {
58        Expr::Lit(l) => Some(l),
59        _ => None,
60    }
61}
62/// Decompose an expression (after WHNF) into its head and spine arguments.
63pub fn whnf_spine(expr: &Expr) -> (WhnfHead, Vec<Expr>) {
64    let reduced = whnf(expr);
65    spine_of(&reduced)
66}
67/// Decompose an already-reduced expression into head and arguments.
68pub fn spine_of(expr: &Expr) -> (WhnfHead, Vec<Expr>) {
69    let mut args = Vec::new();
70    let mut current = expr.clone();
71    loop {
72        match current {
73            Expr::App(f, a) => {
74                args.push(*a);
75                current = *f;
76            }
77            other => {
78                args.reverse();
79                let head = match other {
80                    Expr::Sort(l) => WhnfHead::Sort(l),
81                    Expr::BVar(i) => WhnfHead::BVar(i),
82                    Expr::FVar(id) => WhnfHead::FVar(id),
83                    Expr::Const(n, ls) => WhnfHead::Const(n, ls),
84                    Expr::Lam(bi, n, ty, body) => WhnfHead::Lam(bi, n, ty, body),
85                    Expr::Pi(bi, n, ty, body) => WhnfHead::Pi(bi, n, ty, body),
86                    Expr::Lit(l) => WhnfHead::Lit(l),
87                    Expr::App(_, _) | Expr::Let(_, _, _, _) => unreachable!(),
88                    _ => WhnfHead::BVar(0),
89                };
90                return (head, args);
91            }
92        }
93    }
94}
95/// Decompose with WHNF in environment.
96pub fn whnf_spine_env(expr: &Expr, env: &Environment) -> (WhnfHead, Vec<Expr>) {
97    let reduced = whnf_env(expr, env);
98    spine_of(&reduced)
99}
100/// Reduce with a step budget. Returns None if the budget is exhausted.
101pub fn whnf_budgeted(expr: &Expr, budget: &mut ReductionBudget) -> Option<Expr> {
102    if !budget.consume() {
103        return None;
104    }
105    Some(whnf(expr))
106}
107/// Compare the WHNF heads of two expressions for structural equality.
108pub fn whnf_heads_match(a: &Expr, b: &Expr) -> bool {
109    let (ha, _) = whnf_spine(a);
110    let (hb, _) = whnf_spine(b);
111    match (&ha, &hb) {
112        (WhnfHead::Sort(la), WhnfHead::Sort(lb)) => la == lb,
113        (WhnfHead::BVar(i), WhnfHead::BVar(j)) => i == j,
114        (WhnfHead::FVar(i), WhnfHead::FVar(j)) => i == j,
115        (WhnfHead::Const(na, _), WhnfHead::Const(nb, _)) => na == nb,
116        (WhnfHead::Lit(la), WhnfHead::Lit(lb)) => la == lb,
117        _ => false,
118    }
119}
120/// Count the number of arguments in an application spine.
121pub fn app_arity(expr: &Expr) -> usize {
122    let (_, args) = spine_of(expr);
123    args.len()
124}
125/// Destructure a Pi type after WHNF reduction.
126pub fn whnf_as_pi(expr: &Expr) -> Option<(BinderInfo, Name, Expr, Expr)> {
127    match whnf(expr) {
128        Expr::Pi(bi, name, dom, cod) => Some((bi, name, *dom, *cod)),
129        _ => None,
130    }
131}
132/// Destructure a Pi type after WHNF reduction with environment.
133pub fn whnf_as_pi_env(expr: &Expr, env: &Environment) -> Option<(BinderInfo, Name, Expr, Expr)> {
134    match whnf_env(expr, env) {
135        Expr::Pi(bi, name, dom, cod) => Some((bi, name, *dom, *cod)),
136        _ => None,
137    }
138}
139/// Extract the universe level from a WHNF Sort expression.
140pub fn whnf_as_sort(expr: &Expr) -> Option<Level> {
141    match whnf(expr) {
142        Expr::Sort(l) => Some(l),
143        _ => None,
144    }
145}
146/// Collect the full Pi telescope (sequence of binders) from a type.
147pub fn collect_pi_telescope(ty: &Expr) -> (Vec<(BinderInfo, Name, Expr)>, Expr) {
148    let mut binders = Vec::new();
149    let mut current = ty.clone();
150    loop {
151        match whnf(&current) {
152            Expr::Pi(bi, name, dom, body) => {
153                binders.push((bi, name, *dom));
154                current = *body;
155            }
156            other => return (binders, other),
157        }
158    }
159}
160/// Collect the full Pi telescope using an environment for delta unfolding.
161pub fn collect_pi_telescope_env(
162    ty: &Expr,
163    env: &Environment,
164) -> (Vec<(BinderInfo, Name, Expr)>, Expr) {
165    let mut binders = Vec::new();
166    let mut current = ty.clone();
167    loop {
168        match whnf_env(&current, env) {
169            Expr::Pi(bi, name, dom, body) => {
170                binders.push((bi, name, *dom));
171                current = *body;
172            }
173            other => return (binders, other),
174        }
175    }
176}
177/// Determine why a WHNF expression is stuck.
178pub fn stuck_reason(expr: &Expr) -> StuckReason {
179    match whnf(expr) {
180        Expr::FVar(id) => StuckReason::FreeVariable(id),
181        Expr::Const(n, _) => StuckReason::OpaqueConst(n),
182        _ => StuckReason::NormalForm,
183    }
184}
185#[cfg(test)]
186mod tests {
187    use super::*;
188    use crate::Level;
189    fn sort0() -> Expr {
190        Expr::Sort(Level::zero())
191    }
192    fn sort1() -> Expr {
193        Expr::Sort(Level::succ(Level::zero()))
194    }
195    fn identity_lam() -> Expr {
196        Expr::Lam(
197            BinderInfo::Default,
198            Name::str("x"),
199            Box::new(sort0()),
200            Box::new(Expr::BVar(0)),
201        )
202    }
203    #[test]
204    fn test_is_whnf_sort() {
205        assert!(is_whnf(&sort0()));
206        assert!(is_whnf(&sort1()));
207    }
208    #[test]
209    fn test_is_whnf_bvar() {
210        assert!(is_whnf(&Expr::BVar(0)));
211        assert!(is_whnf(&Expr::BVar(5)));
212    }
213    #[test]
214    fn test_is_whnf_lit() {
215        assert!(is_whnf(&Expr::Lit(Literal::Nat(42))));
216        assert!(is_whnf(&Expr::Lit(Literal::Str("hello".into()))));
217    }
218    #[test]
219    fn test_is_whnf_lam() {
220        assert!(is_whnf(&identity_lam()));
221    }
222    #[test]
223    fn test_is_whnf_let_false() {
224        let e = Expr::Let(
225            Name::str("x"),
226            Box::new(sort0()),
227            Box::new(Expr::Lit(Literal::Nat(1))),
228            Box::new(Expr::BVar(0)),
229        );
230        assert!(!is_whnf(&e));
231    }
232    #[test]
233    fn test_is_whnf_app_lambda_false() {
234        let app = Expr::App(
235            Box::new(identity_lam()),
236            Box::new(Expr::Lit(Literal::Nat(1))),
237        );
238        assert!(!is_whnf(&app));
239    }
240    #[test]
241    fn test_whnf_beta_reduce() {
242        let arg = Expr::Lit(Literal::Nat(99));
243        let app = Expr::App(Box::new(identity_lam()), Box::new(arg.clone()));
244        let result = whnf(&app);
245        assert_eq!(result, arg);
246    }
247    #[test]
248    fn test_whnf_is_sort_true() {
249        assert!(whnf_is_sort(&sort0()));
250    }
251    #[test]
252    fn test_whnf_is_sort_false() {
253        assert!(!whnf_is_sort(&identity_lam()));
254    }
255    #[test]
256    fn test_whnf_is_pi() {
257        let pi = Expr::Pi(
258            BinderInfo::Default,
259            Name::str("x"),
260            Box::new(sort0()),
261            Box::new(sort0()),
262        );
263        assert!(whnf_is_pi(&pi));
264    }
265    #[test]
266    fn test_whnf_is_lambda() {
267        assert!(whnf_is_lambda(&identity_lam()));
268    }
269    #[test]
270    fn test_whnf_is_const() {
271        let c = Expr::Const(Name::str("Nat"), vec![]);
272        assert_eq!(whnf_is_const(&c), Some(Name::str("Nat")));
273    }
274    #[test]
275    fn test_whnf_is_lit() {
276        let l = Expr::Lit(Literal::Nat(7));
277        assert_eq!(whnf_is_lit(&l), Some(Literal::Nat(7)));
278    }
279    #[test]
280    fn test_spine_of_no_args() {
281        let c = Expr::Const(Name::str("Nat"), vec![]);
282        let (head, args) = spine_of(&c);
283        assert_eq!(head.as_const_name(), Some(&Name::str("Nat")));
284        assert!(args.is_empty());
285    }
286    #[test]
287    fn test_spine_of_two_args() {
288        let f = Expr::Const(Name::str("f"), vec![]);
289        let a = Expr::Lit(Literal::Nat(1));
290        let b = Expr::Lit(Literal::Nat(2));
291        let app = Expr::App(
292            Box::new(Expr::App(Box::new(f), Box::new(a.clone()))),
293            Box::new(b.clone()),
294        );
295        let (_, args) = spine_of(&app);
296        assert_eq!(args.len(), 2);
297        assert_eq!(args[0], a);
298        assert_eq!(args[1], b);
299    }
300    #[test]
301    fn test_collect_pi_telescope_empty() {
302        let (binders, body) = collect_pi_telescope(&sort0());
303        assert!(binders.is_empty());
304        assert_eq!(body, sort0());
305    }
306    #[test]
307    fn test_collect_pi_telescope_one() {
308        let pi = Expr::Pi(
309            BinderInfo::Default,
310            Name::str("x"),
311            Box::new(sort0()),
312            Box::new(sort1()),
313        );
314        let (binders, body) = collect_pi_telescope(&pi);
315        assert_eq!(binders.len(), 1);
316        assert_eq!(binders[0].1, Name::str("x"));
317        assert_eq!(body, sort1());
318    }
319    #[test]
320    fn test_collect_pi_telescope_nested() {
321        let pi_inner = Expr::Pi(
322            BinderInfo::Default,
323            Name::str("y"),
324            Box::new(sort0()),
325            Box::new(sort1()),
326        );
327        let pi_outer = Expr::Pi(
328            BinderInfo::Default,
329            Name::str("x"),
330            Box::new(sort0()),
331            Box::new(pi_inner),
332        );
333        let (binders, _body) = collect_pi_telescope(&pi_outer);
334        assert_eq!(binders.len(), 2);
335        assert_eq!(binders[0].1, Name::str("x"));
336        assert_eq!(binders[1].1, Name::str("y"));
337    }
338    #[test]
339    fn test_reduction_budget_basic() {
340        let mut budget = ReductionBudget::new(3);
341        assert!(budget.consume());
342        assert!(budget.consume());
343        assert!(budget.consume());
344        assert!(!budget.consume());
345    }
346    #[test]
347    fn test_reduction_budget_unlimited() {
348        let mut budget = ReductionBudget::unlimited();
349        for _ in 0..1000 {
350            assert!(budget.consume());
351        }
352    }
353    #[test]
354    fn test_whnf_stats_default() {
355        let stats = WhnfStats::new();
356        assert_eq!(stats.total_steps(), 0);
357        assert!(!stats.any_progress());
358    }
359    #[test]
360    fn test_whnf_stats_total() {
361        let stats = WhnfStats {
362            beta_steps: 3,
363            delta_steps: 2,
364            zeta_steps: 1,
365            iota_steps: 4,
366            total_exprs: 10,
367        };
368        assert_eq!(stats.total_steps(), 10);
369        assert!(stats.any_progress());
370    }
371    #[test]
372    fn test_whnf_cache_key() {
373        let e1 = sort0();
374        let e2 = sort0();
375        let k1 = WhnfCacheKey::from_expr(&e1);
376        let k2 = WhnfCacheKey::from_expr(&e2);
377        assert_eq!(k1, k2);
378    }
379    #[test]
380    fn test_stuck_reason_normal_form() {
381        assert_eq!(stuck_reason(&sort0()), StuckReason::NormalForm);
382    }
383    #[test]
384    fn test_stuck_reason_free_var() {
385        let fv = Expr::FVar(FVarId::new(42));
386        assert_eq!(
387            stuck_reason(&fv),
388            StuckReason::FreeVariable(FVarId::new(42))
389        );
390    }
391    #[test]
392    fn test_app_arity() {
393        let f = Expr::Const(Name::str("f"), vec![]);
394        let a = Expr::Lit(Literal::Nat(1));
395        let b = Expr::Lit(Literal::Nat(2));
396        let app = Expr::App(Box::new(Expr::App(Box::new(f), Box::new(a))), Box::new(b));
397        assert_eq!(app_arity(&app), 2);
398    }
399    #[test]
400    fn test_whnf_as_pi() {
401        let pi = Expr::Pi(
402            BinderInfo::Default,
403            Name::str("x"),
404            Box::new(sort0()),
405            Box::new(sort1()),
406        );
407        let result = whnf_as_pi(&pi);
408        assert!(result.is_some());
409        let (bi, name, dom, cod) = result.expect("result should be valid");
410        assert_eq!(bi, BinderInfo::Default);
411        assert_eq!(name, Name::str("x"));
412        assert_eq!(dom, sort0());
413        assert_eq!(cod, sort1());
414    }
415    #[test]
416    fn test_whnf_as_sort() {
417        assert_eq!(whnf_as_sort(&sort0()), Some(Level::zero()));
418        assert_eq!(whnf_as_sort(&identity_lam()), None);
419    }
420    #[test]
421    fn test_whnf_heads_match_sorts() {
422        assert!(whnf_heads_match(&sort0(), &sort0()));
423        assert!(!whnf_heads_match(&sort0(), &sort1()));
424    }
425    #[test]
426    fn test_whnf_heads_match_const() {
427        let c1 = Expr::Const(Name::str("Nat"), vec![]);
428        let c2 = Expr::Const(Name::str("Nat"), vec![]);
429        let c3 = Expr::Const(Name::str("Int"), vec![]);
430        assert!(whnf_heads_match(&c1, &c2));
431        assert!(!whnf_heads_match(&c1, &c3));
432    }
433    #[test]
434    fn test_whnf_head_to_expr() {
435        let head = WhnfHead::Sort(Level::zero());
436        assert_eq!(head.to_expr(), sort0());
437    }
438    #[test]
439    fn test_whnf_budgeted_success() {
440        let mut budget = ReductionBudget::new(10);
441        let result = whnf_budgeted(&sort0(), &mut budget);
442        assert!(result.is_some());
443        assert_eq!(result.expect("result should be valid"), sort0());
444    }
445    #[test]
446    fn test_whnf_budgeted_exhausted() {
447        let mut budget = ReductionBudget::new(0);
448        let result = whnf_budgeted(&sort0(), &mut budget);
449        assert!(result.is_none());
450    }
451}
452/// Fully normalize an expression by repeatedly applying WHNF
453/// and then recursively normalizing all subexpressions.
454///
455/// Warning: may not terminate for non-normalizing terms.
456#[allow(dead_code)]
457pub fn normalize_full(expr: &Expr) -> Expr {
458    let w = whnf(expr);
459    match w {
460        Expr::App(f, a) => {
461            let nf = normalize_full(&f);
462            let na = normalize_full(&a);
463            Expr::App(Box::new(nf), Box::new(na))
464        }
465        Expr::Lam(bi, name, ty, body) => {
466            let nty = normalize_full(&ty);
467            let nbody = normalize_full(&body);
468            Expr::Lam(bi, name, Box::new(nty), Box::new(nbody))
469        }
470        Expr::Pi(bi, name, ty, body) => {
471            let nty = normalize_full(&ty);
472            let nbody = normalize_full(&body);
473            Expr::Pi(bi, name, Box::new(nty), Box::new(nbody))
474        }
475        Expr::Let(name, ty, val, body) => {
476            let nty = normalize_full(&ty);
477            let nval = normalize_full(&val);
478            let nbody = normalize_full(&body);
479            Expr::Let(name, Box::new(nty), Box::new(nval), Box::new(nbody))
480        }
481        other => other,
482    }
483}
484/// Normalize just the head of an expression, without recursing into subexpressions.
485#[allow(dead_code)]
486pub fn normalize_head(expr: &Expr) -> Expr {
487    whnf(expr)
488}
489/// Check whether a WHNF expression's head is a given constant.
490#[allow(dead_code)]
491pub fn whnf_head_is_const(expr: &Expr, name: &Name) -> bool {
492    match whnf(expr) {
493        Expr::Const(n, _) => n == *name,
494        Expr::App(f, _) => whnf_head_is_const(&f, name),
495        _ => false,
496    }
497}
498/// Check whether a WHNF expression is a free variable.
499#[allow(dead_code)]
500pub fn whnf_is_fvar(expr: &Expr) -> bool {
501    matches!(whnf(expr), Expr::FVar(_))
502}
503/// Extract the FVarId from a WHNF expression if it is a free variable.
504#[allow(dead_code)]
505pub fn whnf_as_fvar(expr: &Expr) -> Option<FVarId> {
506    match whnf(expr) {
507        Expr::FVar(id) => Some(id),
508        _ => None,
509    }
510}
511#[cfg(test)]
512mod extra_whnf_tests {
513    use super::*;
514    #[test]
515    fn test_normalize_full_sort() {
516        let e = Expr::Sort(Level::zero());
517        assert_eq!(normalize_full(&e), e);
518    }
519    #[test]
520    fn test_normalize_full_beta() {
521        let lam = Expr::Lam(
522            BinderInfo::Default,
523            Name::str("x"),
524            Box::new(Expr::Sort(Level::zero())),
525            Box::new(Expr::BVar(0)),
526        );
527        let arg = Expr::Lit(Literal::Nat(7));
528        let app = Expr::App(Box::new(lam), Box::new(arg.clone()));
529        let result = normalize_full(&app);
530        assert_eq!(result, arg);
531    }
532    #[test]
533    fn test_normalize_full_lam() {
534        let e = Expr::Lam(
535            BinderInfo::Default,
536            Name::str("x"),
537            Box::new(Expr::Sort(Level::zero())),
538            Box::new(Expr::BVar(0)),
539        );
540        let result = normalize_full(&e);
541        assert!(matches!(result, Expr::Lam(_, _, _, _)));
542    }
543    #[test]
544    fn test_normalize_head_sort() {
545        let e = Expr::Sort(Level::zero());
546        assert_eq!(normalize_head(&e), e);
547    }
548    #[test]
549    fn test_whnf_head_is_const_direct() {
550        let c = Expr::Const(Name::str("Nat"), vec![]);
551        assert!(whnf_head_is_const(&c, &Name::str("Nat")));
552        assert!(!whnf_head_is_const(&c, &Name::str("Bool")));
553    }
554    #[test]
555    fn test_whnf_is_fvar_true() {
556        let fv = Expr::FVar(FVarId::new(0));
557        assert!(whnf_is_fvar(&fv));
558    }
559    #[test]
560    fn test_whnf_is_fvar_false() {
561        let c = Expr::Const(Name::str("Nat"), vec![]);
562        assert!(!whnf_is_fvar(&c));
563    }
564    #[test]
565    fn test_whnf_as_fvar_some() {
566        let id = FVarId::new(42);
567        let fv = Expr::FVar(id);
568        assert_eq!(whnf_as_fvar(&fv), Some(id));
569    }
570    #[test]
571    fn test_whnf_as_fvar_none() {
572        let e = Expr::Sort(Level::zero());
573        assert_eq!(whnf_as_fvar(&e), None);
574    }
575    #[test]
576    fn test_whnf_depth_budget_consumed() {
577        let mut b = WhnfDepthBudget::new(5);
578        for _ in 0..5 {
579            assert!(b.consume());
580        }
581        assert!(b.is_exhausted());
582        assert!(!b.consume());
583    }
584    #[test]
585    fn test_whnf_depth_budget_consumed_count() {
586        let mut b = WhnfDepthBudget::new(10);
587        b.consume();
588        b.consume();
589        b.consume();
590        assert_eq!(b.consumed(), 3);
591    }
592    #[test]
593    fn test_whnf_depth_budget_reset() {
594        let mut b = WhnfDepthBudget::new(3);
595        b.consume();
596        b.consume();
597        b.reset();
598        assert_eq!(b.consumed(), 0);
599    }
600    #[test]
601    fn test_reduction_order_display() {
602        assert_eq!(format!("{}", WhnfReductionOrder::BetaFirst), "beta-first");
603        assert_eq!(format!("{}", WhnfReductionOrder::DeltaFirst), "delta-first");
604        assert_eq!(
605            format!("{}", WhnfReductionOrder::StructuralOnly),
606            "structural-only"
607        );
608    }
609}
610/// Count the total number of nodes (subexpressions) in an expression.
611///
612/// Useful for estimating the size of a proof term or type.
613#[allow(dead_code)]
614pub fn count_nodes(expr: &Expr) -> usize {
615    match expr {
616        Expr::BVar(_) | Expr::FVar(_) | Expr::Sort(_) | Expr::Lit(_) => 1,
617        Expr::Const(_, levels) => 1 + levels.len(),
618        Expr::App(f, a) => 1 + count_nodes(f) + count_nodes(a),
619        Expr::Lam(_, _, ty, body) => 1 + count_nodes(ty) + count_nodes(body),
620        Expr::Pi(_, _, ty, body) => 1 + count_nodes(ty) + count_nodes(body),
621        Expr::Let(_, ty, val, body) => 1 + count_nodes(ty) + count_nodes(val) + count_nodes(body),
622        _ => 1,
623    }
624}
625/// Compute the depth (maximum nesting) of an expression tree.
626#[allow(dead_code)]
627pub fn expr_depth(expr: &Expr) -> usize {
628    match expr {
629        Expr::BVar(_) | Expr::FVar(_) | Expr::Sort(_) | Expr::Lit(_) | Expr::Const(_, _) => 1,
630        Expr::App(f, a) => 1 + count_nodes(f).max(count_nodes(a)),
631        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
632            1 + expr_depth(ty).max(expr_depth(body))
633        }
634        Expr::Let(_, ty, val, body) => {
635            1 + expr_depth(ty).max(expr_depth(val)).max(expr_depth(body))
636        }
637        _ => 1,
638    }
639}
640#[cfg(test)]
641mod whnf_cache_tests {
642    use super::*;
643    #[test]
644    fn test_whnf_cache_empty() {
645        let cache = WhnfCache::new(10);
646        assert!(cache.is_empty());
647        assert_eq!(cache.len(), 0);
648    }
649    #[test]
650    fn test_whnf_cache_insert_get() {
651        let mut cache = WhnfCache::new(10);
652        let key = WhnfCacheKey { expr_hash: 42 };
653        let expr = Expr::Sort(Level::zero());
654        cache.insert(key.clone(), expr.clone());
655        assert_eq!(cache.len(), 1);
656        let result = cache.get(&key);
657        assert!(result.is_some());
658        assert_eq!(*result.expect("result should be valid"), expr);
659    }
660    #[test]
661    fn test_whnf_cache_miss() {
662        let mut cache = WhnfCache::new(10);
663        let key = WhnfCacheKey { expr_hash: 99 };
664        let result = cache.get(&key);
665        assert!(result.is_none());
666        assert_eq!(cache.misses(), 1);
667    }
668    #[test]
669    fn test_whnf_cache_hit_rate() {
670        let mut cache = WhnfCache::new(10);
671        let key = WhnfCacheKey { expr_hash: 1 };
672        cache.insert(key.clone(), Expr::Sort(Level::zero()));
673        cache.get(&key);
674        cache.get(&WhnfCacheKey { expr_hash: 999 });
675        assert!((cache.hit_rate() - 0.5).abs() < 1e-10);
676    }
677    #[test]
678    fn test_whnf_cache_capacity_eviction() {
679        let mut cache = WhnfCache::new(2);
680        let e = Expr::Sort(Level::zero());
681        cache.insert(WhnfCacheKey { expr_hash: 1 }, e.clone());
682        cache.insert(WhnfCacheKey { expr_hash: 2 }, e.clone());
683        cache.insert(WhnfCacheKey { expr_hash: 3 }, e.clone());
684        assert_eq!(cache.len(), 2);
685    }
686    #[test]
687    fn test_whnf_cache_clear() {
688        let mut cache = WhnfCache::new(10);
689        cache.insert(WhnfCacheKey { expr_hash: 1 }, Expr::Sort(Level::zero()));
690        cache.clear();
691        assert!(cache.is_empty());
692    }
693    #[test]
694    fn test_whnf_config_default() {
695        let cfg = WhnfConfig::default();
696        assert!(cfg.beta);
697        assert!(cfg.delta);
698        assert!(cfg.any_enabled());
699    }
700    #[test]
701    fn test_whnf_config_structural() {
702        let cfg = WhnfConfig::structural();
703        assert!(!cfg.delta);
704        assert!(cfg.beta);
705    }
706    #[test]
707    fn test_whnf_config_no_delta() {
708        let cfg = WhnfConfig::default().no_delta();
709        assert!(!cfg.delta);
710    }
711    #[test]
712    fn test_whnf_config_no_beta() {
713        let cfg = WhnfConfig::default().no_beta();
714        assert!(!cfg.beta);
715    }
716    #[test]
717    fn test_count_nodes_sort() {
718        let e = Expr::Sort(Level::zero());
719        assert_eq!(count_nodes(&e), 1);
720    }
721    #[test]
722    fn test_count_nodes_app() {
723        let f = Expr::Const(Name::str("f"), vec![]);
724        let a = Expr::Lit(Literal::Nat(1));
725        let app = Expr::App(Box::new(f), Box::new(a));
726        assert_eq!(count_nodes(&app), 3);
727    }
728    #[test]
729    fn test_expr_depth_sort() {
730        let e = Expr::Sort(Level::zero());
731        assert_eq!(expr_depth(&e), 1);
732    }
733    #[test]
734    fn test_expr_depth_nested() {
735        let inner = Expr::Sort(Level::zero());
736        let lam = Expr::Lam(
737            BinderInfo::Default,
738            Name::str("x"),
739            Box::new(inner.clone()),
740            Box::new(inner),
741        );
742        assert!(expr_depth(&lam) >= 2);
743    }
744    #[test]
745    fn test_whnf_config_with_limit() {
746        let cfg = WhnfConfig::with_limit(100);
747        assert_eq!(cfg.max_steps, 100);
748    }
749}
750#[cfg(test)]
751mod tests_padding_infra {
752    use super::*;
753    #[test]
754    fn test_stat_summary() {
755        let mut ss = StatSummary::new();
756        ss.record(10.0);
757        ss.record(20.0);
758        ss.record(30.0);
759        assert_eq!(ss.count(), 3);
760        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
761        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
762        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
763    }
764    #[test]
765    fn test_transform_stat() {
766        let mut ts = TransformStat::new();
767        ts.record_before(100.0);
768        ts.record_after(80.0);
769        let ratio = ts.mean_ratio().expect("ratio should be present");
770        assert!((ratio - 0.8).abs() < 1e-9);
771    }
772    #[test]
773    fn test_small_map() {
774        let mut m: SmallMap<u32, &str> = SmallMap::new();
775        m.insert(3, "three");
776        m.insert(1, "one");
777        m.insert(2, "two");
778        assert_eq!(m.get(&2), Some(&"two"));
779        assert_eq!(m.len(), 3);
780        let keys = m.keys();
781        assert_eq!(*keys[0], 1);
782        assert_eq!(*keys[2], 3);
783    }
784    #[test]
785    fn test_label_set() {
786        let mut ls = LabelSet::new();
787        ls.add("foo");
788        ls.add("bar");
789        ls.add("foo");
790        assert_eq!(ls.count(), 2);
791        assert!(ls.has("bar"));
792        assert!(!ls.has("baz"));
793    }
794    #[test]
795    fn test_config_node() {
796        let mut root = ConfigNode::section("root");
797        let child = ConfigNode::leaf("key", "value");
798        root.add_child(child);
799        assert_eq!(root.num_children(), 1);
800    }
801    #[test]
802    fn test_versioned_record() {
803        let mut vr = VersionedRecord::new(0u32);
804        vr.update(1);
805        vr.update(2);
806        assert_eq!(*vr.current(), 2);
807        assert_eq!(vr.version(), 2);
808        assert!(vr.has_history());
809        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
810    }
811    #[test]
812    fn test_simple_dag() {
813        let mut dag = SimpleDag::new(4);
814        dag.add_edge(0, 1);
815        dag.add_edge(1, 2);
816        dag.add_edge(2, 3);
817        assert!(dag.can_reach(0, 3));
818        assert!(!dag.can_reach(3, 0));
819        let order = dag.topological_sort().expect("order should be present");
820        assert_eq!(order, vec![0, 1, 2, 3]);
821    }
822    #[test]
823    fn test_focus_stack() {
824        let mut fs: FocusStack<&str> = FocusStack::new();
825        fs.focus("a");
826        fs.focus("b");
827        assert_eq!(fs.current(), Some(&"b"));
828        assert_eq!(fs.depth(), 2);
829        fs.blur();
830        assert_eq!(fs.current(), Some(&"a"));
831    }
832}
833#[cfg(test)]
834mod tests_extra_iterators {
835    use super::*;
836    #[test]
837    fn test_window_iterator() {
838        let data = vec![1u32, 2, 3, 4, 5];
839        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
840        assert_eq!(windows.len(), 3);
841        assert_eq!(windows[0], &[1, 2, 3]);
842        assert_eq!(windows[2], &[3, 4, 5]);
843    }
844    #[test]
845    fn test_non_empty_vec() {
846        let mut nev = NonEmptyVec::singleton(10u32);
847        nev.push(20);
848        nev.push(30);
849        assert_eq!(nev.len(), 3);
850        assert_eq!(*nev.first(), 10);
851        assert_eq!(*nev.last(), 30);
852    }
853}
854#[cfg(test)]
855mod tests_padding2 {
856    use super::*;
857    #[test]
858    fn test_sliding_sum() {
859        let mut ss = SlidingSum::new(3);
860        ss.push(1.0);
861        ss.push(2.0);
862        ss.push(3.0);
863        assert!((ss.sum() - 6.0).abs() < 1e-9);
864        ss.push(4.0);
865        assert!((ss.sum() - 9.0).abs() < 1e-9);
866        assert_eq!(ss.count(), 3);
867    }
868    #[test]
869    fn test_path_buf() {
870        let mut pb = PathBuf::new();
871        pb.push("src");
872        pb.push("main");
873        assert_eq!(pb.as_str(), "src/main");
874        assert_eq!(pb.depth(), 2);
875        pb.pop();
876        assert_eq!(pb.as_str(), "src");
877    }
878    #[test]
879    fn test_string_pool() {
880        let mut pool = StringPool::new();
881        let s = pool.take();
882        assert!(s.is_empty());
883        pool.give("hello".to_string());
884        let s2 = pool.take();
885        assert!(s2.is_empty());
886        assert_eq!(pool.free_count(), 0);
887    }
888    #[test]
889    fn test_transitive_closure() {
890        let mut tc = TransitiveClosure::new(4);
891        tc.add_edge(0, 1);
892        tc.add_edge(1, 2);
893        tc.add_edge(2, 3);
894        assert!(tc.can_reach(0, 3));
895        assert!(!tc.can_reach(3, 0));
896        let r = tc.reachable_from(0);
897        assert_eq!(r.len(), 4);
898    }
899    #[test]
900    fn test_token_bucket() {
901        let mut tb = TokenBucket::new(100, 10);
902        assert_eq!(tb.available(), 100);
903        assert!(tb.try_consume(50));
904        assert_eq!(tb.available(), 50);
905        assert!(!tb.try_consume(60));
906        assert_eq!(tb.capacity(), 100);
907    }
908    #[test]
909    fn test_rewrite_rule_set() {
910        let mut rrs = RewriteRuleSet::new();
911        rrs.add(RewriteRule::unconditional(
912            "beta",
913            "App(Lam(x, b), v)",
914            "b[x:=v]",
915        ));
916        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
917        assert_eq!(rrs.len(), 2);
918        assert_eq!(rrs.unconditional_rules().len(), 1);
919        assert_eq!(rrs.conditional_rules().len(), 1);
920        assert!(rrs.get("beta").is_some());
921        let disp = rrs
922            .get("beta")
923            .expect("element at \'beta\' should exist")
924            .display();
925        assert!(disp.contains("→"));
926    }
927}
928#[cfg(test)]
929mod tests_padding3 {
930    use super::*;
931    #[test]
932    fn test_decision_node() {
933        let tree = DecisionNode::Branch {
934            key: "x".into(),
935            val: "1".into(),
936            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
937            no_branch: Box::new(DecisionNode::Leaf("no".into())),
938        };
939        let mut ctx = std::collections::HashMap::new();
940        ctx.insert("x".into(), "1".into());
941        assert_eq!(tree.evaluate(&ctx), "yes");
942        ctx.insert("x".into(), "2".into());
943        assert_eq!(tree.evaluate(&ctx), "no");
944        assert_eq!(tree.depth(), 1);
945    }
946    #[test]
947    fn test_flat_substitution() {
948        let mut sub = FlatSubstitution::new();
949        sub.add("foo", "bar");
950        sub.add("baz", "qux");
951        assert_eq!(sub.apply("foo and baz"), "bar and qux");
952        assert_eq!(sub.len(), 2);
953    }
954    #[test]
955    fn test_stopwatch() {
956        let mut sw = Stopwatch::start();
957        sw.split();
958        sw.split();
959        assert_eq!(sw.num_splits(), 2);
960        assert!(sw.elapsed_ms() >= 0.0);
961        for &s in sw.splits() {
962            assert!(s >= 0.0);
963        }
964    }
965    #[test]
966    fn test_either2() {
967        let e: Either2<i32, &str> = Either2::First(42);
968        assert!(e.is_first());
969        let mapped = e.map_first(|x| x * 2);
970        assert_eq!(mapped.first(), Some(84));
971        let e2: Either2<i32, &str> = Either2::Second("hello");
972        assert!(e2.is_second());
973        assert_eq!(e2.second(), Some("hello"));
974    }
975    #[test]
976    fn test_write_once() {
977        let wo: WriteOnce<u32> = WriteOnce::new();
978        assert!(!wo.is_written());
979        assert!(wo.write(42));
980        assert!(!wo.write(99));
981        assert_eq!(wo.read(), Some(42));
982    }
983    #[test]
984    fn test_sparse_vec() {
985        let mut sv: SparseVec<i32> = SparseVec::new(100);
986        sv.set(5, 10);
987        sv.set(50, 20);
988        assert_eq!(*sv.get(5), 10);
989        assert_eq!(*sv.get(50), 20);
990        assert_eq!(*sv.get(0), 0);
991        assert_eq!(sv.nnz(), 2);
992        sv.set(5, 0);
993        assert_eq!(sv.nnz(), 1);
994    }
995    #[test]
996    fn test_stack_calc() {
997        let mut calc = StackCalc::new();
998        calc.push(3);
999        calc.push(4);
1000        calc.add();
1001        assert_eq!(calc.peek(), Some(7));
1002        calc.push(2);
1003        calc.mul();
1004        assert_eq!(calc.peek(), Some(14));
1005    }
1006}
1007#[cfg(test)]
1008mod tests_final_padding {
1009    use super::*;
1010    #[test]
1011    fn test_min_heap() {
1012        let mut h = MinHeap::new();
1013        h.push(5u32);
1014        h.push(1u32);
1015        h.push(3u32);
1016        assert_eq!(h.peek(), Some(&1));
1017        assert_eq!(h.pop(), Some(1));
1018        assert_eq!(h.pop(), Some(3));
1019        assert_eq!(h.pop(), Some(5));
1020        assert!(h.is_empty());
1021    }
1022    #[test]
1023    fn test_prefix_counter() {
1024        let mut pc = PrefixCounter::new();
1025        pc.record("hello");
1026        pc.record("help");
1027        pc.record("world");
1028        assert_eq!(pc.count_with_prefix("hel"), 2);
1029        assert_eq!(pc.count_with_prefix("wor"), 1);
1030        assert_eq!(pc.count_with_prefix("xyz"), 0);
1031    }
1032    #[test]
1033    fn test_fixture() {
1034        let mut f = Fixture::new();
1035        f.set("key1", "val1");
1036        f.set("key2", "val2");
1037        assert_eq!(f.get("key1"), Some("val1"));
1038        assert_eq!(f.get("key3"), None);
1039        assert_eq!(f.len(), 2);
1040    }
1041}
oxilean_kernel/whnf/functions.rs

oxilean_kernel/whnf/
functions.rs
