"""Exact unequal-integer certificates for factorial parser blowups.

Only recognizes a deliberately small grammar: nonnegative integer constants,
integer powers and parentheses, with at most one terminal factorial per side.
Different residues prove inequality. Equal residues say nothing. Never returns
a positive grade and never uses a model, question identity or answer lookup.
"""
import ast
import math
import re


def bounded_integer(node, depth=0):
    if depth > 12:
        raise ValueError('expression depth')
    if isinstance(node, ast.Constant) and type(node.value) is int:
        value = node.value
        if value < 0 or value.bit_length() > 16384:
            raise ValueError('integer range')
        return value
    if isinstance(node, ast.BinOp) and isinstance(node.op, ast.Pow):
        base = bounded_integer(node.left, depth+1)
        exponent = bounded_integer(node.right, depth+1)
        if base in (0, 1):
            # Python/SymPy both use 0**0=1, but exclude ambiguity conservatively.
            if base == exponent == 0:
                raise ValueError('zero power zero')
            return base if exponent else 1
        if exponent > 16384 or base.bit_length()*exponent > 16384:
            raise ValueError('power range')
        return base**exponent
    raise ValueError('outside integer-power grammar')


def expression(text):
    if not isinstance(text, str) or len(text) > 512:
        raise ValueError('expression length')
    text = text.strip()
    factorial = text.endswith('!')
    body = text[:-1].strip() if factorial else text
    if not re.fullmatch(r'[0-9()*\s]+', body):
        raise ValueError('outside integer alphabet')
    if factorial and not body.isdecimal():
        # A postfix factorial binds to its immediate atom. Without this check,
        # 2**3! would be incorrectly read as (2**3)! instead of 2**(3!).
        if not body.startswith('(') or not body.endswith(')'):
            raise ValueError('factorial must cover entire expression')
        depth = 0
        for position, char in enumerate(body):
            depth += (char == '(') - (char == ')')
            if depth < 0 or (depth == 0 and position != len(body)-1):
                raise ValueError('factorial must cover entire expression')
        if depth:
            raise ValueError('unbalanced factorial')
    tree = ast.parse(body, mode='eval').body
    value = bounded_integer(tree)
    return factorial, value


def unequal_certificate(prediction_normalized, reference_normalized):
    """Return a checked modular inequality witness or None (never an equality)."""
    try:
        pred_factorial, pred = expression(prediction_normalized)
        ref_factorial, ref = expression(reference_normalized)
    except (ValueError, SyntaxError, RecursionError, TypeError):
        return None
    if not (pred_factorial or ref_factorial):
        return None

    def residue(value, factorial, modulus):
        if not factorial:
            return value % modulus
        # n! contains modulus as a factor whenever n>=modulus. No primality
        # assumption is needed for this implication; small n is evaluated.
        return 0 if value >= modulus else math.factorial(value) % modulus

    for modulus in (2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31):
        a = residue(pred, pred_factorial, modulus)
        b = residue(ref, ref_factorial, modulus)
        if a != b:
            return dict(kind='unequal_integer_residues_v1', modulus=modulus,
                        prediction_residue=a, reference_residue=b,
                        prediction_normalized=prediction_normalized,
                        reference_normalized=reference_normalized,
                        statement='Equal integers have equal residues modulo every positive integer.')
    return None
