from __future__ import annotations

from ragsolver.rag.ingest_mathlib import _should_exclude, record_to_chunk

CFG = {
    "doc_id": "mathlib-v4.28.0-rc1",
    "docs_url_base": "https://leanprover-community.github.io/mathlib4_docs",
    "exclude_kinds": ["instance"],
    "exclude_module_prefixes": ["Mathlib.Tactic", "Mathlib.Deprecated"],
    "exclude_name_substrings": [".proof_", ".match_", "_aux"],
    "exclude_name_regex": r"\.eq_(\d+|def)$",
}


def _record(**overrides) -> dict:
    base = {
        "name": ["Nat.Coprime"],
        "module_name": ["Mathlib", "Data", "Nat", "GCD", "Basic"],
        "type": "ℕ → ℕ → Prop",
        "kind": "def",
        "signature": "ℕ → ℕ → Prop",
        "value": "",
        "informal_name": "Coprimality",
        "informal_description": "Two naturals are coprime if their gcd is 1.",
    }
    base.update(overrides)
    return base


def test_excludes_instances():
    assert _should_exclude(_record(kind="instance"), CFG) is True
    assert _should_exclude(_record(kind="def"), CFG) is False


def test_excludes_tactic_and_deprecated_modules():
    assert _should_exclude(_record(module_name=["Mathlib", "Tactic", "Ring"]), CFG) is True
    assert _should_exclude(_record(module_name=["Mathlib", "Deprecated", "Foo"]), CFG) is True
    assert _should_exclude(_record(module_name=["Mathlib", "Data", "Nat"]), CFG) is False


def test_excludes_autogenerated_aux_names():
    assert _should_exclude(_record(name=["Nat.Coprime.proof_1"]), CFG) is True
    assert _should_exclude(_record(name=["Nat.Coprime.match_1"]), CFG) is True
    assert _should_exclude(_record(name=["Nat.Coprime_aux"]), CFG) is True
    assert _should_exclude(_record(name=["Nat.Coprime.eq_1"]), CFG) is True
    assert _should_exclude(_record(name=["Nat.Coprime"]), CFG) is False


def test_record_to_chunk_builds_expected_fields():
    chunk = record_to_chunk(_record(), CFG, mathlib_tag="v4.28.0-rc1", lean_version="leanprover/lean4:v4.28.0-rc1")
    assert chunk is not None
    assert chunk.chunk_id == "mathlib:Nat.Coprime:0"
    assert chunk.decl_name == "Nat.Coprime"
    assert chunk.module_path == "Mathlib.Data.Nat.GCD.Basic"
    assert chunk.corpus == "mathlib"
    assert chunk.unit_type == "mathlib_decl"
    assert "Coprimality" in chunk.text
    assert "Two naturals are coprime" in chunk.text
    assert chunk.docs_url == (
        "https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/GCD/Basic.html#Nat.Coprime"
    )
    assert chunk.embedding is None


def test_record_to_chunk_returns_none_without_name():
    assert record_to_chunk(_record(name=[]), CFG, "v4.28.0-rc1", "x") is None


def test_name_components_are_joined_into_the_full_declaration_name():
    """Regresión (docs/DECISIONS.md #31): en el JSONL de LeanSearch v2 `name` es la
    lista de componentes del nombre, no una lista de alias. Con `name[0]` el 90% de
    las declaraciones quedaba con nombre/chunk_id/docs_url incorrectos y repetidos."""
    chunk = record_to_chunk(_record(name=["GCDMonoid", "dvd_gcd"]), CFG, mathlib_tag="v4.28.0-rc1", lean_version="x")
    assert chunk.decl_name == "GCDMonoid.dvd_gcd"
    assert chunk.chunk_id == "mathlib:GCDMonoid.dvd_gcd:0"
    assert chunk.docs_url.endswith("#GCDMonoid.dvd_gcd")
    assert chunk.decl_names_alt == []
    assert _should_exclude(_record(name=["Nat", "Coprime", "proof_1"]), CFG) is True


def test_equation_lemmas_are_excluded_but_real_eq_lemmas_are_kept():
    for name, excluded in ((["Nat", "gcd", "eq_1"], True), (["Nat", "gcd", "eq_def"], True), (["Nat", "Prime", "eq_one_or_self_of_dvd"], False), (["eq_comm"], False)):
        assert _should_exclude(_record(name=name), CFG) is excluded, name