oxilean_kernel/infer/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::Node;
6use crate::{BinderInfo, Environment, Expr, FVarId, Level, Literal, Name};
7use std::rc::Rc;
8
9use super::types::{
10    ConfigNode, DecisionNode, Either2, FlatSubstitution, FocusStack, InferCache, InferStats,
11    LabelSet, NonEmptyVec, PathBuf, RewriteRule, RewriteRuleSet, SimpleDag, SlidingSum, SmallMap,
12    SparseVec, StackCalc, StatSummary, Stopwatch, StringPool, TokenBucket, TransformStat,
13    TransitiveClosure, TypeChecker, TypeKind, TypingJudgment, VersionedRecord, WindowIterator,
14    WriteOnce,
15};
16
17#[cfg(test)]
18mod tests {
19    use super::*;
20    use crate::{BinderInfo, Declaration};
21    #[test]
22    fn test_infer_sort() {
23        let env = Environment::new();
24        let mut tc = TypeChecker::new(&env);
25        let prop = Expr::Sort(Level::zero());
26        let prop_ty = tc.infer_type(&prop).expect("prop_ty should be present");
27        assert_eq!(prop_ty, Expr::Sort(Level::succ(Level::zero())));
28    }
29    #[test]
30    fn test_infer_constant() {
31        let mut env = Environment::new();
32        let nat_ty = Expr::Sort(Level::succ(Level::zero()));
33        env.add(Declaration::Axiom {
34            name: Name::str("Nat"),
35            univ_params: vec![],
36            ty: nat_ty.clone(),
37        })
38        .expect("value should be present");
39        let mut tc = TypeChecker::new(&env);
40        let nat_const = Expr::Const(Name::str("Nat"), vec![]);
41        let result = tc.infer_type(&nat_const).expect("result should be present");
42        assert_eq!(result, nat_ty);
43    }
44    #[test]
45    fn test_infer_lambda() {
46        let env = Environment::new();
47        let mut tc = TypeChecker::new(&env);
48        let ty = Expr::Sort(Level::zero());
49        let body = Expr::BVar(0);
50        let lam = Expr::Lam(
51            BinderInfo::Default,
52            Name::str("x"),
53            Node::new(ty.clone()),
54            Node::new(body),
55        );
56        let result = tc.infer_type(&lam).expect("result should be present");
57        assert!(matches!(result, Expr::Pi(_, _, _, _)));
58    }
59    #[test]
60    fn test_infer_literal() {
61        let env = Environment::new();
62        let mut tc = TypeChecker::new(&env);
63        let nat_lit = Expr::Lit(Literal::nat(42));
64        let result = tc.infer_type(&nat_lit).expect("result should be present");
65        assert_eq!(result, Expr::Const(Name::str("Nat"), vec![]));
66    }
67    #[test]
68    fn test_ensure_sort() {
69        let env = Environment::new();
70        let mut tc = TypeChecker::new(&env);
71        let prop = Expr::Sort(Level::zero());
72        let level = tc.ensure_sort(&prop).expect("level should be present");
73        assert_eq!(level, Level::succ(Level::zero()));
74    }
75    #[test]
76    fn test_def_eq_integration() {
77        let mut env = Environment::new();
78        let val = Expr::Lit(Literal::nat(42));
79        env.add(Declaration::Definition {
80            name: Name::str("answer"),
81            univ_params: vec![],
82            ty: Expr::Const(Name::str("Nat"), vec![]),
83            val: val.clone(),
84            hint: crate::ReducibilityHint::Regular(1),
85        })
86        .expect("value should be present");
87        let mut tc = TypeChecker::new(&env);
88        let answer = Expr::Const(Name::str("answer"), vec![]);
89        assert!(tc.is_def_eq(&answer, &val));
90    }
91    #[test]
92    fn test_whnf_integration() {
93        let mut env = Environment::new();
94        let val = Expr::Lit(Literal::nat(42));
95        env.add(Declaration::Definition {
96            name: Name::str("x"),
97            univ_params: vec![],
98            ty: Expr::Const(Name::str("Nat"), vec![]),
99            val: val.clone(),
100            hint: crate::ReducibilityHint::Abbrev,
101        })
102        .expect("value should be present");
103        let mut tc = TypeChecker::new(&env);
104        let result = tc.whnf(&Expr::Const(Name::str("x"), vec![]));
105        assert_eq!(result, val);
106    }
107    #[test]
108    fn test_infer_only_mode() {
109        let env = Environment::new();
110        let mut tc = TypeChecker::new_infer_only(&env);
111        let ty = Expr::FVar(FVarId(999));
112        let body = Expr::BVar(0);
113        let lam = Expr::Lam(
114            BinderInfo::Default,
115            Name::str("x"),
116            Node::new(ty),
117            Node::new(body),
118        );
119        let result = tc.infer_type(&lam);
120        assert!(result.is_ok());
121    }
122    #[test]
123    fn test_const_with_levels() {
124        let mut env = Environment::new();
125        let ci = crate::ConstantInfo::Axiom(crate::declaration::AxiomVal {
126            common: crate::declaration::ConstantVal {
127                name: Name::str("List"),
128                level_params: vec![Name::str("u")],
129                ty: Expr::Sort(Level::succ(Level::param(Name::str("u")))),
130            },
131            is_unsafe: false,
132        });
133        env.add_constant(ci).expect("value should be present");
134        let mut tc = TypeChecker::new(&env);
135        let list_type1 = Expr::Const(Name::str("List"), vec![Level::zero()]);
136        let result = tc
137            .infer_type(&list_type1)
138            .expect("result should be present");
139        assert_eq!(result, Expr::Sort(Level::succ(Level::zero())));
140    }
141}
142#[cfg(test)]
143mod extended_tests {
144    use super::*;
145    use crate::{BinderInfo, Literal};
146    #[test]
147    fn test_infer_app_chain_no_args() {
148        let env = Environment::new();
149        let mut tc = TypeChecker::new(&env);
150        let nat_ty = Expr::Sort(Level::succ(Level::zero()));
151        let fvar = tc.fresh_fvar(Name::str("f"), nat_ty.clone());
152        let result = tc.infer_app_chain(&Expr::FVar(fvar), &[]);
153        assert!(result.is_ok());
154        assert_eq!(result.expect("result should be valid"), nat_ty);
155    }
156    #[test]
157    fn test_telescope_type_no_pis() {
158        let env = Environment::new();
159        let mut tc = TypeChecker::new(&env);
160        let nat = Expr::Const(Name::str("Nat"), vec![]);
161        let (fvars, body) = tc.telescope_type(&nat, 5);
162        assert!(fvars.is_empty());
163        assert_eq!(body, nat);
164    }
165    #[test]
166    fn test_telescope_type_with_pi() {
167        let env = Environment::new();
168        let mut tc = TypeChecker::new(&env);
169        let nat = Expr::Const(Name::str("Nat"), vec![]);
170        let pi = Expr::Pi(
171            BinderInfo::Default,
172            Name::str("x"),
173            Node::new(nat.clone()),
174            Node::new(nat.clone()),
175        );
176        let (fvars, body) = tc.telescope_type(&pi, 1);
177        assert_eq!(fvars.len(), 1);
178        assert_eq!(body, nat);
179    }
180    #[test]
181    fn test_count_pi_binders_none() {
182        let env = Environment::new();
183        let mut tc = TypeChecker::new(&env);
184        let nat = Expr::Const(Name::str("Nat"), vec![]);
185        assert_eq!(tc.count_pi_binders(&nat), 0);
186    }
187    #[test]
188    fn test_count_pi_binders_two() {
189        let env = Environment::new();
190        let mut tc = TypeChecker::new(&env);
191        let nat = Expr::Const(Name::str("Nat"), vec![]);
192        let pi = Expr::Pi(
193            BinderInfo::Default,
194            Name::str("a"),
195            Node::new(nat.clone()),
196            Node::new(Expr::Pi(
197                BinderInfo::Default,
198                Name::str("b"),
199                Node::new(nat.clone()),
200                Node::new(nat.clone()),
201            )),
202        );
203        assert_eq!(tc.count_pi_binders(&pi), 2);
204    }
205    #[test]
206    fn test_close_type_over_fvars_empty() {
207        let env = Environment::new();
208        let mut tc = TypeChecker::new(&env);
209        let ty = Expr::Const(Name::str("Nat"), vec![]);
210        let result = tc.close_type_over_fvars(&[], ty.clone());
211        assert_eq!(result, ty);
212    }
213    #[test]
214    fn test_close_term_over_fvars_empty() {
215        let env = Environment::new();
216        let mut tc = TypeChecker::new(&env);
217        let term = Expr::Lit(Literal::nat(42));
218        let result = tc.close_term_over_fvars(&[], term.clone());
219        assert_eq!(result, term);
220    }
221    #[test]
222    fn test_try_check_correct() {
223        let env = Environment::new();
224        let mut tc = TypeChecker::new(&env);
225        let prop = Expr::Sort(Level::zero());
226        let type1 = Expr::Sort(Level::succ(Level::zero()));
227        assert!(tc.try_check(&prop, &type1));
228    }
229    #[test]
230    fn test_try_check_wrong() {
231        let env = Environment::new();
232        let mut tc = TypeChecker::new(&env);
233        let prop = Expr::Sort(Level::zero());
234        assert!(!tc.try_check(&prop, &prop));
235    }
236    #[test]
237    fn test_normalize_literal() {
238        let env = Environment::new();
239        let mut tc = TypeChecker::new(&env);
240        let lit = Expr::Lit(Literal::nat(5));
241        let result = tc.normalize(&lit);
242        assert_eq!(result, lit);
243    }
244    #[test]
245    fn test_verify_declaration_ok() {
246        let env = Environment::new();
247        let mut tc = TypeChecker::new(&env);
248        let ty = Expr::Sort(Level::succ(Level::zero()));
249        assert!(tc.verify_declaration(&Name::str("Foo"), &ty, None).is_ok());
250    }
251    #[test]
252    fn test_infer_stats_default() {
253        let stats = InferStats::default();
254        assert_eq!(stats.infer_calls, 0);
255        assert_eq!(stats.total_ops(), 0);
256    }
257    #[test]
258    fn test_infer_stats_total_ops() {
259        let stats = InferStats {
260            infer_calls: 3,
261            whnf_calls: 2,
262            def_eq_calls: 1,
263            const_lookups: 4,
264            cache_hits: 0,
265        };
266        assert_eq!(stats.total_ops(), 6);
267    }
268}
269/// Classify the surface shape of an expression.
270#[allow(dead_code)]
271pub fn classify_expr(expr: &Expr) -> TypeKind {
272    match expr {
273        Expr::Sort(l) => {
274            if let Some(n) = l.to_nat() {
275                if n == 0 {
276                    TypeKind::Prop
277                } else if n == 1 {
278                    TypeKind::Type0
279                } else {
280                    TypeKind::LargeType
281                }
282            } else {
283                TypeKind::Universe
284            }
285        }
286        Expr::Pi(_, _, _, _) => TypeKind::Pi,
287        Expr::Lam(_, _, _, _) => TypeKind::Lambda,
288        Expr::App(_, _) => TypeKind::Application,
289        Expr::FVar(_) => TypeKind::FreeVar,
290        Expr::Const(_, _) => TypeKind::Constant,
291        Expr::Lit(_) => TypeKind::Literal,
292        _ => TypeKind::Unknown,
293    }
294}
295/// Check if an expression is syntactically a universe level (Sort).
296#[allow(dead_code)]
297pub fn is_sort(expr: &Expr) -> bool {
298    matches!(expr, Expr::Sort(_))
299}
300/// Check if an expression syntactically looks like a Prop (Sort 0).
301#[allow(dead_code)]
302pub fn is_prop(expr: &Expr) -> bool {
303    matches!(expr, Expr::Sort(l) if l.is_zero())
304}
305/// Check if an expression syntactically looks like a function type (Pi).
306#[allow(dead_code)]
307pub fn is_pi(expr: &Expr) -> bool {
308    matches!(expr, Expr::Pi(_, _, _, _))
309}
310/// Extract the domain and codomain of a Pi type.
311///
312/// Returns `None` if not a Pi.
313#[allow(dead_code)]
314pub fn pi_components(expr: &Expr) -> Option<(&BinderInfo, &Name, &Expr, &Expr)> {
315    match expr {
316        Expr::Pi(bi, name, ty, body) => Some((bi, name, ty, body)),
317        _ => None,
318    }
319}
320/// Compute the sort of a Pi type given the sorts of its domain and codomain.
321///
322/// This follows the standard rules:
323/// - If codomain is Prop → Pi is Prop (impredicativity)
324/// - Otherwise → Sort(max(u, v))
325#[allow(dead_code)]
326pub fn pi_sort(domain_sort: &Level, codomain_sort: &Level) -> Level {
327    if codomain_sort.is_zero() {
328        Level::zero()
329    } else {
330        Level::max(domain_sort.clone(), codomain_sort.clone())
331    }
332}
333#[cfg(test)]
334mod extra_infer_tests {
335    use super::*;
336    #[test]
337    fn test_infer_cache_insert_get() {
338        let mut cache = InferCache::new(10);
339        let expr = Expr::Lit(Literal::nat(42));
340        let ty = Expr::Const(Name::str("Nat"), vec![]);
341        cache.insert(expr.clone(), ty.clone());
342        assert_eq!(cache.get(&expr), Some(&ty));
343    }
344    #[test]
345    fn test_infer_cache_miss() {
346        let cache = InferCache::new(10);
347        let expr = Expr::Lit(Literal::nat(1));
348        assert_eq!(cache.get(&expr), None);
349    }
350    #[test]
351    fn test_infer_cache_eviction() {
352        let mut cache = InferCache::new(2);
353        let e0 = Expr::Lit(Literal::nat(0));
354        let e1 = Expr::Lit(Literal::nat(1));
355        let e2 = Expr::Lit(Literal::nat(2));
356        let ty = Expr::Sort(Level::zero());
357        cache.insert(e0.clone(), ty.clone());
358        cache.insert(e1.clone(), ty.clone());
359        cache.insert(e2.clone(), ty.clone());
360        assert_eq!(cache.get(&e0), None);
361        assert!(cache.get(&e1).is_some());
362        assert!(cache.get(&e2).is_some());
363    }
364    #[test]
365    fn test_infer_cache_clear() {
366        let mut cache = InferCache::new(5);
367        cache.insert(Expr::Lit(Literal::nat(1)), Expr::Sort(Level::zero()));
368        cache.clear();
369        assert!(cache.is_empty());
370    }
371    #[test]
372    fn test_typing_judgment_ok() {
373        let j = TypingJudgment::ok(
374            Expr::Lit(Literal::nat(1)),
375            Expr::Const(Name::str("Nat"), vec![]),
376        );
377        assert!(j.is_ok());
378    }
379    #[test]
380    fn test_typing_judgment_fail() {
381        let j = TypingJudgment::fail(Expr::Lit(Literal::nat(0)));
382        assert!(!j.is_ok());
383    }
384    #[test]
385    fn test_classify_expr_prop() {
386        let prop = Expr::Sort(Level::zero());
387        assert_eq!(classify_expr(&prop), TypeKind::Prop);
388    }
389    #[test]
390    fn test_classify_expr_type0() {
391        let t0 = Expr::Sort(Level::succ(Level::zero()));
392        assert_eq!(classify_expr(&t0), TypeKind::Type0);
393    }
394    #[test]
395    fn test_classify_expr_pi() {
396        let pi = Expr::Pi(
397            BinderInfo::Default,
398            Name::str("x"),
399            Node::new(Expr::Sort(Level::zero())),
400            Node::new(Expr::Sort(Level::zero())),
401        );
402        assert_eq!(classify_expr(&pi), TypeKind::Pi);
403    }
404    #[test]
405    fn test_classify_expr_lambda() {
406        let lam = Expr::Lam(
407            BinderInfo::Default,
408            Name::str("x"),
409            Node::new(Expr::Sort(Level::zero())),
410            Node::new(Expr::BVar(0)),
411        );
412        assert_eq!(classify_expr(&lam), TypeKind::Lambda);
413    }
414    #[test]
415    fn test_classify_expr_literal() {
416        let lit = Expr::Lit(Literal::nat(5));
417        assert_eq!(classify_expr(&lit), TypeKind::Literal);
418    }
419    #[test]
420    fn test_is_sort_true() {
421        assert!(is_sort(&Expr::Sort(Level::zero())));
422    }
423    #[test]
424    fn test_is_sort_false() {
425        assert!(!is_sort(&Expr::Lit(Literal::nat(1))));
426    }
427    #[test]
428    fn test_is_prop_true() {
429        assert!(is_prop(&Expr::Sort(Level::zero())));
430    }
431    #[test]
432    fn test_is_prop_false() {
433        assert!(!is_prop(&Expr::Sort(Level::succ(Level::zero()))));
434    }
435    #[test]
436    fn test_is_pi_true() {
437        let pi = Expr::Pi(
438            BinderInfo::Default,
439            Name::str("_"),
440            Node::new(Expr::Sort(Level::zero())),
441            Node::new(Expr::Sort(Level::zero())),
442        );
443        assert!(is_pi(&pi));
444    }
445    #[test]
446    fn test_pi_components() {
447        let pi = Expr::Pi(
448            BinderInfo::Default,
449            Name::str("x"),
450            Node::new(Expr::Sort(Level::zero())),
451            Node::new(Expr::Sort(Level::succ(Level::zero()))),
452        );
453        let result = pi_components(&pi);
454        assert!(result.is_some());
455        let (_, name, _, _) = result.expect("result should be valid");
456        assert_eq!(*name, Name::str("x"));
457    }
458    #[test]
459    fn test_pi_sort_prop_codomain() {
460        let dom = Level::succ(Level::zero());
461        let cod = Level::zero();
462        let result = pi_sort(&dom, &cod);
463        assert!(result.is_zero());
464    }
465    #[test]
466    fn test_pi_sort_type_codomain() {
467        let dom = Level::succ(Level::zero());
468        let cod = Level::succ(Level::zero());
469        let result = pi_sort(&dom, &cod);
470        assert!(!result.is_zero());
471    }
472}
473#[cfg(test)]
474mod tests_padding_infra {
475    use super::*;
476    #[test]
477    fn test_stat_summary() {
478        let mut ss = StatSummary::new();
479        ss.record(10.0);
480        ss.record(20.0);
481        ss.record(30.0);
482        assert_eq!(ss.count(), 3);
483        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
484        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
485        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
486    }
487    #[test]
488    fn test_transform_stat() {
489        let mut ts = TransformStat::new();
490        ts.record_before(100.0);
491        ts.record_after(80.0);
492        let ratio = ts.mean_ratio().expect("ratio should be present");
493        assert!((ratio - 0.8).abs() < 1e-9);
494    }
495    #[test]
496    fn test_small_map() {
497        let mut m: SmallMap<u32, &str> = SmallMap::new();
498        m.insert(3, "three");
499        m.insert(1, "one");
500        m.insert(2, "two");
501        assert_eq!(m.get(&2), Some(&"two"));
502        assert_eq!(m.len(), 3);
503        let keys = m.keys();
504        assert_eq!(*keys[0], 1);
505        assert_eq!(*keys[2], 3);
506    }
507    #[test]
508    fn test_label_set() {
509        let mut ls = LabelSet::new();
510        ls.add("foo");
511        ls.add("bar");
512        ls.add("foo");
513        assert_eq!(ls.count(), 2);
514        assert!(ls.has("bar"));
515        assert!(!ls.has("baz"));
516    }
517    #[test]
518    fn test_config_node() {
519        let mut root = ConfigNode::section("root");
520        let child = ConfigNode::leaf("key", "value");
521        root.add_child(child);
522        assert_eq!(root.num_children(), 1);
523    }
524    #[test]
525    fn test_versioned_record() {
526        let mut vr = VersionedRecord::new(0u32);
527        vr.update(1);
528        vr.update(2);
529        assert_eq!(*vr.current(), 2);
530        assert_eq!(vr.version(), 2);
531        assert!(vr.has_history());
532        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
533    }
534    #[test]
535    fn test_simple_dag() {
536        let mut dag = SimpleDag::new(4);
537        dag.add_edge(0, 1);
538        dag.add_edge(1, 2);
539        dag.add_edge(2, 3);
540        assert!(dag.can_reach(0, 3));
541        assert!(!dag.can_reach(3, 0));
542        let order = dag.topological_sort().expect("order should be present");
543        assert_eq!(order, vec![0, 1, 2, 3]);
544    }
545    #[test]
546    fn test_focus_stack() {
547        let mut fs: FocusStack<&str> = FocusStack::new();
548        fs.focus("a");
549        fs.focus("b");
550        assert_eq!(fs.current(), Some(&"b"));
551        assert_eq!(fs.depth(), 2);
552        fs.blur();
553        assert_eq!(fs.current(), Some(&"a"));
554    }
555}
556#[cfg(test)]
557mod tests_extra_iterators {
558    use super::*;
559    #[test]
560    fn test_window_iterator() {
561        let data = vec![1u32, 2, 3, 4, 5];
562        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
563        assert_eq!(windows.len(), 3);
564        assert_eq!(windows[0], &[1, 2, 3]);
565        assert_eq!(windows[2], &[3, 4, 5]);
566    }
567    #[test]
568    fn test_non_empty_vec() {
569        let mut nev = NonEmptyVec::singleton(10u32);
570        nev.push(20);
571        nev.push(30);
572        assert_eq!(nev.len(), 3);
573        assert_eq!(*nev.first(), 10);
574        assert_eq!(*nev.last(), 30);
575    }
576}
577#[cfg(test)]
578mod tests_padding2 {
579    use super::*;
580    #[test]
581    fn test_sliding_sum() {
582        let mut ss = SlidingSum::new(3);
583        ss.push(1.0);
584        ss.push(2.0);
585        ss.push(3.0);
586        assert!((ss.sum() - 6.0).abs() < 1e-9);
587        ss.push(4.0);
588        assert!((ss.sum() - 9.0).abs() < 1e-9);
589        assert_eq!(ss.count(), 3);
590    }
591    #[test]
592    fn test_path_buf() {
593        let mut pb = PathBuf::new();
594        pb.push("src");
595        pb.push("main");
596        assert_eq!(pb.as_str(), "src/main");
597        assert_eq!(pb.depth(), 2);
598        pb.pop();
599        assert_eq!(pb.as_str(), "src");
600    }
601    #[test]
602    fn test_string_pool() {
603        let mut pool = StringPool::new();
604        let s = pool.take();
605        assert!(s.is_empty());
606        pool.give("hello".to_string());
607        let s2 = pool.take();
608        assert!(s2.is_empty());
609        assert_eq!(pool.free_count(), 0);
610    }
611    #[test]
612    fn test_transitive_closure() {
613        let mut tc = TransitiveClosure::new(4);
614        tc.add_edge(0, 1);
615        tc.add_edge(1, 2);
616        tc.add_edge(2, 3);
617        assert!(tc.can_reach(0, 3));
618        assert!(!tc.can_reach(3, 0));
619        let r = tc.reachable_from(0);
620        assert_eq!(r.len(), 4);
621    }
622    #[test]
623    fn test_token_bucket() {
624        let mut tb = TokenBucket::new(100, 0);
625        assert_eq!(tb.available(), 100);
626        assert!(tb.try_consume(50));
627        assert_eq!(tb.available(), 50);
628        assert!(!tb.try_consume(60));
629        assert_eq!(tb.capacity(), 100);
630    }
631    #[test]
632    fn test_rewrite_rule_set() {
633        let mut rrs = RewriteRuleSet::new();
634        rrs.add(RewriteRule::unconditional(
635            "beta",
636            "App(Lam(x, b), v)",
637            "b[x:=v]",
638        ));
639        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
640        assert_eq!(rrs.len(), 2);
641        assert_eq!(rrs.unconditional_rules().len(), 1);
642        assert_eq!(rrs.conditional_rules().len(), 1);
643        assert!(rrs.get("beta").is_some());
644        let disp = rrs
645            .get("beta")
646            .expect("element at \'beta\' should exist")
647            .display();
648        assert!(disp.contains("→"));
649    }
650}
651#[cfg(test)]
652mod tests_padding3 {
653    use super::*;
654    #[test]
655    fn test_decision_node() {
656        let tree = DecisionNode::Branch {
657            key: "x".into(),
658            val: "1".into(),
659            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
660            no_branch: Box::new(DecisionNode::Leaf("no".into())),
661        };
662        let mut ctx = std::collections::HashMap::new();
663        ctx.insert("x".into(), "1".into());
664        assert_eq!(tree.evaluate(&ctx), "yes");
665        ctx.insert("x".into(), "2".into());
666        assert_eq!(tree.evaluate(&ctx), "no");
667        assert_eq!(tree.depth(), 1);
668    }
669    #[test]
670    fn test_flat_substitution() {
671        let mut sub = FlatSubstitution::new();
672        sub.add("foo", "bar");
673        sub.add("baz", "qux");
674        assert_eq!(sub.apply("foo and baz"), "bar and qux");
675        assert_eq!(sub.len(), 2);
676    }
677    #[test]
678    fn test_stopwatch() {
679        let mut sw = Stopwatch::start();
680        sw.split();
681        sw.split();
682        assert_eq!(sw.num_splits(), 2);
683        assert!(sw.elapsed_ms() >= 0.0);
684        for &s in sw.splits() {
685            assert!(s >= 0.0);
686        }
687    }
688    #[test]
689    fn test_either2() {
690        let e: Either2<i32, &str> = Either2::First(42);
691        assert!(e.is_first());
692        let mapped = e.map_first(|x| x * 2);
693        assert_eq!(mapped.first(), Some(84));
694        let e2: Either2<i32, &str> = Either2::Second("hello");
695        assert!(e2.is_second());
696        assert_eq!(e2.second(), Some("hello"));
697    }
698    #[test]
699    fn test_write_once() {
700        let wo: WriteOnce<u32> = WriteOnce::new();
701        assert!(!wo.is_written());
702        assert!(wo.write(42));
703        assert!(!wo.write(99));
704        assert_eq!(wo.read(), Some(42));
705    }
706    #[test]
707    fn test_sparse_vec() {
708        let mut sv: SparseVec<i32> = SparseVec::new(100);
709        sv.set(5, 10);
710        sv.set(50, 20);
711        assert_eq!(*sv.get(5), 10);
712        assert_eq!(*sv.get(50), 20);
713        assert_eq!(*sv.get(0), 0);
714        assert_eq!(sv.nnz(), 2);
715        sv.set(5, 0);
716        assert_eq!(sv.nnz(), 1);
717    }
718    #[test]
719    fn test_stack_calc() {
720        let mut calc = StackCalc::new();
721        calc.push(3);
722        calc.push(4);
723        assert_eq!(calc.add(), Some(7));
724        assert_eq!(calc.peek(), Some(7));
725        calc.push(2);
726        assert_eq!(calc.mul(), Some(14));
727        assert_eq!(calc.peek(), Some(14));
728    }
729}
oxilean_kernel/infer/functions.rs

oxilean_kernel/infer/
functions.rs
