Commit d7aee29b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improve documentation a bit.

parent bdc7fc0d
......@@ -48,9 +48,9 @@ Section Binary.
Implicit Arguments exist [[A] [P]].
(** prec is the number of bits of the mantissa including the implicit one
emax is the exponent of the infinities
Typically p=24 and emax = 128 in single precision *)
(** [prec] is the number of bits of the mantissa including the implicit one;
[emax] is the exponent of the infinities.
For instance, binary32 is defined by [prec = 24] and [emax = 128]. *)
Variable prec emax : Z.
Context (prec_gt_0_ : Prec_gt_0 prec).
Hypothesis Hmax : (prec < emax)%Z.
......@@ -74,8 +74,7 @@ Definition valid_binary x :=
end.
(** Basic type used for representing binary FP numbers.
Note that there is exactly one such object per FP datum.
NaNs do not have any payload. They cannot be distinguished. *)
Note that there is exactly one such object per FP datum. *)
Definition nan_pl := {pl | (Zpos (digits2_pos pl) <? prec)%Z = true}.
......@@ -382,6 +381,8 @@ Proof.
now intros [| |? []|].
Qed.
(** Opposite *)
Definition Bopp opp_nan x :=
match x with
| B754_nan sx plx =>
......@@ -647,7 +648,8 @@ generalize (prec_gt_0 prec).
clear -Hmax ; omega.
Qed.
(** mantissa, round and sticky bits *)
(** Truncation *)
Record shr_record := { shr_m : Z ; shr_r : bool ; shr_s : bool }.
Definition shr_1 mrs :=
......@@ -827,6 +829,8 @@ intros H.
now inversion H.
Qed.
(** Rounding modes *)
Inductive mode := mode_NE | mode_ZR | mode_DN | mode_UP | mode_NA.
Definition round_mode m :=
......@@ -1178,6 +1182,8 @@ destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Hx], y as [sy|sy|sy [ply Hply]|sy my
apply B2FF_FF2B.
Qed.
(** Normalization and rounding *)
Definition shl_align mx ex ex' :=
match (ex' - ex)%Z with
| Zneg d => (shift_pos d mx, ex')
......@@ -1361,6 +1367,7 @@ now apply F2R_lt_0_compat.
Qed.
(** Addition *)
Definition Bplus plus_nan m x y :=
let f pl := B754_nan (fst pl) (snd pl) in
match x, y with
......@@ -1542,6 +1549,8 @@ now apply f_equal.
apply Sz.
Qed.
(** Subtraction *)
Definition Bminus minus_nan m x y := Bplus minus_nan m x (Bopp pair y).
Theorem Bminus_correct :
......@@ -1571,6 +1580,7 @@ rewrite is_finite_Bopp. auto. now destruct y as [ | | | ].
Qed.
(** Division *)
Definition Fdiv_core_binary m1 e1 m2 e2 :=
let d1 := Zdigits2 m1 in
let d2 := Zdigits2 m2 in
......@@ -1737,6 +1747,7 @@ now rewrite B2FF_FF2B.
Qed.
(** Square root *)
Definition Fsqrt_core_binary m e :=
let d := Zdigits2 m in
let s := Zmax (2 * prec - d) 0 in
......
......@@ -21,7 +21,7 @@ Require Import ZArith.
Require Import Zquot.
Require Import Fcore_Zaux.
(** Computes the number of bits (radix 2) of a positive integer.
(** Number of bits (radix 2) of a positive integer.
It serves as an upper bound on the number of digits to ensure termination.
*)
......@@ -466,6 +466,8 @@ now apply Hd.
now rewrite 3!Zdigit_lt.
Qed.
(** Left and right shifts *)
Definition Zscale n k :=
if Zle_bool 0 k then (n * Zpower beta k)%Z else Z.quot n (Zpower beta (-k)).
......@@ -545,6 +547,8 @@ rewrite Zle_bool_true with (1 := Hk).
now apply Zscale_mul_pow.
Qed.
(** Slice of an integer *)
Definition Zslice n k1 k2 :=
if Zle_bool 0 k2 then Z.rem (Zscale n (-k1)) (Zpower beta k2) else Z0.
......@@ -756,6 +760,7 @@ Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z :=
End digits_aux.
(** Number of digits of an integer *)
Definition Zdigits n :=
match n with
| Z0 => Z0
......@@ -1011,7 +1016,7 @@ generalize (Zpower_gt_Zdigits e x).
omega.
Qed.
(** Characterizes the number digits of a product.
(** Number of digits of a product.
This strong version is needed for proofs of division and square root
algorithms, since they involve operation remainders.
......@@ -1126,6 +1131,8 @@ Qed.
End Fcore_digits.
(** Specialized version for computing the number of bits of an integer *)
Section Zdigits2.
Theorem Z_of_nat_S_digits2_Pnat :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment