Commit 1ab6cf58 authored by François Bobot's avatar François Bobot
Browse files

[Flocq] Update

parent 61cd66dc
......@@ -190,6 +190,15 @@ let binary_normalize prec emax mode0 m e szero =
(fun m0 -> coq_SF2B prec emax (binary_round prec emax mode0 true m0 e))
m
(** val coq_Fplus_naive :
bool -> Farith_Big.big_int -> Farith_Big.big_int -> bool ->
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int **)
let coq_Fplus_naive sx mx ex sy my ey ez =
Farith_Big.add (cond_Zopp sx (Pervasives.fst (shl_align mx ex ez)))
(cond_Zopp sy (Pervasives.fst (shl_align my ey ez)))
(** val coq_Bplus :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
binary_float -> binary_float -> binary_float **)
......@@ -219,9 +228,7 @@ let coq_Bplus prec emax m x y =
| B754_nan -> B754_nan
| B754_finite (sy, my, ey) ->
let ez = Farith_Big.min ex ey in
binary_normalize prec emax m
(Farith_Big.add (cond_Zopp sx (Pervasives.fst (shl_align mx ex ez)))
(cond_Zopp sy (Pervasives.fst (shl_align my ey ez)))) ez
binary_normalize prec emax m (coq_Fplus_naive sx mx ex sy my ey ez) ez
(match m with
| Farith_Big.DN -> true
| _ -> false))
......@@ -257,8 +264,7 @@ let coq_Bminus prec emax m x y =
| B754_finite (sy, my, ey) ->
let ez = Farith_Big.min ex ey in
binary_normalize prec emax m
(Farith_Big.sub (cond_Zopp sx (Pervasives.fst (shl_align mx ex ez)))
(cond_Zopp sy (Pervasives.fst (shl_align my ey ez)))) ez
(coq_Fplus_naive sx mx ex (Pervasives.not sy) my ey ez) ez
(match m with
| Farith_Big.DN -> true
| _ -> false))
......
......@@ -73,6 +73,11 @@ val binary_normalize :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
Farith_Big.big_int -> Farith_Big.big_int -> bool -> binary_float
val coq_Fplus_naive :
bool -> Farith_Big.big_int -> Farith_Big.big_int -> bool ->
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int
val coq_Bplus :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
-> binary_float -> binary_float
......
open BinInt
open Binary
open SpecFloat
(** val join_bits :
Farith_Big.big_int -> Farith_Big.big_int -> bool -> Farith_Big.big_int ->
......@@ -28,15 +29,11 @@ let split_bits mw ew x =
Farith_Big.big_int **)
let bits_of_binary_float mw ew =
let prec = Farith_Big.add mw Farith_Big.one in
let emax =
Z.pow (Farith_Big.double Farith_Big.one)
(Farith_Big.sub ew Farith_Big.one)
in
let prec = Farith_Big.add mw Farith_Big.one in
let emin =
Farith_Big.sub
(Farith_Big.sub (Farith_Big.succ_double Farith_Big.one) emax) prec
in
(fun x ->
match x with
| B754_zero sx -> join_bits mw ew sx Farith_Big.zero Farith_Big.zero
......@@ -52,7 +49,8 @@ let bits_of_binary_float mw ew =
let m = Farith_Big.sub mx (Z.pow (Farith_Big.double Farith_Big.one) mw) in
if Farith_Big.le Farith_Big.zero m
then join_bits mw ew sx m
(Farith_Big.add (Farith_Big.sub ex emin) Farith_Big.one)
(Farith_Big.add (Farith_Big.sub ex (emin prec emax))
Farith_Big.one)
else join_bits mw ew sx mx Farith_Big.zero)
(** val binary_float_of_bits_aux :
......@@ -60,22 +58,18 @@ let bits_of_binary_float mw ew =
full_float **)
let binary_float_of_bits_aux mw ew =
let prec = Farith_Big.add mw Farith_Big.one in
let emax =
Z.pow (Farith_Big.double Farith_Big.one)
(Farith_Big.sub ew Farith_Big.one)
in
let prec = Farith_Big.add mw Farith_Big.one in
let emin =
Farith_Big.sub
(Farith_Big.sub (Farith_Big.succ_double Farith_Big.one) emax) prec
in
(fun x ->
let (p, ex) = split_bits mw ew x in
let (sx, mx) = p in
if Farith_Big.eq ex Farith_Big.zero
then (Farith_Big.z_case
(fun _ -> F754_zero sx)
(fun px -> F754_finite (sx, px, emin))
(fun px -> F754_finite (sx, px, (emin prec emax)))
(fun _ -> F754_nan (false, Farith_Big.one))
mx)
else if Farith_Big.eq ex
......@@ -89,7 +83,8 @@ let binary_float_of_bits_aux mw ew =
else (Farith_Big.z_case
(fun _ -> F754_nan (false, Farith_Big.one))
(fun px -> F754_finite (sx, px,
(Farith_Big.sub (Farith_Big.add ex emin) Farith_Big.one)))
(Farith_Big.sub (Farith_Big.add ex (emin prec emax))
Farith_Big.one)))
(fun _ -> F754_nan (false,
Farith_Big.one))
(Farith_Big.add mx
......@@ -100,9 +95,9 @@ let binary_float_of_bits_aux mw ew =
binary_float **)
let binary_float_of_bits mw ew x =
let prec = Farith_Big.add mw Farith_Big.one in
let emax =
Z.pow (Farith_Big.double Farith_Big.one)
(Farith_Big.sub ew Farith_Big.one)
in
let prec = Farith_Big.add mw Farith_Big.one in
coq_FF2B prec emax (binary_float_of_bits_aux mw ew x)
open BinInt
open Binary
open SpecFloat
val join_bits :
Farith_Big.big_int -> Farith_Big.big_int -> bool -> Farith_Big.big_int ->
......
......@@ -2,9 +2,8 @@
(** val coq_Flocq_version : Farith_Big.big_int **)
let coq_Flocq_version =
(Farith_Big.double (Farith_Big.succ_double (Farith_Big.double
(Farith_Big.double (Farith_Big.double (Farith_Big.double (Farith_Big.double
(Farith_Big.double (Farith_Big.double (Farith_Big.succ_double
(Farith_Big.double (Farith_Big.double (Farith_Big.double
(Farith_Big.succ_double (Farith_Big.succ_double (Farith_Big.double
(Farith_Big.succ_double (Farith_Big.succ_double (Farith_Big.double
(Farith_Big.succ_double (Farith_Big.succ_double
Farith_Big.one))))))))))))))
(Farith_Big.succ_double (Farith_Big.succ_double (Farith_Big.succ_double
(Farith_Big.double (Farith_Big.double Farith_Big.one)))))))))))))))
Supports Markdown
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