Description:

• The command implementpoly implements the polynomial polynomial in range range as a function called functionname in C code using double, double-double and triple-double arithmetic in a way that the rounding error (estimated at its first order) is bounded by error bound. The produced code is output in a file named filename. The argument format indicates the double, double-double or triple-double format of the variable in which the polynomial varies, influencing also in the signature of the C function.
  
  If a seventh or eighth argument proof filename is given and if this argument evaluates to a variable of type string, the command implementpoly will produce a Gappa proof that the rounding error is less than the given bound. This proof will be output in Gappa syntax in a file name proof filename.
  
  The command implementpoly returns the polynomial that has been implemented. As the command implementpoly tries to adapt the precision needed in each evaluation step to its strict minimum and as it applies renormalization to double-double and triple-double precision coefficients to bring them to a round-to-nearest expansion form, the returned polynomial may differ from the polynomial polynomial. Nevertheless the difference will be small enough that the rounding error bound with regard to the polynomial polynomial (estimated at its first order) will be less than the given error bound.
  
  If a seventh argument honor coefficient precisions is given and evaluates to a variable honorcoeffprec of type honorcoeffprec, implementpoly will honor the precision of the given polynomial polynomials. This means if a coefficient needs a double-double or a triple-double to be exactly stored, implementpoly will allocate appropriate space and use a double-double or triple-double operation even if the automatic (heuristic) determination implemented in command implementpoly indicates that the coefficient could be stored on less precision or, respectively, the operation could be performed with less precision. The use of honorcoeffprec has advantages and disadvantages. If the polynomial polynomial given has not been determined by a process considering directly polynomials with floating-point coefficients, honorcoeffprec should not be indicated. The implementpoly command can then determine the needed precision using the same error estimation as used for the determination of the precisions of the operations. Generally, the coefficients will get rounded to double, double-double and triple-double precision in a way that minimizes their number and respects the rounding error bound error bound. Indicating honorcoeffprec may in this case short-circuit most precision estimations leading to sub-optimal code. On the other hand, if the polynomial polynomial has been determined with floating-point precisions in mind, honorcoeffprec should be indicated because such polynomials often are very sensitive in terms of error propagation with regard to their coefficients' values. Indicating honorcoeffprec prevents the implementpoly command from rounding the coefficients and altering by many orders of magnitude the approximation error of the polynomial with regard to the function it approximates.
  
  The implementer behind the implementpoly command makes some assumptions on its input and verifies them. If some assumption cannot be verified, the implementation will not succeed and implementpoly will evaluate to a variable error of type error. The same behaviour is observed if some file is not writable or some other side-effect fails, e.g. if the implementer runs out of memory.
  
  As error estimation is performed only on the first order, the code produced by the implementpoly command should be considered valid iff a Gappa proof has been produced and successfully run in Gappa.