"""Export the Graph Motif rate certificate (c = 2) to a Lean data file.

Usage (from the repository root):
    python3 formal/scripts/export_cc_cert.py > formal/MaxLeafFormal/CCData.lean

Recomputes the parameters y_j of ancillary/component_count_rate_interval.py
exactly as that program does: for the j-th interval [a_j, b_j] = [0.7175 + j/10^4,
0.7175 + (j+1)/10^4], j = 0, ..., 924, y_j is the floating-point minimiser of phi at the midpoint,
printed with six significant digits ("%.6g") and read back as an exact decimal. The functions
`phif`, `best_y` and `dec` below are copied verbatim from that program (which also imports
python-flint, not needed here).

The generated file is data, not proof: Lean re-checks every interval in the kernel
(`MaxLeafFormal.CCRate.checkIntervals`), so a wrong export can only make a check fail.
"""
import hashlib
import math
import os
import sys
from fractions import Fraction

ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
SRC = os.path.join(ROOT, "ancillary", "component_count_rate_interval.py")


def phif(rho, y):
    s = (1 + 2 * y + math.sqrt(1 + 4 * y * y)) / 2
    return math.log2(1 + y) - rho * math.log2(s / 2)


def best_y(rho):
    grid = [-6 + 10 * i / 2000 for i in range(2001)]
    s = min(grid, key=lambda t: phif(rho, math.exp(t)))
    step = 10 / 2000
    for _ in range(80):
        s = min((s - step, s, s + step), key=lambda t: phif(rho, math.exp(t)))
        step /= 1.5
    return "%.6g" % math.exp(s)


def dec(s):
    # as component_count_rate_interval.dec, with Fraction for fmpq
    s = s.strip()
    if "e" in s.lower():
        m, e = s.lower().split("e")
        return dec(m) * Fraction(10) ** int(e) if int(e) >= 0 else dec(m) / Fraction(10) ** (-int(e))
    if "." in s:
        ip, fp = s.split(".")
        return Fraction(int(ip + fp), 10 ** len(fp))
    return Fraction(int(s))


def q(x):
    x = Fraction(x)
    assert x > 0
    return f"q {x.numerator} {x.denominator}"


def main():
    sys.stdout.reconfigure(encoding="utf-8", newline="\n")
    # Hash LF-normalised bytes, so that the header does not depend on the checkout's line endings.
    sha = hashlib.sha256(open(SRC, "rb").read().replace(b"\r\n", b"\n")).hexdigest()
    rho0, rho1, h = Fraction(7175, 10 ** 4), Fraction(81, 100), Fraction(1, 10 ** 4)
    ys = []
    a = rho0
    while a < rho1:
        b = a + h
        mid = a + b
        ys.append(dec(best_y(float(mid.numerator) / float(mid.denominator) / 2)))
        a = b
    assert len(ys) == 925
    out = [
        "import Mathlib",
        "",
        "/-!",
        "# Graph Motif rate certificate data (generated)",
        "",
        "Generated by `formal/scripts/export_cc_cert.py`, recomputing the parameters of",
        f"`ancillary/component_count_rate_interval.py`, SHA-256 `{sha}`.",
        "Entry `j` is `y_j` for the interval `[0.7175 + j/10^4, 0.7175 + (j+1)/10^4]`.",
        "Do not edit by hand. This file is data, not proof: every condition is re-checked in",
        "`MaxLeafFormal.CCRate`.",
        "-/",
        "",
        "set_option maxRecDepth 100000",
        "",
        "namespace MaxLeafFormal.CCRate",
        "",
        "/-- The rational `a / b`. -/",
        "def q (a b : ℕ) : ℚ := (a : ℚ) / b",
        "",
        "/-- The parameters `y_j`, `j = 0, …, 924`. -/",
        "def ys : List ℚ := [",
        ",\n".join(f"  {q(y)}" for y in ys),
        "]",
        "",
        "end MaxLeafFormal.CCRate",
    ]
    print("\n".join(out))


if __name__ == "__main__":
    main()