Customizing Gappa
=================

These sections explain how rounding operators and back-ends are defined
in the tool. They are meant for developers rather than users of Gappa and
involve manipulating C++ classes defined in the :file:`src/arithmetic`
and :file:`src/backends` directories.

Defining a generator for a new formal system
--------------------------------------------

To be written.

Defining rounding operators for a new arithmetic
------------------------------------------------

Function classes
~~~~~~~~~~~~~~~~

A rounding operator derives from the ``function_class`` class. This class is an
interface to the name of the function and its associated real operator.

.. code-block:: cpp

   struct function_class
   {
     virtual std::string description() const = 0;
     virtual std::string pretty_name() const = 0;
     virtual ~function_class();
   };

The ``description`` method should return the internal name of the
rounding operator. It will be used when generating the notations of the
proof. When the generated notation cannot be reduced to a simple name,
comma-separated additional parameters can be appended. The back-end will
take care of formatting the final string. This remark also applies to
names returned by the theorem methods (see below). The ``pretty_name``
method should return a name that can be used in messages displayed to the
user. Ideally, this string can be reused in an input script.

Function generators
~~~~~~~~~~~~~~~~~~~

Because rounding operators can be parameterized, they have to be
generated by the parser on the fly. This is done by invoking the
functional method of an object derived from the ``function_generator``
class. For identical parameters, the same ``function_class`` object
should be returned, which means that they have to be cached by the generator.

.. code-block:: cpp

   struct function_generator {
     function_generator(const char *);
     virtual function_class const *operator()(function_params const &) const = 0;
     virtual ~function_generator();
   };

The constructor of this class requires the name of the function
template, so that it gets registered by the parser. Method ``operator()`` is
called with a vector of encoded parameters.

If a rounding operator has no parameters, the
``default_function_generator`` class can be used instead to register it.
The first argument of the constructor is the function name. The second
one is the address of the ``function_class`` object.

.. code-block:: cpp

   default_function_generator::default_function_generator(const char *, function_class const *);
