oxilean_kernel/conversion/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::reduce::TransparencyMode;
6use crate::{Environment, Expr, Reducer};
7
8use super::types::{
9    BitSet64, BucketCounter, Coercion, CoercionTable, ConfigNode, ConvResult, ConversionChecker,
10    DecisionNode, Either2, Fixture, FlatSubstitution, FocusStack, LabelSet, MinHeap, NonEmptyVec,
11    PathBuf, PrefixCounter, RewriteRule, RewriteRuleSet, SimpleDag, SlidingSum, SmallMap,
12    SparseVec, StackCalc, StatSummary, Stopwatch, StringPool, TokenBucket, TransformStat,
13    TransitiveClosure, VersionedRecord, WindowIterator, WriteOnce,
14};
15
16#[cfg(test)]
17mod tests {
18    use super::*;
19    use crate::{Level, Literal, Name};
20    #[test]
21    fn test_convertible_identical() {
22        let mut checker = ConversionChecker::new();
23        let e = Expr::Lit(Literal::Nat(42));
24        assert!(checker.is_convertible(&e, &e));
25    }
26    #[test]
27    fn test_convertible_different_lits() {
28        let mut checker = ConversionChecker::new();
29        let e1 = Expr::Lit(Literal::Nat(1));
30        let e2 = Expr::Lit(Literal::Nat(2));
31        assert!(!checker.is_convertible(&e1, &e2));
32    }
33    #[test]
34    fn test_convertible_sorts() {
35        let mut checker = ConversionChecker::new();
36        let s1 = Expr::Sort(Level::zero());
37        let s2 = Expr::Sort(Level::zero());
38        assert!(checker.is_convertible(&s1, &s2));
39    }
40    #[test]
41    fn test_convertible_apps() {
42        let mut checker = ConversionChecker::new();
43        let f = Expr::Const(Name::str("f"), vec![]);
44        let a = Expr::Lit(Literal::Nat(1));
45        let app1 = Expr::App(Box::new(f.clone()), Box::new(a.clone()));
46        let app2 = Expr::App(Box::new(f), Box::new(a));
47        assert!(checker.is_convertible(&app1, &app2));
48    }
49    #[test]
50    fn test_transparency_modes() {
51        let checker = ConversionChecker::with_transparency(TransparencyMode::All);
52        assert_eq!(checker.transparency(), TransparencyMode::All);
53        let checker2 = ConversionChecker::with_transparency(TransparencyMode::None);
54        assert_eq!(checker2.transparency(), TransparencyMode::None);
55    }
56    #[test]
57    fn test_sort_equivalence() {
58        let mut checker = ConversionChecker::new();
59        let s1 = Expr::Sort(crate::Level::max(
60            crate::Level::param(Name::str("u")),
61            crate::Level::param(Name::str("v")),
62        ));
63        let s2 = Expr::Sort(crate::Level::max(
64            crate::Level::param(Name::str("v")),
65            crate::Level::param(Name::str("u")),
66        ));
67        assert!(checker.is_convertible(&s1, &s2));
68    }
69    #[test]
70    fn test_convertible_in_env() {
71        let mut checker = ConversionChecker::new();
72        let mut env = Environment::new();
73        env.add(crate::Declaration::Definition {
74            name: Name::str("answer"),
75            univ_params: vec![],
76            ty: Expr::Const(Name::str("Nat"), vec![]),
77            val: Expr::Lit(Literal::Nat(42)),
78            hint: crate::ReducibilityHint::Regular(1),
79        })
80        .expect("value should be present");
81        let answer = Expr::Const(Name::str("answer"), vec![]);
82        let forty_two = Expr::Lit(Literal::Nat(42));
83        assert!(checker.is_convertible_in_env(&answer, &forty_two, &env));
84    }
85    #[test]
86    fn test_proj_convertible() {
87        let mut checker = ConversionChecker::new();
88        let e = Expr::BVar(0);
89        let p1 = Expr::Proj(Name::str("Prod"), 0, Box::new(e.clone()));
90        let p2 = Expr::Proj(Name::str("Prod"), 0, Box::new(e));
91        assert!(checker.is_convertible(&p1, &p2));
92    }
93}
94pub(super) fn coercion_head_matches(source_ty: &crate::Expr, name: &crate::Name) -> bool {
95    let mut e = source_ty;
96    while let crate::Expr::App(f, _) = e {
97        e = f;
98    }
99    matches!(e, crate ::Expr::Const(n, _) if n == name)
100}
101/// Perform conversion checking with diagnostics.
102pub fn check_conversion(e1: &Expr, e2: &Expr, max_steps: usize) -> ConvResult {
103    let mut checker = ConversionChecker::new();
104    checker.set_max_steps(max_steps);
105    if checker.is_convertible(e1, e2) {
106        ConvResult::Equal
107    } else {
108        ConvResult::NotEqual
109    }
110}
111/// Check if two expressions are definitionally equal with a specified transparency mode.
112pub fn def_eq_with_mode(e1: &Expr, e2: &Expr, env: &Environment, mode: TransparencyMode) -> bool {
113    let mut checker = ConversionChecker::with_transparency(mode);
114    checker.is_convertible_in_env(e1, e2, env)
115}
116/// Check if two level expressions are definitionally equivalent.
117pub fn levels_def_eq(l1: &crate::Level, l2: &crate::Level) -> bool {
118    crate::level::is_equivalent(l1, l2)
119}
120/// Collect pairs of subexpressions that differ between two expressions.
121pub fn conversion_diff(e1: &Expr, e2: &Expr) -> Vec<(Expr, Expr)> {
122    let mut diffs = Vec::new();
123    collect_diffs(e1, e2, &mut diffs);
124    diffs
125}
126pub(super) fn collect_diffs(e1: &Expr, e2: &Expr, diffs: &mut Vec<(Expr, Expr)>) {
127    if e1 == e2 {
128        return;
129    }
130    match (e1, e2) {
131        (Expr::App(f1, a1), Expr::App(f2, a2)) => {
132            collect_diffs(f1, f2, diffs);
133            collect_diffs(a1, a2, diffs);
134        }
135        (Expr::Lam(_, _, ty1, b1), Expr::Lam(_, _, ty2, b2))
136        | (Expr::Pi(_, _, ty1, b1), Expr::Pi(_, _, ty2, b2)) => {
137            collect_diffs(ty1, ty2, diffs);
138            collect_diffs(b1, b2, diffs);
139        }
140        _ => {
141            diffs.push((e1.clone(), e2.clone()));
142        }
143    }
144}
145/// Compute a heuristic convertibility score between 0.0 and 1.0.
146pub fn convertibility_score(e1: &Expr, e2: &Expr) -> f64 {
147    if e1 == e2 {
148        return 1.0;
149    }
150    match (e1, e2) {
151        (Expr::App(f1, a1), Expr::App(f2, a2)) => {
152            (convertibility_score(f1, f2) + convertibility_score(a1, a2)) / 2.0
153        }
154        (Expr::Lam(_, _, ty1, b1), Expr::Lam(_, _, ty2, b2))
155        | (Expr::Pi(_, _, ty1, b1), Expr::Pi(_, _, ty2, b2)) => {
156            (convertibility_score(ty1, ty2) + convertibility_score(b1, b2)) / 2.0
157        }
158        (Expr::Const(n1, _), Expr::Const(n2, _)) if n1 == n2 => 0.9,
159        (Expr::Const(_, _), Expr::Const(_, _)) => 0.0,
160        (Expr::BVar(i1), Expr::BVar(i2)) if i1 == i2 => 1.0,
161        (Expr::BVar(_), Expr::BVar(_)) => 0.0,
162        (Expr::Sort(_), Expr::Sort(_)) => 0.8,
163        _ => 0.0,
164    }
165}
166/// Check whether two expressions have the same outermost constructor/head.
167pub fn same_head(e1: &Expr, e2: &Expr) -> bool {
168    match (e1, e2) {
169        (Expr::BVar(i1), Expr::BVar(i2)) => i1 == i2,
170        (Expr::FVar(f1), Expr::FVar(f2)) => f1 == f2,
171        (Expr::Sort(_), Expr::Sort(_)) => true,
172        (Expr::Lit(_), Expr::Lit(_)) => true,
173        (Expr::Const(n1, _), Expr::Const(n2, _)) => n1 == n2,
174        (Expr::App(_, _), Expr::App(_, _)) => true,
175        (Expr::Lam(_, _, _, _), Expr::Lam(_, _, _, _)) => true,
176        (Expr::Pi(_, _, _, _), Expr::Pi(_, _, _, _)) => true,
177        (Expr::Let(_, _, _, _), Expr::Let(_, _, _, _)) => true,
178        (Expr::Proj(n1, i1, _), Expr::Proj(n2, i2, _)) => n1 == n2 && i1 == i2,
179        _ => false,
180    }
181}
182/// Fast syntactic equality check without reduction.
183pub fn syntactic_eq(e1: &Expr, e2: &Expr) -> bool {
184    e1 == e2
185}
186/// Check whether an expression is transparency-neutral.
187pub fn is_transparency_neutral(expr: &Expr) -> bool {
188    match expr {
189        Expr::BVar(_) | Expr::FVar(_) | Expr::Sort(_) | Expr::Lit(_) => true,
190        Expr::Const(_, _) => false,
191        Expr::App(f, a) => is_transparency_neutral(f) && is_transparency_neutral(a),
192        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
193            is_transparency_neutral(ty) && is_transparency_neutral(body)
194        }
195        Expr::Let(_, ty, val, body) => {
196            is_transparency_neutral(ty)
197                && is_transparency_neutral(val)
198                && is_transparency_neutral(body)
199        }
200        Expr::Proj(_, _, e) => is_transparency_neutral(e),
201    }
202}
203#[cfg(test)]
204mod extended_tests {
205    use super::*;
206    use crate::{Level, Literal, Name};
207    #[test]
208    fn test_coercion_table_empty() {
209        let table = CoercionTable::new();
210        assert!(table.is_empty());
211    }
212    #[test]
213    fn test_coercion_table_register_and_find() {
214        let mut table = CoercionTable::new();
215        let nat = Expr::Const(Name::str("Nat"), vec![]);
216        let int = Expr::Const(Name::str("Int"), vec![]);
217        table.register(Coercion {
218            name: Name::str("Nat.toInt"),
219            source: nat,
220            target: int,
221            priority: 100,
222        });
223        let found = table.find(&Name::str("Nat"));
224        assert_eq!(found.len(), 1);
225    }
226    #[test]
227    fn test_conv_result_is_equal() {
228        assert!(ConvResult::Equal.is_equal());
229        assert!(!ConvResult::NotEqual.is_equal());
230        assert!(!ConvResult::Timeout { steps: 5 }.is_equal());
231    }
232    #[test]
233    fn test_check_conversion_equal() {
234        let e = Expr::Lit(Literal::Nat(42));
235        assert!(check_conversion(&e, &e, 1000).is_equal());
236    }
237    #[test]
238    fn test_conversion_diff_same() {
239        let e = Expr::BVar(0);
240        assert!(conversion_diff(&e, &e).is_empty());
241    }
242    #[test]
243    fn test_conversion_diff_different() {
244        let e1 = Expr::Const(Name::str("A"), vec![]);
245        let e2 = Expr::Const(Name::str("B"), vec![]);
246        assert_eq!(conversion_diff(&e1, &e2).len(), 1);
247    }
248    #[test]
249    fn test_levels_def_eq() {
250        let l1 = Level::zero();
251        let l2 = Level::zero();
252        assert!(levels_def_eq(&l1, &l2));
253    }
254    #[test]
255    fn test_convertibility_score_same() {
256        let e = Expr::Const(Name::str("Nat"), vec![]);
257        assert!((convertibility_score(&e, &e) - 1.0).abs() < 1e-9);
258    }
259    #[test]
260    fn test_same_head_sorts() {
261        let s1 = Expr::Sort(Level::zero());
262        let s2 = Expr::Sort(Level::succ(Level::zero()));
263        assert!(same_head(&s1, &s2));
264    }
265    #[test]
266    fn test_is_transparency_neutral_lit() {
267        assert!(is_transparency_neutral(&Expr::Lit(Literal::Nat(0))));
268    }
269    #[test]
270    fn test_is_transparency_neutral_const() {
271        assert!(!is_transparency_neutral(&Expr::Const(
272            Name::str("foo"),
273            vec![]
274        )));
275    }
276    #[test]
277    fn test_def_eq_with_mode() {
278        let env = Environment::new();
279        let e = Expr::Lit(Literal::Nat(42));
280        assert!(def_eq_with_mode(&e, &e, &env, TransparencyMode::Default));
281    }
282}
283/// Bounded depth search for convertibility.
284pub fn bounded_conversion(e1: &Expr, e2: &Expr, max_depth: usize) -> ConvResult {
285    if syntactic_eq(e1, e2) {
286        return ConvResult::Equal;
287    }
288    let mut checker = ConversionChecker::new();
289    for depth in 1..=max_depth {
290        checker.set_max_steps(depth * 100);
291        if checker.is_convertible(e1, e2) {
292            return ConvResult::Equal;
293        }
294    }
295    ConvResult::NotEqual
296}
297/// Check eta-equality: f and lambda x. f x are eta-equal.
298pub fn is_eta_equal(f: &Expr, g: &Expr) -> bool {
299    if let Expr::Lam(_, _, _, body) = g {
300        if let Expr::App(head, arg) = body.as_ref() {
301            if matches!(arg.as_ref(), Expr::BVar(0)) {
302                return structurally_equal_shifted(f, head, 1);
303            }
304        }
305    }
306    if let Expr::Lam(_, _, _, body) = f {
307        if let Expr::App(head, arg) = body.as_ref() {
308            if matches!(arg.as_ref(), Expr::BVar(0)) {
309                return structurally_equal_shifted(g, head, 1);
310            }
311        }
312    }
313    false
314}
315pub(super) fn structurally_equal_shifted(e1: &Expr, e2: &Expr, shift: u32) -> bool {
316    match (e1, e2) {
317        (Expr::BVar(i1), Expr::BVar(i2)) => i1 == &(*i2 + shift),
318        (Expr::Const(n1, ls1), Expr::Const(n2, ls2)) => n1 == n2 && ls1 == ls2,
319        (Expr::FVar(f1), Expr::FVar(f2)) => f1 == f2,
320        (Expr::App(f1, a1), Expr::App(f2, a2)) => {
321            structurally_equal_shifted(f1, f2, shift) && structurally_equal_shifted(a1, a2, shift)
322        }
323        (Expr::Lam(_, _, ty1, b1), Expr::Lam(_, _, ty2, b2))
324        | (Expr::Pi(_, _, ty1, b1), Expr::Pi(_, _, ty2, b2)) => {
325            structurally_equal_shifted(ty1, ty2, shift) && structurally_equal_shifted(b1, b2, shift)
326        }
327        _ => e1 == e2,
328    }
329}
330#[cfg(test)]
331mod bounded_tests {
332    use super::*;
333    use crate::{Literal, Name};
334    #[test]
335    fn test_syntactic_eq() {
336        let e = Expr::Lit(Literal::Nat(42));
337        assert!(syntactic_eq(&e, &e));
338        assert!(!syntactic_eq(&e, &Expr::Lit(Literal::Nat(43))));
339    }
340    #[test]
341    fn test_bounded_conversion_equal() {
342        let e = Expr::Lit(Literal::Nat(1));
343        assert!(bounded_conversion(&e, &e, 5).is_equal());
344    }
345    #[test]
346    fn test_bounded_conversion_not_equal() {
347        let e1 = Expr::Lit(Literal::Nat(1));
348        let e2 = Expr::Lit(Literal::Nat(2));
349        assert!(!bounded_conversion(&e1, &e2, 5).is_equal());
350    }
351    #[test]
352    fn test_same_head_different() {
353        let s = Expr::Sort(crate::Level::zero());
354        let c = Expr::Const(Name::str("X"), vec![]);
355        assert!(!same_head(&s, &c));
356    }
357    #[test]
358    fn test_same_head_lits() {
359        let l1 = Expr::Lit(Literal::Nat(1));
360        let l2 = Expr::Lit(Literal::Nat(2));
361        assert!(same_head(&l1, &l2));
362    }
363    #[test]
364    fn test_conv_result_is_definitive() {
365        assert!(ConvResult::Equal.is_definitive());
366        assert!(ConvResult::NotEqual.is_definitive());
367        assert!(!ConvResult::Timeout { steps: 0 }.is_definitive());
368    }
369    #[test]
370    fn test_coercion_priority_order() {
371        let mut table = CoercionTable::new();
372        let src = Expr::Const(crate::Name::str("A"), vec![]);
373        let tgt = Expr::Const(crate::Name::str("B"), vec![]);
374        table.register(Coercion {
375            name: crate::Name::str("low"),
376            source: src.clone(),
377            target: tgt.clone(),
378            priority: 10,
379        });
380        table.register(Coercion {
381            name: crate::Name::str("high"),
382            source: src.clone(),
383            target: tgt.clone(),
384            priority: 100,
385        });
386        let found = table.find(&crate::Name::str("A"));
387        assert_eq!(found.len(), 2);
388        assert!(found[0].priority >= found[1].priority);
389    }
390    #[test]
391    fn test_convertibility_score_diff_consts() {
392        let e1 = Expr::Const(crate::Name::str("A"), vec![]);
393        let e2 = Expr::Const(crate::Name::str("B"), vec![]);
394        assert_eq!(convertibility_score(&e1, &e2), 0.0);
395    }
396    #[test]
397    fn test_conversion_diff_app() {
398        let f = Expr::Const(crate::Name::str("f"), vec![]);
399        let a1 = Expr::BVar(0);
400        let a2 = Expr::BVar(1);
401        let app1 = Expr::App(Box::new(f.clone()), Box::new(a1));
402        let app2 = Expr::App(Box::new(f), Box::new(a2));
403        let diffs = conversion_diff(&app1, &app2);
404        assert_eq!(diffs.len(), 1);
405    }
406}
407/// Check if an expression is in "atomic" form (no reducible subexpressions).
408///
409/// Atomic expressions are: BVar, FVar, Sort, Lit, Const.
410pub fn is_atomic(expr: &Expr) -> bool {
411    matches!(
412        expr,
413        Expr::BVar(_) | Expr::FVar(_) | Expr::Sort(_) | Expr::Lit(_) | Expr::Const(_, _)
414    )
415}
416/// Count the number of distinct free variables in an expression.
417pub fn count_free_vars(expr: &Expr) -> usize {
418    let mut seen = std::collections::HashSet::new();
419    count_fvars_impl(expr, &mut seen);
420    seen.len()
421}
422pub(super) fn count_fvars_impl(expr: &Expr, seen: &mut std::collections::HashSet<crate::FVarId>) {
423    match expr {
424        Expr::FVar(id) => {
425            seen.insert(*id);
426        }
427        Expr::App(f, a) => {
428            count_fvars_impl(f, seen);
429            count_fvars_impl(a, seen);
430        }
431        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
432            count_fvars_impl(ty, seen);
433            count_fvars_impl(body, seen);
434        }
435        Expr::Let(_, ty, val, body) => {
436            count_fvars_impl(ty, seen);
437            count_fvars_impl(val, seen);
438            count_fvars_impl(body, seen);
439        }
440        Expr::Proj(_, _, e) => count_fvars_impl(e, seen),
441        _ => {}
442    }
443}
444#[cfg(test)]
445mod atomic_tests {
446    use super::*;
447    use crate::{FVarId, Literal, Name};
448    #[test]
449    fn test_is_atomic_bvar() {
450        assert!(is_atomic(&Expr::BVar(0)));
451    }
452    #[test]
453    fn test_is_atomic_app() {
454        let app = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(1)));
455        assert!(!is_atomic(&app));
456    }
457    #[test]
458    fn test_count_free_vars_none() {
459        assert_eq!(count_free_vars(&Expr::BVar(0)), 0);
460    }
461    #[test]
462    fn test_count_free_vars_one() {
463        let e = Expr::FVar(FVarId(1));
464        assert_eq!(count_free_vars(&e), 1);
465    }
466    #[test]
467    fn test_count_free_vars_dedup() {
468        let fv = Expr::FVar(FVarId(1));
469        let app = Expr::App(Box::new(fv.clone()), Box::new(fv));
470        assert_eq!(count_free_vars(&app), 1);
471    }
472    #[test]
473    fn test_is_eta_equal_basic() {
474        let f = Expr::Const(Name::str("f"), vec![]);
475        let lam = Expr::Lam(
476            crate::BinderInfo::Default,
477            Name::str("x"),
478            Box::new(Expr::Sort(crate::Level::zero())),
479            Box::new(Expr::App(Box::new(Expr::BVar(1)), Box::new(Expr::BVar(0)))),
480        );
481        let _ = is_eta_equal(&f, &lam);
482    }
483    #[test]
484    fn test_is_atomic_lit() {
485        assert!(is_atomic(&Expr::Lit(Literal::Nat(42))));
486    }
487    #[test]
488    fn test_is_atomic_const() {
489        assert!(is_atomic(&Expr::Const(Name::str("Nat"), vec![])));
490    }
491}
492/// Check if an expression has no subterms at all (is completely atomic).
493pub fn is_leaf(expr: &Expr) -> bool {
494    is_atomic(expr)
495}
496/// Check if two expressions are syntactically equal (alias for syntactic_eq).
497pub fn exprs_equal(e1: &Expr, e2: &Expr) -> bool {
498    syntactic_eq(e1, e2)
499}
500/// Check if an expression structurally "contains" another as a subterm.
501#[allow(dead_code)]
502pub fn contains_subterm(haystack: &Expr, needle: &Expr) -> bool {
503    if haystack == needle {
504        return true;
505    }
506    match haystack {
507        Expr::App(f, a) => contains_subterm(f, needle) || contains_subterm(a, needle),
508        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
509            contains_subterm(ty, needle) || contains_subterm(body, needle)
510        }
511        Expr::Let(_, ty, val, body) => {
512            contains_subterm(ty, needle)
513                || contains_subterm(val, needle)
514                || contains_subterm(body, needle)
515        }
516        Expr::Proj(_, _, e) => contains_subterm(e, needle),
517        _ => false,
518    }
519}
520/// Compute the "edit distance" between two expressions as a rough
521/// measure of how different they are structurally.
522///
523/// Returns 0 for identical expressions.
524#[allow(dead_code)]
525pub fn structural_distance(e1: &Expr, e2: &Expr) -> usize {
526    if e1 == e2 {
527        return 0;
528    }
529    match (e1, e2) {
530        (Expr::App(f1, a1), Expr::App(f2, a2)) => {
531            structural_distance(f1, f2) + structural_distance(a1, a2)
532        }
533        (Expr::Lam(_, _, ty1, b1), Expr::Lam(_, _, ty2, b2))
534        | (Expr::Pi(_, _, ty1, b1), Expr::Pi(_, _, ty2, b2)) => {
535            structural_distance(ty1, ty2) + structural_distance(b1, b2)
536        }
537        (Expr::Let(_, ty1, v1, b1), Expr::Let(_, ty2, v2, b2)) => {
538            structural_distance(ty1, ty2)
539                + structural_distance(v1, v2)
540                + structural_distance(b1, b2)
541        }
542        _ => 1,
543    }
544}
545/// Check if two expressions differ only in binder names (alpha-equivalent
546/// at the surface level, without substitution).
547#[allow(dead_code)]
548pub fn alpha_similar(e1: &Expr, e2: &Expr) -> bool {
549    match (e1, e2) {
550        (Expr::BVar(i1), Expr::BVar(i2)) => i1 == i2,
551        (Expr::FVar(f1), Expr::FVar(f2)) => f1 == f2,
552        (Expr::Const(n1, ls1), Expr::Const(n2, ls2)) => n1 == n2 && ls1 == ls2,
553        (Expr::Sort(l1), Expr::Sort(l2)) => crate::level::is_equivalent(l1, l2),
554        (Expr::Lit(l1), Expr::Lit(l2)) => l1 == l2,
555        (Expr::App(f1, a1), Expr::App(f2, a2)) => alpha_similar(f1, f2) && alpha_similar(a1, a2),
556        (Expr::Lam(bi1, _, ty1, b1), Expr::Lam(bi2, _, ty2, b2)) => {
557            bi1 == bi2 && alpha_similar(ty1, ty2) && alpha_similar(b1, b2)
558        }
559        (Expr::Pi(bi1, _, ty1, b1), Expr::Pi(bi2, _, ty2, b2)) => {
560            bi1 == bi2 && alpha_similar(ty1, ty2) && alpha_similar(b1, b2)
561        }
562        (Expr::Let(_, ty1, v1, b1), Expr::Let(_, ty2, v2, b2)) => {
563            alpha_similar(ty1, ty2) && alpha_similar(v1, v2) && alpha_similar(b1, b2)
564        }
565        (Expr::Proj(n1, i1, e1), Expr::Proj(n2, i2, e2)) => {
566            n1 == n2 && i1 == i2 && alpha_similar(e1, e2)
567        }
568        _ => false,
569    }
570}
571/// Depth of an expression tree.
572#[allow(dead_code)]
573pub fn expr_depth(expr: &Expr) -> usize {
574    match expr {
575        Expr::BVar(_) | Expr::FVar(_) | Expr::Sort(_) | Expr::Const(_, _) | Expr::Lit(_) => 0,
576        Expr::App(f, a) => 1 + expr_depth(f).max(expr_depth(a)),
577        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
578            1 + expr_depth(ty).max(expr_depth(body))
579        }
580        Expr::Let(_, ty, val, body) => {
581            1 + expr_depth(ty).max(expr_depth(val)).max(expr_depth(body))
582        }
583        Expr::Proj(_, _, e) => 1 + expr_depth(e),
584    }
585}
586/// Count total number of nodes in an expression tree.
587#[allow(dead_code)]
588pub fn expr_size(expr: &Expr) -> usize {
589    match expr {
590        Expr::BVar(_) | Expr::FVar(_) | Expr::Sort(_) | Expr::Const(_, _) | Expr::Lit(_) => 1,
591        Expr::App(f, a) => 1 + expr_size(f) + expr_size(a),
592        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => 1 + expr_size(ty) + expr_size(body),
593        Expr::Let(_, ty, val, body) => 1 + expr_size(ty) + expr_size(val) + expr_size(body),
594        Expr::Proj(_, _, e) => 1 + expr_size(e),
595    }
596}
597/// Check whether an expression is in normal form: no beta-redexes at top level.
598#[allow(dead_code)]
599pub fn is_beta_normal(expr: &Expr) -> bool {
600    match expr {
601        Expr::App(f, _) => !matches!(f.as_ref(), Expr::Lam(_, _, _, _)),
602        _ => true,
603    }
604}
605#[cfg(test)]
606mod extra_conv_tests {
607    use super::*;
608    use crate::{Literal, Name};
609    #[test]
610    fn test_contains_subterm_self() {
611        let e = Expr::Const(Name::str("Nat"), vec![]);
612        assert!(contains_subterm(&e, &e));
613    }
614    #[test]
615    fn test_contains_subterm_inside_app() {
616        let needle = Expr::BVar(0);
617        let e = Expr::App(
618            Box::new(Expr::Const(Name::str("f"), vec![])),
619            Box::new(needle.clone()),
620        );
621        assert!(contains_subterm(&e, &needle));
622    }
623    #[test]
624    fn test_structural_distance_same() {
625        let e = Expr::Lit(Literal::Nat(1));
626        assert_eq!(structural_distance(&e, &e), 0);
627    }
628    #[test]
629    fn test_structural_distance_diff() {
630        let e1 = Expr::Const(Name::str("A"), vec![]);
631        let e2 = Expr::Const(Name::str("B"), vec![]);
632        assert_eq!(structural_distance(&e1, &e2), 1);
633    }
634    #[test]
635    fn test_alpha_similar_same() {
636        let e = Expr::BVar(0);
637        assert!(alpha_similar(&e, &e));
638    }
639    #[test]
640    fn test_expr_depth_leaf() {
641        assert_eq!(expr_depth(&Expr::BVar(0)), 0);
642    }
643    #[test]
644    fn test_expr_depth_app() {
645        let app = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(1)));
646        assert_eq!(expr_depth(&app), 1);
647    }
648    #[test]
649    fn test_expr_size_leaf() {
650        assert_eq!(expr_size(&Expr::BVar(0)), 1);
651    }
652    #[test]
653    fn test_expr_size_app() {
654        let app = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(1)));
655        assert_eq!(expr_size(&app), 3);
656    }
657    #[test]
658    fn test_is_beta_normal_const() {
659        assert!(is_beta_normal(&Expr::Const(Name::str("f"), vec![])));
660    }
661    #[test]
662    fn test_is_beta_normal_app_not_lam() {
663        let app = Expr::App(
664            Box::new(Expr::Const(Name::str("f"), vec![])),
665            Box::new(Expr::BVar(0)),
666        );
667        assert!(is_beta_normal(&app));
668    }
669    #[test]
670    fn test_is_beta_normal_redex() {
671        use crate::{BinderInfo, Level};
672        let lam = Expr::Lam(
673            BinderInfo::Default,
674            Name::str("x"),
675            Box::new(Expr::Sort(Level::zero())),
676            Box::new(Expr::BVar(0)),
677        );
678        let redex = Expr::App(Box::new(lam), Box::new(Expr::BVar(0)));
679        assert!(!is_beta_normal(&redex));
680    }
681    #[test]
682    fn test_coercion_table_clear() {
683        let mut table = CoercionTable::new();
684        table.register(Coercion {
685            name: Name::str("f"),
686            source: Expr::Const(Name::str("A"), vec![]),
687            target: Expr::Const(Name::str("B"), vec![]),
688            priority: 1,
689        });
690        assert_eq!(table.len(), 1);
691        table.clear();
692        assert!(table.is_empty());
693    }
694    #[test]
695    fn test_alpha_similar_app() {
696        let e1 = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(1)));
697        let e2 = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(1)));
698        assert!(alpha_similar(&e1, &e2));
699    }
700    #[test]
701    fn test_structural_distance_nested() {
702        let e1 = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(1)));
703        let e2 = Expr::App(Box::new(Expr::BVar(0)), Box::new(Expr::BVar(2)));
704        assert_eq!(structural_distance(&e1, &e2), 1);
705    }
706}
707#[cfg(test)]
708mod tests_padding_infra {
709    use super::*;
710    #[test]
711    fn test_stat_summary() {
712        let mut ss = StatSummary::new();
713        ss.record(10.0);
714        ss.record(20.0);
715        ss.record(30.0);
716        assert_eq!(ss.count(), 3);
717        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
718        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
719        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
720    }
721    #[test]
722    fn test_transform_stat() {
723        let mut ts = TransformStat::new();
724        ts.record_before(100.0);
725        ts.record_after(80.0);
726        let ratio = ts.mean_ratio().expect("ratio should be present");
727        assert!((ratio - 0.8).abs() < 1e-9);
728    }
729    #[test]
730    fn test_small_map() {
731        let mut m: SmallMap<u32, &str> = SmallMap::new();
732        m.insert(3, "three");
733        m.insert(1, "one");
734        m.insert(2, "two");
735        assert_eq!(m.get(&2), Some(&"two"));
736        assert_eq!(m.len(), 3);
737        let keys = m.keys();
738        assert_eq!(*keys[0], 1);
739        assert_eq!(*keys[2], 3);
740    }
741    #[test]
742    fn test_label_set() {
743        let mut ls = LabelSet::new();
744        ls.add("foo");
745        ls.add("bar");
746        ls.add("foo");
747        assert_eq!(ls.count(), 2);
748        assert!(ls.has("bar"));
749        assert!(!ls.has("baz"));
750    }
751    #[test]
752    fn test_config_node() {
753        let mut root = ConfigNode::section("root");
754        let child = ConfigNode::leaf("key", "value");
755        root.add_child(child);
756        assert_eq!(root.num_children(), 1);
757    }
758    #[test]
759    fn test_versioned_record() {
760        let mut vr = VersionedRecord::new(0u32);
761        vr.update(1);
762        vr.update(2);
763        assert_eq!(*vr.current(), 2);
764        assert_eq!(vr.version(), 2);
765        assert!(vr.has_history());
766        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
767    }
768    #[test]
769    fn test_simple_dag() {
770        let mut dag = SimpleDag::new(4);
771        dag.add_edge(0, 1);
772        dag.add_edge(1, 2);
773        dag.add_edge(2, 3);
774        assert!(dag.can_reach(0, 3));
775        assert!(!dag.can_reach(3, 0));
776        let order = dag.topological_sort().expect("order should be present");
777        assert_eq!(order, vec![0, 1, 2, 3]);
778    }
779    #[test]
780    fn test_focus_stack() {
781        let mut fs: FocusStack<&str> = FocusStack::new();
782        fs.focus("a");
783        fs.focus("b");
784        assert_eq!(fs.current(), Some(&"b"));
785        assert_eq!(fs.depth(), 2);
786        fs.blur();
787        assert_eq!(fs.current(), Some(&"a"));
788    }
789}
790#[cfg(test)]
791mod tests_extra_iterators {
792    use super::*;
793    #[test]
794    fn test_window_iterator() {
795        let data = vec![1u32, 2, 3, 4, 5];
796        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
797        assert_eq!(windows.len(), 3);
798        assert_eq!(windows[0], &[1, 2, 3]);
799        assert_eq!(windows[2], &[3, 4, 5]);
800    }
801    #[test]
802    fn test_non_empty_vec() {
803        let mut nev = NonEmptyVec::singleton(10u32);
804        nev.push(20);
805        nev.push(30);
806        assert_eq!(nev.len(), 3);
807        assert_eq!(*nev.first(), 10);
808        assert_eq!(*nev.last(), 30);
809    }
810}
811#[cfg(test)]
812mod tests_padding2 {
813    use super::*;
814    #[test]
815    fn test_sliding_sum() {
816        let mut ss = SlidingSum::new(3);
817        ss.push(1.0);
818        ss.push(2.0);
819        ss.push(3.0);
820        assert!((ss.sum() - 6.0).abs() < 1e-9);
821        ss.push(4.0);
822        assert!((ss.sum() - 9.0).abs() < 1e-9);
823        assert_eq!(ss.count(), 3);
824    }
825    #[test]
826    fn test_path_buf() {
827        let mut pb = PathBuf::new();
828        pb.push("src");
829        pb.push("main");
830        assert_eq!(pb.as_str(), "src/main");
831        assert_eq!(pb.depth(), 2);
832        pb.pop();
833        assert_eq!(pb.as_str(), "src");
834    }
835    #[test]
836    fn test_string_pool() {
837        let mut pool = StringPool::new();
838        let s = pool.take();
839        assert!(s.is_empty());
840        pool.give("hello".to_string());
841        let s2 = pool.take();
842        assert!(s2.is_empty());
843        assert_eq!(pool.free_count(), 0);
844    }
845    #[test]
846    fn test_transitive_closure() {
847        let mut tc = TransitiveClosure::new(4);
848        tc.add_edge(0, 1);
849        tc.add_edge(1, 2);
850        tc.add_edge(2, 3);
851        assert!(tc.can_reach(0, 3));
852        assert!(!tc.can_reach(3, 0));
853        let r = tc.reachable_from(0);
854        assert_eq!(r.len(), 4);
855    }
856    #[test]
857    fn test_token_bucket() {
858        let mut tb = TokenBucket::new(100, 10);
859        assert_eq!(tb.available(), 100);
860        assert!(tb.try_consume(50));
861        assert_eq!(tb.available(), 50);
862        assert!(!tb.try_consume(60));
863        assert_eq!(tb.capacity(), 100);
864    }
865    #[test]
866    fn test_rewrite_rule_set() {
867        let mut rrs = RewriteRuleSet::new();
868        rrs.add(RewriteRule::unconditional(
869            "beta",
870            "App(Lam(x, b), v)",
871            "b[x:=v]",
872        ));
873        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
874        assert_eq!(rrs.len(), 2);
875        assert_eq!(rrs.unconditional_rules().len(), 1);
876        assert_eq!(rrs.conditional_rules().len(), 1);
877        assert!(rrs.get("beta").is_some());
878        let disp = rrs
879            .get("beta")
880            .expect("element at \'beta\' should exist")
881            .display();
882        assert!(disp.contains("→"));
883    }
884}
885#[cfg(test)]
886mod tests_padding3 {
887    use super::*;
888    #[test]
889    fn test_decision_node() {
890        let tree = DecisionNode::Branch {
891            key: "x".into(),
892            val: "1".into(),
893            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
894            no_branch: Box::new(DecisionNode::Leaf("no".into())),
895        };
896        let mut ctx = std::collections::HashMap::new();
897        ctx.insert("x".into(), "1".into());
898        assert_eq!(tree.evaluate(&ctx), "yes");
899        ctx.insert("x".into(), "2".into());
900        assert_eq!(tree.evaluate(&ctx), "no");
901        assert_eq!(tree.depth(), 1);
902    }
903    #[test]
904    fn test_flat_substitution() {
905        let mut sub = FlatSubstitution::new();
906        sub.add("foo", "bar");
907        sub.add("baz", "qux");
908        assert_eq!(sub.apply("foo and baz"), "bar and qux");
909        assert_eq!(sub.len(), 2);
910    }
911    #[test]
912    fn test_stopwatch() {
913        let mut sw = Stopwatch::start();
914        sw.split();
915        sw.split();
916        assert_eq!(sw.num_splits(), 2);
917        assert!(sw.elapsed_ms() >= 0.0);
918        for &s in sw.splits() {
919            assert!(s >= 0.0);
920        }
921    }
922    #[test]
923    fn test_either2() {
924        let e: Either2<i32, &str> = Either2::First(42);
925        assert!(e.is_first());
926        let mapped = e.map_first(|x| x * 2);
927        assert_eq!(mapped.first(), Some(84));
928        let e2: Either2<i32, &str> = Either2::Second("hello");
929        assert!(e2.is_second());
930        assert_eq!(e2.second(), Some("hello"));
931    }
932    #[test]
933    fn test_write_once() {
934        let wo: WriteOnce<u32> = WriteOnce::new();
935        assert!(!wo.is_written());
936        assert!(wo.write(42));
937        assert!(!wo.write(99));
938        assert_eq!(wo.read(), Some(42));
939    }
940    #[test]
941    fn test_sparse_vec() {
942        let mut sv: SparseVec<i32> = SparseVec::new(100);
943        sv.set(5, 10);
944        sv.set(50, 20);
945        assert_eq!(*sv.get(5), 10);
946        assert_eq!(*sv.get(50), 20);
947        assert_eq!(*sv.get(0), 0);
948        assert_eq!(sv.nnz(), 2);
949        sv.set(5, 0);
950        assert_eq!(sv.nnz(), 1);
951    }
952    #[test]
953    fn test_stack_calc() {
954        let mut calc = StackCalc::new();
955        calc.push(3);
956        calc.push(4);
957        calc.add();
958        assert_eq!(calc.peek(), Some(7));
959        calc.push(2);
960        calc.mul();
961        assert_eq!(calc.peek(), Some(14));
962    }
963}
964#[cfg(test)]
965mod tests_final_padding {
966    use super::*;
967    #[test]
968    fn test_min_heap() {
969        let mut h = MinHeap::new();
970        h.push(5u32);
971        h.push(1u32);
972        h.push(3u32);
973        assert_eq!(h.peek(), Some(&1));
974        assert_eq!(h.pop(), Some(1));
975        assert_eq!(h.pop(), Some(3));
976        assert_eq!(h.pop(), Some(5));
977        assert!(h.is_empty());
978    }
979    #[test]
980    fn test_prefix_counter() {
981        let mut pc = PrefixCounter::new();
982        pc.record("hello");
983        pc.record("help");
984        pc.record("world");
985        assert_eq!(pc.count_with_prefix("hel"), 2);
986        assert_eq!(pc.count_with_prefix("wor"), 1);
987        assert_eq!(pc.count_with_prefix("xyz"), 0);
988    }
989    #[test]
990    fn test_fixture() {
991        let mut f = Fixture::new();
992        f.set("key1", "val1");
993        f.set("key2", "val2");
994        assert_eq!(f.get("key1"), Some("val1"));
995        assert_eq!(f.get("key3"), None);
996        assert_eq!(f.len(), 2);
997    }
998}
999#[cfg(test)]
1000mod tests_tiny_padding {
1001    use super::*;
1002    #[test]
1003    fn test_bitset64() {
1004        let mut bs = BitSet64::new();
1005        bs.insert(0);
1006        bs.insert(63);
1007        assert!(bs.contains(0));
1008        assert!(bs.contains(63));
1009        assert!(!bs.contains(1));
1010        assert_eq!(bs.len(), 2);
1011        bs.remove(0);
1012        assert!(!bs.contains(0));
1013    }
1014    #[test]
1015    fn test_bucket_counter() {
1016        let mut bc: BucketCounter<4> = BucketCounter::new();
1017        bc.inc(0);
1018        bc.inc(0);
1019        bc.inc(1);
1020        assert_eq!(bc.get(0), 2);
1021        assert_eq!(bc.total(), 3);
1022        assert_eq!(bc.argmax(), 0);
1023    }
1024}
oxilean_kernel/conversion/functions.rs

oxilean_kernel/conversion/
functions.rs
