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

oxilean_kernel/conversion/
functions.rs
