#!/usr/bin/env python3
"""Independent review audit for the regular-expression left-quotient result.

The construction side uses Antimirov partial derivatives.  The oracle side
uses a position (Glushkov) automaton computed from first, last, and follow
sets.  The oracle has no derivative or epsilon-transition machinery.

The script also checks the hostile unary family used to rule out every
uniformly bounded unfolding of the star quotient.
"""

from __future__ import annotations

import hashlib
import itertools
import json
from collections import defaultdict, deque
from functools import lru_cache
from pathlib import Path

ALPHABET = ("a", "b")
ZERO = ("zero",)
ONE = ("one",)

A_SOURCES = (
    "0", "1", "a", "b", "(a|b)", "(a.b)", "(b.a)", "(a)*", "(b)*",
    "((a|b))*", "((a)*.b)", "(a.(b)*)", "((a.b))*", "((b.a))*",
    "((a|b).a)", "(a.(a|b))", "((a.b)|(b.a))", "((a)*.(b)*)",
    "(((a)*.b))*", "(((a.b))*.a)", "((a.b)|1)", "((a|1).b)",
    "(((a.b)|1))*", "(((a|b))*.a.b)", "((a)*|(b)*)",
    "((a)*.b.(a)*)", "(((a|b).(a|b)))*",
)

B_SOURCES = (
    "0", "1", "a", "b", "(a|b)", "(a.b)", "(b.a)", "(a)*", "(b)*",
    "((a|b))*", "((a)*.b)", "(a.(b)*)", "((a.b))*", "((a.b)|1)",
    "((a)*.b.(a)*)",
)


class Parser:
    def __init__(self, source: str):
        self.source = source
        self.index = 0

    def peek(self):
        return self.source[self.index] if self.index < len(self.source) else None

    def take(self, expected=None):
        token = self.peek()
        if token is None or (expected is not None and token != expected):
            raise ValueError(f"expected {expected!r} at {self.index}: {self.source!r}")
        self.index += 1
        return token

    def parse(self):
        expression = self.parse_union()
        if self.peek() is not None:
            raise ValueError(f"trailing input at {self.index}: {self.source!r}")
        return expression

    def parse_union(self):
        expression = self.parse_concat()
        while self.peek() == "|":
            self.take("|")
            expression = ("alt", expression, self.parse_concat())
        return expression

    def parse_concat(self):
        expression = self.parse_postfix()
        while self.peek() == ".":
            self.take(".")
            expression = ("cat", expression, self.parse_postfix())
        return expression

    def parse_postfix(self):
        expression = self.parse_atom()
        while self.peek() == "*":
            self.take("*")
            expression = ("star", expression)
        return expression

    def parse_atom(self):
        token = self.peek()
        if token == "(":
            self.take("(")
            expression = self.parse_union()
            self.take(")")
            return expression
        self.take()
        if token == "0":
            return ZERO
        if token == "1":
            return ONE
        if token in ALPHABET:
            return ("lit", token)
        raise ValueError(f"unexpected {token!r}")


def parse(source: str):
    return Parser(source).parse()


def residual_cat(left, right):
    if left == ZERO or right == ZERO:
        return ZERO
    if left == ONE:
        return right
    if right == ONE:
        return left
    return ("cat", left, right)


@lru_cache(maxsize=None)
def nullable(expression) -> bool:
    tag = expression[0]
    if tag in ("zero", "lit"):
        return False
    if tag in ("one", "star"):
        return True
    if tag == "alt":
        return nullable(expression[1]) or nullable(expression[2])
    if tag == "cat":
        return nullable(expression[1]) and nullable(expression[2])
    raise ValueError(tag)


@lru_cache(maxsize=None)
def partial(expression, letter: str):
    tag = expression[0]
    if tag in ("zero", "one"):
        return frozenset()
    if tag == "lit":
        return frozenset((ONE,)) if expression[1] == letter else frozenset()
    if tag == "alt":
        return partial(expression[1], letter) | partial(expression[2], letter)
    if tag == "cat":
        left, right = expression[1], expression[2]
        result = {residual_cat(item, right) for item in partial(left, letter)}
        result.discard(ZERO)
        if nullable(left):
            result.update(partial(right, letter))
        return frozenset(result)
    if tag == "star":
        loop = expression
        return frozenset(
            item
            for item in (residual_cat(step, loop) for step in partial(expression[1], letter))
            if item != ZERO
        )
    raise ValueError(tag)


def partial_carrier(start):
    states = {start}
    edges = {}
    queue = deque((start,))
    while queue:
        state = queue.popleft()
        for letter in ALPHABET:
            targets = partial(state, letter)
            edges[(state, letter)] = targets
            for target in targets:
                if target not in states:
                    states.add(target)
                    queue.append(target)
    return states, edges


def compose(left, right):
    by_middle = defaultdict(set)
    for middle, target in right:
        by_middle[middle].add(target)
    return {
        (source, target)
        for source, middle in left
        for target in by_middle.get(middle, ())
    }


def closure(relation, states):
    result = set(relation) | {(state, state) for state in states}
    changed = True
    while changed:
        expanded = result | compose(result, result)
        changed = expanded != result
        result = expanded
    return result


def relation_semantics(expression, states, edges):
    identity = {(state, state) for state in states}

    @lru_cache(maxsize=None)
    def interpret(node):
        tag = node[0]
        if tag == "zero":
            return frozenset()
        if tag == "one":
            return frozenset(identity)
        if tag == "lit":
            return frozenset(
                (state, target)
                for state in states
                for target in edges[(state, node[1])]
            )
        if tag == "alt":
            return interpret(node[1]) | interpret(node[2])
        if tag == "cat":
            return frozenset(compose(interpret(node[1]), interpret(node[2])))
        if tag == "star":
            return frozenset(closure(interpret(node[1]), states))
        raise ValueError(tag)

    return interpret(expression)


def antimirov_prepare(a_expression, b_expression):
    states, edges = partial_carrier(b_expression)
    relation = relation_semantics(a_expression, states, edges)
    residuals = frozenset(target for source, target in relation if source == b_expression)
    return residuals, len(states)


def antimirov_accepts(residuals, suffix: str):
    current = residuals
    for letter in suffix:
        current = frozenset(target for state in current for target in partial(state, letter))
    return any(nullable(state) for state in current)


def linearize(expression, counter, symbols):
    tag = expression[0]
    if tag == "lit":
        position = next(counter)
        symbols[position] = expression[1]
        return ("pos", position)
    if tag in ("zero", "one"):
        return expression
    if tag in ("alt", "cat"):
        return (tag, linearize(expression[1], counter, symbols), linearize(expression[2], counter, symbols))
    if tag == "star":
        return (tag, linearize(expression[1], counter, symbols))
    raise ValueError(tag)


def merge_follow(*maps):
    result = defaultdict(set)
    for mapping in maps:
        for source, targets in mapping.items():
            result[source].update(targets)
    return result


def position_info(expression):
    tag = expression[0]
    if tag == "zero":
        return False, set(), set(), defaultdict(set)
    if tag == "one":
        return True, set(), set(), defaultdict(set)
    if tag == "pos":
        position = expression[1]
        return False, {position}, {position}, defaultdict(set)
    if tag == "alt":
        ln, lf, ll, lfollow = position_info(expression[1])
        rn, rf, rl, rfollow = position_info(expression[2])
        return ln or rn, lf | rf, ll | rl, merge_follow(lfollow, rfollow)
    if tag == "cat":
        ln, lf, ll, lfollow = position_info(expression[1])
        rn, rf, rl, rfollow = position_info(expression[2])
        follow = merge_follow(lfollow, rfollow)
        for position in ll:
            follow[position].update(rf)
        first = lf | rf if ln else lf
        last = rl | ll if rn else rl
        return ln and rn, first, last, follow
    if tag == "star":
        _, first, last, follow = position_info(expression[1])
        for position in last:
            follow[position].update(first)
        return True, first, last, follow
    raise ValueError(tag)


def glushkov_compile(expression):
    symbols = {}
    positioned = linearize(expression, itertools.count(1), symbols)
    is_nullable, first, last, follow = position_info(positioned)
    transitions = defaultdict(set)
    for target in first:
        transitions[(0, symbols[target])].add(target)
    for source, targets in follow.items():
        for target in targets:
            transitions[(source, symbols[target])].add(target)
    finals = set(last)
    if is_nullable:
        finals.add(0)
    return transitions, frozenset(finals), len(symbols) + 1


def glushkov_prepare(a_expression, b_expression):
    a_transitions, a_finals, _ = glushkov_compile(a_expression)
    b_transitions, b_finals, _ = glushkov_compile(b_expression)
    reachable = {(0, 0)}
    queue = deque(((0, 0),))
    while queue:
        a_state, b_state = queue.popleft()
        for letter in ALPHABET:
            for target in itertools.product(
                a_transitions[(a_state, letter)],
                b_transitions[(b_state, letter)],
            ):
                if target not in reachable:
                    reachable.add(target)
                    queue.append(target)
    b_starts = frozenset(b_state for a_state, b_state in reachable if a_state in a_finals)
    return b_transitions, b_finals, b_starts, len(reachable)


def glushkov_accepts(prepared, suffix: str):
    transitions, finals, starts, _ = prepared
    current = starts
    for letter in suffix:
        current = frozenset(
            target for state in current for target in transitions[(state, letter)]
        )
    return any(state in finals for state in current)


def words_up_to(maximum_length: int):
    return [
        "".join(letters)
        for length in range(maximum_length + 1)
        for letters in itertools.product(ALPHABET, repeat=length)
    ]


def check_unbounded_star(maximum_k: int):
    failures = []
    for k in range(maximum_k + 1):
        target = "a" * (k + 1)
        truncated_residuals = {
            target[len(prefix):]
            for i in range(k + 1)
            for prefix in ("a" * i,)
            if target.startswith(prefix)
        }
        full_residuals = truncated_residuals | {""}
        if "" in truncated_residuals or "" not in full_residuals:
            failures.append(k)
    return failures


def main() -> int:
    a_expressions = tuple(parse(source) for source in A_SOURCES)
    b_expressions = tuple(parse(source) for source in B_SOURCES)
    suffixes = words_up_to(4)
    transcript = hashlib.sha256()
    mismatches = []
    maximum_carrier = 0
    maximum_product = 0

    for a_index, a_expression in enumerate(a_expressions):
        for b_index, b_expression in enumerate(b_expressions):
            residuals, carrier_size = antimirov_prepare(a_expression, b_expression)
            oracle = glushkov_prepare(a_expression, b_expression)
            maximum_carrier = max(maximum_carrier, carrier_size)
            maximum_product = max(maximum_product, oracle[3])
            for suffix in suffixes:
                construction = antimirov_accepts(residuals, suffix)
                expected = glushkov_accepts(oracle, suffix)
                transcript.update(
                    f"{a_index}:{b_index}:{suffix}:{int(construction)}:{int(expected)}\n".encode()
                )
                if construction != expected:
                    mismatches.append({
                        "a_index": a_index,
                        "b_index": b_index,
                        "suffix": suffix,
                        "antimirov": construction,
                        "glushkov": expected,
                    })

    prior = json.loads(
        (Path(__file__).parents[1] / "left-quotient-regular-expressions" / "certificate.json").read_text()
    )
    digest = transcript.hexdigest()
    star_failures = check_unbounded_star(64)
    certificate = {
        "certificate_type": "fprd-result-review-left-quotient.v1",
        "alphabet": list(ALPHABET),
        "quotienting_expressions": len(a_expressions),
        "target_expressions": len(b_expressions),
        "expression_pairs": len(a_expressions) * len(b_expressions),
        "suffixes": len(suffixes),
        "maximum_suffix_length": 4,
        "membership_comparisons": len(a_expressions) * len(b_expressions) * len(suffixes),
        "mismatch_count": len(mismatches),
        "maximum_antimirov_carrier_states": maximum_carrier,
        "maximum_glushkov_product_states": maximum_product,
        "transcript_sha256": digest,
        "matches_published_semantic_transcript": digest == prior.get("transcript_sha256"),
        "construction": "Antimirov partial-derivative relation semantics",
        "oracle": "epsilon-free Glushkov position automata with synchronized state-pair reachability",
        "shared_mechanics": ["parser", "fixed infix corpus", "alphabet and case ordering"],
        "not_shared": ["derivative transitions", "automaton state space", "quotient acceptance algorithm"],
        "unbounded_star_family": {
            "k_min": 0,
            "k_max": 64,
            "cases": 65,
            "failure_count": len(star_failures),
            "failures": star_failures,
        },
        "mismatches": mismatches,
    }
    print(json.dumps(certificate, indent=2, sort_keys=True))
    return 1 if mismatches or star_failures or not certificate["matches_published_semantic_transcript"] else 0


if __name__ == "__main__":
    raise SystemExit(main())