"""Read a Lean declaration's parameters as roles.

``project(code)`` is deterministic and never calls Lean or a model. It splits the
signature into

* **objects**   explicit/implicit binders whose type is data or a sort: ``(G : Type*)``,
                ``(n : ℕ)``; instance binders ``[Group G]`` attach to the object they
                constrain (``attrs["instances"]``);
* **facts**     binders whose type is a proposition: ``(h : a ∣ b)``, and, when the goal
                is an implication, its premises;
* **goal**      the conclusion of a theorem, or **own** for what a definition is.

Leading ``∀`` binders of the goal are unpacked into objects, so ``(n : ℕ) : n = n`` and
``∀ n : ℕ, n = n`` project to the same roles. Whether a binder is a fact is decided by
a syntactic heuristic (relation symbols, known predicate heads, the ``h…`` naming
convention) and every role records how it was decided in ``attrs["classified_by"]``,
so the heuristic's accuracy can be measured against a manual parse.
"""
from __future__ import annotations

import re
from dataclasses import dataclass, field
from typing import Any

from .schema import (
    KIND_FACT,
    KIND_GOAL,
    KIND_OBJECT,
    KIND_OWN,
    Role,
    Simplex,
)
from .typeindex import _DECL, _IDENT, PROOF_KEYWORDS, _split_top_level, _strip_comments

OPENERS = {"(": ")", "{": "}", "[": "]", "⦃": "⦄", "⟨": "⟩"}
CLOSERS = set(OPENERS.values())
BINDER_KIND = {"(": "explicit", "{": "implicit", "⦃": "strict_implicit", "[": "instance"}

_SORT = re.compile(r"^(Type|Sort)(\b|\*|_)")
_RELATION = re.compile(r"[=≠<>≤≥∣∈∉⊆⊂⊇⊃≡∧∨¬↔∀∃≃≅≈]|\bTrue\b|\bFalse\b")
_PROP_HEAD = re.compile(
    r"^(Is[A-Z]\w*|Nat\.Prime|Prime|Nat\.Coprime|Int\.Coprime|Coprime|Function\.\w+|"
    r"Injective|Surjective|Bijective|Continuous\w*|Differentiable\w*|Monotone\w*|Antitone\w*|"
    r"Finite|Set\.Finite|Set\.Infinite|Infinite|Odd|Even|Irreducible|Squarefree|"
    r"Nonempty|Set\.Nonempty|Nat\.Even|Nat\.Odd)\b"
)
_HYPOTHESIS_NAME = re.compile(r"^h[\w'₀-₉]*$")


def _split_depth0(text: str, separator: str) -> list[str]:
    """Split on ``separator`` outside every bracket pair."""
    parts: list[str] = []
    depth = 0
    start = 0
    for index, char in enumerate(text):
        if char in OPENERS:
            depth += 1
        elif char in CLOSERS:
            depth = max(0, depth - 1)
        elif depth == 0 and text.startswith(separator, index):
            parts.append(text[start:index])
            start = index + len(separator)
    parts.append(text[start:])
    return parts


def _first_depth0(text: str, needle: str) -> int:
    depth = 0
    for index, char in enumerate(text):
        if char in OPENERS:
            depth += 1
        elif char in CLOSERS:
            depth = max(0, depth - 1)
        elif depth == 0 and text.startswith(needle, index):
            if needle == ":" and text.startswith(":=", index):
                continue
            return index
    return -1


def classify(type_text: str, names: list[str], objects: set[str]) -> tuple[str, str]:
    """(kind, how) for a binder with these names and this type."""
    text = type_text.strip()
    if not text:
        return KIND_OBJECT, "untyped"
    if _SORT.match(text):
        return KIND_OBJECT, "sort"
    if _RELATION.search(text):
        return KIND_FACT, "relation"
    if _PROP_HEAD.match(text):
        return KIND_FACT, "predicate"
    if names and all(_HYPOTHESIS_NAME.match(n) for n in names):
        tokens = {t for t in _IDENT.findall(text) if t[:1].islower()}
        if tokens & objects:
            return KIND_FACT, "name"
    return KIND_OBJECT, "default"


@dataclass
class Projection:
    name: str
    keyword: str
    roles: list[Role] = field(default_factory=list)
    simplex: Simplex | None = None
    notes: list[str] = field(default_factory=list)

    @property
    def degenerate(self) -> bool:
        return self.simplex is None

    def by_kind(self, kind: str) -> list[Role]:
        return [r for r in self.roles if r.kind == kind]

    def as_dict(self) -> dict[str, Any]:
        return {
            "name": self.name,
            "keyword": self.keyword,
            "degenerate": self.degenerate,
            "roles": [r.as_dict() for r in self.roles],
            "notes": self.notes,
        }


def _cut_signature(rest: str) -> str:
    depth = 0
    for index, char in enumerate(rest):
        if char in OPENERS:
            depth += 1
        elif char in CLOSERS:
            depth = max(0, depth - 1)
        elif depth == 0:
            if rest.startswith(":=", index) or rest.startswith("\nwhere", index):
                return rest[:index]
            if rest.startswith(" where", index) and index > 0:
                return rest[:index]
    return rest


def _roles_from_group(opener: str, inner: str, objects: set[str], origin: str) -> list[Role]:
    binder_kind = BINDER_KIND.get(opener, "explicit")
    head, _, tail = inner.partition(":")
    names = head.split()
    type_text = tail.strip() if ":" in inner else ""
    if not names or any(not _IDENT.fullmatch(n) and n != "_" for n in names):
        return []
    kind, how = classify(type_text, names, objects)
    roles = []
    for name in names:
        attrs = {"binder_kind": binder_kind, "classified_by": how, "origin": origin}
        roles.append(Role(name, kind, type_text=type_text, attrs=attrs))
        if kind == KIND_OBJECT:
            objects.add(name)
    return roles


def _attach_instance(inner: str, roles: dict[str, Role], notes: list[str]) -> None:
    text = inner.split(":", 1)[1].strip() if ":" in inner else inner.strip()
    owner = None
    for token in _IDENT.findall(text):
        if token in roles and roles[token].kind == KIND_OBJECT:
            owner = roles[token]
    if owner is None:
        notes.append(f"instance [{text}] constrains no named object")
        return
    owner.attrs.setdefault("instances", []).append(text)


def _unpack_forall(goal: str, objects: set[str]) -> tuple[list[Role], str]:
    """Lift leading ``∀`` binders of the goal into object/fact roles."""
    lifted: list[Role] = []
    text = goal.strip()
    while text.startswith("∀"):
        body = text[1:].lstrip()
        comma = _first_depth0(body, ",")
        if comma < 0:
            break
        binders, text = body[:comma].strip(), body[comma + 1 :].strip()
        groups = _split_top_level(binders)
        if groups and binders.startswith(tuple(OPENERS)):
            for opener, inner in groups:
                lifted.extend(_roles_from_group(opener, inner, objects, "forall_in_goal"))
            continue
        bound = re.match(r"^([\w'₀-₉ ]+?)\s*(∈|∉|<|≤|>|≥|≠)\s*(.+)$", binders)
        if bound and ":" not in binders:
            for name in bound.group(1).split():
                lifted.append(Role(name, KIND_OBJECT, attrs={
                    "binder_kind": "explicit", "classified_by": "bounded", "origin": "forall_in_goal"}))
                objects.add(name)
                lifted.append(Role(
                    f"h_{name}", KIND_FACT, type_text=f"{name} {bound.group(2)} {bound.group(3)}",
                    attrs={"binder_kind": "explicit", "classified_by": "bounded",
                           "origin": "forall_in_goal"}))
            continue
        lifted.extend(_roles_from_group("(", binders, objects, "forall_in_goal"))
    return lifted, text


def project(code: str) -> Projection:
    clean = _strip_comments(code)
    match = _DECL.search(clean)
    if not match:
        return Projection("", "", notes=["no declaration found"])
    keyword, name = match.group(1), match.group(2)
    result = Projection(name, keyword)
    signature = _cut_signature(clean[match.end() :])

    colon = _first_depth0(signature, ":")
    binder_text = signature if colon < 0 else signature[:colon]
    goal_text = "" if colon < 0 else signature[colon + 1 :].strip()

    objects: set[str] = set()
    named: dict[str, Role] = {}
    instances: list[str] = []
    for opener, inner in _split_top_level(binder_text):
        if opener == "[":
            instances.append(inner)
            continue
        if opener == "⟨":
            continue
        for role in _roles_from_group(opener, inner, objects, "binder"):
            result.roles.append(role)
            named[role.name] = role
    for inner in instances:
        _attach_instance(inner, named, result.notes)

    if keyword in PROOF_KEYWORDS:
        lifted, goal_text = _unpack_forall(goal_text, objects)
        for role in lifted:
            result.roles.append(role)
            named[role.name] = role
        parts = _split_depth0(goal_text, "→") if goal_text else []
        if len(parts) >= 2:
            for index, premise in enumerate(parts[:-1], start=1):
                result.roles.append(Role(
                    f"premise{index}", KIND_FACT, type_text=premise.strip(),
                    attrs={"binder_kind": "goal_implication", "classified_by": "implication",
                           "origin": "goal"}))
            goal_text = parts[-1].strip()
        result.roles.append(Role(
            "goal", KIND_GOAL, type_text=goal_text,
            attrs={
                "exists_count": goal_text.count("∃"),
                "forall_count": goal_text.count("∀"),
                "is_iff": "↔" in goal_text,
            }))
    else:
        result.roles.append(Role(
            "own", KIND_OWN, type_text=goal_text or keyword, attrs={"keyword": keyword}))

    seen: dict[str, int] = {}
    aliased: dict[str, Role] = {}
    for role in result.roles:
        count = seen.get(role.name, 0) + 1
        seen[role.name] = count
        aliased[role.name if count == 1 else f"{role.name}_{count}"] = role
    if len(aliased) >= 2:
        result.simplex = Simplex(name, aliased)
    else:
        result.notes.append(f"degenerate: only {len(aliased)} role(s)")
    return result