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

[FP] Add interpretation of fp functions

parent 8d32cbf9
(coq.extraction
(prelude extraction)
(extracted_modules BinNums Bool Qextended Utils Binary BinPosDef Datatypes Round Zaux BinarySingleNaN
BinPos Interval SpecFloat Zbool BinInt Bits Specif Zpower Assert GenericFloat Version)
BinPos Interval SpecFloat Zbool BinInt Bits Specif Zpower Assert GenericFloat Version
Defs Operations)
(theories Farith2))
open BinInt
open Bool
open Datatypes
open Defs
open Operations
open Round
open SpecFloat
open Zaux
type binary_float =
| B754_zero of bool
......@@ -28,6 +31,15 @@ let coq_B2SF _ _ = function
| B754_nan -> S754_nan
| B754_finite (s, m, e) -> S754_finite (s, m, e)
(** val coq_Bsign :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool **)
let coq_Bsign _ _ = function
| B754_zero s -> s
| B754_infinity s -> s
| B754_nan -> false
| B754_finite (s, _, _) -> s
(** val is_nan :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool **)
......@@ -251,6 +263,87 @@ let coq_Bminus prec emax m x y =
| Farith_Big.DN -> true
| _ -> false))
(** val coq_Bfma_szero :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
binary_float -> binary_float -> binary_float -> bool **)
let coq_Bfma_szero prec emax m x y z =
let s_xy = xorb (coq_Bsign prec emax x) (coq_Bsign prec emax y) in
if eqb s_xy (coq_Bsign prec emax z)
then s_xy
else (match m with
| Farith_Big.DN -> true
| _ -> false)
(** val coq_Bfma :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
binary_float -> binary_float -> binary_float -> binary_float **)
let coq_Bfma prec emax m x y z =
match x with
| B754_zero _ ->
(match y with
| B754_zero _ ->
(match z with
| B754_zero _ -> B754_zero (coq_Bfma_szero prec emax m x y z)
| B754_nan -> B754_nan
| _ -> z)
| B754_finite (_, _, _) ->
(match z with
| B754_zero _ -> B754_zero (coq_Bfma_szero prec emax m x y z)
| B754_nan -> B754_nan
| _ -> z)
| _ -> B754_nan)
| B754_infinity sx ->
(match y with
| B754_infinity sy ->
let s = xorb sx sy in
(match z with
| B754_infinity sz -> if eqb s sz then z else B754_nan
| B754_nan -> B754_nan
| _ -> B754_infinity s)
| B754_finite (sy, _, _) ->
let s = xorb sx sy in
(match z with
| B754_infinity sz -> if eqb s sz then z else B754_nan
| B754_nan -> B754_nan
| _ -> B754_infinity s)
| _ -> B754_nan)
| B754_nan -> B754_nan
| B754_finite (sx, mx, ex) ->
(match y with
| B754_zero _ ->
(match z with
| B754_zero _ -> B754_zero (coq_Bfma_szero prec emax m x y z)
| B754_nan -> B754_nan
| _ -> z)
| B754_infinity sy ->
let s = xorb sx sy in
(match z with
| B754_infinity sz -> if eqb s sz then z else B754_nan
| B754_nan -> B754_nan
| _ -> B754_infinity s)
| B754_nan -> B754_nan
| B754_finite (sy, my, ey) ->
(match z with
| B754_zero _ ->
let x0 = { coq_Fnum = (cond_Zopp sx mx); coq_Fexp = ex } in
let y0 = { coq_Fnum = (cond_Zopp sy my); coq_Fexp = ey } in
let { coq_Fnum = mr; coq_Fexp = er } = coq_Fmult radix2 x0 y0 in
binary_normalize prec emax m mr er
(coq_Bfma_szero prec emax m x y z)
| B754_infinity _ -> z
| B754_nan -> B754_nan
| B754_finite (sz, mz, ez) ->
let x0 = { coq_Fnum = (cond_Zopp sx mx); coq_Fexp = ex } in
let y0 = { coq_Fnum = (cond_Zopp sy my); coq_Fexp = ey } in
let z0 = { coq_Fnum = (cond_Zopp sz mz); coq_Fexp = ez } in
let { coq_Fnum = mr; coq_Fexp = er } =
coq_Fplus radix2 (coq_Fmult radix2 x0 y0) z0
in
binary_normalize prec emax m mr er
(coq_Bfma_szero prec emax m x y z)))
(** val coq_Bdiv :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
binary_float -> binary_float -> binary_float **)
......
open BinInt
open Bool
open Datatypes
open Defs
open Operations
open Round
open SpecFloat
open Zaux
type binary_float =
| B754_zero of bool
......@@ -16,6 +19,9 @@ val coq_SF2B :
val coq_B2SF :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> spec_float
val coq_Bsign :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool
val is_nan : Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool
val coq_Babs :
......@@ -75,6 +81,14 @@ val coq_Bminus :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
-> binary_float -> binary_float
val coq_Bfma_szero :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
-> binary_float -> binary_float -> bool
val coq_Bfma :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
-> binary_float -> binary_float -> binary_float
val coq_Bdiv :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
-> binary_float -> binary_float
......
......@@ -4,6 +4,7 @@ open BinarySingleNaN
open Bits
open Datatypes
open Interval
open Qextended
open SpecFloat
type __ = Obj.t
......@@ -177,6 +178,18 @@ module GenericFloat =
(coq_Bdiv (cprec x.mw) (cemax x.ew) m x.value
(same_format_cast (prec x) (emax x) (prec y) (emax y) y.value)))
(** val fma : Farith_Big.mode -> t -> t -> t -> t **)
let fma m x y z =
(fun x f -> assert x; f ()) ((&&) (same_format x y) (same_format x z))
(fun _ ->
mk_with x
(coq_Bfma (cprec x.mw) (cemax x.ew) m x.value
(same_format_cast (cprec x.mw) (cemax x.ew) (cprec y.mw)
(cemax y.ew) y.value)
(same_format_cast (cprec x.mw) (cemax x.ew) (cprec z.mw)
(cemax z.ew) z.value)))
(** val sqrt : Farith_Big.mode -> t -> t **)
let sqrt m x =
......@@ -187,6 +200,51 @@ module GenericFloat =
let abs x =
mk_with x (coq_Babs (cprec x.mw) (cemax x.ew) x.value)
(** val neg : t -> t **)
let neg x =
mk_with x
(match x.value with
| B754_zero s -> B754_zero (Pervasives.not s)
| B754_infinity s -> B754_infinity (Pervasives.not s)
| B754_nan -> B754_nan
| B754_finite (s, m, e) -> B754_finite ((Pervasives.not s), m, e))
(** val least_bit_Pnat : Farith_Big.big_int -> Farith_Big.big_int **)
let rec least_bit_Pnat n =
Farith_Big.positive_case
(fun _ -> Farith_Big.zero)
(fun p -> Farith_Big.succ (least_bit_Pnat p))
(fun _ -> Farith_Big.zero)
n
(** val shiftr_pos :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let shiftr_pos a p =
Farith_Big.nat_rect a (fun _ -> Farith_Big.div2_floor) p
(** val to_q : t -> Q.t **)
let to_q f =
match f.value with
| B754_zero _ -> coq_Qx_zero
| B754_infinity b -> if b then coq_Qx_minus_inf else coq_Qx_inf
| B754_nan -> coq_Qx_undef
| B754_finite (b, m, e) ->
let e' = least_bit_Pnat m in
let m' = if b then Farith_Big.opp m else m in
let e'' = Farith_Big.add e (Farith_Big.identity e') in
(Farith_Big.z_case
(fun _ -> Farith_Big.q_mk ((shiftr_pos m' e'),
Farith_Big.one))
(fun _ -> Farith_Big.q_mk ((Farith_Big.shiftl m' e),
Farith_Big.one))
(fun p -> Farith_Big.q_mk ((shiftr_pos m' e'),
(Farith_Big.shiftl Farith_Big.one p)))
e'')
(** val le : t -> t -> bool **)
let le x y =
......
......@@ -4,6 +4,7 @@ open BinarySingleNaN
open Bits
open Datatypes
open Interval
open Qextended
open SpecFloat
type __ = Obj.t
......@@ -79,10 +80,21 @@ module GenericFloat :
val div : Farith_Big.mode -> t -> t -> t
val fma : Farith_Big.mode -> t -> t -> t -> t
val sqrt : Farith_Big.mode -> t -> t
val abs : t -> t
val neg : t -> t
val least_bit_Pnat : Farith_Big.big_int -> Farith_Big.big_int
val shiftr_pos :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
val to_q : t -> Q.t
val le : t -> t -> bool
val lt : t -> t -> bool
......
(** val coq_Qx_zero : Q.t **)
let coq_Qx_zero =
Farith_Big.q_mk (Farith_Big.zero, Farith_Big.one)
(** val coq_Qx_undef : Q.t **)
let coq_Qx_undef =
Farith_Big.q_mk (Farith_Big.zero, Farith_Big.zero)
(** val coq_Qx_inf : Q.t **)
let coq_Qx_inf =
Farith_Big.q_mk (Farith_Big.one, Farith_Big.zero)
(** val coq_Qx_minus_inf : Q.t **)
let coq_Qx_minus_inf =
Farith_Big.q_mk ((Farith_Big.opp Farith_Big.one), Farith_Big.zero)
val coq_Qx_zero : Q.t
val coq_Qx_undef : Q.t
val coq_Qx_inf : Q.t
val coq_Qx_minus_inf : Q.t
type radix =
Farith_Big.big_int
(* singleton inductive, whose constructor was Build_radix *)
(** val radix_val : radix -> Farith_Big.big_int **)
let radix_val r =
r
(** val radix2 : radix **)
let radix2 =
(Farith_Big.double Farith_Big.one)
type radix =
Farith_Big.big_int
(* singleton inductive, whose constructor was Build_radix *)
val radix_val : radix -> Farith_Big.big_int
val radix2 : radix
......@@ -40,3 +40,7 @@
(rule (action (copy ../extract/GenericFloat.mli GenericFloat.mli)) (mode promote))
(rule (action (copy ../extract/Version.ml Version.ml)) (mode promote))
(rule (action (copy ../extract/Version.mli Version.mli)) (mode promote))
(rule (action (copy ../extract/Defs.ml Defs.ml)) (mode promote))
(rule (action (copy ../extract/Defs.mli Defs.mli)) (mode promote))
(rule (action (copy ../extract/Operations.ml Operations.ml)) (mode promote))
(rule (action (copy ../extract/Operations.mli Operations.mli)) (mode promote))
......@@ -100,6 +100,31 @@ module F = struct
let inf ~mw ~ew b = inf (Z.of_int mw) (Z.of_int ew) b
let is_zero t = match t.value with B754_zero _ -> true | _ -> false
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 is_negative t =
match t.value with
| B754_zero true | B754_finite (true, _, _) -> true
| _ -> false
let is_positive t =
match t.value with
| B754_zero false | B754_finite (false, _, _) -> true
| _ -> false
let is_normal t =
match t.value with
| B754_zero _ -> true
| B754_finite (_, e, _) when Z.sign e <> 0 -> true
| _ -> false
let is_subnormal t =
match t.value with
| B754_finite (_, e, _) when Z.sign e = 0 -> true
| _ -> false
end
module I = struct
......
......@@ -48,6 +48,8 @@ module F : sig
val of_q : mw:int -> ew:int -> mode:mode -> Q.t -> t
val to_q : t -> Q.t
val add : mode -> t -> t -> t
val sub : mode -> t -> t -> t
......@@ -56,10 +58,14 @@ module F : sig
val div : mode -> t -> t -> t
val fma : mode -> t -> t -> t -> t
val sqrt : mode -> t -> t
val abs : t -> t
val neg : t -> t
val of_bits : mw:int -> ew:int -> Z.t -> t
val to_bits : t -> Z.t
......@@ -81,6 +87,18 @@ module F : sig
val inf : mw:int -> ew:int -> bool -> t
val is_zero : t -> bool
val is_infinite : t -> bool
val is_nan : t -> bool
val is_negative : t -> bool
val is_positive : t -> bool
val is_normal : t -> bool
val is_subnormal : t -> bool
end
module I : sig
......
......@@ -186,12 +186,153 @@ Module GenericFloat.
Definition div (m : mode) (x y : t) : t :=
AssertF.assert (same_format x y) (fun H => mk_with x (@Bdiv _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y)))).
Program Definition fma (m : mode) (x y z : t) : t :=
AssertF.assert (andb (same_format x y) (same_format x z)) (fun H => mk_with x (@Bfma _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast _ (value y)) (same_format_cast _ (value z)))).
Next Obligation.
rewrite !Bool.andb_true_iff in H.
exact (proj1 H).
Defined.
Next Obligation.
rewrite !Bool.andb_true_iff in H.
exact (proj2 H).
Defined.
Definition sqrt (m : mode) (x : t) : t :=
mk_with x (@Bsqrt _ _ (Hprec x) (Hemax x) m (value x)).
Definition abs (x : t) : t :=
mk_with x (@Babs _ _ (value x)).
Definition neg (x : t) : t :=
mk_with x (match value x with
| B754_nan => B754_nan
| B754_zero s => B754_zero (negb s)
| B754_infinity s => B754_infinity (negb s)
| B754_finite s m e H => B754_finite (negb s) m e H
end).
Fixpoint least_bit_Pnat (n : positive) :=
match n with
| xH => O
| xO p => S (least_bit_Pnat p)
| xI p => O
end.
Definition shiftr_pos a p := Wf_nat.iter_nat p _ Z.div2 a.
Lemma shiftr_pos_is_shiftr :
forall a p, shiftr_pos a p = Z.shiftr a (Z.of_nat p).
Proof.
intros.
destruct p.
reflexivity.
unfold shiftr_pos, Z.shiftr, Z.shiftl, Z.of_nat, Z.opp.
rewrite Pos2Nat.inj_iter.
rewrite SuccNat2Pos.id_succ.
reflexivity.
Qed.
Lemma least_bit_shiftr_pos :
forall m (b:bool),
let e' := least_bit_Pnat m in
let m' := if b then Z.neg m else Z.pos m in
let m'' := shiftr_pos m' e' in
Z.odd m'' = true.
Proof.
induction m; intro b.
- destruct b;reflexivity.
- assert (H:= IHm b);
destruct b;
replace (least_bit_Pnat m~0) with (S (least_bit_Pnat m)) in * by reflexivity;
intros e' m';
replace (shiftr_pos m' e') with (shiftr_pos (Z.div2 m') (least_bit_Pnat m)) by
(unfold shiftr_pos, e'; rewrite nat_rect_succ_r; reflexivity).
* replace (Z.div2 m') with (Z.neg m) by reflexivity.
exact H.
* replace (Z.div2 m') with (Z.pos m) by reflexivity.
exact H.
- destruct b; reflexivity.
Qed.
Lemma gcd_odd_pow_2:
forall (m:positive) n,
match m with xO _ => False | _ => True end ->
Pos.gcd m (Pos.shiftl 1%positive (Npos n)) = 1%positive.
Proof.
destruct m as [p|p|]; intros n H; destruct H; simpl.
- induction n using Pos.peano_ind.
* compute [Pos.iter Z.mul Pos.mul].
unfold Pos.gcd.
replace (Pos.size_nat 2) with (2)%nat by reflexivity.
simpl.
replace (Pos.size_nat p + 2)%nat with (S (S (Pos.size_nat p))) by auto with *.
reflexivity.
* rewrite Pos.iter_succ.
unfold Pos.gcd.
simpl.
replace (Pos.size_nat p + S (Pos.size_nat (Pos.iter xO 1%positive n)))%nat
with (S (Pos.size_nat p + Pos.size_nat (Pos.iter xO 1%positive n))) by auto with *.
exact IHn.
- unfold Pos.gcd.
reflexivity.
Qed.
Lemma to_q (f:t) : Qx.
Proof.
refine (match value f with
| B754_zero _ => Qx_zero
| B754_infinity b => if b then Qx_minus_inf else Qx_inf
| B754_nan => Qx_undef
| B754_finite b m e _ =>
let e' := least_bit_Pnat m in
let m' := if b then Z.neg m else Z.pos m in
let e'' := (e + (Z.of_nat e'))%Z in
match e'' with
| Z0 => Qxmake (shiftr_pos m' e') 1%Z (refl_equal _) _
| Z.pos _ => Qxmake (Z.shiftl m' e)%Z 1%Z (refl_equal _) _
| Z.neg p => Qxmake (shiftr_pos m' e') (Z.shiftl 1%Z (Z.pos p)) _ _
end
end
).
- rewrite Z.gcd_1_r.
reflexivity.
- rewrite Z.gcd_1_r.
reflexivity.
- rewrite Z.shiftl_1_l.
apply Z.leb_le.
apply Z.lt_le_incl.
apply Zpower_pos_gt_0.
reflexivity.
- assert (Z.shiftl 1 (Z.pos p) =? 0 = false)%Z by
(rewrite Z.shiftl_1_l;
apply Z.eqb_neq;
apply Z.neq_sym;
apply Z.lt_neq;
exact (Zpower_pos_gt_0 2%Z p (refl_equal _))).
rewrite H.
assert (Z.odd (shiftr_pos m' e') = true) by (exact (least_bit_shiftr_pos m b)).
destruct (shiftr_pos m' e'); clear H e0 e' m' e''.
discriminate H0.
rewrite <- (shift_equiv _ _ (Pos2Z.is_nonneg _)).
replace (shift (Z.pos p) 1) with (shift_pos p 1%positive) by reflexivity.
rewrite shift_pos_equiv.
compute [Z.gcd].
rewrite gcd_odd_pow_2.
reflexivity.
unfold Z.odd in H0.
destruct p0; [exact I| discriminate H0| exact I].
rewrite <- (shift_equiv _ _ (Pos2Z.is_nonneg _)).
replace (shift (Z.pos p) 1) with (shift_pos p 1%positive) by reflexivity.
rewrite shift_pos_equiv.
compute [Z.gcd].
rewrite gcd_odd_pow_2.
reflexivity.
unfold Z.odd in H0.
destruct p0; [exact I| discriminate H0| exact I].
Defined.
Definition le (x y : t) : bool :=
AssertB.assert (same_format x y) (fun H => (@Bleb _ _ (value x) (same_format_cast H (value y)))).
......
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