lolli-codegen

Code generation for the Lolli linear logic workbench.

This crate generates Rust code from linear logic proofs, translating formulas to types and terms to code.

Linear Logic to Rust Mapping

Example

use lolli_codegen::RustCodegen;
use lolli_core::{Formula, Term};

let codegen = RustCodegen::new();

// Formula to type
let lolli = Formula::lolli(Formula::atom("A"), Formula::atom("B"));
assert_eq!(codegen.formula_to_type(&lolli), "impl FnOnce(A) -> B");

// Term to code
let mut codegen = RustCodegen::new();
let id = Term::Abs("x".to_string(), Box::new(Term::Var("x".to_string())));
assert_eq!(codegen.term_to_code(&id), "|x| x");

lolli-codegen

Code generation for the Lolli linear logic workbench.

Generates Rust code from linear logic proofs, enforcing resource invariants at compile time.

Type Mapping

Usage

use lolli_codegen::RustCodegen;

let mut codegen = RustCodegen::new();
let rust_code = codegen.generate_module(&proofs);

Part of Lolli

This is part of the Lolli linear logic workbench.

License

MIT