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 *);