Skip to main content

Crate oxilean_codegen

Crate oxilean_codegen 

Source
Expand description

§OxiLean Code Generation

Multi-target code generation backend for the OxiLean theorem prover.

This crate compiles type-checked OxiLean kernel expressions into executable code for a wide range of target platforms. Expressions are first lowered to a Lambda-Case Normal Form (LCNF) intermediate representation, then run through optimization passes, and finally emitted by a target-specific backend.

§Pipeline

  1. Kernel Expr is lowered via to_lcnf into the lcnf IR.
  2. Optimization passes in opt_passes orchestrate dead-code elimination (opt_dce), copy propagation and inlining (opt_copy_prop, opt_inline), join-point analysis (opt_join), reference-count reuse (opt_reuse), monomorphization (opt_specialize), common-subexpression elimination (opt_cse), loop-invariant code motion (opt_licm), vectorization (opt_vectorize), and many more.
  3. closure_convert flattens closures.
  4. A backend module emits the target-specific source or bytecode.

§Backends

Native and systems targets include native_backend (Rust), c_backend, llvm_backend, cranelift_backend, x86_64_backend, riscv_backend, mlir_backend, spirv_backend, wasm_backend, and wasm_component_backend. GPU and shader targets include cuda_backend, metal_backend, glsl_backend, and wgsl_backend. Functional and proof-assistant targets include agda_backend, coq_backend, lean4_backend, haskell_backend, idris_backend, ocaml_backend, fsharp_backend, and dhall_backend. Mainstream language targets include js_backend, typescript_backend, python_backend, java_backend, jvm_backend, kotlin_backend, scala_backend, csharp_backend, cil_backend, go_backend, swift_backend, dart_backend, ruby_backend, php_backend, lua_backend, elixir_backend, beam_backend, bash_backend, r_backend, julia_backend, matlab_backend, fortran_backend, zig_backend, nix_backend, prolog_backend, chapel_backend, futhark_backend, chisel_backend, verilog_backend, sql_backend, graphql_backend, and the smart-contract targets evm_backend, solidity_backend, and vyper_backend. C FFI headers are produced by ffi_bridge.

§Usage

See the README for a configuration example using CodegenConfig and CodegenTarget, and the pipeline module for the end-to-end driver. Code Generation Backend for Oxilean

This crate provides compilation from Oxilean kernel expressions

Re-exports§

pub use core_types::*;

Modules§

agda_backend
Auto-generated module structure
bash_backend
Auto-generated module structure
beam_backend
Auto-generated module structure
c_backend
Auto-generated module structure
chapel_backend
Auto-generated module structure
chisel_backend
Auto-generated module structure
cil_backend
Auto-generated module structure
closure_convert
Auto-generated module structure
coq_backend
Auto-generated module structure
core_types
Auto-generated module structure
cranelift_backend
Auto-generated module structure
csharp_backend
Auto-generated module structure
cuda_backend
Auto-generated module structure
dart_backend
Auto-generated module structure
dhall_backend
Auto-generated module structure
elixir_backend
Auto-generated module structure
evm_backend
Auto-generated module structure
ffi_bridge
Auto-generated module structure
fortran_backend
Auto-generated module structure
fsharp_backend
Auto-generated module structure
futhark_backend
Auto-generated module structure
glsl_backend
Auto-generated module structure
go_backend
Auto-generated module structure
graphql_backend
Auto-generated module structure
haskell_backend
Auto-generated module structure
idris_backend
Auto-generated module structure
ir_serialize
Serialization and deserialization of the LCNF intermediate representation.
java_backend
Auto-generated module structure
js_backend
Auto-generated module structure
julia_backend
Auto-generated module structure
jvm_backend
Auto-generated module structure
kotlin_backend
Auto-generated module structure
lcnf
Auto-generated module structure
lean4_backend
Auto-generated module structure
llvm_backend
Auto-generated module structure
llvm_ir_text
Auto-generated module structure
lua_backend
Auto-generated module structure
matlab_backend
Auto-generated module structure
metal_backend
Auto-generated module structure
mlir_backend
Auto-generated module structure
native_backend
Auto-generated module structure
nix_backend
Auto-generated module structure
ocaml_backend
Auto-generated module structure
opt_algebraic
Algebraic Simplification optimisation pass.
opt_alias
Auto-generated module structure
opt_beta_eta
Auto-generated module structure
opt_cache
Auto-generated module structure
opt_copy_prop
Auto-generated module structure
opt_cse
Auto-generated module structure
opt_ctfe
Auto-generated module structure
opt_dce
Auto-generated module structure
opt_dead_branch
Auto-generated module structure
opt_dse
Auto-generated module structure
opt_escape
Auto-generated module structure
opt_gvn
Auto-generated module structure
opt_inline
Auto-generated module structure
opt_join
Auto-generated module structure
opt_licm
Auto-generated module structure
opt_loop_unroll
Auto-generated module structure
opt_mem2reg
Auto-generated module structure
opt_parallel
Auto-generated module structure
opt_partial_eval
Auto-generated module structure
opt_passes
Auto-generated module structure
opt_peephole
Peephole optimisation pass for the Oxilean code generation pipeline.
opt_regalloc
Auto-generated module structure
opt_reuse
Auto-generated module structure
opt_specialize
Auto-generated module structure
opt_specialize_types
Auto-generated module structure
opt_strength
Auto-generated module structure
opt_tail_recursion
Auto-generated module structure
opt_vectorize
Auto-generated module structure
pgo
Auto-generated module structure
php_backend
Auto-generated module structure
pipeline
Auto-generated module structure
prolog_backend
Auto-generated module structure
python_backend
Auto-generated module structure
r_backend
Auto-generated module structure
riscv_backend
Auto-generated module structure
ruby_backend
Auto-generated module structure
runtime_codegen
Auto-generated module structure
rust_target_backend
Auto-generated module structure
scala_backend
Auto-generated module structure
solidity_backend
Auto-generated module structure
spirv_backend
Auto-generated module structure
sql_backend
Auto-generated module structure
swift_backend
Auto-generated module structure
to_lcnf
Auto-generated module structure
typescript_backend
Auto-generated module structure
verilog_backend
Auto-generated module structure
vyper_backend
Auto-generated module structure
wasm_backend
Auto-generated module structure
wasm_component_backend
Auto-generated module structure
wgsl_backend
Auto-generated module structure
x86_64_backend
Auto-generated module structure
zig_backend
Auto-generated module structure