from __future__ import annotations

import json
from pathlib import Path

import pytest

from leanbench.document import Document
from leanbench.verify import MODE_FULL, VerifyResult

PAGE_ONE = """Chapter 1. Divisibility

1.6 Divisibility in the Integers

Definition 1.6.1. Let a and b be integers. We say a divides b, written a | b,
if there exists an integer k such that b = a k.

Theorem 1.6.2. Let a, b and c be integers. If a divides b and a divides c,
then a divides b + c.

Proof. Write b = a k and c = a m. Then b + c = a (k + m). QED

Theorem 1.6.3. Let a and b be nonzero integers. Then the set of common
"""

PAGE_TWO = """divisors of a and b has a greatest element, the greatest common divisor.

Exercise 1.6.4. Show that if a divides b and b divides a, then a = b or a = -b.

Exercise 1.6.5. Prove that the sum of two odd integers is even.
"""


@pytest.fixture()
def two_page_book(tmp_path: Path) -> Document:
    path = tmp_path / "book.txt"
    path.write_text(PAGE_ONE + "\f" + PAGE_TWO, encoding="utf-8")
    return Document.load(path, title="Test Book")


class FakeChecker:
    """A Lean stand-in: fails anything containing ``BAD``, otherwise accepts."""

    def __init__(self) -> None:
        self.calls: list[str] = []

    def available(self) -> bool:
        return True

    def check(self, code: str, *, mode: str = MODE_FULL, imports=None) -> VerifyResult:
        self.calls.append(code)
        if "BAD" in code:
            return VerifyResult(False, mode, False, "LeanBenchCheck.lean:3:0: error: bad")
        return VerifyResult(True, mode, "sorry" in code, "")


@pytest.fixture()
def fake_checker() -> FakeChecker:
    return FakeChecker()


def detection_reply(items: list[dict]) -> str:
    return json.dumps({"items": items})


def formalize_reply(**overrides) -> str:
    payload = {
        "skip": False,
        "reason": "",
        "imports": ["Mathlib"],
        "name": "test_decl",
        "lean_code": "theorem test_decl (a b : Int) (h : a ∣ b) : a ∣ b := by\n  sorry",
        "has_proof": False,
        "informal": "a divides b",
        "index_types": ["Int"],
        "confidence": 0.8,
    }
    payload.update(overrides)
    return json.dumps(payload)