oxilean_kernel/proof/
functions.rs

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

oxilean_kernel/proof/
functions.rs
