diff --git a/src_colibri2/theories/FP/dom_interval.ml b/src_colibri2/theories/FP/dom_interval.ml
index 74e7ba821bc28d222ccc98f81fbfe1a88eb04fc9..bc154d4da8e30f09f26ba81c55200966f1295413 100644
--- a/src_colibri2/theories/FP/dom_interval.ml
+++ b/src_colibri2/theories/FP/dom_interval.ml
@@ -20,7 +20,7 @@
open Colibri2_popop_lib
open Colibri2_core
-open Colibri2_stdlib.Std
+(* open Colibri2_stdlib.Std *)
let debug = Debug.register_info_flag
~desc:"for intervals for the arithmetic theory"
@@ -33,7 +33,7 @@ let dom = Dom.Kind.create (module struct type t = D.t let name = "ARITH" end)
include (Dom.Lattice(struct
include D
let equal (x : t) (y : t) = Stdlib.(=) x y
- let pp _ _ = ()
+ let pp fmt x = Format.fprintf fmt "%s" (D.to_string x)
let key = dom
let inter _ d1 d2 = inter d1 d2
let is_singleton _ d =
@@ -41,39 +41,39 @@ include (Dom.Lattice(struct
end
))
-let is_zero_or_positive d n =
+(* let is_zero_or_positive d n =
match Egraph.get_dom d dom n with
| None -> false
| Some p -> match D.is_comparable D.zero p with
| D.Le | D.Lt -> true
- | D.Ge | D.Gt | D.Uncomparable -> false
+ | D.Ge | D.Gt | D.Uncomparable -> false *)
-let is_not_zero d n =
+(* let is_not_zero d n =
match Egraph.get_dom d dom n with
| None -> false
- | Some p -> D.absent Q.zero p
+ | Some p -> D.absent Q.zero p *)
-let is_strictly_positive d n =
+(* let is_strictly_positive d n =
match Egraph.get_dom d dom n with
| None -> false
| Some p -> match D.is_comparable D.zero p with
| D.Lt -> true
- | D.Le | D.Ge | D.Gt | D.Uncomparable -> false
+ | D.Le | D.Ge | D.Gt | D.Uncomparable -> false *)
-let is_strictly_negative d n =
+(* let is_strictly_negative d n =
match Egraph.get_dom d dom n with
| None -> false
| Some p -> match D.is_comparable D.zero p with
| D.Gt -> true
- | D.Le | D.Ge | D.Lt | D.Uncomparable -> false
+ | D.Le | D.Ge | D.Lt | D.Uncomparable -> false *)
-let is_integer d n =
+(* let is_integer d n =
match Egraph.get_dom d dom n with
| None -> false
- | Some p -> D.is_integer p
+ | Some p -> D.is_integer p *)
-module ChoLRA = struct
+(* module ChoLRA = struct
let make_decision node v env =
Debug.dprintf4 Debug.decision
"[LRA] decide %a on %a" D.pp v Node.pp node;
@@ -94,9 +94,9 @@ module ChoLRA = struct
print_cho = "Decision made by dom_interval.ml";
}
-end
+end *)
-let choice = ChoLRA.choice
+(* let choice = ChoLRA.choice *)
let neg_cmp = function
| `Lt -> `Ge
@@ -110,22 +110,23 @@ let com_cmp = function
| `Ge -> `Le
| `Gt -> `Lt
-let backward = function
+(* let backward = function
| `Lt -> D.lt'
| `Gt -> D.gt'
| `Le -> D.le'
- | `Ge -> D.ge'
+ | `Ge -> D.ge' *)
(** {2 Initialization} *)
let converter d (f:Ground.t) =
let r = Ground.node f in
let reg n = Egraph.register d n in
let open Monad in
- let setb = setv Boolean.dom in
- let getb = getv Boolean.dom in
+ (* let setb = setv Boolean.dom in
+ let getb = getv Boolean.dom in *)
let set = updd upd_dom in
let get = getd dom in
- let cmp test cmp a b =
+ let getm = getv Rounding_mode.key in
+ (* let cmp test cmp a b =
reg a; reg b;
attach d (
setb r (let* va = get a and+ vb = get b in
@@ -135,58 +136,73 @@ let converter d (f:Ground.t) =
set a (let+ vb = get b and+ vr = getb r in
backward (if vr then cmp else (neg_cmp cmp)) vb)
);
- in
+ in *)
match Ground.sem f with
- | { app = {builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
- when Ground.Ty.equal ty Ground.Ty.real ->
- (* Egraph.register_decision d (ChoLRA.choice r) *) (* not useful for now *)
- ()
- | { app = {builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
- when Ground.Ty.equal ty Ground.Ty.int ->
- upd_dom d r D.integers
- | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
- let (a,b) = IArray.extract2_exn args in
- reg a; reg b;
- attach d (
- set r (let+ va = get a and+ vb = get b in D.add va vb) &&
- set a (let+ vb = get b and+ vr = get r in D.minus vr vb) &&
- set b (let+ va = get a and+ vr = get r in D.minus vr va)
- );
- | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
- let (a,b) = IArray.extract2_exn args in
- reg a; reg b;
+ (* | { app = {builtin = Expr.Real_to_fp (8, 24); _}; args; _} ->
+ let m, r = IArray.extract2_exn args in
+ !< (Farith.B32.of_q !>>m !>>>r) *)
+ (* | { app = {builtin = Expr.Plus_infinity (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.infp) *)
+ (* | { app = {builtin = Expr.Minus_infinity (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.infm) *)
+ (* | { app = {builtin = Expr.NaN (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.(nan true Z.one)) *)
+ (* | { app = {builtin = Expr.Plus_zero (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.zerop) *)
+ (* | { app = {builtin = Expr.Minus_zero (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.zero true) *)
+ | { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ reg m; reg a; reg b;
attach d (
- set r (let+ va = get a and+ vb = get b in D.minus va vb) &&
- set a (let+ vb = get b and+ vr = get r in D.add vr vb) &&
- set b (let+ va = get a and+ vr = get r in D.minus va vr)
- );
- | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
+ set r (let+ vm = getm m and+ va = get a and+ vb = get b in D.add vm va vb)
+ )
+ (* | { app = {builtin = Expr.Fp_sub (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ !< (Farith.B32.sub !>>m !>a !>b) *)
+ (* | { app = {builtin = Expr.Fp_mul (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ !< (Farith.B32.mul !>>m !>a !>b) *)
+ (* | { app = {builtin = Expr.Fp_abs (8, 24); _}; args; _} ->
let a = IArray.extract1_exn args in
- reg a;
+ !< (Farith.B32.abs !>a) *)
+ (* | { app = {builtin = Expr.Fp_div (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ if Farith.B32.(eq !>b (zero true) || eq !>b (zero false)) then `Uninterp
+ else !< (Farith.B32.div !>>m !>a !>b) *)
+ (* | { app = {builtin = Expr.Fp_eq (8, 24); _}; args; _} -> *)
+ (* let a, b = IArray.extract2_exn args in
+ reg a; reg b;
attach d (
- set r (let+ va = get a in D.mult_cst Q.minus_one va) &&
- set a (let+ vr = get r in D.mult_cst Q.minus_one vr)
- );
- | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- cmp (function | Uncomparable | Le -> None | Lt -> Some true | Ge | Gt -> Some false) `Lt a b
- | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some true | Gt -> Some false) `Le a b
- | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- cmp (function | Uncomparable | Le -> None | Lt -> Some false | Ge | Gt -> Some true) `Ge a b
- | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some false | Gt -> Some true) `Gt a b
+ set a (let+ va = get a and+ vb = get b and+ vr = getb r in if vr then (D.inter va vb) else va) &&
+ set b (let+ va = get a and+ vb = get b and+ vr = getb r in if vr then &D.inter va vb else vb)
+ ) *)
+
+ (* | { app = {builtin = Expr.Fp_leq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ !<< (Farith.B32.le !>a !>b) *)
+ (* | { app = {builtin = Expr.Fp_lt (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ !<< (Farith.B32.lt !>a !>b) *)
+ (* | { app = {builtin = Expr.Fp_geq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ !<< (Farith.B32.ge !>a !>b) *)
+ (* | { app = {builtin = Expr.Fp_gt (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ !<< (Farith.B32.gt !>a !>b) *)
| _ -> ()
let init env =
- Daemon.attach_reg_value env
+ (* Daemon.attach_reg_value env
Float32.key
(fun d value ->
let v = Float32.value value in
let s = D.singleton v in
Egraph.set_dom d dom (Float32.node value) s
- );
+ ); *)
Ground.register_converter env converter
\ No newline at end of file
diff --git a/src_colibri2/theories/FP/dom_interval/extracted.ml b/src_colibri2/theories/FP/dom_interval/extracted.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src_colibri2/theories/FP/dom_interval/interval_32.ml b/src_colibri2/theories/FP/dom_interval/interval_32.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml
index 9e42756c13cd597094b4a1ce907f7649a887edc0..44de3600c9cf5093c0f11da4159c38eb97e1fb7f 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -214,7 +214,6 @@ let converter d (f:Ground.t) =
cmp Farith.B32.eq a b; attach_interp d f;
| _ -> ()
-
let init env =
Ground.register_converter env converter;
init_ty env;
diff --git a/src_colibri2/theories/FP/interval_32.ml b/src_colibri2/theories/FP/interval_32.ml
index 242614930f9cc57fbce2750c3cd3ba046a549212..7d3103857bd3c53ffa94b528a0997301970c3fda 100644
--- a/src_colibri2/theories/FP/interval_32.ml
+++ b/src_colibri2/theories/FP/interval_32.ml
@@ -1,4 +1,3 @@
-
(** val negb : bool -> bool **)
let negb = function
@@ -146,7 +145,7 @@ module Pos =
compare_cont Eq
end
-module Z =
+module MyZ =
struct
(** val double : z -> z **)
@@ -321,12 +320,12 @@ type spec_float =
(** val emin : z -> z -> z **)
let emin prec0 emax0 =
- Z.sub (Z.sub (Zpos (XI XH)) emax0) prec0
+ MyZ.sub (MyZ.sub (Zpos (XI XH)) emax0) prec0
(** val fexp : z -> z -> z -> z **)
let fexp prec0 emax0 e =
- Z.max (Z.sub e prec0) (emin prec0 emax0)
+ MyZ.max (MyZ.sub e prec0) (emin prec0 emax0)
(** val digits2_pos : positive -> positive **)
@@ -429,7 +428,7 @@ let shr_record_of_loc m = function
let shr mrs e n = match n with
| Zpos p ->
- ((iter_pos shr_1 p mrs), (Z.add e n))
+ ((iter_pos shr_1 p mrs), (MyZ.add e n))
| _ -> (mrs, e)
(** val shr_fexp :
@@ -438,15 +437,15 @@ let shr mrs e n = match n with
let shr_fexp prec0 emax0 m e l =
shr (shr_record_of_loc m l) e
- (Z.sub
+ (MyZ.sub
(fexp prec0 emax0
- (Z.add (zdigits2 m) e)) e)
+ (MyZ.add (zdigits2 m) e)) e)
(** val shl_align :
positive -> z -> z -> positive * z **)
let shl_align mx ex ex' =
- match Z.sub ex' ex with
+ match MyZ.sub ex' ex with
| Zneg d -> ((shift_pos d mx), ex')
| _ -> (mx, ex)
@@ -485,7 +484,7 @@ let sFcompare f1 f2 =
Some
(if s1
then if s2
- then (match Z.compare e1 e2 with
+ then (match MyZ.compare e1 e2 with
| Eq ->
compOpp
(Pos.compare_cont Eq
@@ -495,7 +494,7 @@ let sFcompare f1 f2 =
else Lt
else if s2
then Gt
- else (match Z.compare e1 e2 with
+ else (match MyZ.compare e1 e2 with
| Eq ->
Pos.compare_cont Eq m1
m2
@@ -537,12 +536,12 @@ let sFleb f1 f2 =
(** val cond_Zopp : bool -> z -> z **)
let cond_Zopp b m =
- if b then Z.opp m else m
+ if b then MyZ.opp m else m
(** val cond_incr : bool -> z -> z **)
let cond_incr b m =
- if b then Z.add m (Zpos XH) else m
+ if b then MyZ.add m (Zpos XH) else m
(** val round_sign_DN :
bool -> location -> bool **)
@@ -638,7 +637,7 @@ type mode =
let choice_mode m sx mx lx =
match m with
| Mode_NE ->
- cond_incr (round_N (negb (Z.even mx)) lx)
+ cond_incr (round_N (negb (MyZ.even mx)) lx)
mx
| Mode_ZR -> mx
| Mode_DN ->
@@ -664,17 +663,17 @@ let binary_overflow prec0 emax0 m s =
if overflow_to_inf m s
then S754_infinity s
else S754_finite (s,
- (Z.to_pos
- (Z.sub
- (Z.pow (Zpos (XO XH)) prec0)
- (Zpos XH))), (Z.sub emax0 prec0))
+ (MyZ.to_pos
+ (MyZ.sub
+ (MyZ.pow (Zpos (XO XH)) prec0)
+ (Zpos XH))), (MyZ.sub emax0 prec0))
(** val binary_fit_aux :
z -> z -> mode -> bool -> positive -> z
-> spec_float **)
let binary_fit_aux prec0 emax0 mode0 sx mx ex =
- if Z.leb ex (Z.sub emax0 prec0)
+ if MyZ.leb ex (MyZ.sub emax0 prec0)
then S754_finite (sx, mx, ex)
else binary_overflow prec0 emax0 mode0 sx
@@ -703,7 +702,7 @@ let binary_round_aux prec0 emax0 mode0 sx mx ex lx =
let shl_align_fexp prec0 emax0 mx ex =
shl_align mx ex
(fexp prec0 emax0
- (Z.add (Zpos (digits2_pos mx)) ex))
+ (MyZ.add (Zpos (digits2_pos mx)) ex))
(** val binary_round :
z -> z -> mode -> bool -> positive -> z
@@ -761,9 +760,9 @@ let bplus prec0 emax0 m x y =
| B754_infinity _ -> y
| B754_nan -> B754_nan
| B754_finite (sy, my, ey) ->
- let ez = Z.min ex ey in
+ let ez = MyZ.min ex ey in
binary_normalize prec0 emax0 m
- (Z.add
+ (MyZ.add
(cond_Zopp sx (Zpos
(fst (shl_align mx ex ez))))
(cond_Zopp sy (Zpos
@@ -885,7 +884,22 @@ let iadd' prec0 emax0 m i1 i2 =
let iadd =
iadd'
-module Intv32 =
+module Intv32 : sig
+
+ type t
+
+ val inter : t -> t -> t option
+
+ val add : Farith.mode -> t -> t -> t
+
+ val top : t
+
+ val bot : t option
+
+ val is_singleton : t -> Farith.B32.t option
+
+ val to_string : t -> string
+end =
struct
(** val prec : z **)
@@ -897,21 +911,21 @@ module Intv32 =
let emax =
Zpos (XO (XO (XO (XO (XO (XO (XO XH)))))))
- type float32 = float0
-
type t = interval
- type t_opt = interval_opt
-
- (** val inter : t -> t -> t_opt **)
-
let inter x y =
inter prec emax x y
(** val add : mode -> t -> t -> t **)
- let add =
- iadd prec emax
+ let add m =
+ iadd prec emax (match m with
+ | Farith.DN -> Mode_DN
+ | Farith.NA -> Mode_NA
+ | Farith.NE -> Mode_NE
+ | Farith.UP -> Mode_UP
+ | Farith.ZR -> Mode_ZR
+ )
(** val top : t **)
@@ -927,10 +941,72 @@ module Intv32 =
(** val is_singleton :
t -> float32 option **)
+ let rec pos_to_Z (p : positive) =
+ match p with
+ | XH -> Z.one
+ | XO p' -> Z.shift_left (pos_to_Z p') 1
+ | XI p' -> Z.succ (Z.shift_left (pos_to_Z p') 1)
+
+ let z_to_Z z =
+ match z with
+ | Z0 -> Z.zero
+ | Zpos p -> pos_to_Z p
+ | Zneg p -> Z.neg (pos_to_Z p)
+
+ (* let pos_of_Z z =
+ let rem = ref z in
+ if Z.equal a
+
+ let z_of_Z z =
+ let rem = ref z in
+ let two = Z.(add one one) in
+ if Z.equal z
+ let (q, r) = Z.ediv_rem !rem two in *)
+
+ (*
+ while rem <> 0 :
+ let (q, r) = diveucl rem
+ if r = 0 then
+ append O
+ else
+ append I
+ rem = q
+ *)
+
+ (* let b_of_B32 (f : Farith.B32.t) =
+ match Farith.B32.classify f with
+ | Farith.Zero s -> B754_zero s
+ | Farith.Infinity s -> B754_infinity s
+ | Farith.NaN (_, _) -> B754_nan
+ | Farith.Finite (s, m, e) -> B754_finite (s, _, _) *)
+
+ let b_to_B32 f =
+ match f with
+ | B754_nan -> Farith.B32.default_nan
+ | B754_zero s -> Farith.B32.zero s
+ | B754_infinity s -> Farith.B32.infinity s
+ | B754_finite (s, m, e) ->
+ let m' = if s then Z.neg (pos_to_Z m) else (pos_to_Z m) in
+ let e' = z_to_Z e in
+ Farith.B32.finite NE m' e'
+
let is_singleton = function
- | Inan -> Some B754_nan
+ | Inan -> Some Farith.B32.default_nan
| Intv (a, b, n) ->
if (&&) (beqb prec emax a b) (negb n)
- then Some a
+ then Some (b_to_B32 a)
else None
- end
\ No newline at end of file
+
+ let to_string = function
+ | Inan -> "{ NaN }"
+ | Intv (a, b, nan) ->
+ if nan then
+ Format.sprintf "[%a, %a] + NaN"
+ Farith.B32.pp (b_to_B32 a)
+ Farith.B32.pp (b_to_B32 b)
+ else
+ Format.sprintf "[%a, %a]"
+ Farith.B32.pp (b_to_B32 a)
+ Farith.B32.pp (b_to_B32 b)
+ end
+
diff --git a/src_common/ieee/coq/.nia.cache b/src_common/ieee/coq/.nia.cache
deleted file mode 100644
index e1ba0d8848ad382d95a2522bd2936fc77bc7bf09..0000000000000000000000000000000000000000
Binary files a/src_common/ieee/coq/.nia.cache and /dev/null differ
diff --git a/src_common/ieee/coq/.nra.cache b/src_common/ieee/coq/.nra.cache
index d4eace0958b03eb6573f516a098d386cece26252..d98ef9c4b6c6b430155da61742d938534ee28064 100644
Binary files a/src_common/ieee/coq/.nra.cache and b/src_common/ieee/coq/.nra.cache differ
diff --git a/src_common/ieee/coq/B32.v b/src_common/ieee/coq/B32.v
new file mode 100644
index 0000000000000000000000000000000000000000..3575fe4bcd9185540dce3c6eb06069fc9ca2334e
--- /dev/null
+++ b/src_common/ieee/coq/B32.v
@@ -0,0 +1,116 @@
+From Flocq Require Import Core.Core IEEE754.BinarySingleNaN IEEE754.Bits.
+Require Import QArith.
+Require Import Qreals.
+Require Import Reals.
+Require Import ZBits.
+Require Import Lia Lra.
+Require Coq.Arith.Wf_nat.
+Require Import Extraction.
+From F Require Import Qextended Rextended.
+
+
+Module B32.
+
+Definition prec : Z := 24.
+Definition emax : Z := 128.
+
+Definition mw : Z := 23.
+Definition ew : Z := 8.
+
+Definition t : Type := binary_float prec emax.
+
+Lemma Hprec : Prec_gt_0 prec.
+ Proof. unfold Prec_gt_0, prec; lia. Qed.
+
+Lemma Hemax : Prec_lt_emax prec emax.
+ Proof. unfold Prec_lt_emax, prec, emax; lia. Qed.
+
+Lemma Hmw : (0 < mw)%Z. unfold mw; lia. Qed.
+
+Lemma Hew : (0 < ew)%Z. unfold ew; lia. Qed.
+
+Definition add : mode -> t -> t -> t := @Bplus _ _ Hprec Hemax.
+Definition sub : mode -> t -> t -> t := @Bminus _ _ Hprec Hemax.
+Definition mult : mode -> t -> t -> t := @Bmult _ _ Hprec Hemax.
+Definition div : mode -> t -> t -> t := @Bmult _ _ Hprec Hemax.
+Definition sqrt : mode -> t -> t := @Bsqrt _ _ Hprec Hemax.
+Definition abs : t -> t := Babs.
+
+Definition le : t -> t -> bool := Bleb.
+Definition lt : t -> t -> bool := Bltb.
+Definition eq : t -> t -> bool := Beqb.
+Definition ge : t -> t -> bool := fun x y => Bleb y x.
+Definition gt : t -> t -> bool := fun x y => Bltb y x.
+
+Definition of_bits (b : Z) : t :=
+ match Bits.binary_float_of_bits mw ew Hmw Hew Hemax b with
+ | Binary.B754_nan _ _ _ _ _ => B754_nan
+ | Binary.B754_zero _ _ s => B754_zero s
+ | Binary.B754_infinity _ _ s => B754_infinity s
+ | Binary.B754_finite _ _ s m e H => B754_finite s m e H
+ end.
+
+Definition pl_cst := (Zaux.iter_nat xO (Z.to_nat (Z.pred mw)) xH)%Z.
+
+Lemma pl_valid : (Z.pos (Digits.digits2_pos pl_cst) <? prec)%Z = true.
+Proof.
+ assert (G:forall n, Digits.digits2_Pnat (Zaux.iter_nat xO n xH)%Z = n).
+ - induction n.
+ * reflexivity.
+ * rewrite iter_nat_S; simpl.
+ rewrite IHn; reflexivity.
+ - rewrite Digits.Zpos_digits2_pos.
+ rewrite <- Digits.Z_of_nat_S_digits2_Pnat.
+ unfold pl_cst, prec, mw.
+ rewrite G;clear G.
+ rewrite Nat2Z.inj_succ.
+ rewrite Z2Nat.id; [rewrite Z.ltb_lt | ]; lia.
+Qed.
+
+Definition to_bits (f : t) : Z :=
+ match f with
+ | B754_nan =>
+ Bits.bits_of_binary_float mw ew (Binary.B754_nan prec emax true pl_cst pl_valid)
+ | B754_zero s => Bits.bits_of_binary_float mw ew (Binary.B754_zero prec emax s)
+ | B754_infinity s => Bits.bits_of_binary_float mw ew (Binary.B754_infinity prec emax s)
+ | B754_finite s m e H => Bits.bits_of_binary_float mw ew (Binary.B754_finite prec emax s m e H)
+ end.
+
+Definition of_q (m : mode) (q : Qx) : t :=
+ match Qx_classify q with
+ | Qx_ZERO _ _ _ _ => B754_zero false
+ | Qx_INF _ _ _ => B754_infinity false
+ | Qx_MINF _ _ _ => B754_infinity true
+ | Qx_UNDEF _ _ _ => B754_nan
+ | Qx_NZERO _ _ _ _ _ =>
+ match num q with
+ | Z0 => B754_nan (** absurd *)
+ | Z.pos pn =>
+ SF2B _ (proj1 (Bdiv_correct_aux _ _ Hprec Hemax m false pn 0%Z false (Z.to_pos (den q)) 0%Z))
+ | Z.neg nn =>
+ SF2B _ (proj1 (Bdiv_correct_aux _ _ Hprec Hemax m true nn 0%Z false (Z.to_pos (den q)) 0%Z))
+ end
+ end.
+
+Lemma of_q_correct : forall m q, Q2Rx q = B2Rx (of_q m q).
+Proof.
+ intros m q.
+ unfold of_q, Q2Rx; destruct (Qx_classify q).
+ - rewrite e, e0. reflexivity.
+ - rewrite e, e0. reflexivity.
+ - rewrite e, e0. reflexivity.
+ - rewrite e, e0.
+ destruct (Z.pos pq =? 0)%Z; try reflexivity.
+ unfold Q2R; simpl.
+ now rewrite Rmult_0_l.
+ - rewrite e.
+ destruct (Z.pos pq =? 0)%Z eqn:E1, (num q =? 0)%Z eqn:E2.
+ + rewrite Z.eqb_eq in E1; rewrite E1;
+ rewrite Z.eqb_eq in E2; rewrite E2.
+ reflexivity.
+ + admit.
+ + admit.
+ + admit.
+Admitted.
+
+End B32.
\ No newline at end of file
diff --git a/src_common/ieee/coq/Domains.v b/src_common/ieee/coq/Domains.v
deleted file mode 100644
index bc8a7dd20bbda41ad4fba923bba509e003feb5ec..0000000000000000000000000000000000000000
--- a/src_common/ieee/coq/Domains.v
+++ /dev/null
@@ -1,29 +0,0 @@
-From Flocq Require Import IEEE754.BinarySingleNaN.
-From Coq Require Import ZArith.
-
-Definition Powerset (A : Type) := A -> Prop.
-
-Notation "ð“Ÿ( A )" := (Powerset A).
-
-Module Type Fformat.
- Parameter prec : Z.
- Parameter emax : Z.
- Axiom Hprec : FLX.Prec_gt_0 prec.
- Axiom Hemax : Prec_lt_emax prec emax.
-End Fformat.
-
-Module Fdom (F : Fformat).
-
- Parameter Dom : Type.
-
- Parameter γ : Dom -> ð“Ÿ(binary_float F.prec F.emax).
-
- Parameter add : Dom -> Dom -> Dom.
-
- Axiom add_correct :
- forall (m : mode) (d1 d2 : Dom) (x y : binary_float F.prec F.emax),
- γ d1 x ->
- γ d1 y ->
- γ (add d1 d2) (@Bplus F.prec F.emax F.Hprec F.Hemax m x y).
-
-End Fdom.
diff --git a/src_common/ieee/coq/Interval.v b/src_common/ieee/coq/Interval.v
index 222f99b4d9ebd8fead85d1612e8c22d8a9e6949a..45217ccf5e2fba22886184ff5d59d8208a35c582 100644
--- a/src_common/ieee/coq/Interval.v
+++ b/src_common/ieee/coq/Interval.v
@@ -1,6 +1,6 @@
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import QArith Psatz Reals Extraction.
-Require Import F.Utils F.Domains F.Correction_thms F.Rextended.
+Require Import F.Utils F.Correction_thms F.Rextended.
(*********************************************************
Interval arithmetic over floatting points
diff --git a/src_common/ieee/coq/Colibri2_interval.v b/src_common/ieee/coq/Intv32.v
similarity index 100%
rename from src_common/ieee/coq/Colibri2_interval.v
rename to src_common/ieee/coq/Intv32.v
diff --git a/src_common/ieee/coq/Qextended.v b/src_common/ieee/coq/Qextended.v
new file mode 100644
index 0000000000000000000000000000000000000000..4b0181fff170e6acbeaca0ecbfd4523a08da8b51
--- /dev/null
+++ b/src_common/ieee/coq/Qextended.v
@@ -0,0 +1,66 @@
+From Coq Require Import ZArith Reals Qreals Extraction.
+From F Require Import Rextended.
+
+(** * A type of rationals suitable for conversions from and to fp
+ and compatible with zarith Q
+*)
+
+Record Qx := Qxmake {
+ num : Z.t; den : Z.t;
+ Hden1 : (0 <=? den)%Z = true;
+ Hden2 : (if den =? 0 then orb (orb (num =? -1) (num =? 0)) (num =? 1) else Z.gcd num den =? 1)%Z = true
+}.
+
+Lemma Hden2' :
+ forall q, (den q = 0 -> num q = -1 \/ num q = 0 \/ num q = 1)%Z.
+Proof.
+ intros q H.
+ rewrite <- !Z.eqb_eq in *.
+ assert (H2 := Hden2 q).
+ rewrite H in H2.
+ destruct (num q =? -1)%Z; destruct (num q =? 0)%Z; destruct (num q =? 1)%Z;
+ tauto.
+Qed.
+
+Definition Qx_zero := Qxmake 0%Z 1%Z (refl_equal _) (refl_equal _).
+Definition Qx_undef := Qxmake 0%Z 0%Z (refl_equal _) (refl_equal _).
+Definition Qx_inf := Qxmake 1%Z 0%Z (refl_equal _) (refl_equal _).
+Definition Qx_minus_inf := Qxmake (-1)%Z 0%Z (refl_equal _) (refl_equal _).
+Definition Qx_half := Qxmake (1)%Z 2%Z (refl_equal _) (refl_equal _).
+
+Inductive Qx_kind (q : Qx) := (* cf Q of Zarith *)
+ | Qx_INF: (num q = 1)%Z -> (den q = 0)%Z -> Qx_kind q
+ | Qx_MINF: (num q = -1)%Z -> (den q = 0)%Z -> Qx_kind q
+ | Qx_UNDEF: (num q = 0)%Z -> (den q = 0)%Z -> Qx_kind q
+ | Qx_ZERO: (num q = 0)%Z -> forall pq, (den q = Z.pos pq)%Z -> Qx_kind q
+ | Qx_NZERO: forall nq (s:{num q = Z.pos nq} + {num q = Z.neg nq}) pq, (den q = Z.pos pq)%Z -> Qx_kind q.
+
+Extraction Implicit Qx_ZERO [pq].
+Extraction Implicit Qx_NZERO [nq s pq].
+
+Lemma Qx_classify (q: Qx) : Qx_kind q.
+Proof.
+ intros.
+ case_eq (den q); [intros Hd | intros pd Hd| intros nd Hd].
+ - case_eq (num q); [intros Hn | intros pn Hn| intros nn Hn].
+ * exact (Qx_UNDEF q Hn Hd).
+ * assert (H: num q = ( 1)%Z) by (destruct (Hden2' q Hd) as [H|[H|H]]; rewrite Hn in *;
+ [discriminate H| discriminate H | assumption ]).
+ exact (Qx_INF q H Hd).
+ * assert (H: num q = (-1)%Z) by (destruct (Hden2' q Hd) as [H|[H|H]]; rewrite Hn in *;
+ [assumption| discriminate H | discriminate H]).
+ exact (Qx_MINF q H Hd).
+ - case_eq (num q); [intros Hn | intros nq Hn| intros nq Hn].
+ * exact (Qx_ZERO q Hn pd Hd).
+ * exact (Qx_NZERO q nq (left Hn) pd Hd).
+ * exact (Qx_NZERO q nq (right Hn) pd Hd).
+ - assert (A := Hden1 q).
+ rewrite Hd in A.
+ discriminate A.
+Defined.
+
+Definition Q2Rx q : Rx :=
+ if (den q =? 0)%Z then
+ if (num q =? 0)%Z then Real (0%R)
+ else Inf (num q <? 0)%Z
+ else Real (Q2R (Qmake (num q) (Z.to_pos (den q)))).
\ No newline at end of file
diff --git a/src_common/ieee/coq/_CoqProject b/src_common/ieee/coq/_CoqProject
index f7a97e9b7ce5f2476de2a49da004050fad8cf0ab..1666423c122b9987c7290808db6bdac441dd9065 100644
--- a/src_common/ieee/coq/_CoqProject
+++ b/src_common/ieee/coq/_CoqProject
@@ -1,8 +1,9 @@
-R ./ F
-./Domains.v
./Interval.v
-./Colibri2_interval.v
+./Intv32.v
./Tactics.v
./Rextended.v
+./Qextended.v
./Utils.v
+./B32.v
./Correction_thms.v
\ No newline at end of file