oxilean_kernel/proof/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::{Expr, Level, Name};
6use std::collections::HashSet;
7
8use super::types::{
9    ConfigNode, DecisionNode, Either2, Fixture, FlatSubstitution, FocusStack, LabelSet, MinHeap,
10    NonEmptyVec, PathBuf, PrefixCounter, ProofAnalysis, ProofAnalyzer, ProofCertificate,
11    ProofComplexity, ProofNormalizer, ProofObligation, ProofSkeleton, ProofState, ProofTerm,
12    RewriteRule, RewriteRuleSet, SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc,
13    StatSummary, Stopwatch, StringPool, TokenBucket, TransformStat, TransitiveClosure,
14    VersionedRecord, WindowIterator, WriteOnce,
15};
16
17/// Known classical axioms that make proofs non-constructive.
18pub(crate) const CLASSICAL_AXIOMS: &[&str] = &[
19    "Classical.choice",
20    "Classical.em",
21    "Classical.byContradiction",
22    "Quotient.sound",
23    "propext",
24];
25/// Collect all axiom-like constant dependencies from an expression.
26pub fn collect_axiom_deps(expr: &Expr) -> HashSet<Name> {
27    let mut result = HashSet::new();
28    collect_constants_impl(expr, &mut result);
29    result
30}
31/// Collect constant names recursively.
32pub(super) fn collect_constants_impl(expr: &Expr, result: &mut HashSet<Name>) {
33    match expr {
34        Expr::Const(name, _) => {
35            result.insert(name.clone());
36        }
37        Expr::App(f, a) => {
38            collect_constants_impl(f, result);
39            collect_constants_impl(a, result);
40        }
41        Expr::Lam(_, _, ty, body) => {
42            collect_constants_impl(ty, result);
43            collect_constants_impl(body, result);
44        }
45        Expr::Pi(_, _, ty, body) => {
46            collect_constants_impl(ty, result);
47            collect_constants_impl(body, result);
48        }
49        Expr::Let(_, ty, val, body) => {
50            collect_constants_impl(ty, result);
51            collect_constants_impl(val, result);
52            collect_constants_impl(body, result);
53        }
54        Expr::Proj(_, _, e) => {
55            collect_constants_impl(e, result);
56        }
57        _ => {}
58    }
59}
60/// Check if proof irrelevance applies between two terms of a given type.
61///
62/// Returns true if the type is a Prop and both terms are proofs,
63/// meaning they should be considered definitionally equal.
64pub fn is_proof_irrelevant(ty: &Expr, _t1: &Expr, _t2: &Expr) -> bool {
65    ProofTerm::could_be_prop(ty)
66}
67#[cfg(test)]
68mod tests {
69    use super::*;
70    use crate::{Literal, Name};
71    #[test]
72    fn test_is_proof() {
73        let term = Expr::Lit(Literal::Nat(42));
74        let prop = Expr::Sort(Level::zero());
75        assert!(ProofTerm::is_proof(&term, &prop));
76    }
77    #[test]
78    fn test_is_proof_non_prop() {
79        let term = Expr::Lit(Literal::Nat(42));
80        let non_prop = Expr::Sort(Level::succ(Level::zero()));
81        assert!(!ProofTerm::is_proof(&term, &non_prop));
82    }
83    #[test]
84    fn test_size_simple() {
85        let term = Expr::Lit(Literal::Nat(42));
86        assert_eq!(ProofTerm::size(&term), 1);
87    }
88    #[test]
89    fn test_size_app() {
90        let f = Expr::Const(Name::str("f"), vec![]);
91        let a = Expr::Lit(Literal::Nat(1));
92        let app = Expr::App(Box::new(f), Box::new(a));
93        assert_eq!(ProofTerm::size(&app), 3);
94    }
95    #[test]
96    fn test_depth() {
97        let f = Expr::Const(Name::str("f"), vec![]);
98        let a = Expr::Lit(Literal::Nat(1));
99        let app = Expr::App(Box::new(f), Box::new(a));
100        assert_eq!(ProofTerm::depth(&app), 1);
101    }
102    #[test]
103    fn test_is_constructive() {
104        let term = Expr::BVar(0);
105        assert!(ProofTerm::is_constructive(&term));
106    }
107    #[test]
108    fn test_is_non_constructive() {
109        let term = Expr::Const(Name::str("Classical.choice"), vec![]);
110        assert!(!ProofTerm::is_constructive(&term));
111    }
112    #[test]
113    fn test_collect_constants() {
114        let f = Expr::Const(Name::str("f"), vec![]);
115        let g = Expr::Const(Name::str("g"), vec![]);
116        let app = Expr::App(Box::new(f), Box::new(g));
117        let consts = ProofTerm::collect_constants(&app);
118        assert!(consts.contains(&Name::str("f")));
119        assert!(consts.contains(&Name::str("g")));
120    }
121    #[test]
122    fn test_could_be_prop() {
123        assert!(ProofTerm::could_be_prop(&Expr::Sort(Level::zero())));
124        assert!(!ProofTerm::could_be_prop(&Expr::Sort(Level::succ(
125            Level::zero()
126        ))));
127    }
128    #[test]
129    fn test_is_sort_zero() {
130        assert!(ProofTerm::is_sort_zero(&Expr::Sort(Level::zero())));
131        assert!(!ProofTerm::is_sort_zero(&Expr::Sort(Level::succ(
132            Level::zero()
133        ))));
134    }
135    #[test]
136    fn test_same_proposition_structure() {
137        let p1 = Expr::Const(Name::str("True"), vec![]);
138        let p2 = Expr::Const(Name::str("True"), vec![]);
139        assert!(ProofTerm::same_proposition_structure(&p1, &p2));
140        let p3 = Expr::Const(Name::str("False"), vec![]);
141        assert!(!ProofTerm::same_proposition_structure(&p1, &p3));
142    }
143    #[test]
144    fn test_proof_irrelevance() {
145        let prop_ty = Expr::Sort(Level::zero());
146        let proof1 = Expr::Const(Name::str("p1"), vec![]);
147        let proof2 = Expr::Const(Name::str("p2"), vec![]);
148        assert!(is_proof_irrelevant(&prop_ty, &proof1, &proof2));
149        let type_ty = Expr::Sort(Level::succ(Level::zero()));
150        assert!(!is_proof_irrelevant(&type_ty, &proof1, &proof2));
151    }
152}
153/// Classifies a proof term into a `ProofComplexity` variant.
154#[allow(dead_code)]
155pub fn classify_proof(term: &Expr) -> ProofComplexity {
156    match term {
157        Expr::BVar(_) | Expr::FVar(_) | Expr::Const(_, _) | Expr::Sort(_) | Expr::Lit(_) => {
158            ProofComplexity::Atomic
159        }
160        Expr::Lam(_, _, _, _) => ProofComplexity::Abstraction,
161        Expr::App(_, _) => ProofComplexity::Application,
162        Expr::Let(_, _, _, _) => ProofComplexity::LetBinding,
163        Expr::Proj(_, _, _) => ProofComplexity::Projection,
164        Expr::Pi(_, _, _, _) => ProofComplexity::Composite,
165    }
166}
167/// Returns the set of all axiom constants depended upon by `term`.
168///
169/// This traverses the AST and collects names matching known axiom patterns.
170#[allow(dead_code)]
171pub fn axiom_dependencies(term: &Expr) -> HashSet<Name> {
172    let mut deps = HashSet::new();
173    axiom_deps_impl(term, &mut deps);
174    deps
175}
176pub(super) fn axiom_deps_impl(term: &Expr, deps: &mut HashSet<Name>) {
177    match term {
178        Expr::Const(name, _) => {
179            if CLASSICAL_AXIOMS.contains(&name.to_string().as_str()) {
180                deps.insert(name.clone());
181            }
182        }
183        Expr::App(f, a) => {
184            axiom_deps_impl(f, deps);
185            axiom_deps_impl(a, deps);
186        }
187        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
188            axiom_deps_impl(ty, deps);
189            axiom_deps_impl(body, deps);
190        }
191        Expr::Let(_, ty, val, body) => {
192            axiom_deps_impl(ty, deps);
193            axiom_deps_impl(val, deps);
194            axiom_deps_impl(body, deps);
195        }
196        Expr::Proj(_, _, e) => axiom_deps_impl(e, deps),
197        _ => {}
198    }
199}
200/// Count the number of times a given constant name appears in `term`.
201#[allow(dead_code)]
202pub fn count_const_occurrences(term: &Expr, target: &Name) -> usize {
203    match term {
204        Expr::Const(name, _) => {
205            if name == target {
206                1
207            } else {
208                0
209            }
210        }
211        Expr::App(f, a) => count_const_occurrences(f, target) + count_const_occurrences(a, target),
212        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
213            count_const_occurrences(ty, target) + count_const_occurrences(body, target)
214        }
215        Expr::Let(_, ty, val, body) => {
216            count_const_occurrences(ty, target)
217                + count_const_occurrences(val, target)
218                + count_const_occurrences(body, target)
219        }
220        Expr::Proj(_, _, e) => count_const_occurrences(e, target),
221        _ => 0,
222    }
223}
224/// Returns `true` if `term` contains no free variables (is a closed term).
225///
226/// A closed term has no `FVar` nodes; BVar nodes are allowed (they are bound).
227#[allow(dead_code)]
228pub fn is_closed_term(term: &Expr) -> bool {
229    match term {
230        Expr::FVar(_) => false,
231        Expr::BVar(_) | Expr::Const(_, _) | Expr::Sort(_) | Expr::Lit(_) => true,
232        Expr::App(f, a) => is_closed_term(f) && is_closed_term(a),
233        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
234            is_closed_term(ty) && is_closed_term(body)
235        }
236        Expr::Let(_, ty, val, body) => {
237            is_closed_term(ty) && is_closed_term(val) && is_closed_term(body)
238        }
239        Expr::Proj(_, _, e) => is_closed_term(e),
240    }
241}
242/// Checks whether two proof terms have structurally identical shapes,
243/// ignoring the actual constants and literals at the leaves.
244#[allow(dead_code)]
245pub fn same_proof_shape(a: &Expr, b: &Expr) -> bool {
246    match (a, b) {
247        (Expr::BVar(i), Expr::BVar(j)) => i == j,
248        (Expr::FVar(_), Expr::FVar(_)) => true,
249        (Expr::Const(_, _), Expr::Const(_, _)) => true,
250        (Expr::Sort(_), Expr::Sort(_)) => true,
251        (Expr::Lit(_), Expr::Lit(_)) => true,
252        (Expr::App(f1, a1), Expr::App(f2, a2)) => {
253            same_proof_shape(f1, f2) && same_proof_shape(a1, a2)
254        }
255        (Expr::Lam(_, _, ty1, b1), Expr::Lam(_, _, ty2, b2)) => {
256            same_proof_shape(ty1, ty2) && same_proof_shape(b1, b2)
257        }
258        (Expr::Pi(_, _, ty1, b1), Expr::Pi(_, _, ty2, b2)) => {
259            same_proof_shape(ty1, ty2) && same_proof_shape(b1, b2)
260        }
261        (Expr::Let(_, ty1, v1, b1), Expr::Let(_, ty2, v2, b2)) => {
262            same_proof_shape(ty1, ty2) && same_proof_shape(v1, v2) && same_proof_shape(b1, b2)
263        }
264        (Expr::Proj(i1, _, e1), Expr::Proj(i2, _, e2)) => i1 == i2 && same_proof_shape(e1, e2),
265        _ => false,
266    }
267}
268/// Estimate the "proof effort" metric: a rough measure of how hard it
269/// was to construct the term, based on its size and classical axiom usage.
270#[allow(dead_code)]
271pub fn proof_effort(term: &Expr) -> u64 {
272    let size = ProofTerm::size(term) as u64;
273    let depth = ProofTerm::depth(term) as u64;
274    let classical_penalty: u64 = if ProofTerm::is_constructive(term) {
275        0
276    } else {
277        100
278    };
279    size + depth * 2 + classical_penalty
280}
281#[cfg(test)]
282mod extended_proof_tests {
283    use super::*;
284    fn mk_const(name: &str) -> Expr {
285        Expr::Const(Name::str(name), vec![])
286    }
287    fn mk_prop() -> Expr {
288        Expr::Sort(Level::zero())
289    }
290    #[allow(dead_code)]
291    fn mk_type1() -> Expr {
292        Expr::Sort(Level::succ(Level::zero()))
293    }
294    #[test]
295    fn test_classify_atomic_const() {
296        let term = mk_const("True");
297        assert_eq!(classify_proof(&term), ProofComplexity::Atomic);
298    }
299    #[test]
300    fn test_classify_bvar() {
301        let term = Expr::BVar(0);
302        assert_eq!(classify_proof(&term), ProofComplexity::Atomic);
303    }
304    #[test]
305    fn test_classify_app() {
306        let f = mk_const("f");
307        let a = mk_const("a");
308        let app = Expr::App(Box::new(f), Box::new(a));
309        assert_eq!(classify_proof(&app), ProofComplexity::Application);
310    }
311    #[test]
312    fn test_proof_analysis_size() {
313        let term = Expr::App(Box::new(mk_const("f")), Box::new(mk_const("a")));
314        let analysis = ProofAnalysis::analyse(&term);
315        assert_eq!(analysis.size, 3);
316        assert_eq!(analysis.app_count, 1);
317        assert_eq!(analysis.lambda_count, 0);
318    }
319    #[test]
320    fn test_proof_obligation_discharge() {
321        let prop = mk_prop();
322        let mut obl = ProofObligation::new("main", prop);
323        assert!(!obl.is_discharged());
324        obl.discharge(mk_const("proof"));
325        assert!(obl.is_discharged());
326    }
327    #[test]
328    fn test_proof_state_remaining() {
329        let mut state = ProofState::new();
330        state.add_obligation("goal1", mk_prop());
331        state.add_obligation("goal2", mk_prop());
332        assert_eq!(state.remaining(), 2);
333        assert!(!state.is_complete());
334        state.discharge_next(mk_const("p1"));
335        assert_eq!(state.remaining(), 1);
336        state.discharge_next(mk_const("p2"));
337        assert!(state.is_complete());
338    }
339    #[test]
340    fn test_beta_reduce_simple() {
341        let body = Expr::BVar(0);
342        let lam = Expr::Lam(
343            crate::BinderInfo::Default,
344            Name::str("x"),
345            Box::new(mk_prop()),
346            Box::new(body),
347        );
348        let arg = mk_const("myarg");
349        let app = Expr::App(Box::new(lam), Box::new(arg.clone()));
350        let reduced = ProofNormalizer::beta_reduce(&app);
351        assert_eq!(reduced, arg);
352    }
353    #[test]
354    fn test_count_redexes_none() {
355        let term = mk_const("pure");
356        assert_eq!(ProofNormalizer::count_redexes(&term), 0);
357        assert!(ProofNormalizer::is_beta_normal(&term));
358    }
359    #[test]
360    fn test_count_redexes_one() {
361        let body = Expr::BVar(0);
362        let lam = Expr::Lam(
363            crate::BinderInfo::Default,
364            Name::str("x"),
365            Box::new(mk_prop()),
366            Box::new(body),
367        );
368        let app = Expr::App(Box::new(lam), Box::new(mk_const("arg")));
369        assert_eq!(ProofNormalizer::count_redexes(&app), 1);
370        assert!(!ProofNormalizer::is_beta_normal(&app));
371    }
372    #[test]
373    fn test_axiom_dependencies_classical() {
374        let term = mk_const("Classical.em");
375        let deps = axiom_dependencies(&term);
376        assert!(deps.contains(&Name::str("Classical.em")));
377    }
378    #[test]
379    fn test_axiom_dependencies_constructive() {
380        let term = mk_const("Nat.succ");
381        let deps = axiom_dependencies(&term);
382        assert!(deps.is_empty());
383    }
384    #[test]
385    fn test_count_const_occurrences() {
386        let target = Name::str("f");
387        let f1 = Expr::Const(target.clone(), vec![]);
388        let f2 = Expr::Const(target.clone(), vec![]);
389        let app = Expr::App(Box::new(f1), Box::new(f2));
390        assert_eq!(count_const_occurrences(&app, &target), 2);
391    }
392    #[test]
393    fn test_is_closed_const() {
394        let term = mk_const("True");
395        assert!(is_closed_term(&term));
396    }
397    #[test]
398    fn test_is_not_closed_fvar() {
399        let term = Expr::FVar(crate::FVarId(0));
400        assert!(!is_closed_term(&term));
401    }
402    #[test]
403    fn test_same_proof_shape_bvar() {
404        let a = Expr::BVar(2);
405        let b = Expr::BVar(2);
406        let c = Expr::BVar(3);
407        assert!(same_proof_shape(&a, &b));
408        assert!(!same_proof_shape(&a, &c));
409    }
410    #[test]
411    fn test_proof_effort_classical() {
412        let classical_term = mk_const("Classical.em");
413        let constructive_term = mk_const("Nat.succ");
414        assert!(proof_effort(&classical_term) > proof_effort(&constructive_term));
415    }
416    #[test]
417    fn test_proof_normalizer_subst_bvar_shift() {
418        let term = Expr::BVar(1);
419        let result = ProofNormalizer::subst_bvar(term, 0, &mk_const("x"));
420        assert_eq!(result, Expr::BVar(0));
421    }
422}
423/// Check whether a term contains a sorry-like pattern.
424#[allow(dead_code)]
425pub(crate) fn contains_classical_sorry(term: &Expr) -> bool {
426    match term {
427        Expr::Const(n, _) => {
428            let s = n.to_string();
429            s.contains("sorry") || s.contains("Lean.Elab.Tactic.sorry")
430        }
431        Expr::App(f, a) => contains_classical_sorry(f) || contains_classical_sorry(a),
432        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
433            contains_classical_sorry(ty) || contains_classical_sorry(body)
434        }
435        Expr::Let(_, ty, val, body) => {
436            contains_classical_sorry(ty)
437                || contains_classical_sorry(val)
438                || contains_classical_sorry(body)
439        }
440        _ => false,
441    }
442}
443#[cfg(test)]
444mod extra_proof_tests {
445    use super::*;
446    fn mk_const(s: &str) -> Expr {
447        Expr::Const(Name::str(s), vec![])
448    }
449    #[test]
450    fn test_proof_skeleton_no_holes() {
451        let proof = mk_const("True.intro");
452        let ty = mk_const("True");
453        let skel = ProofSkeleton::new(proof, ty);
454        assert!(skel.is_complete());
455        assert_eq!(skel.num_holes(), 0);
456    }
457    #[test]
458    fn test_proof_skeleton_with_sorry() {
459        let sorry = mk_const("sorry");
460        let ty = mk_const("Nat");
461        let skel = ProofSkeleton::new(sorry, ty);
462        assert!(!skel.is_complete());
463        assert_eq!(skel.num_holes(), 1);
464    }
465    #[test]
466    fn test_proof_skeleton_display() {
467        let proof = mk_const("True.intro");
468        let ty = mk_const("True");
469        let skel = ProofSkeleton::new(proof, ty);
470        let s = format!("{}", skel);
471        assert!(s.contains("ProofSkeleton"));
472    }
473    #[test]
474    fn test_proof_certificate_no_sorry() {
475        let prop = mk_const("True");
476        let proof = mk_const("True.intro");
477        let cert = ProofCertificate::new(prop, proof);
478        assert!(!cert.has_sorry);
479    }
480    #[test]
481    fn test_proof_certificate_trusted() {
482        let prop = mk_const("True");
483        let proof = mk_const("True.intro");
484        let cert = ProofCertificate::new(prop, proof);
485        assert!(cert.is_trusted());
486    }
487    #[test]
488    fn test_proof_analyzer_constructive() {
489        let proof = mk_const("And.intro");
490        assert!(ProofAnalyzer::is_constructive(&proof));
491    }
492    #[test]
493    fn test_proof_analyzer_classical() {
494        let proof = mk_const("Classical.em");
495        assert!(ProofAnalyzer::uses_classical(&proof));
496        assert!(!ProofAnalyzer::is_constructive(&proof));
497    }
498    #[test]
499    fn test_proof_analyzer_count_apps() {
500        let f = mk_const("f");
501        let a = mk_const("a");
502        let app = Expr::App(Box::new(f), Box::new(a));
503        assert_eq!(ProofAnalyzer::count_applications(&app), 1);
504    }
505    #[test]
506    fn test_proof_analyzer_count_apps_nested() {
507        let f = mk_const("f");
508        let a = mk_const("a");
509        let b = mk_const("b");
510        let app1 = Expr::App(Box::new(f), Box::new(a));
511        let app2 = Expr::App(Box::new(app1), Box::new(b));
512        assert_eq!(ProofAnalyzer::count_applications(&app2), 2);
513    }
514    #[test]
515    fn test_contains_classical_sorry_false() {
516        let proof = mk_const("True.intro");
517        assert!(!contains_classical_sorry(&proof));
518    }
519    #[test]
520    fn test_contains_classical_sorry_true() {
521        let sorry = mk_const("sorry");
522        assert!(contains_classical_sorry(&sorry));
523    }
524}
525#[cfg(test)]
526mod tests_padding_infra {
527    use super::*;
528    #[test]
529    fn test_stat_summary() {
530        let mut ss = StatSummary::new();
531        ss.record(10.0);
532        ss.record(20.0);
533        ss.record(30.0);
534        assert_eq!(ss.count(), 3);
535        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
536        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
537        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
538    }
539    #[test]
540    fn test_transform_stat() {
541        let mut ts = TransformStat::new();
542        ts.record_before(100.0);
543        ts.record_after(80.0);
544        let ratio = ts.mean_ratio().expect("ratio should be present");
545        assert!((ratio - 0.8).abs() < 1e-9);
546    }
547    #[test]
548    fn test_small_map() {
549        let mut m: SmallMap<u32, &str> = SmallMap::new();
550        m.insert(3, "three");
551        m.insert(1, "one");
552        m.insert(2, "two");
553        assert_eq!(m.get(&2), Some(&"two"));
554        assert_eq!(m.len(), 3);
555        let keys = m.keys();
556        assert_eq!(*keys[0], 1);
557        assert_eq!(*keys[2], 3);
558    }
559    #[test]
560    fn test_label_set() {
561        let mut ls = LabelSet::new();
562        ls.add("foo");
563        ls.add("bar");
564        ls.add("foo");
565        assert_eq!(ls.count(), 2);
566        assert!(ls.has("bar"));
567        assert!(!ls.has("baz"));
568    }
569    #[test]
570    fn test_config_node() {
571        let mut root = ConfigNode::section("root");
572        let child = ConfigNode::leaf("key", "value");
573        root.add_child(child);
574        assert_eq!(root.num_children(), 1);
575    }
576    #[test]
577    fn test_versioned_record() {
578        let mut vr = VersionedRecord::new(0u32);
579        vr.update(1);
580        vr.update(2);
581        assert_eq!(*vr.current(), 2);
582        assert_eq!(vr.version(), 2);
583        assert!(vr.has_history());
584        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
585    }
586    #[test]
587    fn test_simple_dag() {
588        let mut dag = SimpleDag::new(4);
589        dag.add_edge(0, 1);
590        dag.add_edge(1, 2);
591        dag.add_edge(2, 3);
592        assert!(dag.can_reach(0, 3));
593        assert!(!dag.can_reach(3, 0));
594        let order = dag.topological_sort().expect("order should be present");
595        assert_eq!(order, vec![0, 1, 2, 3]);
596    }
597    #[test]
598    fn test_focus_stack() {
599        let mut fs: FocusStack<&str> = FocusStack::new();
600        fs.focus("a");
601        fs.focus("b");
602        assert_eq!(fs.current(), Some(&"b"));
603        assert_eq!(fs.depth(), 2);
604        fs.blur();
605        assert_eq!(fs.current(), Some(&"a"));
606    }
607}
608#[cfg(test)]
609mod tests_extra_iterators {
610    use super::*;
611    #[test]
612    fn test_window_iterator() {
613        let data = vec![1u32, 2, 3, 4, 5];
614        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
615        assert_eq!(windows.len(), 3);
616        assert_eq!(windows[0], &[1, 2, 3]);
617        assert_eq!(windows[2], &[3, 4, 5]);
618    }
619    #[test]
620    fn test_non_empty_vec() {
621        let mut nev = NonEmptyVec::singleton(10u32);
622        nev.push(20);
623        nev.push(30);
624        assert_eq!(nev.len(), 3);
625        assert_eq!(*nev.first(), 10);
626        assert_eq!(*nev.last(), 30);
627    }
628}
629#[cfg(test)]
630mod tests_padding2 {
631    use super::*;
632    #[test]
633    fn test_sliding_sum() {
634        let mut ss = SlidingSum::new(3);
635        ss.push(1.0);
636        ss.push(2.0);
637        ss.push(3.0);
638        assert!((ss.sum() - 6.0).abs() < 1e-9);
639        ss.push(4.0);
640        assert!((ss.sum() - 9.0).abs() < 1e-9);
641        assert_eq!(ss.count(), 3);
642    }
643    #[test]
644    fn test_path_buf() {
645        let mut pb = PathBuf::new();
646        pb.push("src");
647        pb.push("main");
648        assert_eq!(pb.as_str(), "src/main");
649        assert_eq!(pb.depth(), 2);
650        pb.pop();
651        assert_eq!(pb.as_str(), "src");
652    }
653    #[test]
654    fn test_string_pool() {
655        let mut pool = StringPool::new();
656        let s = pool.take();
657        assert!(s.is_empty());
658        pool.give("hello".to_string());
659        let s2 = pool.take();
660        assert!(s2.is_empty());
661        assert_eq!(pool.free_count(), 0);
662    }
663    #[test]
664    fn test_transitive_closure() {
665        let mut tc = TransitiveClosure::new(4);
666        tc.add_edge(0, 1);
667        tc.add_edge(1, 2);
668        tc.add_edge(2, 3);
669        assert!(tc.can_reach(0, 3));
670        assert!(!tc.can_reach(3, 0));
671        let r = tc.reachable_from(0);
672        assert_eq!(r.len(), 4);
673    }
674    #[test]
675    fn test_token_bucket() {
676        let mut tb = TokenBucket::new(100, 10);
677        assert_eq!(tb.available(), 100);
678        assert!(tb.try_consume(50));
679        assert_eq!(tb.available(), 50);
680        assert!(!tb.try_consume(60));
681        assert_eq!(tb.capacity(), 100);
682    }
683    #[test]
684    fn test_rewrite_rule_set() {
685        let mut rrs = RewriteRuleSet::new();
686        rrs.add(RewriteRule::unconditional(
687            "beta",
688            "App(Lam(x, b), v)",
689            "b[x:=v]",
690        ));
691        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
692        assert_eq!(rrs.len(), 2);
693        assert_eq!(rrs.unconditional_rules().len(), 1);
694        assert_eq!(rrs.conditional_rules().len(), 1);
695        assert!(rrs.get("beta").is_some());
696        let disp = rrs
697            .get("beta")
698            .expect("element at \'beta\' should exist")
699            .display();
700        assert!(disp.contains("→"));
701    }
702}
703#[cfg(test)]
704mod tests_padding3 {
705    use super::*;
706    #[test]
707    fn test_decision_node() {
708        let tree = DecisionNode::Branch {
709            key: "x".into(),
710            val: "1".into(),
711            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
712            no_branch: Box::new(DecisionNode::Leaf("no".into())),
713        };
714        let mut ctx = std::collections::HashMap::new();
715        ctx.insert("x".into(), "1".into());
716        assert_eq!(tree.evaluate(&ctx), "yes");
717        ctx.insert("x".into(), "2".into());
718        assert_eq!(tree.evaluate(&ctx), "no");
719        assert_eq!(tree.depth(), 1);
720    }
721    #[test]
722    fn test_flat_substitution() {
723        let mut sub = FlatSubstitution::new();
724        sub.add("foo", "bar");
725        sub.add("baz", "qux");
726        assert_eq!(sub.apply("foo and baz"), "bar and qux");
727        assert_eq!(sub.len(), 2);
728    }
729    #[test]
730    fn test_stopwatch() {
731        let mut sw = Stopwatch::start();
732        sw.split();
733        sw.split();
734        assert_eq!(sw.num_splits(), 2);
735        assert!(sw.elapsed_ms() >= 0.0);
736        for &s in sw.splits() {
737            assert!(s >= 0.0);
738        }
739    }
740    #[test]
741    fn test_either2() {
742        let e: Either2<i32, &str> = Either2::First(42);
743        assert!(e.is_first());
744        let mapped = e.map_first(|x| x * 2);
745        assert_eq!(mapped.first(), Some(84));
746        let e2: Either2<i32, &str> = Either2::Second("hello");
747        assert!(e2.is_second());
748        assert_eq!(e2.second(), Some("hello"));
749    }
750    #[test]
751    fn test_write_once() {
752        let wo: WriteOnce<u32> = WriteOnce::new();
753        assert!(!wo.is_written());
754        assert!(wo.write(42));
755        assert!(!wo.write(99));
756        assert_eq!(wo.read(), Some(42));
757    }
758    #[test]
759    fn test_sparse_vec() {
760        let mut sv: SparseVec<i32> = SparseVec::new(100);
761        sv.set(5, 10);
762        sv.set(50, 20);
763        assert_eq!(*sv.get(5), 10);
764        assert_eq!(*sv.get(50), 20);
765        assert_eq!(*sv.get(0), 0);
766        assert_eq!(sv.nnz(), 2);
767        sv.set(5, 0);
768        assert_eq!(sv.nnz(), 1);
769    }
770    #[test]
771    fn test_stack_calc() {
772        let mut calc = StackCalc::new();
773        calc.push(3);
774        calc.push(4);
775        calc.add();
776        assert_eq!(calc.peek(), Some(7));
777        calc.push(2);
778        calc.mul();
779        assert_eq!(calc.peek(), Some(14));
780    }
781}
782#[cfg(test)]
783mod tests_final_padding {
784    use super::*;
785    #[test]
786    fn test_min_heap() {
787        let mut h = MinHeap::new();
788        h.push(5u32);
789        h.push(1u32);
790        h.push(3u32);
791        assert_eq!(h.peek(), Some(&1));
792        assert_eq!(h.pop(), Some(1));
793        assert_eq!(h.pop(), Some(3));
794        assert_eq!(h.pop(), Some(5));
795        assert!(h.is_empty());
796    }
797    #[test]
798    fn test_prefix_counter() {
799        let mut pc = PrefixCounter::new();
800        pc.record("hello");
801        pc.record("help");
802        pc.record("world");
803        assert_eq!(pc.count_with_prefix("hel"), 2);
804        assert_eq!(pc.count_with_prefix("wor"), 1);
805        assert_eq!(pc.count_with_prefix("xyz"), 0);
806    }
807    #[test]
808    fn test_fixture() {
809        let mut f = Fixture::new();
810        f.set("key1", "val1");
811        f.set("key2", "val2");
812        assert_eq!(f.get("key1"), Some("val1"));
813        assert_eq!(f.get("key3"), None);
814        assert_eq!(f.len(), 2);
815    }
816}
oxilean_kernel/proof/functions.rs

oxilean_kernel/proof/
functions.rs
