Module type Intervals_intf.FieldType

An ordered field type is an ordered ring type equipped with a multiplicative inverse.

include RingType
include OrderedType
type finite

The type of finite values.

val pp_finite : finite Fmt.t

Pretty-printer for finite values.

type t

The type of extended values used to represent interval bounds.

val pp : t Fmt.t

Pretty-printer for extended values.

val equal : t -> t -> bool

Equality on extended values. Must be compatible with compare.

val compare : t -> t -> int

The comparison function on extended values is an extension of the regular order on finite values.

val view : t -> finite bound

view t converts the internal representation to a bound for examination.

val minfty : t

minfty is an extended value -\infty such that for any extended value x, -\infty \le x.

val finite : finite -> t

Finite values are included in t. We will identify a finite value in finite and its representation in t.

val pinfty : t

pinfty is an extended value +\infty such that for any extended value x, x \le +\infty.

val value_opt : t -> finite option

value_opt is the partial inverse of finite.

val succ : t -> t

Each element of the ordered type t has a successor. The successor of an element is always greater than the element itself:

        \forall x, x \le \mathrm{succ}(x)

We say that x is a finite upper bound if it is strictly smaller than its successor, i.e. if x < \mathrm{succ}(x), and we require that all finite values are finite upper bounds (however there may be finite upper bounds that are not finite values).

succ must be the inverse of pred below.

val pred : t -> t

Each element of the ordered type t has a predecessor. The predecessor of an element is always smaller than the element itself:

        \forall x, \mathrm{pred}(x) \le x

We say that x is a finite lower bound if it is strictly greater than its predecessor, i.e. if \mathrm{pred}(x) < x, and we require that all finite values are finite lower bounds (however there may be finite lower bounds that are not finite values).

pred must be the inverse of succ above.

val add : t -> t -> t

add will only be called with values that are compatible with its monotonicity: its argument can never be two bounds of different kinds (upper or lower).

val zero : t

Neutral element for addition.

val neg : t -> t

Inverse for addition: for all u, add u (neg u) = zero.

val mul : t -> t -> t

mul will be only be called with values that are compatible with its monotonicity: its arguments can be two bounds with the same sign and kind (upper or lower), or two bounds with opposite signs and opposite kinds (upper or lower), but never two bounds with the same sign and opposite kinds or opposite signs and the same kind.

It is recommended to program defensively and raise an assertion failure if mul is ever called with two bounds of the same sign and opposite kinds or opposite signs and the same kind.

val pow : int -> t -> t

pow n x raises x to the n-th power.

  • raises Invalid_arg

    if n is nonpositive.

val inv : t -> t

Inverse for multiplication: for all u, mul u (inv u) = one.

inv zero is undefined.