logicaffeine-compile 0.10.1

//! Verified SVA Compiler via Futamura Projections
//!
//! P1: Specialize SVA synthesis for a fixed spec → compiled generator
//! P2: Specialize the specializer for SVA synthesis → SVA compiler
//!
//! The key property: compiled output == interpreted output.
//! Compiler correctness is inherited from the projection framework.

use super::fol_to_sva::{synthesize_sva_from_spec, SynthesizedSva};
use super::sva_model::parse_sva;
use super::{SvaProperty, SvaAssertionKind, emit_sva_property};
use std::collections::hash_map::DefaultHasher;
use std::hash::{Hash, Hasher};

/// A compiled SVA generator — P1 output.
///
/// Captures the synthesis result for a fixed spec. Calling `generate(clock)`
/// reconstructs the SVA with the given clock, without re-parsing or re-synthesizing.
#[derive(Debug, Clone)]
pub struct CompiledGenerator {
    cached_body: String,
    cached_signals: Vec<String>,
    cached_kind: String,
    spec_hash: u64,
}

impl CompiledGenerator {
    /// Generate SVA for this fixed spec with the given clock.
    ///
    /// This is the "compiled" path — no spec parsing, no KG extraction,
    /// no synthesis. Pure string formatting from cached data.
    pub fn generate(&self, clock: &str) -> Result<SynthesizedSva, String> {
        let sva_text = format!(
            "property p_compiled;\n    @(posedge {}) {};\nendproperty\nassert property (p_compiled);",
            clock, self.cached_body
        );
        Ok(SynthesizedSva {
            sva_text,
            body: self.cached_body.clone(),
            signals: self.cached_signals.clone(),
            kind: self.cached_kind.clone(),
        })
    }

    /// Check if this generator was compiled from a specific spec.
    pub fn spec_hash(&self) -> u64 {
        self.spec_hash
    }

    /// Get the cached body (no synthesis overhead).
    pub fn body(&self) -> &str {
        &self.cached_body
    }

    /// Get the cached signals.
    pub fn signals(&self) -> &[String] {
        &self.cached_signals
    }
}

/// An SVA compiler — P2 output.
///
/// A factory that creates `CompiledGenerator` instances for any spec.
/// This is the "compiler compiled by the compiler" — the second Futamura projection.
pub struct SvaCompiler;

impl SvaCompiler {
    /// Compile a spec into a `CompiledGenerator`.
    ///
    /// This is P2 applied: the compiler takes a spec and produces a compiled generator.
    pub fn compile(&self, spec: &str) -> Result<CompiledGenerator, String> {
        compile_sva_generator(spec)
    }
}

/// P1: Specialize SVA synthesis for a fixed spec → compiled generator.
///
/// Calls `synthesize_sva_from_spec` once and caches the result.
/// The returned `CompiledGenerator` produces SVA without re-synthesis.
pub fn compile_sva_generator(spec: &str) -> Result<CompiledGenerator, String> {
    // Run the "interpreter" once
    let synthesized = synthesize_sva_from_spec(spec, "clk")?;

    // Cache the result
    let mut hasher = DefaultHasher::new();
    spec.hash(&mut hasher);
    let spec_hash = hasher.finish();

    Ok(CompiledGenerator {
        cached_body: synthesized.body,
        cached_signals: synthesized.signals,
        cached_kind: synthesized.kind,
        spec_hash,
    })
}

/// P2: Specialize the specializer for SVA synthesis → SVA compiler.
///
/// Returns a compiler that, for any spec, produces a compiled generator.
pub fn compile_sva_compiler() -> SvaCompiler {
    SvaCompiler
}

/// Verify compiler correctness: compiled output == interpreted output.
///
/// The fundamental Futamura property: for any spec and clock,
/// the compiled path produces the same SVA as the interpreted path.
pub fn verify_compiler_correctness(spec: &str, clock: &str) -> bool {
    let interpreted = match synthesize_sva_from_spec(spec, clock) {
        Ok(s) => s,
        Err(_) => return false,
    };

    let compiled = match compile_sva_generator(spec) {
        Ok(gen) => match gen.generate(clock) {
            Ok(s) => s,
            Err(_) => return false,
        },
        Err(_) => return false,
    };

    // The bodies must be identical
    let mut int_signals = interpreted.signals.clone();
    let mut comp_signals = compiled.signals.clone();
    int_signals.sort();
    comp_signals.sort();
    interpreted.body == compiled.body
        && int_signals == comp_signals
        && interpreted.kind == compiled.kind
}