# 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

from .scanner import Scanner
from .term import Ctor, Term
from .ast import Rule, Theorem, Development


class Parser(object):
    def __init__(self, text: str):
        self.scanner = Scanner(text, "...")

    def development(self) -> Development:
        theorems = []
        rules = []
        while self.scanner.on("rule"):
            rules.append(self.rule_decl())
        while self.scanner.on("proof", "theorem"):
            theorems.append(self.theorem())
        return Development(rules=rules, theorems=theorems)

    def rule_decl(self) -> Rule:
        self.scanner.expect("rule")
        return self.rule()

    def rule(self) -> Rule:
        lhs = self.term()
        assert isinstance(lhs, Ctor)
        self.scanner.expect("=>")
        rhs = self.term()
        return Rule(lhs=lhs, rhs=rhs)

    def theorem(self) -> Theorem:
        rule = None
        if self.scanner.consume("theorem"):
            rule = self.rule()
        self.scanner.expect("proof")
        terms = []
        while not self.scanner.on("qed"):
            terms.append(self.term())
        self.scanner.expect("qed")
        return Theorem(rule=rule, terms=terms)

    def term(self) -> Term:
        is_decoration = False
        if self.scanner.consume("*"):
            is_decoration = True
        if self.scanner.on_type("identifier"):
            assert self.scanner.token
            symbol = ("*" if is_decoration else "") + self.scanner.token
            self.scanner.scan()
            subterms = []
            if self.scanner.consume('('):
                while not self.scanner.on(')'):
                    subterms.append(self.term())
                    if not self.scanner.on(')'):
                        self.scanner.expect(',')
                self.scanner.expect(')')
            return Ctor(symbol=symbol, subterms=subterms)
        else:
            self.scanner.syntax_error(
                f"Expected identifier or integer literal, found '{self.scanner.token}'"
            )
            raise