oxilean_std/compiler_theory/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
6use std::collections::{BTreeMap, HashMap, HashSet, VecDeque};
7
8use super::types::{
9    AbstractInterpreter, BasicBlock, Closure, CompilerCorrectness, ContextFreeGrammar,
10    DataFlowAnalysis, DataflowSolver, GrammarType, HMType, HindleyMilnerInference, LRParser,
11    PushdownAutomaton, RegisterAllocation, RegisterColoringSimple, SSAConstructor, SSAForm,
12    SignValue, TypedLambdaCalculus,
13};
14
15pub fn app(f: Expr, a: Expr) -> Expr {
16    Expr::App(Box::new(f), Box::new(a))
17}
18pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
19    app(app(f, a), b)
20}
21pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
22    app(app2(f, a, b), c)
23}
24pub fn cst(s: &str) -> Expr {
25    Expr::Const(Name::str(s), vec![])
26}
27pub fn prop() -> Expr {
28    Expr::Sort(Level::zero())
29}
30pub fn type0() -> Expr {
31    Expr::Sort(Level::succ(Level::zero()))
32}
33pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
34    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
35}
36pub fn arrow(a: Expr, b: Expr) -> Expr {
37    pi(BinderInfo::Default, "_", a, b)
38}
39pub fn bvar(n: u32) -> Expr {
40    Expr::BVar(n)
41}
42pub fn nat_ty() -> Expr {
43    cst("Nat")
44}
45pub fn bool_ty() -> Expr {
46    cst("Bool")
47}
48pub fn string_ty() -> Expr {
49    cst("String")
50}
51pub fn list_ty(elem: Expr) -> Expr {
52    app(cst("List"), elem)
53}
54pub fn option_ty(elem: Expr) -> Expr {
55    app(cst("Option"), elem)
56}
57pub fn pair_ty(a: Expr, b: Expr) -> Expr {
58    app2(cst("Prod"), a, b)
59}
60pub fn grammar_type_ty() -> Expr {
61    type0()
62}
63pub fn context_free_grammar_ty() -> Expr {
64    type0()
65}
66pub fn pushdown_automaton_ty() -> Expr {
67    type0()
68}
69pub fn lr_parser_ty() -> Expr {
70    type0()
71}
72pub fn typed_lambda_calculus_ty() -> Expr {
73    type0()
74}
75pub fn closure_ty() -> Expr {
76    type0()
77}
78pub fn register_allocation_ty() -> Expr {
79    type0()
80}
81pub fn data_flow_analysis_ty() -> Expr {
82    type0()
83}
84pub fn ssa_form_ty() -> Expr {
85    type0()
86}
87pub fn compiler_correctness_ty() -> Expr {
88    type0()
89}
90pub fn chomsky_hierarchy_ty() -> Expr {
91    arrow(grammar_type_ty(), nat_ty())
92}
93pub fn cfg_is_ambiguous_ty() -> Expr {
94    arrow(context_free_grammar_ty(), bool_ty())
95}
96pub fn cfg_cnf_ty() -> Expr {
97    arrow(context_free_grammar_ty(), context_free_grammar_ty())
98}
99pub fn cyk_parse_ty() -> Expr {
100    arrow(
101        context_free_grammar_ty(),
102        arrow(list_ty(nat_ty()), bool_ty()),
103    )
104}
105pub fn pda_accepts_ty() -> Expr {
106    arrow(pushdown_automaton_ty(), arrow(list_ty(nat_ty()), bool_ty()))
107}
108pub fn lr_is_lr1_ty() -> Expr {
109    arrow(lr_parser_ty(), bool_ty())
110}
111pub fn tlc_is_normalizing_ty() -> Expr {
112    arrow(typed_lambda_calculus_ty(), bool_ty())
113}
114pub fn closure_convert_ty() -> Expr {
115    arrow(closure_ty(), closure_ty())
116}
117pub fn reg_alloc_graph_color_ty() -> Expr {
118    arrow(register_allocation_ty(), option_ty(list_ty(nat_ty())))
119}
120pub fn dataflow_worklist_ty() -> Expr {
121    arrow(data_flow_analysis_ty(), bool_ty())
122}
123pub fn ssa_convert_ty() -> Expr {
124    arrow(ssa_form_ty(), ssa_form_ty())
125}
126pub fn compiler_correctness_sim_ty() -> Expr {
127    arrow(compiler_correctness_ty(), prop())
128}
129pub fn type_scheme_ty() -> Expr {
130    type0()
131}
132pub fn substitution_ty() -> Expr {
133    type0()
134}
135pub fn unification_problem_ty() -> Expr {
136    type0()
137}
138pub fn type_env_ty() -> Expr {
139    type0()
140}
141/// Hindley-Milner type inference: TypeEnv → Expr → Option TypeScheme
142pub fn hindley_milner_infer_ty() -> Expr {
143    arrow(type_env_ty(), arrow(type0(), option_ty(type_scheme_ty())))
144}
145/// Algorithm W: TypeEnv → Expr → Option (Substitution × Type)
146pub fn algorithm_w_ty() -> Expr {
147    arrow(
148        type_env_ty(),
149        arrow(type0(), option_ty(pair_ty(substitution_ty(), type0()))),
150    )
151}
152/// Unification: two types → Option Substitution
153pub fn unification_ty() -> Expr {
154    arrow(type0(), arrow(type0(), option_ty(substitution_ty())))
155}
156/// Most general unifier: unification is complete
157pub fn mgu_complete_ty() -> Expr {
158    arrow(unification_problem_ty(), option_ty(substitution_ty()))
159}
160pub fn system_f_term_ty() -> Expr {
161    type0()
162}
163pub fn rank_n_type_ty() -> Expr {
164    type0()
165}
166/// System F type-checking: SystemFTerm → Bool
167pub fn system_f_type_check_ty() -> Expr {
168    arrow(system_f_term_ty(), bool_ty())
169}
170/// Rank-n polymorphism check: RankNType → Nat → Bool
171pub fn rank_n_check_ty() -> Expr {
172    arrow(rank_n_type_ty(), arrow(nat_ty(), bool_ty()))
173}
174/// Impredicativity: System F allows instantiation with polymorphic types
175pub fn system_f_impredicative_ty() -> Expr {
176    arrow(system_f_term_ty(), arrow(type0(), system_f_term_ty()))
177}
178pub fn domain_equation_ty() -> Expr {
179    type0()
180}
181pub fn fixpoint_sem_ty() -> Expr {
182    type0()
183}
184/// Domain equation solver: DomainEquation → Type
185pub fn domain_eq_solve_ty() -> Expr {
186    arrow(domain_equation_ty(), type0())
187}
188/// Fixpoint semantics: FixpointSem → (Type → Type) → Type
189pub fn fixpoint_semantics_ty() -> Expr {
190    arrow(fixpoint_sem_ty(), arrow(arrow(type0(), type0()), type0()))
191}
192/// Full abstraction: observational equivalence = denotational equality
193pub fn full_abstraction_ty() -> Expr {
194    arrow(fixpoint_sem_ty(), prop())
195}
196pub fn small_step_rel_ty() -> Expr {
197    type0()
198}
199pub fn big_step_rel_ty() -> Expr {
200    type0()
201}
202pub fn bisimulation_ty() -> Expr {
203    type0()
204}
205/// Small-step step: SmallStepRel → Expr → Option Expr
206pub fn small_step_ty() -> Expr {
207    arrow(small_step_rel_ty(), arrow(type0(), option_ty(type0())))
208}
209/// Big-step eval: BigStepRel → Expr → Option Value
210pub fn big_step_ty() -> Expr {
211    arrow(big_step_rel_ty(), arrow(type0(), option_ty(type0())))
212}
213/// Bisimulation check: Bisimulation → Bool
214pub fn bisimulation_check_ty() -> Expr {
215    arrow(bisimulation_ty(), bool_ty())
216}
217/// Logical relation: two terms are logically related at a type
218pub fn logical_relation_ty() -> Expr {
219    arrow(type0(), arrow(type0(), arrow(type0(), prop())))
220}
221pub fn abstract_domain_ty() -> Expr {
222    type0()
223}
224pub fn galois_connection_ty() -> Expr {
225    type0()
226}
227/// Galois connection: AbstractDomain → (Expr → Expr) → Bool (monotone)
228pub fn galois_connection_monotone_ty() -> Expr {
229    arrow(galois_connection_ty(), prop())
230}
231/// Widening operator: AbstractDomain → AbstractDomain → AbstractDomain
232pub fn widening_ty() -> Expr {
233    arrow(
234        abstract_domain_ty(),
235        arrow(abstract_domain_ty(), abstract_domain_ty()),
236    )
237}
238/// Narrowing operator: AbstractDomain → AbstractDomain → AbstractDomain
239pub fn narrowing_ty() -> Expr {
240    arrow(
241        abstract_domain_ty(),
242        arrow(abstract_domain_ty(), abstract_domain_ty()),
243    )
244}
245/// Abstract fixpoint: (AbstractDomain → AbstractDomain) → AbstractDomain
246pub fn abstract_fixpoint_ty() -> Expr {
247    arrow(
248        arrow(abstract_domain_ty(), abstract_domain_ty()),
249        abstract_domain_ty(),
250    )
251}
252pub fn call_graph_ty() -> Expr {
253    type0()
254}
255pub fn cfa_result_ty() -> Expr {
256    type0()
257}
258/// 0-CFA analysis: Program → CFAResult
259pub fn zero_cfa_ty() -> Expr {
260    arrow(type0(), cfa_result_ty())
261}
262/// k-CFA analysis: Nat → Program → CFAResult
263pub fn k_cfa_ty() -> Expr {
264    arrow(nat_ty(), arrow(type0(), cfa_result_ty()))
265}
266/// Points-to analysis: Program → (Var → Set Addr)
267pub fn points_to_analysis_ty() -> Expr {
268    arrow(type0(), arrow(type0(), list_ty(nat_ty())))
269}
270/// Call graph construction: Program → CallGraph
271pub fn call_graph_build_ty() -> Expr {
272    arrow(type0(), call_graph_ty())
273}
274pub fn reaching_def_ty() -> Expr {
275    type0()
276}
277pub fn live_var_ty() -> Expr {
278    type0()
279}
280pub fn avail_expr_ty() -> Expr {
281    type0()
282}
283/// Reaching definitions: BasicBlock → ReachingDef
284pub fn reaching_definitions_ty() -> Expr {
285    arrow(type0(), reaching_def_ty())
286}
287/// Live variable analysis: BasicBlock → LiveVar
288pub fn live_variables_ty() -> Expr {
289    arrow(type0(), live_var_ty())
290}
291/// Available expressions: BasicBlock → AvailExpr
292pub fn available_expressions_ty() -> Expr {
293    arrow(type0(), avail_expr_ty())
294}
295pub fn phi_function_ty() -> Expr {
296    type0()
297}
298pub fn dom_frontier_ty() -> Expr {
299    type0()
300}
301/// Dominance frontier: CFG → DomFrontier
302pub fn dominance_frontier_ty() -> Expr {
303    arrow(type0(), dom_frontier_ty())
304}
305/// SSA construction: CFG → DomFrontier → SSAForm
306pub fn ssa_construction_ty() -> Expr {
307    arrow(type0(), arrow(dom_frontier_ty(), ssa_form_ty()))
308}
309/// Phi function placement: DomFrontier → List PhiFunction
310pub fn phi_placement_ty() -> Expr {
311    arrow(dom_frontier_ty(), list_ty(phi_function_ty()))
312}
313pub fn interference_graph_ty() -> Expr {
314    type0()
315}
316pub fn spill_code_ty() -> Expr {
317    type0()
318}
319/// Linear scan allocation: List LiveRange → Nat → Option (List Register)
320pub fn linear_scan_alloc_ty() -> Expr {
321    arrow(
322        list_ty(pair_ty(nat_ty(), nat_ty())),
323        arrow(nat_ty(), option_ty(list_ty(nat_ty()))),
324    )
325}
326/// Spill code insertion: InterferenceGraph → SpillCode
327pub fn spill_code_insert_ty() -> Expr {
328    arrow(interference_graph_ty(), spill_code_ty())
329}
330pub fn tree_pattern_ty() -> Expr {
331    type0()
332}
333pub fn instruction_ty() -> Expr {
334    type0()
335}
336/// Tree tiling (BURS): TreePattern → Instruction
337pub fn tree_tiling_ty() -> Expr {
338    arrow(tree_pattern_ty(), instruction_ty())
339}
340/// Instruction selection: IR → List Instruction
341pub fn instruction_selection_ty() -> Expr {
342    arrow(type0(), list_ty(instruction_ty()))
343}
344pub fn basic_block_ty() -> Expr {
345    type0()
346}
347pub fn dag_ty() -> Expr {
348    type0()
349}
350/// Basic block scheduling: BasicBlock → BasicBlock
351pub fn basic_block_schedule_ty() -> Expr {
352    arrow(basic_block_ty(), basic_block_ty())
353}
354/// DAG scheduling: DAG → List Instruction
355pub fn dag_schedule_ty() -> Expr {
356    arrow(dag_ty(), list_ty(instruction_ty()))
357}
358pub fn inline_candidate_ty() -> Expr {
359    type0()
360}
361pub fn loop_nest_ty() -> Expr {
362    type0()
363}
364/// Inlining: InlineCandidate → IR → IR
365pub fn inlining_ty() -> Expr {
366    arrow(inline_candidate_ty(), arrow(type0(), type0()))
367}
368/// Loop transformation (unroll/tile): LoopNest → LoopNest
369pub fn loop_transform_ty() -> Expr {
370    arrow(loop_nest_ty(), loop_nest_ty())
371}
372/// Vectorization: LoopNest → Option (List Instruction)
373pub fn vectorization_ty() -> Expr {
374    arrow(loop_nest_ty(), option_ty(list_ty(instruction_ty())))
375}
376pub fn heap_ty() -> Expr {
377    type0()
378}
379pub fn gc_roots_ty() -> Expr {
380    type0()
381}
382/// Mark-sweep GC: Heap → GCRoots → Heap
383pub fn mark_sweep_ty() -> Expr {
384    arrow(heap_ty(), arrow(gc_roots_ty(), heap_ty()))
385}
386/// Copying GC: Heap → GCRoots → Heap
387pub fn copying_gc_ty() -> Expr {
388    arrow(heap_ty(), arrow(gc_roots_ty(), heap_ty()))
389}
390/// Generational GC: Nat (generations) → Heap → GCRoots → Heap
391pub fn generational_gc_ty() -> Expr {
392    arrow(nat_ty(), arrow(heap_ty(), arrow(gc_roots_ty(), heap_ty())))
393}
394/// Incremental GC: Bool (pause-free) → Heap → GCRoots → Heap
395pub fn incremental_gc_ty() -> Expr {
396    arrow(bool_ty(), arrow(heap_ty(), arrow(gc_roots_ty(), heap_ty())))
397}
398pub fn jit_state_ty() -> Expr {
399    type0()
400}
401pub fn deopt_info_ty() -> Expr {
402    type0()
403}
404/// On-stack replacement: JITState → Nat (point) → JITState
405pub fn on_stack_replacement_ty() -> Expr {
406    arrow(jit_state_ty(), arrow(nat_ty(), jit_state_ty()))
407}
408/// Deoptimization: JITState → DeoptInfo → JITState
409pub fn deoptimization_ty() -> Expr {
410    arrow(jit_state_ty(), arrow(deopt_info_ty(), jit_state_ty()))
411}
412/// Tracing JIT: JITState → List Instruction → JITState
413pub fn tracing_jit_ty() -> Expr {
414    arrow(
415        jit_state_ty(),
416        arrow(list_ty(instruction_ty()), jit_state_ty()),
417    )
418}
419pub fn simulation_rel_ty() -> Expr {
420    type0()
421}
422/// CompCert-style forward simulation: SimulationRel → Prop
423pub fn forward_simulation_ty() -> Expr {
424    arrow(simulation_rel_ty(), prop())
425}
426/// CakeML-style verified semantics preservation: IR → IR → Prop
427pub fn semantics_preservation_ty() -> Expr {
428    arrow(type0(), arrow(type0(), prop()))
429}
430pub fn build_compiler_theory_env() -> Environment {
431    let mut env = Environment::new();
432    let axioms: &[(&str, Expr)] = &[
433        ("GrammarType", grammar_type_ty()),
434        ("ContextFreeGrammar", context_free_grammar_ty()),
435        ("PushdownAutomaton", pushdown_automaton_ty()),
436        ("LRParser", lr_parser_ty()),
437        ("TypedLambdaCalculus", typed_lambda_calculus_ty()),
438        ("Closure", closure_ty()),
439        ("RegisterAllocation", register_allocation_ty()),
440        ("DataFlowAnalysis", data_flow_analysis_ty()),
441        ("SSAForm", ssa_form_ty()),
442        ("CompilerCorrectness", compiler_correctness_ty()),
443        ("ChomskyHierarchy", chomsky_hierarchy_ty()),
444        ("CFG_IsAmbiguous", cfg_is_ambiguous_ty()),
445        ("CFG_ChomskyNormalForm", cfg_cnf_ty()),
446        ("CYKParse", cyk_parse_ty()),
447        ("PDA_Accepts", pda_accepts_ty()),
448        ("LR_IsLR1", lr_is_lr1_ty()),
449        ("TLC_IsNormalizing", tlc_is_normalizing_ty()),
450        ("ClosureConvert", closure_convert_ty()),
451        ("RegAlloc_GraphColor", reg_alloc_graph_color_ty()),
452        ("DataFlow_Worklist", dataflow_worklist_ty()),
453        ("SSA_Convert", ssa_convert_ty()),
454        ("CompilerCorrectness_Sim", compiler_correctness_sim_ty()),
455        ("TypeScheme", type_scheme_ty()),
456        ("Substitution", substitution_ty()),
457        ("UnificationProblem", unification_problem_ty()),
458        ("TypeEnv", type_env_ty()),
459        ("HindleyMilner_Infer", hindley_milner_infer_ty()),
460        ("AlgorithmW", algorithm_w_ty()),
461        ("Unification", unification_ty()),
462        ("MGU_Complete", mgu_complete_ty()),
463        ("SystemFTerm", system_f_term_ty()),
464        ("RankNType", rank_n_type_ty()),
465        ("SystemF_TypeCheck", system_f_type_check_ty()),
466        ("RankN_Check", rank_n_check_ty()),
467        ("SystemF_Impredicative", system_f_impredicative_ty()),
468        ("DomainEquation", domain_equation_ty()),
469        ("FixpointSem", fixpoint_sem_ty()),
470        ("DomainEq_Solve", domain_eq_solve_ty()),
471        ("Fixpoint_Semantics", fixpoint_semantics_ty()),
472        ("FullAbstraction", full_abstraction_ty()),
473        ("SmallStepRel", small_step_rel_ty()),
474        ("BigStepRel", big_step_rel_ty()),
475        ("Bisimulation", bisimulation_ty()),
476        ("SmallStep", small_step_ty()),
477        ("BigStep", big_step_ty()),
478        ("Bisimulation_Check", bisimulation_check_ty()),
479        ("LogicalRelation", logical_relation_ty()),
480        ("AbstractDomain", abstract_domain_ty()),
481        ("GaloisConnection", galois_connection_ty()),
482        ("GaloisConnection_Monotone", galois_connection_monotone_ty()),
483        ("Widening", widening_ty()),
484        ("Narrowing", narrowing_ty()),
485        ("AbstractFixpoint", abstract_fixpoint_ty()),
486        ("CallGraph", call_graph_ty()),
487        ("CFAResult", cfa_result_ty()),
488        ("ZeroCFA", zero_cfa_ty()),
489        ("KCFA", k_cfa_ty()),
490        ("PointsTo_Analysis", points_to_analysis_ty()),
491        ("CallGraph_Build", call_graph_build_ty()),
492        ("ReachingDef", reaching_def_ty()),
493        ("LiveVar", live_var_ty()),
494        ("AvailExpr", avail_expr_ty()),
495        ("ReachingDefinitions", reaching_definitions_ty()),
496        ("LiveVariables", live_variables_ty()),
497        ("AvailableExpressions", available_expressions_ty()),
498        ("PhiFunction", phi_function_ty()),
499        ("DomFrontier", dom_frontier_ty()),
500        ("DominanceFrontier", dominance_frontier_ty()),
501        ("SSA_Construction", ssa_construction_ty()),
502        ("PhiPlacement", phi_placement_ty()),
503        ("InterferenceGraph", interference_graph_ty()),
504        ("SpillCode", spill_code_ty()),
505        ("LinearScan_Alloc", linear_scan_alloc_ty()),
506        ("SpillCode_Insert", spill_code_insert_ty()),
507        ("TreePattern", tree_pattern_ty()),
508        ("Instruction", instruction_ty()),
509        ("TreeTiling", tree_tiling_ty()),
510        ("InstructionSelection", instruction_selection_ty()),
511        ("BasicBlock", basic_block_ty()),
512        ("DAG", dag_ty()),
513        ("BasicBlock_Schedule", basic_block_schedule_ty()),
514        ("DAG_Schedule", dag_schedule_ty()),
515        ("InlineCandidate", inline_candidate_ty()),
516        ("LoopNest", loop_nest_ty()),
517        ("Inlining", inlining_ty()),
518        ("LoopTransform", loop_transform_ty()),
519        ("Vectorization", vectorization_ty()),
520        ("Heap", heap_ty()),
521        ("GCRoots", gc_roots_ty()),
522        ("MarkSweep", mark_sweep_ty()),
523        ("CopyingGC", copying_gc_ty()),
524        ("GenerationalGC", generational_gc_ty()),
525        ("IncrementalGC", incremental_gc_ty()),
526        ("JITState", jit_state_ty()),
527        ("DeoptInfo", deopt_info_ty()),
528        ("OnStackReplacement", on_stack_replacement_ty()),
529        ("Deoptimization", deoptimization_ty()),
530        ("TracingJIT", tracing_jit_ty()),
531        ("SimulationRel", simulation_rel_ty()),
532        ("ForwardSimulation", forward_simulation_ty()),
533        ("SemanticPreservation", semantics_preservation_ty()),
534    ];
535    for (name, ty) in axioms {
536        env.add(Declaration::Axiom {
537            name: Name::str(*name),
538            univ_params: vec![],
539            ty: ty.clone(),
540        })
541        .ok();
542    }
543    env
544}
545#[cfg(test)]
546mod tests {
547    use super::*;
548    #[test]
549    fn test_build_env_nonempty() {
550        let env = build_compiler_theory_env();
551        let names = [
552            "GrammarType",
553            "ContextFreeGrammar",
554            "PushdownAutomaton",
555            "LRParser",
556            "TypedLambdaCalculus",
557            "Closure",
558            "RegisterAllocation",
559            "DataFlowAnalysis",
560            "SSAForm",
561            "CompilerCorrectness",
562        ];
563        let count = names
564            .iter()
565            .filter(|&&n| env.get(&Name::str(n)).is_some())
566            .count();
567        assert_eq!(count, 10);
568    }
569    #[test]
570    fn test_grammar_type_chomsky() {
571        assert_eq!(GrammarType::Regular.chomsky_hierarchy_level(), 3);
572        assert_eq!(GrammarType::CFL.chomsky_hierarchy_level(), 2);
573        assert_eq!(GrammarType::CSL.chomsky_hierarchy_level(), 1);
574        assert_eq!(
575            GrammarType::RecursivelyEnumerable.chomsky_hierarchy_level(),
576            0
577        );
578    }
579    #[test]
580    fn test_grammar_type_closure_regular() {
581        let props = GrammarType::Regular.closure_properties();
582        assert!(props.contains(&"complement"));
583        assert!(props.contains(&"union"));
584    }
585    #[test]
586    fn test_cfg_cyk_parse_simple() {
587        let cfg = ContextFreeGrammar::new(
588            vec!['S', 'A', 'B'],
589            vec!['a', 'b'],
590            'S',
591            vec![
592                ('S', "AB".to_string()),
593                ('A', "a".to_string()),
594                ('B', "b".to_string()),
595            ],
596        );
597        assert!(cfg.cyk_parse(&['a', 'b']));
598        assert!(!cfg.cyk_parse(&['b', 'a']));
599        assert!(!cfg.cyk_parse(&['a']));
600    }
601    #[test]
602    fn test_cfg_is_ambiguous_false() {
603        let cfg = ContextFreeGrammar::new(
604            vec!['S'],
605            vec!['a'],
606            'S',
607            vec![('S', "a".to_string()), ('S', "aa".to_string())],
608        );
609        assert!(!cfg.is_ambiguous());
610    }
611    #[test]
612    fn test_cfg_is_ambiguous_true() {
613        let cfg = ContextFreeGrammar::new(
614            vec!['S'],
615            vec!['a'],
616            'S',
617            vec![('S', "a".to_string()), ('S', "a".to_string())],
618        );
619        assert!(cfg.is_ambiguous());
620    }
621    #[test]
622    fn test_cfg_cnf() {
623        let cfg = ContextFreeGrammar::new(
624            vec!['S'],
625            vec!['a', 'b', 'c'],
626            'S',
627            vec![('S', "abc".to_string())],
628        );
629        let cnf = cfg.chomsky_normal_form();
630        for (_, rhs) in &cnf.rules {
631            assert!(rhs.chars().count() <= 2);
632        }
633    }
634    #[test]
635    fn test_pda_accepts() {
636        let pda = PushdownAutomaton::new(2, vec!['Z'], vec![]);
637        assert!(pda.accepts(&[]));
638    }
639    #[test]
640    fn test_lr_parser_is_lr1_clean() {
641        let action = vec![
642            vec!["s1".to_string(), "".to_string()],
643            vec!["acc".to_string(), "r1".to_string()],
644        ];
645        let goto = vec![vec![1usize], vec![0usize]];
646        let parser = LRParser::new(2, action, goto);
647        assert!(parser.is_lr1());
648    }
649    #[test]
650    fn test_lr_parser_conflict() {
651        let action = vec![vec!["s1,r2".to_string()]];
652        let goto = vec![vec![0usize]];
653        let parser = LRParser::new(1, action, goto);
654        assert!(!parser.is_lr1());
655    }
656    #[test]
657    fn test_typed_lambda_calculus() {
658        assert!(TypedLambdaCalculus::SimplyTyped.is_normalizing());
659        assert!(TypedLambdaCalculus::SimplyTyped.is_decidable());
660        assert!(TypedLambdaCalculus::SystemF.is_normalizing());
661        assert!(!TypedLambdaCalculus::SystemF.is_decidable());
662        assert!(TypedLambdaCalculus::CoC.is_decidable());
663    }
664    #[test]
665    fn test_closure_convert() {
666        let c = Closure::new(
667            vec!["x".to_string(), "y".to_string()],
668            vec![("z".to_string(), "42".to_string())],
669        );
670        let converted = c.closure_convert();
671        assert!(converted.free_vars.is_empty());
672        assert!(converted.env.iter().any(|(k, _)| k == "x"));
673        assert!(converted.env.iter().any(|(k, _)| k == "y"));
674    }
675    #[test]
676    fn test_closure_lambda_lift() {
677        let c = Closure::new(
678            vec!["x".to_string()],
679            vec![("y".to_string(), "1".to_string())],
680        );
681        let params = c.lambda_lift();
682        assert!(params.contains(&"x".to_string()));
683        assert!(params.contains(&"y".to_string()));
684    }
685    #[test]
686    fn test_register_allocation_graph_color() {
687        let ra = RegisterAllocation::new(
688            vec!["a".to_string(), "b".to_string(), "c".to_string()],
689            vec![(0, 2), (3, 5), (6, 8)],
690            2,
691        );
692        let coloring = ra.graph_color();
693        assert!(coloring.is_some());
694        let c = coloring.expect("coloring should be valid");
695        assert_eq!(c.len(), 3);
696    }
697    #[test]
698    fn test_register_allocation_spill_needed() {
699        let ra = RegisterAllocation::new(
700            vec!["a".to_string(), "b".to_string(), "c".to_string()],
701            vec![(0, 10), (0, 10), (0, 10)],
702            2,
703        );
704        let coloring = ra.graph_color();
705        assert!(coloring.is_none());
706    }
707    #[test]
708    fn test_dataflow_fixed_point() {
709        let df = DataFlowAnalysis::new("forward", "powerset");
710        let result = df.fixed_point(0u32, |&v| if v < 5 { v + 1 } else { v });
711        assert_eq!(result, 5);
712    }
713    #[test]
714    fn test_dataflow_worklist() {
715        let df = DataFlowAnalysis::new("forward", "interval");
716        let edges = vec![vec![1usize], vec![2], vec![]];
717        let init = vec![1u32, 0, 0];
718        let result = df.worklist_algorithm(3, &edges, init, |_, v| *v, |a, b| (*a).max(*b));
719        assert_eq!(result[2], 1);
720    }
721    #[test]
722    fn test_ssa_form_convert() {
723        let ssa = SSAForm::new(
724            vec!["x".to_string(), "x".to_string(), "y".to_string()],
725            vec![("x".to_string(), vec!["x0".to_string(), "x1".to_string()])],
726        );
727        let converted = ssa.convert_to_ssa();
728        assert!(converted.variables.iter().any(|v| v.contains('_')));
729        let frontier = converted.dominance_frontier();
730        assert!(!frontier.is_empty());
731    }
732    #[test]
733    fn test_compiler_correctness() {
734        let cc = CompilerCorrectness::new("denotational_sem", "operational_sem");
735        assert!(cc.observable_equivalence());
736        let sim = cc.simulation_relation();
737        assert!(sim.contains("denotational_sem"));
738        assert!(sim.contains("operational_sem"));
739    }
740    #[test]
741    fn test_spill_cost() {
742        let ra = RegisterAllocation::new(
743            vec!["a".to_string(), "b".to_string()],
744            vec![(0, 4), (1, 3)],
745            4,
746        );
747        let costs = ra.spill_cost();
748        assert_eq!(costs[0], 5.0);
749        assert_eq!(costs[1], 3.0);
750    }
751    #[test]
752    fn test_build_env_new_axioms() {
753        let env = build_compiler_theory_env();
754        let new_names = [
755            "TypeScheme",
756            "Substitution",
757            "HindleyMilner_Infer",
758            "AlgorithmW",
759            "Unification",
760            "MGU_Complete",
761            "SystemFTerm",
762            "RankNType",
763            "SystemF_TypeCheck",
764            "DomainEquation",
765            "FixpointSem",
766            "FullAbstraction",
767            "SmallStepRel",
768            "BigStepRel",
769            "Bisimulation",
770            "LogicalRelation",
771            "GaloisConnection",
772            "Widening",
773            "Narrowing",
774            "AbstractFixpoint",
775            "ZeroCFA",
776            "KCFA",
777            "PointsTo_Analysis",
778            "ReachingDefinitions",
779            "LiveVariables",
780            "AvailableExpressions",
781            "DominanceFrontier",
782            "SSA_Construction",
783            "PhiPlacement",
784            "LinearScan_Alloc",
785            "TreeTiling",
786            "InstructionSelection",
787            "BasicBlock_Schedule",
788            "DAG_Schedule",
789            "Inlining",
790            "LoopTransform",
791            "Vectorization",
792            "MarkSweep",
793            "CopyingGC",
794            "GenerationalGC",
795            "IncrementalGC",
796            "OnStackReplacement",
797            "Deoptimization",
798            "TracingJIT",
799            "ForwardSimulation",
800            "SemanticPreservation",
801        ];
802        let count = new_names
803            .iter()
804            .filter(|&&n| env.get(&Name::str(n)).is_some())
805            .count();
806        assert_eq!(count, new_names.len());
807    }
808    #[test]
809    fn test_hm_infer_simple_types() {
810        let mut hm = HindleyMilnerInference::new();
811        assert_eq!(hm.infer_simple("int"), HMType::Int);
812        assert_eq!(hm.infer_simple("bool"), HMType::Bool);
813        match hm.infer_simple("fun") {
814            HMType::Fun(_, _) => {}
815            other => panic!("expected Fun, got {:?}", other),
816        }
817    }
818    #[test]
819    fn test_hm_unify_base_types() {
820        let mut hm = HindleyMilnerInference::new();
821        assert!(hm.unify(&HMType::Int, &HMType::Int).is_ok());
822        assert!(hm.unify(&HMType::Bool, &HMType::Bool).is_ok());
823        assert!(hm.unify(&HMType::Int, &HMType::Bool).is_err());
824    }
825    #[test]
826    fn test_hm_unify_var() {
827        let mut hm = HindleyMilnerInference::new();
828        let v = hm.fresh();
829        assert!(hm.unify(&v, &HMType::Int).is_ok());
830        let resolved = hm.resolve(&v);
831        assert_eq!(resolved, HMType::Int);
832    }
833    #[test]
834    fn test_hm_unify_fun() {
835        let mut hm = HindleyMilnerInference::new();
836        let t1 = HMType::Fun(Box::new(HMType::Int), Box::new(HMType::Bool));
837        let t2 = HMType::Fun(Box::new(HMType::Int), Box::new(HMType::Bool));
838        assert!(hm.unify(&t1, &t2).is_ok());
839    }
840    #[test]
841    fn test_hm_occurs_check() {
842        let mut hm = HindleyMilnerInference::new();
843        let v = hm.fresh();
844        let v_idx = match &v {
845            HMType::Var(i) => *i,
846            _ => panic!(),
847        };
848        let recursive_ty = HMType::Fun(Box::new(v.clone()), Box::new(v.clone()));
849        assert!(hm.unify(&HMType::Var(v_idx), &recursive_ty).is_err());
850    }
851    #[test]
852    fn test_abstract_interpreter_assign_lookup() {
853        let mut ai = AbstractInterpreter::new();
854        ai.assign("x", SignValue::Positive);
855        assert_eq!(ai.lookup("x"), SignValue::Positive);
856        assert_eq!(ai.lookup("y"), SignValue::Top);
857    }
858    #[test]
859    fn test_sign_join() {
860        assert_eq!(
861            SignValue::Positive.join(&SignValue::Positive),
862            SignValue::Positive
863        );
864        assert_eq!(
865            SignValue::Bottom.join(&SignValue::Negative),
866            SignValue::Negative
867        );
868        assert_eq!(
869            SignValue::Positive.join(&SignValue::Negative),
870            SignValue::Top
871        );
872        assert_eq!(SignValue::Zero.join(&SignValue::Bottom), SignValue::Zero);
873    }
874    #[test]
875    fn test_sign_add() {
876        assert_eq!(
877            SignValue::Positive.add(&SignValue::Positive),
878            SignValue::Positive
879        );
880        assert_eq!(
881            SignValue::Negative.add(&SignValue::Negative),
882            SignValue::Negative
883        );
884        assert_eq!(
885            SignValue::Zero.add(&SignValue::Positive),
886            SignValue::Positive
887        );
888        assert_eq!(
889            SignValue::Positive.add(&SignValue::Negative),
890            SignValue::Top
891        );
892    }
893    #[test]
894    fn test_sign_mul() {
895        assert_eq!(
896            SignValue::Positive.mul(&SignValue::Positive),
897            SignValue::Positive
898        );
899        assert_eq!(
900            SignValue::Negative.mul(&SignValue::Negative),
901            SignValue::Positive
902        );
903        assert_eq!(
904            SignValue::Positive.mul(&SignValue::Negative),
905            SignValue::Negative
906        );
907        assert_eq!(SignValue::Zero.mul(&SignValue::Top), SignValue::Zero);
908    }
909    #[test]
910    fn test_abstract_interpreter_join_state() {
911        let mut ai1 = AbstractInterpreter::new();
912        ai1.assign("x", SignValue::Positive);
913        let mut ai2 = AbstractInterpreter::new();
914        ai2.assign("x", SignValue::Negative);
915        ai2.assign("y", SignValue::Zero);
916        let joined = ai1.join_state(&ai2);
917        assert_eq!(joined.lookup("x"), SignValue::Top);
918        assert_eq!(joined.lookup("y"), SignValue::Zero);
919    }
920    #[test]
921    fn test_abstract_interpreter_widen() {
922        let mut ai1 = AbstractInterpreter::new();
923        ai1.assign("x", SignValue::Positive);
924        let mut ai2 = AbstractInterpreter::new();
925        ai2.assign("x", SignValue::Negative);
926        let widened = ai1.widen(&ai2);
927        assert_eq!(widened.lookup("x"), SignValue::Top);
928    }
929    #[test]
930    fn test_dataflow_solver_forward_simple() {
931        let solver = DataflowSolver::new(
932            3,
933            vec![vec![1], vec![2], vec![]],
934            vec![
935                [0].iter().copied().collect(),
936                [1].iter().copied().collect(),
937                HashSet::new(),
938            ],
939            vec![
940                HashSet::new(),
941                [0].iter().copied().collect(),
942                HashSet::new(),
943            ],
944        );
945        let (_, out) = solver.solve_forward();
946        assert!(out[0].contains(&0));
947        assert!(out[1].contains(&1));
948        assert!(!out[1].contains(&0));
949        assert!(out[2].contains(&1));
950    }
951    #[test]
952    fn test_dataflow_solver_backward_simple() {
953        let solver = DataflowSolver::new(
954            2,
955            vec![vec![1], vec![]],
956            vec![HashSet::new(), [5].iter().copied().collect()],
957            vec![HashSet::new(), HashSet::new()],
958        );
959        let (in_sets, _) = solver.solve_backward();
960        assert!(in_sets[0].contains(&5));
961    }
962    #[test]
963    fn test_reg_coloring_no_interference() {
964        let rc = RegisterColoringSimple::new(3, &[], 1);
965        let coloring = rc.color();
966        assert!(coloring.is_some());
967        let c = coloring.expect("coloring should be valid");
968        assert_eq!(c, vec![0, 0, 0]);
969    }
970    #[test]
971    fn test_reg_coloring_triangle_3regs() {
972        let rc = RegisterColoringSimple::new(3, &[(0, 1), (1, 2), (0, 2)], 3);
973        let coloring = rc.color();
974        assert!(coloring.is_some());
975        let c = coloring.expect("coloring should be valid");
976        assert_ne!(c[0], c[1]);
977        assert_ne!(c[1], c[2]);
978        assert_ne!(c[0], c[2]);
979    }
980    #[test]
981    fn test_reg_coloring_triangle_2regs_impossible() {
982        let rc = RegisterColoringSimple::new(3, &[(0, 1), (1, 2), (0, 2)], 2);
983        assert!(rc.color().is_none());
984    }
985    #[test]
986    fn test_reg_coloring_clique_lower_bound() {
987        let rc =
988            RegisterColoringSimple::new(4, &[(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)], 4);
989        assert!(rc.clique_lower_bound() >= 4);
990    }
991    #[test]
992    fn test_ssa_constructor_all_vars() {
993        let blocks = vec![
994            BasicBlock::new(0, vec!["x".to_string(), "y".to_string()], vec![], vec![1]),
995            BasicBlock::new(1, vec!["z".to_string()], vec!["x".to_string()], vec![]),
996        ];
997        let ctor = SSAConstructor::new(blocks);
998        let vars = ctor.all_vars();
999        assert!(vars.contains("x"));
1000        assert!(vars.contains("y"));
1001        assert!(vars.contains("z"));
1002    }
1003    #[test]
1004    fn test_ssa_constructor_rename() {
1005        let blocks = vec![BasicBlock::new(
1006            0,
1007            vec!["x".to_string(), "x".to_string()],
1008            vec![],
1009            vec![],
1010        )];
1011        let ctor = SSAConstructor::new(blocks);
1012        let renaming = ctor.rename_variables();
1013        assert_eq!(renaming.get(&(0, "x".to_string())), Some(&1));
1014    }
1015    #[test]
1016    fn test_ssa_constructor_phi_insertion() {
1017        let blocks = vec![
1018            BasicBlock::new(0, vec!["x".to_string()], vec![], vec![1, 2]),
1019            BasicBlock::new(1, vec![], vec!["x".to_string()], vec![3]),
1020            BasicBlock::new(2, vec![], vec!["x".to_string()], vec![3]),
1021            BasicBlock::new(3, vec![], vec!["x".to_string()], vec![]),
1022        ];
1023        let ctor = SSAConstructor::new(blocks);
1024        let phi_pts = ctor.phi_insertion_points();
1025        let _ = phi_pts;
1026    }
1027    #[test]
1028    fn test_ssa_constructor_dominance_frontier() {
1029        let blocks = vec![
1030            BasicBlock::new(0, vec![], vec![], vec![1]),
1031            BasicBlock::new(1, vec![], vec![], vec![2]),
1032            BasicBlock::new(2, vec![], vec![], vec![]),
1033        ];
1034        let ctor = SSAConstructor::new(blocks);
1035        let df = ctor.dominance_frontier_map();
1036        let _ = df;
1037    }
1038}
oxilean_std/compiler_theory/functions.rs

oxilean_std/compiler_theory/
functions.rs
