oxilean_kernel/expr/
functions.rs

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

oxilean_kernel/expr/
functions.rs
