#!/usr/bin/env python3
"""Checks a packing of unit squares in a square by exact arithmetic: rational numbers throughout, no floating point, no tolerance.

    python verify_exact.py certificate.csv --squares=17 --reference=4.67553009360455 --epsilon=1e-11
    python verify_exact.py --records=records.json

A certificate: lines starting with # are comments; then one line "side,<L>"; then one line per square: x,y,t, its centre and t = tan(half its turn).
All numbers are read as exact decimals. cos = (1 - t^2) / (1 + t^2) and sin = 2t / (1 + t^2) are exact rationals with cos^2 + sin^2 = 1, so each square is exactly a unit square by construction; the script confirms that on the numbers anyway.
Any other form of file is refused. There is no way to get a PASS from rounded corners.

A PASS establishes, about exactly the numbers in the file:
  1. UNIT SQUARES: each piece has four sides of length exactly 1 and four exact right angles.
  2. CONTAINED: each corner of each square lies in the closed box [0, L] x [0, L], and L > 0.
  3. DISJOINT: no two squares share interior points; they may touch. For each pair, one edge of one square has every corner of the other on or beyond its line (the separating axis theorem for convex shapes), or their exact bounding boxes do not overlap.
  4. COUNT: with --squares=N, the file holds exactly N squares.

With --reference, the closeness to a reference value is a separate result, printed exactly: L - reference. With --epsilon it is also tested exactly: |L - reference| <= epsilon, reported as MATCH or NO MATCH. A valid packing can be no match.

A PASS does NOT establish that a packing is optimal, that a reference value is the current record, or how or by whom the layout was found.

--records=<records.json> checks every record listed in that file, each against its own square count and best known value, and prints one line each and a total. Files are looked for beside records.json.
Exit code 0: every file passed (and matched, where an epsilon was asked for). 1: otherwise. 2: a file could not be read as a certificate.
"""
import json
import os
import sys
from fractions import Fraction as F


class NotACertificate(Exception):
    pass


def read(path):
    side = None
    poses = []
    with open(path, encoding="utf-8") as lines:
        for number, line in enumerate(lines, 1):
            line = line.strip()
            if not line or line.startswith("#"):
                continue
            fields = line.split(",")
            try:
                if fields[0] == "side":
                    if side is not None:
                        raise NotACertificate(f"line {number}: a second side line")
                    if len(fields) != 2:
                        raise NotACertificate(f"line {number}: the side line is side,<L>")
                    side = F(fields[1])
                    continue
                if len(fields) != 3:
                    raise NotACertificate(f"line {number}: a square is x,y,t, three numbers; found {len(fields)}. Rounded corners are not accepted")
                poses.append((F(fields[0]), F(fields[1]), F(fields[2])))
            except (ValueError, ZeroDivisionError) as error:
                raise NotACertificate(f"line {number}: not an exact number: {error}")
    if side is None:
        raise NotACertificate("no side line")
    return side, poses


def corners(x, y, t):
    c = (1 - t * t) / (1 + t * t)
    s = 2 * t / (1 + t * t)
    half = F(1, 2)
    return [(x + (a * c - b * s) * half, y + (a * s + b * c) * half) for a, b in ((-1, -1), (1, -1), (1, 1), (-1, 1))]


def separated(a, b):
    """An edge of a (counter-clockwise) with every corner of b on or beyond its line."""
    for i in range(4):
        ux, uy = a[i]
        wx, wy = a[(i + 1) % 4]
        ex, ey = wx - ux, wy - uy
        if all(ex * (y - uy) - ey * (x - ux) <= 0 for x, y in b):
            return True
    return False


def exact_text(x):
    """A rational as its exact decimal when it has one, else as a fraction: nothing is rounded."""
    if x == 0:
        return "0"
    sign = "-" if x < 0 else "+"
    x = abs(x)
    denominator = x.denominator
    twos = fives = 0
    while denominator % 2 == 0:
        denominator //= 2
        twos += 1
    while denominator % 5 == 0:
        denominator //= 5
        fives += 1
    if denominator != 1:
        return f"{sign}{x.numerator}/{x.denominator}"
    places = max(twos, fives)
    scaled = x.numerator * 10 ** places // x.denominator
    digits = str(scaled).rjust(places + 1, "0")
    text = digits[:-places] + "." + digits[-places:] if places else digits
    return sign + text


def check(path, expected=None, reference=None, epsilon=None):
    """Answers (passed, matched or None, the line to print). Raises NotACertificate."""
    side, poses = read(path)
    squares = [corners(*p) for p in poses]
    n = len(squares)
    lengths_ok = all((s[i][0] - s[(i + 1) % 4][0]) ** 2 + (s[i][1] - s[(i + 1) % 4][1]) ** 2 == 1 for s in squares for i in range(4))
    angles_ok = all((s[(i + 1) % 4][0] - s[i][0]) * (s[(i + 3) % 4][0] - s[i][0]) + (s[(i + 1) % 4][1] - s[i][1]) * (s[(i + 3) % 4][1] - s[i][1]) == 0 for s in squares for i in range(4))
    unit = lengths_ok and angles_ok
    outside = sum(1 for s in squares if any(not (0 <= x <= side and 0 <= y <= side) for x, y in s))
    boxes = [(min(p[0] for p in s), max(p[0] for p in s), min(p[1] for p in s), max(p[1] for p in s)) for s in squares]
    overlapping = 0
    for i in range(n):
        for j in range(i):
            if boxes[i][1] <= boxes[j][0] or boxes[j][1] <= boxes[i][0] or boxes[i][3] <= boxes[j][2] or boxes[j][3] <= boxes[i][2]:
                continue
            if not (separated(squares[i], squares[j]) or separated(squares[j], squares[i])):
                overlapping += 1
    count_ok = expected is None or n == expected
    passed = n > 0 and side > 0 and unit and outside == 0 and overlapping == 0 and count_ok
    parts = [f"{path}: {'PASS' if passed else 'FAIL'}", f"{n} squares" + ("" if count_ok else f", {expected} EXPECTED"), "unit squares exact" if unit else "NOT UNIT SQUARES", f"corners outside the box: {outside}", f"overlapping pairs: {overlapping}", f"L = {exact_text(side)[1:]}"]
    matched = None
    if reference is not None:
        difference = side - reference
        parts.append(f"L - reference = {exact_text(difference)}")
        if epsilon is not None:
            matched = passed and abs(difference) <= epsilon
            parts.append(f"{'MATCH' if matched else 'NO MATCH'} at |L - reference| <= {exact_text(epsilon)[1:]}")
    return passed, matched, "; ".join(parts)


def main(arguments):
    paths, expected, reference, epsilon, records = [], None, None, None, None
    for a in arguments:
        if a.startswith("--squares="):
            expected = int(a.split("=", 1)[1])
        elif a.startswith("--reference="):
            reference = F(a.split("=", 1)[1])
        elif a.startswith("--epsilon="):
            epsilon = F(a.split("=", 1)[1])
        elif a.startswith("--records="):
            records = a.split("=", 1)[1]
        elif a.startswith("--"):
            print(f"unknown option {a}", file=sys.stderr)
            return 2
        else:
            paths.append(a)
    if records is None and not paths:
        print(__doc__)
        return 2
    code = 0
    if records is not None:
        data = json.load(open(records, encoding="utf-8"))
        folder = os.path.dirname(os.path.abspath(records))
        rule = F(data["epsilon"]) if "epsilon" in data else None
        total = matches = 0
        for r in data["records"]:
            path = os.path.join(folder, r["files"]["csv"])
            total += 1
            try:
                passed, matched, line = check(path, r["squares"], F(r["best_known"]), rule)
            except (NotACertificate, OSError) as error:
                print(f"{path}: REFUSED: {error}")
                code = max(code, 2)
                continue
            print(line)
            if passed and matched is not False:
                matches += 1
            else:
                code = max(code, 1)
        print(f"{matches} of {total} records passed" + (f" and matched within {exact_text(rule)[1:]}" if rule is not None else ""))
        return code
    for path in paths:
        try:
            passed, matched, line = check(path, expected, reference, epsilon)
        except (NotACertificate, OSError) as error:
            print(f"{path}: REFUSED: {error}")
            code = max(code, 2)
            continue
        print(line)
        if not passed or matched is False:
            code = max(code, 1)
    return code


if __name__ == "__main__":
    sys.exit(main(sys.argv[1:]))