# 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 `src/arithmetic` and `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.

    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.

    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.

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