oxilean_kernel/expr/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::{Level, Name};
6
7use super::types::{
8    BinderInfo, ConfigNode, DecisionNode, Either2, Expr, FVarId, FVarIdGen, Fixture,
9    FlatSubstitution, FocusStack, LabelSet, Literal, MinHeap, NonEmptyVec, PathBuf, PrefixCounter,
10    RewriteRule, RewriteRuleSet, SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc,
11    StatSummary, Stopwatch, StringPool, TokenBucket, TransformStat, TransitiveClosure,
12    VersionedRecord, WindowIterator, WriteOnce,
13};
14
15/// Check if an expression has a loose bound variable at the given level.
16///
17/// This is a helper for pretty-printing Pi types to determine if they're
18/// non-dependent arrows.
19pub(super) fn has_loose_bvar(e: &Expr, level: u32) -> bool {
20    match e {
21        Expr::BVar(n) => *n == level,
22        Expr::App(f, a) => has_loose_bvar(f, level) || has_loose_bvar(a, level),
23        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
24            has_loose_bvar(ty, level) || has_loose_bvar(body, level + 1)
25        }
26        Expr::Let(_, ty, val, body) => {
27            has_loose_bvar(ty, level)
28                || has_loose_bvar(val, level)
29                || has_loose_bvar(body, level + 1)
30        }
31        Expr::Proj(_, _, e) => has_loose_bvar(e, level),
32        _ => false,
33    }
34}
35#[cfg(test)]
36mod tests {
37    use super::*;
38    #[test]
39    fn test_expr_predicates() {
40        let prop = Expr::Sort(Level::zero());
41        let bvar = Expr::BVar(0);
42        let fvar = Expr::FVar(FVarId::new(1));
43        assert!(prop.is_sort());
44        assert!(prop.is_prop());
45        assert!(bvar.is_bvar());
46        assert!(fvar.is_fvar());
47    }
48    #[test]
49    fn test_expr_display() {
50        let prop = Expr::Sort(Level::zero());
51        let nat_const = Expr::Const(Name::str("Nat"), vec![]);
52        let app = Expr::App(
53            Box::new(nat_const.clone()),
54            Box::new(Expr::Lit(Literal::Nat(42))),
55        );
56        assert_eq!(prop.to_string(), "Prop");
57        assert_eq!(nat_const.to_string(), "Nat");
58        assert!(app.to_string().contains("Nat"));
59    }
60}
61pub(super) fn count_bvar_occ(e: &Expr, idx: u32) -> usize {
62    match e {
63        Expr::BVar(n) => {
64            if *n == idx {
65                1
66            } else {
67                0
68            }
69        }
70        Expr::App(f, a) => count_bvar_occ(f, idx) + count_bvar_occ(a, idx),
71        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
72            count_bvar_occ(ty, idx) + count_bvar_occ(body, idx + 1)
73        }
74        Expr::Let(_, ty, val, body) => {
75            count_bvar_occ(ty, idx) + count_bvar_occ(val, idx) + count_bvar_occ(body, idx + 1)
76        }
77        Expr::Proj(_, _, s) => count_bvar_occ(s, idx),
78        _ => 0,
79    }
80}
81pub(super) fn max_loose_bvar_impl(e: &Expr, depth: u32) -> Option<u32> {
82    match e {
83        Expr::BVar(n) if *n >= depth => Some(*n - depth),
84        Expr::App(f, a) => {
85            let mf = max_loose_bvar_impl(f, depth);
86            let ma = max_loose_bvar_impl(a, depth);
87            match (mf, ma) {
88                (Some(x), Some(y)) => Some(x.max(y)),
89                (Some(x), None) | (None, Some(x)) => Some(x),
90                (None, None) => None,
91            }
92        }
93        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
94            let mt = max_loose_bvar_impl(ty, depth);
95            let mb = max_loose_bvar_impl(body, depth + 1);
96            match (mt, mb) {
97                (Some(x), Some(y)) => Some(x.max(y)),
98                (Some(x), None) | (None, Some(x)) => Some(x),
99                (None, None) => None,
100            }
101        }
102        Expr::Let(_, ty, val, body) => {
103            let mt = max_loose_bvar_impl(ty, depth);
104            let mv = max_loose_bvar_impl(val, depth);
105            let mb = max_loose_bvar_impl(body, depth + 1);
106            [mt, mv, mb].into_iter().flatten().max()
107        }
108        Expr::Proj(_, _, s) => max_loose_bvar_impl(s, depth),
109        _ => None,
110    }
111}
112pub(super) fn collect_fvars(e: &Expr, out: &mut std::collections::HashSet<FVarId>) {
113    match e {
114        Expr::FVar(id) => {
115            out.insert(*id);
116        }
117        Expr::App(f, a) => {
118            collect_fvars(f, out);
119            collect_fvars(a, out);
120        }
121        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
122            collect_fvars(ty, out);
123            collect_fvars(body, out);
124        }
125        Expr::Let(_, ty, val, body) => {
126            collect_fvars(ty, out);
127            collect_fvars(val, out);
128            collect_fvars(body, out);
129        }
130        Expr::Proj(_, _, s) => collect_fvars(s, out),
131        _ => {}
132    }
133}
134pub(super) fn collect_consts(e: &Expr, out: &mut std::collections::HashSet<Name>) {
135    match e {
136        Expr::Const(n, _) => {
137            out.insert(n.clone());
138        }
139        Expr::App(f, a) => {
140            collect_consts(f, out);
141            collect_consts(a, out);
142        }
143        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
144            collect_consts(ty, out);
145            collect_consts(body, out);
146        }
147        Expr::Let(_, ty, val, body) => {
148            collect_consts(ty, out);
149            collect_consts(val, out);
150            collect_consts(body, out);
151        }
152        Expr::Proj(_, _, s) => collect_consts(s, out),
153        _ => {}
154    }
155}
156/// Convenience constructor: `Prop` (Sort 0).
157pub fn prop() -> Expr {
158    Expr::Sort(Level::zero())
159}
160/// Convenience constructor: `Type 0` (Sort 1).
161pub fn type0() -> Expr {
162    Expr::Sort(Level::succ(Level::zero()))
163}
164/// Convenience constructor: `Type 1` (Sort 2).
165pub fn type1() -> Expr {
166    Expr::Sort(Level::succ(Level::succ(Level::zero())))
167}
168/// Build a named constant with no universe parameters.
169pub fn mk_const(name: &str) -> Expr {
170    Expr::Const(Name::str(name), vec![])
171}
172/// Build a non-dependent arrow type: `a → b`.
173pub fn mk_arrow(a: Expr, b: Expr) -> Expr {
174    Expr::Pi(
175        BinderInfo::Default,
176        Name::str("_"),
177        Box::new(a),
178        Box::new(b),
179    )
180}
181/// Build a chain of non-dependent arrow types.
182///
183/// `mk_arrows(&[A, B, C])` produces `A → B → C`.
184pub fn mk_arrows(tys: &[Expr]) -> Expr {
185    assert!(!tys.is_empty(), "mk_arrows requires at least one type");
186    if tys.len() == 1 {
187        return tys[0].clone();
188    }
189    mk_arrow(tys[0].clone(), mk_arrows(&tys[1..]))
190}
191#[cfg(test)]
192mod extended_expr_tests {
193    use super::*;
194    #[test]
195    fn test_fvar_id_gen_fresh() {
196        let mut gen = FVarIdGen::new();
197        let id0 = gen.fresh();
198        let id1 = gen.fresh();
199        assert_ne!(id0, id1);
200        assert_eq!(id0.raw(), 0);
201        assert_eq!(id1.raw(), 1);
202    }
203    #[test]
204    fn test_fvar_id_gen_reset() {
205        let mut gen = FVarIdGen::new();
206        let _ = gen.fresh();
207        gen.reset();
208        assert_eq!(gen.current(), 0);
209    }
210    #[test]
211    fn test_binder_info_predicates() {
212        assert!(BinderInfo::Default.is_explicit());
213        assert!(!BinderInfo::Implicit.is_explicit());
214        assert!(BinderInfo::Implicit.is_implicit());
215        assert!(BinderInfo::StrictImplicit.is_implicit());
216        assert!(BinderInfo::InstImplicit.is_inst_implicit());
217    }
218    #[test]
219    fn test_binder_info_delimiters() {
220        assert_eq!(BinderInfo::Default.open_delim(), "(");
221        assert_eq!(BinderInfo::Implicit.open_delim(), "{");
222        assert_eq!(BinderInfo::InstImplicit.open_delim(), "[");
223    }
224    #[test]
225    fn test_literal_predicates() {
226        let n = Literal::Nat(42);
227        let s = Literal::Str("hello".to_string());
228        assert!(n.is_nat());
229        assert!(!n.is_str());
230        assert!(s.is_str());
231        assert_eq!(n.as_nat(), Some(42));
232        assert_eq!(s.as_str(), Some("hello"));
233        assert_eq!(n.type_name(), "Nat");
234        assert_eq!(s.type_name(), "String");
235    }
236    #[test]
237    fn test_expr_is_atom() {
238        assert!(Expr::Sort(Level::zero()).is_atom());
239        assert!(Expr::BVar(0).is_atom());
240        assert!(Expr::Const(Name::str("Nat"), vec![]).is_atom());
241        assert!(!Expr::App(
242            Box::new(Expr::Const(Name::str("f"), vec![])),
243            Box::new(Expr::BVar(0))
244        )
245        .is_atom());
246    }
247    #[test]
248    fn test_expr_as_bvar() {
249        assert_eq!(Expr::BVar(3).as_bvar(), Some(3));
250        assert_eq!(Expr::Sort(Level::zero()).as_bvar(), None);
251    }
252    #[test]
253    fn test_expr_as_const_name() {
254        let e = Expr::Const(Name::str("Nat"), vec![]);
255        assert_eq!(e.as_const_name(), Some(&Name::str("Nat")));
256        assert_eq!(Expr::BVar(0).as_const_name(), None);
257    }
258    #[test]
259    fn test_expr_app_head_args() {
260        let f = Expr::Const(Name::str("f"), vec![]);
261        let a = Expr::BVar(0);
262        let b = Expr::BVar(1);
263        let app = Expr::App(
264            Box::new(Expr::App(Box::new(f.clone()), Box::new(a.clone()))),
265            Box::new(b.clone()),
266        );
267        let (head, args) = app.app_head_args();
268        assert_eq!(head, &f);
269        assert_eq!(args.len(), 2);
270    }
271    #[test]
272    fn test_expr_app_arity() {
273        let f = Expr::Const(Name::str("f"), vec![]);
274        let app1 = Expr::App(Box::new(f.clone()), Box::new(Expr::BVar(0)));
275        let app2 = Expr::App(Box::new(app1), Box::new(Expr::BVar(1)));
276        assert_eq!(app2.app_arity(), 2);
277        assert_eq!(f.app_arity(), 0);
278    }
279    #[test]
280    fn test_expr_pi_arity() {
281        let nat = Expr::Const(Name::str("Nat"), vec![]);
282        let pi1 = Expr::Pi(
283            BinderInfo::Default,
284            Name::str("x"),
285            Box::new(nat.clone()),
286            Box::new(nat.clone()),
287        );
288        let pi2 = Expr::Pi(
289            BinderInfo::Default,
290            Name::str("y"),
291            Box::new(nat.clone()),
292            Box::new(pi1),
293        );
294        assert_eq!(pi2.pi_arity(), 2);
295    }
296    #[test]
297    fn test_expr_size() {
298        let e = Expr::BVar(0);
299        assert_eq!(e.size(), 1);
300        let app = Expr::App(Box::new(e.clone()), Box::new(e.clone()));
301        assert_eq!(app.size(), 3);
302    }
303    #[test]
304    fn test_expr_ast_depth() {
305        let e = Expr::BVar(0);
306        assert_eq!(e.ast_depth(), 0);
307        let app = Expr::App(Box::new(e.clone()), Box::new(e.clone()));
308        assert_eq!(app.ast_depth(), 1);
309    }
310    #[test]
311    fn test_mk_app_many() {
312        let f = Expr::Const(Name::str("f"), vec![]);
313        let a = Expr::BVar(0);
314        let b = Expr::BVar(1);
315        let app = f.mk_app_many(&[a, b]);
316        assert_eq!(app.app_arity(), 2);
317    }
318    #[test]
319    fn test_count_bvar_occurrences() {
320        let e = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(0)));
321        assert_eq!(e.count_bvar_occurrences(0), 2);
322        assert_eq!(e.count_bvar_occurrences(1), 0);
323    }
324    #[test]
325    fn test_free_vars_empty() {
326        let e = Expr::Const(Name::str("Nat"), vec![]);
327        assert!(e.free_vars().is_empty());
328    }
329    #[test]
330    fn test_free_vars_with_fvar() {
331        let id = FVarId::new(99);
332        let e = Expr::FVar(id);
333        let fvars = e.free_vars();
334        assert_eq!(fvars.len(), 1);
335        assert!(fvars.contains(&id));
336    }
337    #[test]
338    fn test_constants_collection() {
339        let nat = Expr::Const(Name::str("Nat"), vec![]);
340        let int = Expr::Const(Name::str("Int"), vec![]);
341        let app = Expr::App(Box::new(nat), Box::new(int));
342        let consts = app.constants();
343        assert_eq!(consts.len(), 2);
344    }
345    #[test]
346    fn test_mk_arrow() {
347        let nat = mk_const("Nat");
348        let arr = mk_arrow(nat.clone(), nat.clone());
349        assert!(arr.is_pi());
350        assert_eq!(arr.pi_arity(), 1);
351    }
352    #[test]
353    fn test_mk_arrows_chain() {
354        let nat = mk_const("Nat");
355        let chain = mk_arrows(&[nat.clone(), nat.clone(), nat.clone()]);
356        assert_eq!(chain.pi_arity(), 2);
357    }
358    #[test]
359    fn test_prop_type0_type1() {
360        assert!(prop().is_prop());
361        assert!(type0().is_sort());
362        assert!(type1().is_sort());
363    }
364}
365/// Build a lambda over a list of binders, innermost last.
366///
367/// `mk_lam_many(&[(name, ty), ...], body)` wraps `body` in lambdas.
368pub fn mk_lam_many(binders: &[(Name, Expr)], body: Expr) -> Expr {
369    binders.iter().rev().fold(body, |acc, (name, ty)| {
370        Expr::Lam(
371            BinderInfo::Default,
372            name.clone(),
373            Box::new(ty.clone()),
374            Box::new(acc),
375        )
376    })
377}
378/// Build a Pi type over a list of binders.
379///
380/// `mk_pi_many(&[(name, ty), ...], body)` wraps `body` in Pis.
381pub fn mk_pi_many(binders: &[(Name, Expr)], body: Expr) -> Expr {
382    binders.iter().rev().fold(body, |acc, (name, ty)| {
383        Expr::Pi(
384            BinderInfo::Default,
385            name.clone(),
386            Box::new(ty.clone()),
387            Box::new(acc),
388        )
389    })
390}
391/// Build `Eq α a b`: the propositional equality type.
392pub fn mk_eq(alpha: Expr, a: Expr, b: Expr) -> Expr {
393    let eq_const = Expr::Const(Name::str("Eq"), vec![]);
394    Expr::App(
395        Box::new(Expr::App(
396            Box::new(Expr::App(Box::new(eq_const), Box::new(alpha))),
397            Box::new(a),
398        )),
399        Box::new(b),
400    )
401}
402/// Build `Eq.refl α a`.
403pub fn mk_refl(alpha: Expr, a: Expr) -> Expr {
404    let refl = Expr::Const(Name::str("Eq.refl"), vec![]);
405    Expr::App(
406        Box::new(Expr::App(Box::new(refl), Box::new(alpha))),
407        Box::new(a),
408    )
409}
410/// Build `And a b`: logical conjunction.
411pub fn mk_and(a: Expr, b: Expr) -> Expr {
412    let and_const = Expr::Const(Name::str("And"), vec![]);
413    Expr::App(
414        Box::new(Expr::App(Box::new(and_const), Box::new(a))),
415        Box::new(b),
416    )
417}
418/// Build `Or a b`: logical disjunction.
419pub fn mk_or(a: Expr, b: Expr) -> Expr {
420    let or_const = Expr::Const(Name::str("Or"), vec![]);
421    Expr::App(
422        Box::new(Expr::App(Box::new(or_const), Box::new(a))),
423        Box::new(b),
424    )
425}
426/// Build `Not p = p → False`.
427pub fn mk_not(p: Expr) -> Expr {
428    let false_expr = Expr::Const(Name::str("False"), vec![]);
429    mk_arrow(p, false_expr)
430}
431/// Build a let-binding `let x : ty := val in body`.
432pub fn mk_let(name: Name, ty: Expr, val: Expr, body: Expr) -> Expr {
433    Expr::Let(name, Box::new(ty), Box::new(val), Box::new(body))
434}
435/// Check if two expressions share the same head constant.
436pub fn same_head(e1: &Expr, e2: &Expr) -> bool {
437    let h1 = app_head(e1);
438    let h2 = app_head(e2);
439    match (h1, h2) {
440        (Expr::Const(n1, _), Expr::Const(n2, _)) => n1 == n2,
441        (Expr::FVar(f1), Expr::FVar(f2)) => f1 == f2,
442        (Expr::BVar(b1), Expr::BVar(b2)) => b1 == b2,
443        _ => false,
444    }
445}
446/// Return the head of an application spine (strips all Apps).
447pub fn app_head(e: &Expr) -> &Expr {
448    let mut cur = e;
449    while let Expr::App(f, _) = cur {
450        cur = f;
451    }
452    cur
453}
454/// Collect the arguments from an application spine.
455pub fn app_args(e: &Expr) -> Vec<&Expr> {
456    let mut args = Vec::new();
457    let mut cur = e;
458    while let Expr::App(f, a) = cur {
459        args.push(a.as_ref());
460        cur = f;
461    }
462    args.reverse();
463    args
464}
465/// Substitute `old` with `new_expr` everywhere it appears in `expr`.
466///
467/// Only performs exact structural matching (not modulo alpha-equivalence).
468pub fn subst_expr(expr: &Expr, old: &Expr, new_expr: &Expr) -> Expr {
469    if expr == old {
470        return new_expr.clone();
471    }
472    match expr {
473        Expr::App(f, a) => Expr::App(
474            Box::new(subst_expr(f, old, new_expr)),
475            Box::new(subst_expr(a, old, new_expr)),
476        ),
477        Expr::Lam(bi, n, ty, body) => Expr::Lam(
478            *bi,
479            n.clone(),
480            Box::new(subst_expr(ty, old, new_expr)),
481            Box::new(subst_expr(body, old, new_expr)),
482        ),
483        Expr::Pi(bi, n, ty, body) => Expr::Pi(
484            *bi,
485            n.clone(),
486            Box::new(subst_expr(ty, old, new_expr)),
487            Box::new(subst_expr(body, old, new_expr)),
488        ),
489        Expr::Let(n, ty, val, body) => Expr::Let(
490            n.clone(),
491            Box::new(subst_expr(ty, old, new_expr)),
492            Box::new(subst_expr(val, old, new_expr)),
493            Box::new(subst_expr(body, old, new_expr)),
494        ),
495        Expr::Proj(n, i, e) => Expr::Proj(n.clone(), *i, Box::new(subst_expr(e, old, new_expr))),
496        other => other.clone(),
497    }
498}
499/// Count the total number of occurrences of a sub-expression in another.
500pub fn count_occurrences(expr: &Expr, target: &Expr) -> usize {
501    if expr == target {
502        return 1;
503    }
504    match expr {
505        Expr::App(f, a) => count_occurrences(f, target) + count_occurrences(a, target),
506        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
507            count_occurrences(ty, target) + count_occurrences(body, target)
508        }
509        Expr::Let(_, ty, val, body) => {
510            count_occurrences(ty, target)
511                + count_occurrences(val, target)
512                + count_occurrences(body, target)
513        }
514        Expr::Proj(_, _, e) => count_occurrences(e, target),
515        _ => 0,
516    }
517}
518#[cfg(test)]
519mod expr_new_tests {
520    use super::*;
521    #[test]
522    fn test_mk_lam_many() {
523        let nat = mk_const("Nat");
524        let binders = vec![(Name::str("x"), nat.clone()), (Name::str("y"), nat.clone())];
525        let body = Expr::BVar(0);
526        let result = mk_lam_many(&binders, body);
527        assert_eq!(result.lam_arity(), 2);
528    }
529    #[test]
530    fn test_mk_pi_many() {
531        let nat = mk_const("Nat");
532        let binders = vec![(Name::str("x"), nat.clone())];
533        let body = nat.clone();
534        let result = mk_pi_many(&binders, body);
535        assert_eq!(result.pi_arity(), 1);
536    }
537    #[test]
538    fn test_mk_eq() {
539        let nat = mk_const("Nat");
540        let a = Expr::BVar(0);
541        let b = Expr::BVar(1);
542        let eq = mk_eq(nat, a, b);
543        assert_eq!(eq.app_arity(), 3);
544    }
545    #[test]
546    fn test_mk_refl() {
547        let nat = mk_const("Nat");
548        let a = Expr::BVar(0);
549        let refl = mk_refl(nat, a);
550        assert_eq!(refl.app_arity(), 2);
551    }
552    #[test]
553    fn test_mk_and() {
554        let p = mk_const("P");
555        let q = mk_const("Q");
556        let conj = mk_and(p, q);
557        assert_eq!(conj.app_arity(), 2);
558    }
559    #[test]
560    fn test_mk_or() {
561        let p = mk_const("P");
562        let q = mk_const("Q");
563        let disj = mk_or(p, q);
564        assert_eq!(disj.app_arity(), 2);
565    }
566    #[test]
567    fn test_mk_not() {
568        let p = mk_const("P");
569        let neg = mk_not(p);
570        assert!(neg.is_pi());
571    }
572    #[test]
573    fn test_mk_let() {
574        let nat = mk_const("Nat");
575        let val = Expr::Lit(Literal::Nat(42));
576        let body = Expr::BVar(0);
577        let let_expr = mk_let(Name::str("x"), nat, val, body);
578        assert!(let_expr.is_let());
579    }
580    #[test]
581    fn test_app_head() {
582        let f = mk_const("f");
583        let a = Expr::BVar(0);
584        let b = Expr::BVar(1);
585        let app = Expr::App(
586            Box::new(Expr::App(Box::new(f.clone()), Box::new(a))),
587            Box::new(b),
588        );
589        assert_eq!(app_head(&app), &f);
590    }
591    #[test]
592    fn test_app_args() {
593        let f = mk_const("f");
594        let a = Expr::BVar(0);
595        let b = Expr::BVar(1);
596        let app = Expr::App(
597            Box::new(Expr::App(Box::new(f), Box::new(a.clone()))),
598            Box::new(b.clone()),
599        );
600        let args = app_args(&app);
601        assert_eq!(args.len(), 2);
602    }
603    #[test]
604    fn test_same_head_true() {
605        let f = mk_const("f");
606        let e1 = Expr::App(Box::new(f.clone()), Box::new(Expr::BVar(0)));
607        let e2 = Expr::App(Box::new(f.clone()), Box::new(Expr::BVar(1)));
608        assert!(same_head(&e1, &e2));
609    }
610    #[test]
611    fn test_same_head_false() {
612        let f = mk_const("f");
613        let g = mk_const("g");
614        let e1 = Expr::App(Box::new(f), Box::new(Expr::BVar(0)));
615        let e2 = Expr::App(Box::new(g), Box::new(Expr::BVar(0)));
616        assert!(!same_head(&e1, &e2));
617    }
618    #[test]
619    fn test_subst_expr() {
620        let target = Expr::Lit(Literal::Nat(1));
621        let replacement = Expr::Lit(Literal::Nat(99));
622        let expr = Expr::App(Box::new(target.clone()), Box::new(target.clone()));
623        let result = subst_expr(&expr, &target, &replacement);
624        if let Expr::App(f, a) = &result {
625            assert_eq!(f.as_ref(), &replacement);
626            assert_eq!(a.as_ref(), &replacement);
627        } else {
628            panic!("expected App");
629        }
630    }
631    #[test]
632    fn test_count_occurrences() {
633        let target = Expr::Lit(Literal::Nat(42));
634        let expr = Expr::App(
635            Box::new(Expr::App(
636                Box::new(target.clone()),
637                Box::new(target.clone()),
638            )),
639            Box::new(target.clone()),
640        );
641        assert_eq!(count_occurrences(&expr, &target), 3);
642    }
643    #[test]
644    fn test_count_occurrences_not_found() {
645        let target = Expr::Lit(Literal::Nat(0));
646        let expr = Expr::Lit(Literal::Nat(1));
647        assert_eq!(count_occurrences(&expr, &target), 0);
648    }
649}
650#[cfg(test)]
651mod tests_padding_infra {
652    use super::*;
653    #[test]
654    fn test_stat_summary() {
655        let mut ss = StatSummary::new();
656        ss.record(10.0);
657        ss.record(20.0);
658        ss.record(30.0);
659        assert_eq!(ss.count(), 3);
660        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
661        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
662        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
663    }
664    #[test]
665    fn test_transform_stat() {
666        let mut ts = TransformStat::new();
667        ts.record_before(100.0);
668        ts.record_after(80.0);
669        let ratio = ts.mean_ratio().expect("ratio should be present");
670        assert!((ratio - 0.8).abs() < 1e-9);
671    }
672    #[test]
673    fn test_small_map() {
674        let mut m: SmallMap<u32, &str> = SmallMap::new();
675        m.insert(3, "three");
676        m.insert(1, "one");
677        m.insert(2, "two");
678        assert_eq!(m.get(&2), Some(&"two"));
679        assert_eq!(m.len(), 3);
680        let keys = m.keys();
681        assert_eq!(*keys[0], 1);
682        assert_eq!(*keys[2], 3);
683    }
684    #[test]
685    fn test_label_set() {
686        let mut ls = LabelSet::new();
687        ls.add("foo");
688        ls.add("bar");
689        ls.add("foo");
690        assert_eq!(ls.count(), 2);
691        assert!(ls.has("bar"));
692        assert!(!ls.has("baz"));
693    }
694    #[test]
695    fn test_config_node() {
696        let mut root = ConfigNode::section("root");
697        let child = ConfigNode::leaf("key", "value");
698        root.add_child(child);
699        assert_eq!(root.num_children(), 1);
700    }
701    #[test]
702    fn test_versioned_record() {
703        let mut vr = VersionedRecord::new(0u32);
704        vr.update(1);
705        vr.update(2);
706        assert_eq!(*vr.current(), 2);
707        assert_eq!(vr.version(), 2);
708        assert!(vr.has_history());
709        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
710    }
711    #[test]
712    fn test_simple_dag() {
713        let mut dag = SimpleDag::new(4);
714        dag.add_edge(0, 1);
715        dag.add_edge(1, 2);
716        dag.add_edge(2, 3);
717        assert!(dag.can_reach(0, 3));
718        assert!(!dag.can_reach(3, 0));
719        let order = dag.topological_sort().expect("order should be present");
720        assert_eq!(order, vec![0, 1, 2, 3]);
721    }
722    #[test]
723    fn test_focus_stack() {
724        let mut fs: FocusStack<&str> = FocusStack::new();
725        fs.focus("a");
726        fs.focus("b");
727        assert_eq!(fs.current(), Some(&"b"));
728        assert_eq!(fs.depth(), 2);
729        fs.blur();
730        assert_eq!(fs.current(), Some(&"a"));
731    }
732}
733#[cfg(test)]
734mod tests_extra_iterators {
735    use super::*;
736    #[test]
737    fn test_window_iterator() {
738        let data = vec![1u32, 2, 3, 4, 5];
739        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
740        assert_eq!(windows.len(), 3);
741        assert_eq!(windows[0], &[1, 2, 3]);
742        assert_eq!(windows[2], &[3, 4, 5]);
743    }
744    #[test]
745    fn test_non_empty_vec() {
746        let mut nev = NonEmptyVec::singleton(10u32);
747        nev.push(20);
748        nev.push(30);
749        assert_eq!(nev.len(), 3);
750        assert_eq!(*nev.first(), 10);
751        assert_eq!(*nev.last(), 30);
752    }
753}
754#[cfg(test)]
755mod tests_padding2 {
756    use super::*;
757    #[test]
758    fn test_sliding_sum() {
759        let mut ss = SlidingSum::new(3);
760        ss.push(1.0);
761        ss.push(2.0);
762        ss.push(3.0);
763        assert!((ss.sum() - 6.0).abs() < 1e-9);
764        ss.push(4.0);
765        assert!((ss.sum() - 9.0).abs() < 1e-9);
766        assert_eq!(ss.count(), 3);
767    }
768    #[test]
769    fn test_path_buf() {
770        let mut pb = PathBuf::new();
771        pb.push("src");
772        pb.push("main");
773        assert_eq!(pb.as_str(), "src/main");
774        assert_eq!(pb.depth(), 2);
775        pb.pop();
776        assert_eq!(pb.as_str(), "src");
777    }
778    #[test]
779    fn test_string_pool() {
780        let mut pool = StringPool::new();
781        let s = pool.take();
782        assert!(s.is_empty());
783        pool.give("hello".to_string());
784        let s2 = pool.take();
785        assert!(s2.is_empty());
786        assert_eq!(pool.free_count(), 0);
787    }
788    #[test]
789    fn test_transitive_closure() {
790        let mut tc = TransitiveClosure::new(4);
791        tc.add_edge(0, 1);
792        tc.add_edge(1, 2);
793        tc.add_edge(2, 3);
794        assert!(tc.can_reach(0, 3));
795        assert!(!tc.can_reach(3, 0));
796        let r = tc.reachable_from(0);
797        assert_eq!(r.len(), 4);
798    }
799    #[test]
800    fn test_token_bucket() {
801        let mut tb = TokenBucket::new(100, 10);
802        assert_eq!(tb.available(), 100);
803        assert!(tb.try_consume(50));
804        assert_eq!(tb.available(), 50);
805        assert!(!tb.try_consume(60));
806        assert_eq!(tb.capacity(), 100);
807    }
808    #[test]
809    fn test_rewrite_rule_set() {
810        let mut rrs = RewriteRuleSet::new();
811        rrs.add(RewriteRule::unconditional(
812            "beta",
813            "App(Lam(x, b), v)",
814            "b[x:=v]",
815        ));
816        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
817        assert_eq!(rrs.len(), 2);
818        assert_eq!(rrs.unconditional_rules().len(), 1);
819        assert_eq!(rrs.conditional_rules().len(), 1);
820        assert!(rrs.get("beta").is_some());
821        let disp = rrs
822            .get("beta")
823            .expect("element at \'beta\' should exist")
824            .display();
825        assert!(disp.contains("→"));
826    }
827}
828#[cfg(test)]
829mod tests_padding3 {
830    use super::*;
831    #[test]
832    fn test_decision_node() {
833        let tree = DecisionNode::Branch {
834            key: "x".into(),
835            val: "1".into(),
836            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
837            no_branch: Box::new(DecisionNode::Leaf("no".into())),
838        };
839        let mut ctx = std::collections::HashMap::new();
840        ctx.insert("x".into(), "1".into());
841        assert_eq!(tree.evaluate(&ctx), "yes");
842        ctx.insert("x".into(), "2".into());
843        assert_eq!(tree.evaluate(&ctx), "no");
844        assert_eq!(tree.depth(), 1);
845    }
846    #[test]
847    fn test_flat_substitution() {
848        let mut sub = FlatSubstitution::new();
849        sub.add("foo", "bar");
850        sub.add("baz", "qux");
851        assert_eq!(sub.apply("foo and baz"), "bar and qux");
852        assert_eq!(sub.len(), 2);
853    }
854    #[test]
855    fn test_stopwatch() {
856        let mut sw = Stopwatch::start();
857        sw.split();
858        sw.split();
859        assert_eq!(sw.num_splits(), 2);
860        assert!(sw.elapsed_ms() >= 0.0);
861        for &s in sw.splits() {
862            assert!(s >= 0.0);
863        }
864    }
865    #[test]
866    fn test_either2() {
867        let e: Either2<i32, &str> = Either2::First(42);
868        assert!(e.is_first());
869        let mapped = e.map_first(|x| x * 2);
870        assert_eq!(mapped.first(), Some(84));
871        let e2: Either2<i32, &str> = Either2::Second("hello");
872        assert!(e2.is_second());
873        assert_eq!(e2.second(), Some("hello"));
874    }
875    #[test]
876    fn test_write_once() {
877        let wo: WriteOnce<u32> = WriteOnce::new();
878        assert!(!wo.is_written());
879        assert!(wo.write(42));
880        assert!(!wo.write(99));
881        assert_eq!(wo.read(), Some(42));
882    }
883    #[test]
884    fn test_sparse_vec() {
885        let mut sv: SparseVec<i32> = SparseVec::new(100);
886        sv.set(5, 10);
887        sv.set(50, 20);
888        assert_eq!(*sv.get(5), 10);
889        assert_eq!(*sv.get(50), 20);
890        assert_eq!(*sv.get(0), 0);
891        assert_eq!(sv.nnz(), 2);
892        sv.set(5, 0);
893        assert_eq!(sv.nnz(), 1);
894    }
895    #[test]
896    fn test_stack_calc() {
897        let mut calc = StackCalc::new();
898        calc.push(3);
899        calc.push(4);
900        calc.add();
901        assert_eq!(calc.peek(), Some(7));
902        calc.push(2);
903        calc.mul();
904        assert_eq!(calc.peek(), Some(14));
905    }
906}
907#[cfg(test)]
908mod tests_final_padding {
909    use super::*;
910    #[test]
911    fn test_min_heap() {
912        let mut h = MinHeap::new();
913        h.push(5u32);
914        h.push(1u32);
915        h.push(3u32);
916        assert_eq!(h.peek(), Some(&1));
917        assert_eq!(h.pop(), Some(1));
918        assert_eq!(h.pop(), Some(3));
919        assert_eq!(h.pop(), Some(5));
920        assert!(h.is_empty());
921    }
922    #[test]
923    fn test_prefix_counter() {
924        let mut pc = PrefixCounter::new();
925        pc.record("hello");
926        pc.record("help");
927        pc.record("world");
928        assert_eq!(pc.count_with_prefix("hel"), 2);
929        assert_eq!(pc.count_with_prefix("wor"), 1);
930        assert_eq!(pc.count_with_prefix("xyz"), 0);
931    }
932    #[test]
933    fn test_fixture() {
934        let mut f = Fixture::new();
935        f.set("key1", "val1");
936        f.set("key2", "val2");
937        assert_eq!(f.get("key1"), Some("val1"));
938        assert_eq!(f.get("key3"), None);
939        assert_eq!(f.len(), 2);
940    }
941}
oxilean_kernel/expr/functions.rs

oxilean_kernel/expr/
functions.rs
