//! Continued fractions — the Euclidean quotient sequence and its convergents.

/// A `u64/b` expansion has at most 92 partial quotients — the worst case is two
/// consecutive Fibonacci numbers, on which the Euclidean algorithm takes the most
/// steps (Lamé's theorem). The capacity is therefore fixed and no allocation is
/// needed; 93 leaves one slot of headroom so `push` never reaches the end.
const MAX_QUOTIENTS: usize = 93;

/// The continued-fraction expansion of a rational `a/b`, returned by
/// [`continued_fraction`]: the partial quotients `[a₀; a₁, a₂, …]` of the
/// Euclidean algorithm on `(a, b)`, in order of index. A `u64/u64` expansion has
/// at most 92 terms, so the storage is a fixed array — no allocation.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct ContinuedFraction {
    quotients: [u64; MAX_QUOTIENTS],
    len: usize,
}

impl ContinuedFraction {
    /// The partial quotients `[a₀, a₁, …, aₙ]`, in order. `a₀ = ⌊a/b⌋`.
    #[must_use]
    pub fn as_slice(&self) -> &[u64] {
        &self.quotients[..self.len]
    }

    /// The convergents `hₖ/kₖ` as ascending `(numerator, denominator)` pairs,
    /// starting at `a₀/1`. The last convergent is `a/b` in lowest terms —
    /// `(a/gcd(a,b), b/gcd(a,b))`. Each denominator is the best rational
    /// approximation of `a/b` of its size; this is the lever Wiener's small-`d`
    /// RSA attack pulls on `e/N`.
    #[must_use]
    pub fn convergents(&self) -> Convergents {
        Convergents {
            quotients: self.quotients, // own a copy of the fixed array (no borrow)
            len: self.len,
            i: 0,
            h: (0, 1), // (h₋₂, h₋₁)
            k: (1, 0), // (k₋₂, k₋₁)
        }
    }

    /// Append a partial quotient. `len` never reaches `MAX_QUOTIENTS`: a `u64/u64`
    /// expansion has at most 92 terms (Lamé) and the capacity is 93.
    fn push(&mut self, q: u64) {
        self.quotients[self.len] = q;
        self.len += 1;
    }
}

/// Iterator over the convergents `(hₖ, kₖ)` of a [`ContinuedFraction`], from
/// [`ContinuedFraction::convergents`]. Yields `(numerator, denominator)` in order,
/// from `a₀/1` up to `a/b` in lowest terms.
///
/// It **owns** a copy of the quotient array rather than borrowing the source
/// [`ContinuedFraction`] (the array is a fixed `[u64; 93]`, ~744 bytes copied
/// once per [`ContinuedFraction::convergents`] call). Owning the data — instead
/// of holding a `&[u64]` borrow stepped across `next` calls — is what lets the
/// Aeneas→Lean leg model the iterator: a borrow held in a struct field across
/// calls is outside Aeneas's functional translation, an owned array is not.
#[derive(Clone, Debug)]
pub struct Convergents {
    quotients: [u64; MAX_QUOTIENTS],
    len: usize,
    i: usize,
    h: (u64, u64), // (hₖ₋₂, hₖ₋₁)
    k: (u64, u64), // (kₖ₋₂, kₖ₋₁)
}

impl Iterator for Convergents {
    type Item = (u64, u64);

    fn next(&mut self) -> Option<(u64, u64)> {
        if self.i >= self.len {
            return None; // exhausted (i < len ≤ 92, so the index below is in bounds)
        }
        let a = self.quotients[self.i];
        // hₖ = aₖ·hₖ₋₁ + hₖ₋₂ and kₖ = aₖ·kₖ₋₁ + kₖ₋₂. Both stay below the inputs
        // — the sequences are non-decreasing and the last convergent is a/b in
        // lowest terms, so hₖ ≤ a and kₖ ≤ b — hence neither product overflows u64.
        let h = a * self.h.1 + self.h.0;
        let k = a * self.k.1 + self.k.0;
        self.h = (self.h.1, h);
        self.k = (self.k.1, k);
        self.i += 1;
        Some((h, k))
    }
}

/// The continued-fraction expansion of the rational `a/b`: the partial quotients
/// `[a₀; a₁, …]` produced by the Euclidean algorithm on `(a, b)`. `a₀ = ⌊a/b⌋`;
/// for `a < b` it is `0` and the expansion opens `[0; …]`. By convention
/// `continued_fraction(a, 0) = [a]`.
///
/// Total over every `u64` pair and overflow-free: each quotient is one Euclidean
/// division and there are at most 92 of them. Recover the value — or its best
/// rational approximations — with [`ContinuedFraction::convergents`]; the final
/// convergent is `a/b` in lowest terms.
///
/// # Examples
///
/// ```
/// use coprime::number::continued_fraction;
///
/// assert_eq!(continued_fraction(415, 93).as_slice(), &[4, 2, 6, 7]);
/// assert_eq!(continued_fraction(649, 200).as_slice(), &[3, 4, 12, 4]);
/// assert_eq!(continued_fraction(1, 2).as_slice(), &[0, 2]); // a < b opens with 0
///
/// // the convergents climb to a/b in lowest terms
/// let last = continued_fraction(415, 93).convergents().last().unwrap();
/// assert_eq!(last, (415, 93));
/// ```
#[must_use]
pub fn continued_fraction(a: u64, b: u64) -> ContinuedFraction {
    let mut cf = ContinuedFraction {
        quotients: [0; MAX_QUOTIENTS],
        len: 0,
    };
    let (mut x, mut y) = (a, b);
    while y != 0 {
        cf.push(x / y);
        (x, y) = (y, x % y);
    }
    if cf.len == 0 {
        cf.push(x); // y was 0 from the start: a/0 ↦ [a] by convention
    }
    cf
}

/// Extraction anchor for the Aeneas→Lean leg — **not** part of the public API.
///
/// `Convergents::next` is a trait-impl method; Charon translates it but Aeneas
/// only emits an impl method that some *free* function in the extracted closure
/// calls (a `--start-from` leaf method is pruned). This free function calls
/// `next()` directly so the concrete `Convergents::next` is emitted as a Lean
/// definition for `CfracSpec.lean` to prove the convergent recurrence against;
/// `.last()` would not do — Aeneas models that default method as opaque. The
/// body mirrors how every caller drives the iterator (walk to the last
/// convergent, `a/b` in lowest terms). `#[cfg(not(kani))]` keeps it off the
/// Kani build, where the unused-function lint is live.
#[cfg(not(kani))]
#[allow(dead_code)]
// The explicit `while let … = conv.next()` is load-bearing: a `for c in conv`
// loop desugars through `IntoIterator`, which Aeneas models with builtin
// iterator machinery that never names the concrete `Convergents::next` — so it
// would not get emitted. Calling `next()` directly is the whole point.
#[allow(clippy::while_let_on_iterator)]
fn convergents_extraction_anchor(cf: &ContinuedFraction) -> Option<(u64, u64)> {
    let mut conv = cf.convergents();
    let mut last = None;
    while let Some(c) = conv.next() {
        last = Some(c);
    }
    last
}
