oxilean_kernel/def_eq/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::reduce::{Reducer, ReducibilityHint, TransparencyMode};
6use crate::Node;
7use crate::{Environment, Expr};
8use std::collections::HashMap;
9use std::rc::Rc;
10
11use super::types::{
12    BatchDefEqChecker, ConfigNode, DecisionNode, DefEqChecker, DefEqConfig, DefEqStats, Either2,
13    FlatSubstitution, FocusStack, LabelSet, NameIndex, NonEmptyVec, PathBuf, RewriteRule,
14    RewriteRuleSet, SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch,
15    StringPool, StringTrie, TokenBucket, TransformStat, TransitiveClosure, VersionedRecord,
16    WindowIterator, WriteOnce,
17};
18
19/// Standalone function for definitional equality (without environment).
20pub fn is_def_eq_simple(t: &Expr, s: &Expr) -> bool {
21    let env = Environment::new();
22    let mut checker = DefEqChecker::new(&env);
23    checker.is_def_eq(t, s)
24}
25#[cfg(test)]
26mod tests {
27    use super::*;
28    use crate::{BinderInfo, Declaration, Level, Literal, Name, ReducibilityHint};
29    #[test]
30    fn test_reflexivity() {
31        let expr = Expr::Lit(Literal::nat(42));
32        assert!(is_def_eq_simple(&expr, &expr));
33    }
34    #[test]
35    fn test_beta_reduction() {
36        let lam = Expr::Lam(
37            BinderInfo::Default,
38            Name::str("x"),
39            Node::new(Expr::Sort(Level::zero())),
40            Node::new(Expr::BVar(0)),
41        );
42        let arg = Expr::Lit(Literal::nat(42));
43        let app = Expr::App(Node::new(lam), Node::new(arg.clone()));
44        assert!(is_def_eq_simple(&app, &arg));
45    }
46    #[test]
47    fn test_delta_reduction() {
48        let mut env = Environment::new();
49        let forty_two = Expr::Lit(Literal::nat(42));
50        env.add(Declaration::Definition {
51            name: Name::str("answer"),
52            univ_params: vec![],
53            ty: Expr::Const(Name::str("Nat"), vec![]),
54            val: forty_two.clone(),
55            hint: ReducibilityHint::Regular(1),
56        })
57        .expect("value should be present");
58        let mut checker = DefEqChecker::new(&env);
59        let answer_const = Expr::Const(Name::str("answer"), vec![]);
60        assert!(checker.is_def_eq(&answer_const, &forty_two));
61    }
62    #[test]
63    fn test_level_equivalence() {
64        let s1 = Expr::Sort(Level::max(
65            Level::param(Name::str("u")),
66            Level::param(Name::str("v")),
67        ));
68        let s2 = Expr::Sort(Level::max(
69            Level::param(Name::str("v")),
70            Level::param(Name::str("u")),
71        ));
72        assert!(is_def_eq_simple(&s1, &s2));
73    }
74    #[test]
75    fn test_not_equal() {
76        let n1 = Expr::Lit(Literal::nat(1));
77        let n2 = Expr::Lit(Literal::nat(2));
78        assert!(!is_def_eq_simple(&n1, &n2));
79    }
80    #[test]
81    fn test_lazy_delta() {
82        let mut env = Environment::new();
83        let val = Expr::Lit(Literal::nat(42));
84        env.add(Declaration::Definition {
85            name: Name::str("a"),
86            univ_params: vec![],
87            ty: Expr::Const(Name::str("Nat"), vec![]),
88            val: val.clone(),
89            hint: ReducibilityHint::Regular(1),
90        })
91        .expect("value should be present");
92        env.add(Declaration::Definition {
93            name: Name::str("b"),
94            univ_params: vec![],
95            ty: Expr::Const(Name::str("Nat"), vec![]),
96            val,
97            hint: ReducibilityHint::Regular(2),
98        })
99        .expect("value should be present");
100        let mut checker = DefEqChecker::new(&env);
101        let a = Expr::Const(Name::str("a"), vec![]);
102        let b = Expr::Const(Name::str("b"), vec![]);
103        assert!(checker.is_def_eq(&a, &b));
104    }
105    #[test]
106    fn test_app_equality() {
107        let f = Expr::Const(Name::str("f"), vec![]);
108        let a = Expr::Lit(Literal::nat(1));
109        let app1 = Expr::App(Node::new(f.clone()), Node::new(a.clone()));
110        let app2 = Expr::App(Node::new(f), Node::new(a));
111        assert!(is_def_eq_simple(&app1, &app2));
112    }
113    #[test]
114    fn test_pi_equality() {
115        let pi1 = Expr::Pi(
116            BinderInfo::Default,
117            Name::str("x"),
118            Node::new(Expr::Sort(Level::zero())),
119            Node::new(Expr::Sort(Level::zero())),
120        );
121        let pi2 = Expr::Pi(
122            BinderInfo::Default,
123            Name::str("y"),
124            Node::new(Expr::Sort(Level::zero())),
125            Node::new(Expr::Sort(Level::zero())),
126        );
127        assert!(is_def_eq_simple(&pi1, &pi2));
128    }
129}
130/// Syntactic equality check (no reduction).
131#[allow(dead_code)]
132pub fn syntactic_eq(t: &Expr, s: &Expr) -> bool {
133    match (t, s) {
134        (Expr::BVar(i), Expr::BVar(j)) => i == j,
135        (Expr::FVar(a), Expr::FVar(b)) => a == b,
136        (Expr::Sort(l1), Expr::Sort(l2)) => crate::level::is_equivalent(l1, l2),
137        (Expr::Const(n1, ls1), Expr::Const(n2, ls2)) => {
138            n1 == n2
139                && ls1.len() == ls2.len()
140                && ls1
141                    .iter()
142                    .zip(ls2.iter())
143                    .all(|(l1, l2)| crate::level::is_equivalent(l1, l2))
144        }
145        (Expr::App(f1, a1), Expr::App(f2, a2)) => syntactic_eq(f1, f2) && syntactic_eq(a1, a2),
146        (Expr::Lam(_, _, ty1, b1), Expr::Lam(_, _, ty2, b2)) => {
147            syntactic_eq(ty1, ty2) && syntactic_eq(b1, b2)
148        }
149        (Expr::Pi(_, _, ty1, b1), Expr::Pi(_, _, ty2, b2)) => {
150            syntactic_eq(ty1, ty2) && syntactic_eq(b1, b2)
151        }
152        (Expr::Let(_, ty1, v1, b1), Expr::Let(_, ty2, v2, b2)) => {
153            syntactic_eq(ty1, ty2) && syntactic_eq(v1, v2) && syntactic_eq(b1, b2)
154        }
155        (Expr::Lit(l1), Expr::Lit(l2)) => l1 == l2,
156        (Expr::Proj(n1, i1, e1), Expr::Proj(n2, i2, e2)) => {
157            n1 == n2 && i1 == i2 && syntactic_eq(e1, e2)
158        }
159        _ => false,
160    }
161}
162/// Check definitional equality with a specific transparency mode.
163#[allow(dead_code)]
164pub fn is_def_eq_with_mode(t: &Expr, s: &Expr, env: &Environment, mode: TransparencyMode) -> bool {
165    let mut checker = DefEqChecker::new(env);
166    checker.set_transparency(mode);
167    checker.is_def_eq(t, s)
168}
169/// Check definitional equality for a sequence of argument lists.
170#[allow(dead_code)]
171pub fn is_def_eq_args(args1: &[Expr], args2: &[Expr], checker: &mut DefEqChecker<'_>) -> bool {
172    if args1.len() != args2.len() {
173        return false;
174    }
175    args1
176        .iter()
177        .zip(args2.iter())
178        .all(|(a, b)| checker.is_def_eq(a, b))
179}
180#[cfg(test)]
181mod extended_def_eq_tests {
182    use super::*;
183    use crate::{BinderInfo, Level, Literal, Name};
184    #[test]
185    fn test_syntactic_eq_lit() {
186        let a = Expr::Lit(Literal::nat(5));
187        let b = Expr::Lit(Literal::nat(5));
188        let c = Expr::Lit(Literal::nat(6));
189        assert!(syntactic_eq(&a, &b));
190        assert!(!syntactic_eq(&a, &c));
191    }
192    #[test]
193    fn test_syntactic_eq_bvar() {
194        assert!(syntactic_eq(&Expr::BVar(0), &Expr::BVar(0)));
195        assert!(!syntactic_eq(&Expr::BVar(0), &Expr::BVar(1)));
196    }
197    #[test]
198    fn test_syntactic_eq_const() {
199        let a = Expr::Const(Name::str("Nat"), vec![]);
200        let b = Expr::Const(Name::str("Nat"), vec![]);
201        let c = Expr::Const(Name::str("Bool"), vec![]);
202        assert!(syntactic_eq(&a, &b));
203        assert!(!syntactic_eq(&a, &c));
204    }
205    #[test]
206    fn test_batch_checker_basic() {
207        let env = Environment::new();
208        let mut batch = BatchDefEqChecker::new(&env);
209        let a = Expr::Lit(Literal::nat(1));
210        let b = Expr::Lit(Literal::nat(1));
211        let c = Expr::Lit(Literal::nat(2));
212        assert!(batch.check(&a, &b));
213        assert!(!batch.check(&a, &c));
214    }
215    #[test]
216    fn test_batch_check_all() {
217        let env = Environment::new();
218        let mut batch = BatchDefEqChecker::new(&env);
219        let pairs = vec![
220            (Expr::Lit(Literal::nat(1)), Expr::Lit(Literal::nat(1))),
221            (Expr::Lit(Literal::nat(2)), Expr::Lit(Literal::nat(2))),
222        ];
223        assert!(batch.check_all(&pairs));
224    }
225    #[test]
226    fn test_batch_check_all_fail() {
227        let env = Environment::new();
228        let mut batch = BatchDefEqChecker::new(&env);
229        let pairs = vec![
230            (Expr::Lit(Literal::nat(1)), Expr::Lit(Literal::nat(1))),
231            (Expr::Lit(Literal::nat(2)), Expr::Lit(Literal::nat(3))),
232        ];
233        assert!(!batch.check_all(&pairs));
234    }
235    #[test]
236    fn test_batch_count_equal() {
237        let env = Environment::new();
238        let mut batch = BatchDefEqChecker::new(&env);
239        let pairs = vec![
240            (Expr::Lit(Literal::nat(1)), Expr::Lit(Literal::nat(1))),
241            (Expr::Lit(Literal::nat(2)), Expr::Lit(Literal::nat(3))),
242            (Expr::Lit(Literal::nat(4)), Expr::Lit(Literal::nat(4))),
243        ];
244        assert_eq!(batch.count_equal(&pairs), 2);
245    }
246    #[test]
247    fn test_def_eq_config_default() {
248        let cfg = DefEqConfig::default();
249        assert!(cfg.proof_irrelevance);
250        assert!(cfg.eta);
251        assert!(cfg.lazy_delta);
252    }
253    #[test]
254    fn test_def_eq_config_opaque() {
255        let cfg = DefEqConfig::opaque();
256        assert!(!cfg.lazy_delta);
257    }
258    #[test]
259    fn test_def_eq_stats_hit_rate() {
260        let stats = DefEqStats {
261            cache_hits: 8,
262            cache_misses: 2,
263            ..Default::default()
264        };
265        assert!((stats.cache_hit_rate() - 0.8).abs() < 1e-10);
266        assert_eq!(stats.total_cache_accesses(), 10);
267    }
268    #[test]
269    fn test_def_eq_stats_no_accesses() {
270        let stats = DefEqStats::default();
271        assert_eq!(stats.cache_hit_rate(), 1.0);
272        assert_eq!(stats.total_reductions(), 0);
273    }
274    #[test]
275    fn test_is_def_eq_args_equal() {
276        let env = Environment::new();
277        let mut checker = DefEqChecker::new(&env);
278        let args1 = vec![Expr::Lit(Literal::nat(1)), Expr::Lit(Literal::nat(2))];
279        let args2 = vec![Expr::Lit(Literal::nat(1)), Expr::Lit(Literal::nat(2))];
280        assert!(is_def_eq_args(&args1, &args2, &mut checker));
281    }
282    #[test]
283    fn test_is_def_eq_args_different_lengths() {
284        let env = Environment::new();
285        let mut checker = DefEqChecker::new(&env);
286        let args1 = vec![Expr::Lit(Literal::nat(1))];
287        let args2 = vec![Expr::Lit(Literal::nat(1)), Expr::Lit(Literal::nat(2))];
288        assert!(!is_def_eq_args(&args1, &args2, &mut checker));
289    }
290    #[test]
291    fn test_syntactic_eq_app() {
292        let f = Expr::Const(Name::str("f"), vec![]);
293        let x = Expr::Lit(Literal::nat(1));
294        let app1 = Expr::App(Node::new(f.clone()), Node::new(x.clone()));
295        let app2 = Expr::App(Node::new(f), Node::new(x));
296        assert!(syntactic_eq(&app1, &app2));
297    }
298    #[test]
299    fn test_syntactic_eq_pi() {
300        let ty = Expr::Sort(Level::zero());
301        let pi1 = Expr::Pi(
302            BinderInfo::Default,
303            Name::str("x"),
304            Node::new(ty.clone()),
305            Node::new(ty.clone()),
306        );
307        let pi2 = Expr::Pi(
308            BinderInfo::Default,
309            Name::str("y"),
310            Node::new(ty.clone()),
311            Node::new(ty),
312        );
313        assert!(syntactic_eq(&pi1, &pi2));
314    }
315    #[test]
316    fn test_batch_check_any() {
317        let env = Environment::new();
318        let mut batch = BatchDefEqChecker::new(&env);
319        let pairs = vec![
320            (Expr::Lit(Literal::nat(1)), Expr::Lit(Literal::nat(2))),
321            (Expr::Lit(Literal::nat(3)), Expr::Lit(Literal::nat(3))),
322        ];
323        assert!(batch.check_any(&pairs));
324    }
325    /// Build a minimal environment with:
326    ///   - `TrueProp : Prop` (an axiom with type `Sort 0`)
327    ///   - `proof1 : TrueProp` (an axiom)
328    ///   - `proof2 : TrueProp` (a different axiom for the same proposition)
329    fn make_proof_irrel_env() -> Environment {
330        use crate::{BinderInfo, Declaration, ReducibilityHint};
331        let mut env = Environment::new();
332        let prop = Expr::Sort(Level::zero());
333        env.add(Declaration::Axiom {
334            name: Name::str("TrueProp"),
335            univ_params: vec![],
336            ty: prop.clone(),
337        })
338        .expect("value should be present");
339        env.add(Declaration::Axiom {
340            name: Name::str("proof1"),
341            univ_params: vec![],
342            ty: Expr::Const(Name::str("TrueProp"), vec![]),
343        })
344        .expect("value should be present");
345        env.add(Declaration::Axiom {
346            name: Name::str("proof2"),
347            univ_params: vec![],
348            ty: Expr::Const(Name::str("TrueProp"), vec![]),
349        })
350        .expect("value should be present");
351        env.add(Declaration::Axiom {
352            name: Name::str("FalseProp"),
353            univ_params: vec![],
354            ty: prop.clone(),
355        })
356        .expect("value should be present");
357        env.add(Declaration::Axiom {
358            name: Name::str("bad_proof"),
359            univ_params: vec![],
360            ty: Expr::Const(Name::str("FalseProp"), vec![]),
361        })
362        .expect("value should be present");
363        env.add(Declaration::Axiom {
364            name: Name::str("SetProp"),
365            univ_params: vec![],
366            ty: Expr::Sort(Level::succ(Level::zero())),
367        })
368        .expect("value should be present");
369        env.add(Declaration::Axiom {
370            name: Name::str("set_elem1"),
371            univ_params: vec![],
372            ty: Expr::Const(Name::str("SetProp"), vec![]),
373        })
374        .expect("value should be present");
375        env.add(Declaration::Axiom {
376            name: Name::str("set_elem2"),
377            univ_params: vec![],
378            ty: Expr::Const(Name::str("SetProp"), vec![]),
379        })
380        .expect("value should be present");
381        let _ = BinderInfo::Default;
382        let _ = ReducibilityHint::Regular(1);
383        env
384    }
385    #[test]
386    fn test_proof_irrelevance_same_prop() {
387        let env = make_proof_irrel_env();
388        let mut checker = DefEqChecker::new(&env);
389        let p1 = Expr::Const(Name::str("proof1"), vec![]);
390        let p2 = Expr::Const(Name::str("proof2"), vec![]);
391        assert!(
392            checker.is_def_eq(&p1, &p2),
393            "Two proofs of TrueProp must be definitionally equal by proof irrelevance"
394        );
395    }
396    #[test]
397    fn test_proof_irrelevance_different_props() {
398        let env = make_proof_irrel_env();
399        let mut checker = DefEqChecker::new(&env);
400        let p1 = Expr::Const(Name::str("proof1"), vec![]);
401        let bad = Expr::Const(Name::str("bad_proof"), vec![]);
402        assert!(
403            !checker.is_def_eq(&p1, &bad),
404            "Proofs of different Props must NOT be identified by proof irrelevance"
405        );
406    }
407    #[test]
408    fn test_proof_irrelevance_disabled() {
409        let env = make_proof_irrel_env();
410        let mut checker = DefEqChecker::new(&env);
411        checker.set_proof_irrelevance(false);
412        let p1 = Expr::Const(Name::str("proof1"), vec![]);
413        let p2 = Expr::Const(Name::str("proof2"), vec![]);
414        assert!(
415            !checker.is_def_eq(&p1, &p2),
416            "With proof irrelevance disabled, distinct axioms must not be def-eq"
417        );
418    }
419    #[test]
420    fn test_proof_irrelevance_does_not_apply_to_types() {
421        let env = make_proof_irrel_env();
422        let mut checker = DefEqChecker::new(&env);
423        let e1 = Expr::Const(Name::str("set_elem1"), vec![]);
424        let e2 = Expr::Const(Name::str("set_elem2"), vec![]);
425        assert!(
426            !checker.is_def_eq(&e1, &e2),
427            "Terms of Sort 1 (Type) must NOT be identified by proof irrelevance"
428        );
429    }
430    #[test]
431    fn test_proof_irrelevance_self() {
432        let env = make_proof_irrel_env();
433        let mut checker = DefEqChecker::new(&env);
434        let p1 = Expr::Const(Name::str("proof1"), vec![]);
435        assert!(checker.is_def_eq(&p1, &p1));
436    }
437}
438/// Version tag for this module.
439#[allow(dead_code)]
440pub const MODULE_VERSION: &str = "1.0.0";
441/// Marker trait for types that can be used in module-specific contexts.
442///
443/// This is a doc-only trait providing context about the module's design philosophy.
444#[allow(dead_code)]
445pub trait ModuleMarker: Sized + Clone + std::fmt::Debug {}
446/// Generic result type for operations in this module.
447#[allow(dead_code)]
448pub type ModuleResult<T> = Result<T, String>;
449/// Create a module-level error string.
450#[allow(dead_code)]
451pub fn module_err(msg: impl Into<String>) -> String {
452    format!("[{module}] {msg}", module = "def_eq", msg = msg.into())
453}
454/// Compute the Levenshtein distance between two string slices.
455///
456/// This is used for providing "did you mean?" suggestions in error messages.
457#[allow(dead_code)]
458pub fn levenshtein_distance(a: &str, b: &str) -> usize {
459    let la = a.len();
460    let lb = b.len();
461    if la == 0 {
462        return lb;
463    }
464    if lb == 0 {
465        return la;
466    }
467    let mut row: Vec<usize> = (0..=lb).collect();
468    for (i, ca) in a.chars().enumerate() {
469        let mut prev = i;
470        row[0] = i + 1;
471        for (j, cb) in b.chars().enumerate() {
472            let old = row[j + 1];
473            row[j + 1] = if ca == cb {
474                prev
475            } else {
476                1 + old.min(row[j]).min(prev)
477            };
478            prev = old;
479        }
480    }
481    row[lb]
482}
483/// Find the closest match in a list of candidates using Levenshtein distance.
484///
485/// Returns None if candidates is empty.
486#[allow(dead_code)]
487pub fn closest_match<'a>(query: &str, candidates: &[&'a str]) -> Option<&'a str> {
488    candidates
489        .iter()
490        .min_by_key(|&&c| levenshtein_distance(query, c))
491        .copied()
492}
493/// Format a list of names for display in an error message.
494#[allow(dead_code)]
495pub fn format_name_list(names: &[&str]) -> String {
496    match names.len() {
497        0 => "(none)".to_string(),
498        1 => names[0].to_string(),
499        2 => format!("{} and {}", names[0], names[1]),
500        _ => {
501            let mut s = names[..names.len() - 1].join(", ");
502            s.push_str(", and ");
503            s.push_str(names[names.len() - 1]);
504            s
505        }
506    }
507}
508/// Collect all strings from a trie node.
509pub(super) fn collect_strings(node: &StringTrie, results: &mut Vec<String>) {
510    if let Some(v) = &node.value {
511        results.push(v.clone());
512    }
513    for child in node.children.values() {
514        collect_strings(child, results);
515    }
516}
517#[cfg(test)]
518mod utility_tests {
519    use super::*;
520    #[test]
521    fn test_levenshtein_same_string() {
522        assert_eq!(levenshtein_distance("hello", "hello"), 0);
523    }
524    #[test]
525    fn test_levenshtein_empty() {
526        assert_eq!(levenshtein_distance("", "abc"), 3);
527        assert_eq!(levenshtein_distance("abc", ""), 3);
528    }
529    #[test]
530    fn test_levenshtein_one_edit() {
531        assert_eq!(levenshtein_distance("cat", "bat"), 1);
532        assert_eq!(levenshtein_distance("cat", "cats"), 1);
533        assert_eq!(levenshtein_distance("cats", "cat"), 1);
534    }
535    #[test]
536    fn test_closest_match_found() {
537        let candidates = &["intro", "intros", "exact", "apply"];
538        let result = closest_match("intoo", candidates);
539        assert!(result.is_some());
540        assert_eq!(result.expect("result should be valid"), "intro");
541    }
542    #[test]
543    fn test_closest_match_empty() {
544        let result = closest_match("x", &[]);
545        assert!(result.is_none());
546    }
547    #[test]
548    fn test_format_name_list_empty() {
549        assert_eq!(format_name_list(&[]), "(none)");
550    }
551    #[test]
552    fn test_format_name_list_one() {
553        assert_eq!(format_name_list(&["foo"]), "foo");
554    }
555    #[test]
556    fn test_format_name_list_two() {
557        assert_eq!(format_name_list(&["a", "b"]), "a and b");
558    }
559    #[test]
560    fn test_format_name_list_many() {
561        let result = format_name_list(&["a", "b", "c"]);
562        assert!(result.contains("a"));
563        assert!(result.contains("b"));
564        assert!(result.contains("c"));
565        assert!(result.contains("and"));
566    }
567    #[test]
568    fn test_string_trie_insert_contains() {
569        let mut trie = StringTrie::new();
570        trie.insert("hello");
571        trie.insert("help");
572        trie.insert("world");
573        assert!(trie.contains("hello"));
574        assert!(trie.contains("help"));
575        assert!(trie.contains("world"));
576        assert!(!trie.contains("hell"));
577        assert_eq!(trie.len(), 3);
578    }
579    #[test]
580    fn test_string_trie_starts_with() {
581        let mut trie = StringTrie::new();
582        trie.insert("hello");
583        trie.insert("help");
584        trie.insert("world");
585        let results = trie.starts_with("hel");
586        assert_eq!(results.len(), 2);
587    }
588    #[test]
589    fn test_string_trie_empty_prefix() {
590        let mut trie = StringTrie::new();
591        trie.insert("a");
592        trie.insert("b");
593        let results = trie.starts_with("");
594        assert_eq!(results.len(), 2);
595    }
596    #[test]
597    fn test_name_index_basic() {
598        let mut idx = NameIndex::new();
599        let id1 = idx.insert("Nat");
600        let id2 = idx.insert("Bool");
601        let id3 = idx.insert("Nat");
602        assert_eq!(id1, id3);
603        assert_ne!(id1, id2);
604        assert_eq!(idx.len(), 2);
605    }
606    #[test]
607    fn test_name_index_get() {
608        let mut idx = NameIndex::new();
609        let id = idx.insert("test");
610        assert_eq!(idx.get_id("test"), Some(id));
611        assert_eq!(idx.get_name(id), Some("test"));
612        assert_eq!(idx.get_id("missing"), None);
613    }
614    #[test]
615    fn test_name_index_empty() {
616        let idx = NameIndex::new();
617        assert!(idx.is_empty());
618        assert_eq!(idx.len(), 0);
619    }
620}
621#[cfg(test)]
622mod tests_padding_infra {
623    use super::*;
624    #[test]
625    fn test_stat_summary() {
626        let mut ss = StatSummary::new();
627        ss.record(10.0);
628        ss.record(20.0);
629        ss.record(30.0);
630        assert_eq!(ss.count(), 3);
631        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
632        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
633        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
634    }
635    #[test]
636    fn test_transform_stat() {
637        let mut ts = TransformStat::new();
638        ts.record_before(100.0);
639        ts.record_after(80.0);
640        let ratio = ts.mean_ratio().expect("ratio should be present");
641        assert!((ratio - 0.8).abs() < 1e-9);
642    }
643    #[test]
644    fn test_small_map() {
645        let mut m: SmallMap<u32, &str> = SmallMap::new();
646        m.insert(3, "three");
647        m.insert(1, "one");
648        m.insert(2, "two");
649        assert_eq!(m.get(&2), Some(&"two"));
650        assert_eq!(m.len(), 3);
651        let keys = m.keys();
652        assert_eq!(*keys[0], 1);
653        assert_eq!(*keys[2], 3);
654    }
655    #[test]
656    fn test_label_set() {
657        let mut ls = LabelSet::new();
658        ls.add("foo");
659        ls.add("bar");
660        ls.add("foo");
661        assert_eq!(ls.count(), 2);
662        assert!(ls.has("bar"));
663        assert!(!ls.has("baz"));
664    }
665    #[test]
666    fn test_config_node() {
667        let mut root = ConfigNode::section("root");
668        let child = ConfigNode::leaf("key", "value");
669        root.add_child(child);
670        assert_eq!(root.num_children(), 1);
671    }
672    #[test]
673    fn test_versioned_record() {
674        let mut vr = VersionedRecord::new(0u32);
675        vr.update(1);
676        vr.update(2);
677        assert_eq!(*vr.current(), 2);
678        assert_eq!(vr.version(), 2);
679        assert!(vr.has_history());
680        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
681    }
682    #[test]
683    fn test_simple_dag() {
684        let mut dag = SimpleDag::new(4);
685        dag.add_edge(0, 1);
686        dag.add_edge(1, 2);
687        dag.add_edge(2, 3);
688        assert!(dag.can_reach(0, 3));
689        assert!(!dag.can_reach(3, 0));
690        let order = dag.topological_sort().expect("order should be present");
691        assert_eq!(order, vec![0, 1, 2, 3]);
692    }
693    #[test]
694    fn test_focus_stack() {
695        let mut fs: FocusStack<&str> = FocusStack::new();
696        fs.focus("a");
697        fs.focus("b");
698        assert_eq!(fs.current(), Some(&"b"));
699        assert_eq!(fs.depth(), 2);
700        fs.blur();
701        assert_eq!(fs.current(), Some(&"a"));
702    }
703}
704#[cfg(test)]
705mod tests_extra_iterators {
706    use super::*;
707    #[test]
708    fn test_window_iterator() {
709        let data = vec![1u32, 2, 3, 4, 5];
710        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
711        assert_eq!(windows.len(), 3);
712        assert_eq!(windows[0], &[1, 2, 3]);
713        assert_eq!(windows[2], &[3, 4, 5]);
714    }
715    #[test]
716    fn test_non_empty_vec() {
717        let mut nev = NonEmptyVec::singleton(10u32);
718        nev.push(20);
719        nev.push(30);
720        assert_eq!(nev.len(), 3);
721        assert_eq!(*nev.first(), 10);
722        assert_eq!(*nev.last(), 30);
723    }
724}
725#[cfg(test)]
726mod tests_padding2 {
727    use super::*;
728    #[test]
729    fn test_sliding_sum() {
730        let mut ss = SlidingSum::new(3);
731        ss.push(1.0);
732        ss.push(2.0);
733        ss.push(3.0);
734        assert!((ss.sum() - 6.0).abs() < 1e-9);
735        ss.push(4.0);
736        assert!((ss.sum() - 9.0).abs() < 1e-9);
737        assert_eq!(ss.count(), 3);
738    }
739    #[test]
740    fn test_path_buf() {
741        let mut pb = PathBuf::new();
742        pb.push("src");
743        pb.push("main");
744        assert_eq!(pb.as_str(), "src/main");
745        assert_eq!(pb.depth(), 2);
746        pb.pop();
747        assert_eq!(pb.as_str(), "src");
748    }
749    #[test]
750    fn test_string_pool() {
751        let mut pool = StringPool::new();
752        let s = pool.take();
753        assert!(s.is_empty());
754        pool.give("hello".to_string());
755        let s2 = pool.take();
756        assert!(s2.is_empty());
757        assert_eq!(pool.free_count(), 0);
758    }
759    #[test]
760    fn test_transitive_closure() {
761        let mut tc = TransitiveClosure::new(4);
762        tc.add_edge(0, 1);
763        tc.add_edge(1, 2);
764        tc.add_edge(2, 3);
765        assert!(tc.can_reach(0, 3));
766        assert!(!tc.can_reach(3, 0));
767        let r = tc.reachable_from(0);
768        assert_eq!(r.len(), 4);
769    }
770    #[test]
771    fn test_token_bucket() {
772        let mut tb = TokenBucket::new(100, 0);
773        assert_eq!(tb.available(), 100);
774        assert!(tb.try_consume(50));
775        assert_eq!(tb.available(), 50);
776        assert!(!tb.try_consume(60));
777        assert_eq!(tb.capacity(), 100);
778    }
779    #[test]
780    fn test_rewrite_rule_set() {
781        let mut rrs = RewriteRuleSet::new();
782        rrs.add(RewriteRule::unconditional(
783            "beta",
784            "App(Lam(x, b), v)",
785            "b[x:=v]",
786        ));
787        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
788        assert_eq!(rrs.len(), 2);
789        assert_eq!(rrs.unconditional_rules().len(), 1);
790        assert_eq!(rrs.conditional_rules().len(), 1);
791        assert!(rrs.get("beta").is_some());
792        let disp = rrs
793            .get("beta")
794            .expect("element at \'beta\' should exist")
795            .display();
796        assert!(disp.contains("→"));
797    }
798}
799#[cfg(test)]
800mod tests_padding3 {
801    use super::*;
802    #[test]
803    fn test_decision_node() {
804        let tree = DecisionNode::Branch {
805            key: "x".into(),
806            val: "1".into(),
807            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
808            no_branch: Box::new(DecisionNode::Leaf("no".into())),
809        };
810        let mut ctx = std::collections::HashMap::new();
811        ctx.insert("x".into(), "1".into());
812        assert_eq!(tree.evaluate(&ctx), "yes");
813        ctx.insert("x".into(), "2".into());
814        assert_eq!(tree.evaluate(&ctx), "no");
815        assert_eq!(tree.depth(), 1);
816    }
817    #[test]
818    fn test_flat_substitution() {
819        let mut sub = FlatSubstitution::new();
820        sub.add("foo", "bar");
821        sub.add("baz", "qux");
822        assert_eq!(sub.apply("foo and baz"), "bar and qux");
823        assert_eq!(sub.len(), 2);
824    }
825    #[test]
826    fn test_stopwatch() {
827        let mut sw = Stopwatch::start();
828        sw.split();
829        sw.split();
830        assert_eq!(sw.num_splits(), 2);
831        assert!(sw.elapsed_ms() >= 0.0);
832        for &s in sw.splits() {
833            assert!(s >= 0.0);
834        }
835    }
836    #[test]
837    fn test_either2() {
838        let e: Either2<i32, &str> = Either2::First(42);
839        assert!(e.is_first());
840        let mapped = e.map_first(|x| x * 2);
841        assert_eq!(mapped.first(), Some(84));
842        let e2: Either2<i32, &str> = Either2::Second("hello");
843        assert!(e2.is_second());
844        assert_eq!(e2.second(), Some("hello"));
845    }
846    #[test]
847    fn test_write_once() {
848        let wo: WriteOnce<u32> = WriteOnce::new();
849        assert!(!wo.is_written());
850        assert!(wo.write(42));
851        assert!(!wo.write(99));
852        assert_eq!(wo.read(), Some(42));
853    }
854    #[test]
855    fn test_sparse_vec() {
856        let mut sv: SparseVec<i32> = SparseVec::new(100);
857        sv.set(5, 10);
858        sv.set(50, 20);
859        assert_eq!(*sv.get(5), 10);
860        assert_eq!(*sv.get(50), 20);
861        assert_eq!(*sv.get(0), 0);
862        assert_eq!(sv.nnz(), 2);
863        sv.set(5, 0);
864        assert_eq!(sv.nnz(), 1);
865    }
866    #[test]
867    fn test_stack_calc() {
868        let mut calc = StackCalc::new();
869        calc.push(3);
870        calc.push(4);
871        assert_eq!(calc.add(), Some(7));
872        assert_eq!(calc.peek(), Some(7));
873        calc.push(2);
874        assert_eq!(calc.mul(), Some(14));
875        assert_eq!(calc.peek(), Some(14));
876    }
877}
oxilean_kernel/def_eq/functions.rs

oxilean_kernel/def_eq/
functions.rs
