from __future__ import annotations

import json
from pathlib import Path

import pytest

from leanbench.db import Database, ItemRow, item_id


def row(**overrides) -> ItemRow:
    data = dict(
        id="",
        source_hash="book-hash-a",
        kind="statement",
        label="Theorem 1.6.2",
        summary="divisibility is additive",
        informal="a | b and a | c implies a | b + c",
        start_page=12,
        start_index=100,
        end_page=12,
        end_index=260,
        page_checksum="abc",
        source_text="Theorem 1.6.2 ...",
        lean_name="dvd_add'",
        lean_code="theorem dvd_add' (a b c : Int) : True := trivial",
        imports=["Mathlib"],
        has_proof=True,
        verified=True,
        proved=True,
        verify_mode="full",
        diagnostics="",
        confidence=0.9,
        match_method="exact",
        match_score=1.0,
        truncated=False,
        types=[("Int", "input")],
    )
    data.update(overrides)
    if not data["id"]:
        data["id"] = item_id(data["source_hash"], data["start_page"], data["start_index"],
                             data["end_page"], data["end_index"])
    return ItemRow(**data)


@pytest.fixture()
def database(tmp_path: Path) -> Database:
    db = Database(tmp_path / "test.sqlite")
    db.upsert_source("book-hash-a", title="Algebra", path="a.pdf", pages=400)
    yield db
    db.close()


def test_item_id_is_stable_for_the_same_span() -> None:
    first = item_id("h", 1, 2, 3, 4)
    assert first == item_id("h", 1, 2, 3, 4)
    assert first != item_id("h", 1, 2, 3, 5)


def test_store_and_read_back(database: Database) -> None:
    identifier = database.upsert_item(row())
    stored = database.get(identifier)
    assert stored is not None
    assert stored["imports"] == ["Mathlib"]
    assert stored["types"] == [{"name": "Int", "role": "input"}]


def test_reingesting_the_same_span_updates_rather_than_duplicates(database: Database) -> None:
    database.upsert_item(row())
    database.upsert_item(row(lean_name="renamed", types=[("Nat", "input")]))
    assert database.stats()["items"] == 1
    stored = database.get(item_id("book-hash-a", 12, 100, 12, 260))
    assert stored is not None and stored["lean_name"] == "renamed"
    assert stored["types"] == [{"name": "Nat", "role": "input"}], "stale types are dropped"


def test_search_by_type_is_the_point(database: Database) -> None:
    database.upsert_item(row(types=[("Int", "input")]))
    database.upsert_item(row(start_index=500, end_index=700, kind="problem",
                             types=[("Polynomial", "input"), ("Int", "input")]))
    assert len(database.search(types=["Int"])) == 2
    assert len(database.search(types=["Polynomial"])) == 1
    assert len(database.search(types=["Int", "Polynomial"], match_all_types=True)) == 1
    assert len(database.search(types=["Int"], kind="problem")) == 1


def test_search_by_role_separates_definitions_from_theorems(database: Database) -> None:
    database.upsert_item(row(types=[("Ideal", "own")]))
    database.upsert_item(row(start_index=900, end_index=950, types=[("Ideal", "input")]))
    assert len(database.search(types=["Ideal"], roles=["own"])) == 1
    assert len(database.search(types=["Ideal"], roles=["input"])) == 1


def test_search_by_page_finds_items_spanning_it(database: Database) -> None:
    database.upsert_item(row(start_page=12, end_page=14))
    assert len(database.search(page=13)) == 1
    assert len(database.search(page=20)) == 0


def test_dropping_a_page_range_lets_you_redo_part_of_a_book(database: Database) -> None:
    database.upsert_item(row(start_page=12))
    database.upsert_item(row(start_page=40, start_index=1, end_page=40, end_index=50))
    removed = database.delete_pages("book-hash-a", 10, 20)
    assert removed == 1
    assert database.stats()["items"] == 1
    assert database.search(page=40)


def test_dropping_a_source_takes_its_items_with_it(database: Database) -> None:
    database.upsert_item(row())
    database.delete_source("book-hash-a")
    assert database.stats()["items"] == 0
    assert database.sources() == []


def test_export_jsonl_leaves_out_bulk_by_default(database: Database, tmp_path: Path) -> None:
    database.upsert_item(row())
    out = tmp_path / "items.jsonl"
    assert database.export_jsonl(out) == 1
    record = json.loads(out.read_text(encoding="utf-8").splitlines()[0])
    assert "source_text" not in record and "diagnostics" not in record
    assert record["types"] == [{"name": "Int", "role": "input"}]
    assert database.export_jsonl(out, include_source_text=True) == 1
    assert "source_text" in json.loads(out.read_text(encoding="utf-8").splitlines()[0])


def test_stats_counts_the_things_that_matter(database: Database) -> None:
    database.upsert_item(row())
    database.upsert_item(row(start_index=2, kind="problem", proved=False, verified=True))
    stats = database.stats()
    assert stats["items"] == 2 and stats["statements"] == 1 and stats["problems"] == 1
    assert stats["verified"] == 2 and stats["proved"] == 1
    assert database.type_counts()[0]["name"] == "Int"