1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import PrimInt63 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.
Register float_comparison as kernel.ind_f_cmp.
Register float_class as kernel.ind_f_class.
(** ** The main type *)
(** [float]: primitive type for Binary64 floating-point numbers. *)
Primitive float := #float64_type.
(** ** Syntax support *)
Module Import PrimFloatNotationsInternalA.
Declare Scope float_scope.
Delimit Scope float_scope with float.
Bind Scope float_scope with float.
End PrimFloatNotationsInternalA.
Declare ML Module "float_syntax_plugin".
(** ** Floating-point operators *)
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_int63]: convert a primitive integer into a float value.
The value is rounded if need be. *)
Primitive of_int63 := #float64_of_int63.
(** Specification of [normfr_mantissa]:
- If the input is a float value with an absolute value inside $[0.5, 1.)$#[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. *)
Primitive normfr_mantissa := #float64_normfr_mantissa.
(** ** Exponent manipulation functions *)
(** [frshiftexp]: convert a float to fractional part in $[0.5, 1.)$#[0.5, 1.)#
and integer part. *)
Primitive frshiftexp := #float64_frshiftexp.
(** [ldshiftexp]: multiply a float by an integral power of 2. *)
Primitive ldshiftexp := #float64_ldshiftexp.
(** ** 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. *)
Primitive next_down := #float64_next_down.
(** ** 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).
Register infinity as num.float.infinity.
Register neg_infinity as num.float.neg_infinity.
Register nan as num.float.nan.
(** ** 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. (* note: 0 =? -0 with floats *)
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.
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.
|
