from leanbench.project import classify, project
from leanbench.schema import KIND_FACT, KIND_GOAL, KIND_OBJECT, KIND_OWN


def roles(code):
    return {r.name: r for r in project(code).roles}


def test_objects_instances_and_goal():
    p = project(
        "theorem t (G : Type*) [Group G] [Fintype G] (g : G) : g ^ Fintype.card G = 1 := by sorry"
    )
    got = {r.name: r for r in p.roles}
    assert list(got) == ["G", "g", "goal"]
    assert got["G"].kind == KIND_OBJECT
    assert got["G"].attrs["instances"] == ["Group G", "Fintype G"]
    assert got["goal"].kind == KIND_GOAL
    assert not p.degenerate
    assert p.simplex is not None and len(p.simplex.roles) == 3


def test_hypothesis_binders_become_facts():
    got = roles("theorem t (n : ℕ) (a : ℤ) (h : Nat.Coprime a n) : a ≡ 1 [ZMOD n] := by sorry")
    assert got["h"].kind == KIND_FACT
    assert got["h"].attrs["classified_by"] == "predicate"
    assert got["n"].kind == KIND_OBJECT


def test_relation_symbols_mark_a_fact():
    got = roles("theorem t (a b : ℤ) (hab : a ∣ b) (hpos : 0 < a) : a ≤ b := by sorry")
    assert got["hab"].kind == KIND_FACT and got["hpos"].kind == KIND_FACT
    assert got["a"].kind == KIND_OBJECT


def test_function_type_is_data_not_a_fact():
    kind, how = classify("ℕ → ℕ", ["f"], set())
    assert kind == KIND_OBJECT and how == "default"
    assert classify("Type*", ["G"], set()) == (KIND_OBJECT, "sort")


def test_leading_forall_is_lifted_so_both_spellings_agree():
    a = project("theorem t (n : ℕ) : n = n := by rfl")
    b = project("theorem t : ∀ n : ℕ, n = n := by rfl")
    assert [(r.name, r.kind) for r in a.roles] == [(r.name, r.kind) for r in b.roles]
    assert {r.attrs.get("origin") for r in b.roles if r.name == "n"} == {"forall_in_goal"}


def test_goal_implication_splits_into_premises():
    got = roles("theorem t : ∀ n m : ℕ, n < m → m < 10 → n < 10 := by omega")
    assert [n for n in got if n.startswith("premise")] == ["premise1", "premise2"]
    assert got["goal"].type_text == "n < 10"


def test_bounded_forall_adds_an_object_and_a_fact():
    got = roles("theorem t : ∀ x ∈ S, f x = 0 := by sorry")
    assert got["x"].kind == KIND_OBJECT and got["h_x"].kind == KIND_FACT


def test_definition_has_an_own_role():
    p = project("def divides (a b : Int) : Prop := ∃ k, b = a * k")
    assert p.by_kind(KIND_OWN)[0].type_text == "Prop"
    assert [r.name for r in p.roles] == ["a", "b", "own"]


def test_structure_stops_at_where_and_ignores_extends():
    p = project("structure Ring (R : Type*) extends AddCommGroup R, Mul R where\n  x : R")
    assert [r.name for r in p.roles] == ["R", "own"]


def test_bare_statement_is_degenerate_not_an_error():
    p = project("theorem t : 2 + 2 = 4 := by norm_num")
    assert p.degenerate and p.simplex is None
    assert [r.name for r in p.roles] == ["goal"]


def test_no_declaration():
    p = project("-- just a comment")
    assert p.degenerate and p.notes == ["no declaration found"]


def test_instance_without_target_is_noted():
    p = project("theorem t (n : ℕ) [Fact (1 < 2)] : n = n := by rfl")
    assert any("constrains no named object" in n for n in p.notes)


def test_duplicate_names_are_aliased():
    p = project("theorem t (h : 0 < 1) (h : 1 < 2) : True := by trivial")
    assert p.simplex is not None
    assert "h" in p.simplex.roles and "h_2" in p.simplex.roles


def test_comments_and_proof_body_are_ignored():
    code = "/- doc -/\ntheorem t (n : ℕ) : n = n := by\n  -- (x : T) here is noise\n  rfl"
    assert [r.name for r in project(code).roles] == ["n", "goal"]