SilverSight/python/q16_fraction.py

"""
Q16_16 Fraction Arithmetic — exact rational exploration (no float in compute path)

Uses Python's Fraction for exact intermediate arithmetic.  Float only at the
outer I/O boundary (JSON/sensor input).  All compute-path operations are
pure Fraction arithmetic.

Designed for mutation value-set exploration:
  - No rounding, no truncation, no float error during sweeps
  - Quantize to Q16_16 raw int only at the final output boundary

Usage:
    from q16_fraction import Q16, q16_mul, q16_div, to_raw

    a = Q16.from_float(3.14)       # I/O boundary: float → Fraction
    b = Q16(1, 2)                  # exact 0.5:  Fraction(1, 2) * 65536
    c = q16_mul(a, b)              # exact 1.57: no truncation
    raw = to_raw(c)                # → 102893  (int, Lean-compatible)

Reference: FixedPoint.lean:298 — Lean truncates toward zero at each op.
           This module TRUNCATES only at the final to_raw() boundary.
           Exploration path uses exact arithmetic throughout.
"""

from __future__ import annotations

import math
import struct
from fractions import Fraction
from typing import Union

# ── Constants ──────────────────────────────────────────────────────────────

Q16_SCALE = 65536
INT32_MAX = 2147483647
INT32_MIN = -2147483648


# ── Q16 type: a Fraction scaled by 65536 in value, but exact in operation ──

class Q16(Fraction):
    """Q16_16 value as an exact Fraction.

    All arithmetic is exact rational (no float, no truncation).
    The value is the real number it represents (not the raw int).

    Construction:
        Q16(num, den)       — Fraction(num, den)  (exact rational)
        Q16.from_float(f)   — I/O boundary         (float → Fraction)
        Q16.from_raw(i)     — int raw value        (raw → Fraction)

    Conversion:
        to_raw(q)           — Fraction → int       (output boundary)
    """

    __slots__ = ()

    def __repr__(self) -> str:
        return f"Q16({float(self):.6f})"

    @classmethod
    def from_float(cls, f: float) -> Q16:
        """I/O boundary: float → Q16 via exact Fraction conversion.

        Uses Fraction.from_float for exact binary→rational conversion,
        then limits denominator to 65536 for Q16_16 compatibility.
        Raises ValueError if f is NaN or infinite.
        """
        if math.isnan(f) or math.isinf(f):
            raise ValueError(f"Non-finite float: {f}")
        return cls(Fraction.from_float(f).limit_denominator(Q16_SCALE))

    @classmethod
    def from_raw(cls, raw: int) -> Q16:
        """Convert a Q16_16 raw integer back to Q16.

        The raw int represents value * 65536 with truncation.
        This reverses the truncation: the Fraction captures the
        exact value that the raw int encodes.
        """
        return cls(raw, Q16_SCALE)

    def to_raw(self) -> int:
        """Quantize to Q16_16 raw int (truncation toward zero).

        Matches FixedPoint.lean:298 semantics at the output boundary.
        Use this when emitting Lean-compatible values.
        """
        num = self.numerator * Q16_SCALE
        den = self.denominator
        if num >= 0:
            return max(INT32_MIN, min(INT32_MAX, num // den))
        else:
            return max(INT32_MIN, min(INT32_MAX, -(-num // den)))

    def to_raw_rounded(self) -> int:
        """Quantize to Q16_16 raw int with round-half-up.

        Alternative output boundary for cases where rounding is preferred
        over truncation.  Not Lean-compatible by default.
        """
        return max(
            INT32_MIN,
            min(INT32_MAX, int(round(self.numerator * Q16_SCALE / self.denominator))),
        )

    def to_float(self) -> float:
        """Debug/convenience: convert to float.

        Not part of the compute path — use only for logging/display.
        """
        return float(self)


# ── Arithmetic (exact Fraction, no float, no truncation) ──────────────────

def q16_mul(a: Union[Q16, Fraction], b: Union[Q16, Fraction]) -> Q16:
    """Exact Q16 multiplication.  No truncation, no float.

    Contrast with Lean's truncating mul (FixedPoint.lean:298).
    This path preserves full precision for mutation exploration.
    """
    return Q16(a * b)


def q16_div(a: Union[Q16, Fraction], b: Union[Q16, Fraction]) -> Q16:
    """Exact Q16 division.  No truncation, no float.

    Raises ZeroDivisionError if b is zero.
    """
    if b == 0:
        raise ZeroDivisionError("Q16 division by zero")
    return Q16(a / b)


def q16_add(a: Union[Q16, Fraction], b: Union[Q16, Fraction]) -> Q16:
    return Q16(a + b)


def q16_sub(a: Union[Q16, Fraction], b: Union[Q16, Fraction]) -> Q16:
    return Q16(a - b)


# ── Convenience constructors ───────────────────────────────────────────────

def to_raw(a: Union[Q16, Fraction]) -> int:
    """Convert any Q16/Fraction to Q16_16 raw int.

    One-shot boundary function for the common case.
    """
    if isinstance(a, Fraction) and not isinstance(a, Q16):
        a = Q16(a)
    return a.to_raw()


def from_raw(raw: int) -> Q16:
    return Q16.from_raw(raw)


def from_float(f: float) -> Q16:
    return Q16.from_float(f)


# ── Serialization ──────────────────────────────────────────────────────────

def q16_from_bytes(raw_bytes: bytes) -> Q16:
    return Q16.from_raw(struct.unpack("<i", raw_bytes)[0])


def q16_to_bytes(a: Union[Q16, Fraction]) -> bytes:
    return struct.pack("<i", to_raw(a))


# ── Eval witnesses ────────────────────────────────────────────────────────

if __name__ == "__main__":
    # Mutation exploration: all arithmetic is exact
    a = Q16.from_float(3.0)
    b = Q16(1, 3)  # exact 1/3

    c = q16_mul(a, b)  # exact 1.0
    d = q16_div(a, b)  # exact 9.0
    e = q16_add(c, d)  # exact 10.0

    print(f"  3.0 × 1/3 = {c.to_float():.6f}  (raw={to_raw(c)})")
    print(f"  3.0 ÷ 1/3 = {d.to_float():.6f}  (raw={to_raw(d)})")
    print(f"  1.0 + 9.0 = {e.to_float():.6f}  (raw={to_raw(e)})")

    # Compare with Lean-compatible truncation at boundary
    a_raw = from_float(3.14)
    b_raw = from_raw(102893)
    print(f"  3.14 as Q16: {a_raw}  (raw={to_raw(a_raw)})")
    print(f"  raw 102893  → {b_raw.to_float():.6f}")