oxilean_kernel/context/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::Node;
6use crate::{BinderInfo, Expr, FVarId, Name};
7use std::collections::HashMap;
8use std::rc::Rc;
9
10use super::types::{
11    ConfigNode, Context, ContextChain, ContextDiff, ContextEntry, ContextStats, DecisionNode,
12    Either2, FlatSubstitution, FocusStack, FreshNameSeq, HypContext, LabelSet, NameGenerator,
13    NonEmptyVec, PathBuf, RewriteRule, RewriteRuleSet, ScopedContext, SimpleDag, SlidingSum,
14    SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch, StringPool, TokenBucket, TransformStat,
15    TransitiveClosure, VersionedRecord, WindowIterator, WriteOnce,
16};
17
18/// Abstract a single free variable in an expression, replacing it with BVar(0).
19pub(super) fn abstract_fvar(expr: Expr, fvar: FVarId) -> Expr {
20    abstract_fvar_at(expr, fvar, 0)
21}
22/// Abstract a free variable, replacing with BVar(depth).
23pub(super) fn abstract_fvar_at(expr: Expr, fvar: FVarId, depth: u32) -> Expr {
24    match expr {
25        Expr::FVar(id) if id == fvar => Expr::BVar(depth),
26        Expr::App(f, a) => Expr::App(
27            Node::new(abstract_fvar_at((*f).clone(), fvar, depth)),
28            Node::new(abstract_fvar_at((*a).clone(), fvar, depth)),
29        ),
30        Expr::Lam(bi, n, ty, body) => Expr::Lam(
31            bi,
32            n,
33            Node::new(abstract_fvar_at((*ty).clone(), fvar, depth)),
34            Node::new(abstract_fvar_at((*body).clone(), fvar, depth + 1)),
35        ),
36        Expr::Pi(bi, n, ty, body) => Expr::Pi(
37            bi,
38            n,
39            Node::new(abstract_fvar_at((*ty).clone(), fvar, depth)),
40            Node::new(abstract_fvar_at((*body).clone(), fvar, depth + 1)),
41        ),
42        Expr::Let(n, ty, val, body) => Expr::Let(
43            n,
44            Node::new(abstract_fvar_at((*ty).clone(), fvar, depth)),
45            Node::new(abstract_fvar_at((*val).clone(), fvar, depth)),
46            Node::new(abstract_fvar_at((*body).clone(), fvar, depth + 1)),
47        ),
48        _ => expr,
49    }
50}
51/// Helper: abstract earlier fvars in a type expression for telescope construction.
52///
53/// When building `λ x₁ x₂ x₃, body`, the type annotation τᵢ of each binder xᵢ
54/// may reference the outer binders x₁…xᵢ₋₁.  This function replaces each such
55/// free variable with the appropriate de Bruijn index so that the resulting
56/// telescope is well-scoped.
57///
58/// Concretely, if `current_fvar` is at index `k` in `fvars`, then fvars[0..k]
59/// are outer binders and must be replaced with BVar(k-1-i) for fvar at index i.
60pub(super) fn abstract_fvars_in_type(ty: Expr, fvars: &[FVarId], current_fvar: FVarId) -> Expr {
61    let current_idx = match fvars.iter().position(|&f| f == current_fvar) {
62        Some(idx) => idx,
63        None => return ty,
64    };
65    if current_idx == 0 {
66        return ty;
67    }
68    let mut result = ty;
69    for (i, &fvar) in fvars[..current_idx].iter().enumerate() {
70        let depth = (current_idx - 1 - i) as u32;
71        result = abstract_fvar_at(result, fvar, depth);
72    }
73    result
74}
75#[cfg(test)]
76mod tests {
77    use super::*;
78    use crate::{Level, Literal};
79    #[test]
80    fn test_context_create() {
81        let ctx = Context::new();
82        assert_eq!(ctx.num_locals(), 0);
83        assert!(ctx.is_empty());
84    }
85    #[test]
86    fn test_push_local() {
87        let mut ctx = Context::new();
88        let ty = Expr::Sort(Level::zero());
89        let fvar = ctx.push_local(Name::str("x"), ty, None);
90        assert_eq!(ctx.num_locals(), 1);
91        assert!(!ctx.is_empty());
92        let local = ctx.get_local(fvar).expect("local should be present");
93        assert_eq!(local.name, Name::str("x"));
94    }
95    #[test]
96    fn test_pop_local() {
97        let mut ctx = Context::new();
98        let ty = Expr::Sort(Level::zero());
99        ctx.push_local(Name::str("x"), ty.clone(), None);
100        ctx.push_local(Name::str("y"), ty, None);
101        assert_eq!(ctx.num_locals(), 2);
102        let popped = ctx.pop_local().expect("popped should be present");
103        assert_eq!(popped.name, Name::str("y"));
104        assert_eq!(ctx.num_locals(), 1);
105    }
106    #[test]
107    fn test_find_local() {
108        let mut ctx = Context::new();
109        let ty = Expr::Sort(Level::zero());
110        ctx.push_local(Name::str("x"), ty.clone(), None);
111        ctx.push_local(Name::str("y"), ty, None);
112        let local = ctx
113            .find_local(&Name::str("x"))
114            .expect("local should be present");
115        assert_eq!(local.name, Name::str("x"));
116    }
117    #[test]
118    fn test_find_local_not_found() {
119        let ctx = Context::new();
120        assert!(ctx.find_local(&Name::str("z")).is_none());
121    }
122    #[test]
123    fn test_local_with_value() {
124        let mut ctx = Context::new();
125        let ty = Expr::Sort(Level::zero());
126        let val = Expr::Lit(Literal::nat(42));
127        let fvar = ctx.push_local(Name::str("x"), ty, Some(val.clone()));
128        let local = ctx.get_local(fvar).expect("local should be present");
129        assert!(local.val.is_some());
130        assert_eq!(local.val.as_ref().expect("as_ref should succeed"), &val);
131    }
132    #[test]
133    fn test_clear() {
134        let mut ctx = Context::new();
135        let ty = Expr::Sort(Level::zero());
136        ctx.push_local(Name::str("x"), ty, None);
137        ctx.clear();
138        assert_eq!(ctx.num_locals(), 0);
139        assert!(ctx.is_empty());
140    }
141    #[test]
142    fn test_mk_local_decl() {
143        let mut ctx = Context::new();
144        let ty = Expr::Sort(Level::zero());
145        let fvar_expr = ctx.mk_local_decl(Name::str("x"), BinderInfo::Default, ty);
146        assert!(matches!(fvar_expr, Expr::FVar(_)));
147        assert_eq!(ctx.num_locals(), 1);
148    }
149    #[test]
150    fn test_mk_let_decl() {
151        let mut ctx = Context::new();
152        let ty = Expr::Sort(Level::zero());
153        let val = Expr::Lit(Literal::nat(42));
154        let fvar_expr = ctx.mk_let_decl(Name::str("x"), ty, val);
155        if let Expr::FVar(id) = fvar_expr {
156            assert!(ctx.is_let(id));
157        } else {
158            panic!("Expected FVar");
159        }
160    }
161    #[test]
162    fn test_save_restore() {
163        let mut ctx = Context::new();
164        let ty = Expr::Sort(Level::zero());
165        ctx.push_local(Name::str("x"), ty.clone(), None);
166        let snap = ctx.save();
167        ctx.push_local(Name::str("y"), ty.clone(), None);
168        ctx.push_local(Name::str("z"), ty, None);
169        assert_eq!(ctx.num_locals(), 3);
170        ctx.restore(&snap);
171        assert_eq!(ctx.num_locals(), 1);
172    }
173    #[test]
174    fn test_get_fvars() {
175        let mut ctx = Context::new();
176        let ty = Expr::Sort(Level::zero());
177        ctx.push_local(Name::str("x"), ty.clone(), None);
178        ctx.push_local(Name::str("y"), ty, None);
179        let fvars = ctx.get_fvars();
180        assert_eq!(fvars.len(), 2);
181    }
182    #[test]
183    fn test_name_generator() {
184        let mut gen = NameGenerator::new("x");
185        let n1 = gen.next();
186        let n2 = gen.next();
187        assert_ne!(n1, n2);
188        assert_eq!(n1, Name::str("x_0"));
189        assert_eq!(n2, Name::str("x_1"));
190    }
191    #[test]
192    fn test_with_local() {
193        let mut ctx = Context::new();
194        let ty = Expr::Sort(Level::zero());
195        let fvar_inside = ctx.with_local(Name::str("temp"), ty, |ctx, fvar| {
196            assert_eq!(ctx.num_locals(), 1);
197            assert!(ctx.get_local(fvar).is_some());
198            fvar
199        });
200        assert_eq!(ctx.num_locals(), 0);
201        assert!(ctx.get_local(fvar_inside).is_none());
202    }
203    #[test]
204    fn test_binder_info_preserved() {
205        let mut ctx = Context::new();
206        let ty = Expr::Sort(Level::zero());
207        let fvar = ctx.push_local_with_binder(Name::str("x"), BinderInfo::Implicit, ty, None);
208        let local = ctx.get_local(fvar).expect("local should be present");
209        assert_eq!(local.binder_info, BinderInfo::Implicit);
210    }
211    #[test]
212    fn test_abstract_fvar() {
213        let fvar_id = FVarId(42);
214        let expr = Expr::App(
215            Node::new(Expr::Const(Name::str("f"), vec![])),
216            Node::new(Expr::FVar(fvar_id)),
217        );
218        let abstracted = abstract_fvar(expr, fvar_id);
219        let expected = Expr::App(
220            Node::new(Expr::Const(Name::str("f"), vec![])),
221            Node::new(Expr::BVar(0)),
222        );
223        assert_eq!(abstracted, expected);
224    }
225}
226/// Fresh name generation utilities.
227#[allow(dead_code)]
228pub mod name_gen {
229    use super::Name;
230    /// Generate a fresh name based on a base and a counter.
231    pub fn fresh(base: &str, counter: u64) -> Name {
232        Name::str(format!("{}_{}", base, counter))
233    }
234    /// Generate a Greek letter name for type variables.
235    pub fn greek(idx: usize) -> Name {
236        const GREEK: &[&str] = &[
237            "alpha", "beta", "gamma", "delta", "epsilon", "zeta", "eta", "theta", "iota", "kappa",
238            "lambda", "mu", "nu", "xi", "pi", "rho", "sigma", "tau", "upsilon", "phi", "chi",
239            "psi", "omega",
240        ];
241        if idx < GREEK.len() {
242            Name::str(GREEK[idx])
243        } else {
244            Name::str(format!("alpha{}", idx))
245        }
246    }
247    /// Generate a metavariable-style name.
248    pub fn mvar(idx: u64) -> Name {
249        Name::str(format!("?m{}", idx))
250    }
251    /// Generate a local hypothesis name.
252    pub fn hyp(idx: usize) -> Name {
253        Name::str(format!("h{}", idx))
254    }
255}
256#[cfg(test)]
257mod extended_ctx_tests {
258    use super::*;
259    use crate::{Level, Literal};
260    #[test]
261    fn test_context_entry_local() {
262        let e = ContextEntry::local(Name::str("x"), Expr::Sort(Level::zero()));
263        assert!(!e.is_let());
264        assert!(!e.is_implicit());
265    }
266    #[test]
267    fn test_context_entry_implicit() {
268        let e = ContextEntry::implicit(Name::str("alpha"), Expr::Sort(Level::zero()));
269        assert!(e.is_implicit());
270        assert!(!e.is_let());
271    }
272    #[test]
273    fn test_context_entry_let() {
274        let e = ContextEntry::let_binding(
275            Name::str("x"),
276            Expr::Sort(Level::zero()),
277            Expr::Lit(Literal::nat(1)),
278        );
279        assert!(e.is_let());
280    }
281    #[test]
282    fn test_context_chain_empty() {
283        let chain = ContextChain::new();
284        assert!(chain.is_empty());
285        assert_eq!(chain.len(), 0);
286    }
287    #[test]
288    fn test_context_chain_push_pop() {
289        let mut chain = ContextChain::new();
290        chain.push(ContextEntry::local(
291            Name::str("x"),
292            Expr::Sort(Level::zero()),
293        ));
294        chain.push(ContextEntry::implicit(
295            Name::str("y"),
296            Expr::Sort(Level::zero()),
297        ));
298        assert_eq!(chain.len(), 2);
299        assert_eq!(chain.num_implicit(), 1);
300        assert_eq!(chain.num_lets(), 0);
301        let popped = chain.pop().expect("collection should not be empty");
302        assert_eq!(popped.name, Name::str("y"));
303    }
304    #[test]
305    fn test_context_chain_find() {
306        let mut chain = ContextChain::new();
307        chain.push(ContextEntry::local(
308            Name::str("a"),
309            Expr::Sort(Level::zero()),
310        ));
311        chain.push(ContextEntry::local(
312            Name::str("b"),
313            Expr::Sort(Level::zero()),
314        ));
315        assert!(chain.find(&Name::str("a")).is_some());
316        assert!(chain.find(&Name::str("c")).is_none());
317    }
318    #[test]
319    fn test_context_chain_from_context() {
320        let mut ctx = Context::new();
321        ctx.push_local(Name::str("x"), Expr::Sort(Level::zero()), None);
322        ctx.push_local(
323            Name::str("y"),
324            Expr::Sort(Level::zero()),
325            Some(Expr::Lit(Literal::nat(0))),
326        );
327        let chain = ContextChain::from_context(&ctx);
328        assert_eq!(chain.len(), 2);
329        assert_eq!(chain.num_lets(), 1);
330    }
331    #[test]
332    fn test_context_stats() {
333        let mut ctx = Context::new();
334        ctx.push_local(Name::str("x"), Expr::Sort(Level::zero()), None);
335        ctx.push_local_with_binder(
336            Name::str("y"),
337            BinderInfo::Implicit,
338            Expr::Sort(Level::zero()),
339            None,
340        );
341        let stats = ContextStats::from_context(&ctx);
342        assert_eq!(stats.num_locals, 2);
343        assert_eq!(stats.num_implicit, 1);
344        assert_eq!(stats.num_lets, 0);
345    }
346    #[test]
347    fn test_context_diff_compute() {
348        let mut old_ctx = Context::new();
349        old_ctx.push_local(Name::str("x"), Expr::Sort(Level::zero()), None);
350        let mut new_ctx = Context::new();
351        new_ctx.push_local(Name::str("x"), Expr::Sort(Level::zero()), None);
352        new_ctx.push_local(Name::str("y"), Expr::Sort(Level::zero()), None);
353        let diff = ContextDiff::compute(&old_ctx, &new_ctx);
354        assert!(diff.added.contains(&Name::str("y")));
355        assert!(diff.removed.is_empty());
356        assert!(!diff.is_empty());
357    }
358    #[test]
359    fn test_context_diff_empty() {
360        let ctx = Context::new();
361        let diff = ContextDiff::compute(&ctx, &ctx);
362        assert!(diff.is_empty());
363    }
364    #[test]
365    fn test_name_gen_fresh() {
366        let n = name_gen::fresh("x", 5);
367        assert_eq!(n, Name::str("x_5"));
368    }
369    #[test]
370    fn test_name_gen_greek() {
371        let alpha = name_gen::greek(0);
372        let beta = name_gen::greek(1);
373        assert_ne!(alpha, beta);
374        let overflow = name_gen::greek(100);
375        assert_eq!(overflow, Name::str("alpha100"));
376    }
377    #[test]
378    fn test_name_gen_mvar() {
379        let m = name_gen::mvar(3);
380        assert_eq!(m, Name::str("?m3"));
381    }
382    #[test]
383    fn test_name_gen_hyp() {
384        let h = name_gen::hyp(0);
385        assert_eq!(h, Name::str("h0"));
386    }
387    #[test]
388    fn test_context_with_local_cleanup() {
389        let mut ctx = Context::new();
390        let ty = Expr::Sort(Level::zero());
391        let saw_local = ctx.with_local(Name::str("temp"), ty, |ctx, _fvar| {
392            assert_eq!(ctx.num_locals(), 1);
393            true
394        });
395        assert!(saw_local);
396        assert_eq!(ctx.num_locals(), 0);
397    }
398    #[test]
399    fn test_context_mk_lambda() {
400        let mut ctx = Context::new();
401        let ty = Expr::Sort(Level::zero());
402        let fvar = ctx.push_local(Name::str("x"), ty, None);
403        let body = Expr::FVar(fvar);
404        let lam = ctx.mk_lambda(&[fvar], body);
405        assert!(matches!(lam, Expr::Lam(_, _, _, _)));
406    }
407    #[test]
408    fn test_context_mk_pi() {
409        let mut ctx = Context::new();
410        let ty = Expr::Sort(Level::zero());
411        let fvar = ctx.push_local(Name::str("x"), ty, None);
412        let body = Expr::FVar(fvar);
413        let pi = ctx.mk_pi(&[fvar], body);
414        assert!(matches!(pi, Expr::Pi(_, _, _, _)));
415    }
416}
417/// Rename a free variable in an expression.
418///
419/// All occurrences of `Expr::FVar(old)` are replaced with `Expr::FVar(new)`.
420#[allow(dead_code)]
421pub fn rename_fvar(expr: Expr, old: FVarId, new: FVarId) -> Expr {
422    match expr {
423        Expr::FVar(id) if id == old => Expr::FVar(new),
424        Expr::App(f, a) => Expr::App(
425            Node::new(rename_fvar((*f).clone(), old, new)),
426            Node::new(rename_fvar((*a).clone(), old, new)),
427        ),
428        Expr::Lam(bi, n, ty, body) => Expr::Lam(
429            bi,
430            n,
431            Node::new(rename_fvar((*ty).clone(), old, new)),
432            Node::new(rename_fvar((*body).clone(), old, new)),
433        ),
434        Expr::Pi(bi, n, ty, body) => Expr::Pi(
435            bi,
436            n,
437            Node::new(rename_fvar((*ty).clone(), old, new)),
438            Node::new(rename_fvar((*body).clone(), old, new)),
439        ),
440        Expr::Let(n, ty, val, body) => Expr::Let(
441            n,
442            Node::new(rename_fvar((*ty).clone(), old, new)),
443            Node::new(rename_fvar((*val).clone(), old, new)),
444            Node::new(rename_fvar((*body).clone(), old, new)),
445        ),
446        other => other,
447    }
448}
449/// Collect all free variable IDs in an expression.
450#[allow(dead_code)]
451pub fn collect_fvars(expr: &Expr) -> Vec<FVarId> {
452    let mut result = Vec::new();
453    collect_fvars_helper(expr, &mut result);
454    result
455}
456pub(super) fn collect_fvars_helper(expr: &Expr, acc: &mut Vec<FVarId>) {
457    match expr {
458        Expr::FVar(id) if !acc.contains(id) => {
459            acc.push(*id);
460        }
461        Expr::FVar(_) => {}
462        Expr::App(f, a) => {
463            collect_fvars_helper(f, acc);
464            collect_fvars_helper(a, acc);
465        }
466        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
467            collect_fvars_helper(ty, acc);
468            collect_fvars_helper(body, acc);
469        }
470        Expr::Let(_, ty, val, body) => {
471            collect_fvars_helper(ty, acc);
472            collect_fvars_helper(val, acc);
473            collect_fvars_helper(body, acc);
474        }
475        _ => {}
476    }
477}
478/// Count the number of occurrences of a free variable in an expression.
479#[allow(dead_code)]
480pub fn count_fvar(expr: &Expr, fvar: FVarId) -> usize {
481    match expr {
482        Expr::FVar(id) if *id == fvar => 1,
483        Expr::FVar(_) => 0,
484        Expr::App(f, a) => count_fvar(f, fvar) + count_fvar(a, fvar),
485        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
486            count_fvar(ty, fvar) + count_fvar(body, fvar)
487        }
488        Expr::Let(_, ty, val, body) => {
489            count_fvar(ty, fvar) + count_fvar(val, fvar) + count_fvar(body, fvar)
490        }
491        _ => 0,
492    }
493}
494/// Check whether a free variable occurs in an expression.
495#[allow(dead_code)]
496pub fn fvar_occurs(expr: &Expr, fvar: FVarId) -> bool {
497    count_fvar(expr, fvar) > 0
498}
499#[cfg(test)]
500mod scoped_ctx_tests {
501    use super::*;
502    use crate::Level;
503    #[test]
504    fn test_rename_fvar() {
505        let old = FVarId(0);
506        let new = FVarId(1);
507        let expr = Expr::App(
508            Node::new(Expr::Const(Name::str("f"), vec![])),
509            Node::new(Expr::FVar(old)),
510        );
511        let renamed = rename_fvar(expr, old, new);
512        if let Expr::App(_, a) = renamed {
513            assert_eq!(*a, Expr::FVar(new));
514        } else {
515            panic!("expected App");
516        }
517    }
518    #[test]
519    fn test_collect_fvars() {
520        let e1 = Expr::FVar(FVarId(0));
521        let e2 = Expr::FVar(FVarId(1));
522        let expr = Expr::App(Node::new(e1), Node::new(e2));
523        let fvars = collect_fvars(&expr);
524        assert_eq!(fvars.len(), 2);
525    }
526    #[test]
527    fn test_collect_fvars_dedup() {
528        let fv = FVarId(5);
529        let expr = Expr::App(Node::new(Expr::FVar(fv)), Node::new(Expr::FVar(fv)));
530        let fvars = collect_fvars(&expr);
531        assert_eq!(fvars.len(), 1);
532    }
533    #[test]
534    fn test_count_fvar() {
535        let fv = FVarId(3);
536        let expr = Expr::App(Node::new(Expr::FVar(fv)), Node::new(Expr::FVar(fv)));
537        assert_eq!(count_fvar(&expr, fv), 2);
538        assert_eq!(count_fvar(&expr, FVarId(99)), 0);
539    }
540    #[test]
541    fn test_fvar_occurs() {
542        let fv = FVarId(7);
543        let expr = Expr::FVar(fv);
544        assert!(fvar_occurs(&expr, fv));
545        assert!(!fvar_occurs(&expr, FVarId(8)));
546    }
547    #[test]
548    fn test_scoped_context_push_pop() {
549        let mut ctx = ScopedContext::new();
550        ctx.push_scope();
551        ctx.add_local(Name::str("x"), Expr::Sort(Level::zero()));
552        assert_eq!(ctx.num_locals(), 1);
553        ctx.pop_scope();
554        assert_eq!(ctx.num_locals(), 0);
555    }
556    #[test]
557    fn test_scoped_context_depth() {
558        let mut ctx = ScopedContext::new();
559        assert_eq!(ctx.scope_depth(), 0);
560        ctx.push_scope();
561        assert_eq!(ctx.scope_depth(), 1);
562        ctx.push_scope();
563        assert_eq!(ctx.scope_depth(), 2);
564        ctx.pop_scope();
565        assert_eq!(ctx.scope_depth(), 1);
566    }
567    #[test]
568    fn test_hyp_context_add_find() {
569        let mut ctx = HypContext::new();
570        let ty = Expr::Sort(Level::zero());
571        let fvar = ctx.add_hyp(Name::str("h"), ty);
572        let found = ctx.find_hyp(&Name::str("h"));
573        assert_eq!(found, Some(fvar));
574        assert_eq!(ctx.num_hyps(), 1);
575    }
576    #[test]
577    fn test_hyp_context_not_found() {
578        let ctx = HypContext::new();
579        assert!(ctx.find_hyp(&Name::str("missing")).is_none());
580    }
581    #[test]
582    fn test_hyp_context_hyp_type() {
583        let mut ctx = HypContext::new();
584        let ty = Expr::Sort(Level::zero());
585        let fvar = ctx.add_hyp(Name::str("h"), ty.clone());
586        assert_eq!(ctx.hyp_type(fvar), Some(&ty));
587    }
588    #[test]
589    fn test_hyp_context_remove_last() {
590        let mut ctx = HypContext::new();
591        let ty = Expr::Sort(Level::zero());
592        ctx.add_hyp(Name::str("h1"), ty.clone());
593        ctx.add_hyp(Name::str("h2"), ty);
594        ctx.remove_last_hyp();
595        assert_eq!(ctx.num_hyps(), 1);
596        assert!(ctx.find_hyp(&Name::str("h2")).is_none());
597    }
598    #[test]
599    fn test_fresh_name_seq() {
600        let mut seq = FreshNameSeq::new("x");
601        let n1 = seq.next();
602        let n2 = seq.next();
603        assert_ne!(n1, n2);
604        assert_eq!(seq.count(), 2);
605    }
606    #[test]
607    fn test_fresh_name_seq_reserve() {
608        let mut seq = FreshNameSeq::new("h");
609        seq.reserve("h");
610        let n = seq.next();
611        assert_ne!(n, Name::str("h"));
612    }
613}
614#[cfg(test)]
615mod tests_padding_infra {
616    use super::*;
617    #[test]
618    fn test_stat_summary() {
619        let mut ss = StatSummary::new();
620        ss.record(10.0);
621        ss.record(20.0);
622        ss.record(30.0);
623        assert_eq!(ss.count(), 3);
624        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
625        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
626        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
627    }
628    #[test]
629    fn test_transform_stat() {
630        let mut ts = TransformStat::new();
631        ts.record_before(100.0);
632        ts.record_after(80.0);
633        let ratio = ts.mean_ratio().expect("ratio should be present");
634        assert!((ratio - 0.8).abs() < 1e-9);
635    }
636    #[test]
637    fn test_small_map() {
638        let mut m: SmallMap<u32, &str> = SmallMap::new();
639        m.insert(3, "three");
640        m.insert(1, "one");
641        m.insert(2, "two");
642        assert_eq!(m.get(&2), Some(&"two"));
643        assert_eq!(m.len(), 3);
644        let keys = m.keys();
645        assert_eq!(*keys[0], 1);
646        assert_eq!(*keys[2], 3);
647    }
648    #[test]
649    fn test_label_set() {
650        let mut ls = LabelSet::new();
651        ls.add("foo");
652        ls.add("bar");
653        ls.add("foo");
654        assert_eq!(ls.count(), 2);
655        assert!(ls.has("bar"));
656        assert!(!ls.has("baz"));
657    }
658    #[test]
659    fn test_config_node() {
660        let mut root = ConfigNode::section("root");
661        let child = ConfigNode::leaf("key", "value");
662        root.add_child(child);
663        assert_eq!(root.num_children(), 1);
664    }
665    #[test]
666    fn test_versioned_record() {
667        let mut vr = VersionedRecord::new(0u32);
668        vr.update(1);
669        vr.update(2);
670        assert_eq!(*vr.current(), 2);
671        assert_eq!(vr.version(), 2);
672        assert!(vr.has_history());
673        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
674    }
675    #[test]
676    fn test_simple_dag() {
677        let mut dag = SimpleDag::new(4);
678        dag.add_edge(0, 1);
679        dag.add_edge(1, 2);
680        dag.add_edge(2, 3);
681        assert!(dag.can_reach(0, 3));
682        assert!(!dag.can_reach(3, 0));
683        let order = dag.topological_sort().expect("order should be present");
684        assert_eq!(order, vec![0, 1, 2, 3]);
685    }
686    #[test]
687    fn test_focus_stack() {
688        let mut fs: FocusStack<&str> = FocusStack::new();
689        fs.focus("a");
690        fs.focus("b");
691        assert_eq!(fs.current(), Some(&"b"));
692        assert_eq!(fs.depth(), 2);
693        fs.blur();
694        assert_eq!(fs.current(), Some(&"a"));
695    }
696}
697#[cfg(test)]
698mod tests_extra_iterators {
699    use super::*;
700    #[test]
701    fn test_window_iterator() {
702        let data = vec![1u32, 2, 3, 4, 5];
703        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
704        assert_eq!(windows.len(), 3);
705        assert_eq!(windows[0], &[1, 2, 3]);
706        assert_eq!(windows[2], &[3, 4, 5]);
707    }
708    #[test]
709    fn test_non_empty_vec() {
710        let mut nev = NonEmptyVec::singleton(10u32);
711        nev.push(20);
712        nev.push(30);
713        assert_eq!(nev.len(), 3);
714        assert_eq!(*nev.first(), 10);
715        assert_eq!(*nev.last(), 30);
716    }
717}
718#[cfg(test)]
719mod tests_padding2 {
720    use super::*;
721    #[test]
722    fn test_sliding_sum() {
723        let mut ss = SlidingSum::new(3);
724        ss.push(1.0);
725        ss.push(2.0);
726        ss.push(3.0);
727        assert!((ss.sum() - 6.0).abs() < 1e-9);
728        ss.push(4.0);
729        assert!((ss.sum() - 9.0).abs() < 1e-9);
730        assert_eq!(ss.count(), 3);
731    }
732    #[test]
733    fn test_path_buf() {
734        let mut pb = PathBuf::new();
735        pb.push("src");
736        pb.push("main");
737        assert_eq!(pb.as_str(), "src/main");
738        assert_eq!(pb.depth(), 2);
739        pb.pop();
740        assert_eq!(pb.as_str(), "src");
741    }
742    #[test]
743    fn test_string_pool() {
744        let mut pool = StringPool::new();
745        let s = pool.take();
746        assert!(s.is_empty());
747        pool.give("hello".to_string());
748        let s2 = pool.take();
749        assert!(s2.is_empty());
750        assert_eq!(pool.free_count(), 0);
751    }
752    #[test]
753    fn test_transitive_closure() {
754        let mut tc = TransitiveClosure::new(4);
755        tc.add_edge(0, 1);
756        tc.add_edge(1, 2);
757        tc.add_edge(2, 3);
758        assert!(tc.can_reach(0, 3));
759        assert!(!tc.can_reach(3, 0));
760        let r = tc.reachable_from(0);
761        assert_eq!(r.len(), 4);
762    }
763    #[test]
764    fn test_token_bucket() {
765        let mut tb = TokenBucket::new(100, 0);
766        assert_eq!(tb.available(), 100);
767        assert!(tb.try_consume(50));
768        assert_eq!(tb.available(), 50);
769        assert!(!tb.try_consume(60));
770        assert_eq!(tb.capacity(), 100);
771    }
772    #[test]
773    fn test_rewrite_rule_set() {
774        let mut rrs = RewriteRuleSet::new();
775        rrs.add(RewriteRule::unconditional(
776            "beta",
777            "App(Lam(x, b), v)",
778            "b[x:=v]",
779        ));
780        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
781        assert_eq!(rrs.len(), 2);
782        assert_eq!(rrs.unconditional_rules().len(), 1);
783        assert_eq!(rrs.conditional_rules().len(), 1);
784        assert!(rrs.get("beta").is_some());
785        let disp = rrs
786            .get("beta")
787            .expect("element at \'beta\' should exist")
788            .display();
789        assert!(disp.contains("→"));
790    }
791}
792#[cfg(test)]
793mod tests_padding3 {
794    use super::*;
795    #[test]
796    fn test_decision_node() {
797        let tree = DecisionNode::Branch {
798            key: "x".into(),
799            val: "1".into(),
800            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
801            no_branch: Box::new(DecisionNode::Leaf("no".into())),
802        };
803        let mut ctx = std::collections::HashMap::new();
804        ctx.insert("x".into(), "1".into());
805        assert_eq!(tree.evaluate(&ctx), "yes");
806        ctx.insert("x".into(), "2".into());
807        assert_eq!(tree.evaluate(&ctx), "no");
808        assert_eq!(tree.depth(), 1);
809    }
810    #[test]
811    fn test_flat_substitution() {
812        let mut sub = FlatSubstitution::new();
813        sub.add("foo", "bar");
814        sub.add("baz", "qux");
815        assert_eq!(sub.apply("foo and baz"), "bar and qux");
816        assert_eq!(sub.len(), 2);
817    }
818    #[test]
819    fn test_stopwatch() {
820        let mut sw = Stopwatch::start();
821        sw.split();
822        sw.split();
823        assert_eq!(sw.num_splits(), 2);
824        assert!(sw.elapsed_ms() >= 0.0);
825        for &s in sw.splits() {
826            assert!(s >= 0.0);
827        }
828    }
829    #[test]
830    fn test_either2() {
831        let e: Either2<i32, &str> = Either2::First(42);
832        assert!(e.is_first());
833        let mapped = e.map_first(|x| x * 2);
834        assert_eq!(mapped.first(), Some(84));
835        let e2: Either2<i32, &str> = Either2::Second("hello");
836        assert!(e2.is_second());
837        assert_eq!(e2.second(), Some("hello"));
838    }
839    #[test]
840    fn test_write_once() {
841        let wo: WriteOnce<u32> = WriteOnce::new();
842        assert!(!wo.is_written());
843        assert!(wo.write(42));
844        assert!(!wo.write(99));
845        assert_eq!(wo.read(), Some(42));
846    }
847    #[test]
848    fn test_sparse_vec() {
849        let mut sv: SparseVec<i32> = SparseVec::new(100);
850        sv.set(5, 10);
851        sv.set(50, 20);
852        assert_eq!(*sv.get(5), 10);
853        assert_eq!(*sv.get(50), 20);
854        assert_eq!(*sv.get(0), 0);
855        assert_eq!(sv.nnz(), 2);
856        sv.set(5, 0);
857        assert_eq!(sv.nnz(), 1);
858    }
859    #[test]
860    fn test_stack_calc() {
861        let mut calc = StackCalc::new();
862        calc.push(3);
863        calc.push(4);
864        assert_eq!(calc.add(), Some(7));
865        assert_eq!(calc.peek(), Some(7));
866        calc.push(2);
867        assert_eq!(calc.mul(), Some(14));
868        assert_eq!(calc.peek(), Some(14));
869    }
870}
oxilean_kernel/context/functions.rs

oxilean_kernel/context/
functions.rs
