//! SVA property assertion emission, module structure helpers,
//! and input synchronizer chain generation.

#![forbid(unsafe_code)]

use crate::ast::program::Module;
use crate::ast::property::{PropertyDecl, PropertyDirective, PropertyFormula};
use crate::ast::types::SignalKind;
use crate::emit::fpga_target::MAX_SYNC_STAGES;
use crate::pipeline::PipelineResult;

// -----------------------------------------------------------------------
// Module structure helpers
// -----------------------------------------------------------------------

pub(super) fn emit_header(out: &mut String) {
    out.push_str("// Auto-generated by MIRR compiler (Phase 6)\n");
    out.push_str("// Do not edit — regenerate from .mirr source.\n");
    out.push_str("// Target: SystemVerilog (.sv)\n\n");
}

/// Emit pattern expansion annotations as SV comments.
pub(super) fn emit_pattern_annotations(module: &Module, out: &mut String) {
    if module.pattern_origins.is_empty() {
        return;
    }
    out.push_str("// ── Pattern Expansions ──\n");
    for origin in &module.pattern_origins {
        out.push_str(&format!(
            "// Pattern: {}({})\n",
            origin.pattern_name, origin.call_args_summary
        ));
    }
    out.push('\n');
}

pub(super) fn emit_module_decl(module: &Module, out: &mut String) {
    out.push_str(&format!("module {} (\n", module.name));

    let has_clk = module.signals.iter().any(|s| s.name == "clk");
    let has_rst_n = module.signals.iter().any(|s| s.name == "rst_n");
    let needs_temporal = !module.guards.is_empty();

    let mut ports: Vec<String> = Vec::new();

    // Auto-inject clk and rst_n when temporal guards exist.
    if needs_temporal && !has_clk {
        ports.push("  input  logic        clk".to_string());
    }
    if needs_temporal && !has_rst_n {
        ports.push("  input  logic        rst_n".to_string());
    }

    for s in &module.signals {
        if s.kind == SignalKind::Input || s.kind == SignalKind::Output {
            let dir = match s.kind {
                SignalKind::Input => "input ",
                SignalKind::Output => "output",
                SignalKind::Internal => "internal",
            };
            let type_str = super::super::sv_type(&s.ty.signal_type());
            ports.push(format!("  {dir} {type_str} {}", s.name));
        }
    }

    let port_count = ports.len();
    for (i, port) in ports.iter().enumerate() {
        let comma = if i + 1 < port_count { "," } else { "" };
        out.push_str(&format!("{port}{comma}\n"));
    }

    out.push_str(");\n\n");
}

pub(super) fn emit_internal_signals(module: &Module, out: &mut String) {
    let internals: Vec<_> =
        module.signals.iter().filter(|s| s.kind == SignalKind::Internal).collect();

    if !internals.is_empty() {
        out.push_str("  // Internal signals\n");
        for s in &internals {
            if let Some(ref origin) = s.origin {
                out.push_str(&format!("  // Pattern: {origin}\n"));
            }
            let type_str = super::super::sv_type(&s.ty.signal_type());
            out.push_str(&format!("  {type_str} {};\n", s.name));
        }
        out.push('\n');
    }
}

pub(super) fn emit_module_end(out: &mut String) {
    out.push_str("endmodule\n");
}

// -----------------------------------------------------------------------
// Safety Property Assertions (SVA)
// -----------------------------------------------------------------------

/// Check if the module declares an input signal named `rst_n`.
pub(super) fn module_has_rst_n(module: &Module) -> bool {
    module.signals.iter().any(|s| s.name == "rst_n" && s.kind == SignalKind::Input)
}

/// Emit SVA assertion blocks for all property declarations.
pub(super) fn emit_property_assertions(module: &Module, has_rst_n: bool, out: &mut String) {
    if module.properties.is_empty() {
        return;
    }

    out.push_str("  // ── Safety Properties (SVA) ──\n\n");

    for prop in &module.properties {
        emit_single_property(prop, has_rst_n, out);
    }
}

/// Emit a single SVA `assert property` statement.
pub(super) fn emit_single_property(prop: &PropertyDecl, has_rst_n: bool, out: &mut String) {
    if let Some(ref origin) = prop.origin {
        out.push_str(&format!("  // Pattern: {origin}\n"));
    }
    out.push_str(&format!("  // property: {}\n", prop.name));

    let sva_keyword = match prop.directive {
        PropertyDirective::Assert => "assert",
        PropertyDirective::Cover => "cover",
        PropertyDirective::Assume => "assume",
    };

    let disable_clause = if has_rst_n { " disable iff (!rst_n)" } else { "" };

    match &prop.formula {
        PropertyFormula::Always(expr) => {
            let sv_expr = super::emit_expr_inline(expr);
            out.push_str(&format!(
                "  {sva_keyword} property (@(posedge clk){disable_clause}\n    {sv_expr});\n\n"
            ));
        }
        PropertyFormula::Never(expr) => {
            let sv_expr = super::emit_expr_inline(expr);
            out.push_str(&format!(
                "  {sva_keyword} property (@(posedge clk){disable_clause}\n    !({sv_expr}));\n\n"
            ));
        }
        PropertyFormula::AlwaysImplies { antecedent, consequent } => {
            let ante_sv = super::emit_expr_inline(antecedent);
            let cons_sv = super::emit_expr_inline(consequent);
            out.push_str(&format!(
                "  {sva_keyword} property (@(posedge clk){disable_clause}\n    {ante_sv} |-> {cons_sv});\n\n"
            ));
        }
        PropertyFormula::NeverImplies { antecedent, consequent } => {
            let ante_sv = super::emit_expr_inline(antecedent);
            let cons_sv = super::emit_expr_inline(consequent);
            out.push_str(&format!(
                "  {sva_keyword} property (@(posedge clk){disable_clause}\n    !({ante_sv} |-> {cons_sv}));\n\n"
            ));
        }
        PropertyFormula::EventuallyWithin { expr, cycles } => {
            let sv_expr = super::emit_expr_inline(expr);
            out.push_str(&format!(
                "  {sva_keyword} property (@(posedge clk){disable_clause}\n    ##[1:{cycles}] {sv_expr});\n\n"
            ));
        }
        PropertyFormula::AlwaysFollowedBy { trigger, response, delay_cycles } => {
            let trig_sv = super::emit_expr_inline(trigger);
            let resp_sv = super::emit_expr_inline(response);
            out.push_str(&format!(
                "  {sva_keyword} property (@(posedge clk){disable_clause}\n    {trig_sv} |-> ##{delay_cycles} {resp_sv});\n\n"
            ));
        }
    }
}

// -----------------------------------------------------------------------
// Input Synchronizer Chains
// -----------------------------------------------------------------------

/// Emit 2-stage (or N-stage) synchronizer chains for all input signals
/// except `clk` and `rst_n`. Returns a mapping of original signal names
/// to their synchronized versions (_s suffix).
pub fn emit_synchronizer_chains(
    module: &Module,
    sync_stages: u32,
    out: &mut String,
) -> Vec<(String, String)> {
    if sync_stages == 0 {
        return Vec::new();
    }
    let stages = sync_stages.min(MAX_SYNC_STAGES);

    let mut mappings = Vec::new();
    out.push_str("  // ── Input Synchronizer Chains ──\n\n");

    for s in &module.signals {
        if s.kind != SignalKind::Input {
            continue;
        }
        if s.name == "clk" || s.name == "rst_n" {
            continue;
        }

        let width = s.ty.signal_type().width();
        let sync_name = format!("{}_s", s.name);
        let sync_reg = format!("{}_sync", s.name);

        // Declare synchronizer register chain.
        let total_bits = width * stages;
        out.push_str(&format!("  // {}-stage synchronizer for {}\n", stages, s.name));
        out.push_str(&format!("  logic [{}:0] {};\n", total_bits.saturating_sub(1), sync_reg,));

        // Sequential synchronizer logic.
        out.push_str("  always_ff @(posedge clk or negedge rst_n) begin\n");
        out.push_str(&format!("    if (!rst_n)\n      {} <= '0;\n", sync_reg));
        if stages == 1 {
            out.push_str(&format!("    else\n      {} <= {};\n", sync_reg, s.name));
        } else {
            // Shift chain: {input, sync[high:width]}
            out.push_str(&format!(
                "    else\n      {} <= {{{}, {}[{}:{}]}};\n",
                sync_reg,
                s.name,
                sync_reg,
                total_bits.saturating_sub(1),
                width,
            ));
        }
        out.push_str("  end\n");

        // Output: synchronized signal is the last stage.
        let type_str = super::super::sv_type(&s.ty.signal_type());
        out.push_str(&format!(
            "  {} {} = {}[{}:0];\n\n",
            type_str,
            sync_name,
            sync_reg,
            width.saturating_sub(1),
        ));

        mappings.push((s.name.clone(), sync_name));
    }

    mappings
}

/// Emit only the SVA assertion block (no module wrapper).
///
/// Used by `--emit sva` standalone mode.
pub fn emit_sva_only(result: &PipelineResult) -> String {
    let module = &result.program.module;
    let mut out = String::with_capacity(1024);

    out.push_str("// Auto-generated SVA assertions from MIRR compiler\n");
    out.push_str(&format!("// Module: {}\n\n", module.name));

    let has_rst_n = module_has_rst_n(module);

    for prop in &module.properties {
        emit_single_property(prop, has_rst_n, &mut out);
    }

    out
}
