Module `ItvUtils.Float`

Float - Floating-point arihmetics with rounding.

We rely on C code to provide functions with correct rounding (rounding direction and rounding precision).

Types

type t = float

type bit_float = {

sign : bool;
(*
sign bit (true means negative)
*)
fraction : Z.t;
(*
fraction bits
*)
exponent : int;
(*
exponent (positive, with bias)
*)

}

Bit-representation of a float value.

Global rounding direction

val set_round_near : unit -> unit

val set_round_up : unit -> unit

val set_round_down : unit -> unit

val set_round_zero : unit -> unit

Set the rounding mode globally. This affects the behaviors of all floating-point operations, including OCaml's native float operations, but excluding the operations in this module (and the float interval module) that specify a rounding direction.

Note that the operations with specified rounding directions may change the rounding direction globally in some unspecified way, and not reset it to its former value (this is done for efficiency).

Operations without rounding

val neg : t -> t

val abs : t -> t

val fmod : t -> t -> t

Remainder (fmod, not equivalent to IEEE 754's float remainder).

val infinite : int -> t

Constructs an infinity with the given sign. Zero maps to zero.

Predicates

val is_nan : t -> bool

val is_finite : t -> bool

Whether x is finite or not (infinite or NaN).

val is_infinite : t -> bool

val is_normal : t -> bool

val is_denormal : t -> bool

val sign : t -> int

Sign of x: -1 (negative), 0 (zero or NaN), or 1 (positive).

val sign_zero : t -> int

As sign, but zero is signed. Returns -1 (negative or -0), 0 (NaN), or 1 (positive of +0)

val equal : t -> t -> bool

Equality comparison. Identical to =, i.e., NaN ≠ NaN

val equal_nan : t -> t -> bool

As equal, but NaN equals NaN (and NaN ≠ non-NaN).

val leq : t -> t -> bool

val geq : t -> t -> bool

val lt : t -> t -> bool

val gt : t -> t -> bool

val eq : t -> t -> bool

val neq : t -> t -> bool

Comparison predicates. Returns false if one argument is NaN.

val min : t -> t -> t

val max : t -> t -> t

Minimum and maximum.

val is_zero : t -> bool

val is_nonzero : t -> bool

val is_positive : t -> bool

val is_negative : t -> bool

val is_positive_strict : t -> bool

val is_negative_strict : t -> bool

Sign predicates.

Printing

type print_format =

| Dfl
| Hex
(*
Control the printing of a float (precision, rounding, etc.).
*)

val dfl_fmt : print_format

Default format.

val hex_fmt : print_format

val to_string : print_format -> t -> string

val print : print_format -> out_channel -> t -> unit

val fprint : print_format -> Format.formatter -> t -> unit

val bprint : print_format -> Buffer.t -> t -> unit

Operations with specific rounding direction and precision

We provide the classic operations (and more) for single and double precision and all four rounding directions.

module Single : sig ... end

Single precision operations.

module Double : sig ... end

Double precision operations.

Operations with rounding mode as argument

type prec = [

| `SINGLE
(*
32-bit single precision
*)
| `DOUBLE
(*
64-bit double precision
*)

]

Precision.

type round = [

| `NEAR
(*
To nearest
*)
| `UP
(*
Upwards
*)
| `DOWN
(*
Downwards
*)
| `ZERO
(*
Towards 0
*)

]

Rounding direction.

val add : prec -> round -> t -> t -> t

Addition.

val sub : prec -> round -> t -> t -> t

Subtraction.

val mul : prec -> round -> t -> t -> t

Multiplication.

val mulz : prec -> round -> t -> t -> t

Multiplication, where 0 * infinity is 0, not Nan.

val div : prec -> round -> t -> t -> t

Division.

val divz : prec -> round -> t -> t -> t

Division, where 0 / 0 is 0, not Nan.

val rem : prec -> round -> t -> t -> t

Modulo.

val square : prec -> round -> t -> t

Square.

val sqrt : prec -> round -> t -> t

Square root.

val round : prec -> round -> t -> t

val round_int : prec -> round -> t -> t

Rounds to integer (the result remains a float).

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

Conversion from int.

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

Conversion from int64.

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

Conversion from Z.t

val of_string : prec -> [ `DOWN | `UP ] -> string -> t

Conversion from string, with safe rounding.

val succ : prec -> t -> t

Number immediately after.

val pred : prec -> t -> t

Number immediately before.

val succ_zero : prec -> t -> t

Number immediately after. Does not cross zero.

val pred_zero : prec -> t -> t

Number immediately before. Does not cross zero.

val mantissa_bits : prec -> int

val exponent_bits : prec -> int

val exponent_bias : prec -> int

val min_exponent : prec -> int

val max_exponent : prec -> int

val nan_infinity_exponent : prec -> int

val min_denormal : prec -> t

val min_normal : prec -> t

val max_normal : prec -> t

val max_exact : prec -> t

val ulp : prec -> t

Useful constants.

val to_bits : prec -> float -> bit_float

val of_bits : prec -> bit_float -> float

Bit-level extraction.

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_utils/Mopsa_utils/ItvUtils/Float/index.html

Module `ItvUtils.Float`

Types

Global rounding direction

Operations without rounding

Predicates

Printing

Operations with specific rounding direction and precision

Operations with rounding mode as argument

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_utils/Mopsa_utils/ItvUtils/Float/index.html

Module ItvUtils.Float

Types

Global rounding direction

Operations without rounding

Predicates

Printing

Operations with specific rounding direction and precision

Operations with rounding mode as argument

dune-project
Dependency

Module `ItvUtils.Float`