"""``logic-kernel@v1`` π* — propositional-logic CNF canonicalizer.

Domain: ``logic``. Implements SQD whitepaper §14.3's proof-object
canonicalizer at the propositional level: parse a Boolean expression
over named atoms, convert to **canonical Conjunctive Normal Form**
(CNF), serialize as a deterministic string.

Algorithm
---------
1. Tokenize using the same lexer as
   :func:`bench.batteries.b_5t._eval_propositional` (AND/OR/NOT/
   XOR/IMPL/IFF + parens + uppercase atom names).
2. Parse via recursive descent → AST.
3. Eliminate IMPL/IFF/XOR by rewriting:

   - ``A IMPL B``  →  ``(NOT A) OR B``
   - ``A IFF B``   →  ``((NOT A) OR B) AND ((NOT B) OR A)``
   - ``A XOR B``   →  ``(A OR B) AND ((NOT A) OR (NOT B))``

4. Push NOT inward (De Morgan + double-negation elimination):

   - ``NOT (A AND B)``  →  ``(NOT A) OR (NOT B)``
   - ``NOT (A OR B)``   →  ``(NOT A) AND (NOT B)``
   - ``NOT NOT A``      →  ``A``

5. Distribute OR over AND until CNF.
6. Within each clause: dedupe + sort literals by ``(name, negated)``.
7. Detect tautological clauses (contains both ``A`` and ``NOT A``)
   → drop the clause (it's always true).
8. Detect contradiction (clause ``A AND NOT A`` after step 6 yields
   the empty disjunction → unsatisfiable). Surface as a special
   canonical form ``"FALSE"``.
9. Detect tautology (no clauses left after step 7) → ``"TRUE"``.
10. Sort clauses lexically by literal-tuple representation; dedupe.
11. Serialize as ``(L1 OR L2) AND (L3 OR L4) AND ...``.

Equivalence classes preserved
-----------------------------
- Commutativity: ``A AND B`` ≡ ``B AND A``
- Associativity: ``(A AND B) AND C`` ≡ ``A AND (B AND C)``
- IMPL/IFF/XOR rewrites: ``A IMPL B`` ≡ ``NOT A OR B``
- De Morgan's: ``NOT (A AND B)`` ≡ ``(NOT A) OR (NOT B)``
- Double negation: ``NOT NOT A`` ≡ ``A``
- Distribution: ``A OR (B AND C)`` ≡ ``(A OR B) AND (A OR C)``
- Tautology collapse: ``A OR NOT A`` ≡ ``TRUE``
- Idempotence: ``A AND A`` ≡ ``A``

Equivalence classes kept distinct
---------------------------------
- Different atom sets: ``A AND B`` ≢ ``A AND C``
- Logically distinct: ``A AND B`` ≢ ``A OR B``

Round-trip property
-------------------
Idempotent on its own output: re-canonicalizing the canonical form
yields the same bytes (CNF is closed under the algorithm).

Versioning
----------
``logic-kernel@v1`` pins this algorithm. CNF blow-up bound: input
expressions with N atoms can produce up to 2^N clauses. v1 caps
at N=8 (256 clauses) to keep canonicalization deterministic in
bounded time; raises :class:`PiStarError` on excess.

Source: ticket #000015 §1.7 declared the stub. This commit
graduates it. Closes the math/logic-kernel half of the 2026-05-08
fox roadmap note alongside ``arithmetic@v1``.
"""

from __future__ import annotations

from dataclasses import dataclass
from typing import Optional

from arborist.pi_star.protocol import PiStarError
from arborist.pi_star.registry import register


_MAX_ATOMS = 8


@dataclass
class LogicKernelV1:
    name: str = "logic-kernel"
    version: str = "v1"
    domain: str = "logic"

    def canonicalize(self, raw: bytes) -> bytes:
        if not isinstance(raw, (bytes, bytearray)):
            raise PiStarError(
                "logic-kernel@v1 expects bytes; got "
                f"{type(raw).__name__}"
            )
        try:
            source = raw.decode("utf-8", errors="surrogatepass")
        except UnicodeDecodeError as exc:  # pragma: no cover
            raise PiStarError(f"input not valid UTF-8: {exc}") from exc
        source = source.strip()
        if not source:
            raise PiStarError("logic-kernel@v1 input is empty")

        tokens = _tokenize(source)
        atoms = sorted({t for t in tokens if _is_atom(t)})
        if len(atoms) > _MAX_ATOMS:
            raise PiStarError(
                f"logic-kernel@v1 caps atoms at {_MAX_ATOMS}; "
                f"got {len(atoms)} ({atoms})"
            )
        ast = _parse(tokens)
        ast = _eliminate(ast)
        ast = _push_not(ast)
        clauses = _to_cnf(ast)
        # Each clause is a frozenset of (atom, negated) literals.
        canonical_clauses = []
        for clause in clauses:
            # Drop tautological clauses (A and NOT A both present).
            atoms_present = {a for (a, _) in clause}
            tautology = any(
                (a, False) in clause and (a, True) in clause
                for a in atoms_present
            )
            if tautology:
                continue
            canonical_clauses.append(tuple(sorted(clause)))
        # Dedupe clauses.
        canonical_clauses = sorted(set(canonical_clauses))
        if not canonical_clauses:
            return b"TRUE"
        # Empty clause = contradiction.
        if any(len(c) == 0 for c in canonical_clauses):
            return b"FALSE"
        return _serialize(canonical_clauses).encode("utf-8")


# ---------------------------------------------------------------------
# Tokenizer (identical surface to b_5t._tokenize_propositional)
# ---------------------------------------------------------------------


def _tokenize(expr: str) -> list[str]:
    out: list[str] = []
    i = 0
    while i < len(expr):
        c = expr[i]
        if c.isspace():
            i += 1
            continue
        if c in "()":
            out.append(c)
            i += 1
            continue
        if c.isalpha():
            j = i
            while j < len(expr) and expr[j].isalpha():
                j += 1
            tok = expr[i:j]
            up = tok.upper()
            if up in ("AND", "OR", "NOT", "XOR", "IMPL", "IFF", "TRUE", "FALSE"):
                out.append(up)
            elif len(tok) == 1:
                out.append(tok.upper())
            else:
                raise PiStarError(f"unrecognized token: {tok!r}")
            i = j
            continue
        raise PiStarError(f"unexpected char: {c!r}")
    return out


def _is_atom(token: str) -> bool:
    return len(token) == 1 and token.isupper() and token.isalpha()


# ---------------------------------------------------------------------
# Parser (recursive descent → tuple-AST)
#
# Returned shape:
#   ('atom', name)
#   ('not', child)
#   ('and', left, right)
#   ('or', left, right)
#   ('impl', left, right)
#   ('iff', left, right)
#   ('xor', left, right)
#   ('true',)
#   ('false',)
#
# Tuple form keeps the kernel pure-functional and easy to pattern-match.
# ---------------------------------------------------------------------


def _parse(tokens: list[str]) -> tuple:
    pos = [0]

    def peek() -> Optional[str]:
        return tokens[pos[0]] if pos[0] < len(tokens) else None

    def expect(t: str) -> None:
        if peek() != t:
            raise PiStarError(f"expected {t!r} at {pos[0]}, got {peek()!r}")
        pos[0] += 1

    def parse_atom() -> tuple:
        t = peek()
        if t is None:
            raise PiStarError("unexpected end of expression")
        if t == "(":
            pos[0] += 1
            v = parse_or()
            expect(")")
            return v
        if t == "NOT":
            pos[0] += 1
            return ("not", parse_atom())
        if t == "TRUE":
            pos[0] += 1
            return ("true",)
        if t == "FALSE":
            pos[0] += 1
            return ("false",)
        if _is_atom(t):
            pos[0] += 1
            return ("atom", t)
        raise PiStarError(f"unexpected token {t!r}")

    def parse_and() -> tuple:
        left = parse_atom()
        while peek() == "AND":
            pos[0] += 1
            right = parse_atom()
            left = ("and", left, right)
        return left

    def parse_or() -> tuple:
        left = parse_and()
        while peek() in ("OR", "XOR", "IMPL", "IFF"):
            op = peek()
            pos[0] += 1
            right = parse_and()
            mapping = {"OR": "or", "XOR": "xor", "IMPL": "impl", "IFF": "iff"}
            left = (mapping[op], left, right)
        return left

    result = parse_or()
    if pos[0] != len(tokens):
        raise PiStarError(f"unconsumed tokens at {pos[0]}: {tokens[pos[0]:]!r}")
    return result


# ---------------------------------------------------------------------
# Eliminate IMPL/IFF/XOR → AND/OR/NOT only
# ---------------------------------------------------------------------


def _eliminate(node: tuple) -> tuple:
    if node[0] in ("atom", "true", "false"):
        return node
    if node[0] == "not":
        return ("not", _eliminate(node[1]))
    if node[0] in ("and", "or"):
        return (node[0], _eliminate(node[1]), _eliminate(node[2]))
    if node[0] == "impl":
        # A IMPL B  →  (NOT A) OR B
        a, b = _eliminate(node[1]), _eliminate(node[2])
        return ("or", ("not", a), b)
    if node[0] == "iff":
        # A IFF B  →  (NOT A OR B) AND (NOT B OR A)
        a, b = _eliminate(node[1]), _eliminate(node[2])
        return (
            "and",
            ("or", ("not", a), b),
            ("or", ("not", b), a),
        )
    if node[0] == "xor":
        # A XOR B  →  (A OR B) AND (NOT A OR NOT B)
        a, b = _eliminate(node[1]), _eliminate(node[2])
        return (
            "and",
            ("or", a, b),
            ("or", ("not", a), ("not", b)),
        )
    raise PiStarError(f"unknown node tag: {node[0]}")


# ---------------------------------------------------------------------
# Push NOT inward (NNF — Negation Normal Form)
# ---------------------------------------------------------------------


def _push_not(node: tuple) -> tuple:
    if node[0] in ("atom", "true", "false"):
        return node
    if node[0] == "not":
        inner = node[1]
        if inner[0] == "atom":
            return node
        if inner[0] == "true":
            return ("false",)
        if inner[0] == "false":
            return ("true",)
        if inner[0] == "not":
            # NOT NOT A → A
            return _push_not(inner[1])
        if inner[0] == "and":
            # NOT (A AND B) → (NOT A) OR (NOT B)
            return _push_not(("or", ("not", inner[1]), ("not", inner[2])))
        if inner[0] == "or":
            return _push_not(("and", ("not", inner[1]), ("not", inner[2])))
        raise PiStarError(f"unexpected tag inside NOT: {inner[0]}")
    if node[0] in ("and", "or"):
        return (node[0], _push_not(node[1]), _push_not(node[2]))
    raise PiStarError(f"unknown node tag in _push_not: {node[0]}")


# ---------------------------------------------------------------------
# Distribute OR over AND → CNF
#
# Produces a list of clauses (frozensets of literals).
# Each literal is (atom_name, negated).
# ---------------------------------------------------------------------


def _to_cnf(node: tuple) -> list[frozenset]:
    if node[0] == "true":
        return []  # TRUE = no constraints
    if node[0] == "false":
        return [frozenset()]  # empty clause = contradiction
    if node[0] == "atom":
        return [frozenset({(node[1], False)})]
    if node[0] == "not":
        if node[1][0] != "atom":
            raise PiStarError(
                f"_to_cnf expects NNF; got NOT around {node[1][0]}"
            )
        return [frozenset({(node[1][1], True)})]
    if node[0] == "and":
        return _to_cnf(node[1]) + _to_cnf(node[2])
    if node[0] == "or":
        # Distribute: OR of two CNFs = AND of pairwise-OR'd clauses.
        left = _to_cnf(node[1])
        right = _to_cnf(node[2])
        out = []
        for lc in left:
            for rc in right:
                out.append(lc | rc)
        return out
    raise PiStarError(f"unknown node tag in _to_cnf: {node[0]}")


# ---------------------------------------------------------------------
# Serialize sorted clauses as canonical text.
# ---------------------------------------------------------------------


def _serialize(clauses: list[tuple]) -> str:
    """Each clause is a sorted tuple of (atom, negated) literals."""

    def lit_str(lit):
        atom, neg = lit
        return f"NOT {atom}" if neg else atom

    parts = []
    for clause in clauses:
        if len(clause) == 1:
            parts.append(lit_str(clause[0]))
        else:
            parts.append("(" + " OR ".join(lit_str(l) for l in clause) + ")")
    return " AND ".join(parts)


register(LogicKernelV1())
