oxilean_kernel/type_erasure/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::types::{
6    AnfConverter, EraseConfig, ErasedAst, ErasedBetaReducer, ErasedBitOps, ErasedCallSite,
7    ErasedClosureEnv, ErasedCodegen, ErasedConstantPool, ErasedDCE, ErasedDecl, ErasedEnv,
8    ErasedExpr, ErasedExprExt, ErasedFlatApp, ErasedHeapObj, ErasedInliner, ErasedInterpreter,
9    ErasedLetChain, ErasedLiveness, ErasedMatchArm, ErasedModule, ErasedNormalizer,
10    ErasedOptimizer, ErasedPattern, ErasedPrinter, ErasedReachability, ErasedRenamer, ErasedScope,
11    ErasedSizeBound, ErasedStack, ErasedSubstMap, ErasedTupleOps, ErasedTypeMap, ErasedValue,
12    ErasureContext, ErasurePass, ErasureStats, TypeEraser,
13};
14
15/// Substitute `TypeErased` for `BVar(target)` in an erased expression.
16///
17/// De Bruijn shifting is not implemented here for simplicity; this is
18/// a best-effort helper used during optimisation.
19pub(super) fn subst_bvar(expr: ErasedExpr, target: u32, replacement: &ErasedExpr) -> ErasedExpr {
20    match expr {
21        ErasedExpr::BVar(i) if i == target => replacement.clone(),
22        ErasedExpr::Lam(body) => {
23            ErasedExpr::Lam(Box::new(subst_bvar(*body, target + 1, replacement)))
24        }
25        ErasedExpr::App(f, arg) => ErasedExpr::App(
26            Box::new(subst_bvar(*f, target, replacement)),
27            Box::new(subst_bvar(*arg, target, replacement)),
28        ),
29        ErasedExpr::Let(val, body) => ErasedExpr::Let(
30            Box::new(subst_bvar(*val, target, replacement)),
31            Box::new(subst_bvar(*body, target + 1, replacement)),
32        ),
33        other => other,
34    }
35}
36#[cfg(test)]
37mod tests {
38    use super::*;
39    #[test]
40    fn test_erase_config_default() {
41        let cfg = EraseConfig::default();
42        assert!(!cfg.keep_props);
43        assert!(!cfg.inline_defs);
44    }
45    #[test]
46    fn test_erase_sort() {
47        let eraser = TypeEraser::new();
48        assert_eq!(eraser.erase_sort(), ErasedExpr::TypeErased);
49    }
50    #[test]
51    fn test_erase_pi() {
52        let eraser = TypeEraser::new();
53        assert_eq!(eraser.erase_pi(), ErasedExpr::TypeErased);
54    }
55    #[test]
56    fn test_erase_lam() {
57        let eraser = TypeEraser::new();
58        let body = ErasedExpr::BVar(0);
59        let lam = eraser.erase_lam_body(body.clone());
60        assert_eq!(lam, ErasedExpr::Lam(Box::new(body)));
61    }
62    #[test]
63    fn test_erase_app() {
64        let f = ErasedExpr::Var("f".to_string());
65        let arg = ErasedExpr::Lit(42);
66        let app = TypeEraser::erase_app(f.clone(), arg.clone());
67        assert_eq!(app, ErasedExpr::App(Box::new(f), Box::new(arg)));
68    }
69    #[test]
70    fn test_erase_lit() {
71        assert_eq!(TypeEraser::erase_lit(0), ErasedExpr::Lit(0));
72        assert_eq!(TypeEraser::erase_lit(999), ErasedExpr::Lit(999));
73    }
74    #[test]
75    fn test_erasure_stats_ratio() {
76        let mut stats = ErasureStats::new();
77        assert_eq!(stats.ratio_erased(), 0.0);
78        stats.add_sort();
79        stats.add_pi();
80        stats.add_term();
81        stats.add_term();
82        assert!((stats.ratio_erased() - 0.5).abs() < 1e-10);
83    }
84    #[test]
85    fn test_optimize_type_erased() {
86        let eraser = TypeEraser::new();
87        let app = ErasedExpr::App(
88            Box::new(ErasedExpr::TypeErased),
89            Box::new(ErasedExpr::Lit(1)),
90        );
91        assert_eq!(eraser.optimize(app), ErasedExpr::TypeErased);
92        let lam_body = ErasedExpr::BVar(0);
93        let lam = ErasedExpr::Lam(Box::new(lam_body));
94        let app2 = ErasedExpr::App(Box::new(lam), Box::new(ErasedExpr::TypeErased));
95        assert_eq!(eraser.optimize(app2), ErasedExpr::TypeErased);
96        assert_eq!(eraser.optimize(ErasedExpr::Lit(7)), ErasedExpr::Lit(7));
97    }
98}
99/// Substitute BVar(0) with `replacement` in `expr`, shifting free variables.
100#[allow(dead_code)]
101pub fn subst_bvar0(expr: ErasedExprExt, replacement: ErasedExprExt) -> ErasedExprExt {
102    subst_bvar_rec(expr, 0, &replacement, 0)
103}
104pub(super) fn subst_bvar_rec(
105    expr: ErasedExprExt,
106    target: u32,
107    replacement: &ErasedExprExt,
108    depth: u32,
109) -> ErasedExprExt {
110    match expr {
111        ErasedExprExt::BVar(i) => {
112            if i == target + depth {
113                shift_up(replacement.clone(), depth)
114            } else if i > target + depth {
115                ErasedExprExt::BVar(i - 1)
116            } else {
117                ErasedExprExt::BVar(i)
118            }
119        }
120        ErasedExprExt::Lam(b) => {
121            ErasedExprExt::Lam(Box::new(subst_bvar_rec(*b, target, replacement, depth + 1)))
122        }
123        ErasedExprExt::App(f, x) => ErasedExprExt::App(
124            Box::new(subst_bvar_rec(*f, target, replacement, depth)),
125            Box::new(subst_bvar_rec(*x, target, replacement, depth)),
126        ),
127        ErasedExprExt::Let(v, b) => ErasedExprExt::Let(
128            Box::new(subst_bvar_rec(*v, target, replacement, depth)),
129            Box::new(subst_bvar_rec(*b, target, replacement, depth + 1)),
130        ),
131        other => other,
132    }
133}
134pub(super) fn shift_up(expr: ErasedExprExt, amount: u32) -> ErasedExprExt {
135    if amount == 0 {
136        return expr;
137    }
138    match expr {
139        ErasedExprExt::BVar(i) => ErasedExprExt::BVar(i + amount),
140        ErasedExprExt::Lam(b) => ErasedExprExt::Lam(Box::new(shift_up(*b, amount))),
141        ErasedExprExt::App(f, x) => ErasedExprExt::App(
142            Box::new(shift_up(*f, amount)),
143            Box::new(shift_up(*x, amount)),
144        ),
145        ErasedExprExt::Let(v, b) => ErasedExprExt::Let(
146            Box::new(shift_up(*v, amount)),
147            Box::new(shift_up(*b, amount)),
148        ),
149        other => other,
150    }
151}
152/// Counts free variables in an erased expression.
153#[allow(dead_code)]
154pub fn count_free_vars(expr: &ErasedExprExt) -> usize {
155    count_fv_rec(expr, 0)
156}
157fn count_fv_rec(expr: &ErasedExprExt, depth: u32) -> usize {
158    match expr {
159        ErasedExprExt::BVar(i) => {
160            if *i >= depth {
161                1
162            } else {
163                0
164            }
165        }
166        ErasedExprExt::FVar(_) => 1,
167        ErasedExprExt::Lam(b) => count_fv_rec(b, depth + 1),
168        ErasedExprExt::App(f, x) => count_fv_rec(f, depth) + count_fv_rec(x, depth),
169        ErasedExprExt::Let(v, b) => count_fv_rec(v, depth) + count_fv_rec(b, depth + 1),
170        _ => 0,
171    }
172}
173/// Collects all constant references in an expression.
174#[allow(dead_code)]
175pub fn collect_consts(expr: &ErasedExprExt) -> Vec<String> {
176    let mut consts = Vec::new();
177    collect_consts_rec(expr, &mut consts);
178    consts
179}
180pub(super) fn collect_consts_rec(expr: &ErasedExprExt, out: &mut Vec<String>) {
181    match expr {
182        ErasedExprExt::Const(name) => {
183            if !out.contains(name) {
184                out.push(name.clone());
185            }
186        }
187        ErasedExprExt::Lam(b) => collect_consts_rec(b, out),
188        ErasedExprExt::App(f, x) => {
189            collect_consts_rec(f, out);
190            collect_consts_rec(x, out);
191        }
192        ErasedExprExt::Let(v, b) => {
193            collect_consts_rec(v, out);
194            collect_consts_rec(b, out);
195        }
196        _ => {}
197    }
198}
199#[cfg(test)]
200mod tests_erased_expr {
201    use super::*;
202    #[test]
203    fn test_erased_expr_size() {
204        let e = ErasedExprExt::App(
205            Box::new(ErasedExprExt::Lam(Box::new(ErasedExprExt::BVar(0)))),
206            Box::new(ErasedExprExt::Lit(42)),
207        );
208        assert_eq!(e.size(), 4);
209    }
210    #[test]
211    fn test_erased_expr_predicates() {
212        assert!(ErasedExprExt::Lit(0).is_lit());
213        assert!(ErasedExprExt::Lam(Box::new(ErasedExprExt::Unit)).is_lam());
214        assert!(ErasedExprExt::TypeErased.is_type_erased());
215    }
216    #[test]
217    fn test_subst_bvar0() {
218        let body = ErasedExprExt::BVar(0);
219        let result = subst_bvar0(body, ErasedExprExt::Lit(42));
220        assert_eq!(result, ErasedExprExt::Lit(42));
221    }
222    #[test]
223    fn test_beta_reduce_lam_app() {
224        let lam = ErasedExprExt::Lam(Box::new(ErasedExprExt::BVar(0)));
225        let app = ErasedExprExt::App(Box::new(lam), Box::new(ErasedExprExt::Lit(7)));
226        let mut reducer = ErasedBetaReducer::new(100);
227        let result = reducer.step(app);
228        assert_eq!(result, ErasedExprExt::Lit(7));
229        assert_eq!(reducer.steps, 1);
230    }
231    #[test]
232    fn test_count_free_vars() {
233        let e1 = ErasedExprExt::Lam(Box::new(ErasedExprExt::BVar(0)));
234        assert_eq!(count_free_vars(&e1), 0);
235        let e2 = ErasedExprExt::BVar(0);
236        assert_eq!(count_free_vars(&e2), 1);
237    }
238    #[test]
239    fn test_collect_consts() {
240        let e = ErasedExprExt::App(
241            Box::new(ErasedExprExt::Const("Nat.add".to_string())),
242            Box::new(ErasedExprExt::App(
243                Box::new(ErasedExprExt::Const("Nat.add".to_string())),
244                Box::new(ErasedExprExt::Lit(1)),
245            )),
246        );
247        let consts = collect_consts(&e);
248        assert_eq!(consts, vec!["Nat.add".to_string()]);
249    }
250    #[test]
251    fn test_erased_inliner() {
252        let mut inliner = ErasedInliner::new();
253        inliner.register("id", ErasedExprExt::Lam(Box::new(ErasedExprExt::BVar(0))));
254        let e = ErasedExprExt::App(
255            Box::new(ErasedExprExt::Const("id".to_string())),
256            Box::new(ErasedExprExt::Lit(99)),
257        );
258        let result = inliner.inline(e);
259        assert_eq!(inliner.inlined, 1);
260        assert!(result.is_app());
261    }
262    #[test]
263    fn test_erased_dce() {
264        let e = ErasedExprExt::App(
265            Box::new(ErasedExprExt::Lit(5)),
266            Box::new(ErasedExprExt::TypeErased),
267        );
268        let mut dce = ErasedDCE::new();
269        let result = dce.elim(e);
270        assert_eq!(result, ErasedExprExt::Lit(5));
271        assert_eq!(dce.eliminated, 1);
272    }
273    #[test]
274    fn test_erased_optimizer() {
275        let mut opt = ErasedOptimizer::new(100);
276        let lam_body = ErasedExprExt::BVar(0);
277        let lam = ErasedExprExt::App(
278            Box::new(ErasedExprExt::Lam(Box::new(lam_body))),
279            Box::new(ErasedExprExt::TypeErased),
280        );
281        let result = opt.optimize(lam);
282        assert_eq!(result, ErasedExprExt::TypeErased);
283    }
284}
285/// Pretty prints an erased expression to a string.
286#[allow(dead_code)]
287pub fn pretty_print_erased(expr: &ErasedExprExt) -> String {
288    match expr {
289        ErasedExprExt::BVar(i) => format!("#{}", i),
290        ErasedExprExt::FVar(name) => name.clone(),
291        ErasedExprExt::Lit(n) => n.to_string(),
292        ErasedExprExt::CtorTag(t) => format!("ctor({})", t),
293        ErasedExprExt::Lam(b) => format!("(λ. {})", pretty_print_erased(b)),
294        ErasedExprExt::App(f, x) => {
295            format!("({} {})", pretty_print_erased(f), pretty_print_erased(x))
296        }
297        ErasedExprExt::Const(name) => name.clone(),
298        ErasedExprExt::Let(v, b) => {
299            format!(
300                "(let {} in {})",
301                pretty_print_erased(v),
302                pretty_print_erased(b)
303            )
304        }
305        ErasedExprExt::TypeErased => "_".to_string(),
306        ErasedExprExt::Unit => "()".to_string(),
307    }
308}
309/// Computes the lambda depth of an expression.
310#[allow(dead_code)]
311pub fn lambda_depth(expr: &ErasedExprExt) -> u32 {
312    match expr {
313        ErasedExprExt::Lam(b) => 1 + lambda_depth(b),
314        ErasedExprExt::App(f, x) => lambda_depth(f).max(lambda_depth(x)),
315        ErasedExprExt::Let(v, b) => lambda_depth(v).max(lambda_depth(b)),
316        _ => 0,
317    }
318}
319/// Count the number of App nodes.
320#[allow(dead_code)]
321pub fn count_apps(expr: &ErasedExprExt) -> usize {
322    match expr {
323        ErasedExprExt::App(f, x) => 1 + count_apps(f) + count_apps(x),
324        ErasedExprExt::Lam(b) => count_apps(b),
325        ErasedExprExt::Let(v, b) => count_apps(v) + count_apps(b),
326        _ => 0,
327    }
328}
329/// Return whether BVar(0) appears free in expr at the given depth.
330#[allow(dead_code)]
331pub fn has_free_bvar(expr: &ErasedExprExt, depth: u32) -> bool {
332    match expr {
333        ErasedExprExt::BVar(i) => *i == depth,
334        ErasedExprExt::Lam(b) => has_free_bvar(b, depth + 1),
335        ErasedExprExt::App(f, x) => has_free_bvar(f, depth) || has_free_bvar(x, depth),
336        ErasedExprExt::Let(v, b) => has_free_bvar(v, depth) || has_free_bvar(b, depth + 1),
337        _ => false,
338    }
339}
340pub(super) fn is_atom(expr: &ErasedExprExt) -> bool {
341    matches!(
342        expr,
343        ErasedExprExt::BVar(_)
344            | ErasedExprExt::FVar(_)
345            | ErasedExprExt::Lit(_)
346            | ErasedExprExt::Const(_)
347            | ErasedExprExt::Unit
348            | ErasedExprExt::TypeErased
349    )
350}
351#[cfg(test)]
352mod tests_erasure_extended {
353    use super::*;
354    #[test]
355    fn test_erased_pattern_depth() {
356        let p = ErasedPattern::Ctor(
357            0,
358            vec![
359                ErasedPattern::Ctor(1, vec![ErasedPattern::Wildcard]),
360                ErasedPattern::Lit(0),
361            ],
362        );
363        assert_eq!(p.depth(), 3);
364    }
365    #[test]
366    fn test_erased_pattern_irrefutable() {
367        assert!(ErasedPattern::Wildcard.is_irrefutable());
368        assert!(ErasedPattern::Var("x".to_string()).is_irrefutable());
369        assert!(!ErasedPattern::Lit(0).is_irrefutable());
370    }
371    #[test]
372    fn test_erased_match_arm() {
373        let arm = ErasedMatchArm::new(ErasedPattern::Wildcard, ErasedExprExt::Unit);
374        assert!(arm.is_catch_all());
375        let arm2 = ErasedMatchArm::new(ErasedPattern::Lit(0), ErasedExprExt::Lit(0));
376        assert!(!arm2.is_catch_all());
377    }
378    #[test]
379    fn test_erased_module() {
380        let mut m = ErasedModule::new("Nat");
381        m.add(ErasedDecl::Def {
382            name: "zero".to_string(),
383            body: ErasedExprExt::Lit(0),
384        });
385        m.add(ErasedDecl::Axiom {
386            name: "propext".to_string(),
387        });
388        m.add(ErasedDecl::Inductive {
389            name: "Nat".to_string(),
390            ctor_count: 2,
391        });
392        assert_eq!(m.len(), 3);
393        assert_eq!(
394            m.find("zero").expect("value should be present").name(),
395            "zero"
396        );
397        assert_eq!(m.function_names(), vec!["zero"]);
398    }
399    #[test]
400    fn test_erasure_context() {
401        let mut ctx = ErasureContext::new();
402        ctx.push(true);
403        ctx.push(false);
404        assert!(!ctx.is_type_at(0));
405        assert!(ctx.is_type_at(1));
406        assert_eq!(ctx.depth(), 2);
407    }
408    #[test]
409    fn test_erased_scope() {
410        let mut scope = ErasedScope::new();
411        scope.bind("x", ErasedValue::Int(42));
412        scope.bind("y", ErasedValue::Int(7));
413        assert!(scope.lookup("x").is_some());
414        let cp = scope.save();
415        scope.bind("z", ErasedValue::Unit);
416        assert_eq!(scope.depth(), 3);
417        scope.restore(cp);
418        assert_eq!(scope.depth(), 2);
419        assert!(scope.lookup("z").is_none());
420    }
421    #[test]
422    fn test_erased_type_map() {
423        let mut m = ErasedTypeMap::new();
424        m.insert(1, ErasedExprExt::Lit(42));
425        m.insert(2, ErasedExprExt::Unit);
426        assert_eq!(m.get(1), Some(&ErasedExprExt::Lit(42)));
427        assert_eq!(m.get(99), None);
428        m.insert(1, ErasedExprExt::Lit(99));
429        assert_eq!(m.get(1), Some(&ErasedExprExt::Lit(99)));
430    }
431    #[test]
432    fn test_pretty_print_erased() {
433        let e = ErasedExprExt::App(
434            Box::new(ErasedExprExt::Const("f".to_string())),
435            Box::new(ErasedExprExt::Lit(5)),
436        );
437        assert_eq!(pretty_print_erased(&e), "(f 5)");
438        let lam = ErasedExprExt::Lam(Box::new(ErasedExprExt::BVar(0)));
439        assert_eq!(pretty_print_erased(&lam), "(λ. #0)");
440    }
441    #[test]
442    fn test_lambda_depth() {
443        let e = ErasedExprExt::Lam(Box::new(ErasedExprExt::Lam(Box::new(ErasedExprExt::BVar(
444            0,
445        )))));
446        assert_eq!(lambda_depth(&e), 2);
447    }
448    #[test]
449    fn test_count_apps() {
450        let e = ErasedExprExt::App(
451            Box::new(ErasedExprExt::App(
452                Box::new(ErasedExprExt::Const("f".to_string())),
453                Box::new(ErasedExprExt::Lit(1)),
454            )),
455            Box::new(ErasedExprExt::Lit(2)),
456        );
457        assert_eq!(count_apps(&e), 2);
458    }
459    #[test]
460    fn test_has_free_bvar() {
461        let e = ErasedExprExt::BVar(0);
462        assert!(has_free_bvar(&e, 0));
463        assert!(!has_free_bvar(&e, 1));
464        let lam = ErasedExprExt::Lam(Box::new(ErasedExprExt::BVar(0)));
465        assert!(!has_free_bvar(&lam, 0));
466    }
467    #[test]
468    fn test_anf_converter() {
469        let mut conv = AnfConverter::new();
470        let e = ErasedExprExt::App(
471            Box::new(ErasedExprExt::App(
472                Box::new(ErasedExprExt::Const("f".to_string())),
473                Box::new(ErasedExprExt::Lit(1)),
474            )),
475            Box::new(ErasedExprExt::Lit(2)),
476        );
477        let anf = conv.convert(e);
478        assert!(
479            conv.let_count > 0
480                || matches!(anf, ErasedExprExt::Let(_, _) | ErasedExprExt::App(_, _))
481        );
482    }
483    #[test]
484    fn test_erased_reachability() {
485        let mut ra = ErasedReachability::new();
486        ra.add_root("main");
487        ra.mark_reachable("helper");
488        assert!(ra.is_reachable("main"));
489        assert!(ra.is_reachable("helper"));
490        assert!(!ra.is_reachable("dead_fn"));
491        assert_eq!(ra.reachable_count(), 2);
492    }
493    #[test]
494    fn test_erased_codegen() {
495        let mut cg = ErasedCodegen::new();
496        let mut m = ErasedModule::new("Test");
497        m.add(ErasedDecl::Def {
498            name: "id".to_string(),
499            body: ErasedExprExt::Lam(Box::new(ErasedExprExt::BVar(0))),
500        });
501        cg.gen_module(&m);
502        assert!(cg.output.contains("id"));
503        assert!(cg.output.contains("fun x"));
504    }
505}
506#[cfg(test)]
507mod tests_erasure_extended2 {
508    use super::*;
509    #[test]
510    fn test_erased_interpreter_lit() {
511        let mut interp = ErasedInterpreter::new(100);
512        let result = interp.eval(ErasedExprExt::Lit(42));
513        assert_eq!(result, Some(ErasedValue::Int(42)));
514    }
515    #[test]
516    fn test_erased_interpreter_app_lam() {
517        let mut interp = ErasedInterpreter::new(100);
518        let lam = ErasedExprExt::Lam(Box::new(ErasedExprExt::BVar(0)));
519        let app = ErasedExprExt::App(Box::new(lam), Box::new(ErasedExprExt::Lit(7)));
520        let result = interp.eval(app);
521        assert_eq!(result, Some(ErasedValue::Int(7)));
522    }
523    #[test]
524    fn test_erased_heap_obj() {
525        let lit = ErasedHeapObj::Lit(42);
526        assert!(!lit.is_ctor());
527        let ctor = ErasedHeapObj::Ctor {
528            tag: 1,
529            fields: vec![],
530        };
531        assert!(ctor.is_ctor());
532        assert_eq!(ctor.ctor_tag(), Some(1));
533        let closure = ErasedHeapObj::Closure {
534            arity: 1,
535            fn_ptr: 0,
536            num_caps: 0,
537        };
538        assert!(closure.is_closure());
539        let thunk = ErasedHeapObj::Thunk { code: 999 };
540        assert!(thunk.is_thunk());
541    }
542    #[test]
543    fn test_erased_renamer() {
544        let mut r = ErasedRenamer::new(vec![("old_fn".to_string(), "new_fn".to_string())]);
545        let e = ErasedExprExt::Const("old_fn".to_string());
546        let result = r.rename(e);
547        assert_eq!(result, ErasedExprExt::Const("new_fn".to_string()));
548        assert_eq!(r.renames, 1);
549    }
550    #[test]
551    fn test_erasure_pass_pipeline() {
552        let mut pass = ErasurePass::new("test_pass");
553        let lam_body = ErasedExprExt::BVar(0);
554        let app2 = ErasedExprExt::App(
555            Box::new(ErasedExprExt::Lam(Box::new(lam_body))),
556            Box::new(ErasedExprExt::TypeErased),
557        );
558        assert_eq!(pass.run(app2), ErasedExprExt::TypeErased);
559        let plain = ErasedExprExt::Lit(7);
560        assert_eq!(pass.run(plain), ErasedExprExt::Lit(7));
561    }
562    #[test]
563    fn test_size_bound_checker() {
564        let checker = ErasedSizeBound::new(10);
565        let small = ErasedExprExt::Lit(1);
566        assert!(checker.check(&small));
567        assert_eq!(checker.size_of(&small), 1);
568        let big = ErasedExprExt::App(
569            Box::new(ErasedExprExt::Lam(Box::new(ErasedExprExt::App(
570                Box::new(ErasedExprExt::BVar(0)),
571                Box::new(ErasedExprExt::Lit(1)),
572            )))),
573            Box::new(ErasedExprExt::App(
574                Box::new(ErasedExprExt::Const("f".to_string())),
575                Box::new(ErasedExprExt::App(
576                    Box::new(ErasedExprExt::Lit(2)),
577                    Box::new(ErasedExprExt::Lit(3)),
578                )),
579            )),
580        );
581        let size = checker.size_of(&big);
582        assert!(size > 5);
583    }
584    #[test]
585    fn test_erased_printer() {
586        let mut printer = ErasedPrinter::new();
587        printer.print(&ErasedExprExt::Lit(42));
588        assert!(printer.result().contains("42"));
589        printer.clear();
590        assert!(printer.result().is_empty());
591    }
592    #[test]
593    fn test_erased_tuple_ops() {
594        let pair = ErasedTupleOps::make_pair(ErasedExprExt::Lit(1), ErasedExprExt::Lit(2));
595        let fst = ErasedTupleOps::fst(pair.clone());
596        assert!(matches!(fst, ErasedExprExt::App(_, _)));
597        let snd = ErasedTupleOps::snd(pair);
598        assert!(matches!(snd, ErasedExprExt::App(_, _)));
599        let triple = ErasedTupleOps::n_tuple(vec![
600            ErasedExprExt::Lit(1),
601            ErasedExprExt::Lit(2),
602            ErasedExprExt::Lit(3),
603        ]);
604        assert!(matches!(triple, ErasedExprExt::App(_, _)));
605    }
606}
607/// Flatten left-associated App chains into (head, [arg1, arg2, ...]).
608#[allow(dead_code)]
609pub fn flatten_apps(expr: ErasedExpr) -> (ErasedExpr, Vec<ErasedExpr>) {
610    let mut args = Vec::new();
611    let mut cur = expr;
612    loop {
613        match cur {
614            ErasedExpr::App(f, x) => {
615                args.push(*x);
616                cur = *f;
617            }
618            other => {
619                args.reverse();
620                return (other, args);
621            }
622        }
623    }
624}
625/// Build a left-associated App chain from (head, [arg1, arg2, ...]).
626#[allow(dead_code)]
627pub fn build_apps(head: ErasedExpr, args: Vec<ErasedExpr>) -> ErasedExpr {
628    args.into_iter()
629        .fold(head, |f, x| ErasedExpr::App(Box::new(f), Box::new(x)))
630}
631#[cfg(test)]
632mod tests_erasure_normalizer {
633    use super::*;
634    #[test]
635    fn test_erased_normalizer_whnf() {
636        let mut norm = ErasedNormalizer::new(100);
637        let app = ErasedExpr::App(
638            Box::new(ErasedExpr::Lam(Box::new(ErasedExpr::BVar(0)))),
639            Box::new(ErasedExpr::Lit(5)),
640        );
641        let result = norm.whnf(app);
642        assert_eq!(result, ErasedExpr::Lit(5));
643        assert_eq!(norm.beta_steps, 1);
644    }
645    #[test]
646    fn test_erased_normalizer_const_fold() {
647        let mut norm = ErasedNormalizer::new(100);
648        let add_3_4 = ErasedExpr::App(
649            Box::new(ErasedExpr::App(
650                Box::new(ErasedExpr::Const("Nat.add".to_string())),
651                Box::new(ErasedExpr::Lit(3)),
652            )),
653            Box::new(ErasedExpr::Lit(4)),
654        );
655        let result = norm.const_fold_add(add_3_4);
656        assert_eq!(result, ErasedExpr::Lit(7));
657        assert_eq!(norm.const_folds, 1);
658    }
659    #[test]
660    fn test_erased_stack() {
661        let mut stack = ErasedStack::new();
662        stack.push(ErasedExpr::Lit(1));
663        stack.push(ErasedExpr::Lit(2));
664        assert_eq!(stack.depth(), 2);
665        assert_eq!(stack.pop(), Some(ErasedExpr::Lit(2)));
666        assert_eq!(stack.peek(), Some(&ErasedExpr::Lit(1)));
667    }
668    #[test]
669    fn test_erased_env() {
670        let mut env = ErasedEnv::new();
671        env.bind("x", ErasedExpr::Lit(42));
672        env.bind("y", ErasedExpr::Lit(7));
673        assert_eq!(env.get("x"), Some(&ErasedExpr::Lit(42)));
674        assert_eq!(env.get("z"), None);
675    }
676    #[test]
677    fn test_flatten_build_apps() {
678        let expr = ErasedExpr::App(
679            Box::new(ErasedExpr::App(
680                Box::new(ErasedExpr::Const("f".to_string())),
681                Box::new(ErasedExpr::Lit(1)),
682            )),
683            Box::new(ErasedExpr::Lit(2)),
684        );
685        let (head, args) = flatten_apps(expr);
686        assert_eq!(head, ErasedExpr::Const("f".to_string()));
687        assert_eq!(args.len(), 2);
688        assert_eq!(args[0], ErasedExpr::Lit(1));
689        assert_eq!(args[1], ErasedExpr::Lit(2));
690        let rebuilt = build_apps(head, args);
691        if let ErasedExpr::App(outer, arg2) = rebuilt {
692            assert_eq!(*arg2, ErasedExpr::Lit(2));
693            if let ErasedExpr::App(inner_f, arg1) = *outer {
694                assert_eq!(*inner_f, ErasedExpr::Const("f".to_string()));
695                assert_eq!(*arg1, ErasedExpr::Lit(1));
696            }
697        }
698    }
699    #[test]
700    fn test_erased_bit_ops() {
701        assert_eq!(ErasedBitOps::fold_and(&[0xFF, 0x0F, 0x3F]), 0x0F);
702        assert_eq!(ErasedBitOps::fold_or(&[0x01, 0x02, 0x04]), 0x07);
703        assert_eq!(ErasedBitOps::fold_binop(&[1, 2, 3, 4], 0, |a, b| a + b), 10);
704    }
705}
706/// Count lambda depth in an ErasedExpr.
707#[allow(dead_code)]
708pub(super) fn erased_expr_depth(expr: &ErasedExpr) -> u32 {
709    match expr {
710        ErasedExpr::Lam(b) => 1 + erased_expr_depth(b),
711        ErasedExpr::App(f, _) => erased_expr_depth(f),
712        _ => 0,
713    }
714}
715/// Count apps in an ErasedExpr.
716#[allow(dead_code)]
717pub(super) fn erased_expr_apps(expr: &ErasedExpr) -> usize {
718    match expr {
719        ErasedExpr::App(f, x) => 1 + erased_expr_apps(f) + erased_expr_apps(x),
720        ErasedExpr::Lam(b) => erased_expr_apps(b),
721        ErasedExpr::Let(v, b) => erased_expr_apps(v) + erased_expr_apps(b),
722        _ => 0,
723    }
724}
725/// A generic transformation pass over erased expressions.
726#[allow(dead_code)]
727pub trait ErasedPass {
728    /// Name of the pass, for diagnostic output.
729    fn name(&self) -> &str;
730    /// Run the pass on `expr`, returning the (possibly transformed) result.
731    fn run(&mut self, expr: ErasedExpr) -> ErasedExpr;
732    /// Run the pass on a slice of declarations.
733    fn run_on_module(&mut self, _decls: &mut Vec<ErasedDecl>) {}
734}
735#[cfg(test)]
736mod tests_erasure_extra {
737    use super::*;
738    #[test]
739    fn test_erased_let_chain_empty() {
740        let body = ErasedExprExt::Unit;
741        let chain = ErasedLetChain::new(body);
742        assert!(chain.is_empty());
743        assert_eq!(chain.len(), 0);
744    }
745    #[test]
746    fn test_erased_let_chain_push_and_into() {
747        let body = ErasedExprExt::BVar(0);
748        let mut chain = ErasedLetChain::new(body);
749        chain.push("x", ErasedExprExt::Lit(42));
750        assert_eq!(chain.len(), 1);
751        let expr = chain.into_expr();
752        match expr {
753            ErasedExprExt::Let(rhs, _body2) => {
754                assert!(matches!(*rhs, ErasedExprExt::Lit(42)));
755            }
756            _ => panic!("expected Let"),
757        }
758    }
759    #[test]
760    fn test_closure_env_lookup() {
761        let mut env = ErasedClosureEnv::new();
762        env.capture("x", ErasedExprExt::Lit(10));
763        env.capture("y", ErasedExprExt::Lit(20));
764        assert!(env.lookup("x").is_some());
765        assert!(env.lookup("z").is_none());
766        assert_eq!(env.size(), 2);
767    }
768    #[test]
769    fn test_call_site_self_tail() {
770        let cs = ErasedCallSite::new("foo", 2, true);
771        assert!(cs.is_self_tail("foo"));
772        assert!(!cs.is_self_tail("bar"));
773    }
774    #[test]
775    fn test_liveness_merge() {
776        let mut a = ErasedLiveness::new();
777        a.mark_live(0);
778        a.mark_live(2);
779        let mut b = ErasedLiveness::new();
780        b.mark_live(1);
781        b.mark_live(2);
782        a.merge(&b);
783        assert!(a.is_live(0));
784        assert!(a.is_live(1));
785        assert!(a.is_live(2));
786        assert_eq!(a.count(), 3);
787        assert_eq!(a.max_live(), Some(2));
788    }
789    #[test]
790    fn test_constant_pool_intern() {
791        let mut pool = ErasedConstantPool::new();
792        let idx1 = pool.intern(99);
793        let idx2 = pool.intern(99);
794        assert_eq!(idx1, idx2);
795        let idx3 = pool.intern(100);
796        assert_ne!(idx1, idx3);
797        assert_eq!(pool.get(idx1), Some(99));
798        assert_eq!(pool.len(), 2);
799    }
800    #[test]
801    fn test_flat_app_round_trip() {
802        let expr = ErasedExpr::App(
803            Box::new(ErasedExpr::App(
804                Box::new(ErasedExpr::Const("f".into())),
805                Box::new(ErasedExpr::Lit(1)),
806            )),
807            Box::new(ErasedExpr::Lit(2)),
808        );
809        let flat = ErasedFlatApp::from_expr(expr);
810        assert_eq!(flat.arity(), 2);
811        let rebuilt = flat.into_expr();
812        assert!(matches!(rebuilt, ErasedExpr::App(_, _)));
813    }
814    #[test]
815    fn test_subst_map() {
816        let mut m = ErasedSubstMap::new();
817        m.insert(0, ErasedExpr::Lit(5));
818        assert!(m.get(0).is_some());
819        assert!(m.get(1).is_none());
820        assert_eq!(m.len(), 1);
821    }
822    #[test]
823    fn test_erased_ast_size() {
824        let expr = ErasedExpr::App(
825            Box::new(ErasedExpr::Const("g".into())),
826            Box::new(ErasedExpr::Lit(7)),
827        );
828        let ast = ErasedAst::new(expr, "test");
829        assert!(ast.size() >= 1);
830    }
831}
oxilean_kernel/type_erasure/functions.rs

oxilean_kernel/type_erasure/
functions.rs
