Source code for logic1.firstorder.quantified

r"""We provide subclasses of :class:`Formula <.formula.Formula>` that implement
quantified formulas in the sense that their toplevel operator is one of the
quantifiers :math:`\exists` or :math:`\forall`.
"""
from __future__ import annotations

from abc import abstractmethod
from collections import deque
from typing import final, Sequence

from logic1.firstorder.term import Variable
from logic1.firstorder.formula import α, τ, χ, σ, Formula

from logic1.support.tracing import trace




class QuantifiedFormula(Formula[α, τ, χ, σ]):
    r"""A class whose instances are quantified formulas in the sense that their
    toplevel operator is one of the quantifiers :math:`\exists` or
    :math:`\forall`. Note that members of :class:`QuantifiedFormula` may have
    subformulas with other logical operators deeper in the expression tree.
    """

    @property
    def var(self) -> χ:
        """The variable of the quantifier.

        >>> from logic1.theories.RCF import *
        >>> x, y = VV.get('x', 'y')
        >>> f = All(x, Ex(y, x == y))
        >>> f.var
        x

        .. seealso::
            * :attr:`args <.formula.Formula.op>` -- all arguments as a tuple
            * :attr:`op <.formula.Formula.op>` -- operator
        """
        return self.args[0]

    @property
    def arg(self) -> Formula[α, τ, χ, σ]:
        """The subformula in the scope of the :class:`QuantifiedFormula`.

        >>> from logic1.theories.RCF import *
        >>> x, y = VV.get('x', 'y')
        >>> f = All(x, Ex(y, x == y))
        >>> f.arg
        Ex(y, x - y == 0)

        .. seealso::
            * :attr:`args <.formula.Formula.op>` -- all arguments as a tuple
            * :attr:`op <.formula.Formula.op>` -- operator
        """
        return self.args[1]

    @abstractmethod
    def __init__(self, vars_: χ | Sequence[χ], arg: Formula[α, τ, χ, σ]) -> None:
        """Construct a quantified formula.

        >>> from logic1.theories.RCF import VV
        >>> a, b, x = VV.get('a', 'b', 'x')
        >>> All((a, b), Ex(x, a*x + b >= 0))
        All(a, All(b, Ex(x, a*x + b >= 0)))
        """
        assert self.op in (Ex, All)  # in lack of abstract class properties
        super().__init__()
        if not isinstance(arg, Formula):
            raise ValueError(f'{arg!r} is not a Formula')
        match vars_:
            case Variable():
                assert not isinstance(vars_, Sequence)
                self._args = (vars_, arg)
            case (Variable(), *_):
                f = arg
                for v in reversed(vars_[1:]):
                    f = self.op(v, f)
                self._args = (vars_[0], f)
            case _:
                raise ValueError(f'{vars_!r} is not a Variable')

    def __le__(self, other: Formula[α, τ, χ, σ]) -> bool:
        """Compare two quantified formulas by their quantifier variable and
        subformula. Use the :meth:`sort_key <.term.Variable.sort_key>` of the
        variables.

        >>> from logic1.theories.RCF import *
        >>> x, y = VV.get('x', 'y')
        >>> f1 = All(x, x**2 >= 0)
        >>> f2 = All(y, y**2 >= 0)
        >>> f2 <= f1
        True
        """
        if isinstance(other, QuantifiedFormula) and self.op is other.op:
            return self.var.sort_key() <= other.var.sort_key() and self.arg <= other.arg
        else:
            return super().__le__(other)





@final
class Ex(QuantifiedFormula[α, τ, χ, σ]):
    r"""A class whose instances are existentially quantified formulas in the
    sense that their toplevel operator represents the quantifier symbol
    :math:`\exists`. Besides variables, the quantifier accepts sequences of
    variables as a shorthand.

    >>> from logic1.firstorder import *
    >>> from logic1.theories.RCF import *
    >>> x, y, z = VV.get('x', 'y', 'z')
    >>> Ex(x, x**2 == y)
    Ex(x, x**2 - y == 0)
    >>> Ex([x, y], And(x > 0, y > 0, z == x - y))
    Ex(x, Ex(y, And(x > 0, y > 0, x - y - z == 0)))
    """



    def __init__(self, vars_: χ | Sequence[χ], arg: Formula[α, τ, χ, σ]) -> None:
        """Construct an existentially quantified formula.

        >>> from logic1.theories.RCF import VV
        >>> x, y = VV.get('x', 'y')
        >>> Ex(x, x**2 == y)
        Ex(x, x**2 - y == 0)
        """
        super().__init__(vars_, arg)




    @classmethod
    def dual(cls) -> type[All[α, τ, χ, σ]]:
        r"""A class method yielding the class :class:`All`, which implements
        the dual operator :math:`\forall` of :math:`\exists`.
        """
        return All






@final
class All(QuantifiedFormula[α, τ, χ, σ]):
    r"""A class whose instances are universally quantified formulas in the
    sense that their toplevel operator represents the quantifier symbol
    :math:`\forall`. Besides variables, the quantifier accepts sequences of
    variables as a shorthand.

    >>> from logic1.theories.RCF import *
    >>> x, y = VV.get('x', 'y')
    >>> All(x, x**2 >= 0)
    All(x, x**2 >= 0)
    >>> All([x, y], (x + y)**2 >= 0)
    All(x, All(y, x**2 + 2*x*y + y**2 >= 0))
    """



    def __init__(self, vars_: χ | Sequence[χ], arg: Formula[α, τ, χ, σ]) -> None:
        """Construct a universally quantified formula.

        >>> from logic1.theories.RCF import VV
        >>> x, y = VV.get('x', 'y')
        >>> All(x, x**2 >= 0)
        All(x, x**2 >= 0)
        """
        super().__init__(vars_, arg)




    @classmethod
    def dual(cls) -> type[Ex[α, τ, χ, σ]]:
        """A class method yielding the dual class :class:`Ex` of class:`All`.
        """
        return Ex






class Prefix(deque[tuple[type[All | Ex], list[χ]]]):
    """Holds a quantifier prefix of a formula.

    >>> from logic1.theories.RCF import *
    >>> x, x0, epsilon, delta = VV.get('x', 'x0', 'epsilon', 'delta')
    >>> Prefix((All, [x0, epsilon]), (Ex, [delta]), (All, [x]))
    Prefix([(<class 'logic1.firstorder.quantified.All'>, [x0, epsilon]),
            (<class 'logic1.firstorder.quantified.Ex'>, [delta]),
            (<class 'logic1.firstorder.quantified.All'>, [x])])
    >>> print(_)
    All [x0, epsilon]  Ex [delta]  All [x]

    .. seealso::
        * :external:class:`collections.deque` -- for methods inherited from double-ended queues
        * :meth:`matrix <.Formula.matrix>` -- the matrix of a prenex formula
        * :meth:`quantify <.Formula.quantify>` -- add quantifier prefix
    """

    def __init__(self, *blocks: tuple[type[All[α, τ, χ, σ] | Ex[α, τ, χ, σ]], list[χ]]) -> None:
        super().__init__(blocks)

    def __str__(self) -> str:
        return '  '.join(q.__name__ + ' ' + str(vars_) for q, vars_ in self)