# Copyright (c) 2025-2026, Chris Pressey, Cat's Eye Technologies.
# This file is distributed under a 2-clause BSD license.  See LICENSES/ dir.
# SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Lome

import logging
from dataclasses import dataclass
from typing import List, Union

from .ast import Development, Theorem
from .reduce import ProofSystem, ReductionError, reduce_term
from .term import strip_decorators, terms_equal, render_term


logger = logging.getLogger(__name__)


@dataclass
class OK:
    pass


@dataclass
class Error:
    msg: str


def check_development(development: Development) -> List[Union[OK, Error]]:
    proof_system = ProofSystem()
    for rule in development.rules:
        proof_system.add_rule(rule)
    results = []
    for theorem in development.theorems:
        result = check_theorem(theorem, proof_system)
        results.append(result)
    return results


def check_theorem(theorem: Theorem, proof_system: ProofSystem) -> Union[OK, Error]:
    terms = theorem.terms
    if not terms:
        return Error("Proof has no terms")
    for i in range(1, len(terms)):
        prev_term = terms[i - 1]
        current_term = terms[i]
        try:
            reduced_prev = reduce_term(prev_term, proof_system)
            stripped_current = strip_decorators(current_term)
        except ReductionError as e:
            return Error(str(e))
        logger.debug("previous term: %s", render_term(prev_term))
        logger.debug("current term: %s", render_term(current_term))
        logger.debug("reduced previous: %s", render_term(reduced_prev))
        logger.debug("stripped current: %s", render_term(stripped_current))
        if not terms_equal(reduced_prev, stripped_current):
            return Error(
                f"Step {i+1} is invalid: {render_term(terms[i-1])} "
                f"does not lead to {render_term(terms[i])}"
            )
    if theorem.rule:
        proof_system.add_rule(theorem.rule)
    return OK()