aprender_contracts_cli/commands/
codegen.rs

1//! `pv codegen` — generate Rust `debug_assert`!() from YAML contracts.
2
3use provable_contracts::codegen;
4use std::path::Path;
5
6pub fn run(contract_dir: &Path, output: Option<&Path>) -> Result<(), Box<dyn std::error::Error>> {
7    let contracts = codegen::generate_all(contract_dir);
8
9    if contracts.is_empty() {
10        println!("No contracts with preconditions/postconditions/invariants found.");
11        return Ok(());
12    }
13
14    let mut total_pre = 0;
15    let mut total_post = 0;
16    let mut total_inv = 0;
17    let mut total_lean = 0;
18
19    for c in &contracts {
20        total_pre += c.precondition_count;
21        total_post += c.postcondition_count;
22        total_inv += c.invariant_count;
23        total_lean += c.lean_theorem_count;
24    }
25
26    println!("pv codegen — contract → Rust assertions");
27    println!("========================================\n");
28    println!("Contracts:      {}", contracts.len());
29    println!("Preconditions:  {total_pre}");
30    println!("Postconditions: {total_post}");
31    println!("Invariants:     {total_inv}");
32    println!("Lean theorems:  {total_lean}");
33
34    let out_path = output.unwrap_or(Path::new("src/generated_contracts.rs"));
35
36    // Create parent directory if it doesn't exist
37    if let Some(parent) = out_path.parent() {
38        if !parent.as_os_str().is_empty() {
39            std::fs::create_dir_all(parent)?;
40        }
41    }
42
43    codegen::write_rust_module(&contracts, out_path)?;
44    println!("\nGenerated: {}", out_path.display());
45
46    Ok(())
47}
aprender_contracts_cli/commands/codegen.rs

aprender_contracts_cli/commands/
codegen.rs
