Commit c03040da authored by Guillaume Melquiond's avatar Guillaume Melquiond

Removed an occurrence of digits. This speeds up Bplus by 4200% in the worst case.

parent 5f43eaf0
......@@ -461,7 +461,8 @@ now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct
Qed.
Definition shr_fexp m e l :=
shr (shr_record_of_loc m l) e (fexp (digits radix2 m + e) - e).
let d := match m with Z0 => m | Zpos p => Z_of_nat (S (digits2_Pnat p)) | Zneg p => Z_of_nat (S (digits2_Pnat p)) end in
shr (shr_record_of_loc m l) e (fexp (d + e) - e).
Theorem shr_truncate :
forall m e l,
......@@ -473,6 +474,9 @@ intros m e l Hm.
case_eq (truncate radix2 fexp (m, e, l)).
intros (m', e') l'.
unfold shr_fexp.
replace (match m with Z0 => m | Zpos p => Z_of_nat (S (digits2_Pnat p)) | Zneg p => Z_of_nat (S (digits2_Pnat p)) end)
with (digits radix2 m).
2: now case m ; intros ; try rewrite Z_of_nat_S_digits2_Pnat.
case_eq (fexp (digits radix2 m + e) - e)%Z.
(* *)
intros He.
......
Markdown is supported
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