1 files changed, 3 insertions, 33 deletions
diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v
index 4d74edddab..d057d641da 100644
--- a/theories/Floats/FloatAxioms.v
+++ b/theories/Floats/FloatAxioms.v
@@ -1,8 +1,4 @@
-Require Import ZArith Int63 SpecFloat PrimFloat.
-
-(* Properties of the Binary64 IEEE 754 format *)
-Definition prec := 53%Z.
-Definition emax := 1024%Z.
+Require Import ZArith Int63 SpecFloat PrimFloat FloatOps.
 
 Notation valid_binary := (valid_binary prec emax).
 
@@ -12,32 +8,6 @@ Definition SF64sub := SFsub prec emax.
 Definition SF64div := SFdiv prec emax.
 Definition SF64sqrt := SFsqrt prec emax.
 
-Definition Prim2SF f :=
-  if is_nan f then S754_nan
-  else if is_zero f then S754_zero (get_sign f)
-       else if is_infinity f then S754_infinity (get_sign f)
-            else
-              let (r, exp) := frexp f in
-              let e := (exp - prec)%Z in
-              let (shr, e') := shr_fexp prec emax [| normfr_mantissa r |]%int63 e loc_Exact in
-              match shr_m shr with
-              | Zpos p => S754_finite (get_sign f) p e'
-              | Zneg _ | Z0 => S754_zero false (* must never occur *)
-              end.
-
-Definition SF2Prim ef :=
-  match ef with
-  | S754_nan => nan
-  | S754_zero false => zero
-  | S754_zero true => neg_zero
-  | S754_infinity false => infinity
-  | S754_infinity true => neg_infinity
-  | S754_finite s m e =>
-    let pm := of_int63 (of_Z (Zpos m)) in
-    let f := ldexp pm e in
-    if s then (-f)%float else f
-  end.
-
 Axiom Prim2SF_valid : forall x, valid_binary (Prim2SF x) = true.
 Axiom SF2Prim_Prim2SF : forall x, SF2Prim (Prim2SF x) = x.
 Axiom Prim2SF_SF2Prim : forall x, valid_binary x = true -> Prim2SF (SF2Prim x) = x.
@@ -62,5 +32,5 @@ Axiom sqrt_spec : forall x, Prim2SF (sqrt x) = SF64sqrt (Prim2SF x).
 Axiom of_int63_spec : forall n, Prim2SF (of_int63 n) = binary_normalize prec emax (to_Z n) 0%Z false.
 Axiom normfr_mantissa_spec : forall f, to_Z (normfr_mantissa f) = Z.of_N (SFnormfr_mantissa prec (Prim2SF f)).
 
-Axiom frexp_spec : forall f, let (m,e) := frexp f in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF f).
-Axiom ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2SF f) e.
+Axiom frshiftexp_spec : forall f, let (m,e) := frshiftexp f in (Prim2SF m, ((to_Z e) - (to_Z shift))%Z) = SFfrexp prec emax (Prim2SF f).
+Axiom ldshiftexp_spec : forall f e, Prim2SF (ldshiftexp f e) = SFldexp prec emax (Prim2SF f) ((to_Z e) - (to_Z shift)).