//! hybrid_zeckendorf_eval.rs
//!
//! Safe Rust transpilation from verified C (CAB pipeline).
//! Source: HeytingLean.Bridge.Veselov.HybridZeckendorf.HybridNumber
//!
//! Core types, evaluation maps, and canonical constructors.
//!
//! Provenance: Lean 4 → LambdaIR → MiniC → C → Rust
//! Correctness inherited from verified C source.

use crate::hybrid_zeckendorf_fib::{fib, lazy_eval_fib};
use crate::hybrid_zeckendorf_weight::weight;

/// Maximum number of hierarchy levels.
pub const MAX_LEVELS: usize = 8;

/// A single level's Zeckendorf payload: a list of Fibonacci indices.
///
/// (Lean: `ZeckPayload` / `LazyPayload` = `List Nat`)
#[derive(Clone, Debug, Default)]
pub struct Payload {
    pub indices: Vec<u32>,
}

impl Payload {
    pub fn new() -> Self {
        Self { indices: Vec::new() }
    }

    pub fn from_indices(indices: Vec<u32>) -> Self {
        Self { indices }
    }

    pub fn is_empty(&self) -> bool {
        self.indices.is_empty()
    }

    pub fn len(&self) -> usize {
        self.indices.len()
    }
}

/// A hybrid number: finite-support map from level to payload.
///
/// (Lean: `HybridNumber = Nat →₀ ZeckPayload`)
#[derive(Clone, Debug)]
pub struct HybridNumber {
    pub levels: Vec<Payload>,
}

impl HybridNumber {
    /// Zero hybrid number.
    pub fn zero() -> Self {
        Self {
            levels: (0..MAX_LEVELS).map(|_| Payload::new()).collect(),
        }
    }

    /// Single-level hybrid number with given payload at level `i`.
    pub fn single(level: usize, indices: Vec<u32>) -> Self {
        let mut num = Self::zero();
        if level < MAX_LEVELS {
            num.levels[level] = Payload::from_indices(indices);
        }
        num
    }

    /// Number of active levels.
    pub fn num_levels(&self) -> usize {
        self.levels
            .iter()
            .rposition(|p| !p.is_empty())
            .map_or(0, |i| i + 1)
    }
}

impl Default for HybridNumber {
    fn default() -> Self {
        Self::zero()
    }
}

/// Per-level semantic value.
///
/// (Lean: `levelEval z = lazyEvalFib z`)
pub fn level_eval(payload: &Payload) -> u64 {
    lazy_eval_fib(&payload.indices)
}

/// Full semantic value of a hybrid number.
///
/// `eval(X) = Σ_i levelEval(X_i) * weight(i)`
///
/// (Lean theorems: `eval_single`, `eval_add`, `eval_fromNat`)
pub fn eval(x: &HybridNumber) -> u64 {
    x.levels
        .iter()
        .enumerate()
        .map(|(i, p)| {
            if p.is_empty() {
                0
            } else {
                level_eval(p) * weight(i as u32)
            }
        })
        .sum()
}

/// Compute canonical Zeckendorf representation of `n`.
///
/// Returns indices in decreasing order (greedy algorithm).
///
/// (Lean: `Nat.zeckendorf`)
pub fn zeckendorf(n: u64) -> Vec<u32> {
    if n == 0 {
        return Vec::new();
    }

    let mut max_idx: u32 = 2;
    while fib(max_idx + 1) <= n {
        max_idx += 1;
    }

    let mut result = Vec::new();
    let mut remaining = n;
    let mut idx = max_idx;

    while idx >= 2 && remaining > 0 {
        let f = fib(idx);
        if f <= remaining {
            result.push(idx);
            remaining -= f;
            if idx > 1 {
                idx -= 1; // skip consecutive (Zeckendorf property)
            }
        }
        if idx == 0 {
            break;
        }
        idx -= 1;
    }
    if remaining > 0 && remaining == fib(1) {
        result.push(1);
    }

    result
}

/// Embed a natural number as a single-level-0 canonical hybrid number.
///
/// (Lean: `fromNat`)
pub fn from_nat(n: u64) -> HybridNumber {
    HybridNumber::single(0, zeckendorf(n))
}

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

    #[test]
    fn test_eval_zero() {
        assert_eq!(eval(&HybridNumber::zero()), 0);
    }

    #[test]
    fn test_from_nat_roundtrip() {
        for n in [0, 1, 5, 13, 100, 1000] {
            assert_eq!(eval(&from_nat(n)), n);
        }
    }

    #[test]
    fn test_zeckendorf_canonical() {
        let z = zeckendorf(100);
        // No two consecutive indices
        for w in z.windows(2) {
            assert!(w[0] > w[1] + 1, "consecutive indices: {} and {}", w[0], w[1]);
        }
        // Sum equals input
        assert_eq!(lazy_eval_fib(&z), 100);
    }
}