oxilean_codegen/lean4_backend/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::types::{
6    L4AnalysisCache, L4ConstantFoldingHelper, L4DepGraph, L4DominatorTree, L4ExtCache,
7    L4ExtConstFolder, L4ExtDepGraph, L4ExtDomTree, L4ExtLiveness, L4ExtPassConfig, L4ExtPassPhase,
8    L4ExtPassRegistry, L4ExtPassStats, L4ExtWorklist, L4LivenessInfo, L4PassConfig, L4PassPhase,
9    L4PassRegistry, L4PassStats, L4Worklist, Lean4Abbrev, Lean4Axiom, Lean4Backend, Lean4CalcStep,
10    Lean4Constructor, Lean4Decl, Lean4Def, Lean4DoStmt, Lean4Expr, Lean4File, Lean4Inductive,
11    Lean4Instance, Lean4Pattern, Lean4Structure, Lean4Theorem, Lean4Type,
12};
13
14/// Wrap a type in parens if it's complex (for use as an argument).
15pub(super) fn paren_type(ty: &Lean4Type) -> std::string::String {
16    match ty {
17        Lean4Type::App(_, _)
18        | Lean4Type::Fun(_, _)
19        | Lean4Type::ForAll(_, _, _)
20        | Lean4Type::List(_)
21        | Lean4Type::Option(_)
22        | Lean4Type::Prod(_, _)
23        | Lean4Type::Sum(_, _)
24        | Lean4Type::IO(_)
25        | Lean4Type::Array(_)
26        | Lean4Type::Fin(_) => format!("({})", ty),
27        _ => ty.to_string(),
28    }
29}
30/// Wrap a type in parens for product/sum (avoids ambiguity with →).
31pub(super) fn paren_complex_type(ty: &Lean4Type) -> std::string::String {
32    match ty {
33        Lean4Type::Fun(_, _) | Lean4Type::ForAll(_, _, _) => format!("({})", ty),
34        _ => ty.to_string(),
35    }
36}
37/// Wrap a function domain in parens if it's also a function.
38pub(super) fn paren_fun_type(ty: &Lean4Type) -> std::string::String {
39    match ty {
40        Lean4Type::Fun(_, _) | Lean4Type::ForAll(_, _, _) => format!("({})", ty),
41        _ => ty.to_string(),
42    }
43}
44/// Wrap an expression in parens if it is complex.
45pub(super) fn paren_expr(e: &Lean4Expr) -> std::string::String {
46    match e {
47        Lean4Expr::App(_, _)
48        | Lean4Expr::Lambda(_, _, _)
49        | Lean4Expr::If(_, _, _)
50        | Lean4Expr::Let(_, _, _, _)
51        | Lean4Expr::LetRec(_, _, _)
52        | Lean4Expr::Match(_, _)
53        | Lean4Expr::Have(_, _, _, _)
54        | Lean4Expr::Show(_, _)
55        | Lean4Expr::Do(_)
56        | Lean4Expr::Calc(_)
57        | Lean4Expr::ByTactic(_) => format!("({})", e),
58        _ => e.to_string(),
59    }
60}
61/// Wrap a pattern in parens if complex.
62pub(super) fn paren_pattern(p: &Lean4Pattern) -> std::string::String {
63    match p {
64        Lean4Pattern::Ctor(_, args) if !args.is_empty() => format!("({})", p),
65        Lean4Pattern::Or(_, _) => format!("({})", p),
66        _ => p.to_string(),
67    }
68}
69#[cfg(test)]
70mod tests {
71    use super::*;
72    #[test]
73    pub(super) fn test_type_nat() {
74        assert_eq!(Lean4Type::Nat.to_string(), "Nat");
75    }
76    #[test]
77    pub(super) fn test_type_bool() {
78        assert_eq!(Lean4Type::Bool.to_string(), "Bool");
79    }
80    #[test]
81    pub(super) fn test_type_prop() {
82        assert_eq!(Lean4Type::Prop.to_string(), "Prop");
83    }
84    #[test]
85    pub(super) fn test_type_type_zero() {
86        assert_eq!(Lean4Type::Type(0).to_string(), "Type");
87    }
88    #[test]
89    pub(super) fn test_type_type_nonzero() {
90        assert_eq!(Lean4Type::Type(1).to_string(), "Type 1");
91    }
92    #[test]
93    pub(super) fn test_type_list() {
94        let ty = Lean4Type::List(Box::new(Lean4Type::Nat));
95        assert_eq!(ty.to_string(), "List Nat");
96    }
97    #[test]
98    pub(super) fn test_type_option() {
99        let ty = Lean4Type::Option(Box::new(Lean4Type::Int));
100        assert_eq!(ty.to_string(), "Option Int");
101    }
102    #[test]
103    pub(super) fn test_type_prod() {
104        let ty = Lean4Type::Prod(Box::new(Lean4Type::Nat), Box::new(Lean4Type::Bool));
105        assert_eq!(ty.to_string(), "Nat × Bool");
106    }
107    #[test]
108    pub(super) fn test_type_fun() {
109        let ty = Lean4Type::Fun(Box::new(Lean4Type::Nat), Box::new(Lean4Type::Bool));
110        assert_eq!(ty.to_string(), "Nat → Bool");
111    }
112    #[test]
113    pub(super) fn test_type_forall() {
114        let ty = Lean4Type::ForAll(
115            "n".to_string(),
116            Box::new(Lean4Type::Nat),
117            Box::new(Lean4Type::Prop),
118        );
119        assert_eq!(ty.to_string(), "∀ (n : Nat), Prop");
120    }
121    #[test]
122    pub(super) fn test_type_io() {
123        let ty = Lean4Type::IO(Box::new(Lean4Type::Unit));
124        assert_eq!(ty.to_string(), "IO Unit");
125    }
126    #[test]
127    pub(super) fn test_type_array() {
128        let ty = Lean4Type::Array(Box::new(Lean4Type::Float));
129        assert_eq!(ty.to_string(), "Array Float");
130    }
131    #[test]
132    pub(super) fn test_expr_var() {
133        let e = Lean4Expr::Var("x".to_string());
134        assert_eq!(e.to_string(), "x");
135    }
136    #[test]
137    pub(super) fn test_expr_nat_lit() {
138        let e = Lean4Expr::NatLit(42);
139        assert_eq!(e.to_string(), "42");
140    }
141    #[test]
142    pub(super) fn test_expr_bool_lit() {
143        let e = Lean4Expr::BoolLit(true);
144        assert_eq!(e.to_string(), "true");
145    }
146    #[test]
147    pub(super) fn test_expr_str_lit() {
148        let e = Lean4Expr::StrLit("hello".to_string());
149        assert_eq!(e.to_string(), "\"hello\"");
150    }
151    #[test]
152    pub(super) fn test_expr_str_lit_escaping() {
153        let e = Lean4Expr::StrLit("say \"hi\"".to_string());
154        assert!(e.to_string().contains("\\\""));
155    }
156    #[test]
157    pub(super) fn test_expr_sorry() {
158        let e = Lean4Expr::Sorry;
159        assert_eq!(e.to_string(), "sorry");
160    }
161    #[test]
162    pub(super) fn test_expr_hole() {
163        let e = Lean4Expr::Hole;
164        assert_eq!(e.to_string(), "_");
165    }
166    #[test]
167    pub(super) fn test_expr_app() {
168        let e = Lean4Expr::App(
169            Box::new(Lean4Expr::Var("f".to_string())),
170            Box::new(Lean4Expr::Var("x".to_string())),
171        );
172        assert_eq!(e.to_string(), "f x");
173    }
174    #[test]
175    pub(super) fn test_expr_lambda_untyped() {
176        let e = Lean4Expr::Lambda(
177            "x".to_string(),
178            None,
179            Box::new(Lean4Expr::Var("x".to_string())),
180        );
181        assert_eq!(e.to_string(), "fun x => x");
182    }
183    #[test]
184    pub(super) fn test_expr_lambda_typed() {
185        let e = Lean4Expr::Lambda(
186            "x".to_string(),
187            Some(Box::new(Lean4Type::Nat)),
188            Box::new(Lean4Expr::Var("x".to_string())),
189        );
190        assert_eq!(e.to_string(), "fun (x : Nat) => x");
191    }
192    #[test]
193    pub(super) fn test_expr_if() {
194        let e = Lean4Expr::If(
195            Box::new(Lean4Expr::BoolLit(true)),
196            Box::new(Lean4Expr::NatLit(1)),
197            Box::new(Lean4Expr::NatLit(0)),
198        );
199        assert_eq!(e.to_string(), "if true then 1 else 0");
200    }
201    #[test]
202    pub(super) fn test_expr_tuple() {
203        let e = Lean4Expr::Tuple(vec![Lean4Expr::NatLit(1), Lean4Expr::NatLit(2)]);
204        assert_eq!(e.to_string(), "(1, 2)");
205    }
206    #[test]
207    pub(super) fn test_expr_anonymous_ctor() {
208        let e = Lean4Expr::AnonymousCtor(vec![Lean4Expr::NatLit(1), Lean4Expr::NatLit(2)]);
209        assert_eq!(e.to_string(), "⟨1, 2⟩");
210    }
211    #[test]
212    pub(super) fn test_expr_by_tactic() {
213        let e = Lean4Expr::ByTactic(vec!["simp".to_string(), "exact h".to_string()]);
214        assert_eq!(e.to_string(), "by simp; exact h");
215    }
216    #[test]
217    pub(super) fn test_pattern_wildcard() {
218        assert_eq!(Lean4Pattern::Wildcard.to_string(), "_");
219    }
220    #[test]
221    pub(super) fn test_pattern_var() {
222        assert_eq!(Lean4Pattern::Var("x".to_string()).to_string(), "x");
223    }
224    #[test]
225    pub(super) fn test_pattern_ctor_noargs() {
226        let p = Lean4Pattern::Ctor("none".to_string(), vec![]);
227        assert_eq!(p.to_string(), "none");
228    }
229    #[test]
230    pub(super) fn test_pattern_ctor_with_args() {
231        let p = Lean4Pattern::Ctor("some".to_string(), vec![Lean4Pattern::Var("x".to_string())]);
232        assert_eq!(p.to_string(), "some x");
233    }
234    #[test]
235    pub(super) fn test_pattern_tuple() {
236        let p = Lean4Pattern::Tuple(vec![
237            Lean4Pattern::Var("a".to_string()),
238            Lean4Pattern::Var("b".to_string()),
239        ]);
240        assert_eq!(p.to_string(), "(a, b)");
241    }
242    #[test]
243    pub(super) fn test_pattern_or() {
244        let p = Lean4Pattern::Or(
245            Box::new(Lean4Pattern::Lit("0".to_string())),
246            Box::new(Lean4Pattern::Lit("1".to_string())),
247        );
248        assert_eq!(p.to_string(), "0 | 1");
249    }
250    #[test]
251    pub(super) fn test_def_emit_simple() {
252        let def = Lean4Def::simple(
253            "id",
254            vec![("x".to_string(), Lean4Type::Nat)],
255            Lean4Type::Nat,
256            Lean4Expr::Var("x".to_string()),
257        );
258        let out = def.emit();
259        assert!(out.contains("def id"));
260        assert!(out.contains("(x : Nat)"));
261        assert!(out.contains(": Nat"));
262        assert!(out.contains(":="));
263        assert!(out.contains("x"));
264    }
265    #[test]
266    pub(super) fn test_def_emit_with_attribute() {
267        let mut def = Lean4Def::simple("myFn", vec![], Lean4Type::Nat, Lean4Expr::NatLit(0));
268        def.attributes.push("simp".to_string());
269        let out = def.emit();
270        assert!(out.contains("@[simp]"));
271    }
272    #[test]
273    pub(super) fn test_def_emit_noncomputable() {
274        let mut def = Lean4Def::simple(
275            "realVal",
276            vec![],
277            Lean4Type::Float,
278            Lean4Expr::FloatLit(3.14),
279        );
280        def.is_noncomputable = true;
281        let out = def.emit();
282        assert!(out.contains("noncomputable"));
283    }
284    #[test]
285    pub(super) fn test_def_emit_private() {
286        let mut def = Lean4Def::simple("helper", vec![], Lean4Type::Nat, Lean4Expr::NatLit(0));
287        def.is_private = true;
288        let out = def.emit();
289        assert!(out.contains("private"));
290    }
291    #[test]
292    pub(super) fn test_theorem_emit_tactic() {
293        let thm = Lean4Theorem::tactic(
294            "add_zero",
295            vec![("n".to_string(), Lean4Type::Nat)],
296            Lean4Type::Custom("n + 0 = n".to_string()),
297            vec!["simp".to_string()],
298        );
299        let out = thm.emit();
300        assert!(out.contains("theorem add_zero"));
301        assert!(out.contains("(n : Nat)"));
302        assert!(out.contains("by simp"));
303    }
304    #[test]
305    pub(super) fn test_theorem_emit_term_mode() {
306        let thm = Lean4Theorem::term_mode(
307            "trivial_thm",
308            vec![],
309            Lean4Type::Custom("True".to_string()),
310            Lean4Expr::Var("trivial".to_string()),
311        );
312        let out = thm.emit();
313        assert!(out.contains("theorem trivial_thm"));
314        assert!(out.contains("trivial"));
315    }
316    #[test]
317    pub(super) fn test_inductive_emit_simple() {
318        let ind = Lean4Inductive::simple(
319            "Color",
320            vec![
321                Lean4Constructor::positional("red", vec![]),
322                Lean4Constructor::positional("green", vec![]),
323                Lean4Constructor::positional("blue", vec![]),
324            ],
325        );
326        let out = ind.emit();
327        assert!(out.contains("inductive Color"));
328        assert!(out.contains("| red"));
329        assert!(out.contains("| green"));
330        assert!(out.contains("| blue"));
331    }
332    #[test]
333    pub(super) fn test_inductive_emit_with_fields() {
334        let ind = Lean4Inductive::simple(
335            "Expr",
336            vec![
337                Lean4Constructor::positional("lit", vec![Lean4Type::Nat]),
338                Lean4Constructor::positional(
339                    "add",
340                    vec![
341                        Lean4Type::Custom("Expr".to_string()),
342                        Lean4Type::Custom("Expr".to_string()),
343                    ],
344                ),
345            ],
346        );
347        let out = ind.emit();
348        assert!(out.contains("inductive Expr"));
349        assert!(out.contains("| lit"));
350        assert!(out.contains("Nat"));
351    }
352    #[test]
353    pub(super) fn test_structure_emit() {
354        let s = Lean4Structure::simple(
355            "Point",
356            vec![
357                ("x".to_string(), Lean4Type::Float),
358                ("y".to_string(), Lean4Type::Float),
359            ],
360        );
361        let out = s.emit();
362        assert!(out.contains("structure Point"));
363        assert!(out.contains("x : Float"));
364        assert!(out.contains("y : Float"));
365    }
366    #[test]
367    pub(super) fn test_file_emit_imports() {
368        let file = Lean4File::new()
369            .with_import("Mathlib.Data.Nat.Basic")
370            .with_open("Nat");
371        let out = file.emit();
372        assert!(out.contains("import Mathlib.Data.Nat.Basic"));
373        assert!(out.contains("open Nat"));
374    }
375    #[test]
376    pub(super) fn test_file_emit_with_def() {
377        let mut file = Lean4File::new();
378        let def = Lean4Def::simple(
379            "double",
380            vec![("n".to_string(), Lean4Type::Nat)],
381            Lean4Type::Nat,
382            Lean4Expr::App(
383                Box::new(Lean4Expr::App(
384                    Box::new(Lean4Expr::Var("HAdd.hAdd".to_string())),
385                    Box::new(Lean4Expr::Var("n".to_string())),
386                )),
387                Box::new(Lean4Expr::Var("n".to_string())),
388            ),
389        );
390        file.add_decl(Lean4Decl::Def(def));
391        let out = file.emit();
392        assert!(out.contains("def double"));
393        assert!(out.contains("(n : Nat)"));
394    }
395    #[test]
396    pub(super) fn test_backend_compile_kernel_decl() {
397        let mut backend = Lean4Backend::new();
398        backend.compile_kernel_decl(
399            "identity",
400            vec![("x".to_string(), Lean4Type::Nat)],
401            Lean4Type::Nat,
402            Lean4Expr::Var("x".to_string()),
403        );
404        let out = backend.emit_file();
405        assert!(out.contains("def identity"));
406    }
407    #[test]
408    pub(super) fn test_backend_add_theorem() {
409        let mut backend = Lean4Backend::new();
410        backend.add_theorem(
411            "nat_eq_refl",
412            vec![("n".to_string(), Lean4Type::Nat)],
413            Lean4Type::Custom("n = n".to_string()),
414            vec!["rfl".to_string()],
415        );
416        let out = backend.emit_file();
417        assert!(out.contains("theorem nat_eq_refl"));
418        assert!(out.contains("by rfl"));
419    }
420    #[test]
421    pub(super) fn test_backend_add_inductive() {
422        let mut backend = Lean4Backend::new();
423        let ind = Lean4Inductive::simple(
424            "Tree",
425            vec![
426                Lean4Constructor::positional("leaf", vec![]),
427                Lean4Constructor::positional(
428                    "node",
429                    vec![
430                        Lean4Type::Custom("Tree".to_string()),
431                        Lean4Type::Nat,
432                        Lean4Type::Custom("Tree".to_string()),
433                    ],
434                ),
435            ],
436        );
437        backend.add_inductive(ind);
438        let out = backend.emit_file();
439        assert!(out.contains("inductive Tree"));
440        assert!(out.contains("leaf"));
441        assert!(out.contains("node"));
442    }
443    #[test]
444    pub(super) fn test_namespace_emit() {
445        let decl = Lean4Decl::Namespace(
446            "MyNS".to_string(),
447            vec![Lean4Decl::Def(Lean4Def::simple(
448                "foo",
449                vec![],
450                Lean4Type::Nat,
451                Lean4Expr::NatLit(0),
452            ))],
453        );
454        let out = decl.emit();
455        assert!(out.contains("namespace MyNS"));
456        assert!(out.contains("end MyNS"));
457        assert!(out.contains("def foo"));
458    }
459    #[test]
460    pub(super) fn test_section_emit() {
461        let decl = Lean4Decl::Section(
462            "Aux".to_string(),
463            vec![Lean4Decl::Check(Lean4Expr::NatLit(42))],
464        );
465        let out = decl.emit();
466        assert!(out.contains("section Aux"));
467        assert!(out.contains("end Aux"));
468        assert!(out.contains("#check"));
469    }
470    #[test]
471    pub(super) fn test_axiom_emit() {
472        let ax = Lean4Axiom {
473            name: "classical".to_string(),
474            args: vec![("p".to_string(), Lean4Type::Prop)],
475            ty: Lean4Type::Custom("p ∨ ¬p".to_string()),
476            doc_comment: Some("Law of excluded middle".to_string()),
477        };
478        let out = ax.emit();
479        assert!(out.contains("axiom classical"));
480        assert!(out.contains("(p : Prop)"));
481        assert!(out.contains("Law of excluded middle"));
482    }
483    #[test]
484    pub(super) fn test_abbrev_emit() {
485        let a = Lean4Abbrev {
486            name: "MyNat".to_string(),
487            args: vec![],
488            ty: Some(Lean4Type::Type(0)),
489            body: Lean4Expr::Var("Nat".to_string()),
490        };
491        let out = a.emit();
492        assert!(out.contains("abbrev MyNat"));
493        assert!(out.contains("Nat"));
494    }
495    #[test]
496    pub(super) fn test_instance_emit() {
497        let inst = Lean4Instance {
498            name: Some("instAddNat".to_string()),
499            ty: Lean4Type::Custom("Add Nat".to_string()),
500            args: vec![],
501            body: Lean4Expr::StructLit(
502                "".to_string(),
503                vec![("add".to_string(), Lean4Expr::Var("Nat.add".to_string()))],
504            ),
505        };
506        let out = inst.emit();
507        assert!(out.contains("instance instAddNat"));
508        assert!(out.contains("Add Nat"));
509    }
510    #[test]
511    pub(super) fn test_do_notation() {
512        let stmt = Lean4DoStmt::Bind(
513            "line".to_string(),
514            None,
515            Box::new(Lean4Expr::Var("IO.getLine".to_string())),
516        );
517        let s = stmt.to_string();
518        assert!(s.contains("let line ←"));
519        assert!(s.contains("IO.getLine"));
520    }
521    #[test]
522    pub(super) fn test_calc_step() {
523        let step = Lean4CalcStep {
524            lhs: Lean4Expr::Var("a".to_string()),
525            relation: "=".to_string(),
526            rhs: Lean4Expr::Var("b".to_string()),
527            justification: Lean4Expr::Var("h".to_string()),
528        };
529        let s = step.to_string();
530        assert!(s.contains("a = b := h"));
531    }
532    #[test]
533    pub(super) fn test_module_doc_emit() {
534        let mut file = Lean4File::new();
535        file.module_doc = Some("This is a module.".to_string());
536        let out = file.emit();
537        assert!(out.contains("/-!"));
538        assert!(out.contains("This is a module."));
539        assert!(out.contains("-/"));
540    }
541    #[test]
542    pub(super) fn test_structure_with_extends() {
543        let mut s = Lean4Structure::simple("Point3D", vec![("z".to_string(), Lean4Type::Float)]);
544        s.extends.push("Point".to_string());
545        let out = s.emit();
546        assert!(out.contains("extends Point"));
547    }
548    #[test]
549    pub(super) fn test_inductive_with_derives() {
550        let mut ind = Lean4Inductive::simple(
551            "MyType",
552            vec![Lean4Constructor::positional("mk", vec![Lean4Type::Nat])],
553        );
554        ind.derives.push("Repr".to_string());
555        ind.derives.push("DecidableEq".to_string());
556        let out = ind.emit();
557        assert!(out.contains("deriving Repr, DecidableEq"));
558    }
559}
560#[cfg(test)]
561mod L4_infra_tests {
562    use super::*;
563    #[test]
564    pub(super) fn test_pass_config() {
565        let config = L4PassConfig::new("test_pass", L4PassPhase::Transformation);
566        assert!(config.enabled);
567        assert!(config.phase.is_modifying());
568        assert_eq!(config.phase.name(), "transformation");
569    }
570    #[test]
571    pub(super) fn test_pass_stats() {
572        let mut stats = L4PassStats::new();
573        stats.record_run(10, 100, 3);
574        stats.record_run(20, 200, 5);
575        assert_eq!(stats.total_runs, 2);
576        assert!((stats.average_changes_per_run() - 15.0).abs() < 0.01);
577        assert!((stats.success_rate() - 1.0).abs() < 0.01);
578        let s = stats.format_summary();
579        assert!(s.contains("Runs: 2/2"));
580    }
581    #[test]
582    pub(super) fn test_pass_registry() {
583        let mut reg = L4PassRegistry::new();
584        reg.register(L4PassConfig::new("pass_a", L4PassPhase::Analysis));
585        reg.register(L4PassConfig::new("pass_b", L4PassPhase::Transformation).disabled());
586        assert_eq!(reg.total_passes(), 2);
587        assert_eq!(reg.enabled_count(), 1);
588        reg.update_stats("pass_a", 5, 50, 2);
589        let stats = reg.get_stats("pass_a").expect("stats should exist");
590        assert_eq!(stats.total_changes, 5);
591    }
592    #[test]
593    pub(super) fn test_analysis_cache() {
594        let mut cache = L4AnalysisCache::new(10);
595        cache.insert("key1".to_string(), vec![1, 2, 3]);
596        assert!(cache.get("key1").is_some());
597        assert!(cache.get("key2").is_none());
598        assert!((cache.hit_rate() - 0.5).abs() < 0.01);
599        cache.invalidate("key1");
600        assert!(!cache.entries["key1"].valid);
601        assert_eq!(cache.size(), 1);
602    }
603    #[test]
604    pub(super) fn test_worklist() {
605        let mut wl = L4Worklist::new();
606        assert!(wl.push(1));
607        assert!(wl.push(2));
608        assert!(!wl.push(1));
609        assert_eq!(wl.len(), 2);
610        assert_eq!(wl.pop(), Some(1));
611        assert!(!wl.contains(1));
612        assert!(wl.contains(2));
613    }
614    #[test]
615    pub(super) fn test_dominator_tree() {
616        let mut dt = L4DominatorTree::new(5);
617        dt.set_idom(1, 0);
618        dt.set_idom(2, 0);
619        dt.set_idom(3, 1);
620        assert!(dt.dominates(0, 3));
621        assert!(dt.dominates(1, 3));
622        assert!(!dt.dominates(2, 3));
623        assert!(dt.dominates(3, 3));
624    }
625    #[test]
626    pub(super) fn test_liveness() {
627        let mut liveness = L4LivenessInfo::new(3);
628        liveness.add_def(0, 1);
629        liveness.add_use(1, 1);
630        assert!(liveness.defs[0].contains(&1));
631        assert!(liveness.uses[1].contains(&1));
632    }
633    #[test]
634    pub(super) fn test_constant_folding() {
635        assert_eq!(L4ConstantFoldingHelper::fold_add_i64(3, 4), Some(7));
636        assert_eq!(L4ConstantFoldingHelper::fold_div_i64(10, 0), None);
637        assert_eq!(L4ConstantFoldingHelper::fold_div_i64(10, 2), Some(5));
638        assert_eq!(
639            L4ConstantFoldingHelper::fold_bitand_i64(0b1100, 0b1010),
640            0b1000
641        );
642        assert_eq!(L4ConstantFoldingHelper::fold_bitnot_i64(0), -1);
643    }
644    #[test]
645    pub(super) fn test_dep_graph() {
646        let mut g = L4DepGraph::new();
647        g.add_dep(1, 2);
648        g.add_dep(2, 3);
649        g.add_dep(1, 3);
650        assert_eq!(g.dependencies_of(2), vec![1]);
651        let topo = g.topological_sort();
652        assert_eq!(topo.len(), 3);
653        assert!(!g.has_cycle());
654        let pos: std::collections::HashMap<u32, usize> =
655            topo.iter().enumerate().map(|(i, &n)| (n, i)).collect();
656        assert!(pos[&1] < pos[&2]);
657        assert!(pos[&1] < pos[&3]);
658        assert!(pos[&2] < pos[&3]);
659    }
660}
661#[cfg(test)]
662mod l4ext_pass_tests {
663    use super::*;
664    #[test]
665    pub(super) fn test_l4ext_phase_order() {
666        assert_eq!(L4ExtPassPhase::Early.order(), 0);
667        assert_eq!(L4ExtPassPhase::Middle.order(), 1);
668        assert_eq!(L4ExtPassPhase::Late.order(), 2);
669        assert_eq!(L4ExtPassPhase::Finalize.order(), 3);
670        assert!(L4ExtPassPhase::Early.is_early());
671        assert!(!L4ExtPassPhase::Early.is_late());
672    }
673    #[test]
674    pub(super) fn test_l4ext_config_builder() {
675        let c = L4ExtPassConfig::new("p")
676            .with_phase(L4ExtPassPhase::Late)
677            .with_max_iter(50)
678            .with_debug(1);
679        assert_eq!(c.name, "p");
680        assert_eq!(c.max_iterations, 50);
681        assert!(c.is_debug_enabled());
682        assert!(c.enabled);
683        let c2 = c.disabled();
684        assert!(!c2.enabled);
685    }
686    #[test]
687    pub(super) fn test_l4ext_stats() {
688        let mut s = L4ExtPassStats::new();
689        s.visit();
690        s.visit();
691        s.modify();
692        s.iterate();
693        assert_eq!(s.nodes_visited, 2);
694        assert_eq!(s.nodes_modified, 1);
695        assert!(s.changed);
696        assert_eq!(s.iterations, 1);
697        let e = s.efficiency();
698        assert!((e - 0.5).abs() < 1e-9);
699    }
700    #[test]
701    pub(super) fn test_l4ext_registry() {
702        let mut r = L4ExtPassRegistry::new();
703        r.register(L4ExtPassConfig::new("a").with_phase(L4ExtPassPhase::Early));
704        r.register(L4ExtPassConfig::new("b").disabled());
705        assert_eq!(r.len(), 2);
706        assert_eq!(r.enabled_passes().len(), 1);
707        assert_eq!(r.passes_in_phase(&L4ExtPassPhase::Early).len(), 1);
708    }
709    #[test]
710    pub(super) fn test_l4ext_cache() {
711        let mut c = L4ExtCache::new(4);
712        assert!(c.get(99).is_none());
713        c.put(99, vec![1, 2, 3]);
714        let v = c.get(99).expect("v should be present in map");
715        assert_eq!(v, &[1u8, 2, 3]);
716        assert!(c.hit_rate() > 0.0);
717        assert_eq!(c.live_count(), 1);
718    }
719    #[test]
720    pub(super) fn test_l4ext_worklist() {
721        let mut w = L4ExtWorklist::new(10);
722        w.push(5);
723        w.push(3);
724        w.push(5);
725        assert_eq!(w.len(), 2);
726        assert!(w.contains(5));
727        let first = w.pop().expect("first should be available to pop");
728        assert!(!w.contains(first));
729    }
730    #[test]
731    pub(super) fn test_l4ext_dom_tree() {
732        let mut dt = L4ExtDomTree::new(5);
733        dt.set_idom(1, 0);
734        dt.set_idom(2, 0);
735        dt.set_idom(3, 1);
736        dt.set_idom(4, 1);
737        assert!(dt.dominates(0, 3));
738        assert!(dt.dominates(1, 4));
739        assert!(!dt.dominates(2, 3));
740        assert_eq!(dt.depth_of(3), 2);
741    }
742    #[test]
743    pub(super) fn test_l4ext_liveness() {
744        let mut lv = L4ExtLiveness::new(3);
745        lv.add_def(0, 1);
746        lv.add_use(1, 1);
747        assert!(lv.var_is_def_in_block(0, 1));
748        assert!(lv.var_is_used_in_block(1, 1));
749        assert!(!lv.var_is_def_in_block(1, 1));
750    }
751    #[test]
752    pub(super) fn test_l4ext_const_folder() {
753        let mut cf = L4ExtConstFolder::new();
754        assert_eq!(cf.add_i64(3, 4), Some(7));
755        assert_eq!(cf.div_i64(10, 0), None);
756        assert_eq!(cf.mul_i64(6, 7), Some(42));
757        assert_eq!(cf.and_i64(0b1100, 0b1010), 0b1000);
758        assert_eq!(cf.fold_count(), 3);
759        assert_eq!(cf.failure_count(), 1);
760    }
761    #[test]
762    pub(super) fn test_l4ext_dep_graph() {
763        let mut g = L4ExtDepGraph::new(4);
764        g.add_edge(0, 1);
765        g.add_edge(1, 2);
766        g.add_edge(2, 3);
767        assert!(!g.has_cycle());
768        assert_eq!(g.topo_sort(), Some(vec![0, 1, 2, 3]));
769        assert_eq!(g.reachable(0).len(), 4);
770        let sccs = g.scc();
771        assert_eq!(sccs.len(), 4);
772    }
773}
oxilean_codegen/lean4_backend/functions.rs

oxilean_codegen/lean4_backend/
functions.rs
