"""Cheap static checks for formalizations that compile and are probably wrong.

These are a baseline for the fidelity filter, not a replacement for one: each looks
at the projected roles and the text of the declaration only, with no model and no
Lean. They catch encoding hazards (natural-number subtraction, integer division),
binders the statement never uses, and goals that say nothing.
"""
from __future__ import annotations

import re

from .project import Projection
from .schema import KIND_FACT, KIND_GOAL, KIND_OBJECT

_NAT = re.compile(r"\b(ℕ|Nat)\b")
_OTHER_NUMBERS = re.compile(r"[ℤℚℝℂ]|\b(Int|Rat|Real|Complex)\b")
_SUBTRACTION = re.compile(r"[\w)\]]\s*-\s*[\w(]")
_DIVISION = re.compile(r"[\w)\]]\s*/\s*[\w(]")
_IDENT = re.compile(r"[A-Za-z_][A-Za-z0-9_']*")


def lint(projection: Projection) -> list[str]:
    findings: list[str] = []
    if projection.degenerate:
        findings.append("degenerate")
    texts = [r.type_text for r in projection.roles if r.kind in (KIND_FACT, KIND_GOAL)]
    body = " ".join(texts)
    declared = " ".join(r.type_text for r in projection.roles if r.kind == KIND_OBJECT)

    for role in projection.roles:
        if role.kind != KIND_OBJECT or role.attrs.get("binder_kind") != "explicit":
            continue
        if role.type_text.strip().startswith(("Type", "Sort")):
            continue  # a carrier: used by the instances that constrain it
        used = set(_IDENT.findall(body)) | set(_IDENT.findall(declared.replace(role.type_text, "")))
        if role.name != "_" and role.name not in used:
            findings.append(f"unused_binder:{role.name}")

    nat_only = _NAT.search(declared + " " + body) and not _OTHER_NUMBERS.search(declared + body)
    if nat_only and _SUBTRACTION.search(body):
        findings.append("nat_subtraction")
    if (_NAT.search(declared) or re.search(r"\b(ℤ|Int)\b", declared)) and _DIVISION.search(body):
        findings.append("integer_division")

    goal = next((r for r in projection.roles if r.kind == KIND_GOAL), None)
    if goal is not None and goal.type_text.strip() in ("", "True", "False", "1 = 1", "0 = 0"):
        findings.append("trivial_goal")
    return findings