Skip to content
GitLab
Commit 12421740 authored by François Bobot's avatar François Bobot
Browse files

Optimise by removing Let and precomputing some values

parent 81eafae0
Pipeline #594 failed with stage
Expand all Hide whitespace changes
Inline Side-by-side
F_aux.v
View file @ 12421740
......@@ -20,6 +20,8 @@
(**************************************************************************)
Require Import Fcore.
Require Import Fcore_digits.
Require Import Fcalc_bracket.
Require Import Fappli_IEEE.
Require Import Fappli_IEEE_bits.
Require Import QArith.
......@@ -28,6 +30,7 @@ Require Import Reals.
Require Import ZBits.
Parameter assert : forall (b:bool) (t:Type), ((b=true) -> t) -> t.
Definition Zcompare_to_zero := Zcompare Z.zero.
Fixpoint least_bit_Pnat (n : positive) :=
match n with
......@@ -175,30 +178,43 @@ Parameter hash_combine: nativeint -> nativeint -> nativeint.
Definition cprec_mw mw := (Z.succ mw).
Definition cemax_ew ew := Zpower 2 (ew - 1).
(* (if Z.eqb ew 1 then 1 else Z.pow_pos 2 (Z.to_pos (ew - 1)))%Z. *)
Record fconf (t:Type) :=
FConf { mw : Z;
ew : Z;
cprec : Z;
cemax : Z;
Hcprec : cprec = cprec_mw mw%Z;
Hcemax : cemax = cemax_ew ew;
(* (if Z.eqb ew 1 then 1 else Z.pow_pos 2 (Z.to_pos (ew - 1)))%Z. *)
cprec : { z | z = cprec_mw mw}%Z;
cemax : { z | z = cemax_ew ew}%Z;
max_mantisse : { m | m = (match (Zpower 2 (proj1_sig cprec) - 1)%Z with Zpos p => p | _ => xH end) };
max_exponent : {z | z = ((proj1_sig cemax) - (proj1_sig cprec))%Z};
emin : { z | z = (3 - (proj1_sig cemax) - (proj1_sig cprec))%Z };
Hmw : (0 < mw)%Z;
Hew : (0 < ew)%Z;
Hemax : (cprec < cemax)%Z;
Hprec : (0 < cprec)%Z;
Ht : t = binary_float cprec cemax
Hemax : (proj1_sig cprec < proj1_sig cemax)%Z;
Hprec : (0 < proj1_sig cprec)%Z;
Ht : t = binary_float (proj1_sig cprec) (proj1_sig cemax)%Z
}.
Definition check_param mw ew :=
andb (andb (0 <? mw)%Z (0 <? ew)%Z) (cprec_mw mw <? cemax_ew ew)%Z.
Definition mk_conf : forall mw ew, check_param mw ew = true -> fconf (binary_float (cprec_mw mw) (cemax_ew ew)).
Proof.
intros mw ew H.
refine (FConf _ mw ew (cprec_mw mw) (cemax_ew ew) (refl_equal _) (refl_equal _) _ _ _ _ (refl_equal _));
unfold check_param in H;
set (cprec := (cprec_mw mw)).
set (cemax := (cemax_ew ew)).
set (max_mantisse := (match (Zpower 2 cprec - 1)%Z with Zpos p => p | _ => xH end)).
set (max_exponent := (cemax - cprec)%Z).
set (emin := (3 - cemax - cprec)%Z).
refine (FConf _ mw ew
(exist _ cprec (refl_equal _))
(exist _ cemax (refl_equal _))
(exist _ max_mantisse (refl_equal _))
(exist _ max_exponent (refl_equal _))
(exist _ emin (refl_equal _))
_ _ _ _ (refl_equal _));
unfold check_param in H; unfold cprec, cemax; simpl;
rewrite !Bool.andb_true_iff in H;
rewrite <- !Zlt_is_lt_bool in H;
intuition.
......@@ -221,11 +237,11 @@ Section Direct.
Variable conf : fconf t'.
Let mw : Z := mw t' conf.
Let ew : Z := ew t' conf.
Let prec := cprec t' conf.
Let emax := cemax t' conf.
Let t := binary_float prec emax.
Definition mw : Z := mw t' conf.
Definition ew : Z := ew t' conf.
Definition prec := proj1_sig (cprec t' conf).
Definition emax := proj1_sig (cemax t' conf).
Definition t := binary_float prec emax.
Implicit Arguments B754_nan [[prec] [emax]].
Implicit Arguments B754_zero [[prec] [emax]].
......@@ -237,16 +253,16 @@ Section Direct.
Let Hprec : (0 < prec)%Z := Hprec t' conf.
Lemma Hemax' : (cprec_mw mw < cemax_ew ew)%Z.
Proof.
unfold mw, ew; clear.
destruct conf;simpl in *.
unfold mw, ew.
rewrite <- Hcprec0, <- Hcemax0.
rewrite <- (proj2_sig cprec0), <- (proj2_sig cemax0).
now trivial.
Qed.
Lemma Hprec' : (0 < cprec_mw mw)%Z.
Proof.
unfold mw, ew; clear.
destruct conf;simpl in *.
unfold mw, ew.
rewrite <- Hcprec0.
rewrite <- (proj2_sig cprec0).
now trivial.
Qed.
......@@ -265,8 +281,9 @@ Section Direct.
rewrite G;clear G.
rewrite Nat2Z.inj_succ.
rewrite Z2Nat.id;[rewrite Z.ltb_lt | ]. 2: omega.
unfold mw; clear.
destruct conf; simpl in *.
rewrite Hcprec0.
rewrite (proj2_sig cprec0).
auto with zarith.
Qed.
......@@ -297,8 +314,16 @@ Section Direct.
Definition of_bits := binary_float_of_bits mw ew Hmw Hew Hemax'.
Definition to_bits := bits_of_binary_float mw ew.
Let emin := (3 - emax - prec)%Z.
Let fexp := FLT_exp emin prec.
Lemma Hemin : (proj1_sig (emin _ conf)) = (3 - emax - prec)%Z.
Proof.
unfold emax, prec; clear.
destruct conf; destruct emin0 as [emin0 Hemin0]; simpl in *.
unfold emax; unfold prec.
rewrite Hemin0.
reflexivity.
Qed.
Let fexp := FLT_exp (proj1_sig (emin _ conf)) prec.
Definition of_correct mode szero r (f:t) :=
if Rlt_bool (Rabs (round radix2 fexp (round_mode mode) r)) (bpow radix2 emax) then
......@@ -321,6 +346,9 @@ Section Direct.
(F2R (Float radix2 mx ex))
(binary_normalize _ _ Hprec Hemax m mx ex szero).
Proof.
unfold of_correct.
unfold fexp.
rewrite Hemin.
exact (binary_normalize_correct _ _ Hprec Hemax).
Qed.
......@@ -383,6 +411,7 @@ Section Direct.
exact (Rinv_0_lt_compat _ Hy).
Qed.
(*
Lemma Bdiv_correct_aux' :
forall m sx mx ex sy my ey,
let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in
......@@ -427,10 +456,67 @@ Section Direct.
rewrite B2FF_FF2B;
exact correct.
Qed.
*)
(** copy function from IEEE in order to make them faster and to
compute the constants *)
(* Let emin := (3 - emax - prec)%Z. *)
(* Let fexp := FLT_exp emin prec. *)
Definition of_z mode z : t := binary_normalize _ _ Hprec Hemax mode z 0%Z false.
Definition shr_fexp_opt m e l :=
shr (shr_record_of_loc m l) e (fexp (Zdigits2 m + e) - e).
Definition binary_overflow_opt m s :=
if overflow_to_inf m s then F754_infinity s
else F754_finite s (proj1_sig (max_mantisse _ conf)) (proj1_sig (max_exponent _ conf)).
Definition binary_round_opt mode sx mx ex lx :=
let '(mrs', e') := shr_fexp_opt (Zpos mx) ex lx in
let '(mrs'', e'') := shr_fexp_opt (choice_mode mode sx (shr_m mrs') (loc_of_shr_record mrs')) e' loc_Exact in
let m := shr_m mrs'' in
match Zcompare_to_zero m with
| Eq => F754_zero sx
| Gt => if Zle_bool e'' (proj1_sig (max_exponent _ conf))
then F754_finite sx (Z.to_pos m) e''
else binary_overflow_opt mode sx
| Lt => F754_nan false xH (* dummy *)
end.
Definition Fdiv_core_binary_opt m1 e1 m2 e2 :=
let d1 := Zdigits2 m1 in
let d2 := Zdigits2 m2 in
let e := (e1 - e2)%Z in
let (m, e') :=
let p := (d2 + prec - d1)%Z in
match Zcompare_to_zero p with
| Gt => (Z.shiftl m1 p, e + Z.opp p)%Z
| _ => (m1, e)
end in
let '(q, r) := Z.quotrem m m2 in
(q, e', new_location m2 r loc_Exact).
Definition Bdiv_correct_opt m sx mx ex sy my ey :=
let '(mz, ez, lz) := Fdiv_core_binary_opt (Zpos mx) ex (Zpos my) ey in
binary_round_opt m (xorb sx sy) (Z.to_pos mz) ez lz.
Lemma Bdiv_correct_opt_correct m sx mx ex sy my ey :
Bdiv_correct_opt m sx mx ex sy my ey =
B2FF _ _ (FF2B _ _ _ (proj1 (Bdiv_correct_aux _ _ Hprec Hemax m sx mx ex sy my ey))).
Proof.
Admitted.
Definition Bdiv_correct_opt' : mode -> bool -> positive -> Z -> bool -> positive -> Z -> t.
Proof.
intros m sx mx ex sy my ey.
refine (FF2B _ _ (Bdiv_correct_opt m sx mx ex sy my ey) _).
rewrite Bdiv_correct_opt_correct.
apply valid_binary_B2FF.
Qed.
Definition of_z mode z : t := binary_normalize _ _ Hprec Hemax mode z 0%Z false.
(*
Theorem of_z_correct :
forall mode z, of_correct mode false (Z2R z) (of_z mode z).
Proof.
......@@ -440,7 +526,7 @@ Section Direct.
unfold F2R; simpl.
apply Rmult_1_r.
Qed.
*)
Definition default_nan : t := B754_nan (fst default_nan_pl) (snd default_nan_pl).
Definition of_q mode q : t :=
......@@ -450,21 +536,11 @@ Section Direct.
| Qz_MINF _ _ => B754_infinity true
| Qz_UNDEF _ _ => default_nan
| Qz_NZERO _ _ _ _ =>
match num q with
| Z0 => default_nan (** absurd *)
| Z.pos pn =>
FF2B _ _ _ (proj1 (Bdiv_correct_aux _ _ Hprec Hemax
mode
false pn 0%Z
false (Z.to_pos (den q)) 0%Z))
| Z.neg nn =>
FF2B _ _ _ (proj1 (Bdiv_correct_aux _ _ Hprec Hemax
mode
true nn 0%Z
false (Z.to_pos (den q)) 0%Z))
end
let b := match Zcompare_to_zero (num q) with Lt => true | _ => false end in
(Bdiv_correct_opt' mode b (Z.to_pos (num q)) 0%Z false (Z.to_pos (den q)) 0%Z)
end.
(*
Theorem of_q_correct :
forall mode q,
match Qz2Rplus q with
......@@ -510,7 +586,7 @@ Section Direct.
rewrite !Rmult_1_r.
reflexivity.
Qed.
*)
Lemma least_bit_shiftr_pos :
forall m (b:bool),
let e' := least_bit_Pnat m in
......@@ -943,16 +1019,16 @@ Section Direct.
Definition abs : t -> t. Proof. rewrite_type Aux.abs. Defined.
Definition of_bits : Z -> t. Proof.
set (of_bits := Aux.of_bits t conf).
destruct conf as [? ? ? ? ? ? ? ? ? ? Ht];simpl in *.
destruct conf as [? ? ? ? ? ? ? ? ? ? ? Ht];simpl in *.
rewrite Ht.
rewrite Hcprec0, Hcemax0.
rewrite (proj2_sig cprec0), (proj2_sig cemax0).
exact of_bits.
Defined.
Definition to_bits : t -> Z. Proof.
set (to_bits := Aux.to_bits t conf).
destruct conf as [? ? ? ? ? ? ? ? ? ? Ht];simpl in *.
destruct conf as [? ? ? ? ? ? ? ? ? ? ? Ht];simpl in *.
rewrite Ht.
rewrite Hcprec0, Hcemax0.
rewrite (proj2_sig cprec0), (proj2_sig cemax0).
exact to_bits.
Defined.
......@@ -983,7 +1059,7 @@ Section Direct.
Definition finite : mode -> Z.t -> Z.t -> t. Proof. rewrite_type Aux.finite. Defined.
Definition classify : t -> Fappli_IEEE.full_float. Proof. rewrite_type Aux.classify. Defined.
Definition cast_to_t (t:Type) (x:fconf t) : t -> binary_float (cprec _ x) (cemax _ x) :=
Definition cast_to_t (t:Type) (x:fconf t) : t -> binary_float (proj1_sig (cprec _ x)) (proj1_sig (cemax _ x)) :=
match Ht t x in Logic.eq _ x return t -> x with
| refl_equal => (fun x => x)
end.
......@@ -998,7 +1074,7 @@ Section Direct.
| B754_zero b => B754_zero _ _ b
| B754_nan b _ => B754_nan _ _ b (snd (Aux.default_nan_pl _ conf2))
| B754_infinity b => B754_infinity _ _ b
| B754_finite sx mx ex _ => FF2B _ _ _ (proj1 (binary_round_correct (cprec _ conf2) (cemax _ conf2) (Hprec _ conf2) (Hemax _ conf2) mode sx mx ex))
| B754_finite sx mx ex _ => FF2B _ _ _ (proj1 (binary_round_correct (proj1_sig (cprec _ conf2)) (proj1_sig (cemax _ conf2)) (Hprec _ conf2) (Hemax _ conf2) mode sx mx ex))
end).
Defined.
......
extract.v
View file @ 12421740
......@@ -422,6 +422,7 @@ Extract Inlined Constant F_aux.hash_combine => "Farith_Big.combine_hash".
Extract Inlined Constant F_aux.least_bit_Pnat => "Farith_Big.least_bit_Pnat".
Extract Inductive Fappli_IEEE.mode => "Farith_Big.mode" ["Farith_Big.NE" "Farith_Big.ZR" "Farith_Big.DN" "Farith_Big.UP" "Farith_Big.NA" ].
Extract Inductive Fappli_IEEE.full_float => "Farith_Big.classify" ["Farith_Big.Zero" "Farith_Big.Infinity" "Farith_Big.NaN" "Farith_Big.Finite"].
Extract Inductive Fappli_IEEE.binary_float => "Farith_Big.classify" ["Farith_Big.Zero" "Farith_Big.Infinity" "Farith_Big.NaN" "Farith_Big.Finite"].
......
extracted/farith_F_aux.ml
View file @ 12421740
This diff is collapsed.
extracted/farith_F_aux.mli
View file @ 12421740
......@@ -23,9 +23,13 @@ open Farith_BinInt
open Farith_Datatypes
open Farith_Fappli_IEEE
open Farith_Fappli_IEEE_bits
open Farith_Fcalc_bracket
open Farith_Fcore_FLT
type __ = Obj.t
val coq_Zcompare_to_zero : Farith_Big.big_int -> comparison
val shiftr_pos :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
......@@ -42,7 +46,10 @@ val cprec_mw : Farith_Big.big_int -> Farith_Big.big_int
val cemax_ew : Farith_Big.big_int -> Farith_Big.big_int
type 't fconf = { mw : Farith_Big.big_int; ew : Farith_Big.big_int;
cprec : Farith_Big.big_int; cemax : Farith_Big.big_int }
cprec : Farith_Big.big_int; cemax : Farith_Big.big_int;
max_mantisse : Farith_Big.big_int;
max_exponent : Farith_Big.big_int;
emin : Farith_Big.big_int }
val mw : 'a1 fconf -> Farith_Big.big_int
......@@ -52,6 +59,12 @@ val cprec : 'a1 fconf -> Farith_Big.big_int
val cemax : 'a1 fconf -> Farith_Big.big_int
val max_mantisse : 'a1 fconf -> Farith_Big.big_int
val max_exponent : 'a1 fconf -> Farith_Big.big_int
val emin : 'a1 fconf -> Farith_Big.big_int
val check_param : Farith_Big.big_int -> Farith_Big.big_int -> bool
val mk_conf :
......@@ -59,14 +72,23 @@ val mk_conf :
module Aux :
sig
val mw : 'a1 fconf -> Farith_Big.big_int
val ew : 'a1 fconf -> Farith_Big.big_int
val prec : 'a1 fconf -> Farith_Big.big_int
val emax : 'a1 fconf -> Farith_Big.big_int
type ' t' t = Farith_Big.classify
val pl_cst : 'a1 fconf -> Farith_Big.big_int
val default_nan_pl : 'a1 fconf -> bool * nan_pl
val unop_nan_pl : 'a1 fconf -> Farith_Big.classify -> bool * nan_pl
val unop_nan_pl : 'a1 fconf -> 'a1 t -> bool * nan_pl
val binop_nan_pl :
'a1 fconf -> Farith_Big.classify -> Farith_Big.classify -> bool * nan_pl
val binop_nan_pl : 'a1 fconf -> 'a1 t -> 'a1 t -> bool * nan_pl
val opp : 'a1 fconf -> Farith_Big.classify -> Farith_Big.classify
......@@ -96,26 +118,47 @@ module Aux :
val to_bits : 'a1 fconf -> Farith_Big.classify -> Farith_Big.big_int
val internal_eq_rew_dep : 'a1 -> 'a2 -> 'a1 -> 'a2
val shr_fexp_opt :
'a1 fconf -> Farith_Big.big_int -> Farith_Big.big_int -> location ->
Farith_Big.shr_record * Farith_Big.big_int
val binary_overflow_opt :
'a1 fconf -> Farith_Big.mode -> bool -> Farith_Big.classify
val binary_round_opt :
'a1 fconf -> Farith_Big.mode -> bool -> Farith_Big.big_int ->
Farith_Big.big_int -> location -> Farith_Big.classify
val coq_Fdiv_core_binary_opt :
'a1 fconf -> Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int -> Farith_Big.big_int ->
(Farith_Big.big_int * Farith_Big.big_int) * location
val coq_Bdiv_correct_opt :
'a1 fconf -> Farith_Big.mode -> bool -> Farith_Big.big_int ->
Farith_Big.big_int -> bool -> Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.classify
val coq_Bdiv_correct_opt' :
'a1 fconf -> Farith_Big.mode -> bool -> Farith_Big.big_int ->
Farith_Big.big_int -> bool -> Farith_Big.big_int -> Farith_Big.big_int ->
'a1 t
val of_z :
'a1 fconf -> Farith_Big.mode -> Farith_Big.big_int -> Farith_Big.classify
val of_z : 'a1 fconf -> Farith_Big.mode -> Farith_Big.big_int -> 'a1 t
val default_nan : 'a1 fconf -> Farith_Big.classify
val default_nan : 'a1 fconf -> 'a1 t
val of_q : 'a1 fconf -> Farith_Big.mode -> Q.t -> Farith_Big.classify
val of_q : 'a1 fconf -> Farith_Big.mode -> Q.t -> 'a1 t
val to_q : 'a1 fconf -> Farith_Big.classify -> Q.t
val to_q : 'a1 fconf -> 'a1 t -> Q.t
val compare_aux :
'a1 fconf -> Farith_Big.classify -> Farith_Big.classify -> comparison
val compare_aux : 'a1 fconf -> 'a1 t -> 'a1 t -> comparison
val compare :
'a1 fconf -> Farith_Big.classify -> Farith_Big.classify -> int
val compare : 'a1 fconf -> 'a1 t -> 'a1 t -> int
val equal : 'a1 fconf -> Farith_Big.classify -> Farith_Big.classify -> bool
val equal : 'a1 fconf -> 'a1 t -> 'a1 t -> bool
val hash : 'a1 fconf -> Farith_Big.classify -> int
val hash : 'a1 fconf -> 'a1 t -> int
val fcompare :
'a1 fconf -> Farith_Big.classify -> Farith_Big.classify -> int option
......@@ -132,23 +175,23 @@ module Aux :
val neq : 'a1 fconf -> Farith_Big.classify -> Farith_Big.classify -> bool
val infinity : 'a1 fconf -> bool -> Farith_Big.classify
val infinity : 'a1 fconf -> bool -> 'a1 t
val infp : 'a1 fconf -> Farith_Big.classify
val infp : 'a1 fconf -> 'a1 t
val infm : 'a1 fconf -> Farith_Big.classify
val infm : 'a1 fconf -> 'a1 t
val zero : 'a1 fconf -> bool -> Farith_Big.classify
val zero : 'a1 fconf -> bool -> 'a1 t
val zerop : 'a1 fconf -> Farith_Big.classify
val zerop : 'a1 fconf -> 'a1 t
val nan : 'a1 fconf -> bool -> Farith_Big.big_int -> Farith_Big.classify
val nan : 'a1 fconf -> bool -> Farith_Big.big_int -> 'a1 t
val finite :
'a1 fconf -> Farith_Big.mode -> Farith_Big.big_int -> Farith_Big.big_int
-> Farith_Big.classify
-> 'a1 t
val classify : 'a1 fconf -> Farith_Big.classify -> Farith_Big.classify
val classify : 'a1 fconf -> 'a1 t -> Farith_Big.classify
end
module D :
......
farith_Big.ml
View file @ 12421740
......@@ -141,6 +141,10 @@ let sgn z = Z.of_int (Z.sign z)
let compare_case e l g x y =
let s = compare x y in if s = 0 then e else if s<0 then l else g
let zcompare_to_zero e l g x =
let s = sign x in if s = 0 then e else if s<0 then l else g
let nat_rec fO fS =
let rec loop acc n =
if sign n <= 0 then acc else loop (fS acc) (pred n)
......
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