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

oxilean_kernel/def_eq/
functions.rs
