oxilean_kernel/infer/
functions.rs

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

oxilean_kernel/infer/
functions.rs
