//! FIRRTL emitter for MIRR IR.
//!
//! Produces FIRRTL (Flexible Intermediate Representation for RTL) output
//! from the compiled pipeline result. FIRRTL is the intermediate language
//! used by the CHIPS Alliance / CIRCT ecosystem.
//!
//! Mapping notes:
//! - Signals → FIRRTL `input`/`output`/`wire` declarations
//! - Guards → shift-register or counter hardware (from temporal netlist)
//! - Reflexes → conditional `connect` statements under `when` blocks
//! - Properties → FIRRTL `assert` intrinsics (limited; SVA has no FIRRTL
//!   equivalent, so properties emit as verification comments)
//!
//! Width mapping: `bool` → `UInt<1>`, `uN` → `UInt<N>`.

#![forbid(unsafe_code)]

use crate::ast::expr::Expr;
use crate::ast::program::Module;
use crate::ast::types::{BinaryOp, LiteralValue, SignalKind, SignalType, UnaryOp};
use crate::ast::MAX_EXPR_NODES;
use crate::pipeline::PipelineResult;
use crate::temporal::low_level_ir::{CompiledGuard, TemporalNetlist};

/// Emit FIRRTL from pipeline results.
pub fn emit_firrtl(result: &PipelineResult) -> String {
    let module = &result.program.module;
    let mut out = String::with_capacity(4096);

    emit_header(&mut out);
    out.push_str("circuit ");
    out.push_str(&module.name);
    out.push_str(" :\n");

    emit_module(module, result.temporal_netlist.as_ref(), &mut out);

    out
}

// -----------------------------------------------------------------------
// Internal helpers
// -----------------------------------------------------------------------

fn emit_header(out: &mut String) {
    out.push_str("; Auto-generated by MIRR compiler\n");
    out.push_str("; Do not edit — regenerate from .mirr source.\n");
    out.push_str("; Target: FIRRTL\n");
    out.push_str("FIRRTL version 1.1.0\n");
}

fn emit_module(module: &Module, temporal_netlist: Option<&TemporalNetlist>, out: &mut String) {
    out.push_str("  module ");
    out.push_str(&module.name);
    out.push_str(" :\n");

    // Clock and reset (implicit in MIRR, explicit in FIRRTL).
    out.push_str("    input clk : Clock\n");
    out.push_str("    input rst_n : UInt<1>\n");

    emit_ports(module, out);
    emit_internal_wires(module, out);
    out.push('\n');

    if let Some(netlist) = temporal_netlist {
        emit_temporal_logic(netlist, out);
    }

    emit_reflex_logic(module, out);
    emit_property_comments(module, out);
}

fn emit_ports(module: &Module, out: &mut String) {
    for s in &module.signals {
        let dir = match s.kind {
            SignalKind::Input => "input",
            SignalKind::Output => "output",
            SignalKind::Internal => continue, // handled as wires
        };
        let ty = firrtl_type(&s.ty.signal_type());
        out.push_str(&format!("    {} {} : {}\n", dir, s.name, ty));
    }
}

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

    if internals.is_empty() {
        return;
    }

    out.push_str("\n    ; Internal signals\n");
    for s in &internals {
        let ty = firrtl_type(&s.ty.signal_type());
        out.push_str(&format!("    wire {} : {}\n", s.name, ty));
    }
}

fn emit_temporal_logic(netlist: &TemporalNetlist, out: &mut String) {
    out.push_str("\n    ; ── Temporal Guards ──\n");

    for guard in &netlist.guards {
        match guard {
            CompiledGuard::ShiftRegister(sr) => {
                emit_shift_register_firrtl(sr, out);
            }
            CompiledGuard::Counter(cg) => {
                emit_counter_firrtl(cg, out);
            }
            CompiledGuard::Complex(cx) => {
                out.push_str(&format!(
                    "\n    ; Complex guard: {} (sub-guards combined)\n",
                    cx.name
                ));
                let ty = "UInt<1>";
                out.push_str(&format!("    wire {} : {}\n", cx.output_signal, ty));
                let expr = emit_expr_firrtl(&cx.combination_logic);
                out.push_str(&format!("    connect {} , {}\n", cx.output_signal, expr));
            }
            CompiledGuard::DynamicCounter(dc) => {
                out.push_str(&format!(
                    "\n    ; Dynamic counter guard: {} (max {} cycles)\n",
                    dc.name, dc.max_delay
                ));
                let width = dc.counter_width();
                out.push_str(&format!("    reg {} : UInt<{}>, clock\n", dc.counter_signal, width));
                out.push_str(&format!("    wire {} : UInt<1>\n", dc.output_signal));
            }
        }
    }
}

fn emit_shift_register_firrtl(
    sr: &crate::temporal::low_level_ir::ShiftRegisterGuard,
    out: &mut String,
) {
    let stage_count = sr.delay_cycles.min(super::verilog::MAX_SR_STAGES_INLINE);
    let cond = emit_condition_firrtl(&sr.condition_kind);

    out.push_str(&format!(
        "\n    ; Guard: {} — {} for {} cycles\n",
        sr.name,
        sr.condition_kind.describe(),
        sr.delay_cycles,
    ));

    // Shift register as a vector of 1-bit registers.
    out.push_str(&format!(
        "    reg {}_sr : UInt<{}> , clk with : (reset => (not(rst_n), UInt(0)))\n",
        sr.name, stage_count,
    ));

    // Condition wire.
    out.push_str(&format!("    wire {}_cond : UInt<1>\n", sr.name));
    out.push_str(&format!("    connect {}_cond , {}\n", sr.name, cond));

    // Shift operation: sr <= cat(cond, sr[high:1]).
    out.push_str(&format!("    connect {0}_sr , cat({0}_cond, shr({0}_sr, 1))\n", sr.name,));

    // Output: guard fires when all bits are 1.
    out.push_str(&format!("    wire {} : UInt<1>\n", sr.output_signal));
    out.push_str(&format!("    connect {} , andr({}_sr)\n", sr.output_signal, sr.name,));
}

fn emit_counter_firrtl(cg: &crate::temporal::low_level_ir::CounterGuard, out: &mut String) {
    let width = cg.counter_width();
    let cond = emit_condition_firrtl(&cg.condition_kind);

    out.push_str(&format!(
        "\n    ; Guard: {} — {} for {} cycles (counter)\n",
        cg.name,
        cg.condition_kind.describe(),
        cg.target_count,
    ));

    // Counter register.
    out.push_str(&format!(
        "    reg {} : UInt<{}> , clk with : (reset => (not(rst_n), UInt(0)))\n",
        cg.counter_signal, width,
    ));

    // Condition wire.
    out.push_str(&format!("    wire {}_cond : UInt<1>\n", cg.name));
    out.push_str(&format!("    connect {}_cond , {}\n", cg.name, cond));

    // Counter logic.
    out.push_str(&format!(
        "    when not({0}_cond) :\n      connect {1} , UInt(0)\n",
        cg.name, cg.counter_signal,
    ));
    out.push_str(&format!(
        "    else when lt({0}, UInt({1})) :\n      connect {0} , add({0}, UInt(1))\n",
        cg.counter_signal, cg.target_count,
    ));

    // Output: guard fires when counter >= target.
    out.push_str(&format!("    wire {} : UInt<1>\n", cg.output_signal));
    out.push_str(&format!(
        "    connect {} , geq({}, UInt({}))\n",
        cg.output_signal, cg.counter_signal, cg.target_count,
    ));
}

fn emit_reflex_logic(module: &Module, out: &mut String) {
    if module.reflexes.is_empty() {
        return;
    }

    out.push_str("\n    ; ── Reflex Assignments ──\n");

    for r in &module.reflexes {
        out.push_str(&format!("\n    ; Reflex: {}\n", r.name));

        let guard_cond = if r.guard_names.len() == 1 {
            format!("{}_out", r.guard_names[0])
        } else {
            let mut expr = format!("{}_out", r.guard_names[0]);
            let mut i = 1;
            while i < r.guard_names.len() {
                expr = format!("and({}, {}_out)", expr, r.guard_names[i]);
                i += 1;
            }
            expr
        };

        for a in &r.assignments {
            let val = emit_expr_firrtl(&a.value);
            out.push_str(&format!(
                "    when {} :\n      connect {} , {}\n    else :\n      connect {} , UInt(0)\n",
                guard_cond, a.target, val, a.target,
            ));
        }
    }
}

fn emit_property_comments(module: &Module, out: &mut String) {
    if module.properties.is_empty() {
        return;
    }

    out.push_str(
        "\n    ; ── Safety Properties (verification only — no FIRRTL equivalent to SVA) ──\n",
    );

    for prop in &module.properties {
        let desc = match &prop.formula {
            crate::ast::property::PropertyFormula::Always(expr) => {
                format!("always ({})", expr_text(expr))
            }
            crate::ast::property::PropertyFormula::Never(expr) => {
                format!("never ({})", expr_text(expr))
            }
            crate::ast::property::PropertyFormula::AlwaysImplies { antecedent, consequent } => {
                format!("always ({} -> {})", expr_text(antecedent), expr_text(consequent),)
            }
            crate::ast::property::PropertyFormula::NeverImplies { antecedent, consequent } => {
                format!("never ({} -> {})", expr_text(antecedent), expr_text(consequent),)
            }
            crate::ast::property::PropertyFormula::EventuallyWithin { expr, cycles } => {
                format!("eventually within {} ({})", cycles, expr_text(expr))
            }
            crate::ast::property::PropertyFormula::AlwaysFollowedBy {
                trigger,
                response,
                delay_cycles,
            } => {
                format!(
                    "always ({} followed_by {} {})",
                    expr_text(trigger),
                    delay_cycles,
                    expr_text(response),
                )
            }
        };

        let directive_prefix = match prop.directive {
            crate::ast::property::PropertyDirective::Assert => "",
            crate::ast::property::PropertyDirective::Cover => "cover ",
            crate::ast::property::PropertyDirective::Assume => "assume ",
        };
        out.push_str(&format!("    ; {}property {}: {}\n", directive_prefix, prop.name, desc,));
    }
}

// -----------------------------------------------------------------------
// Type mapping
// -----------------------------------------------------------------------

fn firrtl_type(ty: &SignalType) -> String {
    // Iterative to satisfy NASA P10 (no recursion). MAX_ARRAY_DIMS bounds nesting.
    const MAX_DEPTH: usize = crate::ast::types::MAX_ARRAY_DIMS + 2;
    enum Work<'a> {
        Emit(&'a SignalType),
        SuffixOwned(String),
    }
    let mut stack: Vec<Work<'_>> = Vec::with_capacity(MAX_DEPTH * 2);
    let mut result = String::new();
    stack.push(Work::Emit(ty));
    let mut iters = 0usize;
    while let Some(w) = stack.pop() {
        iters += 1;
        if iters > MAX_DEPTH * 4 {
            break;
        }
        match w {
            Work::Emit(t) => match t {
                SignalType::Bool => result.push_str("UInt<1>"),
                SignalType::Unsigned(w) => result.push_str(&format!("UInt<{}>", w)),
                SignalType::Signed(w) => result.push_str(&format!("SInt<{}>", w)),
                SignalType::Array { element, length } => {
                    stack.push(Work::SuffixOwned(format!("[{}]", length)));
                    stack.push(Work::Emit(element));
                }
                SignalType::Struct { fields, .. } => {
                    let mut parts = Vec::new();
                    let mut i = 0;
                    while i < fields.len() && i < crate::ast::types::MAX_STRUCT_FIELDS {
                        parts.push(format!("{}: {}", fields[i].0, firrtl_type_flat(&fields[i].1)));
                        i += 1;
                    }
                    result.push_str(&format!("{{ {} }}", parts.join(", ")));
                }
                SignalType::FixedPoint { total_bits, frac_bits } => {
                    result.push_str(&format!("FixedPoint<{},{}>", total_bits, frac_bits));
                }
                SignalType::Bundle(name) => {
                    result.push_str(&format!("{{ /* interface {} */ }}", name));
                }
                SignalType::Fifo { element, depth } => {
                    let elem_ty = firrtl_type_flat(element);
                    result.push_str(&format!("{}[{}]", elem_ty, depth));
                }
            },
            Work::SuffixOwned(s) => result.push_str(&s),
        }
    }
    result
}

/// Non-recursive helper for struct field types (limited to scalar + FixedPoint).
fn firrtl_type_flat(ty: &SignalType) -> String {
    match ty {
        SignalType::Bool => "UInt<1>".to_string(),
        SignalType::Unsigned(w) => format!("UInt<{}>", w),
        SignalType::Signed(w) => format!("SInt<{}>", w),
        SignalType::FixedPoint { total_bits, frac_bits } => {
            format!("FixedPoint<{},{}>", total_bits, frac_bits)
        }
        SignalType::Array { element, length } => {
            format!("{}[{}]", firrtl_type_flat(element), length)
        }
        SignalType::Fifo { element, depth } => {
            format!("{}[{}]", firrtl_type_flat(element), depth)
        }
        _ => format!("UInt<{}>", ty.width()),
    }
}

// -----------------------------------------------------------------------
// Expression mapping
// -----------------------------------------------------------------------

fn emit_condition_firrtl(ck: &crate::temporal::low_level_ir::ConditionKind) -> String {
    use crate::temporal::low_level_ir::ConditionKind;
    match ck {
        ConditionKind::SimpleSignal(s) => s.clone(),
        ConditionKind::NegatedSignal(s) => format!("not({})", s),
        ConditionKind::PrevSignal { signal, .. } => signal.clone(),
        ConditionKind::Comparison { signal, op, value } => {
            let op_fn = match op {
                BinaryOp::Eq => "eq",
                BinaryOp::Ne => "neq",
                BinaryOp::Lt => "lt",
                BinaryOp::Le => "leq",
                BinaryOp::Gt => "gt",
                BinaryOp::Ge => "geq",
                _ => "eq",
            };
            let val = match value {
                LiteralValue::Integer(n) => format!("UInt({})", n),
                LiteralValue::Bool(true) => "UInt(1)".to_string(),
                LiteralValue::Bool(false) => "UInt(0)".to_string(),
            };
            format!("{}({}, {})", op_fn, signal, val)
        }
        ConditionKind::AlwaysTrue => "UInt<1>(1)".to_string(),
    }
}

/// Emit an Expr as a FIRRTL expression string. Bounded by MAX_EXPR_NODES.
fn emit_expr_firrtl(expr: &Expr) -> String {
    let mut iterations = 0usize;
    emit_expr_firrtl_bounded(expr, &mut iterations)
}

fn emit_expr_firrtl_bounded(expr: &Expr, iterations: &mut usize) -> String {
    *iterations += 1;
    if *iterations > MAX_EXPR_NODES {
        return "; truncated".to_string();
    }

    match expr {
        Expr::Literal(LiteralValue::Bool(true)) => "UInt<1>(1)".to_string(),
        Expr::Literal(LiteralValue::Bool(false)) => "UInt<1>(0)".to_string(),
        Expr::Literal(LiteralValue::Integer(n)) => format!("UInt({})", n),
        Expr::Signal(name) => name.clone(),
        Expr::Prev { signal, delay } => {
            format!("{}_d{}", signal, delay)
        }
        Expr::Unary { op: UnaryOp::Not, operand } => {
            let inner = emit_expr_firrtl_bounded(operand, iterations);
            format!("not({})", inner)
        }
        Expr::Unary { op: UnaryOp::Negate, operand } => {
            let inner = emit_expr_firrtl_bounded(operand, iterations);
            format!("neg({})", inner)
        }
        Expr::Binary { op, left, right } => {
            let l = emit_expr_firrtl_bounded(left, iterations);
            let r = emit_expr_firrtl_bounded(right, iterations);
            let op_fn = match op {
                BinaryOp::And => "and",
                BinaryOp::Or => "or",
                BinaryOp::BitwiseOr => "or",
                BinaryOp::BitwiseAnd => "and",
                BinaryOp::Xor => "xor",
                BinaryOp::Lt => "lt",
                BinaryOp::Le => "leq",
                BinaryOp::Gt => "gt",
                BinaryOp::Ge => "geq",
                BinaryOp::Eq => "eq",
                BinaryOp::Ne => "neq",
                BinaryOp::Add => "add",
                BinaryOp::Sub => "sub",
                BinaryOp::Mul => "mul",
                BinaryOp::Shl => "dshl",
                BinaryOp::Shr => "dshr",
            };
            format!("{}({}, {})", op_fn, l, r)
        }
        Expr::ArrayIndex { array, index } => {
            let a = emit_expr_firrtl_bounded(array, iterations);
            let i = emit_expr_firrtl_bounded(index, iterations);
            format!("{}[{}]", a, i)
        }
        Expr::FieldAccess { object, field } => {
            let o = emit_expr_firrtl_bounded(object, iterations);
            format!("{}.{}", o, field)
        }
        Expr::ArrayLiteral(elems) => {
            let parts: Vec<String> = elems
                .iter()
                .take(MAX_EXPR_NODES)
                .map(|e| emit_expr_firrtl_bounded(e, iterations))
                .collect();
            if parts.is_empty() {
                "UInt(0)".to_string()
            } else {
                format!("cat({})", parts.join(", "))
            }
        }
        Expr::StructLiteral { fields, .. } => {
            let parts: Vec<String> = fields
                .iter()
                .take(crate::ast::types::MAX_STRUCT_FIELDS)
                .map(|(_, v)| emit_expr_firrtl_bounded(v, iterations))
                .collect();
            if parts.is_empty() {
                "UInt(0)".to_string()
            } else {
                format!("cat({})", parts.join(", "))
            }
        }
        Expr::UnfoldIndex(name) => unreachable!("UnfoldIndex '{}' reached FIRRTL emit", name),
    }
}

use super::expr_text;
