Library Coq.Floats.PrimFloat

Require Import Int63 FloatClass.

Definition of the interface for primitive floating-point arithmetic

This interface provides processor operators for the Binary64 format of the IEEE 754-2008 standard.

Type definition for the co-domain of compare

Variant float_comparison : Set := FEq | FLt | FGt | FNotComparable.



The main type

float: primitive type for Binary64 floating-point numbers.

Syntax support

Delimit Scope float_scope with float.


Floating-point operators




Notation "- x" := (opp x) : float_scope.

Notation "x == y" := (eqb x y) (at level 70, no associativity) : float_scope.

Notation "x < y" := (ltb x y) (at level 70, no associativity) : float_scope.

Notation "x <= y" := (leb x y) (at level 70, no associativity) : float_scope.

Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope.

Notation "x * y" := (mul x y) : float_scope.

Notation "x + y" := (add x y) : float_scope.

Notation "x - y" := (sub x y) : float_scope.

Notation "x / y" := (div x y) : float_scope.

Conversions

of_int63: convert a primitive integer into a float value. The value is rounded if need be.

Specification of normfr_mantissa:
  • If the input is a float value with an absolute value inside [0.5, 1.);
  • Then return its mantissa as a primitive integer. The mantissa will be a 53-bit integer with its most significant bit set to 1;
  • Else return zero.
The sign bit is always ignored.

Exponent manipulation functions

frshiftexp: convert a float to fractional part in [0.5, 1.) and integer part.

ldshiftexp: multiply a float by an integral power of 2.

Predecesor/Successor functions

next_up: return the next float towards positive infinity.

next_down: return the next float towards negative infinity.

Special values (needed for pretty-printing)

Definition infinity := Eval compute in div (of_int63 1) (of_int63 0).
Definition neg_infinity := Eval compute in opp infinity.
Definition nan := Eval compute in div (of_int63 0) (of_int63 0).


Other special values

Definition one := Eval compute in (of_int63 1).
Definition zero := Eval compute in (of_int63 0).
Definition neg_zero := Eval compute in (-zero)%float.
Definition two := Eval compute in (of_int63 2).

Predicates and helper functions

Definition is_nan f := negb (f == f)%float.

Definition is_zero f := (f == zero)%float.
Definition is_infinity f := (abs f == infinity)%float.

Definition is_finite (x : float) := negb (is_nan x || is_infinity x).

get_sign: return true for - sign, false for + sign.
Definition get_sign f :=
  let f := if is_zero f then (one / f)%float else f in
  (f < zero)%float.