oxilean_codegen/
lib.rs

1//! # OxiLean Code Generation
2//!
3//! Multi-target code generation backend for the OxiLean theorem prover.
4//!
5//! This crate compiles type-checked OxiLean kernel expressions into executable
6//! code for a wide range of target platforms. Expressions are first lowered to
7//! a Lambda-Case Normal Form (LCNF) intermediate representation, then run
8//! through optimization passes, and finally emitted by a target-specific
9//! backend.
10//!
11//! ## Pipeline
12//!
13//! 1. Kernel `Expr` is lowered via [`to_lcnf`] into the [`lcnf`] IR.
14//! 2. Optimization passes in [`opt_passes`] orchestrate dead-code elimination
15//!    ([`opt_dce`]), copy propagation and inlining ([`opt_copy_prop`],
16//!    [`opt_inline`]), join-point analysis ([`opt_join`]), reference-count
17//!    reuse ([`opt_reuse`]), monomorphization ([`opt_specialize`]),
18//!    common-subexpression elimination ([`opt_cse`]), loop-invariant code
19//!    motion ([`opt_licm`]), vectorization ([`opt_vectorize`]), and many more.
20//! 3. [`closure_convert`] flattens closures.
21//! 4. A backend module emits the target-specific source or bytecode.
22//!
23//! ## Backends
24//!
25//! Native and systems targets include [`native_backend`] (Rust), [`c_backend`],
26//! [`llvm_backend`], [`cranelift_backend`], [`x86_64_backend`], [`riscv_backend`],
27//! [`mlir_backend`], [`spirv_backend`], [`wasm_backend`], and
28//! [`wasm_component_backend`]. GPU and shader targets include [`cuda_backend`],
29//! [`metal_backend`], [`glsl_backend`], and [`wgsl_backend`]. Functional and
30//! proof-assistant targets include [`agda_backend`], [`coq_backend`],
31//! [`lean4_backend`], [`haskell_backend`], [`idris_backend`], [`ocaml_backend`],
32//! [`fsharp_backend`], and [`dhall_backend`]. Mainstream language targets
33//! include [`js_backend`], [`typescript_backend`], [`python_backend`],
34//! [`java_backend`], [`jvm_backend`], [`kotlin_backend`], [`scala_backend`],
35//! [`csharp_backend`], [`cil_backend`], [`go_backend`], [`swift_backend`],
36//! [`dart_backend`], [`ruby_backend`], [`php_backend`], [`lua_backend`],
37//! [`elixir_backend`], [`beam_backend`], [`bash_backend`], [`r_backend`],
38//! [`julia_backend`], [`matlab_backend`], [`fortran_backend`], [`zig_backend`],
39//! [`nix_backend`], [`prolog_backend`], [`chapel_backend`], [`futhark_backend`],
40//! [`chisel_backend`], [`verilog_backend`], [`sql_backend`],
41//! [`graphql_backend`], and the smart-contract targets [`evm_backend`],
42//! [`solidity_backend`], and [`vyper_backend`]. C FFI headers are produced by
43//! [`ffi_bridge`].
44//!
45//! ## Usage
46//!
47//! See the README for a configuration example using `CodegenConfig` and
48//! `CodegenTarget`, and the [`pipeline`] module for the end-to-end driver.
49
50#![allow(dead_code)]
51#![allow(unused_imports)]
52#![allow(unused_mut)]
53#![allow(clippy::new_without_default)]
54#![allow(non_snake_case)]
55#![allow(clippy::collapsible_if)]
56#![allow(clippy::collapsible_match)]
57#![allow(clippy::approx_constant)]
58#![allow(clippy::should_implement_trait)]
59#![allow(clippy::single_match)]
60#![allow(clippy::field_reassign_with_default)]
61#![allow(clippy::len_without_is_empty)]
62#![allow(clippy::useless_format)]
63#![allow(clippy::type_complexity)]
64#![allow(clippy::items_after_test_module)]
65#![allow(clippy::too_many_arguments)]
66#![allow(clippy::result_large_err)]
67#![allow(clippy::vec_init_then_push)]
68#![allow(clippy::comparison_chain)]
69#![allow(clippy::write_with_newline)]
70#![allow(clippy::absurd_extreme_comparisons)]
71#![allow(clippy::unnecessary_map_or)]
72#![allow(clippy::derivable_impls)]
73#![allow(clippy::if_same_then_else)]
74#![allow(clippy::only_used_in_recursion)]
75#![allow(clippy::module_inception)]
76#![allow(clippy::needless_range_loop)]
77#![allow(clippy::manual_map)]
78#![allow(clippy::ptr_arg)]
79#![allow(clippy::while_let_loop)]
80#![allow(clippy::unnecessary_map_on_constructor)]
81#![allow(clippy::iter_kv_map)]
82#![allow(clippy::collapsible_str_replace)]
83#![allow(clippy::default_constructed_unit_structs)]
84#![allow(clippy::needless_lifetimes)]
85#![allow(clippy::needless_borrow)]
86#![allow(clippy::redundant_closure)]
87#![allow(clippy::len_zero)]
88#![allow(clippy::get_first)]
89#![allow(clippy::manual_find)]
90#![allow(clippy::float_cmp)]
91#![allow(clippy::excessive_precision)]
92#![allow(clippy::inconsistent_digit_grouping)]
93#![allow(clippy::needless_ifs)]
94#![allow(clippy::needless_borrows_for_generic_args)]
95#![allow(clippy::doc_lazy_continuation)]
96#![allow(clippy::unnecessary_unwrap)]
97#![allow(clippy::for_kv_map)]
98#![allow(unused_comparisons)]
99#![allow(private_interfaces)]
100#![allow(clippy::incompatible_msrv)]
101
102//! Code Generation Backend for Oxilean
103//!
104//! This crate provides compilation from Oxilean kernel expressions
105// to various target languages: Rust, C, LLVM IR, and interpretation.
106//
107// The pipeline consists of:
108// 1. Expression to Intermediate Representation (ExprToIr)
109// 2. IR optimization (Optimizer)
110// 3. Backend-specific code emission (IrToRust, IrToC)
111
112pub mod agda_backend;
113pub mod bash_backend;
114pub mod beam_backend;
115pub mod c_backend;
116pub mod chapel_backend;
117pub mod chisel_backend;
118pub mod cil_backend;
119pub mod closure_convert;
120pub mod coq_backend;
121pub mod cranelift_backend;
122pub mod csharp_backend;
123pub mod cuda_backend;
124pub mod dart_backend;
125pub mod dhall_backend;
126pub mod elixir_backend;
127pub mod evm_backend;
128pub mod ffi_bridge;
129pub mod fortran_backend;
130pub mod fsharp_backend;
131pub mod futhark_backend;
132pub mod glsl_backend;
133pub mod go_backend;
134pub mod graphql_backend;
135pub mod haskell_backend;
136pub mod idris_backend;
137pub mod ir_serialize;
138pub mod java_backend;
139pub mod js_backend;
140pub mod julia_backend;
141pub mod jvm_backend;
142pub mod kotlin_backend;
143pub mod lcnf;
144pub mod lean4_backend;
145pub mod llvm_backend;
146pub mod llvm_ir_text;
147pub mod lua_backend;
148pub mod matlab_backend;
149pub mod metal_backend;
150pub mod mlir_backend;
151pub mod native_backend;
152pub mod nix_backend;
153pub mod ocaml_backend;
154pub mod opt_algebraic;
155pub mod opt_alias;
156pub mod opt_beta_eta;
157pub mod opt_cache;
158pub mod opt_copy_prop;
159pub mod opt_cse;
160pub mod opt_ctfe;
161pub mod opt_dce;
162pub mod opt_dead_branch;
163pub mod opt_dse;
164pub mod opt_escape;
165pub mod opt_gvn;
166pub mod opt_inline;
167pub mod opt_join;
168pub mod opt_licm;
169pub mod opt_loop_unroll;
170pub mod opt_mem2reg;
171pub mod opt_parallel;
172pub mod opt_partial_eval;
173pub mod opt_passes;
174pub mod opt_peephole;
175pub mod opt_regalloc;
176pub mod opt_reuse;
177pub mod opt_specialize;
178pub mod opt_specialize_types;
179pub mod opt_strength;
180pub mod opt_tail_recursion;
181pub mod opt_vectorize;
182pub mod pgo;
183pub mod php_backend;
184pub mod pipeline;
185pub mod prolog_backend;
186pub mod python_backend;
187pub mod r_backend;
188pub mod riscv_backend;
189pub mod ruby_backend;
190pub mod runtime_codegen;
191pub mod rust_target_backend;
192pub mod scala_backend;
193pub mod solidity_backend;
194pub mod spirv_backend;
195pub mod sql_backend;
196pub mod swift_backend;
197pub mod to_lcnf;
198pub mod typescript_backend;
199pub mod verilog_backend;
200pub mod vyper_backend;
201pub mod wasm_backend;
202pub mod wasm_component_backend;
203pub mod wgsl_backend;
204pub mod x86_64_backend;
205pub mod zig_backend;
206
207pub mod core_types;
208pub use core_types::*;
oxilean_codegen/lib.rs

oxilean_codegen/
lib.rs
