Module ItvUtils.FloatItvNanSource

FloatItvNan - Floating-point intervals with special IEEE numbers.

Adds special IEEE number managenement (NaN, infinities) to FloatItv.

Sourcemodule F = Float
Sourcemodule FI = FloatItv
Sourcemodule B = IntBound
Sourcemodule II = IntItv

Types

Sourcetype t = {
  1. itv : FI.t Utils_core.Bot.with_bot;
    (*

    Interval of non-special values. Bounds cannot be NaN. Bounds can be infinities to represent non-infinity floats outside the range of doubles.

    *)
  2. nan : bool;
    (*

    Whether to include NaN.

    *)
  3. pinf : bool;
    (*

    Whether to include +∞.

    *)
  4. minf : bool;
    (*

    Whether to include -∞.

    *)
}

A set of IEEE floating-point values. Represented as a set of non-special values, and boolean flags to indicate the presence of each special IEEE value. The value 0 in the interval represents both IEEE +0 and -0. Note: the type can naturally represent the empty set.

Sourceval is_valid : t -> bool

All elements of type t whould satisfy this predicate.

Sourcetype prec = [
  1. | `SINGLE
    (*

    32-bit single precision

    *)
  2. | `DOUBLE
    (*

    64-bit double precision

    *)
  3. | `EXTRA
    (*

    anything larger than 64-bit double precision floats

    *)
  4. | `REAL
    (*

    real arithmetic

    *)
]

Precision. All bounds are represented as double, whatever the precision.

Sourcetype round = [
  1. | `NEAR
    (*

    To nearest

    *)
  2. | `UP
    (*

    Upwards

    *)
  3. | `DOWN
    (*

    Downwards

    *)
  4. | `ZERO
    (*

    Towards 0

    *)
  5. | `ANY
    (*

    Any rounding mode

    *)
]

Rounding direction.

Constructors

Sourceval bot : t

Empty float set.

Sourceval pinf : t
Sourceval minf : t
Sourceval nan : t
Sourceval infinities : t
Sourceval specials : t

Special values.

Sourceval of_float : float -> float -> t

Float set reduced to an interval of non-special values. lo should not be +oo nor NaN. up should not be -oo nor NaN. We can have lo = -oo and up = +oo to represent sets of non-infinity floats larger than the range of double.

Sourceval of_interval : FI.t -> t
Sourceval of_interval_bot : FI.t_with_bot -> t
Sourceval hull : float -> float -> t

Constructs the smallest interval containing a and b.

Sourceval cst : float -> t

Singleton (possibly infinity or NaN).

Sourceval zero : t
Sourceval one : t
Sourceval two : t
Sourceval mone : t
Sourceval zero_one : t
Sourceval mone_zero : t
Sourceval mone_one : t
Sourceval mhalf_half : t

Useful intervals.

Sourceval add_special : t -> t

Adds NaN and infinities to a set.

Sourceval remove_special : t -> t

Removes NaN and infinities from a set.

Sourceval single : t

Non-special single precision floats.

Sourceval double : t

Non-special double precision floats.

Sourceval extra : t

Non-special extra (> double) precision.

Sourceval real : t

Reals.

Sourceval single_special : t

Single precision floats with specials.

Sourceval double_special : t

Double precision floats with specials.

Sourceval extra_special : t

Extra (> double) precision floats with specials.

Set-theoretic

Sourceval equal : t -> t -> bool

Set equality. = also works.

Sourceval included : t -> t -> bool

Set inclusion.

Sourceval intersect_finite : t -> t -> bool

Whether the finite parts of the sets have a non-empty intersection.

Sourceval intersect : t -> t -> bool

Whether the sets have an non-empty intersection.

Sourceval contains : float -> t -> bool

Whether the set contains a certain (finite, infinite or NaN) value.

Sourceval compare : t -> t -> int

A total ordering returning -1, 0, or 1.

Sourceval is_bot : t -> bool

Whether the argument is the empty set.

Sourceval is_finite : t -> bool

Whether the argument contains only finite values (or is empty).

Sourceval is_infinity : t -> bool

Whether the argument contains only infinities (or is empty).

Sourceval is_special : t -> bool

Whether the argument contains only special values (or is empty).

Sourceval is_zero : t -> bool

Whether the argument is the singleton 0.

Sourceval is_null : t -> bool

Whether the argument contains only 0 (or is empty).

Sourceval is_positive : t -> bool

Whether the argument contains only (possibly infinite) positive non-NaN values (or is empty).

Sourceval is_negative : t -> bool

Whether the argument contains only (possibly infinite) negative non-NaN values (or is empty).

Sourceval is_positive_strict : t -> bool

Whether the argument contains only (possibly infinite) strictly positive non-NaN values (or is empty).

Sourceval is_negative_strict : t -> bool

Whether the argument contains only (possibly infinite) strictly negative non-NaN values (or is empty).

Sourceval is_nonzero : t -> bool

Whether the argument contains only (possibly infinite or NaN) non-zero values (or is empty).

Sourceval approx_size : t -> int
Sourceval is_singleton : t -> bool

Whether the argument contains only a single element.

Sourceval contains_finite : t -> bool

Whether the argument contains at least one finite value.

Sourceval contains_infinity : t -> bool

Whether the argument contains an infinity.

Sourceval contains_special : t -> bool

Whether the argument contains an infinity or NaN.

Sourceval contains_zero : t -> bool

Whether the argument contains 0.

Sourceval contains_nonzero : t -> bool

Whether the argument contains a (possibly NaN or infinite) non-0 value.

Sourceval contains_positive : t -> bool

Whether the argument contains a (possibly infinite) positive value.

Sourceval contains_negative : t -> bool

Whether the argument contains a (possibly infinite) negative value.

Sourceval contains_positive_strict : t -> bool

Whether the argument contains a (possibly infinite) strictly positive value.

Sourceval contains_negative_strict : t -> bool

Whether the argument contains a (possibly infinite) strictly negative value.

Sourceval contains_non_nan : t -> bool

Whether the argument contains a non-NaN value.

Sourceval is_in_range : t -> float -> float -> bool

Whether the argument contains only finite values, and they are included in the range lo,up.

Sourceval join : t -> t -> t
Sourceval join_list : t list -> t
Sourceval meet : t -> t -> t
Sourceval widen : t -> t -> t
Sourceval positive : t -> t

Positive part of the argument, excluding NaN.

Sourceval negative : t -> t

Negative part of the argument, excluding NaN.

Sourceval meet_zero : t -> t

Intersects with

(excluding infinities and NaN).

Printing

Sourcetype print_format = FI.print_format
Sourceval to_string : print_format -> t -> string
Sourceval print : print_format -> Stdlib.out_channel -> t -> unit
Sourceval fprint : print_format -> Stdlib.Format.formatter -> t -> unit
Sourceval bprint : print_format -> Stdlib.Buffer.t -> t -> unit

C predicates

Sourceval is_log_eq : t -> t -> bool
Sourceval is_log_leq : t -> t -> bool
Sourceval is_log_lt : t -> t -> bool
Sourceval is_log_geq : t -> t -> bool
Sourceval is_log_gt : t -> t -> bool
Sourceval is_log_neq : t -> t -> bool

C comparison tests. Returns true if the test may succeed, false if it cannot. Note that NaN always compares different to all values (including NaN).

Sourceval is_log_leq_false : t -> t -> bool
Sourceval is_log_lt_false : t -> t -> bool
Sourceval is_log_geq_false : t -> t -> bool
Sourceval is_log_gt_false : t -> t -> bool
Sourceval is_log_eq_false : t -> t -> bool
Sourceval is_log_neq_false : t -> t -> bool

Returns true if the test may fail, false if it cannot. Due to NaN, which compare always different, <= (resp. >) do not return the boolean negation of > (resp. <). However, == is the negation of != even for NaN.

Forward arithmetic

Sourceval fix_itv : prec -> t -> t
Sourceval neg : t -> t

Negation.

Sourceval abs : t -> t

Absolute value.

Sourceval fix_prec : prec -> FI.prec
Sourceval add : prec -> round -> t -> t -> t

Addition.

Sourceval sub : prec -> round -> t -> t -> t

Subtraction.

Sourceval mul : prec -> round -> t -> t -> t

Multiplication.

Sourceval div : prec -> round -> t -> t -> t

Division.

Sourceval fmod : prec -> round -> t -> t -> t

Remainder (modulo).

Sourceval square : prec -> round -> t -> t

Square.

Sourceval sqrt : prec -> round -> t -> t

Square root.

Sourceval round_int : prec -> round -> t -> t

Round to integer.

Sourceval round : prec -> round -> t -> t

Round to float.

Sourceval of_int : prec -> round -> int -> int -> t

Conversion from integer range.

Sourceval of_int64 : prec -> round -> int64 -> int64 -> t

Conversion from int64 range.

Sourceval of_z : prec -> round -> Z.t -> Z.t -> t

Conversion from integer range.

Sourceval to_z : t -> (Z.t * Z.t) Utils_core.Bot.with_bot

Conversion to integer range with truncation. NaN and infinities are discarded.

Sourceval of_float_prec : prec -> round -> float -> float -> t

From bounds, with rounding, precision and handling of specials.

Sourceval of_int_itv : prec -> round -> II.t -> t

Conversion from integer intervals (handling overflows to infinities).

Sourceval of_int_itv_bot : prec -> round -> II.t Utils_core.Bot.with_bot -> t

Conversion from integer intervals (handling overflows to infinities).

Conversion to integer interval with truncation. Handles infinities.

Filters

Sourceval filter_eq : prec -> t -> t -> t * t
Sourceval lift_filter_itv : (FI.t -> FI.t -> ('a * 'b) Utils_core.Bot.with_bot) -> t -> t -> 'a Utils_core.Bot.with_bot * 'b Utils_core.Bot.with_bot
Sourceval filter_leq : prec -> t -> t -> t * t
Sourceval filter_lt : prec -> t -> t -> t * t

C comparison filters. Keep the parts of the arguments that can satisfy the condition. NaN is assumed to be different from any value (including NaN).

Sourceval filter_geq : prec -> t -> t -> t * t
Sourceval filter_gt : prec -> t -> t -> t * t
Sourceval filter_neq : prec -> t -> t -> t * t
Sourceval filter_nonzero : prec -> t -> t
Sourceval filter_zero : prec -> t -> t

Refine both arguments assuming that the test is true.

Sourceval filter_leq_false : prec -> t -> t -> t * t
Sourceval filter_lt_false : prec -> t -> t -> t * t
Sourceval filter_geq_false : prec -> t -> t -> t * t
Sourceval filter_gt_false : prec -> t -> t -> t * t
Sourceval filter_eq_false : prec -> t -> t -> t * t
Sourceval filter_neq_false : prec -> t -> t -> t * t
Sourceval filter_zero_false : prec -> t -> t
Sourceval filter_nonzero_false : prec -> t -> t

Refine both arguments assuming that the test is false.

Backward arithmetic

Sourceval bwd_neg : t -> t -> t

Backward negation.

Sourceval bwd_abs : t -> t -> t

Backward absolute value.

Sourceval bwd_generic2 : prec -> round -> (FI.prec -> round -> FI.t -> FI.t -> FI.t -> (FI.t * FI.t) Utils_core.Bot.with_bot) -> t -> t -> t -> t * t
Sourceval bwd_add : prec -> round -> t -> t -> t -> t * t

Backward addition.

Sourceval bwd_sub : prec -> round -> t -> t -> t -> t * t

Backward subtraction.

Sourceval bwd_mul : prec -> round -> t -> t -> t -> t * t

Backward multiplication.

Sourceval bwd_div : prec -> round -> t -> t -> t -> t * t

Backward division.

Sourceval bwd_fmod : prec -> round -> t -> t -> t -> t * t

Backward modulo.

Sourceval bwd_generic1 : prec -> round -> (FI.prec -> round -> FI.t -> FI.t -> FI.t Utils_core.Bot.with_bot) -> t -> t -> t
Sourceval bwd_round_int : prec -> round -> t -> t -> t

Backward rounding to int.

Sourceval bwd_round : prec -> round -> t -> t -> t

Backward rounding to float.

Sourceval bwd_square : prec -> round -> t -> t -> t

Backward square.

Sourceval bwd_sqrt : prec -> round -> t -> t -> t

Backward square root.

Sourceval bwd_of_int_itv : prec -> round -> II.t -> t -> II.t_with_bot

Backward conversion from integer interval.

Sourceval bwd_to_int_itv : t -> II.t -> t

Backward conversion to integer interval (with truncation).