Module Theory.IEEE754

Sorts implementing IEEE754 formats.

This module provides an infinite set of indexed sorts for floating-point numbers defined in the IEEE754 standard.

This sorts are not referenced in the Core Theory (or any other theory in this library) and provided for user convenience. Any other format could be used with the Core Theory.

type ('b, 'e, 't) t

a type for IEEE754 format.

The type is indexed with three indices:

  • 'b the value of the base;
  • 'e the size of the exponent;
  • 't the size of the significand.
type ('a, 'e, 't) ieee754 = ('a, 'e, 't) t
type parameters = private {
  1. base : int;
  2. bias : int;
  3. k : int;
  4. p : int;
  5. w : int;
  6. t : int;
}

A named tuple of representation parameters.

The names of parameter are taken from the IEEE 754-1985 standard section 3.6, table 3.5 on page 13. For the convenience, here is their meaning (refer the original standard for more detailed definitions):

  • k - storage width in bits;
  • p - precision in bits;
  • w - exponent field width in bits;
  • t - trailing significand field width in bits;

The module provides a set of common predefined formats as well as safe constructors to define uncommon formats.

val binary16 : parameters

Parameters for the binary16 IEEE754 format.

val binary32 : parameters

Parameters for the binary32 IEEE754 format.

val binary64 : parameters

Parameters for the binary64 IEEE754 format.

val binary80 : parameters

Parameters for the binary80 IEEE754 format.

val binary128 : parameters

Parameters for the binary128 IEEE754 format.

val decimal32 : parameters

Parameters for the decimal32 IEEE754 format.

val decimal64 : parameters

Parameters for the decimal64 IEEE754 format.

val decimal128 : parameters

Parameters for the decimal128 IEEE754 format.

val binary : int -> parameters option

binary N are parameters for the binary<N> IEEE754 format.

Where N is the storage width in bits, and parameters are defined for the following N: 16,80, k*32, for all natural k that are greater than 0.

val decimal : int -> parameters option

decimal N are parameters for the decimal<N> IEEE754 format.

Where N is the storage width in bits, and parameters are defined for all N = k*32 where k is a natural number greater than zero.

module Sort : sig ... end

IEEE754 sorts.