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

oxilean_kernel/expr/
functions.rs
