========
Formulas
========

Logics express
consecutions involving fundamental linguistic (or syntactical) objects 
called *formulas*.
The set of all formulas that may be present in consecutions of a given logic is the *object-language*, 
or simply the *language*, of such logic.
Currently, *ct4l* supports only propositional languages, as we describe below.

.. contents:: :local:

Propositional languages
-----------------------

A *propositional language* :math:`\mathbf{L}_\Sigma(P)` over a propositional signature :math:`\Sigma`
is the absolutely free algebra over :math:`\Sigma` freely generated by the set
:math:`P = \{p_i : i \in \omega\}` of *propositional variables*.
The elements of the carrier :math:`L_\Sigma(P)` of this algebra are called *propositional formulas*,
commonly denoted by Greek letters (like :math:`\varphi`, :math:`\psi`, :math:`\phi`, :math:`\ldots`).

In *ct4l*, we have an interface for propositional formulas called :cpp:class:`ct4l::PropFmla`,
and two specializations:

    - :cpp:class:`ct4l::PropVar` represents propositional variables:

        .. code-block:: cpp

            ct4l::PropVar p {"p"};

    - :cpp:class:`ct4l::PropCompound` represents compound formulas, holding a pointer 
      to a :math:`k`-ary connective (a :cpp:class:`ct4l::Connective` object) and a vector of 
      pointers to :math:`k` :cpp:class:`ct4l::PropFmla` objects. 
      
      For example, the formula :math:`p\,\mathsf{and}\,q` can be constructed in the following way:

        .. code-block:: cpp

            using namespace std;
            using namespace ct4l;

            auto and = make_shared<Connective> {"and", 2};
            auto p = make_shared<PropVar> {"p"};
            auto q = make_shared<PropVar> {"q"};
            PropCompound p_and_q {and, {p, q}};
   
      We recommend, however, to use a parser to build formulas. See 
      :ref:`parser propositional` for more details.

On propositional formulas we may perform the basic operations described below.

    - the set of subformulas of a given formula is given by:
    
        .. math::
            
            \mathsf{subformulas}(\varphi) =
            \begin{cases}
                \{\varphi\} & \text{ if } \varphi \in P\\
                \{\varphi\} \cup \bigcup_{i=1}^n \mathsf{subformulas}(\varphi_i) & \text{ if } \varphi=\#(\varphi_1,\ldots,\varphi_n)\\
            \end{cases}
        
        Just call:

        .. code-block:: cpp

            auto subfmlas = fmla.subformulas();

    - the set of propositional variables of a given formula is given by the function:

        .. math::
            
            \mathsf{props}(\varphi) =
            \begin{cases}
                \{\varphi\} & \text{ if } \varphi \in P\\
                \bigcup_{i=1}^n \mathsf{props}(\varphi_i) & \text{ if } \varphi=\#(\varphi_1,\ldots,\varphi_n)\\
            \end{cases}

        Just call:

        .. code-block:: cpp

            auto props = fmla.props();

    - the complexity of a formula is given by:

        .. math::
            \mathsf{complexity}(\varphi)=
            \begin{cases}
                0 & \text{ if } \varphi \in P\\
                1 + \sum_{i=1}^n \mathsf{complexity}(\varphi_i) & \text{ if } \varphi=\#(\varphi_1,\ldots,\varphi_n)\\
            \end{cases}
        
        Just call:

        .. code-block:: cpp

            auto complexity = fmla.complexity();    

    - we infer the formula signature by (for operations on signatures, check :cpp:class:`ct4l::PropSignature`):

        .. math::
            \mathsf{signature}(\varphi)=
            \begin{cases}
                \mathsf{empty\_signature} & \text{ if } \varphi \in P\\
                \sum_{i=1}^n(\mathsf{signature}(\varphi_i)) + \# & \text{ if } \varphi=\#(\varphi_1,\ldots,\varphi_n)\\
            \end{cases}

        Just call:

        .. code-block:: cpp

            auto signature = fmla.infer_signature();




.. _parser propositional:

Parsing propositional formulas
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

We provide by default the parser :cpp:class:`ct4l::PropParser` 
for propositional formulas, to produce
:cpp:class:`ct4l::PropFmla` instances from strings.
Here is how you can parse a formula (see below for a more secure version):

    .. code-block:: cpp

        ct4l::PropParser parser;
        auto [fmla, msgs] = parser.parse("p and q");

In the code above, the variable `msgs` holds a list of messages 
(objects of class :cpp:class:`ct4l::RowColMessage`)
possibly produced during
the parsing process. Any unexpected character during parsing 
produces a warning, while incompatibility with the grammar produces errors.
We suggest to always check if this list is empty or not. Moreover,
unrecoverable errors during parsing results in an exception that should be
checked. Here is a code that *securely* parses a formula: 

    .. code-block:: cpp

        ct4l::PropParser parser;
        try {
            auto [fmla, msgs] = parser.parse("p and q");
            if (msgs.empty()) {
                // secure to use the formula, no errors or warnings
            } else {
                // some warning was produced, maybe check with the user if they want to continue
            }
        } catch (ParseException& e) {
            // deal with the error, messages are in e.messages()
        }

By default, the parser logs the messages on the screen. You can overwrite this
behaviour by passing a callback to the parser constructor that simply ignores the messages: 

    .. code-block:: cpp

        ct4l::PropParser parser {[](auto m){}};

You can actually give two callbacks to this constructor: the first one is 
called whenever the lexer produces a message (that is, whenever unexpected 
characters are produced), and the second one is called whenever 
a parsing problem occurs. The argument given to each callback is
an instance of :cpp:class:`ct4l::RowColMessage`. When you pass only one, 
it is used for both purposes.

The default parser implements the following grammar, using the *Bison* tool:

.. math::
    \begin{split}
        \mathsf{digit} &:= [0-9]\\
        \mathsf{integer} &:= \{\mathsf{digit}\}+\\
        \mathsf{alpha} &:= [\mathrm{a-zA-Z}]\\
        \mathsf{symbol} &:= [\#\$ ! @ \% \& < > ?]\\
        \mathsf{Id} &:= (\mathsf{alpha}|\mathsf{symbol})(\mathsf{alpha}|\mathsf{digit}|\mathsf{symbol})*\\
        \mathsf{NullaryConn} &:= \text{top } \mid \text{ bot}\\
        \mathsf{UnaryConn} &:= \text{neg} \mid - \\
        \mathsf{BinaryConn} &:= \text{and} \mid \text{or} \mid \text{->} \mid + \mid - \mid * \mid /\\
        \mathsf{Fmla} &:= \mathsf{Prop} \mid \mathsf{NullaryComp} \mid \mathsf{UnaryComp} \mid \mathsf{BinaryComp} \mid \mathsf{KAryComp}\\
        \mathsf{Prop} &:= \mathsf{Id} \\
        \mathsf{NullaryComp} &:= \mathsf{NullaryConn} \mid `\mathsf{Id}`\\
        \mathsf{UnaryComp} &:= \mathsf{UnaryConn}\,\mathsf{Fmla} \mid `\mathsf{Id}`\,\mathsf{Fmla}\\
        \mathsf{BinaryComp} &:= \mathsf{Fmla}\,\mathsf{BinaryConn}\,\mathsf{Fmla} \mid \mathsf{Fmla}\,`\mathsf{Id}`\,\mathsf{Fmla}\\
        \mathsf{KAryComp} &:= \mathsf{Id}([\mathsf{Fmla}[,\mathsf{Fmla}]])\\
    \end{split}

Some examples of strings accepted by this parser (and their corresponding formulas) are:

- :code:`"p"`: :math:`p` (a propositional variable)
- :code:`"p and q"`: :math:`p \, \mathsf{and} \, q` (a binary compound)
- :code:`"p 'foo' q"`: :math:`p \, \mathsf{foo} \, q` (:math:`\mathsf{foo}` is parsed as a binary connective)
- :code:`"neg p"`: a unary compound
- :code:`"'box' p"`: a unary compound, with :math:`\mathsf{box}` parsed as a unary connective
- :code:`"pt(p, q, r)"`: a ternary compound, with :math:`\mathsf{pt}` parsed as a ternary connective
- :code:`"top"`: the nullary formula called :math:`\mathsf{top}`
- :code:`"'botop'"`: the nullary formula called :math:`\mathsf{botop}`
- :code:`"p(q) and p"`: no problem with :code:`p` being both a connective and a propositional variable

Now, some invalid cases:

- :code:`"p and"`: `and` is binary
- :code:`"p lor q"`: `lor` is not a default binary connective; it should be declared with quotes


Working with sets of formulas
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

We provide the :code:`ct4l::PropFmlaPtrSet` type to work
with sets of formulas:

    .. code-block:: cpp

        using namespace ct4l;

        PropParser parser;
        auto [f1, m1] = parser.parse("p and q");
        auto [f2, m2] = parser.parse("p and r");
        PropFmlaPtrSet s {f1, f2};

.. note::
    As :cpp:class:`ct4l::PropFmla` is abstract, sets of formulas here
    are actually sets of pointers to formulas. The comparator given for
    the set container uses the strict weak ordering
    of the underlying concrete formulas.

First-order languages
---------------------

Future work.

API
---

.. doxygenclass:: ct4l::PropFmla
    :members:

.. doxygenclass:: ct4l::PropVar
    :members:

.. doxygenclass:: ct4l::PropCompound
    :members:

.. doxygenclass:: ct4l::PropFmlaVisitor
    :members:

.. doxygenclass:: ct4l::PropFmlaParserI
    :members:

.. doxygenclass:: ct4l::BisonPropFmlaParser
    :members: