"""Tiny trusted kernel: Fitch-style natural deduction for propositional logic.

The kernel is the only thing a result depends on. It is deliberately small
(no tactics, no search, no automation): it parses a proof and checks each line
against one inference rule. A proof is accepted only if every line checks, all
subproofs are closed, and the last line at depth 0 is exactly the goal.

Proof format, one step per line:
    <n>. <bars> <formula>   <rule> [refs]
where <bars> is zero or more '|' marking subproof depth, e.g.
    1. | p & q          assume
    2. | p              andE1 1
    3. p & q -> p       impI 1-2

Formulas: atoms are lowercase identifiers, F is falsum, ~ not, & and, | or,
-> implies (right-assoc). Precedence: ~ > & > | > ->.
"""
from __future__ import annotations
import re
from dataclasses import dataclass

# ---------------------------------------------------------------- formulas
# A formula is a tuple: ('atom', name) | ('F',) | ('not', a) | ('and', a, b)
# | ('or', a, b) | ('imp', a, b)

TOK = re.compile(r"\s*(->|[()~&|]|F\b|[a-z][a-z0-9_]*)")


class ParseError(Exception):
    pass


def parse(s: str):
    toks, pos = [], 0
    s = s.replace("→", "->").replace("¬", "~").replace("∧", "&").replace("∨", "|").replace("⊥", "F")
    while pos < len(s):
        if s[pos:].strip() == "":
            break
        m = TOK.match(s, pos)
        if not m:
            raise ParseError(f"bad token at '{s[pos:pos+10]}'")
        toks.append(m.group(1))
        pos = m.end()
    i = 0

    def peek():
        return toks[i] if i < len(toks) else None

    def eat(t=None):
        nonlocal i
        if i >= len(toks) or (t and toks[i] != t):
            raise ParseError(f"expected {t or 'token'} in '{s}'")
        i += 1
        return toks[i - 1]

    def imp():
        a = orr()
        if peek() == "->":
            eat("->")
            return ("imp", a, imp())
        return a

    def orr():
        a = andd()
        while peek() == "|":
            eat("|")
            a = ("or", a, andd())
        return a

    def andd():
        a = unary()
        while peek() == "&":
            eat("&")
            a = ("and", a, unary())
        return a

    def unary():
        t = peek()
        if t == "~":
            eat("~")
            return ("not", unary())
        if t == "(":
            eat("(")
            a = imp()
            eat(")")
            return a
        if t == "F":
            eat()
            return ("F",)
        if t and re.fullmatch(r"[a-z][a-z0-9_]*", t):
            eat()
            return ("atom", t)
        raise ParseError(f"unexpected '{t}' in '{s}'")

    f = imp()
    if i != len(toks):
        raise ParseError(f"trailing input in '{s}'")
    return f


def show(f) -> str:
    k = f[0]
    if k == "atom":
        return f[1]
    if k == "F":
        return "F"
    if k == "not":
        a = f[1]
        return "~" + (show(a) if a[0] in ("atom", "F", "not") else f"({show(a)})")
    op = {"and": " & ", "or": " | ", "imp": " -> "}[k]
    prec = {"and": 3, "or": 2, "imp": 1}

    def side(x, right):
        if x[0] in prec and (prec[x[0]] < prec[k] or (prec[x[0]] == prec[k] and (k == "imp") != right)):
            return f"({show(x)})"
        return show(x)

    return side(f[1], False) + op + side(f[2], True)


def atoms(f, acc=None):
    acc = set() if acc is None else acc
    if f[0] == "atom":
        acc.add(f[1])
    for x in f[1:]:
        if isinstance(x, tuple):
            atoms(x, acc)
    return acc


def evaluate(f, v) -> bool:
    k = f[0]
    if k == "atom":
        return v[f[1]]
    if k == "F":
        return False
    if k == "not":
        return not evaluate(f[1], v)
    a, b = evaluate(f[1], v), evaluate(f[2], v)
    return {"and": a and b, "or": a or b, "imp": (not a) or b}[k]


def tautology(f) -> bool:
    """Classical truth-table check — used only to audit the kernel (soundness)."""
    names = sorted(atoms(f))
    for m in range(1 << len(names)):
        if not evaluate(f, {n: bool(m >> i & 1) for i, n in enumerate(names)}):
            return False
    return True


# ---------------------------------------------------------------- proofs
LINE = re.compile(r"^\s*(\d+)\s*[.:)]\s*((?:\|\s*)*)(.*?)\s{2,}([A-Za-z0-9_]+)\s*([\d\s,\-]*)$")
LINE_LOOSE = re.compile(r"^\s*(\d+)\s*[.:)]\s*((?:\|\s*)*)(.*\S)\s+([A-Za-z][A-Za-z0-9_]*)\s*([\d\s,\-]*)$")
RULES = {"assume", "reit", "andI", "andE1", "andE2", "orI1", "orI2", "orE", "impI", "impE",
         "notI", "notE", "botE", "dne"}


class ProofError(Exception):
    pass


@dataclass
class Step:
    n: int
    depth: int
    f: tuple
    rule: str
    refs: list
    scope: tuple  # ids of the subproofs (innermost last) that contain this line


LENIENT = False  # ablation: accept either reference order for notE / impE


def steps_of(proof: str):
    """Checked steps of a proof (no goal), for the semantic audit."""
    return _check(proof, None)


def check(proof: str, goal) -> tuple[bool, str]:
    """Return (ok, message). message names the first failing line."""
    try:
        _check(proof, goal)
        return True, "QED"
    except (ProofError, ParseError) as e:
        return False, str(e)


def _check(proof: str, goal):
    steps: list[Step] = []
    scope: tuple = ()       # currently open subproof ids
    opened: dict = {}       # subproof id -> (first line, depth, parent scope)
    last_in: dict = {}      # subproof id -> last line number directly inside it
    lines = [l for l in proof.strip().splitlines() if l.strip() and not l.strip().startswith("#")]
    if not lines:
        raise ProofError("empty proof")
    for raw in lines:
        m = LINE.match(raw) or LINE_LOOSE.match(raw)
        if not m:
            raise ProofError(f"cannot read line: '{raw.strip()[:60]}' (format: 'n. | formula  rule refs')")
        n, bars, ftxt, rule, reftxt = m.groups()
        n, depth = int(n), bars.count("|")
        where = f"line {n}"
        if n != len(steps) + 1:
            raise ProofError(f"{where}: lines must be numbered 1, 2, 3, ... (expected {len(steps)+1})")
        if rule not in RULES:
            raise ProofError(f"{where}: unknown rule '{rule}'")
        try:
            f = parse(ftxt)
        except ParseError as e:
            raise ProofError(f"{where}: {e}")
        refs = []
        for part in [p for p in re.split(r"[\s,]+", reftxt.strip()) if p]:
            if "-" in part:
                a, b = part.split("-", 1)
                if not a.isdigit() or not b.isdigit():
                    raise ProofError(f"{where}: bad range '{part}'")
                refs.append((int(a), int(b)))
            else:
                refs.append(int(part))
        # depth / scope bookkeeping
        if rule == "assume":
            if depth < 1 or depth > len(scope) + 1:
                raise ProofError(f"{where}: an assumption opens a subproof one level deeper (depth {len(scope)+1} or less, at least 1), got {depth}")
            scope = scope[: depth - 1] + (n,)
            opened[n] = (n, depth, scope[:-1])
        else:
            if depth > len(scope):
                raise ProofError(f"{where}: depth {depth} but only {len(scope)} subproof(s) open — open a subproof with 'assume'")
            scope = scope[:depth]
        st = Step(n, depth, f, rule, refs, scope)
        if scope:
            last_in[scope[-1]] = n  # line n sits directly in the innermost open subproof
        _rule(st, steps, opened, last_in, where)
        steps.append(st)
    final = steps[-1]
    if final.depth != 0:
        raise ProofError(f"proof ends inside a subproof (line {final.n}); close it with impI/notI/orE")
    if goal is not None and final.f != goal:
        raise ProofError(f"last line proves '{show(final.f)}', goal is '{show(goal)}'")
    return steps


def _rule(st: Step, steps, opened, last_in, where):
    def line(i):
        if not isinstance(i, int):
            raise ProofError(f"{where}: expected a line number, got range {i[0]}-{i[1]}")
        if not 1 <= i < st.n:
            raise ProofError(f"{where}: reference {i} is not an earlier line")
        s = steps[i - 1]
        if s.scope != st.scope[: len(s.scope)]:
            raise ProofError(f"{where}: line {i} is inside a closed subproof and cannot be used here")
        return s.f

    def sub(r):
        if not isinstance(r, tuple):
            raise ProofError(f"{where}: expected a subproof range like 3-5, got {r}")
        a, b = r
        if a not in opened or not (1 <= b < st.n):
            raise ProofError(f"{where}: {a}-{b} is not a subproof (it must start at an 'assume' line)")
        _, d, parent = opened[a]
        if a in st.scope:
            raise ProofError(f"{where}: subproof {a}-{b} is still open; this line must be one level shallower")
        if parent != st.scope[: len(parent)] or len(parent) != len(st.scope):
            raise ProofError(f"{where}: subproof {a}-{b} is not directly inside the current scope")
        if last_in.get(a) != b:
            raise ProofError(f"{where}: subproof starting at {a} ends at line {last_in.get(a)}, not {b}")
        return steps[a - 1].f, steps[b - 1].f

    f, r, R = st.f, st.rule, st.refs

    def need(k):
        if len(R) != k:
            raise ProofError(f"{where}: {r} takes {k} reference(s), got {len(R)}")

    def bad(msg):
        raise ProofError(f"{where}: {r} does not justify '{show(f)}' — {msg}")

    if r == "assume":
        need(0)
    elif r == "reit":
        need(1)
        if line(R[0]) != f:
            bad("reit must repeat the referenced formula exactly")
    elif r == "andI":
        need(2)
        if f != ("and", line(R[0]), line(R[1])):
            bad("expected the conjunction of the two referenced lines, in order")
    elif r in ("andE1", "andE2"):
        need(1)
        a = line(R[0])
        if a[0] != "and" or a[1 if r == "andE1" else 2] != f:
            bad("referenced line must be A & B; andE1 gives A, andE2 gives B")
    elif r in ("orI1", "orI2"):
        need(1)
        a = line(R[0])
        if f[0] != "or" or f[1 if r == "orI1" else 2] != a:
            bad("orI1 turns A into A | B, orI2 turns B into A | B")
    elif r == "orE":
        need(3)
        d = line(R[0])
        (h1, c1), (h2, c2) = sub(R[1]), sub(R[2])
        if d[0] != "or" or h1 != d[1] or h2 != d[2] or c1 != f or c2 != f:
            bad("needs A | B, a subproof A..C and a subproof B..C, concluding C")
    elif r == "impI":
        need(1)
        h, c = sub(R[0])
        if f != ("imp", h, c):
            bad("subproof assuming A and ending in B gives A -> B")
    elif r == "impE":
        need(2)
        a, b = line(R[0]), line(R[1])
        if a != ("imp", b, f) and not (LENIENT and b == ("imp", a, f)):
            bad("needs A -> B (first ref) and A (second ref)")
    elif r == "notI":
        need(1)
        h, c = sub(R[0])
        if c != ("F",) or f != ("not", h):
            bad("subproof assuming A and ending in F gives ~A")
    elif r == "notE":
        need(2)
        a, b = line(R[0]), line(R[1])
        if f != ("F",) or (b != ("not", a) and not (LENIENT and a == ("not", b))):
            bad("needs A (first ref) and ~A (second ref), concludes F")
    elif r == "botE":
        need(1)
        if line(R[0]) != ("F",):
            bad("referenced line must be F")
    elif r == "dne":
        need(1)
        if line(R[0]) != ("not", ("not", f)):
            bad("referenced line must be ~~A, concluding A")