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

oxilean_kernel/conversion/
functions.rs
