# Copyright (c) 2022-2024 Chris Pressey, Cat's Eye Technologies
# This file is distributed under a 2-clause BSD license.  See LICENSES directory:
# SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Eqthy

from typing import Union

from eqthy.objects import (
    Document, Axiom, Theorem, Step,
    Hint, Reflexivity, Substitution, Congruence, Reference
)
from eqthy.scanner import Scanner, EqthySyntaxError
from eqthy.terms import Term, Ctor, Variable, Eqn


# Document := {Axiom} {Theorem}.
# Axiom    := "axiom" [Name] Eqn.
# Theorem  := "theorem" [Name] Eqn "proof" {Step} "qed".
# Name     := "(" Ident ")".
# Step     := Eqn ["[" "by" Hint "]"].
# Hint     := "reflexivity"
#           | "substitution" "of" Term "into" Var
#           | "congruence" "of" Var "and" Term
#           | Ident ["on" ("LHS" | "RHS")] ["with" Subst {"," Subst}].
# Eqn      := Term "=" Term.
# Term     := Var | Ctor ["(" [Term {"," Term} ")"].


class Parser(object):
    def __init__(self, text: str, filename: str):
        self.scanner = Scanner(text, filename)
        self.axiom_count: int = 0
        self.theorem_count: int = 0

    def document(self) -> Document:
        axioms = []
        theorems = []
        while self.scanner.on('axiom'):
            axioms.append(self.axiom())
        while self.scanner.on('theorem'):
            theorems.append(self.theorem())
        if (not axioms) and (not theorems):
            raise EqthySyntaxError(
                self.scanner.filename,
                self.scanner.line_number,
                "Eqthy document is empty"
            )
        self.scanner.check_eof()
        return Document(axioms=axioms, theorems=theorems)

    def axiom(self) -> Axiom:
        self.scanner.expect('axiom')
        name = self.name()
        eqn = self.eqn()
        if not name:
            self.axiom_count += 1
            name = 'unnamed_axiom_{}'.format(self.axiom_count)
        return Axiom(name=name, eqn=eqn)

    def theorem(self) -> Theorem:
        self.scanner.expect('theorem')
        name = self.name()
        eqn = self.eqn()
        self.scanner.expect('proof')
        steps = []
        while not self.scanner.on('qed'):
            steps.append(self.step())
        self.scanner.expect('qed')
        if not name:
            self.theorem_count += 1
            name = 'unnamed_theorem_{}'.format(self.theorem_count)
        return Theorem(name=name, eqn=eqn, steps=steps)

    def name(self) -> Union[str, None]:
        if self.scanner.consume('('):
            ident = self.scanner.token
            self.scanner.scan()
            self.scanner.expect(')')
            return ident
        else:
            return None

    def step(self) -> Step:
        eqn = self.eqn()
        hint: Union[Hint, None] = None
        if self.scanner.consume('['):
            self.scanner.expect('by')
            hint = self.hint()
            self.scanner.expect(']')
        return Step(eqn=eqn, hint=hint)

    def hint(self) -> Hint:
        if self.scanner.consume('reflexivity'):
            return Reflexivity()
        elif self.scanner.consume('substitution'):
            self.scanner.expect('of')
            term = self.term()
            self.scanner.expect('into')
            variable = self.var()
            return Substitution(term=term, variable=variable)
        elif self.scanner.consume('congruence'):
            self.scanner.expect('of')
            variable = self.var()
            self.scanner.expect('and')
            term = self.term()
            return Congruence(term=term, variable=variable)
        else:
            name = self.scanner.token
            side = None
            substs = []
            self.scanner.scan()
            if self.scanner.consume('on'):
                if self.scanner.on('LHS') or self.scanner.on('RHS'):
                    side = self.scanner.token
                    self.scanner.scan()
                else:
                    self.scanner.syntax_error("Expected 'LHS' or 'RHS'")
            if self.scanner.consume('with'):
                substs.append(self.eqn())
                while self.scanner.consume(','):
                    substs.append(self.eqn())
            assert isinstance(name, str)
            return Reference(name=name, side=side, substs=substs)

    def eqn(self) -> Eqn:
        lhs = self.term()
        self.scanner.expect('=')
        rhs = self.term()
        return Eqn(lhs=lhs, rhs=rhs)

    def term(self) -> Term:
        name = self.scanner.token
        assert isinstance(name, str)
        self.scanner.scan()
        if name.isupper():
            return Variable(name=name)
        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(ctor=name, subterms=subterms)

    def var(self) -> Variable:
        var = self.term()
        if not isinstance(var, Variable):
            self.scanner.syntax_error("Expected variable")
        assert isinstance(var, Variable)
        return var