Library Coq.Floats.PrimFloat
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
The main type
float: primitive type for Binary64 floating-point numbers.
Primitive float := #
float64_type.
Primitive classify := #
float64_classify.
Primitive abs := #
float64_abs.
Primitive sqrt := #
float64_sqrt.
Primitive opp := #
float64_opp.
Primitive eqb := #
float64_eq.
Primitive ltb := #
float64_lt.
Primitive leb := #
float64_le.
Primitive compare := #
float64_compare.
Primitive mul := #
float64_mul.
Primitive add := #
float64_add.
Primitive sub := #
float64_sub.
Primitive div := #
float64_div.
Module Import PrimFloatNotationsInternalB.
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.
End PrimFloatNotationsInternalB.
Conversions
of_uint63: convert a primitive unsigned 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.
Primitive next_up := #
float64_next_up.
next_down: return the next float towards negative infinity.
Special values (needed for pretty-printing)
Definition infinity :=
Eval compute in div (
of_uint63 1) (
of_uint63 0).
Definition neg_infinity :=
Eval compute in opp infinity.
Definition nan :=
Eval compute in div (
of_uint63 0) (
of_uint63 0).
Register infinity as num.float.infinity.
Register neg_infinity as num.float.neg_infinity.
Register nan as num.float.nan.
Definition one :=
Eval compute in (
of_uint63 1).
Definition zero :=
Eval compute in (
of_uint63 0).
Definition neg_zero :=
Eval compute in (
-zero)%
float.
Definition two :=
Eval compute in (
of_uint63 2).
Predicates and helper functions
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.
Module Export PrimFloatNotations.
Local Open Scope float_scope.
#[
deprecated(
since="8.13",
note="use infix <? instead")]
Notation "x < y" := (
x <? y) (
at level 70,
no associativity) :
float_scope.
#[
deprecated(
since="8.13",
note="use infix <=? instead")]
Notation "x <= y" := (
x <=? y) (
at level 70,
no associativity) :
float_scope.
#[
deprecated(
since="8.13",
note="use infix =? instead")]
Notation "x == y" := (
x =? y) (
at level 70,
no associativity) :
float_scope.
Export PrimFloatNotationsInternalA.
Export PrimFloatNotationsInternalB.
End PrimFloatNotations.
#[
deprecated(
since="8.14",
note="Use of_uint63 instead.")]
Notation of_int63 :=
of_uint63 (
only parsing).