Module AltErgoLib.Intervals_intf

Interface for union-of-interval modules.

type 'a interval = {
  1. lb : 'a;
  2. ub : 'a;
}

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.

type 'a bound =
  1. | Open of 'a
    (*

    An open (strict) finite bound.

    *)
  2. | Closed of 'a
    (*

    A closed (large) finite bound.

    *)
  3. | Unbounded
    (*

    An infinite bound.

    *)

The type 'a bound is used to create and inspect intervals; see OrderedType.view and Interval.of_bounds.

module type Explanations = sig ... end

Type 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 ... end

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.

module type Interval = sig ... end

Intervals over an OrderedType.

type ('a, 'b) kind =
  1. | NonEmpty of 'a
    (*

    A non-empty value of type 'a.

    *)
  2. | Empty of 'b
    (*

    An empty value with additional justification.

    *)

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 ... end

Signature for union-of-intervals implementations with explanations.

module type Core = sig ... end

Polymorphic Union implementations.

module type RingType = sig ... end

An ordered ring is an ordered type with addition and multiplication that follows ring laws.

module type Ring = sig ... end

Union-of-intervals over a RingType.

module type FieldType = sig ... end

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

module type Field = sig ... end

Union-of-intervals over a FieldType.

module type AlgebraicType = sig ... end

An ordered algebraic type is an ordered field with an (approximation of) the n-th root.

module type AlgebraicField = sig ... end

Union-of-intervals over an AlgebraicType.

module type EuclideanType = sig ... end

An ordered euclidean type is an ordered ring equipped with an euclidean division.

module type EuclideanRing = sig ... end

Union-of-intervals over an EuclideanType.