Interface for union-of-interval modules.
The type of closed intervals over type 'a.
An interval { lb ; ub } represents the closed interval [lb, ub], i.e. a value v is in the interval iff lb <= v <= ub.
The type 'a bound is used to create and inspect intervals; see OrderedType.view and Interval.of_bounds.
module type Explanations = sig ... endType signature for explanations. This is mostly intended for Alt-Ergo's built-in Explanation module, but it can be convenient to use a different module for debugging.
module type OrderedType = sig ... endAn 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.
module type Interval = sig ... endIntervals over an OrderedType.
The kind type is an equivalent to the result type from the standard library with more appropriate constructor names.
It is used to distinguish between unions of intervals that are empty in the current context (with an explanation abstracting a set of model where the union is also empty) and unions of intervals that have at least one value in the current context.
module type Union = sig ... endSignature for union-of-intervals implementations with explanations.
module type RingType = sig ... endAn ordered ring is an ordered type with addition and multiplication that follows ring laws.
module type FieldType = sig ... endAn ordered field type is an ordered ring type equipped with a multiplicative inverse.
module type AlgebraicType = sig ... endAn ordered algebraic type is an ordered field with an (approximation of) the n-th root.
module type AlgebraicField = sig ... endUnion-of-intervals over an AlgebraicType.
module type EuclideanType = sig ... endAn ordered euclidean type is an ordered ring equipped with an euclidean division.
module type EuclideanRing = sig ... endUnion-of-intervals over an EuclideanType.