Module ItvUtils.IntBoundSource

IntBound - Enriches arbitrary precision integers with +∞ and -∞.

Useful as interval bounds.

Types

Sourcetype t =
  1. | Finite of Z.t
  2. | MINF
    (*

    -∞

    *)
  3. | PINF
    (*

    +∞

    *)

Internal utilities

Constructors

Sourceval zero : t
Sourceval one : t
Sourceval minus_one : t

Useful constants

Sourceval of_int : int -> t
Sourceval of_int64 : int64 -> t

Exact conversion from machine integers.

Sourceval of_float : float -> t

Conversion with truncation from floats. Handles infinites. Raises an exception on NaNs.

Sourceval infinite : int -> t

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

Sourceval pow2 : int -> t

A power of two. The argument must be positive.

Predicates

Sourceval sign : t -> int

Sign of x: -1, 0, or 1.

Sourceval is_finite : t -> bool

Whether x is finite or not.

Sourceval equal : t -> t -> bool

Equality comparison. = also works.

Sourceval compare : t -> t -> int

Total order. Returns -1 (strictly smaller), 0 (equal), or 1 (strictly greater).

Sourceval leq : t -> t -> bool
Sourceval geq : t -> t -> bool
Sourceval lt : t -> t -> bool
Sourceval gt : t -> t -> bool
Sourceval eq : t -> t -> bool
Sourceval neq : t -> t -> bool

Comparison predicates.

Sourceval min : t -> t -> t
Sourceval max : t -> t -> t

Minimum and maximum.

Sourceval is_zero : t -> bool
Sourceval is_nonzero : t -> bool
Sourceval is_positive : t -> bool
Sourceval is_negative : t -> bool
Sourceval is_positive_strict : t -> bool
Sourceval is_negative_strict : t -> bool

Sign predicates.

Sourceval hash : t -> int

Hashing function.

Printing

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

Operators

Sourceval succ : t -> t

+1. Infinities are left unchanged.

Sourceval pred : t -> t

-1. Infinities are left unchanged.

Sourceval neg : t -> t

Negation.

Sourceval abs : t -> t

Absolute value.

Sourceval add : t -> t -> t

Addition. +∞ + -∞ is undefined (invalid argument exception).

Sourceval sub : t -> t -> t

Subtraction. +∞ - +∞ is undefined (invalid argument exception).

Sourceval mul : t -> t -> t

Multiplication. Always defined: +∞ * 0 = 0

Sourceval div : t -> t -> t

Division. Always defined: 0 / 0 = 0, x / +∞ = 0, x / 0 = sign(x) * ∞

Sourceval ediv : t -> t -> t

Euclidian division. Always defined: 0 / 0 = 0, x / +∞ = 0, x / 0 = sign(x) * ∞

Sourceval rem : t -> t -> t

Remainder. rem x y has the sign of x, rem x (-y) = rem x y, and rem x +∞ = x. rem +∞ y and rem x 0 are undefined (invalid argument exception).

Sourceval erem : t -> t -> t

Euclidian remainder. erem x y >= 0, rem x y < |b| and a = b * ediv a b + erem a b. rem +∞ y and rem x 0 are undefined (invalid argument exception).

Sourceval shift_left : t -> t -> t

Left bitshift. Undefined if the second argument is negative (invalid argument exception). Returns an infinity if the second argument is too large.

Sourceval shift_right : t -> t -> t

Right bitshift, rounding towards -∞. Undefined if the second argument is negative (invalid argument exception). Returns zero if the second argument is too large.

Sourceval shift_right_trunc : t -> t -> t

Right bitshift, rounding towards 0 (truncation). Undefined if the second argument is negative (invalid argument exception). Returns zero if the second argument is too large.

Sourceval only_finite : string -> (Z.t -> Z.t -> Z.t) -> t -> t -> t
Sourceval bit_or : t -> t -> t
Sourceval bit_xor : t -> t -> t
Sourceval bit_and : t -> t -> t

Bitwise operations. Undefined for infinites (invalid argument exception).

Sourceval pow : t -> t -> t

Power. Undefined if the second argument is negative or too large.