Parameter Union.OT

An ordered type of finite values, extended with positive and negative infinites as well as successor and predecessor functions to represent strict lower and upper bounds.

Negative and positive infinites are used to represent half-planes as intervals; we require that all values are larger than the negative infinite and smaller than the positive infinite.

Values of the form x + \epsilon and x - \epsilon are used to transform open bounds in the finite type into closed bounds on the extended type t, with the equivalence:

        y <= x - \epsilon \Leftrightarrow y < x

and

        x + \epsilon <= y \Leftrightarrow y < x

This signature does not expose x + \epsilon and x - \epsilon values directly; instead, we use \mathrm{succ} and \mathrm{pred} functions which can be thought of as addition and subtraction of \epsilon, respectively.

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.

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.