logicaffeine_compile/extraction/
mod.rs

1//! Program extraction from kernel terms to Rust.
2//!
3//! This module compiles verified kernel terms into executable Rust source code.
4//!
5//! # Extraction Rules
6//!
7//! | Kernel Term | Rust Output |
8//! |-------------|-------------|
9//! | Inductive | `enum Name { Ctor(Args...) }` |
10//! | Fix + Lambdas | `fn name(args) -> Ret { body }` |
11//! | Match | `match disc { Name::Ctor(vars) => body }` |
12//! | App | `func(arg)` |
13//!
14//! # Structural Honesty
15//!
16//! We extract types exactly as defined, with no optimization.
17//! For example, `Nat` becomes `enum Nat { Zero, Succ(Box<Nat>) }`.
18//! This guarantees that the extracted code is isomorphic to the verified logic.
19
20mod codegen;
21mod collector;
22mod error;
23pub mod fol_model;
24pub mod verilog;
25
26pub use codegen::{emit_property_check, emit_value, primitive_rust_type};
27pub use collector::{is_extractable, is_logical_type};
28pub use error::ExtractError;
29
30use logicaffeine_kernel::Context;
31use codegen::CodeGen;
32use collector::collect_dependencies;
33use std::collections::HashSet;
34
35/// Extract a program rooted at the given entry point.
36///
37/// Returns Rust source code as a string.
38///
39/// # Arguments
40///
41/// * `ctx` - The kernel context containing definitions and inductives
42/// * `entry` - The name of the entry point to extract
43///
44/// # Errors
45///
46/// Returns an error if the entry point is not found or cannot be extracted.
47pub fn extract_program(ctx: &Context, entry: &str) -> Result<String, ExtractError> {
48    extract_programs(ctx, &[entry])
49}
50
51/// Extract a program rooted at several entry points into one Rust module.
52///
53/// Returns Rust source code as a string. The transitive dependencies of every
54/// entry are unioned, topologically sorted once, and emitted through a single
55/// [`CodeGen`], so shared dependencies (e.g. a `Nat` enum used by both `add` and
56/// `double`) are emitted exactly once.
57///
58/// # Arguments
59///
60/// * `ctx` - The kernel context containing definitions and inductives
61/// * `entries` - The names of the entry points to extract
62///
63/// # Errors
64///
65/// Returns an error if any entry point is not found or cannot be extracted.
66pub fn extract_programs(ctx: &Context, entries: &[&str]) -> Result<String, ExtractError> {
67    // 1. Collect the union of all dependencies, validating each entry exists.
68    let mut all_deps: HashSet<String> = HashSet::new();
69    for entry in entries {
70        if !ctx.is_inductive(entry) && !ctx.is_definition(entry) && !ctx.is_constructor(entry) {
71            return Err(ExtractError::NotFound((*entry).to_string()));
72        }
73        all_deps.extend(collect_dependencies(ctx, entry));
74    }
75
76    // 2. Topologically sort (inductives first, then definitions)
77    let sorted = topological_sort(ctx, &all_deps);
78
79    // 3. Generate code through a single CodeGen so shared deps dedup.
80    let mut codegen = CodeGen::new(ctx);
81    for name in &sorted {
82        if ctx.is_inductive(name) {
83            // Opaque/primitive inductives (Int, Float, Text, Bool, Duration, …)
84            // are declared with NO constructors; they have no enum form and are
85            // mapped to Rust types at use sites, so skip them rather than
86            // erroring with `NotFound`.
87            if !ctx.get_constructors(name).is_empty() {
88                codegen.emit_inductive(name)?;
89            }
90        } else if ctx.is_definition(name) {
91            codegen.emit_definition(name)?;
92        }
93        // Skip constructors (emitted with their inductive)
94    }
95
96    Ok(codegen.finish())
97}
98
99/// Topologically sort dependencies.
100///
101/// Inductives come first, then definitions in dependency order.
102fn topological_sort(ctx: &Context, deps: &HashSet<String>) -> Vec<String> {
103    let mut inductives = Vec::new();
104    let mut definitions = Vec::new();
105
106    for name in deps {
107        if ctx.is_inductive(name) {
108            inductives.push(name.clone());
109        } else if ctx.is_definition(name) {
110            definitions.push(name.clone());
111        }
112        // Skip constructors - they're emitted with their inductive
113    }
114
115    // Inductives first, then definitions — and each group sorted by name so the
116    // emitted module is DETERMINISTIC regardless of HashSet/HashMap iteration
117    // order (every Compile builds a fresh kernel with new hash seeds). Rust
118    // resolves top-level items order-independently, so sorting is sound.
119    inductives.sort();
120    definitions.sort();
121    inductives.extend(definitions);
122    inductives
123}
logicaffeine_compile/extraction/mod.rs

logicaffeine_compile/extraction/
mod.rs
