oxilean_codegen/agda_backend/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::types::{
6    AgdaAnalysisCache, AgdaClause, AgdaConstantFoldingHelper, AgdaConstructor, AgdaData, AgdaDecl,
7    AgdaDepGraph, AgdaDominatorTree, AgdaExpr, AgdaExtCache, AgdaExtConstFolder, AgdaExtDepGraph,
8    AgdaExtDomTree, AgdaExtLiveness, AgdaExtPassConfig, AgdaExtPassPhase, AgdaExtPassRegistry,
9    AgdaExtPassStats, AgdaExtWorklist, AgdaField, AgdaLivenessInfo, AgdaModule, AgdaPassConfig,
10    AgdaPassPhase, AgdaPassRegistry, AgdaPassStats, AgdaPattern, AgdaRecord, AgdaWorklist,
11    AgdaX2Cache, AgdaX2ConstFolder, AgdaX2DepGraph, AgdaX2DomTree, AgdaX2Liveness,
12    AgdaX2PassConfig, AgdaX2PassPhase, AgdaX2PassRegistry, AgdaX2PassStats, AgdaX2Worklist,
13};
14
15/// Escape special characters in an Agda string literal.
16pub(super) fn escape_agda_string(s: &str) -> String {
17    let mut out = String::with_capacity(s.len());
18    for c in s.chars() {
19        match c {
20            '"' => out.push_str("\\\""),
21            '\\' => out.push_str("\\\\"),
22            '\n' => out.push_str("\\n"),
23            '\t' => out.push_str("\\t"),
24            c => out.push(c),
25        }
26    }
27    out
28}
29/// Emit `(x : T) (y : U)` parameter list.
30pub(super) fn emit_agda_params(params: &[(String, AgdaExpr)], indent: usize) -> String {
31    params
32        .iter()
33        .map(|(x, ty)| format!("({} : {})", x, ty.emit(indent)))
34        .collect::<Vec<_>>()
35        .join(" ")
36}
37/// Build `AgdaExpr::Var`.
38pub fn var(name: impl Into<String>) -> AgdaExpr {
39    AgdaExpr::Var(name.into())
40}
41/// Build a left-associative application chain: `f a1 a2 ...`.
42pub fn app(func: AgdaExpr, args: Vec<AgdaExpr>) -> AgdaExpr {
43    args.into_iter()
44        .fold(func, |acc, a| AgdaExpr::App(Box::new(acc), Box::new(a)))
45}
46/// Build `f a` (single-argument application).
47pub fn app1(func: AgdaExpr, arg: AgdaExpr) -> AgdaExpr {
48    AgdaExpr::App(Box::new(func), Box::new(arg))
49}
50/// Build a non-dependent Pi type: `A → B`.
51pub fn arrow(dom: AgdaExpr, cod: AgdaExpr) -> AgdaExpr {
52    AgdaExpr::Pi(None, Box::new(dom), Box::new(cod))
53}
54/// Build a dependent Pi type: `(x : A) → B`.
55pub fn pi(x: impl Into<String>, dom: AgdaExpr, cod: AgdaExpr) -> AgdaExpr {
56    AgdaExpr::Pi(Some(x.into()), Box::new(dom), Box::new(cod))
57}
58/// Build a lambda: `λ x → body`.
59pub fn lam(x: impl Into<String>, body: AgdaExpr) -> AgdaExpr {
60    AgdaExpr::Lambda(x.into(), Box::new(body))
61}
62#[cfg(test)]
63mod tests {
64    use super::*;
65    pub(super) fn nat() -> AgdaExpr {
66        var("ℕ")
67    }
68    pub(super) fn set0() -> AgdaExpr {
69        AgdaExpr::Set(None)
70    }
71    pub(super) fn bool_t() -> AgdaExpr {
72        var("Bool")
73    }
74    #[test]
75    pub(super) fn test_pattern_var() {
76        assert_eq!(AgdaPattern::Var("n".into()).to_string(), "n");
77    }
78    #[test]
79    pub(super) fn test_pattern_wildcard() {
80        assert_eq!(AgdaPattern::Wildcard.to_string(), "_");
81    }
82    #[test]
83    pub(super) fn test_pattern_con_nullary() {
84        assert_eq!(AgdaPattern::Con("zero".into(), vec![]).to_string(), "zero");
85    }
86    #[test]
87    pub(super) fn test_pattern_con_unary() {
88        let p = AgdaPattern::Con("suc".into(), vec![AgdaPattern::Var("n".into())]);
89        assert_eq!(p.to_string(), "(suc n)");
90    }
91    #[test]
92    pub(super) fn test_pattern_absurd() {
93        assert_eq!(AgdaPattern::Absurd.to_string(), "()");
94    }
95    #[test]
96    pub(super) fn test_pattern_implicit() {
97        let p = AgdaPattern::Implicit(Box::new(AgdaPattern::Var("A".into())));
98        assert_eq!(p.to_string(), "{A}");
99    }
100    #[test]
101    pub(super) fn test_pattern_as() {
102        let p = AgdaPattern::As(
103            "xs".into(),
104            Box::new(AgdaPattern::Con(
105                "_∷_".into(),
106                vec![AgdaPattern::Var("x".into()), AgdaPattern::Var("xt".into())],
107            )),
108        );
109        assert_eq!(p.to_string(), "xs@(_∷_ x xt)");
110    }
111    #[test]
112    pub(super) fn test_expr_var() {
113        assert_eq!(var("ℕ").emit(0), "ℕ");
114    }
115    #[test]
116    pub(super) fn test_expr_num() {
117        assert_eq!(AgdaExpr::Num(42).emit(0), "42");
118    }
119    #[test]
120    pub(super) fn test_expr_str() {
121        assert_eq!(AgdaExpr::Str("hello".into()).emit(0), "\"hello\"");
122    }
123    #[test]
124    pub(super) fn test_expr_set() {
125        assert_eq!(AgdaExpr::Set(None).emit(0), "Set");
126        assert_eq!(AgdaExpr::Set(Some(0)).emit(0), "Set");
127        assert_eq!(AgdaExpr::Set(Some(1)).emit(0), "Set₁");
128    }
129    #[test]
130    pub(super) fn test_expr_prop() {
131        assert_eq!(AgdaExpr::Prop.emit(0), "Prop");
132    }
133    #[test]
134    pub(super) fn test_expr_hole() {
135        assert_eq!(AgdaExpr::Hole.emit(0), "{! !}");
136    }
137    #[test]
138    pub(super) fn test_expr_app_simple() {
139        let t = app1(var("suc"), var("n"));
140        assert_eq!(t.emit(0), "suc n");
141    }
142    #[test]
143    pub(super) fn test_expr_app_chain() {
144        let t = app(var("_+_"), vec![var("m"), var("n")]);
145        assert_eq!(t.emit(0), "_+_ m n");
146    }
147    #[test]
148    pub(super) fn test_expr_app_nested_parens() {
149        let inner = app1(var("suc"), var("n"));
150        let outer = app1(var("suc"), inner);
151        assert_eq!(outer.emit(0), "suc (suc n)");
152    }
153    #[test]
154    pub(super) fn test_expr_lambda() {
155        let t = lam("n", app1(var("suc"), var("n")));
156        assert_eq!(t.emit(0), "λ n → suc n");
157    }
158    #[test]
159    pub(super) fn test_expr_arrow() {
160        let t = arrow(nat(), nat());
161        assert_eq!(t.emit(0), "ℕ → ℕ");
162    }
163    #[test]
164    pub(super) fn test_expr_pi_dependent() {
165        let t = pi("n", nat(), app1(var("Vec"), var("n")));
166        assert_eq!(t.emit(0), "(n : ℕ) → Vec n");
167    }
168    #[test]
169    pub(super) fn test_expr_implicit() {
170        let t = AgdaExpr::Implicit(Box::new(var("A")));
171        assert_eq!(t.emit(0), "{A}");
172    }
173    #[test]
174    pub(super) fn test_expr_tuple() {
175        let t = AgdaExpr::Tuple(vec![AgdaExpr::Num(1), AgdaExpr::Num(2)]);
176        assert_eq!(t.emit(0), "(1 , 2)");
177    }
178    #[test]
179    pub(super) fn test_expr_record_construction() {
180        let t = AgdaExpr::Record(vec![
181            ("fst".into(), AgdaExpr::Num(1)),
182            ("snd".into(), AgdaExpr::Num(2)),
183        ]);
184        assert_eq!(t.emit(0), "record { fst = 1 ; snd = 2 }");
185    }
186    #[test]
187    pub(super) fn test_expr_ascription() {
188        let t = AgdaExpr::Ascription(Box::new(AgdaExpr::Num(0)), Box::new(nat()));
189        assert_eq!(t.emit(0), "(0 : ℕ)");
190    }
191    #[test]
192    pub(super) fn test_expr_if_then_else() {
193        let t = AgdaExpr::IfThenElse(
194            Box::new(var("b")),
195            Box::new(AgdaExpr::Num(1)),
196            Box::new(AgdaExpr::Num(0)),
197        );
198        assert_eq!(t.emit(0), "if b then 1 else 0");
199    }
200    #[test]
201    pub(super) fn test_clause_base_case() {
202        let c = AgdaClause {
203            patterns: vec![AgdaPattern::Con("zero".into(), vec![])],
204            rhs: Some(AgdaExpr::Num(0)),
205            where_decls: vec![],
206        };
207        let s = c.emit_clause("factorial", 0);
208        assert_eq!(s, "factorial zero = 0");
209    }
210    #[test]
211    pub(super) fn test_clause_recursive() {
212        let c = AgdaClause {
213            patterns: vec![AgdaPattern::Con(
214                "suc".into(),
215                vec![AgdaPattern::Var("n".into())],
216            )],
217            rhs: Some(app(
218                var("_*_"),
219                vec![app1(var("suc"), var("n")), app1(var("factorial"), var("n"))],
220            )),
221            where_decls: vec![],
222        };
223        let s = c.emit_clause("factorial", 0);
224        assert!(s.starts_with("factorial (suc n) ="));
225    }
226    #[test]
227    pub(super) fn test_decl_func_type() {
228        let d = AgdaDecl::FuncType {
229            name: "double".into(),
230            ty: arrow(nat(), nat()),
231        };
232        assert_eq!(d.emit(0), "double : ℕ → ℕ");
233    }
234    #[test]
235    pub(super) fn test_decl_func_def_two_clauses() {
236        let d = AgdaDecl::FuncDef {
237            name: "_+_".into(),
238            clauses: vec![
239                AgdaClause {
240                    patterns: vec![
241                        AgdaPattern::Con("zero".into(), vec![]),
242                        AgdaPattern::Var("m".into()),
243                    ],
244                    rhs: Some(var("m")),
245                    where_decls: vec![],
246                },
247                AgdaClause {
248                    patterns: vec![
249                        AgdaPattern::Con("suc".into(), vec![AgdaPattern::Var("n".into())]),
250                        AgdaPattern::Var("m".into()),
251                    ],
252                    rhs: Some(app1(var("suc"), app(var("_+_"), vec![var("n"), var("m")]))),
253                    where_decls: vec![],
254                },
255            ],
256        };
257        let s = d.emit(0);
258        assert!(s.contains("_+_ zero m = m"));
259        assert!(s.contains("_+_ (suc n) m = suc (_+_ n m)"));
260    }
261    #[test]
262    pub(super) fn test_decl_data_nat() {
263        let d = AgdaDecl::DataDecl(AgdaData {
264            name: "ℕ".into(),
265            params: vec![],
266            indices: set0(),
267            constructors: vec![
268                AgdaConstructor {
269                    name: "zero".into(),
270                    ty: var("ℕ"),
271                },
272                AgdaConstructor {
273                    name: "suc".into(),
274                    ty: arrow(var("ℕ"), var("ℕ")),
275                },
276            ],
277        });
278        let s = d.emit(0);
279        assert!(s.contains("data ℕ : Set where"));
280        assert!(s.contains("zero : ℕ"));
281        assert!(s.contains("suc : ℕ → ℕ"));
282    }
283    #[test]
284    pub(super) fn test_decl_data_list() {
285        let d = AgdaDecl::DataDecl(AgdaData {
286            name: "List".into(),
287            params: vec![("A".into(), set0())],
288            indices: set0(),
289            constructors: vec![
290                AgdaConstructor {
291                    name: "[]".into(),
292                    ty: app1(var("List"), var("A")),
293                },
294                AgdaConstructor {
295                    name: "_∷_".into(),
296                    ty: arrow(
297                        var("A"),
298                        arrow(app1(var("List"), var("A")), app1(var("List"), var("A"))),
299                    ),
300                },
301            ],
302        });
303        let s = d.emit(0);
304        assert!(s.contains("data List (A : Set) : Set where"));
305        assert!(s.contains("[] : List A"));
306        assert!(s.contains("_∷_ : A → List A → List A"));
307    }
308    #[test]
309    pub(super) fn test_decl_record_sigma() {
310        let d = AgdaDecl::RecordDecl(AgdaRecord {
311            name: "Σ".into(),
312            params: vec![("A".into(), set0()), ("B".into(), arrow(var("A"), set0()))],
313            universe: set0(),
314            constructor: Some("_,_".into()),
315            fields: vec![
316                AgdaField {
317                    name: "fst".into(),
318                    ty: var("A"),
319                },
320                AgdaField {
321                    name: "snd".into(),
322                    ty: app1(var("B"), var("fst")),
323                },
324            ],
325            copattern_defs: vec![],
326        });
327        let s = d.emit(0);
328        assert!(s.contains("record Σ (A : Set) (B : A → Set) : Set where"));
329        assert!(s.contains("constructor _,_"));
330        assert!(s.contains("fst : A"));
331        assert!(s.contains("snd : B fst"));
332    }
333    #[test]
334    pub(super) fn test_decl_postulate() {
335        let d = AgdaDecl::Postulate(vec![(
336            "LEM".into(),
337            pi(
338                "P",
339                var("Prop"),
340                app(var("_⊎_"), vec![var("P"), app1(var("¬"), var("P"))]),
341            ),
342        )]);
343        let s = d.emit(0);
344        assert!(s.starts_with("postulate"));
345        assert!(s.contains("LEM : (P : Prop) → _⊎_ P (¬ P)"));
346    }
347    #[test]
348    pub(super) fn test_decl_import() {
349        let d = AgdaDecl::Import("Data.Nat".into());
350        assert_eq!(d.emit(0), "import Data.Nat");
351    }
352    #[test]
353    pub(super) fn test_decl_open() {
354        let d = AgdaDecl::Open("Data.Nat".into());
355        assert_eq!(d.emit(0), "open Data.Nat");
356    }
357    #[test]
358    pub(super) fn test_decl_variable() {
359        let d = AgdaDecl::Variable(vec![("A".into(), set0()), ("B".into(), set0())]);
360        let s = d.emit(0);
361        assert!(s.contains("variable"));
362        assert!(s.contains("{A : Set}"));
363        assert!(s.contains("{B : Set}"));
364    }
365    #[test]
366    pub(super) fn test_decl_module() {
367        let d = AgdaDecl::ModuleDecl {
368            name: "Inner".into(),
369            params: vec![],
370            body: vec![AgdaDecl::FuncType {
371                name: "id".into(),
372                ty: arrow(bool_t(), bool_t()),
373            }],
374        };
375        let s = d.emit(0);
376        assert!(s.contains("module Inner where"));
377        assert!(s.contains("id : Bool → Bool"));
378    }
379    #[test]
380    pub(super) fn test_decl_pragma() {
381        let d = AgdaDecl::Pragma("BUILTIN NATURAL ℕ".into());
382        assert_eq!(d.emit(0), "{-# BUILTIN NATURAL ℕ #-}");
383    }
384    #[test]
385    pub(super) fn test_decl_comment() {
386        let d = AgdaDecl::Comment("Identity function".into());
387        assert_eq!(d.emit(0), "-- Identity function");
388    }
389    #[test]
390    pub(super) fn test_module_emit_basic() {
391        let mut m = AgdaModule::new("MyModule");
392        m.import("Data.Nat");
393        m.open("Data.Nat");
394        m.add(AgdaDecl::Comment("a function".into()));
395        m.add(AgdaDecl::FuncType {
396            name: "f".into(),
397            ty: arrow(nat(), nat()),
398        });
399        m.add(AgdaDecl::FuncDef {
400            name: "f".into(),
401            clauses: vec![AgdaClause {
402                patterns: vec![AgdaPattern::Var("n".into())],
403                rhs: Some(var("n")),
404                where_decls: vec![],
405            }],
406        });
407        let s = m.emit();
408        assert!(s.contains("module MyModule where"));
409        assert!(s.contains("import Data.Nat"));
410        assert!(s.contains("open Data.Nat"));
411        assert!(s.contains("-- a function"));
412        assert!(s.contains("f : ℕ → ℕ"));
413        assert!(s.contains("f n = n"));
414    }
415    #[test]
416    pub(super) fn test_module_parameterised() {
417        let mut m = AgdaModule::new("Container");
418        m.params.push(("A".into(), set0()));
419        let s = m.emit();
420        assert!(s.contains("module Container (A : Set) where"));
421    }
422    #[test]
423    pub(super) fn test_module_full_identity_proof() {
424        let mut m = AgdaModule::new("IdentityProof");
425        m.import("Relation.Binary.PropositionalEquality");
426        m.open("Relation.Binary.PropositionalEquality");
427        m.add(AgdaDecl::FuncType {
428            name: "refl-is-refl".into(),
429            ty: pi(
430                "A",
431                set0(),
432                pi("x", var("A"), app(var("_≡_"), vec![var("x"), var("x")])),
433            ),
434        });
435        m.add(AgdaDecl::FuncDef {
436            name: "refl-is-refl".into(),
437            clauses: vec![AgdaClause {
438                patterns: vec![AgdaPattern::Wildcard, AgdaPattern::Wildcard],
439                rhs: Some(var("refl")),
440                where_decls: vec![],
441            }],
442        });
443        let s = m.emit();
444        assert!(s.contains("refl-is-refl : (A : Set) → (x : A) → _≡_ x x"));
445        assert!(s.contains("refl-is-refl _ _ = refl"));
446    }
447}
448#[cfg(test)]
449mod Agda_infra_tests {
450    use super::*;
451    #[test]
452    pub(super) fn test_pass_config() {
453        let config = AgdaPassConfig::new("test_pass", AgdaPassPhase::Transformation);
454        assert!(config.enabled);
455        assert!(config.phase.is_modifying());
456        assert_eq!(config.phase.name(), "transformation");
457    }
458    #[test]
459    pub(super) fn test_pass_stats() {
460        let mut stats = AgdaPassStats::new();
461        stats.record_run(10, 100, 3);
462        stats.record_run(20, 200, 5);
463        assert_eq!(stats.total_runs, 2);
464        assert!((stats.average_changes_per_run() - 15.0).abs() < 0.01);
465        assert!((stats.success_rate() - 1.0).abs() < 0.01);
466        let s = stats.format_summary();
467        assert!(s.contains("Runs: 2/2"));
468    }
469    #[test]
470    pub(super) fn test_pass_registry() {
471        let mut reg = AgdaPassRegistry::new();
472        reg.register(AgdaPassConfig::new("pass_a", AgdaPassPhase::Analysis));
473        reg.register(AgdaPassConfig::new("pass_b", AgdaPassPhase::Transformation).disabled());
474        assert_eq!(reg.total_passes(), 2);
475        assert_eq!(reg.enabled_count(), 1);
476        reg.update_stats("pass_a", 5, 50, 2);
477        let stats = reg.get_stats("pass_a").expect("stats should exist");
478        assert_eq!(stats.total_changes, 5);
479    }
480    #[test]
481    pub(super) fn test_analysis_cache() {
482        let mut cache = AgdaAnalysisCache::new(10);
483        cache.insert("key1".to_string(), vec![1, 2, 3]);
484        assert!(cache.get("key1").is_some());
485        assert!(cache.get("key2").is_none());
486        assert!((cache.hit_rate() - 0.5).abs() < 0.01);
487        cache.invalidate("key1");
488        assert!(!cache.entries["key1"].valid);
489        assert_eq!(cache.size(), 1);
490    }
491    #[test]
492    pub(super) fn test_worklist() {
493        let mut wl = AgdaWorklist::new();
494        assert!(wl.push(1));
495        assert!(wl.push(2));
496        assert!(!wl.push(1));
497        assert_eq!(wl.len(), 2);
498        assert_eq!(wl.pop(), Some(1));
499        assert!(!wl.contains(1));
500        assert!(wl.contains(2));
501    }
502    #[test]
503    pub(super) fn test_dominator_tree() {
504        let mut dt = AgdaDominatorTree::new(5);
505        dt.set_idom(1, 0);
506        dt.set_idom(2, 0);
507        dt.set_idom(3, 1);
508        assert!(dt.dominates(0, 3));
509        assert!(dt.dominates(1, 3));
510        assert!(!dt.dominates(2, 3));
511        assert!(dt.dominates(3, 3));
512    }
513    #[test]
514    pub(super) fn test_liveness() {
515        let mut liveness = AgdaLivenessInfo::new(3);
516        liveness.add_def(0, 1);
517        liveness.add_use(1, 1);
518        assert!(liveness.defs[0].contains(&1));
519        assert!(liveness.uses[1].contains(&1));
520    }
521    #[test]
522    pub(super) fn test_constant_folding() {
523        assert_eq!(AgdaConstantFoldingHelper::fold_add_i64(3, 4), Some(7));
524        assert_eq!(AgdaConstantFoldingHelper::fold_div_i64(10, 0), None);
525        assert_eq!(AgdaConstantFoldingHelper::fold_div_i64(10, 2), Some(5));
526        assert_eq!(
527            AgdaConstantFoldingHelper::fold_bitand_i64(0b1100, 0b1010),
528            0b1000
529        );
530        assert_eq!(AgdaConstantFoldingHelper::fold_bitnot_i64(0), -1);
531    }
532    #[test]
533    pub(super) fn test_dep_graph() {
534        let mut g = AgdaDepGraph::new();
535        g.add_dep(1, 2);
536        g.add_dep(2, 3);
537        g.add_dep(1, 3);
538        assert_eq!(g.dependencies_of(2), vec![1]);
539        let topo = g.topological_sort();
540        assert_eq!(topo.len(), 3);
541        assert!(!g.has_cycle());
542        let pos: std::collections::HashMap<u32, usize> =
543            topo.iter().enumerate().map(|(i, &n)| (n, i)).collect();
544        assert!(pos[&1] < pos[&2]);
545        assert!(pos[&1] < pos[&3]);
546        assert!(pos[&2] < pos[&3]);
547    }
548}
549#[cfg(test)]
550mod agdaext_pass_tests {
551    use super::*;
552    #[test]
553    pub(super) fn test_agdaext_phase_order() {
554        assert_eq!(AgdaExtPassPhase::Early.order(), 0);
555        assert_eq!(AgdaExtPassPhase::Middle.order(), 1);
556        assert_eq!(AgdaExtPassPhase::Late.order(), 2);
557        assert_eq!(AgdaExtPassPhase::Finalize.order(), 3);
558        assert!(AgdaExtPassPhase::Early.is_early());
559        assert!(!AgdaExtPassPhase::Early.is_late());
560    }
561    #[test]
562    pub(super) fn test_agdaext_config_builder() {
563        let c = AgdaExtPassConfig::new("p")
564            .with_phase(AgdaExtPassPhase::Late)
565            .with_max_iter(50)
566            .with_debug(1);
567        assert_eq!(c.name, "p");
568        assert_eq!(c.max_iterations, 50);
569        assert!(c.is_debug_enabled());
570        assert!(c.enabled);
571        let c2 = c.disabled();
572        assert!(!c2.enabled);
573    }
574    #[test]
575    pub(super) fn test_agdaext_stats() {
576        let mut s = AgdaExtPassStats::new();
577        s.visit();
578        s.visit();
579        s.modify();
580        s.iterate();
581        assert_eq!(s.nodes_visited, 2);
582        assert_eq!(s.nodes_modified, 1);
583        assert!(s.changed);
584        assert_eq!(s.iterations, 1);
585        let e = s.efficiency();
586        assert!((e - 0.5).abs() < 1e-9);
587    }
588    #[test]
589    pub(super) fn test_agdaext_registry() {
590        let mut r = AgdaExtPassRegistry::new();
591        r.register(AgdaExtPassConfig::new("a").with_phase(AgdaExtPassPhase::Early));
592        r.register(AgdaExtPassConfig::new("b").disabled());
593        assert_eq!(r.len(), 2);
594        assert_eq!(r.enabled_passes().len(), 1);
595        assert_eq!(r.passes_in_phase(&AgdaExtPassPhase::Early).len(), 1);
596    }
597    #[test]
598    pub(super) fn test_agdaext_cache() {
599        let mut c = AgdaExtCache::new(4);
600        assert!(c.get(99).is_none());
601        c.put(99, vec![1, 2, 3]);
602        let v = c.get(99).expect("v should be present in map");
603        assert_eq!(v, &[1u8, 2, 3]);
604        assert!(c.hit_rate() > 0.0);
605        assert_eq!(c.live_count(), 1);
606    }
607    #[test]
608    pub(super) fn test_agdaext_worklist() {
609        let mut w = AgdaExtWorklist::new(10);
610        w.push(5);
611        w.push(3);
612        w.push(5);
613        assert_eq!(w.len(), 2);
614        assert!(w.contains(5));
615        let first = w.pop().expect("first should be available to pop");
616        assert!(!w.contains(first));
617    }
618    #[test]
619    pub(super) fn test_agdaext_dom_tree() {
620        let mut dt = AgdaExtDomTree::new(5);
621        dt.set_idom(1, 0);
622        dt.set_idom(2, 0);
623        dt.set_idom(3, 1);
624        dt.set_idom(4, 1);
625        assert!(dt.dominates(0, 3));
626        assert!(dt.dominates(1, 4));
627        assert!(!dt.dominates(2, 3));
628        assert_eq!(dt.depth_of(3), 2);
629    }
630    #[test]
631    pub(super) fn test_agdaext_liveness() {
632        let mut lv = AgdaExtLiveness::new(3);
633        lv.add_def(0, 1);
634        lv.add_use(1, 1);
635        assert!(lv.var_is_def_in_block(0, 1));
636        assert!(lv.var_is_used_in_block(1, 1));
637        assert!(!lv.var_is_def_in_block(1, 1));
638    }
639    #[test]
640    pub(super) fn test_agdaext_const_folder() {
641        let mut cf = AgdaExtConstFolder::new();
642        assert_eq!(cf.add_i64(3, 4), Some(7));
643        assert_eq!(cf.div_i64(10, 0), None);
644        assert_eq!(cf.mul_i64(6, 7), Some(42));
645        assert_eq!(cf.and_i64(0b1100, 0b1010), 0b1000);
646        assert_eq!(cf.fold_count(), 3);
647        assert_eq!(cf.failure_count(), 1);
648    }
649    #[test]
650    pub(super) fn test_agdaext_dep_graph() {
651        let mut g = AgdaExtDepGraph::new(4);
652        g.add_edge(0, 1);
653        g.add_edge(1, 2);
654        g.add_edge(2, 3);
655        assert!(!g.has_cycle());
656        assert_eq!(g.topo_sort(), Some(vec![0, 1, 2, 3]));
657        assert_eq!(g.reachable(0).len(), 4);
658        let sccs = g.scc();
659        assert_eq!(sccs.len(), 4);
660    }
661}
662#[cfg(test)]
663mod agdax2_pass_tests {
664    use super::*;
665    #[test]
666    pub(super) fn test_agdax2_phase_order() {
667        assert_eq!(AgdaX2PassPhase::Early.order(), 0);
668        assert_eq!(AgdaX2PassPhase::Middle.order(), 1);
669        assert_eq!(AgdaX2PassPhase::Late.order(), 2);
670        assert_eq!(AgdaX2PassPhase::Finalize.order(), 3);
671        assert!(AgdaX2PassPhase::Early.is_early());
672        assert!(!AgdaX2PassPhase::Early.is_late());
673    }
674    #[test]
675    pub(super) fn test_agdax2_config_builder() {
676        let c = AgdaX2PassConfig::new("p")
677            .with_phase(AgdaX2PassPhase::Late)
678            .with_max_iter(50)
679            .with_debug(1);
680        assert_eq!(c.name, "p");
681        assert_eq!(c.max_iterations, 50);
682        assert!(c.is_debug_enabled());
683        assert!(c.enabled);
684        let c2 = c.disabled();
685        assert!(!c2.enabled);
686    }
687    #[test]
688    pub(super) fn test_agdax2_stats() {
689        let mut s = AgdaX2PassStats::new();
690        s.visit();
691        s.visit();
692        s.modify();
693        s.iterate();
694        assert_eq!(s.nodes_visited, 2);
695        assert_eq!(s.nodes_modified, 1);
696        assert!(s.changed);
697        assert_eq!(s.iterations, 1);
698        let e = s.efficiency();
699        assert!((e - 0.5).abs() < 1e-9);
700    }
701    #[test]
702    pub(super) fn test_agdax2_registry() {
703        let mut r = AgdaX2PassRegistry::new();
704        r.register(AgdaX2PassConfig::new("a").with_phase(AgdaX2PassPhase::Early));
705        r.register(AgdaX2PassConfig::new("b").disabled());
706        assert_eq!(r.len(), 2);
707        assert_eq!(r.enabled_passes().len(), 1);
708        assert_eq!(r.passes_in_phase(&AgdaX2PassPhase::Early).len(), 1);
709    }
710    #[test]
711    pub(super) fn test_agdax2_cache() {
712        let mut c = AgdaX2Cache::new(4);
713        assert!(c.get(99).is_none());
714        c.put(99, vec![1, 2, 3]);
715        let v = c.get(99).expect("v should be present in map");
716        assert_eq!(v, &[1u8, 2, 3]);
717        assert!(c.hit_rate() > 0.0);
718        assert_eq!(c.live_count(), 1);
719    }
720    #[test]
721    pub(super) fn test_agdax2_worklist() {
722        let mut w = AgdaX2Worklist::new(10);
723        w.push(5);
724        w.push(3);
725        w.push(5);
726        assert_eq!(w.len(), 2);
727        assert!(w.contains(5));
728        let first = w.pop().expect("first should be available to pop");
729        assert!(!w.contains(first));
730    }
731    #[test]
732    pub(super) fn test_agdax2_dom_tree() {
733        let mut dt = AgdaX2DomTree::new(5);
734        dt.set_idom(1, 0);
735        dt.set_idom(2, 0);
736        dt.set_idom(3, 1);
737        dt.set_idom(4, 1);
738        assert!(dt.dominates(0, 3));
739        assert!(dt.dominates(1, 4));
740        assert!(!dt.dominates(2, 3));
741        assert_eq!(dt.depth_of(3), 2);
742    }
743    #[test]
744    pub(super) fn test_agdax2_liveness() {
745        let mut lv = AgdaX2Liveness::new(3);
746        lv.add_def(0, 1);
747        lv.add_use(1, 1);
748        assert!(lv.var_is_def_in_block(0, 1));
749        assert!(lv.var_is_used_in_block(1, 1));
750        assert!(!lv.var_is_def_in_block(1, 1));
751    }
752    #[test]
753    pub(super) fn test_agdax2_const_folder() {
754        let mut cf = AgdaX2ConstFolder::new();
755        assert_eq!(cf.add_i64(3, 4), Some(7));
756        assert_eq!(cf.div_i64(10, 0), None);
757        assert_eq!(cf.mul_i64(6, 7), Some(42));
758        assert_eq!(cf.and_i64(0b1100, 0b1010), 0b1000);
759        assert_eq!(cf.fold_count(), 3);
760        assert_eq!(cf.failure_count(), 1);
761    }
762    #[test]
763    pub(super) fn test_agdax2_dep_graph() {
764        let mut g = AgdaX2DepGraph::new(4);
765        g.add_edge(0, 1);
766        g.add_edge(1, 2);
767        g.add_edge(2, 3);
768        assert!(!g.has_cycle());
769        assert_eq!(g.topo_sort(), Some(vec![0, 1, 2, 3]));
770        assert_eq!(g.reachable(0).len(), 4);
771        let sccs = g.scc();
772        assert_eq!(sccs.len(), 4);
773    }
774}
oxilean_codegen/agda_backend/functions.rs

oxilean_codegen/agda_backend/
functions.rs
