An integer of type 'a t is between 0 and saturated.

The type parameter 'a is mul_safe if the integer is known not to overflow when multiplied with another mul_safe t.

The type parameter 'a is may_saturate if the integer is not known to be sufficiently small to prevent overflow during multiplication.

to_int x returns the underlying integer representing x.

0

1

2^62 - 1

We inherit the order over native integers.

a >! b is a > b. Avoids using to_int.

numbits x returns the number of bits used in the binary representation of x.

shift_right x y behaves like a logical shift of x by y bits to the right. y must be between 0 and 63.

shift_left x y behaves like a logical shift of x by y bits to the left. y must be between 0 and 63. In cases where x lsl y is overflowing, shift_left x y is saturated.

mul x y behaves like multiplication between native integers as long as its result stay below saturated. Otherwise, mul returns saturated.

mul_safe x returns a mul_safe t only if x does not trigger overflows when multiplied with another mul_safe t. More precisely, x is safe for fast multiplications if x < 2147483648.

mul_fast x y exploits the fact that x and y are known not to provoke overflows during multiplication to perform a mere multiplication.

scale_fast x y exploits the fact that x is known not to provoke overflows during multiplication to perform a multiplication faster than mul.

add x y behaves like addition between native integers as long as its result stay below saturated. Otherwise, add returns saturated.

succ x is like add one x

sub x y behaves like subtraction between native integers as long as its result stay positive. Otherwise, sub returns zero. This function assumes that x is not saturated.

sub_opt x y behaves like subtraction between native integers as long as its result stay positive. Otherwise, sub returns None.

ediv x y returns x / y. This operation never saturates, hence it is exactly the same as its native counterpart. y is supposed to be strictly greater than 0, otherwise this function raises Division_by_zero.

erem x y returns x mod y. y is supposed to be strictly greater than 0, otherwise this function raises Division_by_zero.

sqrt x returns the square root of x, rounded down.

of_int_opt x returns Some x if x >= 0 and x < saturated, and None otherwise.

of_z_opt x returns Some x if x >= 0 and x < saturated, and None otherwise.

When a saturated integer is sufficiently small (i.e. strictly less than 2147483648), we can assign it the type mul_safe S.t to use it within fast multiplications, named S.scale_fast and S.mul_fast.

The following function allows such type assignment but may raise an exception if the assumption is wrong. Therefore, mul_safe_exn should only be used to define toplevel values, so that these exceptions can only occur during startup.

mul_safe_of_int_exn x is the composition of of_int_opt and mul_safe in the option monad. This function raises Invalid_argument if x is not safe. This function should be used on integer literals that are obviously mul_safe.

safe_z z is of_z_opt x |> saturate_if_undef.

safe_int x is of_int_opt x |> saturate_if_undef.

to_z z is Z.of_int.

Encoding for t through the encoding for z integers.

Encoding for t through the encoding for non-negative integers.

A pretty-printer for native integers.

Syntax for simple representations.