Library Coq.Floats.FloatOps

Require Import ZArith Int63 SpecFloat PrimFloat.

Derived operations and mapping between primitive floats and spec_floats

Definition prec := 53%Z.
Definition emax := 1024%Z.
Notation emin := (emin prec emax).

Definition shift := 2101%Z.
= 2*emax + prec

Definition frexp f :=
  let (m, se) := frshiftexp f in
  (m, (φ se - shift)%Z%int63).

Definition ldexp f e :=
  let e' := Z.max (Z.min e (emax - emin)) (emin - emax - 1) in
  ldshiftexp f (of_Z (e' + shift)).

Definition ulp f := ldexp one (fexp prec emax (snd (frexp f))).

Prim2SF is an injective function that will be useful to express the properties of the implemented Binary64 format (see FloatAxioms).
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)
              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

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