Add next_{up,down} primitive float functions

4 files changed, 41 insertions, 0 deletions

diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v
index d78e3192e7..142883171e 100644
--- a/theories/Floats/FloatAxioms.v
+++ b/theories/Floats/FloatAxioms.v
@@ -8,6 +8,8 @@ Definition SF64add := SFadd prec emax.
 Definition SF64sub := SFsub prec emax.
 Definition SF64div := SFdiv prec emax.
 Definition SF64sqrt := SFsqrt prec emax.
+Definition SF64succ := SFsucc prec emax.
+Definition SF64pred := SFpred prec emax.
 
 Axiom Prim2SF_valid : forall x, valid_binary (Prim2SF x) = true.
 Axiom SF2Prim_Prim2SF : forall x, SF2Prim (Prim2SF x) = x.
@@ -45,3 +47,6 @@ Axiom normfr_mantissa_spec : forall f, to_Z (normfr_mantissa f) = Z.of_N (SFnorm
 
 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)).
+
+Axiom next_up_spec : forall x, Prim2SF (next_up x) = SF64succ (Prim2SF x).
+Axiom next_down_spec : forall x, Prim2SF (next_down x) = SF64pred (Prim2SF x).
diff --git a/theories/Floats/FloatOps.v b/theories/Floats/FloatOps.v
index 8a3ec6c181..6cc7cb0568 100644
--- a/theories/Floats/FloatOps.v
+++ b/theories/Floats/FloatOps.v
@@ -13,6 +13,8 @@ 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))).
+
 Definition Prim2SF f :=
   if is_nan f then S754_nan
   else if is_zero f then S754_zero (get_sign f)
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index bc5c49d085..b84965a11a 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -50,6 +50,9 @@ Definition shift := (2101)%int63. (* = 2*emax + prec *)
 Primitive frshiftexp := #float64_frshiftexp.
 Primitive ldshiftexp := #float64_ldshiftexp.
 
+Primitive next_up := #float64_next_up.
+Primitive next_down := #float64_next_down.
+
 Local Open Scope float_scope.
 
 (* Special values *)
diff --git a/theories/Floats/SpecFloat.v b/theories/Floats/SpecFloat.v
index fc26ba8cab..900739812a 100644
--- a/theories/Floats/SpecFloat.v
+++ b/theories/Floats/SpecFloat.v
@@ -349,4 +349,35 @@ Section FloatOps.
         (S754_finite sx (shift_pos (Z.to_pos d) mx) (-prec), (ex+prec-d)%Z)
     | _ => (f, (-2*emax-prec)%Z)
     end.
+
+  Definition SFone := binary_round false 1 0.
+
+  Definition SFulp x := SFldexp SFone (fexp (snd (SFfrexp x))).
+
+  Definition SFpred_pos x :=
+    match x with
+    | S754_finite _ mx _ =>
+      let d :=
+        if (mx~0 =? shift_pos (Z.to_pos prec) 1)%positive then
+          SFldexp SFone (fexp (snd (SFfrexp x) - 1))
+        else
+          SFulp x in
+      SFsub x d
+    | _ => x
+    end.
+
+  Definition SFmax_float :=
+    S754_finite false (shift_pos (Z.to_pos prec) 1 - 1) (emax - prec).
+
+  Definition SFsucc x :=
+    match x with
+    | S754_zero _ => SFldexp SFone emin
+    | S754_infinity false => x
+    | S754_infinity true => SFopp SFmax_float
+    | S754_nan => x
+    | S754_finite false _ _ => SFadd x (SFulp x)
+    | S754_finite true _ _ => SFopp (SFpred_pos (SFopp x))
+    end.
+
+  Definition SFpred f := SFopp (SFsucc (SFopp f)).
 End FloatOps.