//! hybrid_zeckendorf_multiply.rs
//!
//! Safe Rust transpilation from verified C (CAB pipeline).
//! Source: HeytingLean.Bridge.Veselov.HybridZeckendorf.Multiplication
//!
//! Structural multiplication via level fold, halving/doubling,
//! parity detection, and density statistics.
//!
//! Provenance: Lean 4 → LambdaIR → MiniC → C → Rust
//! Correctness inherited from verified C source.

use crate::hybrid_zeckendorf_add::add;
use crate::hybrid_zeckendorf_eval::{eval, from_nat, HybridNumber, MAX_LEVELS};
use crate::hybrid_zeckendorf_fib::lazy_eval_fib;
use crate::hybrid_zeckendorf_weight::weight;

/// Double operation: `doubleHybrid(X) = add(X, X)`.
///
/// (Lean: `doubleHybrid`)
///
/// Theorem preserved: `doubleHybrid_correct` — `eval(double X) = 2 * eval X`
pub fn double_hybrid(x: &HybridNumber) -> HybridNumber {
    add(x, x)
}

/// Structural half of positive-level contributions.
///
/// (Lean: `halfTailNat`)
fn half_tail_nat(x: &HybridNumber) -> u64 {
    (1..MAX_LEVELS)
        .filter(|&i| !x.levels[i].is_empty())
        .map(|i| {
            let lev = lazy_eval_fib(&x.levels[i].indices);
            lev * (weight(i as u32) / 2)
        })
        .sum()
}

/// Halve a hybrid number by structural decomposition.
///
/// Level 0 handles odd remainder; positive levels contribute even tail.
///
/// (Lean: `halveHybrid`)
///
/// Theorem preserved: `halveHybrid_correct` — `eval(halve X) = eval X / 2`
pub fn halve_hybrid(x: &HybridNumber) -> HybridNumber {
    let level0_val = lazy_eval_fib(&x.levels[0].indices);
    let level0_half = level0_val / 2;
    let tail_half = half_tail_nat(x);

    let a = from_nat(level0_half);
    let b = from_nat(tail_half);
    add(&a, &b)
}

/// Parity query.
///
/// (Lean: `isOddHybrid`)
pub fn is_odd(x: &HybridNumber) -> bool {
    eval(x) % 2 == 1
}

/// Repeated structural addition: `repeatAdd(A, n) = A` added `n` times.
///
/// (Lean: `repeatAdd`)
///
/// Theorem preserved: `repeatAdd_correct` — `eval(repeatAdd A n) = eval A * n`
pub fn repeat_add(a: &HybridNumber, n: u64) -> HybridNumber {
    let mut acc = HybridNumber::zero();
    for _ in 0..n {
        acc = add(&acc, a);
    }
    acc
}

/// Bounded multiplication fold over levels `0..n-1`.
///
/// (Lean: `multiplyUpTo`)
///
/// Theorem preserved: `multiplyUpTo_correct`
pub fn multiply_up_to(a: &HybridNumber, b: &HybridNumber, n: usize) -> HybridNumber {
    let mut acc = HybridNumber::zero();
    for i in 0..n.min(MAX_LEVELS) {
        if !b.levels[i].is_empty() {
            let lev = lazy_eval_fib(&b.levels[i].indices);
            let mult = lev * weight(i as u32);
            if mult > 0 {
                let term = repeat_add(a, mult);
                acc = add(&acc, &term);
            }
        }
    }
    acc
}

/// Binary multiplication via structural bounded fold over support depth.
///
/// (Lean: `multiplyBinary`)
///
/// Theorem preserved: `multiplyBinary_correct` — `eval(multiply A B) = eval A * eval B`
pub fn multiply(a: &HybridNumber, b: &HybridNumber) -> HybridNumber {
    let depth = b
        .levels
        .iter()
        .rposition(|p| !p.is_empty())
        .map_or(0, |i| i + 1);
    multiply_up_to(a, b, depth)
}

/// Number of active indices across all levels.
///
/// (Lean: `supportCard`)
pub fn support_card(x: &HybridNumber) -> u64 {
    x.levels.iter().map(|p| p.len() as u64).sum()
}

/// Density-like statistic: `supportCard / log_phi(eval)`.
///
/// (Lean: `density`)
///
/// Golden ratio `phi = (1 + sqrt(5)) / 2`.
pub fn density(x: &HybridNumber) -> f64 {
    let val = eval(x);
    if val == 0 {
        return 0.0;
    }
    let phi = (1.0 + 5.0_f64.sqrt()) / 2.0;
    let log_phi_val = (val as f64).ln() / phi.ln();
    support_card(x) as f64 / log_phi_val
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_double_correct() {
        let x = from_nat(42);
        assert_eq!(eval(&double_hybrid(&x)), 84);
    }

    #[test]
    fn test_halve_correct() {
        let x = from_nat(100);
        assert_eq!(eval(&halve_hybrid(&x)), 50);
    }

    #[test]
    fn test_multiply_correct() {
        let a = from_nat(7);
        let b = from_nat(6);
        assert_eq!(eval(&multiply(&a, &b)), 42);
    }

    #[test]
    fn test_density_positive() {
        let x = from_nat(1000);
        assert!(density(&x) > 0.0);
    }
}