"""
    This module hosts propositions.
"""

from __future__ import annotations
from typing import Callable

from .terms import USABLE_VAR_NAMES, Const, Term, Var, ecsl
from dataclasses import dataclass

class Prop:
    """
        A proposition is a logical statement. It can be proven by the proof
        checker, or it can be used as a hypothesis to prove another
        proposition.
    """

    def __repr__(self) -> str:
        """
            Create a representation of a proposition.

            :return: String representation of the proposition.
            :rtype: str
        """
        return self.to_str(vars=set())

    def contains(self, term : Term) -> bool:
        """
            Determine whether a given term, value or variable is contained or
            described by this proposition.

            :param term: The term to look for.
            :type term: Term
            :return: Whether the term is contained in this proposition.
            :rtype: bool
        """
        return False
    
    def normalize(self) -> Prop:
        """
            Simplify the terms of a proposition.
        """
        return self
    
    def replace(self, old : Term, new : Term) -> Prop:
        """
            Find any occurrence of a given term, and replace it with the new
            term.

            :param old: The term to replace.
            :type old: Term
            :param new: The term to replace it with.
            :type new: Term
            :return: The proposition with the term replaced.
            :rtype: Prop
        """
        return self

    def to_str(self, vars : set[str]) -> str:
        return "<undefined prop>"

@dataclass(frozen=True)
class And(Prop):
    """
        The logical and-operator `P ∧ Q`.
    """

    P : Prop
    Q : Prop

    def __repr__(self) -> str:
        """
            Create a representation of a proposition.

            :return: String representation of the proposition.
            :rtype: str
        """
        return self.to_str(vars=set())

    def contains(self, term: Term) -> bool:
        return self.P.contains(term) or self.Q.contains(term)
    
    def normalize(self) -> Prop:
        """
            Simplify the terms of a proposition.
        """
        return And(P=self.P.normalize(), Q=self.Q.normalize())
    
    def replace(self, old: Term, new: Term) -> Prop:
        return And(
            P=self.P.replace(old=old, new=new),
            Q=self.Q.replace(old=old, new=new),
        )
    
    def to_str(self, vars: set[str]) -> str:
        p_str = ecsl(self.P.to_str(vars=vars))
        q_str = ecsl(self.Q.to_str(vars=vars))
        return f"{p_str} ∧ {q_str}"

@dataclass(frozen=True)
class Eq(Prop):
    """
        Compare whether two terms are equal.
    """

    x : Term
    y : Term

    def __repr__(self) -> str:
        """
            Create a representation of a proposition.

            :return: String representation of the proposition.
            :rtype: str
        """
        return self.to_str(vars=set())

    def contains(self, term: Term) -> bool:
        return self.x.contains(term) or self.y.contains(term)
    
    def normalize(self) -> Prop:
        """
            Simplify the terms of a proposition.
        """
        return Eq(x=self.x.normalize(), y=self.y.normalize())
    
    def replace(self, old: Term, new: Term) -> Prop:
        return Eq(
            x=self.x.replace(old=old, new=new),
            y=self.y.replace(old=old, new=new),
        )

    def to_str(self, vars : set[str]) -> str:
        x_str = ecsl(self.x.to_str(vars={ key : Var() for key in vars }))
        y_str = ecsl(self.y.to_str(vars={ key : Var() for key in vars }))
        return f"{x_str} = {y_str}"

@dataclass(frozen=True)
class Exists(Prop):
    """
        Create a statement that demonstrates there exists an x such that the
        given statement is true.
    """

    x : Callable[[Term], Prop]

    def __repr__(self) -> str:
        """
            Create a representation of a proposition.

            :return: String representation of the proposition.
            :rtype: str
        """
        return self.to_str(vars=set())

    def contains(self, term : Term) -> bool:
        i, c = 0, Const("")

        while i == 0 or term.contains(c):
            i += 1
            c = Const("temp_exists_variable_{i}")

        return self.x(c).contains(term=term)
    
    def normalize(self) -> Prop:
        """
            Simplify the terms of a proposition.
        """
        return Exists(lambda n : self.x(n).normalize())
    
    def replace(self, old: Term, new: Term) -> Prop:
        def replaced_func(input_term : Term) -> Prop:
            c = unique_const(input_term=input_term)
            return (
                self.x(c)
                    .replace(old=old, new=new)
                    .replace(old=c, new=input_term)
            )
        
        def unique_const(input_term : Term) -> Term:
            """
                Get a unique const value that doesn't interfere with either the
                old term that needs to be replaced, nor with the input term. 
            """
            i, c = 0, Const("")

            while i == 0 or input_term.contains(c) or old.contains(c):
                i += 1
                c = Const(f"temp_unique_value_{i}")
            
            return c

        return Exists(replaced_func)
    
    def to_str(self, vars : set[str]) -> str:
        for c in USABLE_VAR_NAMES:
            if c in vars:
                continue
            
            vars.add(c)
            s = self.x(Const(c)).to_str(vars=vars)
            vars.remove(c)

            return "∃" + c + "." + ecsl(s)
        else:
            raise ValueError(
                "Ran out of usable var names!"
            )

@dataclass(frozen=True)
class ForAll(Prop):
    """
        Create a statement that is true for all x
    """

    x : Callable[[Term], Prop]

    def __repr__(self) -> str:
        """
            Create a representation of a proposition.

            :return: String representation of the proposition.
            :rtype: str
        """
        return self.to_str(vars=set())

    def contains(self, term : Term) -> bool:
        i, c = 0, Const("")

        while i == 0 or term.contains(c):
            i += 1
            c = Const("temp_forall_variable_{i}")

        return self.x(c).contains(term=term)
    
    def normalize(self) -> Prop:
        """
            Simplify the terms of a proposition.
        """
        return ForAll(lambda n : self.x(n).normalize())
    
    def replace(self, old: Term, new: Term) -> Prop:
        def replaced_func(input_term : Term) -> Prop:
            c = unique_const(input_term=input_term)
            return (
                self.x(c)
                    .replace(old=old, new=new)
                    .replace(old=c, new=input_term)
            )
        
        def unique_const(input_term : Term) -> Term:
            """
                Get a unique const value that doesn't interfere with either the
                old term that needs to be replaced, nor with the input term. 
            """
            i, c = 0, Const("")

            while i == 0 or input_term.contains(c) or old.contains(c):
                i += 1
                c = Const(f"temp_unique_value_{i}")
            
            return c

        return ForAll(replaced_func)
    
    def to_str(self, vars : set[str]) -> str:
        for c in USABLE_VAR_NAMES:
            if c in vars:
                continue
            
            vars.add(c)
            s = self.x(Const(c)).to_str(vars=vars)
            vars.remove(c)

            return "∀" + c + "." + ecsl(s)
        else:
            raise ValueError(
                "Ran out of usable var names!"
            )

@dataclass(frozen=True)
class Implies(Prop):
    """
        The logical operator `P -> Q`.
    """

    P : Prop
    Q : Prop

    def __repr__(self) -> str:
        """
            Create a representation of a proposition.

            :return: String representation of the proposition.
            :rtype: str
        """
        return self.to_str(vars=set())

    def contains(self, term: Term) -> bool:
        return self.P.contains(term) or self.Q.contains(term)
    
    def normalize(self) -> Prop:
        """
            Simplify the terms of a proposition.
        """
        return Implies(P=self.P.normalize(), Q=self.Q.normalize())
    
    def replace(self, old: Term, new: Term) -> Prop:
        return Implies(
            P=self.P.replace(old=old, new=new),
            Q=self.Q.replace(old=old, new=new),
        )
    
    def to_str(self, vars: set[str]) -> str:
        p_str = ecsl(self.P.to_str(vars=vars))
        q_str = ecsl(self.Q.to_str(vars=vars))
        return f"{p_str} → {q_str}"

@dataclass(frozen=True)
class Or(Prop):
    """
        The logical and-operator `P v Q`.
    """

    P : Prop
    Q : Prop

    def __repr__(self) -> str:
        """
            Create a representation of a proposition.

            :return: String representation of the proposition.
            :rtype: str
        """
        return self.to_str(vars=set())

    def contains(self, term: Term) -> bool:
        return self.P.contains(term) or self.Q.contains(term)
    
    def normalize(self) -> Prop:
        """
            Simplify the terms of a proposition.
        """
        return Or(P=self.P.normalize(), Q=self.Q.normalize())

    def replace(self, old: Term, new: Term) -> Prop:
        return Or(
            P=self.P.replace(old=old, new=new),
            Q=self.Q.replace(old=old, new=new),
        )

    def to_str(self, vars: set[str]) -> str:
        p_str = ecsl(self.P.to_str(vars=vars))
        q_str = ecsl(self.Q.to_str(vars=vars))
        return f"{p_str} ∨ {q_str}"