Commit 0d13c6bd authored by François Bobot's avatar François Bobot
Browse files

Add tests for farith2

parent f5fd1738
......@@ -248,7 +248,7 @@ module Z = Z (* zarith *)
(* Q *)
(* must be already normalize *)
let q_mk (den, num) = { Q.den; Q.num }
let q_mk (num, den) = { Q.den; Q.num }
let q_case f q = f q.Q.den q.Q.num
......
......@@ -20,6 +20,8 @@
(**************************************************************************)
open Base
module Format = Stdlib.Format
module Z = struct
include Z
......@@ -85,7 +87,7 @@ module F = struct
(Z.of_string m, Z.of_string e)
| None -> (Z.of_string s, Z.zero)
let of_q ~mw ~ew ~mode q = of_q (Z.of_int mw) (Z.of_int ew) mode q
let of_q ~mw ~ew mode q = of_q (Z.of_int mw) (Z.of_int ew) mode q
let of_bits ~mw ~ew z = of_bits (Z.of_int mw) (Z.of_int ew) z
let to_bits t = to_bits t
let nan ~mw ~ew = nan (Z.of_int mw) (Z.of_int ew)
......@@ -95,6 +97,23 @@ module F = struct
let is_infinite t = match t.value with B754_infinity _ -> true | _ -> false
let is_nan t = match t.value with B754_nan -> true | _ -> false
let round ~mw ~ew mode (f:t) : t =
(match f.value with
| B754_zero _
| B754_infinity _
| B754_nan -> { mw = Z.of_int mw; ew = Z.of_int ew; value = f.value }
| B754_finite (_, _, _) ->
(of_q ~mw ~ew mode (to_q f))
)
let of_float f = of_bits ~mw:52 ~ew:11
@@ Z.extract (Z.of_int64 (Int64.bits_of_float f)) 0 64
let to_float mode f = round ~mw:52 ~ew:11 mode f
|> to_bits
|> fun z -> Z.signed_extract z 0 64
|> Z.to_int64
|> Int64.float_of_bits
let is_negative t =
match t.value with
| B754_zero true | B754_finite (true, _, _) -> true
......
......@@ -46,7 +46,7 @@ module F : sig
val pp : Format.formatter -> t -> unit
val of_q : mw:int -> ew:int -> mode:mode -> Q.t -> t
val of_q : mw:int -> ew:int -> mode -> Q.t -> t
val to_q : t -> Q.t
......@@ -74,6 +74,12 @@ module F : sig
val to_bits : t -> Z.t
val of_float : float -> t
val to_float : mode -> t -> float
val round: mw:int -> ew:int -> mode -> t -> t
val ge : t -> t -> bool
val gt : t -> t -> bool
......@@ -133,6 +139,8 @@ module I : sig
val is_singleton : t -> F.t option
end
val flocq_version: Z.t
(* (\** {2 Generic Version } *\)
*
*
......
[F] 0.100000 : +3602879701896397p-55
open Format
module G = Farith.B64
open Farith2
let f_convert r =
let fp = F.of_float r in
printf "[F] %f : %a@." r F.pp fp ; fp
let g_convert r =
let fp = G.of_float r in
printf "[G] %f : %a@." r G.pp fp ; fp
let () =
begin
ignore (g_convert 0.1) ;
ignore (f_convert 0.1) ;
end
[F] 3.1 = +6980579422424269p-51
[Fp] 3.1 = +6501171p-21
[Fq] 3.1 = +6501171p-21
-----------------------
Simple Roundings
-----------------------
Q=31/10
[F-NE] +6980579422424269p-51
[F-NE] -6980579422424269p-51
-----------------------
Q=31/10
[F-NA] +6980579422424269p-51
[F-NA] -6980579422424269p-51
-----------------------
Q=31/10
[F-ZR] +1745144855606067p-49
[F-ZR] -1745144855606067p-49
-----------------------
Q=31/10
[F-UP] +6980579422424269p-51
[F-UP] -1745144855606067p-49
-----------------------
Q=31/10
[F-DN] +1745144855606067p-49
[F-DN] -6980579422424269p-51
-----------------------
Tie Breaks (NE)
-----------------------
Q=562949953421313/562949953421312
[F-NE-ex] +562949953421313p-49
[F-NE-ex] -562949953421313p-49
-----------------------
Q=2251799813685253/2251799813685248
[F-NE-lo] +2251799813685253p-51
[F-NE-lo] -2251799813685253p-51
-----------------------
Q=1125899906842627/1125899906842624
[F-NE-ti] +1125899906842627p-50
[F-NE-ti] -1125899906842627p-50
-----------------------
Q=2251799813685255/2251799813685248
[F-NE-up] +2251799813685255p-51
[F-NE-up] -2251799813685255p-51
-----------------------
Tie Breaks (NA)
-----------------------
Q=562949953421313/562949953421312
[F-NA-ex] +562949953421313p-49
[F-NA-ex] -562949953421313p-49
-----------------------
Q=2251799813685253/2251799813685248
[F-NA-lo] +2251799813685253p-51
[F-NA-lo] -2251799813685253p-51
-----------------------
Q=1125899906842627/1125899906842624
[F-NA-ti] +1125899906842627p-50
[F-NA-ti] -1125899906842627p-50
-----------------------
Q=2251799813685255/2251799813685248
[F-NA-up] +2251799813685255p-51
[F-NA-up] -2251799813685255p-51
module F = Farith2.F
module G = Farith.B64
let gpp mode fmt q = G.pp fmt (G.of_q mode q)
let fpp mode fmt q = F.pp fmt (F.of_qint ~mode ~bits:F.b64 q)
let fpp mode fmt q = F.pp fmt (F.of_q mode ~mw:52 ~ew:11 q)
let () =
begin
Format.printf "[G] 3.1 = %a@." G.pp (G.of_float 3.1) ;
Format.printf "[F] 3.1 = %a@." F.pp (F.of_float 3.1) ;
let f = (F.of_float 3.1) in
Format.printf "[F] 3.1 = %a@." F.pp f;
let q = Q.make (Z.of_int 31) (Z.of_int 10) in
Format.printf "[Fp] 3.1 = %a@." F.pp (F.round ~mode:F.ZR ~bits:25 (F.of_float 3.1)) ;
Format.printf "[Fq] 3.1 = %a@." F.pp (F.of_qint ~mode:F.ZR ~bits:25 q) ;
Format.printf "[Fp] 3.1 = %a@." F.pp (F.round ~mw:24 ~ew:11 ZR (F.of_float 3.1)) ;
Format.printf "[Fq] 3.1 = %a@." F.pp (F.of_q ~mw:24 ~ew:11 ZR q) ;
Format.printf "-----------------------@." ;
Format.printf " Simple Roundings@." ;
let job m m1 m2 q =
let job m m2 q =
begin
Format.printf "-----------------------@." ;
Format.printf "Q=%a@." Q.pp_print q ;
Format.printf "[G-%s] %a@." m (gpp m1) q ;
Format.printf "[F-%s] %a@." m (fpp m2) q ;
Format.printf "[G-%s] %a@." m (gpp m1) (Q.neg q) ;
Format.printf "[F-%s] %a@." m (fpp m2) (Q.neg q) ;
end in
job "NE" Farith.NE F.NE q ;
job "NA" Farith.NA F.NA q ;
job "ZR" Farith.ZR F.ZR q ;
job "UP" Farith.UP F.UP q ;
job "DN" Farith.DN F.DN q ;
job "NE" Farith2.NE q ;
job "NA" Farith2.NA q ;
job "ZR" Farith2.ZR q ;
job "UP" Farith2.UP q ;
job "DN" Farith2.DN q ;
Format.printf "-----------------------@." ;
Format.printf " Tie Breaks (NE)@." ;
let eps = Z.shift_left Z.one 51 in
......@@ -34,14 +30,14 @@ let () =
let e_lo = Q.make (Z.of_int 0b101) eps in
let e_ti = Q.make (Z.of_int 0b110) eps in
let e_up = Q.make (Z.of_int 0b111) eps in
job "NE-ex" Farith.NE F.NE (Q.add Q.one e_ex) ;
job "NE-lo" Farith.NE F.NE (Q.add Q.one e_lo) ;
job "NE-ti" Farith.NE F.NE (Q.add Q.one e_ti) ;
job "NE-up" Farith.NE F.NE (Q.add Q.one e_up) ;
job "NE-ex" Farith2.NE (Q.add Q.one e_ex) ;
job "NE-lo" Farith2.NE (Q.add Q.one e_lo) ;
job "NE-ti" Farith2.NE (Q.add Q.one e_ti) ;
job "NE-up" Farith2.NE (Q.add Q.one e_up) ;
Format.printf "-----------------------@." ;
Format.printf " Tie Breaks (NA)@." ;
job "NA-ex" Farith.NA F.NA (Q.add Q.one e_ex) ;
job "NA-lo" Farith.NA F.NA (Q.add Q.one e_lo) ;
job "NA-ti" Farith.NA F.NA (Q.add Q.one e_ti) ;
job "NA-up" Farith.NA F.NA (Q.add Q.one e_up) ;
job "NA-ex" Farith2.NA (Q.add Q.one e_ex) ;
job "NA-lo" Farith2.NA (Q.add Q.one e_lo) ;
job "NA-ti" Farith2.NA (Q.add Q.one e_ti) ;
job "NA-up" Farith2.NA (Q.add Q.one e_up) ;
end
of-float 1p1023 = +1p1023 (normal)
of-float 1p1024 = +∞ (infinity)
of-float 1p-1022 = +1p-1022 (normal)
of-float 1p-1023 = +1p-1023 (sub-normal)
of-float 1p-1048 = +1p-1048 (sub-normal)
of-float 1p-1074 = +1p-1074 (sub-normal)
of-float 1p-1075 = +0 (zero)
open Farith2
let eps n = Stdlib.ldexp 1.0 n
......@@ -14,28 +15,25 @@ let pp_class fmt u =
let test_of_float n =
let u = eps n in
try
let f = F.of_float u in
Format.printf "of-float 1p%d = %a (%a)@." n F.pp f pp_class u
with F.Undefined ->
Format.printf "of-float 1p%d = undefined (%a)@." n pp_class u
let test_to_float n =
begin
let u = eps n in
let f = F.power2 n in
let v = F.to_float f in
Format.printf "to-float %a = %f (%a)@." F.pp f v pp_class v ;
let fu,eu = Stdlib.frexp u in
let fv,ev = Stdlib.frexp v in
Format.printf " expected = %fp%d@\n" fu eu ;
Format.printf " obtained = %fp%d@." fv ev ;
end
(* let test_to_float n =
* begin
* let u = eps n in
* let f = F.power2 n in
* let v = F.to_float f in
* Format.printf "to-float %a = %f (%a)@." F.pp f v pp_class v ;
* let fu,eu = Stdlib.frexp u in
* let fv,ev = Stdlib.frexp v in
* Format.printf " expected = %fp%d@\n" fu eu ;
* Format.printf " obtained = %fp%d@." fv ev ;
* end *)
let limits = [ 1023;1024;-1022;-1023;-1048;-1074;-1075 ]
let () =
begin
List.iter test_of_float limits ;
List.iter test_to_float limits ;
(* List.iter test_to_float limits ; *)
end
Flocq version: 40000
Run tests with Farith2.F
0.100000 + 2.000000 = 2.100000
0.100000 : +3602879701896397p-55
2.000000 : +1p1
2.100000 : +4728779608739021p-51
-0.100000 + 2.000000 = 1.900000
-0.100000 : -3602879701896397p-55
2.000000 : +1p1
1.900000 : +4278419646001971p-51
-0.100000 + -2.000000 = -2.100000
-0.100000 : -3602879701896397p-55
-2.000000 : -1p1
-2.100000 : -4728779608739021p-51
0.100000 + -2.000000 = -1.900000
0.100000 : +3602879701896397p-55
-2.000000 : -1p1
-1.900000 : -4278419646001971p-51
......@@ -2,45 +2,25 @@ open Format
let () =
printf "Flocq version: %a@."
Z.pp_print Farith.flocq_version
Z.pp_print Farith2.flocq_version
module type Tested = sig
val name: string
type t
val of_float : float -> t
val to_float : t -> float
val add : t -> t -> t
val pp : Format.formatter -> t -> unit
end
open Farith2
module Run(T:Tested) = struct
module Run = struct
let () =
printf "@[<3>Run tests with %s@\n" T.name;
printf "@[<3>Run tests with %s@\n" "Farith2.F";
let add u v =
let fu = T.of_float u in
let fv = T.of_float v in
let fr = T.add fu fv in
let r = T.to_float fr in
let fu = F.of_float u in
let fv = F.of_float v in
let fr = F.add NE fu fv in
let r = F.to_float NE fr in
printf "%f + %f = %f@\n" u v r;
printf "%f : %a@\n" u T.pp fu;
printf "%f : %a@\n" v T.pp fv;
printf "%f : %a@]@\n" r T.pp fr;
printf "%f : %a@\n" u F.pp fu;
printf "%f : %a@\n" v F.pp fv;
printf "%f : %a@]@\n" r F.pp fr;
in
add (0.1) (2.0);
add (-.0.1) (2.0);
add (-.0.1) (-.2.0);
add (0.1) (-.2.0)
end
module E1 = Run(struct
let name = "Farith"
include Farith.B64
let add = Farith.B64.add Farith.ZR
end)
module E2 = Run(struct
let name = "F"
include F
let to_float = to_float ~mode:F.NE
let add x y = F.round_f64 ~mode:F.ZR (F.add x y)
let pp = F.pretty
end)
------------------------------------------
- +4503599627370496 (+1p52)
1p52+1/2 = +9007199254740993p-1 (+9007199254740993p-1)
+ +4503599627370497 (+4503599627370497)
mantissa = 9007199254740992
=NE +1p52
+NE +1p52 (+4503599627370496)
-NE -1p52 (-4503599627370496)
=NA +4503599627370497p0
+NA +4503599627370497 (+4503599627370497)
-NA -4503599627370497 (-4503599627370497)
------------------------------------------
- +4503599627370497 (+4503599627370497)
1p52+3/2 = +9007199254740995p-1 (+9007199254740995p-1)
+ +4503599627370498 (+2251799813685249p1)
mantissa = 9007199254740992
=NE +2251799813685249p1
+NE +2251799813685249p1 (+4503599627370498)
-NE -2251799813685249p1 (-4503599627370498)
=NA +2251799813685249p1
+NA +2251799813685249p1 (+4503599627370498)
-NA -2251799813685249p1 (-4503599627370498)
open Farith2
let pp fmt z =
let n = F.exponent z in
let a = F.mantissa z in
if 0 <= Z.sign a then Format.pp_print_char fmt '+' ;
if n >= 0
then
Z.pp_print fmt (Z.shift_left a n)
else
Format.fprintf fmt "%ap%d" Z.pp_print a n
(** not tested *)
let tiebreak a b n =
begin
......@@ -18,7 +11,7 @@ let tiebreak a b n =
let f0 = F.of_qint ~bits:(n+1) q in (* exact *)
let f1,f2 = F.seize ~bits:n f0 in
Format.printf "------------------------------------------@\n" ;
Format.printf " - %a (%a)@\n" pp f1 F.pp f1 ;
Format.printf " - %a (%a)@\n" F.pp f1 F.pp f1 ;
Format.printf "1p%d+%d/%d = %a (%a)@\n" m a b pp f0 F.pp f0 ;
Format.printf " + %a (%a)@\n" pp f2 F.pp f2 ;
Format.printf "mantissa = %a@\n" Z.pp_print (Z.shift_left Z.one n) ;
......@@ -27,13 +20,8 @@ let tiebreak a b n =
let pos_na = F.round ~mode:F.NA ~bits:n f0 in
let neg_ne = F.round ~mode:F.NE ~bits:n f1 in
let neg_na = F.round ~mode:F.NA ~bits:n f1 in
let module G = Farith.Make(struct let ew = 8 let mw = m end) in
let coq_ne = G.of_q Farith.NE q in
let coq_na = G.of_q Farith.NA q in
Format.printf "=NE %a@\n" G.pp coq_ne ;
Format.printf "+NE %a (%a)@\n" F.pp pos_ne pp pos_ne ;
Format.printf "-NE %a (%a)@\n" F.pp neg_ne pp neg_ne ;
Format.printf "=NA %a@\n" G.pp coq_na ;
Format.printf "+NA %a (%a)@\n" F.pp pos_na pp pos_na ;
Format.printf "-NA %a (%a)@\n" F.pp neg_na pp neg_na ;
Format.print_flush () ;
......
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