diff --git a/.gitignore b/.gitignore
index 9a29e7203869e1ecc46d5ff7d20d8bf5ac626a96..19cae1d82697e9c99de6c83af7113225881f0a66 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,6 +16,18 @@ why3shapes.gz
dolmen/
farith/
+# coq artifacts
+
+**/*.vo
+**/*.vok
+**/*.glob
+**/*.lia.cache
+**/*.aux
+**/*.vk
+**/.CoqMakefile.d
+**/*.vos
+**/CoqMakefile
+**/CoqMakefile.conf
# doc
*.html
@@ -27,3 +39,7 @@ farith/
# debug files
*debug_graph.tmp/
+
+# mac artifacts
+
+.DS_Store
\ No newline at end of file
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 93c4d178a6214e0d5fe2663ddeee85c6f376836c..f7e889a02cd5cbfd1f8e57192876a40edf57270d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,6 +1,5 @@
stages:
- test
- - deploy
.build-matrix:
parallel:
@@ -41,8 +40,10 @@ tests:
- opam pin --no-action --yes .
- opam depext --yes colibri2 colibrics farith
- opam install . --deps-only --locked --with-test --with-doc --yes
- - opam depext --yes --install why3 core jingoo yojson logs core # For generation not done in release mode
+ - opam repo add coq-released https://coq.inria.fr/opam/released
+ - opam depext --yes --install why3 core jingoo yojson logs core coq-flocq # For generation not done in release mode
- opam depext --yes --install ounit2 # For tests move to opam file?
+ - make -C farith2
- make
- make test
tags:
@@ -69,40 +70,32 @@ generate-static:
- opam depext --yes colibri2 colibrics farith
- opam install . --dry-run --deps-only --locked --with-test --with-doc --yes | awk '/-> installed/{print $3}' | xargs opam depext --yes
- opam install . --deps-only --locked --with-test --with-doc --yes
- - opam depext --yes --install why3 core jingoo yojson logs core # For generation not done in release mode
+ - opam repo add coq-released https://coq.inria.fr/opam/released
+ - opam depext --yes --install why3 core jingoo yojson logs core coq-flocq coq-coq2html # For generation not done in release mode
- opam depext --yes --install ounit2 # For tests move to opam file?
+ - echo -e "\e[31mCompile Farith2\e[0m"
+ - make -C farith2
+ - make -C farith2 doc
+ - tar -cvf farith2_doc.tar.gz farith2/doc/
+ - echo -e "\e[31mCompile Colibri2 static\e[0m"
- make
- make test
- dune install --destdir=destdir --prefix=/
- cp destdir/bin/colibri2 colibri2
+ - echo -e "\e[31mCreate Starexec archive\e[0m"
+ - mkdir bin
+ - mv colibri2 bin/
+ - mv misc/starexec_run_default bin/
+ - tar -cvf colibri2_starexec_$CI_COMMIT_SHORT_SHA.tar.gz bin/
tags:
- docker
rules:
- - if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
+ - if: $CI_COMMIT_BRANCH != $CI_DEFAULT_BRANCH
when: manual
allow_failure: true
- if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH
artifacts:
- expose_as: 'Colibri2 binary'
paths:
- colibri2
-
-starexec:
- stage: deploy
- # ocaml/opam:alpine-3.13-opam
- image: ocaml/opam@sha256:db94e740f73340f00113f09e5da81fe93183f241ac5974393cc51dfbdcc17b2d
- rules:
- - when: manual
- dependencies:
- - generate-static
- script:
- - mkdir bin
- - mv colibri2 bin/
- - mv misc/starexec_run_default bin/
- artifacts:
- expose_as: 'Starexec'
- name: 'colibri2_starexec_$CI_COMMIT_SHORT_SHA'
- paths:
- - bin/
- tags:
- - docker
+ - farith2_doc.tar.gz
+ - colibri2_starexec_$CI_COMMIT_SHORT_SHA.tar.gz
diff --git a/.lia.cache b/.lia.cache
new file mode 100644
index 0000000000000000000000000000000000000000..76ef9efc0b944a7bc41557da47a648f617d36de3
Binary files /dev/null and b/.lia.cache differ
diff --git a/doc/coq2html.js b/doc/coq2html.js
new file mode 100644
index 0000000000000000000000000000000000000000..d869b602b1c5c440f89ef0198d6c1130eb2d9c88
--- /dev/null
+++ b/doc/coq2html.js
@@ -0,0 +1,25 @@
+
+function toggleDisplay(id)
+{
+ var elt = document.getElementById(id);
+ if (elt.style.display == 'none') {
+ elt.style.display = 'block';
+ } else {
+ elt.style.display = 'none';
+ }
+}
+
+function hideAll(cls)
+{
+ var testClass = new RegExp("(^|s)" + cls + "(s|$)");
+ var tag = tag || "*";
+ var elements = document.getElementsByTagName("div");
+ var current;
+ var length = elements.length;
+ for(var i=0; i<length; i++){
+ current = elements[i];
+ if(testClass.test(current.className)) {
+ current.style.display = 'none';
+ }
+ }
+}
diff --git a/dune b/dune
index 0da6f6ffbb95d0e01b2d771ba974e6bf7b166b3b..9b7d214cb9666ef92a20b79f0c4c45d75c476175 100644
--- a/dune
+++ b/dune
@@ -1 +1 @@
-(vendored_dirs dolmen farith)
+(vendored_dirs dolmen farith farith2)
diff --git a/farith2/.gitignore b/farith2/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..a7d81f76f0912920a891a8325f5ffd2b6b603617
--- /dev/null
+++ b/farith2/.gitignore
@@ -0,0 +1,45 @@
+.*.aux
+.*.d
+*.a
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.glob
+*.ml.d
+*.ml4.d
+*.mlg.d
+*.mli.d
+*.mllib.d
+*.mlpack.d
+*.native
+*.o
+*.v.d
+*.vio
+*.vo
+*.vok
+*.vos
+.coq-native
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache
+native_compute_profile_*.data
+
+# generated timing files
+*.timing.diff
+*.v.after-timing
+*.v.before-timing
+*.v.timing
+time-of-build-after.log
+time-of-build-before.log
+time-of-build-both.log
+time-of-build-pretty.log
\ No newline at end of file
diff --git a/farith2/.nra.cache b/farith2/.nra.cache
new file mode 100644
index 0000000000000000000000000000000000000000..d98ef9c4b6c6b430155da61742d938534ee28064
Binary files /dev/null and b/farith2/.nra.cache differ
diff --git a/farith2/B32.ml b/farith2/B32.ml
new file mode 100644
index 0000000000000000000000000000000000000000..59a32b73f87cfe42b566455c13a4dc3f12353bef
--- /dev/null
+++ b/farith2/B32.ml
@@ -0,0 +1,143 @@
+open BinInt
+open Binary
+open BinarySingleNaN
+open Bits
+open Datatypes
+open SpecFloat
+
+module B32 =
+ struct
+ (** val prec : Farith_Big.big_int **)
+
+ let prec =
+ (Farith_Big.double (Farith_Big.double (Farith_Big.double
+ (Farith_Big.succ_double Farith_Big.one))))
+
+ (** val emax : Farith_Big.big_int **)
+
+ let emax =
+ (Farith_Big.double (Farith_Big.double (Farith_Big.double
+ (Farith_Big.double (Farith_Big.double (Farith_Big.double
+ (Farith_Big.double Farith_Big.one)))))))
+
+ (** val mw : Farith_Big.big_int **)
+
+ let mw =
+ (Farith_Big.succ_double (Farith_Big.succ_double (Farith_Big.succ_double
+ (Farith_Big.double Farith_Big.one))))
+
+ (** val ew : Farith_Big.big_int **)
+
+ let ew =
+ (Farith_Big.double (Farith_Big.double (Farith_Big.double Farith_Big.one)))
+
+ type t = binary_float
+
+ (** val add : Farith_Big.mode -> t -> t -> t **)
+
+ let add =
+ coq_Bplus prec emax
+
+ (** val sub : Farith_Big.mode -> t -> t -> t **)
+
+ let sub =
+ coq_Bminus prec emax
+
+ (** val mult : Farith_Big.mode -> t -> t -> t **)
+
+ let mult =
+ coq_Bmult prec emax
+
+ (** val div : Farith_Big.mode -> t -> t -> t **)
+
+ let div =
+ coq_Bdiv prec emax
+
+ (** val sqrt : Farith_Big.mode -> t -> t **)
+
+ let sqrt =
+ coq_Bsqrt prec emax
+
+ (** val abs : t -> t **)
+
+ let abs =
+ coq_Babs prec emax
+
+ (** val le : t -> t -> bool **)
+
+ let le =
+ coq_Bleb prec emax
+
+ (** val lt : t -> t -> bool **)
+
+ let lt =
+ coq_Bltb prec emax
+
+ (** val eq : t -> t -> bool **)
+
+ let eq =
+ coq_Beqb prec emax
+
+ (** val ge : t -> t -> bool **)
+
+ let ge x y =
+ coq_Bleb prec emax y x
+
+ (** val gt : t -> t -> bool **)
+
+ let gt x y =
+ coq_Bltb prec emax y x
+
+ (** val of_bits : Farith_Big.big_int -> t **)
+
+ let of_bits b =
+ match binary_float_of_bits mw ew b with
+ | Binary.B754_zero s -> B754_zero s
+ | Binary.B754_infinity s -> B754_infinity s
+ | Binary.B754_nan (_, _) -> B754_nan
+ | Binary.B754_finite (s, m, e) -> B754_finite (s, m, e)
+
+ (** val pl_cst : Farith_Big.big_int **)
+
+ let pl_cst =
+ Farith_Big.iter_nat (fun x -> Farith_Big.double x)
+ (Z.to_nat (Farith_Big.pred mw)) Farith_Big.one
+
+ (** val to_bits : t -> Farith_Big.big_int **)
+
+ let to_bits = function
+ | B754_zero s -> bits_of_binary_float mw ew (Binary.B754_zero s)
+ | B754_infinity s -> bits_of_binary_float mw ew (Binary.B754_infinity s)
+ | B754_nan -> bits_of_binary_float mw ew (Binary.B754_nan (true, pl_cst))
+ | B754_finite (s, m, e) ->
+ bits_of_binary_float mw ew (Binary.B754_finite (s, m, e))
+
+ (** val of_q : Farith_Big.mode -> Q.t -> t **)
+
+ let of_q m q =
+ match Q.classify q with
+ | Q.INF -> B754_infinity false
+ | Q.MINF -> B754_infinity true
+ | Q.UNDEF -> B754_nan
+ | Q.ZERO -> B754_zero false
+ | Q.NZERO ->
+ (Farith_Big.z_case
+ (fun _ -> B754_nan)
+ (fun pn ->
+ coq_SF2B prec emax
+ (let (p, lz) =
+ coq_SFdiv_core_binary prec emax pn Farith_Big.zero
+ (Z.to_pos (Farith_Big.q_den q)) Farith_Big.zero
+ in
+ let (mz, ez) = p in
+ binary_round_aux prec emax m (xorb false false) mz ez lz))
+ (fun nn ->
+ coq_SF2B prec emax
+ (let (p, lz) =
+ coq_SFdiv_core_binary prec emax nn Farith_Big.zero
+ (Z.to_pos (Farith_Big.q_den q)) Farith_Big.zero
+ in
+ let (mz, ez) = p in
+ binary_round_aux prec emax m (xorb true false) mz ez lz))
+ (Farith_Big.q_num q))
+ end
diff --git a/farith2/B32.mli b/farith2/B32.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e20ce0b7e88057374bc5023cf1911de183703639
--- /dev/null
+++ b/farith2/B32.mli
@@ -0,0 +1,49 @@
+open BinInt
+open Binary
+open BinarySingleNaN
+open Bits
+open Datatypes
+open SpecFloat
+
+module B32 :
+ sig
+ val prec : Farith_Big.big_int
+
+ val emax : Farith_Big.big_int
+
+ val mw : Farith_Big.big_int
+
+ val ew : Farith_Big.big_int
+
+ type t = binary_float
+
+ val add : Farith_Big.mode -> t -> t -> t
+
+ val sub : Farith_Big.mode -> t -> t -> t
+
+ val mult : Farith_Big.mode -> t -> t -> t
+
+ val div : Farith_Big.mode -> t -> t -> t
+
+ val sqrt : Farith_Big.mode -> t -> t
+
+ val abs : t -> t
+
+ val le : t -> t -> bool
+
+ val lt : t -> t -> bool
+
+ val eq : t -> t -> bool
+
+ val ge : t -> t -> bool
+
+ val gt : t -> t -> bool
+
+ val of_bits : Farith_Big.big_int -> t
+
+ val pl_cst : Farith_Big.big_int
+
+ val to_bits : t -> Farith_Big.big_int
+
+ val of_q : Farith_Big.mode -> Q.t -> t
+ end
diff --git a/farith2/BinInt.ml b/farith2/BinInt.ml
new file mode 100644
index 0000000000000000000000000000000000000000..fc758fddab7cfa584a13b8e4514dc0ff942589e9
--- /dev/null
+++ b/farith2/BinInt.ml
@@ -0,0 +1,83 @@
+
+module Z =
+ struct
+ type t = Farith_Big.big_int
+
+ (** val pow :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
+
+ let pow x y =
+ Farith_Big.z_case
+ (fun _ -> Farith_Big.one)
+ (fun p -> Farith_Big.pow_pos x p)
+ (fun _ -> Farith_Big.zero)
+ y
+
+ (** val to_nat : Farith_Big.big_int -> Farith_Big.big_int **)
+
+ let to_nat z =
+ Farith_Big.z_case
+ (fun _ -> Farith_Big.zero)
+ (fun p -> Farith_Big.identity p)
+ (fun _ -> Farith_Big.zero)
+ z
+
+ (** val to_pos : Farith_Big.big_int -> Farith_Big.big_int **)
+
+ let to_pos z =
+ Farith_Big.z_case
+ (fun _ -> Farith_Big.one)
+ (fun p -> p)
+ (fun _ -> Farith_Big.one)
+ z
+
+ (** val pos_div_eucl :
+ Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int * Farith_Big.big_int **)
+
+ let rec pos_div_eucl a b =
+ Farith_Big.positive_case
+ (fun a' ->
+ let (q, r) = pos_div_eucl a' b in
+ let r' =
+ Farith_Big.add (Farith_Big.mult (Farith_Big.double Farith_Big.one) r)
+ Farith_Big.one
+ in
+ if Farith_Big.lt r' b
+ then ((Farith_Big.mult (Farith_Big.double Farith_Big.one) q), r')
+ else ((Farith_Big.add
+ (Farith_Big.mult (Farith_Big.double Farith_Big.one) q)
+ Farith_Big.one), (Farith_Big.sub r' b)))
+ (fun a' ->
+ let (q, r) = pos_div_eucl a' b in
+ let r' = Farith_Big.mult (Farith_Big.double Farith_Big.one) r in
+ if Farith_Big.lt r' b
+ then ((Farith_Big.mult (Farith_Big.double Farith_Big.one) q), r')
+ else ((Farith_Big.add
+ (Farith_Big.mult (Farith_Big.double Farith_Big.one) q)
+ Farith_Big.one), (Farith_Big.sub r' b)))
+ (fun _ ->
+ if Farith_Big.le (Farith_Big.double Farith_Big.one) b
+ then (Farith_Big.zero, Farith_Big.one)
+ else (Farith_Big.one, Farith_Big.zero))
+ a
+
+ (** val even : Farith_Big.big_int -> bool **)
+
+ let even z =
+ Farith_Big.z_case
+ (fun _ -> true)
+ (fun p ->
+ Farith_Big.positive_case
+ (fun _ -> false)
+ (fun _ -> true)
+ (fun _ -> false)
+ p)
+ (fun p ->
+ Farith_Big.positive_case
+ (fun _ -> false)
+ (fun _ -> true)
+ (fun _ -> false)
+ p)
+ z
+ end
diff --git a/farith2/BinInt.mli b/farith2/BinInt.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c0985b8cd475d4d04c18e43ecd1062fde75095e9
--- /dev/null
+++ b/farith2/BinInt.mli
@@ -0,0 +1,17 @@
+
+module Z :
+ sig
+ type t = Farith_Big.big_int
+
+ val pow : Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
+
+ val to_nat : Farith_Big.big_int -> Farith_Big.big_int
+
+ val to_pos : Farith_Big.big_int -> Farith_Big.big_int
+
+ val pos_div_eucl :
+ Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int * Farith_Big.big_int
+
+ val even : Farith_Big.big_int -> bool
+ end
diff --git a/farith2/BinNums.ml b/farith2/BinNums.ml
new file mode 100644
index 0000000000000000000000000000000000000000..139597f9cb07c5d48bed18984ec4747f4b4f3438
--- /dev/null
+++ b/farith2/BinNums.ml
@@ -0,0 +1,2 @@
+
+
diff --git a/farith2/BinNums.mli b/farith2/BinNums.mli
new file mode 100644
index 0000000000000000000000000000000000000000..139597f9cb07c5d48bed18984ec4747f4b4f3438
--- /dev/null
+++ b/farith2/BinNums.mli
@@ -0,0 +1,2 @@
+
+
diff --git a/farith2/BinPos.ml b/farith2/BinPos.ml
new file mode 100644
index 0000000000000000000000000000000000000000..36df342ec382f6fbc471c010adf71baa3d412a2c
--- /dev/null
+++ b/farith2/BinPos.ml
@@ -0,0 +1,165 @@
+open BinPosDef
+
+module Pos =
+ struct
+ (** val add_carry :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
+
+ let rec add_carry = fun p q -> Farith_Big.succ (Farith_Big.add p q)
+
+ type mask = Pos.mask =
+ | IsNul
+ | IsPos of Farith_Big.big_int
+ | IsNeg
+
+ (** val succ_double_mask : mask -> mask **)
+
+ let succ_double_mask = function
+ | IsNul -> IsPos Farith_Big.one
+ | IsPos p -> IsPos (Farith_Big.succ_double p)
+ | IsNeg -> IsNeg
+
+ (** val double_mask : mask -> mask **)
+
+ let double_mask = function
+ | IsPos p -> IsPos (Farith_Big.double p)
+ | x0 -> x0
+
+ (** val double_pred_mask : Farith_Big.big_int -> mask **)
+
+ let double_pred_mask x =
+ Farith_Big.positive_case
+ (fun p -> IsPos (Farith_Big.double (Farith_Big.double p)))
+ (fun p -> IsPos (Farith_Big.double
+ (Farith_Big.pred_double p)))
+ (fun _ -> IsNul)
+ x
+
+ (** val sub_mask : Farith_Big.big_int -> Farith_Big.big_int -> mask **)
+
+ let rec sub_mask x y =
+ Farith_Big.positive_case
+ (fun p ->
+ Farith_Big.positive_case
+ (fun q -> double_mask (sub_mask p q))
+ (fun q -> succ_double_mask (sub_mask p q))
+ (fun _ -> IsPos (Farith_Big.double p))
+ y)
+ (fun p ->
+ Farith_Big.positive_case
+ (fun q -> succ_double_mask (sub_mask_carry p q))
+ (fun q -> double_mask (sub_mask p q))
+ (fun _ -> IsPos (Farith_Big.pred_double p))
+ y)
+ (fun _ ->
+ Farith_Big.positive_case
+ (fun _ -> IsNeg)
+ (fun _ -> IsNeg)
+ (fun _ -> IsNul)
+ y)
+ x
+
+ (** val sub_mask_carry :
+ Farith_Big.big_int -> Farith_Big.big_int -> mask **)
+
+ and sub_mask_carry x y =
+ Farith_Big.positive_case
+ (fun p ->
+ Farith_Big.positive_case
+ (fun q -> succ_double_mask (sub_mask_carry p q))
+ (fun q -> double_mask (sub_mask p q))
+ (fun _ -> IsPos (Farith_Big.pred_double p))
+ y)
+ (fun p ->
+ Farith_Big.positive_case
+ (fun q -> double_mask (sub_mask_carry p q))
+ (fun q -> succ_double_mask (sub_mask_carry p q))
+ (fun _ -> double_pred_mask p)
+ y)
+ (fun _ -> IsNeg)
+ x
+
+ (** val iter : ('a1 -> 'a1) -> 'a1 -> Farith_Big.big_int -> 'a1 **)
+
+ let rec iter f x n =
+ Farith_Big.positive_case
+ (fun n' -> f (iter f (iter f x n') n'))
+ (fun n' -> iter f (iter f x n') n')
+ (fun _ -> f x)
+ n
+
+ (** val div2 : Farith_Big.big_int -> Farith_Big.big_int **)
+
+ let div2 p =
+ Farith_Big.positive_case
+ (fun p0 -> p0)
+ (fun p0 -> p0)
+ (fun _ -> Farith_Big.one)
+ p
+
+ (** val div2_up : Farith_Big.big_int -> Farith_Big.big_int **)
+
+ let div2_up p =
+ Farith_Big.positive_case
+ (fun p0 -> Farith_Big.succ p0)
+ (fun p0 -> p0)
+ (fun _ -> Farith_Big.one)
+ p
+
+ (** val sqrtrem_step :
+ (Farith_Big.big_int -> Farith_Big.big_int) -> (Farith_Big.big_int ->
+ Farith_Big.big_int) -> (Farith_Big.big_int * mask) ->
+ Farith_Big.big_int * mask **)
+
+ let sqrtrem_step f g = function
+ | (s, y) ->
+ (match y with
+ | IsPos r ->
+ let s' = Farith_Big.succ_double (Farith_Big.double s) in
+ let r' = g (f r) in
+ if Farith_Big.le s' r'
+ then ((Farith_Big.succ_double s), (sub_mask r' s'))
+ else ((Farith_Big.double s), (IsPos r'))
+ | _ ->
+ ((Farith_Big.double s),
+ (sub_mask (g (f Farith_Big.one)) (Farith_Big.double
+ (Farith_Big.double Farith_Big.one)))))
+
+ (** val sqrtrem : Farith_Big.big_int -> Farith_Big.big_int * mask **)
+
+ let rec sqrtrem p =
+ Farith_Big.positive_case
+ (fun p0 ->
+ Farith_Big.positive_case
+ (fun p1 ->
+ sqrtrem_step (fun x -> Farith_Big.succ_double x) (fun x ->
+ Farith_Big.succ_double x) (sqrtrem p1))
+ (fun p1 ->
+ sqrtrem_step (fun x -> Farith_Big.double x) (fun x ->
+ Farith_Big.succ_double x) (sqrtrem p1))
+ (fun _ -> (Farith_Big.one, (IsPos (Farith_Big.double
+ Farith_Big.one))))
+ p0)
+ (fun p0 ->
+ Farith_Big.positive_case
+ (fun p1 ->
+ sqrtrem_step (fun x -> Farith_Big.succ_double x) (fun x ->
+ Farith_Big.double x) (sqrtrem p1))
+ (fun p1 ->
+ sqrtrem_step (fun x -> Farith_Big.double x) (fun x ->
+ Farith_Big.double x) (sqrtrem p1))
+ (fun _ -> (Farith_Big.one, (IsPos Farith_Big.one)))
+ p0)
+ (fun _ -> (Farith_Big.one, IsNul))
+ p
+
+ (** val iter_op :
+ ('a1 -> 'a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1 **)
+
+ let rec iter_op op p a =
+ Farith_Big.positive_case
+ (fun p0 -> op a (iter_op op p0 (op a a)))
+ (fun p0 -> iter_op op p0 (op a a))
+ (fun _ -> a)
+ p
+ end
diff --git a/farith2/BinPos.mli b/farith2/BinPos.mli
new file mode 100644
index 0000000000000000000000000000000000000000..00dbe4ffa8517199cf70622e0a701d540499afa4
--- /dev/null
+++ b/farith2/BinPos.mli
@@ -0,0 +1,37 @@
+open BinPosDef
+
+module Pos :
+ sig
+ val add_carry :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
+
+ type mask = Pos.mask =
+ | IsNul
+ | IsPos of Farith_Big.big_int
+ | IsNeg
+
+ val succ_double_mask : mask -> mask
+
+ val double_mask : mask -> mask
+
+ val double_pred_mask : Farith_Big.big_int -> mask
+
+ val sub_mask : Farith_Big.big_int -> Farith_Big.big_int -> mask
+
+ val sub_mask_carry : Farith_Big.big_int -> Farith_Big.big_int -> mask
+
+ val iter : ('a1 -> 'a1) -> 'a1 -> Farith_Big.big_int -> 'a1
+
+ val div2 : Farith_Big.big_int -> Farith_Big.big_int
+
+ val div2_up : Farith_Big.big_int -> Farith_Big.big_int
+
+ val sqrtrem_step :
+ (Farith_Big.big_int -> Farith_Big.big_int) -> (Farith_Big.big_int ->
+ Farith_Big.big_int) -> (Farith_Big.big_int * mask) ->
+ Farith_Big.big_int * mask
+
+ val sqrtrem : Farith_Big.big_int -> Farith_Big.big_int * mask
+
+ val iter_op : ('a1 -> 'a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1
+ end
diff --git a/farith2/BinPosDef.ml b/farith2/BinPosDef.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e1f8f253c83dbb38118366a179331bdd84bcee5e
--- /dev/null
+++ b/farith2/BinPosDef.ml
@@ -0,0 +1,8 @@
+
+module Pos =
+ struct
+ type mask =
+ | IsNul
+ | IsPos of Farith_Big.big_int
+ | IsNeg
+ end
diff --git a/farith2/BinPosDef.mli b/farith2/BinPosDef.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ae03b859d41d6c6d966489dbfd57a4e72fc34104
--- /dev/null
+++ b/farith2/BinPosDef.mli
@@ -0,0 +1,8 @@
+
+module Pos :
+ sig
+ type mask =
+ | IsNul
+ | IsPos of Farith_Big.big_int
+ | IsNeg
+ end
diff --git a/farith2/Binary.ml b/farith2/Binary.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1fc1c209b69892ff1cd4f018bdba4e92e64982fd
--- /dev/null
+++ b/farith2/Binary.ml
@@ -0,0 +1,21 @@
+
+type full_float =
+| F754_zero of bool
+| F754_infinity of bool
+| F754_nan of bool * Farith_Big.big_int
+| F754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
+
+type binary_float =
+| B754_zero of bool
+| B754_infinity of bool
+| B754_nan of bool * Farith_Big.big_int
+| B754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
+
+(** val coq_FF2B :
+ Farith_Big.big_int -> Farith_Big.big_int -> full_float -> binary_float **)
+
+let coq_FF2B _ _ = function
+| F754_zero s -> B754_zero s
+| F754_infinity s -> B754_infinity s
+| F754_nan (b, pl) -> B754_nan (b, pl)
+| F754_finite (s, m, e) -> B754_finite (s, m, e)
diff --git a/farith2/Binary.mli b/farith2/Binary.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a9eb82be8428482583b233c3cf204d316fd68cae
--- /dev/null
+++ b/farith2/Binary.mli
@@ -0,0 +1,15 @@
+
+type full_float =
+| F754_zero of bool
+| F754_infinity of bool
+| F754_nan of bool * Farith_Big.big_int
+| F754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
+
+type binary_float =
+| B754_zero of bool
+| B754_infinity of bool
+| B754_nan of bool * Farith_Big.big_int
+| B754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
+
+val coq_FF2B :
+ Farith_Big.big_int -> Farith_Big.big_int -> full_float -> binary_float
diff --git a/farith2/BinarySingleNaN.ml b/farith2/BinarySingleNaN.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f3f6d10d7cf7e39663c172a24cfa549d08de13bf
--- /dev/null
+++ b/farith2/BinarySingleNaN.ml
@@ -0,0 +1,295 @@
+open BinInt
+open Bool
+open Datatypes
+open Round
+open SpecFloat
+
+type binary_float =
+| B754_zero of bool
+| B754_infinity of bool
+| B754_nan
+| B754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
+
+(** val coq_SF2B :
+ Farith_Big.big_int -> Farith_Big.big_int -> spec_float -> binary_float **)
+
+let coq_SF2B _ _ = function
+| S754_zero s -> B754_zero s
+| S754_infinity s -> B754_infinity s
+| S754_nan -> B754_nan
+| S754_finite (s, m, e) -> B754_finite (s, m, e)
+
+(** val coq_B2SF :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> spec_float **)
+
+let coq_B2SF _ _ = function
+| B754_zero s -> S754_zero s
+| B754_infinity s -> S754_infinity s
+| B754_nan -> S754_nan
+| B754_finite (s, m, e) -> S754_finite (s, m, e)
+
+(** val is_nan :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool **)
+
+let is_nan _ _ = function
+| B754_nan -> true
+| _ -> false
+
+(** val coq_Babs :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float **)
+
+let coq_Babs _ _ x = match x with
+| B754_zero _ -> B754_zero false
+| B754_infinity _ -> B754_infinity false
+| B754_nan -> x
+| B754_finite (_, mx, ex) -> B754_finite (false, mx, ex)
+
+(** val coq_Beqb :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float
+ -> bool **)
+
+let coq_Beqb prec emax f1 f2 =
+ coq_SFeqb (coq_B2SF prec emax f1) (coq_B2SF prec emax f2)
+
+(** val coq_Bltb :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float
+ -> bool **)
+
+let coq_Bltb prec emax f1 f2 =
+ coq_SFltb (coq_B2SF prec emax f1) (coq_B2SF prec emax f2)
+
+(** val coq_Bleb :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float
+ -> bool **)
+
+let coq_Bleb prec emax f1 f2 =
+ coq_SFleb (coq_B2SF prec emax f1) (coq_B2SF prec emax f2)
+
+(** val choice_mode :
+ Farith_Big.mode -> bool -> Farith_Big.big_int -> location ->
+ Farith_Big.big_int **)
+
+let choice_mode m sx mx lx =
+ match m with
+ | Farith_Big.NE -> cond_incr (round_N (Pervasives.not (Z.even mx)) lx) mx
+ | Farith_Big.ZR -> mx
+ | Farith_Big.DN -> cond_incr (round_sign_DN sx lx) mx
+ | Farith_Big.UP -> cond_incr (round_sign_UP sx lx) mx
+ | Farith_Big.NA -> cond_incr (round_N true lx) mx
+
+(** val overflow_to_inf : Farith_Big.mode -> bool -> bool **)
+
+let overflow_to_inf m s =
+ match m with
+ | Farith_Big.ZR -> false
+ | Farith_Big.DN -> s
+ | Farith_Big.UP -> Pervasives.not s
+ | _ -> true
+
+(** val binary_overflow :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool ->
+ spec_float **)
+
+let binary_overflow prec emax m s =
+ if overflow_to_inf m s
+ then S754_infinity s
+ else S754_finite (s,
+ (Z.to_pos
+ (Farith_Big.sub (Z.pow (Farith_Big.double Farith_Big.one) prec)
+ Farith_Big.one)), (Farith_Big.sub emax prec))
+
+(** val binary_fit_aux :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool ->
+ Farith_Big.big_int -> Farith_Big.big_int -> spec_float **)
+
+let binary_fit_aux prec emax mode0 sx mx ex =
+ if Farith_Big.le ex (Farith_Big.sub emax prec)
+ then S754_finite (sx, mx, ex)
+ else binary_overflow prec emax mode0 sx
+
+(** val binary_round_aux :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool ->
+ Farith_Big.big_int -> Farith_Big.big_int -> location -> spec_float **)
+
+let binary_round_aux prec emax mode0 sx mx ex lx =
+ let (mrs', e') = shr_fexp prec emax mx ex lx in
+ let (mrs'', e'') =
+ shr_fexp prec emax
+ (choice_mode mode0 sx mrs'.shr_m (loc_of_shr_record mrs')) e'
+ Coq_loc_Exact
+ in
+ (Farith_Big.z_case
+ (fun _ -> S754_zero sx)
+ (fun m -> binary_fit_aux prec emax mode0 sx m e'')
+ (fun _ -> S754_nan)
+ mrs''.shr_m)
+
+(** val coq_Bmult :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ binary_float -> binary_float -> binary_float **)
+
+let coq_Bmult prec emax m x y =
+ match x with
+ | B754_zero sx ->
+ (match y with
+ | B754_zero sy -> B754_zero (xorb sx sy)
+ | B754_finite (sy, _, _) -> B754_zero (xorb sx sy)
+ | _ -> B754_nan)
+ | B754_infinity sx ->
+ (match y with
+ | B754_infinity sy -> B754_infinity (xorb sx sy)
+ | B754_finite (sy, _, _) -> B754_infinity (xorb sx sy)
+ | _ -> B754_nan)
+ | B754_nan -> B754_nan
+ | B754_finite (sx, mx, ex) ->
+ (match y with
+ | B754_zero sy -> B754_zero (xorb sx sy)
+ | B754_infinity sy -> B754_infinity (xorb sx sy)
+ | B754_nan -> B754_nan
+ | B754_finite (sy, my, ey) ->
+ coq_SF2B prec emax
+ (binary_round_aux prec emax m (xorb sx sy) (Farith_Big.mult mx my)
+ (Farith_Big.add ex ey) Coq_loc_Exact))
+
+(** val shl_align_fexp :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int -> Farith_Big.big_int * Farith_Big.big_int **)
+
+let shl_align_fexp prec emax mx ex =
+ shl_align mx ex (fexp prec emax (Farith_Big.add (digits2_pos mx) ex))
+
+(** val binary_round :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool ->
+ Farith_Big.big_int -> Farith_Big.big_int -> spec_float **)
+
+let binary_round prec emax m sx mx ex =
+ let (mz, ez) = shl_align_fexp prec emax mx ex in
+ binary_round_aux prec emax m sx mz ez Coq_loc_Exact
+
+(** val binary_normalize :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ Farith_Big.big_int -> Farith_Big.big_int -> bool -> binary_float **)
+
+let binary_normalize prec emax mode0 m e szero =
+ Farith_Big.z_case
+ (fun _ -> B754_zero szero)
+ (fun m0 ->
+ coq_SF2B prec emax (binary_round prec emax mode0 false m0 e))
+ (fun m0 -> coq_SF2B prec emax (binary_round prec emax mode0 true m0 e))
+ m
+
+(** val coq_Bplus :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ binary_float -> binary_float -> binary_float **)
+
+let coq_Bplus prec emax m x y =
+ match x with
+ | B754_zero sx ->
+ (match y with
+ | B754_zero sy ->
+ if eqb sx sy
+ then x
+ else (match m with
+ | Farith_Big.DN -> B754_zero true
+ | _ -> B754_zero false)
+ | B754_nan -> B754_nan
+ | _ -> y)
+ | B754_infinity sx ->
+ (match y with
+ | B754_infinity sy -> if eqb sx sy then x else B754_nan
+ | B754_nan -> B754_nan
+ | _ -> x)
+ | B754_nan -> B754_nan
+ | B754_finite (sx, mx, ex) ->
+ (match y with
+ | B754_zero _ -> x
+ | B754_infinity _ -> y
+ | B754_nan -> B754_nan
+ | B754_finite (sy, my, ey) ->
+ let ez = Farith_Big.min ex ey in
+ binary_normalize prec emax m
+ (Farith_Big.add (cond_Zopp sx (Pervasives.fst (shl_align mx ex ez)))
+ (cond_Zopp sy (Pervasives.fst (shl_align my ey ez)))) ez
+ (match m with
+ | Farith_Big.DN -> true
+ | _ -> false))
+
+(** val coq_Bminus :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ binary_float -> binary_float -> binary_float **)
+
+let coq_Bminus prec emax m x y =
+ match x with
+ | B754_zero sx ->
+ (match y with
+ | B754_zero sy ->
+ if eqb sx (Pervasives.not sy)
+ then x
+ else (match m with
+ | Farith_Big.DN -> B754_zero true
+ | _ -> B754_zero false)
+ | B754_infinity sy -> B754_infinity (Pervasives.not sy)
+ | B754_nan -> B754_nan
+ | B754_finite (sy, my, ey) -> B754_finite ((Pervasives.not sy), my, ey))
+ | B754_infinity sx ->
+ (match y with
+ | B754_infinity sy -> if eqb sx (Pervasives.not sy) then x else B754_nan
+ | B754_nan -> B754_nan
+ | _ -> x)
+ | B754_nan -> B754_nan
+ | B754_finite (sx, mx, ex) ->
+ (match y with
+ | B754_zero _ -> x
+ | B754_infinity sy -> B754_infinity (Pervasives.not sy)
+ | B754_nan -> B754_nan
+ | B754_finite (sy, my, ey) ->
+ let ez = Farith_Big.min ex ey in
+ binary_normalize prec emax m
+ (Farith_Big.sub (cond_Zopp sx (Pervasives.fst (shl_align mx ex ez)))
+ (cond_Zopp sy (Pervasives.fst (shl_align my ey ez)))) ez
+ (match m with
+ | Farith_Big.DN -> true
+ | _ -> false))
+
+(** val coq_Bdiv :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ binary_float -> binary_float -> binary_float **)
+
+let coq_Bdiv prec emax m x y =
+ match x with
+ | B754_zero sx ->
+ (match y with
+ | B754_infinity sy -> B754_zero (xorb sx sy)
+ | B754_finite (sy, _, _) -> B754_zero (xorb sx sy)
+ | _ -> B754_nan)
+ | B754_infinity sx ->
+ (match y with
+ | B754_zero sy -> B754_infinity (xorb sx sy)
+ | B754_finite (sy, _, _) -> B754_infinity (xorb sx sy)
+ | _ -> B754_nan)
+ | B754_nan -> B754_nan
+ | B754_finite (sx, mx, ex) ->
+ (match y with
+ | B754_zero sy -> B754_infinity (xorb sx sy)
+ | B754_infinity sy -> B754_zero (xorb sx sy)
+ | B754_nan -> B754_nan
+ | B754_finite (sy, my, ey) ->
+ coq_SF2B prec emax
+ (let (p, lz) = coq_SFdiv_core_binary prec emax mx ex my ey in
+ let (mz, ez) = p in
+ binary_round_aux prec emax m (xorb sx sy) mz ez lz))
+
+(** val coq_Bsqrt :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ binary_float -> binary_float **)
+
+let coq_Bsqrt prec emax m x = match x with
+| B754_zero _ -> x
+| B754_infinity s -> if s then B754_nan else x
+| B754_nan -> B754_nan
+| B754_finite (sx, mx, ex) ->
+ if sx
+ then B754_nan
+ else coq_SF2B prec emax
+ (let (p, lz) = coq_SFsqrt_core_binary prec emax mx ex in
+ let (mz, ez) = p in binary_round_aux prec emax m false mz ez lz)
diff --git a/farith2/BinarySingleNaN.mli b/farith2/BinarySingleNaN.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5a6d651e302909b2e7c9f2c191b1dd378ed9c7e8
--- /dev/null
+++ b/farith2/BinarySingleNaN.mli
@@ -0,0 +1,84 @@
+open BinInt
+open Bool
+open Datatypes
+open Round
+open SpecFloat
+
+type binary_float =
+| B754_zero of bool
+| B754_infinity of bool
+| B754_nan
+| B754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
+
+val coq_SF2B :
+ Farith_Big.big_int -> Farith_Big.big_int -> spec_float -> binary_float
+
+val coq_B2SF :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> spec_float
+
+val is_nan : Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool
+
+val coq_Babs :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float
+
+val coq_Beqb :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float ->
+ bool
+
+val coq_Bltb :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float ->
+ bool
+
+val coq_Bleb :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float ->
+ bool
+
+val choice_mode :
+ Farith_Big.mode -> bool -> Farith_Big.big_int -> location ->
+ Farith_Big.big_int
+
+val overflow_to_inf : Farith_Big.mode -> bool -> bool
+
+val binary_overflow :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool ->
+ spec_float
+
+val binary_fit_aux :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool ->
+ Farith_Big.big_int -> Farith_Big.big_int -> spec_float
+
+val binary_round_aux :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool ->
+ Farith_Big.big_int -> Farith_Big.big_int -> location -> spec_float
+
+val coq_Bmult :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
+ -> binary_float -> binary_float
+
+val shl_align_fexp :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int -> Farith_Big.big_int * Farith_Big.big_int
+
+val binary_round :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool ->
+ Farith_Big.big_int -> Farith_Big.big_int -> spec_float
+
+val binary_normalize :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ Farith_Big.big_int -> Farith_Big.big_int -> bool -> binary_float
+
+val coq_Bplus :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
+ -> binary_float -> binary_float
+
+val coq_Bminus :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> 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
+
+val coq_Bsqrt :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
+ -> binary_float
diff --git a/farith2/Bits.ml b/farith2/Bits.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a842d4305f0164bb7ae55b4404c840d7d5d821b1
--- /dev/null
+++ b/farith2/Bits.ml
@@ -0,0 +1,108 @@
+open BinInt
+open Binary
+
+(** val join_bits :
+ Farith_Big.big_int -> Farith_Big.big_int -> bool -> Farith_Big.big_int ->
+ Farith_Big.big_int -> Farith_Big.big_int **)
+
+let join_bits mw ew s m e =
+ Farith_Big.add
+ (Farith_Big.shiftl
+ (Farith_Big.add
+ (if s
+ then Z.pow (Farith_Big.double Farith_Big.one) ew
+ else Farith_Big.zero) e) mw) m
+
+(** val split_bits :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ (bool * Farith_Big.big_int) * Farith_Big.big_int **)
+
+let split_bits mw ew x =
+ let mm = Z.pow (Farith_Big.double Farith_Big.one) mw in
+ let em = Z.pow (Farith_Big.double Farith_Big.one) ew in
+ (((Farith_Big.le (Farith_Big.mult mm em) x), (Farith_Big.mod_floor x mm)),
+ (Farith_Big.mod_floor (Farith_Big.div_floor x mm) em))
+
+(** val bits_of_binary_float :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float ->
+ Farith_Big.big_int **)
+
+let bits_of_binary_float mw ew =
+ let emax =
+ Z.pow (Farith_Big.double Farith_Big.one)
+ (Farith_Big.sub ew Farith_Big.one)
+ in
+ let prec = Farith_Big.add mw Farith_Big.one in
+ let emin =
+ Farith_Big.sub
+ (Farith_Big.sub (Farith_Big.succ_double Farith_Big.one) emax) prec
+ in
+ (fun x ->
+ match x with
+ | B754_zero sx -> join_bits mw ew sx Farith_Big.zero Farith_Big.zero
+ | B754_infinity sx ->
+ join_bits mw ew sx Farith_Big.zero
+ (Farith_Big.sub (Z.pow (Farith_Big.double Farith_Big.one) ew)
+ Farith_Big.one)
+ | B754_nan (sx, plx) ->
+ join_bits mw ew sx plx
+ (Farith_Big.sub (Z.pow (Farith_Big.double Farith_Big.one) ew)
+ Farith_Big.one)
+ | B754_finite (sx, mx, ex) ->
+ let m = Farith_Big.sub mx (Z.pow (Farith_Big.double Farith_Big.one) mw) in
+ if Farith_Big.le Farith_Big.zero m
+ then join_bits mw ew sx m
+ (Farith_Big.add (Farith_Big.sub ex emin) Farith_Big.one)
+ else join_bits mw ew sx mx Farith_Big.zero)
+
+(** val binary_float_of_bits_aux :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ full_float **)
+
+let binary_float_of_bits_aux mw ew =
+ let emax =
+ Z.pow (Farith_Big.double Farith_Big.one)
+ (Farith_Big.sub ew Farith_Big.one)
+ in
+ let prec = Farith_Big.add mw Farith_Big.one in
+ let emin =
+ Farith_Big.sub
+ (Farith_Big.sub (Farith_Big.succ_double Farith_Big.one) emax) prec
+ in
+ (fun x ->
+ let (p, ex) = split_bits mw ew x in
+ let (sx, mx) = p in
+ if Farith_Big.eq ex Farith_Big.zero
+ then (Farith_Big.z_case
+ (fun _ -> F754_zero sx)
+ (fun px -> F754_finite (sx, px, emin))
+ (fun _ -> F754_nan (false, Farith_Big.one))
+ mx)
+ else if Farith_Big.eq ex
+ (Farith_Big.sub (Z.pow (Farith_Big.double Farith_Big.one) ew)
+ Farith_Big.one)
+ then (Farith_Big.z_case
+ (fun _ -> F754_infinity sx)
+ (fun plx -> F754_nan (sx, plx))
+ (fun _ -> F754_nan (false, Farith_Big.one))
+ mx)
+ else (Farith_Big.z_case
+ (fun _ -> F754_nan (false, Farith_Big.one))
+ (fun px -> F754_finite (sx, px,
+ (Farith_Big.sub (Farith_Big.add ex emin) Farith_Big.one)))
+ (fun _ -> F754_nan (false,
+ Farith_Big.one))
+ (Farith_Big.add mx
+ (Z.pow (Farith_Big.double Farith_Big.one) mw))))
+
+(** val binary_float_of_bits :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ binary_float **)
+
+let binary_float_of_bits mw ew x =
+ let emax =
+ Z.pow (Farith_Big.double Farith_Big.one)
+ (Farith_Big.sub ew Farith_Big.one)
+ in
+ let prec = Farith_Big.add mw Farith_Big.one in
+ coq_FF2B prec emax (binary_float_of_bits_aux mw ew x)
diff --git a/farith2/Bits.mli b/farith2/Bits.mli
new file mode 100644
index 0000000000000000000000000000000000000000..7fa47fa2f41e77fc088b4109978c45e8552ab7b2
--- /dev/null
+++ b/farith2/Bits.mli
@@ -0,0 +1,21 @@
+open BinInt
+open Binary
+
+val join_bits :
+ Farith_Big.big_int -> Farith_Big.big_int -> bool -> Farith_Big.big_int ->
+ Farith_Big.big_int -> Farith_Big.big_int
+
+val split_bits :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ (bool * Farith_Big.big_int) * Farith_Big.big_int
+
+val bits_of_binary_float :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float ->
+ Farith_Big.big_int
+
+val binary_float_of_bits_aux :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> full_float
+
+val binary_float_of_bits :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ binary_float
diff --git a/farith2/Bool.ml b/farith2/Bool.ml
new file mode 100644
index 0000000000000000000000000000000000000000..15e4eb09a33e0029bd22c6d0a3306dde660ca896
--- /dev/null
+++ b/farith2/Bool.ml
@@ -0,0 +1,5 @@
+
+(** val eqb : bool -> bool -> bool **)
+
+let eqb b1 b2 =
+ if b1 then b2 else if b2 then false else true
diff --git a/farith2/Bool.mli b/farith2/Bool.mli
new file mode 100644
index 0000000000000000000000000000000000000000..2af28bedbbb20beba8789d1d04cc40b9586bcc67
--- /dev/null
+++ b/farith2/Bool.mli
@@ -0,0 +1,2 @@
+
+val eqb : bool -> bool -> bool
diff --git a/farith2/Datatypes.ml b/farith2/Datatypes.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d5c929229ea2573390a9d676a61a8985e4d0d4a1
--- /dev/null
+++ b/farith2/Datatypes.ml
@@ -0,0 +1,17 @@
+
+(** val xorb : bool -> bool -> bool **)
+
+let xorb b1 b2 =
+ if b1 then if b2 then false else true else b2
+
+type comparison =
+| Eq
+| Lt
+| Gt
+
+(** val coq_CompOpp : comparison -> comparison **)
+
+let coq_CompOpp = function
+| Eq -> Eq
+| Lt -> Gt
+| Gt -> Lt
diff --git a/farith2/Datatypes.mli b/farith2/Datatypes.mli
new file mode 100644
index 0000000000000000000000000000000000000000..32ae552786ef1a1097214521ec43849167e8491c
--- /dev/null
+++ b/farith2/Datatypes.mli
@@ -0,0 +1,9 @@
+
+val xorb : bool -> bool -> bool
+
+type comparison =
+| Eq
+| Lt
+| Gt
+
+val coq_CompOpp : comparison -> comparison
diff --git a/farith2/Interval.ml b/farith2/Interval.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f02e05cb3652f931bfb23055c7270e85ec0ca167
--- /dev/null
+++ b/farith2/Interval.ml
@@ -0,0 +1,162 @@
+open BinarySingleNaN
+open Utils
+
+type float = binary_float
+
+type coq_Interval' =
+| Inan
+| Intv of float * float * bool
+
+type coq_Interval = coq_Interval'
+
+type coq_Interval_opt = coq_Interval' option
+
+(** val inter' :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval' ->
+ coq_Interval' -> coq_Interval' option **)
+
+let inter' prec emax i1 i2 =
+ match i1 with
+ | Inan ->
+ (match i2 with
+ | Inan -> Some Inan
+ | Intv (_, _, nan) -> if nan then Some Inan else None)
+ | Intv (lo1, hi1, nan1) ->
+ (match i2 with
+ | Inan -> if nan1 then Some Inan else None
+ | Intv (lo2, hi2, nan2) ->
+ if (||) (coq_Bltb prec emax hi1 lo2) (coq_Bltb prec emax hi2 lo1)
+ then if (&&) nan1 nan2 then Some Inan else None
+ else Some (Intv ((coq_Bmax prec emax lo1 lo2),
+ (coq_Bmin prec emax hi1 hi2), ((&&) nan1 nan2))))
+
+(** val inter :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval
+ -> coq_Interval_opt **)
+
+let inter =
+ inter'
+
+(** val coq_Iadd' :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ coq_Interval' -> coq_Interval' -> coq_Interval' **)
+
+let coq_Iadd' prec emax m i1 i2 =
+ match i1 with
+ | Inan -> Inan
+ | Intv (l, h, n) ->
+ (match i2 with
+ | Inan -> Inan
+ | Intv (l', h', n') ->
+ let sum1 = coq_Bplus prec emax m l l' in
+ let sum2 = coq_Bplus prec emax m h h' in
+ if is_nan prec emax sum1
+ then if is_nan prec emax sum2
+ then Inan
+ else Intv ((B754_infinity false), (B754_infinity false), true)
+ else if is_nan prec emax sum2
+ then Intv ((B754_infinity true), (B754_infinity true), true)
+ else Intv (sum1, sum2,
+ ((||)
+ ((||) ((||) n n')
+ ((&&) (coq_Beqb prec emax h (B754_infinity false))
+ (coq_Beqb prec emax l' (B754_infinity true))))
+ ((&&) (coq_Beqb prec emax h' (B754_infinity false))
+ (coq_Beqb prec emax l (B754_infinity true))))))
+
+(** val coq_Iadd :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ coq_Interval -> coq_Interval -> coq_Interval **)
+
+let coq_Iadd =
+ coq_Iadd'
+
+(** val coq_Ile :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval ->
+ coq_Interval_opt **)
+
+let coq_Ile _ _ = function
+| Inan -> None
+| Intv (_, b, n) -> Some (Intv ((B754_infinity true), b, n))
+
+(** val coq_Ilt :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval ->
+ coq_Interval_opt **)
+
+let coq_Ilt _ _ = function
+| Inan -> None
+| Intv (_, b, n) -> Some (Intv ((B754_infinity true), b, n))
+
+(** val coq_Ige :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval ->
+ coq_Interval_opt **)
+
+let coq_Ige _ _ = function
+| Inan -> None
+| Intv (a, _, n) -> Some (Intv (a, (B754_infinity false), n))
+
+(** val coq_Igt :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval ->
+ coq_Interval_opt **)
+
+let coq_Igt _ _ = function
+| Inan -> None
+| Intv (a, _, n) -> Some (Intv (a, (B754_infinity false), n))
+
+(** val inter_opt :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval_opt ->
+ coq_Interval_opt -> coq_Interval_opt **)
+
+let inter_opt prec emax i1 i2 =
+ match i1 with
+ | Some i3 -> (match i2 with
+ | Some i4 -> inter prec emax i3 i4
+ | None -> None)
+ | None -> None
+
+(** val to_opt :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval ->
+ coq_Interval_opt **)
+
+let to_opt _ _ i =
+ Some i
+
+(** val coq_Ige_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval
+ -> coq_Interval_opt * coq_Interval_opt **)
+
+let coq_Ige_inv prec emax i1 i2 =
+ ((inter_opt prec emax (coq_Ige prec emax i2) (to_opt prec emax i1)),
+ (inter_opt prec emax (coq_Ile prec emax i1) (to_opt prec emax i2)))
+
+(** val coq_Igt_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval
+ -> coq_Interval_opt * coq_Interval_opt **)
+
+let coq_Igt_inv prec emax i1 i2 =
+ ((inter_opt prec emax (coq_Igt prec emax i2) (to_opt prec emax i1)),
+ (inter_opt prec emax (coq_Ilt prec emax i1) (to_opt prec emax i2)))
+
+(** val coq_Ilt_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval
+ -> coq_Interval_opt * coq_Interval_opt **)
+
+let coq_Ilt_inv prec emax i1 i2 =
+ ((inter_opt prec emax (coq_Ilt prec emax i2) (to_opt prec emax i1)),
+ (inter_opt prec emax (coq_Igt prec emax i1) (to_opt prec emax i2)))
+
+(** val coq_Ile_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval
+ -> coq_Interval_opt * coq_Interval_opt **)
+
+let coq_Ile_inv prec emax i1 i2 =
+ ((inter_opt prec emax (coq_Ile prec emax i2) (to_opt prec emax i1)),
+ (inter_opt prec emax (coq_Ige prec emax i1) (to_opt prec emax i2)))
+
+(** val coq_Ieq_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval
+ -> coq_Interval_opt * coq_Interval_opt **)
+
+let coq_Ieq_inv prec emax i1 i2 =
+ ((inter_opt prec emax (to_opt prec emax i1) (to_opt prec emax i2)),
+ (inter_opt prec emax (to_opt prec emax i1) (to_opt prec emax i2)))
diff --git a/farith2/Interval.mli b/farith2/Interval.mli
new file mode 100644
index 0000000000000000000000000000000000000000..19d9d78dcd85b7d1721b25081fe53bcd735900de
--- /dev/null
+++ b/farith2/Interval.mli
@@ -0,0 +1,67 @@
+open BinarySingleNaN
+open Utils
+
+type float = binary_float
+
+type coq_Interval' =
+| Inan
+| Intv of float * float * bool
+
+type coq_Interval = coq_Interval'
+
+type coq_Interval_opt = coq_Interval' option
+
+val inter' :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval' -> coq_Interval'
+ -> coq_Interval' option
+
+val inter :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval ->
+ coq_Interval_opt
+
+val coq_Iadd' :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ coq_Interval' -> coq_Interval' -> coq_Interval'
+
+val coq_Iadd :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> coq_Interval
+ -> coq_Interval -> coq_Interval
+
+val coq_Ile :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval_opt
+
+val coq_Ilt :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval_opt
+
+val coq_Ige :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval_opt
+
+val coq_Igt :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval_opt
+
+val inter_opt :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval_opt ->
+ coq_Interval_opt -> coq_Interval_opt
+
+val to_opt :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval_opt
+
+val coq_Ige_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval ->
+ coq_Interval_opt * coq_Interval_opt
+
+val coq_Igt_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval ->
+ coq_Interval_opt * coq_Interval_opt
+
+val coq_Ilt_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval ->
+ coq_Interval_opt * coq_Interval_opt
+
+val coq_Ile_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval ->
+ coq_Interval_opt * coq_Interval_opt
+
+val coq_Ieq_inv :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval ->
+ coq_Interval_opt * coq_Interval_opt
diff --git a/farith2/Intv32.ml b/farith2/Intv32.ml
new file mode 100644
index 0000000000000000000000000000000000000000..26467f98fcc8c8dfca5a11c7db1d70d075906abe
--- /dev/null
+++ b/farith2/Intv32.ml
@@ -0,0 +1,112 @@
+open BinarySingleNaN
+open Interval
+
+module Intv32 =
+ struct
+ (** val prec : Farith_Big.big_int **)
+
+ let prec =
+ (Farith_Big.double (Farith_Big.double (Farith_Big.double
+ (Farith_Big.succ_double Farith_Big.one))))
+
+ (** val emax : Farith_Big.big_int **)
+
+ let emax =
+ (Farith_Big.double (Farith_Big.double (Farith_Big.double
+ (Farith_Big.double (Farith_Big.double (Farith_Big.double
+ (Farith_Big.double Farith_Big.one)))))))
+
+ type float32 = B32.B32.t
+
+ type t = coq_Interval
+
+ type t_opt = coq_Interval_opt
+
+ (** val inter : t -> t -> t_opt **)
+
+ let inter x y =
+ inter prec emax x y
+
+ (** val add : Farith_Big.mode -> t -> t -> t **)
+
+ let add =
+ coq_Iadd prec emax
+
+ (** val top : t **)
+
+ let top =
+ Intv ((B754_infinity true), (B754_infinity false), true)
+
+ (** val bot : t_opt **)
+
+ let bot =
+ None
+
+ (** val is_singleton : t -> float32 option **)
+
+ let is_singleton = function
+ | Inan -> Some B754_nan
+ | Intv (a, b, n) ->
+ if (&&)
+ ((&&) (coq_Beqb prec emax a b)
+ (Pervasives.not (coq_Beqb prec emax a (B754_zero false))))
+ (Pervasives.not n)
+ then Some a
+ else None
+
+ (** val s0 : coq_Interval **)
+
+ let s0 =
+ Intv ((B754_zero false), (B754_zero true), false)
+
+ (** val singleton : float32 -> t **)
+
+ let singleton x = match x with
+ | B754_nan -> Inan
+ | _ -> Intv (x, x, false)
+
+ (** val ge : t -> t_opt **)
+
+ let ge =
+ coq_Ige prec emax
+
+ (** val le : t -> t_opt **)
+
+ let le =
+ coq_Ile prec emax
+
+ (** val lt : t -> t_opt **)
+
+ let lt =
+ coq_Ilt prec emax
+
+ (** val gt : t -> t_opt **)
+
+ let gt =
+ coq_Igt prec emax
+
+ (** val le_inv : t -> t -> t_opt * t_opt **)
+
+ let le_inv =
+ coq_Ile_inv prec emax
+
+ (** val ge_inv : t -> t -> t_opt * t_opt **)
+
+ let ge_inv =
+ coq_Ige_inv prec emax
+
+ (** val lt_inv : t -> t -> t_opt * t_opt **)
+
+ let lt_inv =
+ coq_Ilt_inv prec emax
+
+ (** val gt_inv : t -> t -> t_opt * t_opt **)
+
+ let gt_inv =
+ coq_Igt_inv prec emax
+
+ (** val eq_inv : t -> t -> t_opt * t_opt **)
+
+ let eq_inv =
+ coq_Ieq_inv prec emax
+ end
diff --git a/farith2/Intv32.mli b/farith2/Intv32.mli
new file mode 100644
index 0000000000000000000000000000000000000000..21914091a50561ac6f9139d062d6fe1a868f46d1
--- /dev/null
+++ b/farith2/Intv32.mli
@@ -0,0 +1,47 @@
+open BinarySingleNaN
+open Interval
+
+module Intv32 :
+ sig
+ val prec : Farith_Big.big_int
+
+ val emax : Farith_Big.big_int
+
+ type float32 = B32.B32.t
+
+ type t = coq_Interval
+
+ type t_opt = coq_Interval_opt
+
+ val inter : t -> t -> t_opt
+
+ val add : Farith_Big.mode -> t -> t -> t
+
+ val top : t
+
+ val bot : t_opt
+
+ val is_singleton : t -> float32 option
+
+ val s0 : coq_Interval
+
+ val singleton : float32 -> t
+
+ val ge : t -> t_opt
+
+ val le : t -> t_opt
+
+ val lt : t -> t_opt
+
+ val gt : t -> t_opt
+
+ val le_inv : t -> t -> t_opt * t_opt
+
+ val ge_inv : t -> t -> t_opt * t_opt
+
+ val lt_inv : t -> t -> t_opt * t_opt
+
+ val gt_inv : t -> t -> t_opt * t_opt
+
+ val eq_inv : t -> t -> t_opt * t_opt
+ end
diff --git a/farith2/Makefile b/farith2/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..a0ebd3b0eaa0108839a40817e86c469ef534f436
--- /dev/null
+++ b/farith2/Makefile
@@ -0,0 +1,13 @@
+include CoqMakefile
+
+CoqMakefile:
+ @ coq_makefile -f _CoqProject -o CoqMakefile
+
+.PHONY: cleandoc doc
+
+cleandoc:
+ @ rm -rf doc/
+
+doc:
+ @ mkdir -p doc
+ @ cd thry && coq2html -base F -d ../doc *.v *.glob
\ No newline at end of file
diff --git a/farith2/Qextended.ml b/farith2/Qextended.ml
new file mode 100644
index 0000000000000000000000000000000000000000..139597f9cb07c5d48bed18984ec4747f4b4f3438
--- /dev/null
+++ b/farith2/Qextended.ml
@@ -0,0 +1,2 @@
+
+
diff --git a/farith2/Qextended.mli b/farith2/Qextended.mli
new file mode 100644
index 0000000000000000000000000000000000000000..139597f9cb07c5d48bed18984ec4747f4b4f3438
--- /dev/null
+++ b/farith2/Qextended.mli
@@ -0,0 +1,2 @@
+
+
diff --git a/farith2/Readme.md b/farith2/Readme.md
new file mode 100644
index 0000000000000000000000000000000000000000..602106b02f647cf8e9dbacfc7cca80456b99c8eb
--- /dev/null
+++ b/farith2/Readme.md
@@ -0,0 +1,18 @@
+# Farith2
+
+Farith2 is an *under construction* Coq module formalizing floating points abstract domains based on [Flocq](http://flocq.gforge.inria.fr/).
+
+## Structure
+
+The structure of the sources may vary a lot over time. For now the structure is as follows :
+
++ the folder `thry` contains all Coq modules
++ the folder `farith_big` contains OCaml modules used to provide a compatibility layer with Zarith for efficient extraction
++ the `extract.v` file drives the extraction to OCaml
++ the root contains `.ml(i)` files generated by extraction
+
+## Compilation
+
+The compilation of the Coq sources is handled with CoqMakefile. To compile everything, simply type `make` at Farith2's root.
+
+To generate the documentation, it is first required to build the sources using `make` and then `make doc` should fill the `doc` folder with the html documentation formatted using [coq2html](https://github.com/xavierleroy/coq2html).
\ No newline at end of file
diff --git a/farith2/Round.ml b/farith2/Round.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f6c4da1bd14072a85f5b3ef326d99257f841c0cf
--- /dev/null
+++ b/farith2/Round.ml
@@ -0,0 +1,28 @@
+open Datatypes
+open SpecFloat
+
+(** val cond_incr : bool -> Farith_Big.big_int -> Farith_Big.big_int **)
+
+let cond_incr b m =
+ if b then Farith_Big.add m Farith_Big.one else m
+
+(** val round_sign_DN : bool -> location -> bool **)
+
+let round_sign_DN s = function
+| Coq_loc_Exact -> false
+| Coq_loc_Inexact _ -> s
+
+(** val round_sign_UP : bool -> location -> bool **)
+
+let round_sign_UP s = function
+| Coq_loc_Exact -> false
+| Coq_loc_Inexact _ -> Pervasives.not s
+
+(** val round_N : bool -> location -> bool **)
+
+let round_N p = function
+| Coq_loc_Exact -> false
+| Coq_loc_Inexact c -> (match c with
+ | Eq -> p
+ | Lt -> false
+ | Gt -> true)
diff --git a/farith2/Round.mli b/farith2/Round.mli
new file mode 100644
index 0000000000000000000000000000000000000000..db97e992a08fb191f1a5a8117f0eec6d956df8ae
--- /dev/null
+++ b/farith2/Round.mli
@@ -0,0 +1,10 @@
+open Datatypes
+open SpecFloat
+
+val cond_incr : bool -> Farith_Big.big_int -> Farith_Big.big_int
+
+val round_sign_DN : bool -> location -> bool
+
+val round_sign_UP : bool -> location -> bool
+
+val round_N : bool -> location -> bool
diff --git a/farith2/SpecFloat.ml b/farith2/SpecFloat.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7c315960cd7f3b2d8a1633fd4e90622501fa08fa
--- /dev/null
+++ b/farith2/SpecFloat.ml
@@ -0,0 +1,290 @@
+open BinInt
+open Datatypes
+open Zpower
+
+type spec_float =
+| S754_zero of bool
+| S754_infinity of bool
+| S754_nan
+| S754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
+
+(** val emin :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
+
+let emin prec emax =
+ Farith_Big.sub
+ (Farith_Big.sub (Farith_Big.succ_double Farith_Big.one) emax) prec
+
+(** val fexp :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int **)
+
+let fexp prec emax e =
+ Farith_Big.max (Farith_Big.sub e prec) (emin prec emax)
+
+(** val digits2_pos : Farith_Big.big_int -> Farith_Big.big_int **)
+
+let rec digits2_pos n =
+ Farith_Big.positive_case
+ (fun p -> Farith_Big.succ (digits2_pos p))
+ (fun p -> Farith_Big.succ (digits2_pos p))
+ (fun _ -> Farith_Big.one)
+ n
+
+(** val coq_Zdigits2 : Farith_Big.big_int -> Farith_Big.big_int **)
+
+let coq_Zdigits2 n =
+ Farith_Big.z_case
+ (fun _ -> n)
+ (fun p -> (digits2_pos p))
+ (fun p -> (digits2_pos p))
+ n
+
+(** val iter_pos : ('a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1 **)
+
+let rec iter_pos f n x =
+ Farith_Big.positive_case
+ (fun n' -> iter_pos f n' (iter_pos f n' (f x)))
+ (fun n' -> iter_pos f n' (iter_pos f n' x))
+ (fun _ -> f x)
+ n
+
+type location =
+| Coq_loc_Exact
+| Coq_loc_Inexact of comparison
+
+type shr_record = { shr_m : Farith_Big.big_int; shr_r : bool; shr_s : bool }
+
+(** val shr_1 : shr_record -> shr_record **)
+
+let shr_1 mrs =
+ let { shr_m = m; shr_r = r; shr_s = s } = mrs in
+ let s0 = (||) r s in
+ (Farith_Big.z_case
+ (fun _ -> { shr_m = Farith_Big.zero; shr_r = false; shr_s =
+ s0 })
+ (fun p0 ->
+ Farith_Big.positive_case
+ (fun p -> { shr_m = p; shr_r = true; shr_s = s0 })
+ (fun p -> { shr_m = p; shr_r = false; shr_s = s0 })
+ (fun _ -> { shr_m = Farith_Big.zero; shr_r = true; shr_s = s0 })
+ p0)
+ (fun p0 ->
+ Farith_Big.positive_case
+ (fun p -> { shr_m = (Farith_Big.opp p); shr_r = true; shr_s =
+ s0 })
+ (fun p -> { shr_m = (Farith_Big.opp p); shr_r = false; shr_s =
+ s0 })
+ (fun _ -> { shr_m = Farith_Big.zero; shr_r = true; shr_s = s0 })
+ p0)
+ m)
+
+(** val loc_of_shr_record : shr_record -> location **)
+
+let loc_of_shr_record mrs =
+ let { shr_m = _; shr_r = shr_r0; shr_s = shr_s0 } = mrs in
+ if shr_r0
+ then if shr_s0 then Coq_loc_Inexact Gt else Coq_loc_Inexact Eq
+ else if shr_s0 then Coq_loc_Inexact Lt else Coq_loc_Exact
+
+(** val shr_record_of_loc : Farith_Big.big_int -> location -> shr_record **)
+
+let shr_record_of_loc m = function
+| Coq_loc_Exact -> { shr_m = m; shr_r = false; shr_s = false }
+| Coq_loc_Inexact c ->
+ (match c with
+ | Eq -> { shr_m = m; shr_r = true; shr_s = false }
+ | Lt -> { shr_m = m; shr_r = false; shr_s = true }
+ | Gt -> { shr_m = m; shr_r = true; shr_s = true })
+
+(** val shr :
+ shr_record -> Farith_Big.big_int -> Farith_Big.big_int ->
+ shr_record * Farith_Big.big_int **)
+
+let shr mrs e n =
+ Farith_Big.z_case
+ (fun _ -> (mrs, e))
+ (fun p -> ((iter_pos shr_1 p mrs), (Farith_Big.add e n)))
+ (fun _ -> (mrs, e))
+ n
+
+(** val shr_fexp :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int -> location -> shr_record * Farith_Big.big_int **)
+
+let shr_fexp prec emax m e l =
+ shr (shr_record_of_loc m l) e
+ (Farith_Big.sub (fexp prec emax (Farith_Big.add (coq_Zdigits2 m) e)) e)
+
+(** val shl_align :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int * Farith_Big.big_int **)
+
+let shl_align mx ex ex' =
+ Farith_Big.z_case
+ (fun _ -> (mx, ex))
+ (fun _ -> (mx, ex))
+ (fun d -> ((shift_pos d mx), ex'))
+ (Farith_Big.sub ex' ex)
+
+(** val coq_SFcompare : spec_float -> spec_float -> comparison option **)
+
+let coq_SFcompare f1 f2 =
+ match f1 with
+ | S754_zero _ ->
+ (match f2 with
+ | S754_zero _ -> Some Eq
+ | S754_infinity s -> Some (if s then Gt else Lt)
+ | S754_nan -> None
+ | S754_finite (s, _, _) -> Some (if s then Gt else Lt))
+ | S754_infinity s ->
+ (match f2 with
+ | S754_infinity s0 ->
+ Some (if s then if s0 then Eq else Lt else if s0 then Gt else Eq)
+ | S754_nan -> None
+ | _ -> Some (if s then Lt else Gt))
+ | S754_nan -> None
+ | S754_finite (s1, m1, e1) ->
+ (match f2 with
+ | S754_zero _ -> Some (if s1 then Lt else Gt)
+ | S754_infinity s -> Some (if s then Gt else Lt)
+ | S754_nan -> None
+ | S754_finite (s2, m2, e2) ->
+ Some
+ (if s1
+ then if s2
+ then (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with
+ | Eq ->
+ coq_CompOpp
+ ((fun c x y -> Farith_Big.compare_case c Lt Gt x y)
+ Eq m1 m2)
+ | Lt -> Gt
+ | Gt -> Lt)
+ else Lt
+ else if s2
+ then Gt
+ else (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with
+ | Eq ->
+ (fun c x y -> Farith_Big.compare_case c Lt Gt x y) Eq
+ m1 m2
+ | x -> x)))
+
+(** val coq_SFeqb : spec_float -> spec_float -> bool **)
+
+let coq_SFeqb f1 f2 =
+ match coq_SFcompare f1 f2 with
+ | Some c -> (match c with
+ | Eq -> true
+ | _ -> false)
+ | None -> false
+
+(** val coq_SFltb : spec_float -> spec_float -> bool **)
+
+let coq_SFltb f1 f2 =
+ match coq_SFcompare f1 f2 with
+ | Some c -> (match c with
+ | Lt -> true
+ | _ -> false)
+ | None -> false
+
+(** val coq_SFleb : spec_float -> spec_float -> bool **)
+
+let coq_SFleb f1 f2 =
+ match coq_SFcompare f1 f2 with
+ | Some c -> (match c with
+ | Gt -> false
+ | _ -> true)
+ | None -> false
+
+(** val cond_Zopp : bool -> Farith_Big.big_int -> Farith_Big.big_int **)
+
+let cond_Zopp b m =
+ if b then Farith_Big.opp m else m
+
+(** val new_location_even :
+ Farith_Big.big_int -> Farith_Big.big_int -> location **)
+
+let new_location_even nb_steps k =
+ if Farith_Big.eq k Farith_Big.zero
+ then Coq_loc_Exact
+ else Coq_loc_Inexact
+ ((Farith_Big.compare_case Eq Lt Gt)
+ (Farith_Big.mult (Farith_Big.double Farith_Big.one) k) nb_steps)
+
+(** val new_location_odd :
+ Farith_Big.big_int -> Farith_Big.big_int -> location **)
+
+let new_location_odd nb_steps k =
+ if Farith_Big.eq k Farith_Big.zero
+ then Coq_loc_Exact
+ else Coq_loc_Inexact
+ (match (Farith_Big.compare_case Eq Lt Gt)
+ (Farith_Big.add
+ (Farith_Big.mult (Farith_Big.double Farith_Big.one) k)
+ Farith_Big.one) nb_steps with
+ | Eq -> Lt
+ | x -> x)
+
+(** val new_location :
+ Farith_Big.big_int -> Farith_Big.big_int -> location **)
+
+let new_location nb_steps =
+ if Z.even nb_steps
+ then new_location_even nb_steps
+ else new_location_odd nb_steps
+
+(** val coq_SFdiv_core_binary :
+ Farith_Big.big_int -> Farith_Big.big_int -> 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 **)
+
+let coq_SFdiv_core_binary prec emax m1 e1 m2 e2 =
+ let d1 = coq_Zdigits2 m1 in
+ let d2 = coq_Zdigits2 m2 in
+ let e' =
+ Farith_Big.min
+ (fexp prec emax
+ (Farith_Big.sub (Farith_Big.add d1 e1) (Farith_Big.add d2 e2)))
+ (Farith_Big.sub e1 e2)
+ in
+ let s = Farith_Big.sub (Farith_Big.sub e1 e2) e' in
+ let m' =
+ Farith_Big.z_case
+ (fun _ -> m1)
+ (fun _ -> Farith_Big.shiftl m1 s)
+ (fun _ -> Farith_Big.zero)
+ s
+ in
+ let (q, r) = Farith_Big.div_mod_floor m' m2 in
+ ((q, e'), (new_location m2 r))
+
+(** val coq_SFsqrt_core_binary :
+ 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 **)
+
+let coq_SFsqrt_core_binary prec emax m e =
+ let d = coq_Zdigits2 m in
+ let e' =
+ Farith_Big.min
+ (fexp prec emax
+ (Farith_Big.div2_floor
+ (Farith_Big.add (Farith_Big.add d e) Farith_Big.one)))
+ (Farith_Big.div2_floor e)
+ in
+ let s =
+ Farith_Big.sub e (Farith_Big.mult (Farith_Big.double Farith_Big.one) e')
+ in
+ let m' =
+ Farith_Big.z_case
+ (fun _ -> m)
+ (fun _ -> Farith_Big.shiftl m s)
+ (fun _ -> Farith_Big.zero)
+ s
+ in
+ let (q, r) = Farith_Big.Z.sqrt_rem m' in
+ let l =
+ if Farith_Big.eq r Farith_Big.zero
+ then Coq_loc_Exact
+ else Coq_loc_Inexact (if Farith_Big.le r q then Lt else Gt)
+ in
+ ((q, e'), l)
diff --git a/farith2/SpecFloat.mli b/farith2/SpecFloat.mli
new file mode 100644
index 0000000000000000000000000000000000000000..0523a53f16cbcff61a123e4627e21b58c9d3ef2c
--- /dev/null
+++ b/farith2/SpecFloat.mli
@@ -0,0 +1,70 @@
+open BinInt
+open Datatypes
+open Zpower
+
+type spec_float =
+| S754_zero of bool
+| S754_infinity of bool
+| S754_nan
+| S754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
+
+val emin : Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
+
+val fexp :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int
+
+val digits2_pos : Farith_Big.big_int -> Farith_Big.big_int
+
+val coq_Zdigits2 : Farith_Big.big_int -> Farith_Big.big_int
+
+val iter_pos : ('a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1
+
+type location =
+| Coq_loc_Exact
+| Coq_loc_Inexact of comparison
+
+type shr_record = { shr_m : Farith_Big.big_int; shr_r : bool; shr_s : bool }
+
+val shr_1 : shr_record -> shr_record
+
+val loc_of_shr_record : shr_record -> location
+
+val shr_record_of_loc : Farith_Big.big_int -> location -> shr_record
+
+val shr :
+ shr_record -> Farith_Big.big_int -> Farith_Big.big_int ->
+ shr_record * Farith_Big.big_int
+
+val shr_fexp :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int -> location -> shr_record * Farith_Big.big_int
+
+val shl_align :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ Farith_Big.big_int * Farith_Big.big_int
+
+val coq_SFcompare : spec_float -> spec_float -> comparison option
+
+val coq_SFeqb : spec_float -> spec_float -> bool
+
+val coq_SFltb : spec_float -> spec_float -> bool
+
+val coq_SFleb : spec_float -> spec_float -> bool
+
+val cond_Zopp : bool -> Farith_Big.big_int -> Farith_Big.big_int
+
+val new_location_even : Farith_Big.big_int -> Farith_Big.big_int -> location
+
+val new_location_odd : Farith_Big.big_int -> Farith_Big.big_int -> location
+
+val new_location : Farith_Big.big_int -> Farith_Big.big_int -> location
+
+val coq_SFdiv_core_binary :
+ Farith_Big.big_int -> Farith_Big.big_int -> 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_SFsqrt_core_binary :
+ 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
diff --git a/farith2/Specif.ml b/farith2/Specif.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c756f547f6bed7dabf5cd7d81e664b8d4dbe9e70
--- /dev/null
+++ b/farith2/Specif.ml
@@ -0,0 +1,3 @@
+
+type 'a coq_sig = 'a
+ (* singleton inductive, whose constructor was exist *)
diff --git a/farith2/Specif.mli b/farith2/Specif.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c756f547f6bed7dabf5cd7d81e664b8d4dbe9e70
--- /dev/null
+++ b/farith2/Specif.mli
@@ -0,0 +1,3 @@
+
+type 'a coq_sig = 'a
+ (* singleton inductive, whose constructor was exist *)
diff --git a/farith2/Utils.ml b/farith2/Utils.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ff1c2c78ec2d4d47eab07021d6b26b42d84198ec
--- /dev/null
+++ b/farith2/Utils.ml
@@ -0,0 +1,19 @@
+open BinarySingleNaN
+
+type float = binary_float
+
+(** val coq_Bmax :
+ Farith_Big.big_int -> Farith_Big.big_int -> float -> float -> float **)
+
+let coq_Bmax prec emax f1 f2 =
+ if (||) (is_nan prec emax f1) (is_nan prec emax f2)
+ then B754_nan
+ else if coq_Bleb prec emax f1 f2 then f2 else f1
+
+(** val coq_Bmin :
+ Farith_Big.big_int -> Farith_Big.big_int -> float -> float -> float **)
+
+let coq_Bmin prec emax f1 f2 =
+ if (||) (is_nan prec emax f1) (is_nan prec emax f2)
+ then B754_nan
+ else if coq_Bleb prec emax f1 f2 then f1 else f2
diff --git a/farith2/Utils.mli b/farith2/Utils.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5eb5b65c88744551c30b0850b19ea251cfc6cb2f
--- /dev/null
+++ b/farith2/Utils.mli
@@ -0,0 +1,9 @@
+open BinarySingleNaN
+
+type float = binary_float
+
+val coq_Bmax :
+ Farith_Big.big_int -> Farith_Big.big_int -> float -> float -> float
+
+val coq_Bmin :
+ Farith_Big.big_int -> Farith_Big.big_int -> float -> float -> float
diff --git a/farith2/Zaux.ml b/farith2/Zaux.ml
new file mode 100644
index 0000000000000000000000000000000000000000..139597f9cb07c5d48bed18984ec4747f4b4f3438
--- /dev/null
+++ b/farith2/Zaux.ml
@@ -0,0 +1,2 @@
+
+
diff --git a/farith2/Zaux.mli b/farith2/Zaux.mli
new file mode 100644
index 0000000000000000000000000000000000000000..139597f9cb07c5d48bed18984ec4747f4b4f3438
--- /dev/null
+++ b/farith2/Zaux.mli
@@ -0,0 +1,2 @@
+
+
diff --git a/farith2/Zbool.ml b/farith2/Zbool.ml
new file mode 100644
index 0000000000000000000000000000000000000000..139597f9cb07c5d48bed18984ec4747f4b4f3438
--- /dev/null
+++ b/farith2/Zbool.ml
@@ -0,0 +1,2 @@
+
+
diff --git a/farith2/Zbool.mli b/farith2/Zbool.mli
new file mode 100644
index 0000000000000000000000000000000000000000..139597f9cb07c5d48bed18984ec4747f4b4f3438
--- /dev/null
+++ b/farith2/Zbool.mli
@@ -0,0 +1,2 @@
+
+
diff --git a/farith2/Zpower.ml b/farith2/Zpower.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d7ddaef5cd096dac49935b076f994f6738fe1b08
--- /dev/null
+++ b/farith2/Zpower.ml
@@ -0,0 +1,7 @@
+open BinPos
+
+(** val shift_pos :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
+
+let shift_pos n z =
+ Pos.iter (fun x -> Farith_Big.double x) z n
diff --git a/farith2/Zpower.mli b/farith2/Zpower.mli
new file mode 100644
index 0000000000000000000000000000000000000000..0887c39e52a58f7598409c912ba4f51569b0a7b2
--- /dev/null
+++ b/farith2/Zpower.mli
@@ -0,0 +1,4 @@
+open BinPos
+
+val shift_pos :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
diff --git a/farith2/_CoqProject b/farith2/_CoqProject
new file mode 100644
index 0000000000000000000000000000000000000000..e5fa34fb951bd2c04b133eb521811322d7941c65
--- /dev/null
+++ b/farith2/_CoqProject
@@ -0,0 +1,11 @@
+-R ./thry F
+./thry/Interval.v
+./thry/All.v
+./thry/Intv32.v
+./thry/Tactics.v
+./thry/Rextended.v
+./thry/Qextended.v
+./thry/Utils.v
+./thry/B32.v
+./thry/Correction_thms.v
+./extraction.v
\ No newline at end of file
diff --git a/farith2/doc/coq2html.js b/farith2/doc/coq2html.js
new file mode 100644
index 0000000000000000000000000000000000000000..d869b602b1c5c440f89ef0198d6c1130eb2d9c88
--- /dev/null
+++ b/farith2/doc/coq2html.js
@@ -0,0 +1,25 @@
+
+function toggleDisplay(id)
+{
+ var elt = document.getElementById(id);
+ if (elt.style.display == 'none') {
+ elt.style.display = 'block';
+ } else {
+ elt.style.display = 'none';
+ }
+}
+
+function hideAll(cls)
+{
+ var testClass = new RegExp("(^|s)" + cls + "(s|$)");
+ var tag = tag || "*";
+ var elements = document.getElementsByTagName("div");
+ var current;
+ var length = elements.length;
+ for(var i=0; i<length; i++){
+ current = elements[i];
+ if(testClass.test(current.className)) {
+ current.style.display = 'none';
+ }
+ }
+}
diff --git a/farith2/dune b/farith2/dune
new file mode 100644
index 0000000000000000000000000000000000000000..541a416dad12c7b413d290f5b2941b75dba419bc
--- /dev/null
+++ b/farith2/dune
@@ -0,0 +1,7 @@
+(include_subdirs unqualified)
+
+(library
+ (name farith2)
+ (public_name farith2)
+ (libraries zarith)
+ (flags "-w" "-33"))
diff --git a/farith2/dune-project b/farith2/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..ab8113ad5e2aa636170feaa81ad55560556c0649
--- /dev/null
+++ b/farith2/dune-project
@@ -0,0 +1,7 @@
+(lang dune 2.8)
+
+(generate_opam_files true)
+
+(package
+ (name farith2)
+ (synopsis "formaly verified floating-points valuations based on Flocq"))
diff --git a/farith2/extraction.v b/farith2/extraction.v
new file mode 100644
index 0000000000000000000000000000000000000000..3ed0abac6151ba4395328d9857440096a1306336
--- /dev/null
+++ b/farith2/extraction.v
@@ -0,0 +1,273 @@
+From Flocq Require Import Core.Zaux IEEE754.BinarySingleNaN IEEE754.Bits.
+From F Require Import Qextended B32 Intv32.
+From Coq Require Import Extraction Lia Arith.Wf_nat ZArith.
+
+Goal (Beqb (B32.add mode_NE (B32.of_q mode_NE Qx_half) (B32.of_q mode_NE Qx_half)) (B32.of_q mode_NE Qx_one) = true).
+Proof.
+ cbn.
+ reflexivity.
+Qed.
+
+Goal (Beqb (B32.div mode_NE (B32.of_q mode_NE Qx_one) (B32.of_q mode_NE Qx_two)) (B32.of_q mode_NE Qx_half) = true).
+Proof.
+ cbn.
+ reflexivity.
+Qed.
+
+Require Import Sumbool.
+
+Extract Inlined Constant bool_of_sumbool => "Farith_Big.identity".
+Extract Inlined Constant sumbool_of_bool => "Farith_Big.identity".
+
+
+(** From ExtrOcamlNatBigInt of coq archive *)
+
+Require Import Arith Even Div2 EqNat Euclid.
+Require Import ExtrOcamlBasic.
+
+Extract Inlined Constant Datatypes.negb => "Pervasives.not".
+Extract Inlined Constant Datatypes.fst => "Pervasives.fst".
+Extract Inlined Constant Datatypes.snd => "Pervasives.snd".
+
+
+(** NB: The extracted code should be linked with [nums.cm(x)a]
+ from ocaml's stdlib and with the wrapper [big.ml] that
+ simplifies the use of [Big_int] (it can be found in the sources
+ of Coq). *)
+
+(** Disclaimer: trying to obtain efficient certified programs
+ by extracting [nat] into [big_int] isn't necessarily a good idea.
+ See comments in [ExtrOcamlNatInt.v].
+*)
+
+
+(** Mapping of [nat] into [big_int]. The last string corresponds to
+ a [nat_case], see documentation of [Extract Inductive]. *)
+
+Extract Inductive nat => "Farith_Big.big_int" [ "Farith_Big.zero" "Farith_Big.succ" ]
+ "Farith_Big.nat_case".
+
+(** Efficient (but uncertified) versions for usual [nat] functions *)
+
+Extract Inlined Constant plus => "Farith_Big.add".
+Extract Inlined Constant mult => "Farith_Big.mult".
+Extract Constant pred => "fun n -> Farith_Big.max Farith_Big.zero (Farith_Big.pred n)".
+Extract Constant minus => "fun n m -> Farith_Big.max Farith_Big.zero (Farith_Big.sub n m)".
+Extract Inlined Constant max => "Farith_Big.max".
+Extract Inlined Constant min => "Farith_Big.min".
+(*Extract Constant nat_beq => "Farith_Big.eq".*)
+Extract Constant EqNat.beq_nat => "Farith_Big.eq".
+Extract Constant EqNat.eq_nat_decide => "Farith_Big.eq".
+
+Extract Constant Peano_dec.eq_nat_dec => "Farith_Big.eq".
+
+(* Extract Constant Compare_dec.nat_compare =>
+ "Farith_Big.compare_case Eq Lt Gt".
+
+Extract Constant Compare_dec.leb => "Farith_Big.le".
+Extract Constant Compare_dec.le_lt_dec => "Farith_Big.le".
+Extract Constant Compare_dec.lt_eq_lt_dec =>
+ "Farith_Big.compare_case (Some false) (Some true) None". *)
+
+Extract Constant Even.even_odd_dec =>
+ "fun n -> Farith_Big.sign (Farith_Big.mod n Farith_Big.two) = 0".
+Extract Constant Div2.div2 => "fun n -> Farith_Big.div n Farith_Big.two".
+
+Extract Inductive Euclid.diveucl => "(Farith_Big.big_int * Farith_Big.big_int)" [""].
+Extract Constant Euclid.eucl_dev => "fun n m -> Farith_Big.quomod m n".
+Extract Constant Euclid.quotient => "fun n m -> Farith_Big.div m n".
+Extract Constant Euclid.modulo => "fun n m -> Farith_Big.modulo m n".
+
+
+(** From ExtrOcamlZBigInt of coq archive *)
+
+Require Import ZArith NArith.
+Require Import ExtrOcamlBasic.
+
+(** NB: The extracted code should be linked with [nums.cm(x)a]
+ from ocaml's stdlib and with the wrapper [big.ml] that
+ simplifies the use of [Big_int] (it can be found in the sources
+ of Coq). *)
+
+(** Disclaimer: trying to obtain efficient certified programs
+ by extracting [Z] into [big_int] isn't necessarily a good idea.
+ See the Disclaimer in [ExtrOcamlNatInt]. *)
+
+(** Mapping of [positive], [Z], [N] into [big_int]. The last strings
+ emulate the matching, see documentation of [Extract Inductive]. *)
+
+Extract Inductive positive => "Farith_Big.big_int"
+ [ "Farith_Big.succ_double" "Farith_Big.double" "Farith_Big.one" ] "Farith_Big.positive_case".
+
+Extract Inductive Z => "Farith_Big.big_int"
+ [ "Farith_Big.zero" "" "Farith_Big.opp" ] "Farith_Big.z_case".
+
+Extract Inductive N => "Farith_Big.big_int"
+ [ "Farith_Big.zero" "" ] "Farith_Big.n_case".
+
+(** Nota: the "" above is used as an identity function "(fun p->p)" *)
+
+(** Efficient (but uncertified) versions for usual functions *)
+
+Extract Inlined Constant Pos.add => "Farith_Big.add".
+Extract Inlined Constant Pos.succ => "Farith_Big.succ".
+Extract Constant Pos.pred => "fun n -> Farith_Big.max Farith_Big.one (Farith_Big.pred n)".
+Extract Constant Pos.sub => "fun n m -> Farith_Big.max Farith_Big.one (Farith_Big.sub n m)".
+Extract Inlined Constant Pos.pred_double => "Farith_Big.pred_double".
+Extract Inlined Constant Pos.mul => "Farith_Big.mult".
+Extract Inlined Constant Pos.min => "Farith_Big.min".
+Extract Inlined Constant Pos.max => "Farith_Big.max".
+Extract Inlined Constant Pos.compare => "(Farith_Big.compare_case Eq Lt Gt)".
+Extract Constant Pos.compare_cont =>
+ "fun c x y -> Farith_Big.compare_case c Lt Gt x y".
+Extract Inlined Constant Pos.eqb => "Farith_Big.eq".
+Extract Inlined Constant Pos.leb => "Farith_Big.le".
+Extract Inlined Constant Pos.ltb => "Farith_Big.lt".
+Extract Inlined Constant Pos.to_nat => "Farith_Big.identity".
+Extract Inlined Constant Pos.of_nat => "Farith_Big.identity".
+Extract Inlined Constant Pos.of_succ_nat => "Farith_Big.succ".
+Extract Constant Pos.add_carry => "fun p q -> Farith_Big.succ (Farith_Big.add p q)".
+Extract Inlined Constant Pos.sqrt => "Farith_Big.Z.sqrt".
+Extract Inlined Constant Pos.square => "Farith_Big.square".
+Extract Inlined Constant Pos.eq_dec => "Farith_Big.Z.equal".
+Extract Inlined Constant Pos.pow => "Farith_Big.pow_pos".
+Extract Inlined Constant Pos.gcd => "Farith_Big.Z.gcd".
+Extract Inlined Constant Pos.lor => "Farith_Big.Z.logor".
+Extract Inlined Constant Pos.land => "Farith_Big.Z.logand".
+Extract Inlined Constant Pos.lxor => "Farith_Big.Z.logxor".
+Extract Inlined Constant Pos.ldiff => "Farith_Big.ldiff".
+Extract Inlined Constant Pos.shiftl_nat => "Farith_Big.shiftl".
+Extract Inlined Constant Pos.shiftr_nat => "Farith_Big.shiftr".
+Extract Inlined Constant Pos.shiftl => "Farith_Big.shiftl".
+Extract Inlined Constant Pos.shiftr => "Farith_Big.shiftr".
+
+Extract Inlined Constant BinPos.Pos.compare_cont => "(fun c x y -> Farith_Big.compare_case c Lt Gt x y)".
+
+
+Extract Inlined Constant N.add => "Farith_Big.add".
+Extract Inlined Constant N.succ => "Farith_Big.succ".
+Extract Constant N.pred => "fun n -> Farith_Big.max Farith_Big.zero (Farith_Big.pred n)".
+Extract Constant N.sub => "fun n m -> Farith_Big.max Farith_Big.zero (Farith_Big.sub n m)".
+Extract Inlined Constant N.mul => "Farith_Big.mult".
+Extract Inlined Constant N.min => "Farith_Big.min".
+Extract Inlined Constant N.max => "Farith_Big.max".
+Extract Constant N.div =>
+ "fun a b -> if Farith_Big.eq b Farith_Big.zero then Farith_Big.zero else Farith_Big.div a b".
+Extract Constant N.modulo =>
+ "fun a b -> if Farith_Big.eq b Farith_Big.zero then Farith_Big.zero else Farith_Big.modulo a b".
+Extract Constant N.compare => "Farith_Big.compare_case Eq Lt Gt".
+Extract Inlined Constant N.succ_double => "Farith_Big.succ_double".
+Extract Inlined Constant N.double => "Farith_Big.double".
+Extract Inlined Constant Pos.Nsucc_double => "Farith_Big.succ_double".
+Extract Inlined Constant Pos.Ndouble => "Farith_Big.double".
+
+Extract Inlined Constant Z.add => "Farith_Big.add".
+Extract Inlined Constant Z.succ => "Farith_Big.succ".
+Extract Inlined Constant Z.pred => "Farith_Big.pred".
+Extract Inlined Constant Z.sub => "Farith_Big.sub".
+Extract Inlined Constant Z.mul => "Farith_Big.mult".
+Extract Inlined Constant Z.opp => "Farith_Big.opp".
+Extract Inlined Constant Z.abs => "Farith_Big.abs".
+Extract Inlined Constant Z.min => "Farith_Big.min".
+Extract Inlined Constant Z.max => "Farith_Big.max".
+Extract Inlined Constant Z.eqb => "Farith_Big.eq".
+Extract Inlined Constant Z.leb => "Farith_Big.le".
+Extract Inlined Constant Z.ltb => "Farith_Big.lt".
+Extract Inlined Constant Z.geb => "Farith_Big.ge".
+Extract Inlined Constant Z.gtb => "Farith_Big.gt".
+Extract Inlined Constant Z.compare => "(Farith_Big.compare_case Eq Lt Gt)".
+Extract Inlined Constant Z.double => "Farith_Big.double".
+Extract Inlined Constant Z.succ_double => "Farith_Big.succ_double".
+Extract Inlined Constant Z.pred_double => "Farith_Big.pred_double".
+Extract Inlined Constant Z.pos_sub => "Farith_Big.sub".
+Extract Inlined Constant Z.gcd => "Farith_Big.Z.gcd".
+Extract Inlined Constant Z.sqrt => "Farith_Big.Z.sqrt".
+Extract Inlined Constant Z.sqrtrem => "Farith_Big.Z.sqrt_rem".
+Extract Inlined Constant Z.square => "Farith_Big.square".
+Extract Inlined Constant Z.lnot => "Farith_Big.Z.lognot".
+Extract Inlined Constant Z.lor => "Farith_Big.Z.logor".
+Extract Inlined Constant Z.land => "Farith_Big.Z.logand".
+Extract Inlined Constant Z.lxor => "Farith_Big.Z.logxor".
+Extract Inlined Constant Z.ldiff => "Farith_Big.ldiff".
+Extract Inlined Constant Z.eq_dec => "Farith_Big.Z.equal".
+Extract Inlined Constant Z.shiftr => "Farith_Big.shiftr".
+Extract Inlined Constant Z.shiftl => "Farith_Big.shiftl".
+Extract Inlined Constant Z.sgn => "Farith_Big.sgn".
+
+Extract Inlined Constant Z.of_N => "Farith_Big.identity".
+Extract Inlined Constant Z.of_nat => "Farith_Big.identity".
+
+Extract Inlined Constant Z.abs_N => "Farith_Big.abs".
+Extract Inlined Constant Z.abs_nat => "Farith_Big.abs".
+
+Extract Inlined Constant Zeq_bool => "Farith_Big.eq".
+
+(** trunc convention *)
+Extract Inlined Constant Z.rem => "Farith_Big.Z.rem".
+Extract Inlined Constant Z.quot => "Farith_Big.Z.div".
+Extract Inlined Constant Z.quot2 => "Farith_Big.div2_trunc".
+Extract Inlined Constant Z.quotrem => "Farith_Big.Z.div_rem".
+
+(** floor convention *)
+Extract Inlined Constant Z.modulo => "Farith_Big.mod_floor".
+Extract Inlined Constant Z.div => "Farith_Big.div_floor".
+Extract Inlined Constant Z.div_eucl => "Farith_Big.div_mod_floor".
+Extract Inlined Constant Z.div2 => "Farith_Big.div2_floor".
+
+(** euclid convention *)
+Require Import Zeuclid.
+Extract Inlined Constant ZEuclid.modulo => "Farith_Big.Z.erem".
+Extract Inlined Constant ZEuclid.div => "Farith_Big.Z.ediv".
+
+Extract Inlined Constant Z.pow_pos => "Farith_Big.pow_pos".
+
+
+
+Require Import Flocq.Core.Zaux.
+Require Coq.Arith.Wf_nat.
+(* Extract Inlined Constant shiftl_pos => "Farith_Big.shiftl_pos". *)
+Extract Inlined Constant Core.Zaux.iter_nat => "Farith_Big.iter_nat".
+Extract Inlined Constant nat_rect => "Farith_Big.nat_rect".
+
+
+(** Some proofs used in function realization *)
+
+Definition div_mod_floor a b :=
+ let (q,r) := Z.quotrem a b in
+ if orb (Z.lxor (Z.sgn a) (Z.sgn b) >=? 0)%Z (r =? 0)%Z
+ then (q,r)
+ else (Z.pred q,b+r)%Z.
+
+Lemma Floor_of_Trunc:
+ forall a b, (b <> 0)%Z -> Z.div_eucl a b = div_mod_floor a b.
+Proof.
+ intros a' b' Hb.
+ unfold div_mod_floor.
+ assert (Lmod := Z.rem_mod a' b' Hb).
+ assert (Ldiv := Z.quot_div a' b' Hb).
+ replace (Z.quotrem a' b') with ((Z.quot a' b',Z.rem a' b')) by
+ (compute [Z.quot Z.rem]; destruct (Z.quotrem a' b'); trivial).
+ replace (Z.pred (Z.quot a' b'))%Z with (-(Z.opp (Z.quot a' b')+1))%Z by lia.
+ rewrite Lmod. rewrite Ldiv.
+ pose (a := a'). pose (b := b').
+ destruct a'; destruct b'; unfold Z.modulo, Z.div; simpl; trivial;
+ destruct (Z.pos_div_eucl p (Z.pos p0)) as [[|pq|nq] [|pr|nr]]; trivial.
+Qed.
+
+(* Avoid name clashes *)
+Extraction Blacklist Big List String Int Z Q.
+
+Extract Inductive Qextended.Qx => "Q.t" [ "Farith_Big.q_mk" ] "Farith_Big.q_case".
+Extract Inlined Constant Qextended.den => "Farith_Big.q_den".
+Extract Inlined Constant Qextended.num => "Farith_Big.q_num".
+Extract Inlined Constant Qextended.Qx_classify => "Q.classify".
+
+Extract Inductive Qx_kind => "Q.kind" [ "Q.INF" "Q.MINF" "Q.UNDEF" "Q.ZERO" "Q.NZERO" ].
+Extract Inlined Constant Qx_classify => "Q.classify".
+
+Extract Inductive mode => "Farith_Big.mode" [
+ "Farith_Big.NE" "Farith_Big.ZR" "Farith_Big.DN" "Farith_Big.UP" "Farith_Big.NA"
+].
+
+Separate Extraction B32.B32 Intv32.
+
diff --git a/farith2/farith_big/farith_Big.ml b/farith2/farith_big/farith_Big.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8ed2ad80c7f2fe17020e800bee1fabd883aae142
--- /dev/null
+++ b/farith2/farith_big/farith_Big.ml
@@ -0,0 +1,238 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** [Big] : a wrapper around ocaml [Big_int] with nicer names,
+ and a few extraction-specific constructions *)
+
+(** To be linked with [nums.(cma|cmxa)] *)
+
+open Big_int_Z
+
+type big_int = Big_int_Z.big_int
+(* The type of big integers. *)
+let zero = zero_big_int
+(* The big integer [0]. *)
+let one = unit_big_int
+(* The big integer [1]. *)
+let two = big_int_of_int 2
+(* The big integer [2]. *)
+
+(* {6 Arithmetic operations} *)
+
+let opp = minus_big_int
+(* Unary negation. *)
+let abs = abs_big_int
+(* Absolute value. *)
+let add = add_big_int
+(* Addition. *)
+let succ = succ_big_int
+(* Successor (add 1). *)
+let add_int = add_int_big_int
+(* Addition of a small integer to a big integer. *)
+let sub = sub_big_int
+(* Subtraction. *)
+let pred = pred_big_int
+(* Predecessor (subtract 1). *)
+let mult = mult_big_int
+(* Multiplication of two big integers. *)
+let mult_int = mult_int_big_int
+(* Multiplication of a big integer by a small integer *)
+let _square = square_big_int
+(* Return the square of the given big integer *)
+let sqrt = sqrt_big_int
+(* [sqrt_big_int a] returns the integer square root of [a],
+ that is, the largest big integer [r] such that [r * r <= a].
+ Raise [Invalid_argument] if [a] is negative. *)
+let quomod = quomod_big_int
+(* Euclidean division of two big integers.
+ The first part of the result is the quotient,
+ the second part is the remainder.
+ Writing [(q,r) = quomod_big_int a b], we have
+ [a = q * b + r] and [0 <= r < |b|].
+ Raise [Division_by_zero] if the divisor is zero. *)
+let div = div_big_int
+(* Euclidean quotient of two big integers.
+ This is the first result [q] of [quomod_big_int] (see above). *)
+let modulo = mod_big_int
+(* Euclidean modulus of two big integers.
+ This is the second result [r] of [quomod_big_int] (see above). *)
+let gcd = gcd_big_int
+(* Greatest common divisor of two big integers. *)
+let power = power_big_int_positive_big_int
+(* Exponentiation functions. Return the big integer
+ representing the first argument [a] raised to the power [b]
+ (the second argument). Depending
+ on the function, [a] and [b] can be either small integers
+ or big integers. Raise [Invalid_argument] if [b] is negative. *)
+
+(* {6 Comparisons and tests} *)
+
+let sign = sign_big_int
+(* Return [0] if the given big integer is zero,
+ [1] if it is positive, and [-1] if it is negative. *)
+let compare = compare_big_int
+(* [compare_big_int a b] returns [0] if [a] and [b] are equal,
+ [1] if [a] is greater than [b], and [-1] if [a] is smaller
+ than [b]. *)
+let eq = eq_big_int
+let le = le_big_int
+let ge = ge_big_int
+let lt = lt_big_int
+let gt = gt_big_int
+(* Usual boolean comparisons between two big integers. *)
+let max = max_big_int
+(* Return the greater of its two arguments. *)
+let min = min_big_int
+(* Return the smaller of its two arguments. *)
+(* {6 Conversions to and from strings} *)
+
+let to_string = string_of_big_int
+(* Return the string representation of the given big integer,
+ in decimal (base 10). *)
+let of_string = big_int_of_string
+(* Convert a string to a big integer, in decimal.
+ The string consists of an optional [-] or [+] sign,
+ followed by one or several decimal digits. *)
+
+(* {6 Conversions to and from other numerical types} *)
+
+let of_int = big_int_of_int
+(* Convert a small integer to a big integer. *)
+let is_int = is_int_big_int
+(* Test whether the given big integer is small enough to
+ be representable as a small integer (type [int])
+ without loss of precision. On a 32-bit platform,
+ [is_int_big_int a] returns [true] if and only if
+ [a] is between 2{^30} and 2{^30}-1. On a 64-bit platform,
+ [is_int_big_int a] returns [true] if and only if
+ [a] is between -2{^62} and 2{^62}-1. *)
+let to_int = int_of_big_int
+(* Convert a big integer to a small integer (type [int]).
+ Raises [Failure "int_of_big_int"] if the big integer
+ is not representable as a small integer. *)
+
+(* Functions used by extraction *)
+
+let double n = (Z.shift_left n 1)
+let succ_double n = Z.succ (Z.shift_left n 1)
+let pred_double n = Z.pred (Z.shift_left n 1)
+
+let nat_case fO fS n = if sign n <= 0 then fO () else fS (pred n)
+
+let positive_case f2p1 f2p f1 p =
+ if le p one then f1 () else
+ let (q,r) = quomod p two in if eq r zero then f2p q else f2p1 q
+
+let n_case fO fp n = if sign n <= 0 then fO () else fp n
+
+let z_case fO fp fn z =
+ let s = sign z in
+ if s = 0 then fO () else if s > 0 then fp z else fn (opp z)
+
+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 nat_rec fO fS =
+ let rec loop acc n =
+ if sign n <= 0 then acc else loop (fS acc) (pred n)
+ in loop fO
+
+let positive_rec f2p1 f2p f1 =
+ let rec loop n =
+ if le n one then f1
+ else
+ let (q,r) = quomod n two in
+ if eq r zero then f2p (loop q) else f2p1 (loop q)
+ in loop
+
+let z_rec fO fp fn = z_case (fun _ -> fO) fp fn
+
+let rec nat_rect acc f n =
+ if sign n <= 0 then acc else nat_rect (f () acc) f (pred n)
+
+let rec iter_nat f n acc =
+ if sign n <= 0 then acc else iter_nat f (pred n) (f acc)
+
+external identity: 'a -> 'a = "%identity"
+
+let shiftl_pos a p = Z.shift_left a (Z.to_int p)
+
+let modulo_pos a b =
+ assert (sign a >= 0);
+ assert (sign b >= 0);
+ modulo a b
+
+let div_pos a b =
+ assert (sign a >= 0);
+ assert (sign b > 0);
+ div a b
+
+let square a = Z.mul a a
+
+let pow_pos a p =
+ Z.pow a (Z.to_int p)
+
+let div2_trunc n = Z.shift_right_trunc n 1
+
+let div_floor = Z.fdiv
+let div2_floor n = Z.shift_right n 1
+let mod_floor a b =
+ let r = Z.rem a b in
+ if (Stdlib.(lxor) (Z.sign a) (Z.sign b) >= 0) || Z.equal r Z.zero
+ then r
+ else Z.add b r
+
+let div_mod_floor a b =
+ let p,r as pr = Z.div_rem a b in
+ if ((Stdlib.(lxor) (Z.sign a) (Z.sign b)) >= 0) || Z.equal r Z.zero
+ then pr
+ else Z.pred p, Z.add b r
+
+let pos_div_eucl a b =
+ assert (sign a >= 0);
+ assert (sign b > 0);
+ Z.div_rem a b
+
+let shiftl a n =
+ let n = Z.to_int n in
+ if n < 0 then Z.shift_right a (-n)
+ else Z.shift_left a n
+
+let shiftr a n =
+ let n = Z.to_int n in
+ if n < 0 then Z.shift_left a (-n)
+ else Z.shift_right a n
+
+let ldiff a b = Z.logand a (Z.lognot b)
+
+module Z = Z (* zarith *)
+
+
+(* Q *)
+(* must be already normalize *)
+let q_mk (den,num) = {Q.den; Q.num}
+let q_case f q = f q.Q.den q.Q.num
+let q_den q = q.Q.den
+let q_num q = q.Q.num
+
+type mode =
+ | NE
+ | ZR
+ | DN
+ | UP
+ | NA
+
+type classify =
+ | Zero of bool
+ | Infinity of bool
+ | NaN of bool * Z.t
+ | Finite of bool * Z.t * Z.t
+
+let combine_hash acc n = n * 65599 + acc
diff --git a/farith2/thry/.gitignore b/farith2/thry/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..cc786a9724d1c928c856bdcbef4ce2acdc6ede2d
--- /dev/null
+++ b/farith2/thry/.gitignore
@@ -0,0 +1 @@
+doc/
\ No newline at end of file
diff --git a/farith2/thry/.nra.cache b/farith2/thry/.nra.cache
new file mode 100644
index 0000000000000000000000000000000000000000..d98ef9c4b6c6b430155da61742d938534ee28064
Binary files /dev/null and b/farith2/thry/.nra.cache differ
diff --git a/farith2/thry/All.v b/farith2/thry/All.v
new file mode 100644
index 0000000000000000000000000000000000000000..90ece08dd73b91e37aa7dcefd9ee4557c375ef92
--- /dev/null
+++ b/farith2/thry/All.v
@@ -0,0 +1,27 @@
+(** * A list of all submodules of Farith2 *)
+
+(** Usefull facts about floating points *)
+From F Require Import Utils.
+
+(** An extension of [R] including infinite values
+ together with a new semantic for floating points
+*)
+From F Require Import Rextended.
+
+(** An extension of [Q] including infinite values
+ used to write the specifications of conversions from [Q] to [float]
+ and from [float] to [Q]
+*)
+From F Require Import Qextended.
+
+(** Correction lemmas associated to floating point binary operators *)
+From F Require Import Utils.
+
+(** A 32 bits instanciation of Flocq's [BinarySingleNaN] *)
+From F Require Import B32.
+
+(** Generic float intervals with verified propagators *)
+From F Require Import Interval.
+
+(** A 32 bits instanciation of [Interval] *)
+From F Require Import Intv32.
\ No newline at end of file
diff --git a/farith2/thry/B32.v b/farith2/thry/B32.v
new file mode 100644
index 0000000000000000000000000000000000000000..3b42e90e6db5dec1dfb68aa50f953b2b3e0aa60e
--- /dev/null
+++ b/farith2/thry/B32.v
@@ -0,0 +1,134 @@
+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.
+
+
+(** * An instanciation of Flocq's BinarySingleNan for 32 bits IEEE-754 floating points *)
+
+Module B32.
+
+(** ** 1. Precision, maximal exponent & their properties *)
+
+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.
+Proof.
+ unfold mw; lia.
+Qed.
+
+Lemma Hew : (0 < ew)%Z.
+Proof.
+ unfold ew; lia.
+Qed.
+
+(** ** 2. Floating-points operators *)
+
+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 := @Bdiv _ _ Hprec Hemax.
+Definition sqrt : mode -> t -> t := @Bsqrt _ _ Hprec Hemax.
+Definition abs : t -> t := Babs.
+
+(** ** 3. Floating-points relations *)
+
+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.
+
+(** ** 4. convertions to and from [Z] and [Q]*)
+
+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/farith2/thry/Correction_thms.v b/farith2/thry/Correction_thms.v
new file mode 100644
index 0000000000000000000000000000000000000000..ae8eae891593325667706b4f48c757ee2e02e192
--- /dev/null
+++ b/farith2/thry/Correction_thms.v
@@ -0,0 +1,260 @@
+From Flocq Require Import IEEE754.BinarySingleNaN.
+From Coq Require Import ZArith Lia Reals Psatz.
+From F Require Import Utils Rextended.
+
+Section Correction.
+
+Variable prec : Z.
+Variable emax : Z.
+Context (Hprec : FLX.Prec_gt_0 prec).
+Context (Hemax : Prec_lt_emax prec emax).
+
+Definition float : Type := binary_float prec emax.
+
+
+Lemma B2SF_eq :
+ forall (x : float) y H, B2SF x = y -> x = SF2B y H.
+Proof.
+ intros.
+ apply B2SF_inj.
+ rewrite H0.
+ symmetry.
+ apply B2SF_SF2B.
+Qed.
+
+Lemma Bplus_correct :
+ forall (m : mode) (x y : float),
+ is_nan (Bplus m x y) = false ->
+ B2Rx (Bplus m x y) = round m (add (B2Rx x) (B2Rx y)).
+Proof.
+ Ltac compute0 :=
+ match goal with
+ | [ m : mode |- _ ] =>
+ destruct m; simpl (B2Rx (B754_zero _)); (rewrite add_0_l || rewrite add_0_r); try apply round_id; apply round_0
+ end.
+ intros m x y HnanS.
+ destruct (Bplus_not_nan_inv _ _ _ HnanS) as [HnanX HnanY].
+ induction x as [ [ ] | [ ] | | ] eqn:Ex, y as [ [ ] | [ ] | | ] eqn:Ey; try easy; try compute0.
+ unfold add.
+ repeat rewrite (B2Rx_finite (B754_finite _ _ _ _)); auto.
+ unfold round.
+ assert (Fx : is_finite x = true) by (rewrite Ex; auto).
+ assert (Fy : is_finite y = true) by (rewrite Ey; auto).
+ pose proof (Bplus_correct _ _ _ _ m x y Fx Fy).
+ destruct (do_overflow _ _ _ _) eqn:Ho1.
+ - apply do_overflow_true in Ho1.
+ unfold dont_overflow in Ho1.
+ rewrite <- Ex, <- Ey in *.
+ unfold R_imax in Ho1.
+ rewrite Ho1 in H.
+ destruct H as [H1 H2].
+ apply (B2SF_eq _ _ (binary_overflow_correct _ _ _ _ _ _)) in H1.
+ destruct m eqn:Em, (sign (B2R x + B2R y)) eqn:Hs.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_neg_inv in Hs.
+ pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_pos_inv in Hs.
+ pose proof (IZR_neg m2); pose proof (IZR_neg m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_neg_inv in Hs.
+ pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_pos_inv in Hs.
+ change (Z.neg m2) with (- Z.pos m2)%Z in Hs.
+ change (Z.neg m3) with (- Z.pos m3)%Z in Hs.
+ repeat rewrite opp_IZR in Hs.
+ pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_neg_inv in Hs.
+ pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_pos_inv in Hs.
+ pose proof (IZR_neg m2); pose proof (IZR_neg m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ nra.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_neg_inv in Hs.
+ pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_pos_inv in Hs.
+ pose proof (IZR_neg m2); pose proof (IZR_neg m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_neg_inv in Hs.
+ pose proof (IZR_pos m2); pose proof (IZR_pos m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
+ + simpl in *. rewrite H1; simpl.
+ fdestruct x; fdestruct y.
+ destruct s1, s2; simpl in *; try easy.
+ unfold Defs.F2R in Hs; simpl in Hs.
+ apply sign_pos_inv in Hs.
+ pose proof (IZR_neg m2); pose proof (IZR_neg m3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e3);
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e5); nra.
+ - apply do_overflow_false in Ho1.
+ unfold dont_overflow in Ho1.
+ rewrite <- Ex, <- Ey in *.
+ unfold R_imax in Ho1.
+ rewrite Ho1 in H.
+ now destruct H as [<- [Hf _]], (Bplus _ _ _).
+Qed.
+
+Theorem Bplus_le_compat:
+ forall m (a b c : float),
+ is_nan (Bplus m a c) = false ->
+ is_nan (Bplus m b c) = false ->
+ a <= b ->
+ Bplus m a c <= Bplus m b c.
+Proof.
+ intros m a b c Hnan1 Hnan2 Hab.
+ apply B2Rx_le; try easy.
+ rewrite (Bplus_correct m a c Hnan1).
+ rewrite (Bplus_correct m b c Hnan2).
+ apply round_le.
+ apply add_leb_mono_l.
+ fdestruct a; fdestruct b; simpl.
+ - apply Raux.Rle_bool_true; lra.
+ - apply Raux.Rle_bool_true; lra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_pos m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - apply Raux.Rle_bool_true; lra.
+ - apply Raux.Rle_bool_true; lra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_pos m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_neg m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_neg m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - destruct s, s0; simpl; try easy;
+ apply Bleb_Rle in Hab; auto;
+ now apply Raux.Rle_bool_true.
+Qed.
+
+Theorem Bplus_le_compat_l:
+ forall m (a b c : float),
+ is_nan (Bplus m c a) = false ->
+ is_nan (Bplus m c b) = false ->
+ a <= b ->
+ Bplus m c a <= Bplus m c b.
+Proof.
+ intros m a b c Hnan1 Hnan2 Hab.
+ apply B2Rx_le; try easy.
+ rewrite (Bplus_correct m c a Hnan1).
+ rewrite (Bplus_correct m c b Hnan2).
+ apply round_le.
+ apply add_leb_mono_r.
+ fdestruct a; fdestruct b; simpl.
+ - apply Raux.Rle_bool_true; lra.
+ - apply Raux.Rle_bool_true; lra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_pos m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - apply Raux.Rle_bool_true; lra.
+ - apply Raux.Rle_bool_true; lra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_pos m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_neg m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_neg m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - destruct s, s0; simpl; try easy;
+ apply Bleb_Rle in Hab; auto;
+ now apply Raux.Rle_bool_true.
+Qed.
+
+Theorem Bplus_le_compat':
+ forall m (a b c d : float),
+ is_nan (Bplus m a b) = false ->
+ is_nan (Bplus m c d) = false ->
+ a <= c ->
+ b <= d ->
+ Bplus m a b <= Bplus m c d.
+Proof.
+ intros.
+ apply B2Rx_le; try easy.
+ rewrite (Bplus_correct m a b); auto.
+ rewrite (Bplus_correct m c d); auto.
+ eapply leb_trans.
+ - apply round_le.
+ apply add_leb_mono_l.
+ apply (le_B2Rx _ _ H1).
+ - apply round_le.
+ apply add_leb_mono_r.
+ apply (le_B2Rx _ _ H2).
+Qed.
+
+End Correction.
\ No newline at end of file
diff --git a/farith2/thry/Interval.v b/farith2/thry/Interval.v
new file mode 100644
index 0000000000000000000000000000000000000000..5279d9c0a412e8b62e6821db23b23de92cab5d4a
--- /dev/null
+++ b/farith2/thry/Interval.v
@@ -0,0 +1,411 @@
+From Flocq Require Import IEEE754.BinarySingleNaN.
+From Coq Require Import QArith Psatz Reals Extraction.
+Require Import F.Utils F.Correction_thms F.Rextended.
+
+(*********************************************************
+ Interval arithmetic over floatting points
+**********************************************************)
+
+Section Finterval.
+
+Variable prec : Z.
+Variable emax : Z.
+Context (Hprec : FLX.Prec_gt_0 prec).
+Context (Hemax : Prec_lt_emax prec emax).
+
+Definition float := binary_float prec emax.
+
+Inductive Interval' :=
+ | Inan : Interval'
+ | Intv : forall (lo hi : float) (nan : bool), Interval'.
+
+Definition valid (I : Interval') :=
+ match I with
+ | Intv lo hi _ => lo <= hi
+ | _ => True
+ end.
+
+Definition valid_opt (I : option Interval') :=
+ match I with
+ | Some (Intv lo hi _) => lo <= hi
+ | _ => True
+ end.
+
+Definition Interval := { I : Interval' | valid I }.
+
+Definition Interval_opt := { I : option Interval' | valid_opt I }.
+
+Program Definition contains (I : Interval') (x : float) : Prop :=
+ match I with
+ | Inan => is_nan x = true
+ | Intv lo hi nan =>
+ lo <= x <= hi \/ (is_nan x && nan = true)
+ end.
+
+Definition contains_opt (I : option Interval') (x : float) : Prop :=
+ match I with
+ | None => False
+ | Some i => contains i x
+ end.
+
+Program Definition inter' (I1 I2 : Interval') : option Interval' :=
+ match I1, I2 with
+ | Inan, Inan => Some Inan
+ | Inan, Intv _ _ nan =>
+ if nan then Some Inan else None
+ | Intv _ _ nan, Inan =>
+ if nan then Some (Inan) else None
+ | Intv lo1 hi1 nan1, Intv lo2 hi2 nan2 =>
+ if Bltb hi1 lo2 || Bltb hi2 lo1 then
+ if nan1 && nan2 then Some Inan else None
+ else
+ Some (Intv (Bmax lo1 lo2) (Bmin hi1 hi2) (nan1 && nan2))
+ end.
+
+Ltac ieasy :=
+ simpl in *; try easy; try (intuition; fail).
+
+Ltac sdestruct x :=
+ try destruct x; simpl; easy.
+
+Program Definition inter (I1 I2 : Interval) : Interval_opt :=
+ inter' I1 I2.
+Next Obligation.
+ destruct I1 as [[|lo1 hi1 nan1] H1], I2 as [[|lo2 hi2 nan2] H2]; ieasy; try (now destruct nan1 || now destruct nan2).
+ case (Bltb (hi1) (lo2)) eqn:?, (Bltb (hi2) (lo1)) eqn:?; simpl; try (destruct nan1, nan2; simpl; easy).
+ pose proof (le_not_nan_l _ _ H1).
+ pose proof (le_not_nan_r _ _ H2).
+ pose proof (le_not_nan_r _ _ H1).
+ pose proof (le_not_nan_l _ _ H2).
+ auto using Bmax_le, Bmin_le, Bltb_false_Bleb.
+Defined.
+
+Program Lemma inter_precise_l :
+ forall I1 I2, forall x, contains_opt (inter I1 I2) x -> contains I1 x.
+Proof with auto.
+ intros [[|lo1 hi1 nan1] H1] [[|lo2 hi2 nan2] H2] x Hx; simpl in *...
+ + destruct nan2; fdestruct x.
+ + right; destruct nan1; fdestruct x.
+ + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *;
+ try (right; destruct nan1, nan2; simpl in *; fdestruct x; fail).
+ destruct Hx as [[Hc1 Hc2] | H ].
+ - left; split; [ apply (Bmax_le_inv _ _ _ _ _ Hc1) | apply (Bmin_le_inv _ _ _ _ _ Hc2) ].
+ - repeat rewrite andb_true_iff in H; intuition.
+Qed.
+
+Program Lemma inter_precise_r :
+ forall I1 I2, forall x, contains_opt (inter I1 I2) x -> contains I2 x.
+Proof with auto.
+ intros [[|lo1 hi1 nan1] H1] [[|lo2 hi2 nan2] H2] x Hx; simpl in *...
+ + right; destruct nan2; fdestruct x.
+ + destruct nan1; fdestruct x.
+ + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *;
+ try (right; destruct nan1, nan2; simpl in *; fdestruct x; fail).
+ destruct Hx as [[Hc1 Hc2] | H ].
+ - left; split; [ apply (Bmax_le_inv _ _ _ _ _ Hc1) | apply (Bmin_le_inv _ _ _ _ _ Hc2) ].
+ - repeat rewrite andb_true_iff in H; intuition.
+Qed.
+
+Program Lemma inter_correct :
+ forall (I1 I2 : Interval), forall x, contains I1 x -> contains I2 x -> contains_opt (inter I1 I2) x.
+Proof with auto.
+ intros [[|lo1 hi1 nan1] H1] [[|lo2 hi2 nan2] H2] x Hx1 Hx2; simpl in *...
+ - fdestruct x; destruct nan2, Hx2; try easy.
+ - fdestruct x; destruct nan1, Hx1; try easy.
+ - pose proof (le_not_nan_l _ _ H1).
+ pose proof (le_not_nan_r _ _ H1).
+ pose proof (le_not_nan_l _ _ H2).
+ pose proof (le_not_nan_r _ _ H2).
+ destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |]; try (fdestruct x ; fail).
+ + pose proof (Hlt1 := Bleb_trans _ _ _ Hc2 Hc1').
+ apply Bleb_true_Bltb in Hlt1...
+ pose proof (Hlt2 := Bleb_trans _ _ _ Hc1 Hc2').
+ apply Bleb_true_Bltb in Hlt2...
+ rewrite Hlt1, Hlt2; simpl; left; split; auto using Bmax_le, Bmin_le.
+ + fdestruct x; destruct nan2, nan1, (Bltb hi1 _), (Bltb hi2); simpl; try easy.
+ now right.
+Qed.
+
+Definition Iadd' (m : mode) (I1 I2 : Interval') : Interval' :=
+ match I1, I2 with
+ | Inan, _ => Inan
+ | _, Inan => Inan
+ | Intv l h n, Intv l' h' n' =>
+ let sum1 := Bplus m l l' in
+ let sum2 := Bplus m h h' in
+ match is_nan sum1 with
+ | true =>
+ match is_nan sum2 with
+ | true => Inan
+ | false => Intv +oo +oo true
+ end
+ | false =>
+ match is_nan sum2 with
+ | true => Intv -oo -oo true
+ | false => Intv sum1 sum2 (n || n' || (Beqb h +oo && Beqb l' -oo) || (Beqb h' +oo && Beqb l -oo))
+ end
+ end
+ end.
+
+Program Definition Iadd (m : mode) (I1 I2 : Interval) : Interval :=
+ Iadd' m I1 I2.
+Next Obligation.
+ destruct I1 as [[|l1 h1] H1], I2 as [[|l2 h2] H2]; simpl in *; auto.
+ destruct (is_nan (Bplus m l1 l2)) eqn:E1, (is_nan (Bplus m h1 h2)) eqn:E2; try easy; simpl.
+ apply B2Rx_le; auto.
+ repeat (rewrite Bplus_correct; auto).
+ apply round_le.
+ eapply leb_trans.
+ - apply (add_leb_mono_l _ _ _ (le_B2Rx _ _ H1)).
+ - apply (add_leb_mono_r _ _ _ (le_B2Rx _ _ H2)).
+Qed.
+
+Program Lemma Iadd_correct :
+ forall m (I1 I2 : Interval) (x y : float), contains I1 x -> contains I2 y -> contains (Iadd m I1 I2) (Bplus m x y).
+Proof with auto.
+ intros m [[|l1 h1] H1] [[|l2 h2] H2] x y Hx Hy; simpl in *; try (fdestruct x; fdestruct y; fail).
+ case (is_nan (Bplus m l1 l2)) eqn:E1, (is_nan (Bplus m h1 h2)) eqn:E2; intuition; simpl.
+ all: try (fdestruct x; fdestruct y; simpl; auto; fail).
+ - destruct (Bplus_nan_inv _ _ _ E1); intuition; subst; try easy.
+ * rewrite (infp_le_is_infp _ _ _ H0) in *.
+ rewrite (infp_le_is_infp _ _ _ H1) in *.
+ fdestruct h2.
+ rewrite (le_infm_is_infm _ _ _ H5) in *...
+ * rewrite (infp_le_is_infp _ _ _ H4) in *.
+ rewrite (infp_le_is_infp _ _ _ H2) in *.
+ fdestruct h1.
+ rewrite (le_infm_is_infm _ _ _ H3) in *...
+ - destruct (Bplus_nan_inv _ _ _ E1) as [[ -> -> ] | [ [ -> -> ] | [ -> | -> ]]]; try easy;
+ fdestruct x; fdestruct y; simpl...
+ - destruct (Bplus_nan_inv _ _ _ E2) as [[ -> -> ] | [ [ -> -> ] | [ -> | -> ]]]; try easy;
+ fdestruct x; fdestruct y; simpl...
+ - destruct (is_nan (Bplus m x y)) eqn:E.
+ + right. destruct (Bplus_nan_inv _ _ _ E) as [ [-> ->] | [ [ -> -> ] | ] ].
+ * rewrite (infp_le_is_infp _ _ _ H3) in *.
+ rewrite (le_infm_is_infm _ _ _ H4) in *.
+ fdestruct l2; simpl; fdestruct h1; simpl; intuition.
+ * rewrite (infp_le_is_infp _ _ _ H5) in *.
+ rewrite (le_infm_is_infm _ _ _ H0) in *.
+ fdestruct h1; simpl; fdestruct l2; simpl; intuition.
+ * destruct H as [ -> | -> ]; fdestruct h1.
+ + left. split; now apply Bplus_le_compat'.
+ - right; fdestruct y; fdestruct x; destruct nan0; simpl; intuition.
+ - right; fdestruct y; fdestruct x; destruct nan; simpl; intuition.
+ - right; fdestruct y; fdestruct x; destruct nan; simpl; intuition.
+Qed.
+
+Notation "'Interval+⊥'" := Interval_opt.
+
+Program Definition Ile (I : Interval) : Interval+⊥ :=
+ match I with
+ | Inan => None
+ | Intv a b n =>
+ Some (Intv -oo b n)
+ end.
+Next Obligation.
+ destruct I as [[|l1 h1] H1]; simpl in *; fdestruct b.
+ inversion Heq_I; subst.
+ fdestruct l1.
+Defined.
+
+
+Program Theorem Ile_correct :
+ forall (I : Interval) (x y : float), contains I y -> x <= y -> contains_opt (Ile I) x.
+Proof.
+ intros [[| l1 h1] H1] x y Hx Hxy; simpl in *.
+ - fdestruct y; fdestruct x.
+ - destruct (is_nan x), Hx as [ [H H'] | ];
+ try (left ; idtac; split; [ fdestruct x | apply (Bleb_trans _ _ _ Hxy H')]);
+ try (right ; fdestruct y; fdestruct x).
+Qed.
+
+Program Definition Ilt (I : Interval) : Interval+⊥ :=
+ match I with
+ | Inan => None
+ | Intv a b n =>
+ Some (Intv -oo b n)
+ end.
+Next Obligation.
+ destruct I as [[|l1 h1] H1]; simpl in *; fdestruct b;
+ inversion Heq_I; subst; fdestruct l1.
+Defined.
+
+
+Program Theorem Ilt_correct :
+ forall (I : Interval) (x y : float), contains I y -> Bltb x y = true -> contains_opt (Ilt I) x.
+Proof.
+ intros [[| l1 h1] H1] x y Hx Hxy; simpl in *.
+ - fdestruct y; fdestruct x.
+ - apply Bltb_Bleb in Hxy.
+ destruct (is_nan x), Hx as [ [H H'] | ];
+ try (left ; idtac; split; [ fdestruct x | apply (Bleb_trans _ _ _ Hxy H')]);
+ try (right ; fdestruct y; fdestruct x).
+Qed.
+
+Program Definition Ige (I : Interval) : Interval+⊥ :=
+ match I with
+ | Inan => None
+ | Intv a b n =>
+ Some (Intv a +oo n)
+ end.
+Next Obligation.
+ destruct I as [[|l1 h1] H1]; simpl in *; fdestruct b;
+ inversion Heq_I; subst; fdestruct l1.
+Defined.
+
+Program Theorem Ige_correct :
+ forall (I : Interval) (x y : float), contains I y -> Bleb y x = true -> contains_opt (Ige I) x.
+Proof.
+ intros [[| l1 h1] H1] x y Hx Hxy; simpl in *.
+ - fdestruct y; fdestruct x.
+ - destruct (is_nan x), Hx as [ [H H'] | ];
+ try (left ; idtac; split; [ apply (Bleb_trans _ _ _ H Hxy) | fdestruct x; fdestruct y ]);
+ try (right ; fdestruct y; fdestruct x).
+Qed.
+
+Program Definition Igt (I : Interval) : Interval+⊥ :=
+ match I with
+ | Inan => None
+ | Intv a b n =>
+ Some (Intv a +oo n)
+ end.
+Next Obligation.
+ destruct I as [[|l1 h1] H1]; simpl in *; fdestruct b;
+ inversion Heq_I; subst; fdestruct l1.
+Defined.
+
+Program Theorem Igt_correct :
+ forall (I : Interval) (x y : float), contains I y -> Bltb y x = true -> contains_opt (Igt I) x.
+Proof.
+ intros [[| l1 h1] H1] x y Hx Hxy; simpl in *.
+ - fdestruct y; fdestruct x.
+ - apply Bltb_Bleb in Hxy.
+ destruct (is_nan x), Hx as [ [H H'] | ];
+ try (left ; idtac; split; [ apply (Bleb_trans _ _ _ H Hxy) | fdestruct x; fdestruct y ]);
+ try (right ; fdestruct y; fdestruct x).
+Qed.
+
+Program Definition inter_opt (I1 I2 : Interval+⊥) : Interval+⊥ :=
+ match I1, I2 with
+ | None, _ => None
+ | _, None => None
+ | Some i1, Some i2 => inter i1 i2
+ end.
+Next Obligation.
+ destruct I1 as [[[|l1 h1 n1]|] H1]; simpl in *; now inversion Heq_I1.
+Defined.
+Next Obligation.
+ destruct I2 as [[[|l1 h1 n1]|] H1]; simpl in *; now inversion Heq_I2.
+Defined.
+
+Program Definition to_opt (I : Interval) : Interval+⊥ :=
+ Some (I :>).
+Next Obligation.
+ now destruct I as [[| l h n ] H].
+Defined.
+
+Coercion to_opt : Interval >-> Interval_opt.
+
+Ltac fall_cases x :=
+ try (fdestruct x; fail).
+
+Ltac fall_cases2 x y :=
+ try (fdestruct x; fdestruct y; fail).
+
+
+Definition Ige_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+ (inter_opt (Ige I2) I1, inter_opt (Ile I1) I2).
+
+Program Theorem Ige_inv_correct :
+ forall (I1 I2 : Interval) (x y : float),
+ contains I1 x -> contains I2 y ->
+ y <= x ->
+ contains_opt (fst (Ige_inv I1 I2)) x /\
+ contains_opt (snd (Ige_inv I1 I2)) y.
+Proof.
+ intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+ split; apply inter_correct; simpl in *; auto.
+ + destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; fall_cases2 y x.
+ left; split; [ apply (Bleb_trans _ _ _ Hy Hxy) | fdestruct x ].
+ + destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; fall_cases2 y x.
+ left; split; [ fdestruct y; fdestruct x | apply (Bleb_trans _ _ _ Hxy Hx') ].
+Qed.
+
+
+Definition Igt_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+ (inter_opt (Igt I2) I1, inter_opt (Ilt I1) I2).
+
+Program Theorem Igt_inv_correct :
+ forall (I1 I2 : Interval) (x y : float),
+ contains I1 x -> contains I2 y ->
+ Bltb y x = true ->
+ contains_opt (fst (Igt_inv I1 I2)) x /\
+ contains_opt (snd (Igt_inv I1 I2)) y.
+Proof.
+ intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+ split; apply inter_correct; simpl in *; auto; destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; auto; fall_cases2 x y.
+ + left; split.
+ * apply (Bleb_trans _ _ _ Hy (Bltb_Bleb _ _ _ _ Hxy)).
+ * fdestruct x.
+ + left; split.
+ * fdestruct y.
+ * apply (Bleb_trans _ _ _ (Bltb_Bleb _ _ _ _ Hxy) Hx').
+Qed.
+
+Definition Ilt_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+ (inter_opt (Ilt I2) I1, inter_opt (Igt I1) I2).
+
+Program Theorem Ilt_inv_correct :
+ forall (I1 I2 : Interval) (x y : float),
+ contains I1 x -> contains I2 y ->
+ Bltb x y = true ->
+ contains_opt (fst (Ilt_inv I1 I2)) x /\
+ contains_opt (snd (Ilt_inv I1 I2)) y.
+Proof.
+ intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+ split; apply inter_correct; simpl in *; auto; destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; auto; fall_cases2 x y.
+ + left; split; fall_cases x.
+ apply (Bleb_trans _ _ _ (Bltb_Bleb _ _ _ _ Hxy) Hy').
+ + left; split; fall_cases y.
+ apply (Bleb_trans _ _ _ Hx (Bltb_Bleb _ _ _ _ Hxy)).
+Qed.
+
+Definition Ile_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+ (inter_opt (Ile I2) I1, inter_opt (Ige I1) I2).
+
+Program Theorem Ile_inv_correct :
+ forall (I1 I2 : Interval) (x y : float),
+ contains I1 x -> contains I2 y ->
+ x <= y ->
+ contains_opt (fst (Ile_inv I1 I2)) x /\
+ contains_opt (snd (Ile_inv I1 I2)) y.
+Proof.
+ intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+ split; apply inter_correct; simpl in *; auto; destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; auto; fall_cases2 x y.
+ + left; split; fall_cases x.
+ apply (Bleb_trans _ _ _ Hxy Hy').
+ + left; split; fall_cases y.
+ apply (Bleb_trans _ _ _ Hx Hxy).
+Qed.
+
+Definition Ieq_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+ (inter_opt I1 I2, inter_opt I1 I2).
+
+Program Theorem Ieq_inv_correct :
+ forall (I1 I2 : Interval) (x y : float),
+ contains I1 x -> contains I2 y ->
+ Beqb x y = true ->
+ contains_opt (fst (Ieq_inv I1 I2)) x /\
+ contains_opt (snd (Ieq_inv I1 I2)) y.
+Proof.
+ intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+ split; apply inter_correct; simpl in *; auto; destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; auto; fall_cases2 x y.
+ + left; split.
+ * apply (Bleb_trans l2 y x Hy (Beqb_Bleb _ _ _ _ (Beqb_symm _ _ _ _ Hxy))).
+ * apply (Bleb_trans x y h2 (Beqb_Bleb _ _ _ _ Hxy) Hy').
+ + left; split.
+ * apply (Bleb_trans l1 x y Hx (Beqb_Bleb _ _ _ _ Hxy)).
+ * apply (Bleb_trans y x h1 (Beqb_Bleb _ _ _ _ (Beqb_symm _ _ _ _ Hxy)) Hx').
+Qed.
+
+End Finterval.
\ No newline at end of file
diff --git a/farith2/thry/Intv32.v b/farith2/thry/Intv32.v
new file mode 100644
index 0000000000000000000000000000000000000000..5c135e067d802817f17495dc2ebd952527d9078c
--- /dev/null
+++ b/farith2/thry/Intv32.v
@@ -0,0 +1,170 @@
+From Coq Require Import ZArith Extraction Bool Psatz ExtrOcamlBasic.
+From Flocq Require Import IEEE754.BinarySingleNaN FLX.
+From F Require Import Utils Interval B32.
+
+Notation "x '+⊥'" := (option x) (at level 80).
+
+Module Intv32.
+ Definition prec := 24%Z.
+ Definition emax := 128%Z.
+ Definition float32 := B32.t.
+
+ 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.
+
+ Definition t := Interval prec emax.
+
+ Definition t_opt := Interval_opt prec emax.
+
+ Program Definition contains : t -> float32 -> Prop := contains prec emax.
+
+ Program Definition contains_opt : t_opt -> float32 -> Prop := contains_opt prec emax.
+
+ Definition inter (x y : t) : t_opt :=
+ @inter prec emax x y.
+
+ Definition add : mode -> t -> t -> t :=
+ @Iadd prec emax Hprec Hemax.
+
+ Program Lemma inter_correct :
+ forall (i1 i2 : t) (x : float32),
+ contains i1 x -> contains i2 x -> contains_opt (inter i1 i2) x.
+ Proof.
+ apply (inter_correct prec emax).
+ Qed.
+
+ Lemma inter_precise :
+ forall (i1 i2 : t) (x : float32),
+ contains_opt (inter i1 i2) x -> contains i1 x /\ contains i2 x.
+ Proof.
+ intros; split.
+ - apply (inter_precise_l prec emax _ _ _ H).
+ - apply (inter_precise_r prec emax _ _ _ H).
+ Qed.
+
+ Lemma add_correct :
+ forall (m : mode) (i1 i2 : t) (x y : float32),
+ contains i1 x -> contains i2 y -> contains (add m i1 i2) (@Bplus prec emax Hprec Hemax m x y).
+ Proof. apply Iadd_correct. Qed.
+
+ Program Definition top : t := Intv prec emax -oo +oo true.
+
+ Program Definition bot : t_opt := None.
+
+ Lemma top_correct :
+ forall (x : float32), contains top x.
+ Proof with auto.
+ unfold top, contains; fdestruct x; simpl...
+ Qed.
+
+ Lemma bot_correct :
+ forall (x : float32), contains_opt bot x -> False.
+ Proof with auto.
+ unfold bot, contains; fdestruct x.
+ Qed.
+
+ Program Definition is_singleton (I : t) : option float32 :=
+ match I with
+ | Inan _ _ => Some NaN
+ | Intv _ _ a b n =>
+ if Beqb a b && (negb (Beqb a (B754_zero false))) && negb n then Some a
+ else None
+ end.
+
+ Program Definition s0 : Interval prec emax := Intv _ _ (B754_zero false) (B754_zero true) false.
+
+ Program Theorem is_singleton_correct :
+ forall (I : t) (x : float32), (is_singleton I = Some x) -> (forall y, contains I y -> x = y).
+ Proof.
+ intros [[| a b n] H] x; cbn.
+ - intros H1; inversion H1; fdestruct y.
+ - intros H' y [[H1 H2] | H2].
+ + destruct (Beqb a b) eqn:?E, (negb n) eqn:?E, (negb (Beqb a (B754_zero false))) eqn:?; try easy; simpl in *.
+ assert (a <= y <= a) by eauto using E, Beqb_symm, Beqb_Bleb, Bleb_trans.
+ apply Bleb_antisymm_strict in H0.
+ * inversion H'; subst; reflexivity.
+ * now apply Bool.negb_true_iff in Heqb0.
+ + destruct (Beqb a b) eqn:?E, (negb n) eqn:?E, (negb (Beqb a (B754_zero false))) eqn:?; try easy; simpl in *.
+ destruct n; try easy.
+ fdestruct y.
+ Qed.
+
+ Program Definition singleton (x : float32) : t :=
+ match x with
+ | B754_nan => Inan prec emax
+ | _ => Intv _ _ x x false
+ end.
+ Next Obligation.
+ apply Bleb_refl.
+ fdestruct x.
+ Defined.
+
+ Program Theorem singleton_correct :
+ forall (x : float32), Beqb x (B754_zero true) = false -> is_singleton (singleton x) = Some x.
+ Proof.
+ intros [ [ ] | [ ] | | [ ] ] H; try easy; cbn.
+ - rewrite Z.compare_refl, Pcompare_refl; reflexivity.
+ - rewrite Z.compare_refl, Pcompare_refl; reflexivity.
+ Qed.
+
+ Program Definition ge : t -> t_opt := @Ige prec emax.
+ Program Definition le : t -> t_opt := @Ile prec emax.
+ Program Definition lt : t -> t_opt := @Ilt prec emax.
+ Program Definition gt : t -> t_opt := @Igt prec emax.
+
+ Program Definition le_inv : t -> t -> (t_opt * t_opt) := @Ile_inv prec emax.
+ Program Definition ge_inv : t -> t -> (t_opt * t_opt) := @Ige_inv prec emax.
+ Program Definition lt_inv : t -> t -> (t_opt * t_opt) := @Ilt_inv prec emax.
+ Program Definition gt_inv : t -> t -> (t_opt * t_opt) := @Igt_inv prec emax.
+ Program Definition eq_inv : t -> t -> (t_opt * t_opt) := @Ieq_inv prec emax.
+
+ Theorem le_inv_correct :
+ forall (I1 I2 : t) (x y : float32),
+ contains I1 x -> contains I2 y -> x <= y ->
+ contains_opt (fst (le_inv I1 I2)) x /\ contains_opt (snd (le_inv I1 I2)) y.
+ Proof. apply (@Ile_inv_correct prec emax). Qed.
+
+ Theorem ge_inv_correct :
+ forall (I1 I2 : t) (x y : float32),
+ contains I1 x -> contains I2 y -> y <= x ->
+ contains_opt (fst (ge_inv I1 I2)) x /\ contains_opt (snd (ge_inv I1 I2)) y.
+ Proof. apply (@Ige_inv_correct prec emax). Qed.
+
+ Theorem gt_inv_correct :
+ forall (I1 I2 : t) (x y : float32),
+ contains I1 x -> contains I2 y -> Bltb y x = true ->
+ contains_opt (fst (gt_inv I1 I2)) x /\ contains_opt (snd (gt_inv I1 I2)) y.
+ Proof. apply (@Igt_inv_correct prec emax). Qed.
+
+ Theorem lt_inv_correct :
+ forall (I1 I2 : t) (x y : float32),
+ contains I1 x -> contains I2 y -> Bltb x y = true ->
+ contains_opt (fst (lt_inv I1 I2)) x /\ contains_opt (snd (lt_inv I1 I2)) y.
+ Proof. apply (@Ilt_inv_correct prec emax). Qed.
+
+ Theorem eq_inv_correct :
+ forall (I1 I2 : t) (x y : float32),
+ contains I1 x -> contains I2 y -> Beqb x y = true ->
+ contains_opt (fst (eq_inv I1 I2)) x /\ contains_opt (snd (eq_inv I1 I2)) y.
+ Proof. apply (@Ieq_inv_correct prec emax). Qed.
+
+ Theorem le_correct :
+ forall (I : t) (x y : float32), contains I y -> x <= y -> contains_opt (le I) x.
+ Proof. apply (@Ile_correct prec emax). Qed.
+
+ Theorem lt_correct :
+ forall (I : t) (x y : float32), contains I y -> Bltb x y = true -> contains_opt (lt I) x.
+ Proof. apply (@Ilt_correct prec emax). Qed.
+
+ Theorem ge_correct :
+ forall (I : t) (x y : float32), contains I y -> y <= x -> contains_opt (ge I) x.
+ Proof. apply (@Ige_correct prec emax). Qed.
+
+ Theorem gt_correct :
+ forall (I : t) (x y : float32), contains I y -> Bltb y x = true -> contains_opt (gt I) x.
+ Proof. apply (@Igt_correct prec emax). Qed.
+
+End Intv32.
\ No newline at end of file
diff --git a/farith2/thry/Qextended.v b/farith2/thry/Qextended.v
new file mode 100644
index 0000000000000000000000000000000000000000..e6fbf4afac0b73bc80c54753b7f194b40d504a1f
--- /dev/null
+++ b/farith2/thry/Qextended.v
@@ -0,0 +1,68 @@
+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 _).
+Definition Qx_one := Qxmake (1)%Z 1%Z (refl_equal _) (refl_equal _).
+Definition Qx_two := Qxmake (2)%Z (1)%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/farith2/thry/Rextended.v b/farith2/thry/Rextended.v
new file mode 100644
index 0000000000000000000000000000000000000000..7444891bdfef9375f531dc9a9e73ede905ffcfa3
--- /dev/null
+++ b/farith2/thry/Rextended.v
@@ -0,0 +1,676 @@
+(*********************************************************
+ Extension of R with special values +oo, -oo
+**********************************************************)
+
+From Flocq Require Import IEEE754.BinarySingleNaN.
+From Coq Require Import ZArith Psatz Reals.
+From F Require Import Utils.
+
+Set Implicit Arguments.
+
+(**
+ Inject BinarySingleNan in R extended with infinities
+*)
+Section Rextended.
+
+Variable prec : Z.
+Variable emax : Z.
+Context (Hprec : FLX.Prec_gt_0 prec).
+Context (Hemax : Prec_lt_emax prec emax).
+
+Definition float := binary_float prec emax.
+
+(** Reals extended with +oo, -oo *)
+Inductive Rx : Type :=
+ | Real : R -> Rx
+ | Inf : bool -> Rx.
+
+Definition R_imax : R := Raux.bpow Zaux.radix2 emax.
+
+Definition R_fmax : R := Raux.bpow Zaux.radix2 emax - Raux.bpow Zaux.radix2 (emax - prec).
+
+Program Definition F_fmax : float := B754_finite false (Z.to_pos (Zpower 2 prec - 1)%Z) (emax - prec) _.
+Next Obligation.
+ refine (binary_overflow_correct prec emax _ _ mode_ZR false).
+Defined.
+
+Lemma R2F_fmax:
+ R_fmax = B2R (F_fmax).
+Proof.
+ unfold FLX.Prec_gt_0 in Hprec.
+ unfold Prec_lt_emax in Hemax.
+ assert (0 < emax)%Z by lia.
+ unfold R_fmax, F_fmax, B2R, Defs.F2R; simpl.
+ destruct prec eqn:E; try easy.
+ rewrite Z2Pos.id.
+ - rewrite <- E, minus_IZR.
+ replace 2%Z with (Zaux.radix_val Zaux.radix2) by auto.
+ rewrite Raux.IZR_Zpower by lia.
+ rewrite Rmult_minus_distr_r.
+ rewrite <- Raux.bpow_plus.
+ replace (prec + (emax - prec))%Z with emax by lia.
+ lra.
+ - assert (1 < 2 ^ (Z.pos p))%Z.
+ + replace 2%Z with (Zaux.radix_val Zaux.radix2) by auto.
+ apply Zaux.Zpower_gt_1; lia.
+ + lia.
+Qed.
+
+Lemma F_fmax_max :
+ forall (x : float), is_finite x = true -> Bleb x F_fmax = true.
+Proof.
+ intros [ [ ] | [ ] | | [ ] m e Hbound'] Fx; auto.
+ apply Rle_Bleb; auto.
+ rewrite <- R2F_fmax.
+ now apply bounded_le_emax_minus_prec.
+Qed.
+
+Lemma F_fmax_min :
+ forall (x : float), is_finite x = true -> Bleb (Bopp F_fmax) x = true.
+Proof.
+ intros [ [ ] | [ ] | | [ ] m e Hbound'] Fx; auto.
+ apply Rle_Bleb; auto.
+ rewrite pos_Bopp_neg, B2R_Bopp, B2R_Bopp, <- R2F_fmax.
+ apply Ropp_le_contravar.
+ now apply bounded_le_emax_minus_prec.
+Qed.
+
+Lemma Rimax_Rfmax :
+ (R_fmax < R_imax)%R.
+Proof.
+ apply minus_pos_lt, Raux.bpow_gt_0.
+Qed.
+
+Definition leb (x y : Rx) :=
+ match x with
+ | Inf true => true
+ | Inf false =>
+ match y with
+ | Inf s => negb s
+ | _ => false
+ end
+ | Real r1 =>
+ match y with
+ | Inf b => negb b
+ | Real r2 => Raux.Rle_bool r1 r2
+ end
+ end.
+
+Definition fexp := SpecFloat.fexp prec emax.
+
+Definition do_overflow (m : mode) (x : R) : bool :=
+ let fexp := SpecFloat.fexp prec emax in
+ let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) x in
+ Raux.Rle_bool R_imax (Rabs rsum).
+
+Definition dont_overflow (m : mode) (x : R) : bool :=
+ let fexp := SpecFloat.fexp prec emax in
+ let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) x in
+ Raux.Rlt_bool (Rabs rsum) R_imax.
+
+Lemma do_overflow_false :
+ forall m r, do_overflow m r = false -> dont_overflow m r = true.
+Proof.
+ intros. unfold do_overflow, dont_overflow in *.
+ now rewrite <- Raux.negb_Rlt_bool, H.
+Qed.
+
+Lemma do_overflow_true :
+ forall m r, do_overflow m r = true -> dont_overflow m r = false.
+Proof.
+ intros. unfold do_overflow, dont_overflow in *.
+ now rewrite <- Raux.negb_Rlt_bool, H.
+Qed.
+
+Lemma dont_overflow_true :
+ forall m r, dont_overflow m r = true -> do_overflow m r = false.
+Proof.
+ intros. unfold do_overflow, dont_overflow in *.
+ now rewrite <- Raux.negb_Rle_bool, Bool.negb_false_iff.
+Qed.
+
+Lemma dont_overflow_false :
+ forall m r, dont_overflow m r = false -> do_overflow m r = true.
+Proof.
+ intros. unfold do_overflow, dont_overflow in *.
+ now rewrite <- Bool.negb_false_iff, Raux.negb_Rlt_bool.
+Qed.
+
+Lemma F2R_congr :
+ forall m1 e1 m2 e2, m1 = m2 -> e1 = e2 ->
+ @Defs.F2R Zaux.radix2 {| Defs.Fnum := m1; Defs.Fexp := e1 |} =
+ @Defs.F2R Zaux.radix2 {| Defs.Fnum := m2; Defs.Fexp := e2 |}.
+Proof. congruence. Qed.
+
+Definition round (m : mode) (r : Rx) : Rx :=
+ match r with
+ | Real x =>
+ if do_overflow m x then
+ if overflow_to_inf m (sign x) then Inf (sign x)
+ else Real (B2R (if sign x then Bopp F_fmax else F_fmax))
+ else
+ Real (Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) x)
+ | _ => r
+ end.
+
+Lemma dont_overflow_inv :
+ forall m (r : R),
+ do_overflow m r = false ->
+ exists (f : float), Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) r = B2R f /\ is_finite f = true.
+Proof.
+ intros mode r H.
+ apply do_overflow_false in H.
+ unfold dont_overflow in H.
+ apply Rltb_Rlt in H.
+ set (e := Generic_fmt.cexp Zaux.radix2 (SpecFloat.fexp prec emax) r).
+ set (m' := Generic_fmt.scaled_mantissa Zaux.radix2 (SpecFloat.fexp prec emax) r).
+ set (m := Z.to_pos (round_mode mode m')).
+ set (s := sign m').
+ destruct (Rsign_split r) as [ | [ | ]].
+ - admit.
+ - exists (B754_zero false); split; auto.
+ rewrite H0, Generic_fmt.round_0; simpl; intuition.
+ - eexists (B754_finite false m e _); split; auto.
+ unfold Generic_fmt.round; simpl.
+ apply F2R_congr; auto.
+ unfold m, m', SpecFloat.cond_Zopp.
+Admitted.
+
+Lemma R_imax_gt_0: (R_imax > 0)%R.
+ apply Raux.bpow_gt_0.
+Qed.
+
+Lemma F_fmax_ge_0: (B2R F_fmax >= 0)%R.
+ simpl.
+ unfold Defs.F2R; simpl.
+ apply Rle_ge, Rmult_le_pos.
+ + apply IZR_le; lia.
+ + left; apply Raux.bpow_gt_0.
+Qed.
+
+Ltac fformat :=
+ try intuition; try apply fexp_correct.
+
+Theorem generic_format_Rimax :
+ Generic_fmt.generic_format Zaux.radix2 fexp R_imax.
+Proof.
+ intros.
+ red; unfold Defs.F2R, R_imax; simpl.
+ rewrite <- Generic_fmt.scaled_mantissa_generic.
+ + unfold Generic_fmt.scaled_mantissa.
+ rewrite Rmult_assoc, Rmult_comm.
+ rewrite <- Raux.bpow_plus.
+ rewrite (Zplus_comm)%R.
+ rewrite Zegal_left by lia; simpl; lra.
+ + apply (Generic_fmt.generic_format_bpow Zaux.radix2 fexp emax).
+ unfold fexp, SpecFloat.fexp, SpecFloat.emin.
+ unfold FLX.Prec_gt_0 in *.
+ unfold Prec_lt_emax in *.
+ lia.
+Qed.
+
+Theorem round_Rimax :
+ forall m, Generic_fmt.round Zaux.radix2 fexp (round_mode m) R_imax = R_imax.
+Proof.
+ intros.
+ apply Generic_fmt.round_generic; intuition.
+ apply generic_format_Rimax.
+Qed.
+
+Lemma Rltb_lt :
+ forall x y, Raux.Rlt_bool x y = true -> (x < y)%R.
+Proof.
+ intros.
+ pose proof (Hp := Raux.Rlt_bool_spec x y).
+ rewrite H in Hp.
+ now inversion Hp.
+Qed.
+
+Lemma Rimax_float :
+ exists m e, R_imax = Defs.F2R (Defs.Float Zaux.radix2 m e).
+Proof.
+ exists 1%Z.
+ unfold R_imax, Defs.F2R; simpl.
+ eexists.
+ symmetry.
+ apply Rmult_1_l.
+Qed.
+
+Lemma incr_R_fmax_R_imax :
+ @Defs.F2R Zaux.radix2 {| Defs.Fnum := (Zpower 2 prec - 1 + 1)%Z ; Defs.Fexp := (emax - prec) |} = R_imax.
+Proof.
+ unfold Defs.F2R, R_imax; simpl.
+ replace (2 ^ prec - 1 + 1)%Z with (2 ^ prec)%Z by lia.
+ rewrite (Raux.IZR_Zpower Zaux.radix2).
+ + rewrite <- Raux.bpow_plus.
+ replace (prec + (emax - prec))%Z with (emax) by lia.
+ reflexivity.
+ + unfold FLX.Prec_gt_0 in Hprec.
+ unfold Prec_lt_emax in Hemax.
+ lia.
+Qed.
+
+Theorem do_overflow_iff:
+ forall m x,
+ let fexp := SpecFloat.fexp prec emax in
+ let rx := Generic_fmt.round Zaux.radix2 fexp (round_mode m) x in
+ do_overflow m x = true <-> (Raux.Rle_bool R_imax rx = true \/ Raux.Rle_bool rx (-R_imax)%R = true).
+Proof.
+ intros; split; intros.
+ - unfold do_overflow in H.
+ unfold Rabs in H.
+ destruct Rcase_abs.
+ + apply Rleb_Rle in H.
+ right. apply Raux.Rle_bool_true.
+ apply Ropp_le_contravar in H.
+ replace (rx) with (--rx)%R by lra.
+ subst rx; auto.
+ + apply Rleb_Rle in H.
+ left. apply Raux.Rle_bool_true.
+ auto.
+ - destruct H; apply Raux.Rle_bool_true; apply Rleb_Rle in H.
+ + eauto using Rle_trans, H, Rle_abs.
+ + apply Ropp_le_contravar in H.
+ replace (--R_imax)%R with R_imax in H by lra.
+ pose proof R_imax_gt_0.
+ assert (0 <= -rx)%R by lra.
+ assert (0 > rx)%R by lra.
+ assert (-rx > rx)%R by lra.
+ assert (Rabs rx = - rx)%R by auto using Rabs_left.
+ rewrite <- H4 in H.
+ auto.
+Qed.
+
+Lemma overflow_is_le :
+ forall m r1 r2,
+ (r1 <= r2)%R ->
+ (0 <= r1)%R ->
+ do_overflow m r1 = true ->
+ do_overflow m r2 = true.
+Proof.
+ intros m r1 r2 Hle Hr1 Ho.
+ rewrite do_overflow_iff in Ho. destruct Ho as [H | H].
+ - apply Rleb_Rle in H.
+ rewrite do_overflow_iff. left.
+ apply Raux.Rle_bool_true.
+ eapply Generic_fmt.round_le in Hle.
+ + eapply Rle_trans; [apply H | apply Hle].
+ + now apply fexp_correct.
+ + intuition.
+ - apply Rleb_Rle in H.
+ assert (-R_imax < 0)%R.
+ { assert (R_imax > 0)%R by apply R_imax_gt_0. lra. }
+ pose proof H0.
+ apply Rlt_le in H1.
+ eapply Generic_fmt.round_le in Hr1.
+ + erewrite Generic_fmt.round_0 in Hr1.
+ assert (0 < 0)%R.
+ eapply Rle_lt_trans.
+ apply Hr1.
+ eapply Rle_lt_trans.
+ apply H.
+ apply H0.
+ lra.
+ intuition.
+ + now apply fexp_correct.
+ + intuition.
+Qed.
+
+Lemma overflow_is_ge :
+ forall m r1 r2,
+ (r1 <= r2)%R ->
+ (r2 <= 0)%R ->
+ do_overflow m r2 = true ->
+ do_overflow m r1 = true.
+Proof.
+ intros m r1 r2 Hle Hr1 Ho.
+ rewrite do_overflow_iff in Ho. destruct Ho as [H | H].
+ - apply Rleb_Rle in H.
+ rewrite <- (round_Rimax m) in H.
+ eapply (Generic_fmt.round_le Zaux.radix2 fexp (round_mode m)) in Hr1; intuition.
+ rewrite Generic_fmt.round_0 in Hr1.
+ assert (Generic_fmt.round Zaux.radix2 fexp (round_mode m) R_imax <= 0)%R.
+ + eapply Rle_trans.
+ * apply H.
+ * apply Hr1.
+ + pose proof R_imax_gt_0.
+ rewrite (round_Rimax m) in H0.
+ lra.
+ + intuition.
+ - apply Rleb_Rle in H.
+ rewrite do_overflow_iff. right.
+ apply Raux.Rle_bool_true.
+ apply (Generic_fmt.round_le Zaux.radix2 fexp (round_mode m)) in Hle.
+ eapply Rle_trans.
+ + apply Hle.
+ + apply H.
+Qed.
+
+Lemma round_0:
+ forall m,
+ Real 0 = round m (Real 0).
+Proof.
+ intros m.
+ unfold round.
+ assert (H: do_overflow m 0 = false).
+ { unfold do_overflow, R_imax.
+ rewrite Generic_fmt.round_0 by fformat.
+ rewrite Rabs_R0.
+ apply Raux.Rle_bool_false.
+ apply Raux.bpow_gt_0.
+ }
+ rewrite H.
+ now rewrite Generic_fmt.round_0 by fformat.
+Qed.
+
+Theorem round_le:
+ forall (m : mode) (r1 r2 : Rx), leb r1 r2 = true -> leb (round m r1) (round m r2) = true.
+Proof.
+ intros m [ r1 | [] ] [r2 | []] H; try easy.
+ Ltac fbounded :=
+ match goal with
+ | [ Ho1 : do_overflow _ _ = false |- _ ] =>
+ apply Raux.Rle_bool_true;
+ destruct (dont_overflow_inv _ _ Ho1) as (f & [?Hreq ?Hf]);
+ rewrite ?Hreq; first [now apply Bleb_Rle, F_fmax_min | now apply Bleb_Rle, F_fmax_max ]
+ end.
+ Ltac freals :=
+ match goal with
+ | [ H : Raux.Rle_bool _ _ = true |- _ ] =>
+ apply Raux.Rle_bool_true; apply Rleb_Rle in H;
+ now apply Generic_fmt.round_le; fformat
+ end.
+ Ltac finfinites :=
+ simpl; now destruct overflow_to_inf eqn:?, do_overflow eqn:?, sign eqn:?.
+ Ltac absurd_sign :=
+ match goal with
+ | [ Hs2 : sign _ = true, Hs1 : sign _ = false, H : Raux.Rle_bool _ _ = true |- _ ] =>
+ now rewrite (pos_Rleb_neg _ _ Hs1 Hs2) in H
+ end.
+ Ltac absurd_mode :=
+ match goal with
+ | [ m : mode |- _] => now destruct m
+ end.
+ Ltac absurd_overflow :=
+ match goal with
+ | [ H : Raux.Rle_bool _ _ = true,
+ Hs : sign _ = false,
+ Ho1 : do_overflow _ _ = true,
+ Ho2 : do_overflow _ _ = false
+ |- _
+ ] => apply Rleb_Rle in H; now rewrite (overflow_is_le _ H (sign_pos_inv _ Hs) Ho1) in Ho2
+ | [ H : Raux.Rle_bool _ _ = true,
+ Hs : sign _ = true,
+ Ho1 : do_overflow _ _ = false,
+ Ho2 : do_overflow _ _ = true
+ |- _
+ ] => apply Rleb_Rle in H; now rewrite (overflow_is_ge _ H (sign_neg_inv _ Hs) Ho2) in Ho1
+ | [ H : Raux.Rle_bool _ _ = false,
+ Hs : sign _ = true,
+ Ho1 : do_overflow _ _ = true,
+ Ho2 : do_overflow _ _ = false
+ |- _
+ ] => apply Rleb_Rle in H; now rewrite (overflow_is_ge _ H (sign_neg_inv _ Hs) Ho2) in Ho1
+ | [ H1 : overflow_to_inf _ _ = true, H2 : overflow_to_inf _ _ = false |- _ ] =>
+ now rewrite H1 in H2
+ end.
+ Ltac absurd_case :=
+ match goal with
+ | [r1 : R, r2 : R |- _ ] =>
+ try absurd_mode; try absurd_sign; absurd_overflow
+ end.
+ Ltac sign_analysis :=
+ match goal with
+ | [r1 : R, r2 : R |- _ ] =>
+ destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; auto
+ end.
+ - simpl in H. unfold round.
+ destruct (do_overflow m r1) eqn:Ho1;
+ destruct (do_overflow m r2) eqn:Ho2;
+ destruct (overflow_to_inf m (sign r1)) eqn:Hi1;
+ destruct (overflow_to_inf m (sign r2)) eqn:Hi2;
+ (try freals); sign_analysis; try absurd_case; try fbounded ; simpl.
+ + unfold Raux.Rle_bool.
+ destruct Raux.Rcompare eqn:E; try easy.
+ apply Raux.Rcompare_Gt_inv in E; lra.
+ + unfold Raux.Rle_bool.
+ destruct Raux.Rcompare eqn:E; try easy.
+ apply Raux.Rcompare_Gt_inv in E.
+ unfold Defs.F2R in E; simpl in E.
+ apply Rmult_lt_reg_r in E.
+ * apply lt_IZR in E; lia.
+ * apply Raux.bpow_gt_0.
+ + unfold Raux.Rle_bool.
+ destruct Raux.Rcompare eqn:E; try easy.
+ apply Raux.Rcompare_Gt_inv in E; lra.
+ (* + apply Raux.Rle_bool_true.
+ apply do_overflow_false in Ho2.
+ unfold dont_overflow in Ho2.
+ apply Rltb_Rlt in Ho2.
+ apply Raux.Rabs_lt_inv in Ho2.
+ destruct Ho2 as [Ho2 Ho2'].
+ Search ()
+ assert (- R_imax)
+ assert (R_imax < (Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax)
+ (round_mode m) r2))%R.
+
+ unfold R_imax in Ho2.
+
+ destruct (dont_overflow_inv _ _ Ho2) as (f & [?Hreq ?Hf]).
+ unfold Generic_fmt.round, Defs.F2R; simpl.
+ Raux.bpow_simplify.
+ unfold FLX.Prec_gt_0 in Hprec.
+ unfold Prec_lt_emax in Hemax.
+ rewrite <- Raux.IZR_Zpower by lia.
+ rewrite <- mult_IZR.
+ rewrite <- Raux.IZR_Zpower.
+ unfold Generic_fmt.cexp.
+ rewrite <- mult_IZR.
+ apply IZR_le.
+ rewrite Hreq.
+ unfold Generic_fmt.round. apply F2R_congr. *)
+ - finfinites.
+Qed.
+
+Lemma round_inf :
+ forall m b, round m (Inf b) = Inf b.
+Proof. reflexivity. Qed.
+
+
+Example leb_infp_true :
+ forall x, leb x (Inf false) = true.
+Proof. now induction x as [ | [ ] ]. Qed.
+
+Example leb_infm_true :
+ forall x, leb (Inf true) x = true.
+Proof. now induction x as [ | [ ] ]. Qed.
+
+Example leb_real :
+ forall r1 r2, leb (Real r1) (Real r2) = Raux.Rle_bool r1 r2.
+Proof. reflexivity. Qed.
+
+Example leb_refl :
+ forall x, leb x x = true.
+Proof.
+ induction x as [ | [ ] ]; auto.
+ apply Raux.Rle_bool_true; lra.
+Qed.
+
+Definition add (x y : Rx) : Rx :=
+ match x with
+ | Inf true => x
+ | Inf false =>
+ match y with
+ | Inf true => Inf true
+ | _ => x
+ end
+ | Real r =>
+ match y with
+ | Inf _ => y
+ | Real r' => Real (r + r')%R
+ end
+ end.
+
+Lemma leb_trans :
+ forall x y z : Rx, leb x y = true -> leb y z = true -> leb x z = true.
+Proof.
+ intros [ rx | [ ] ] [ ry | [ ] ] [ rz | [ ] ] Hxy Hyz; simpl in *; try easy.
+ apply Rleb_Rle in Hxy.
+ apply Rleb_Rle in Hyz.
+ apply Raux.Rle_bool_true.
+ lra.
+Qed.
+
+Lemma add_leb_mono_l :
+ forall x y z : Rx,
+ leb x y = true -> leb (add x z) (add y z) = true.
+Proof.
+ intros [ ] [ ] [ ] H.
+ - simpl in *.
+ apply Rleb_Rle in H.
+ apply Raux.Rle_bool_true.
+ lra.
+ - now destruct b.
+ - now destruct b.
+ - now destruct b, b0.
+ - now destruct b.
+ - now destruct b, b0.
+ - now destruct b, b0.
+ - now destruct b, b0, b1.
+Qed.
+
+Lemma add_leb_mono_r :
+ forall x y z : Rx,
+ leb x y = true -> leb (add z x) (add z y) = true.
+Proof.
+ intros [ | [ ]] [ | [ ]] [ | [ ]] H; try easy.
+ simpl in *.
+ apply Rleb_Rle in H.
+ apply Raux.Rle_bool_true.
+ lra.
+Qed.
+
+Lemma add_real :
+ forall (r1 r2 : R), add (Real r1) (Real r2) = Real (r1 + r2)%R.
+Proof. reflexivity. Qed.
+
+Lemma add_0_l:
+ forall r : Rx, add (Real 0) r = r.
+Proof. destruct r; simpl; intuition. Qed.
+
+Lemma add_0_r:
+ forall r : Rx, add r (Real 0) = r.
+Proof. destruct r; try destruct b; simpl; intuition. Qed.
+
+Definition B2Rx (x : float) :=
+ match x with
+ | B754_infinity b => Inf b
+ | _ => Real (B2R x)
+ end.
+
+
+Lemma B2Rx_finite :
+ forall (f : float),
+ is_finite f = true -> B2Rx f = Real (B2R f).
+Proof. now destruct f. Qed.
+
+Lemma bounded_dont_overflow :
+ forall mode s m e (H : SpecFloat.bounded prec emax m e = true),
+ dont_overflow mode (B2R (B754_finite s m e H)) = true.
+Proof.
+ intros.
+ unfold dont_overflow.
+ apply Raux.Rlt_bool_true.
+ apply Raux.Rabs_lt; split.
+ + rewrite Generic_fmt.round_generic by (intuition; apply generic_format_B2R).
+ rewrite <- Ropp_involutive.
+ apply Ropp_lt_contravar.
+ rewrite <- B2R_Bopp; simpl (Bopp _).
+ apply (Rle_lt_trans _ R_fmax).
+ - rewrite R2F_fmax. auto using Bleb_Rle, F_fmax_max.
+ - apply Rimax_Rfmax.
+ + rewrite Generic_fmt.round_generic by (intuition; apply generic_format_B2R).
+ apply (Rle_lt_trans _ R_fmax).
+ - rewrite R2F_fmax. auto using Bleb_Rle, F_fmax_max.
+ - apply Rimax_Rfmax.
+Qed.
+
+Lemma round_id :
+ forall m (f : float),
+ B2Rx f = round m (B2Rx f).
+Proof.
+ intros m; destruct f as [ [ ] | [ ] | | ]; try easy.
+ + simpl (B2Rx _); apply round_0.
+ + simpl (B2Rx _); apply round_0.
+ + simpl (B2Rx _); apply round_0.
+ + unfold B2Rx, round.
+ rewrite (dont_overflow_true _ _ (bounded_dont_overflow m s m0 e e0)).
+ now rewrite Generic_fmt.round_generic by (intuition; apply generic_format_B2R).
+Qed.
+
+Lemma B2Rx_le :
+ forall (x y : float),
+ is_nan x = false ->
+ is_nan y = false ->
+ leb (B2Rx x) (B2Rx y) = true ->
+ Bleb x y = true.
+Proof.
+ intros.
+ destruct x as [[ ] | [ ] | | ] eqn:E1; destruct y as [ [ ] | [ ] | | ] eqn:E2; try easy;
+ rewrite <- E1, <- E2 in *;
+ rewrite B2Rx_finite in H1 by (rewrite E1; auto);
+ rewrite B2Rx_finite in H1 by (rewrite E2; auto);
+ unfold leb in H1;
+ unfold Bleb, SpecFloat.SFleb;
+ replace (SpecFloat.SFcompare (B2SF x) (B2SF y)) with (Bcompare x y) by auto;
+ assert (Fx: is_finite x = true) by (rewrite E1; auto);
+ assert (Fy: is_finite y = true) by (rewrite E2; auto);
+ rewrite (Bcompare_correct _ _ x y Fx Fy);
+ destruct Raux.Rcompare eqn:E; auto;
+ apply Raux.Rcompare_Gt_inv in E;
+ destruct (Raux.Rle_bool_spec (B2R x) (B2R y)); auto; lra.
+Qed.
+
+Ltac fdestruct f :=
+ destruct f as [ [ ] | [ ] | | ] eqn:?E; try easy.
+
+Lemma B2Rx_B2R :
+ forall (x : float),
+ is_finite x = true ->
+ B2Rx x = Real (B2R x).
+Proof. now intros [ ] Fx. Qed.
+
+Lemma le_B2Rx :
+ forall (x y : float),
+ Bleb x y = true ->
+ leb (B2Rx x) (B2Rx y) = true.
+Proof.
+ Ltac by_comparison :=
+ match goal with
+ | [ x : _, y : _, E : _, E0 : _, H : _ |- _ ] =>
+ rewrite <- E, <- E0 in H;
+ unfold Bleb, SpecFloat.SFleb in H;
+ replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in H by auto;
+ rewrite E, E0 in *;
+ rewrite Bcompare_correct in H by auto;
+ rewrite B2Rx_B2R by auto;
+ rewrite B2Rx_B2R, leb_real by auto;
+ destruct (Raux.Rcompare _) eqn:Cmp in H; try easy;
+ [ apply Raux.Rcompare_Eq_inv in Cmp | apply Raux.Rcompare_Lt_inv in Cmp ];
+ apply Raux.Rle_bool_true; lra
+ end.
+ Ltac by_computation :=
+ simpl; apply Raux.Rle_bool_true; lra.
+ intros.
+ fdestruct x; fdestruct y; try by_computation; by_comparison.
+Qed.
+
+End Rextended.
+
+Arguments round {prec} {emax} {Hprec} {Hemax}.
+Arguments round_le {prec} {emax} {Hprec} {Hemax}.
+Arguments B2Rx {prec} {emax}.
+Arguments B2Rx_le {prec} {emax}.
+Arguments le_B2Rx {prec} {emax}.
+Arguments B2Rx_B2R {prec} {emax}.
+Arguments B2Rx_finite {prec} {emax}.
diff --git a/farith2/thry/Tactics.v b/farith2/thry/Tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..6a95779372fa1e22c3eed41a0383170da8068328
--- /dev/null
+++ b/farith2/thry/Tactics.v
@@ -0,0 +1,2 @@
+From Flocq Require Import IEEE754.BinarySingleNaN.
+From Coq Require Import QArith Psatz Reals.
diff --git a/farith2/thry/Utils.v b/farith2/thry/Utils.v
new file mode 100644
index 0000000000000000000000000000000000000000..91aacfaee541db10fbfdc9ead83e73897b324513
--- /dev/null
+++ b/farith2/thry/Utils.v
@@ -0,0 +1,705 @@
+From Flocq Require Import IEEE754.BinarySingleNaN.
+From Coq Require Import ZArith Lia Reals Psatz Bool.
+(* From F Require Import Rextended. *)
+
+(**
+ Usefull facts & definitions about R
+*)
+Section Rutils.
+
+Definition sign (r : R) :=
+ Raux.Rlt_bool r 0.
+
+Lemma sign_pos_inv :
+ forall r, sign r = false -> (0 <= r)%R.
+Proof.
+ intros.
+ unfold sign in H.
+ now destruct (Raux.Rlt_bool_spec r 0).
+Qed.
+
+Lemma sign_neg_inv :
+ forall r, sign r = true -> (r <= 0)%R.
+Proof.
+ intros.
+ unfold sign in H. left.
+ now destruct (Raux.Rlt_bool_spec r 0).
+Qed.
+
+Lemma sign_neg_inv_strict:
+ forall r, sign r = true -> (r < 0)%R.
+Proof.
+ intros.
+ unfold sign in H.
+ now destruct (Raux.Rlt_bool_spec r 0).
+Qed.
+
+Lemma minus_pos_lt :
+ forall r1 r2, (0 < r2)%R -> (r1 - r2 < r1)%R.
+Proof.
+ intros; lra.
+Qed.
+
+Lemma IZR_neg :
+ (forall x, IZR (Z.neg x) < 0)%R.
+Proof.
+ induction x; try lra;
+ apply (Rgt_trans _ (IZR (Z.neg x))); auto;
+ apply IZR_lt; lia.
+Qed.
+
+Lemma IZR_pos :
+ (forall x, IZR (Z.pos x) > 0)%R.
+Proof.
+ induction x; try lra;
+ apply (Rgt_trans _ (IZR (Z.pos x))); auto;
+ apply IZR_lt; lia.
+Qed.
+
+Lemma pos_Rleb_neg :
+ forall r1 r2,
+ sign r1 = false ->
+ sign r2 = true ->
+ Raux.Rle_bool r1 r2 = false.
+Proof.
+ intros. unfold sign in *.
+ destruct (Raux.Rlt_bool_spec r1 0); try easy.
+ destruct (Raux.Rlt_bool_spec r2 0); try easy.
+ apply Raux.Rle_bool_false; lra.
+Qed.
+
+Lemma Rleb_Rle :
+ forall r1 r2, Raux.Rle_bool r1 r2 = true -> (r1 <= r2)%R.
+Proof.
+ intros.
+ now destruct (Raux.Rle_bool_spec r1 r2).
+Qed.
+
+Lemma Reqb_Req :
+ forall r1 r2, Raux.Req_bool r1 r2 = true -> (r1 = r2)%R.
+Proof.
+ intros.
+ now destruct (Raux.Req_bool_spec r1 r2).
+Qed.
+
+Lemma Rltb_Rlt :
+ forall r1 r2, Raux.Rlt_bool r1 r2 = true -> (r1 < r2)%R.
+Proof.
+ intros.
+ now destruct (Raux.Rlt_bool_spec r1 r2).
+Qed.
+
+Lemma Rsign_split :
+ forall (r : R), (r < 0 \/ r = 0 \/ r > 0)%R.
+Proof.
+ intros. lra.
+Qed.
+
+End Rutils.
+
+(*********************************************************
+ Simple & usefull results on floats
+**********************************************************)
+
+#[global] Notation "x <= y" := (Bleb x y = true).
+#[global] Notation "x <= y <= z" := (Bleb x y = true /\ Bleb y z = true).
+#[global] Notation "'+oo'" := (B754_infinity false).
+#[global] Notation "'-oo'" := (B754_infinity true).
+#[global] Notation "'NaN'" := (B754_nan).
+
+Ltac fdestruct f :=
+ destruct f as [ [ ] | [ ] | | ]; try easy.
+
+Section Utils.
+
+Variable prec : Z.
+Variable emax : Z.
+Context (Hprec : FLX.Prec_gt_0 prec).
+Context (Hemax : Prec_lt_emax prec emax).
+
+Definition float := binary_float prec emax.
+
+Definition is_inf (x : float) :=
+ match x with
+ | B754_infinity _ => true
+ | _ => false
+ end.
+
+Definition is_infp (x : float) :=
+ match x with
+ | B754_infinity s => negb s
+ | _ => false
+ end.
+
+Definition is_infm (x : float) :=
+ match x with
+ | B754_infinity s => s
+ | _ => false
+ end.
+
+Lemma le_not_nan :
+ forall x y : float, Bleb x y = true -> is_nan x = false /\ is_nan y = false.
+Proof. now intros [ ] [ ]. Qed.
+
+Lemma le_not_nan_l :
+ forall x y : float, Bleb x y = true -> is_nan x = false.
+Proof.
+ intros.
+ exact (proj1 (le_not_nan x y H)).
+Qed.
+
+Lemma le_not_nan_r :
+ forall x y : float, Bleb x y = true -> is_nan y = false.
+Proof.
+ intros.
+ exact (proj2 (le_not_nan x y H)).
+Qed.
+
+Lemma infm_min :
+ forall (x : float), is_nan x = false -> -oo <= x.
+Proof. fdestruct x. Qed.
+
+Lemma infp_max :
+ forall (x : float), is_nan x = false -> x <= +oo.
+Proof. fdestruct x. Qed.
+
+Lemma infp_le_is_infp :
+ forall x : float, +oo <= x -> x = +oo.
+Proof.
+ now intros [ [ ] | [ ] | | ] H.
+Qed.
+
+Lemma le_infm_is_infm :
+ forall x : float, x <= -oo -> x = -oo.
+Proof.
+ now intros [ [ ] | [ ] | | ] H.
+Qed.
+
+Lemma is_infm_inv:
+ forall x : float, is_infm x = true -> x = -oo.
+Proof. now intros [ [ ] | [ ] | | ]. Qed.
+
+Lemma is_infp_inv:
+ forall x : float, is_infp x = true -> x = +oo.
+Proof. now intros [ [ ] | [ ] | | ]. Qed.
+
+Lemma is_nan_inv:
+ forall x : float, is_nan x = true -> x = NaN.
+Proof. now intros [ ]. Qed.
+
+Lemma le_infp_finite:
+ forall x : float, is_finite x = true -> +oo <= x -> False.
+Proof. now intros [ ]. Qed.
+
+Lemma le_infm_finite:
+ forall x : float, is_finite x = true -> x <= -oo -> False.
+Proof. now intros [ ]. Qed.
+
+Lemma Bplus_finites_not_nan :
+ forall m (x y : float),
+ is_finite x = true ->
+ is_finite y = true ->
+ is_nan (Bplus m x y) = false.
+Proof.
+ intros m [[ ] | [ ] | | ] [ [ ] | [ ] | | ] Fx Fy; try easy.
+ - now destruct m.
+ - now destruct m.
+ - unfold Bplus.
+ auto using (is_nan_binary_normalize prec emax).
+Qed.
+
+Lemma Bplus_nan_inv :
+ forall (m : mode) (x y:float), is_nan (Bplus m x y) = true ->
+ x = +oo /\ y = -oo \/ x = -oo /\ y = +oo \/ x = NaN \/ y = NaN.
+Proof.
+ intros; fdestruct x; fdestruct y; auto.
+ - now destruct m.
+ - now destruct m.
+ - now rewrite Bplus_finites_not_nan in H.
+Qed.
+
+Lemma Bplus_not_nan_inv :
+ forall (m : mode) (x y:float), is_nan (Bplus m x y) = false ->
+ ~(x = +oo /\ y = -oo) /\ ~(x = -oo /\ y = +oo) /\ (is_nan x = false) /\ (is_nan y = false).
+Proof.
+ intros; repeat split; fdestruct x; fdestruct y.
+Qed.
+
+(* Lemma Bplus_nan_if :
+ forall m (x y : float),
+ is_nan x = false ->
+ is_nan y = false ->
+ is_nan (Bplus m x y) = true ->
+ (x = +oo /\ y = -oo) \/ (x = -oo /\ y = +oo).
+Proof.
+ intros.
+ fdestruct x; fdestruct y; try now destruct m; intuition.
+ assert (is_nan (Bplus m (B754_finite s m0 e e0) (B754_finite s0 m1 e1 e2)) = false) by auto using Bplus_finites_not_nan.
+ rewrite H1 in H2; discriminate.
+Qed. *)
+
+Lemma Bplus_zero :
+ forall m b (x : float),
+ B2R (Bplus m (B754_zero b) x) = B2R x.
+Proof.
+ intros ? [ ] [ [ ] | [ ] | | ]; try easy.
+ - simpl; destruct m; reflexivity.
+ - simpl; destruct m; reflexivity.
+Qed.
+
+Lemma pos_Bopp_neg :
+ forall m e Hb, @B754_finite prec emax true m e Hb = Bopp (B754_finite false m e Hb).
+Proof. reflexivity. Qed.
+
+Lemma neg_Bopp_pos :
+ forall m e Hb, @B754_finite prec emax false m e Hb = Bopp (B754_finite true m e Hb).
+Proof. reflexivity. Qed.
+
+Lemma Rle_Bleb :
+ forall (x y : float),
+ is_finite x = true ->
+ is_finite y = true ->
+ (B2R x <= B2R y)%R ->
+ Bleb x y = true.
+Proof.
+ intros x y Fx Fy Hxy.
+ unfold Bleb, SpecFloat.SFleb.
+ replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
+ rewrite (Bcompare_correct _ _ x y Fx Fy).
+ destruct Raux.Rcompare eqn:E; try easy.
+ apply Raux.Rcompare_Gt_inv in E; lra.
+Qed.
+
+Lemma Rlt_Bltb :
+ forall (x y : float),
+ is_finite x = true ->
+ is_finite y = true ->
+ (B2R x < B2R y)%R ->
+ Bltb x y = true.
+Proof.
+ intros x y Fx Fy Hxy.
+ unfold Bltb, SpecFloat.SFltb.
+ replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
+ rewrite (Bcompare_correct _ _ x y Fx Fy).
+ destruct Raux.Rcompare eqn:E; auto.
+ - apply Raux.Rcompare_Eq_inv in E; lra.
+ - apply Raux.Rcompare_Gt_inv in E; lra.
+Qed.
+
+Lemma Bleb_Rle :
+ forall x y : float, is_finite x = true -> is_finite y = true ->
+ Bleb x y = true -> (B2R x <= B2R y)%R.
+Proof.
+ intros x y Fx Fy H.
+ unfold Bleb, SpecFloat.SFleb in H.
+ replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) in H by auto.
+ rewrite (Bcompare_correct _ _ x y Fx Fy) in H.
+ destruct (Raux.Rcompare) eqn:E in H; try easy.
+ + apply Raux.Rcompare_Eq_inv in E; lra.
+ + apply Raux.Rcompare_Lt_inv in E; lra.
+Qed.
+
+Lemma Bltb_Rlt :
+ forall x y : float, is_finite x = true -> is_finite y = true ->
+ Bltb x y = true -> (B2R x < B2R y)%R.
+Proof.
+ intros x y Fx Fy H.
+ unfold Bltb, SpecFloat.SFltb in H.
+ replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) in H by auto.
+ rewrite (Bcompare_correct _ _ x y Fx Fy) in H.
+ destruct (Raux.Rcompare) eqn:E in H; try easy.
+ apply Raux.Rcompare_Lt_inv in E; lra.
+Qed.
+
+Lemma Bleb_trans :
+ forall (x y z : float), x <= y -> y <= z -> x <= z.
+Proof.
+ intros x y z Hxy Hyz.
+ fdestruct x; fdestruct y; fdestruct z;
+ apply Rle_Bleb; auto;
+ apply Bleb_Rle in Hxy; auto;
+ apply Bleb_Rle in Hyz; auto;
+ lra.
+Qed.
+
+Lemma Bltb_trans :
+ forall (x y z : float), Bltb x y = true -> Bltb y z = true -> Bltb x z = true.
+Proof.
+ intros x y z Hxy Hyz.
+ fdestruct x; fdestruct y; fdestruct z;
+ apply Rlt_Bltb; auto;
+ apply Bltb_Rlt in Hxy; auto;
+ apply Bltb_Rlt in Hyz; auto;
+ lra.
+Qed.
+
+Lemma Bltb_Bleb_trans :
+ forall x y z : float, Bltb x y = true -> y <= z -> Bltb x z = true.
+Proof.
+ intros x y z Hxy Hyz.
+ fdestruct x; fdestruct y; fdestruct z;
+ apply Rlt_Bltb; auto;
+ apply Bltb_Rlt in Hxy; auto;
+ apply Bleb_Rle in Hyz; auto;
+ lra.
+Qed.
+
+Lemma Bleb_Bltb_trans :
+ forall x y z : float, Bleb x y = true -> Bltb y z = true -> Bltb x z = true.
+Proof.
+ intros x y z Hxy Hyz.
+ fdestruct x; fdestruct y; fdestruct z;
+ apply Rlt_Bltb; auto;
+ apply Bleb_Rle in Hxy; auto;
+ apply Bltb_Rlt in Hyz; auto;
+ lra.
+Qed.
+
+Lemma Beqb_refl :
+ forall x : float, is_nan x = false -> Beqb x x = true.
+Proof.
+ intros; fdestruct x.
+ unfold Beqb; cbn.
+ destruct s;
+ rewrite (Zaux.Zcompare_Eq e e) by reflexivity;
+ now rewrite (Pcompare_refl m).
+Qed.
+
+Lemma Beqb_nan_l :
+ forall (x : float), Beqb NaN x = false.
+Proof. fdestruct x. Qed.
+
+Lemma Beqb_nan_r :
+ forall (x : float), Beqb x NaN = false.
+Proof. fdestruct x. Qed.
+
+Lemma Beqb_Bleb :
+ forall x y : float, Beqb x y = true -> Bleb x y = true.
+Proof.
+ intros x y Hxy.
+ fdestruct x; fdestruct y; rewrite Beqb_correct in Hxy; auto;
+ apply Rle_Bleb; auto; right;
+ now apply Reqb_Req in Hxy.
+Qed.
+
+
+Lemma Bleb_refl :
+ forall x:float, is_nan x = false -> Bleb x x = true.
+Proof.
+ intros x Hx; fdestruct x.
+ apply Rle_Bleb; auto; lra.
+Qed.
+
+Lemma Bltb_Bleb :
+ forall x y : float, Bltb x y = true -> Bleb x y = true.
+Proof.
+ intros x y Hxy.
+ fdestruct x; fdestruct y;
+ apply Rle_Bleb; auto;
+ apply Bltb_Rlt in Hxy; auto;
+ lra.
+Qed.
+
+Axiom proof_irr :
+ forall m e (H H' : SpecFloat.bounded prec emax m e = true), H = H'.
+
+Lemma Bleb_antisymm_strict :
+ forall x y : float, x <= y <= x -> Beqb x (B754_zero true) = false -> x = y.
+Proof.
+ intros x y [H1 H2].
+ fdestruct x; fdestruct y;
+ try (destruct s; try easy);
+ try (destruct s0; try easy).
+ - intros _.
+ cbn in H1, H2.
+ destruct (e ?= e1)%Z eqn:E1; rewrite (Z.compare_antisym _ _), E1 in H2; simpl in H2; try discriminate.
+ rewrite <- ZC4 in H1.
+ destruct (Pos.compare_cont Eq m0 m) eqn:E2; try easy.
+ apply (Pcompare_Eq_eq _ _) in E2; subst.
+ apply (Z.compare_eq) in E1; subst; cbn.
+ rewrite (proof_irr _ _ e0 e2).
+ reflexivity.
+ - intros _.
+ cbn in H1, H2.
+ rewrite ZC4 in H2.
+ destruct (e1 ?= e)%Z eqn:E1; rewrite (Z.compare_antisym _ _), E1 in H1; simpl in H2; try discriminate.
+ destruct (Pos.compare_cont Eq m m0) eqn:E2; try easy.
+ + apply (Pcompare_Eq_eq _ _) in E2; subst.
+ apply (Z.compare_eq) in E1; subst; cbn.
+ rewrite (proof_irr _ _ e0 e2).
+ reflexivity.
+Qed.
+
+
+Lemma Bleb_antisymm :
+ forall x y : float, x <= y <= x -> Beqb x y = true.
+Proof.
+ intros x y [H1 H2].
+ fdestruct x; fdestruct y;
+ try (destruct s; try easy);
+ try (destruct s0; try easy).
+ - cbn in H1, H2.
+ destruct (e ?= e1)%Z eqn:E1; rewrite (Z.compare_antisym _ _), E1 in H2; simpl in H2; try discriminate.
+ rewrite <- ZC4 in H1.
+ destruct (Pos.compare_cont Eq m0 m) eqn:E2; try easy.
+ apply (Pcompare_Eq_eq _ _) in E2; subst.
+ apply (Z.compare_eq) in E1; subst; cbn.
+ now rewrite Z.compare_refl, Pcompare_refl.
+ - cbn in H1, H2.
+ destruct (e ?= e1)%Z eqn:E1; rewrite (Z.compare_antisym _ _), E1 in H2; simpl in H2; try discriminate.
+ destruct (Pos.compare_cont Eq m m0) eqn:E2; try easy.
+ + apply (Pcompare_Eq_eq) in E2; subst.
+ apply (Z.compare_eq) in E1; subst; cbn.
+ now rewrite Z.compare_refl, Pcompare_refl.
+ + destruct (Pos.compare_cont Eq m0 m) eqn:E3; try easy.
+ * apply Pos.compare_nge_iff in E2.
+ apply Pos.compare_eq_iff in E3.
+ intuition.
+ * apply Pos.compare_nge_iff in E2.
+ apply Pos.compare_nge_iff in E3.
+ intuition.
+Qed.
+
+Lemma Beqb_symm :
+ forall x y : float, Beqb x y = true -> Beqb y x = true.
+Proof.
+ intros x y Hxy.
+ fdestruct x; fdestruct y; unfold Beqb in Hxy; simpl in *; try (now destruct s).
+ unfold SpecFloat.SFeqb in Hxy; simpl in *.
+ destruct s, s0; auto.
+ * rewrite <- ZC4 in Hxy.
+ destruct (e ?= e1)%Z eqn:E1, (Pos.compare_cont Eq m0 m) eqn:E2; simpl in *; try discriminate.
+ rewrite Z.compare_eq_iff in E1; subst.
+ apply Pcompare_Eq_eq in E2; subst.
+ rewrite Beqb_correct; auto; simpl.
+ unfold Raux.Req_bool.
+ rewrite Raux.Rcompare_Eq; reflexivity.
+ * destruct (e ?= e1)%Z eqn:E1, (Pos.compare_cont Eq m m0) eqn:E2; simpl in *; try discriminate.
+ rewrite Z.compare_eq_iff in E1; subst.
+ apply Pcompare_Eq_eq in E2; subst.
+ rewrite Beqb_correct; auto; simpl.
+ unfold Raux.Req_bool.
+ rewrite Raux.Rcompare_Eq; reflexivity.
+Qed.
+
+Lemma Beqb_trans :
+ forall x y z : float, Beqb x y = true -> Beqb y z = true -> Beqb x z = true.
+Proof.
+ intros x y z H1 H2.
+ apply Bleb_antisymm; split.
+ - apply (Bleb_trans _ _ _ (Beqb_Bleb _ _ H1) (Beqb_Bleb _ _ H2)).
+ - apply (Bleb_trans _ _ _ (Beqb_Bleb _ _ (Beqb_symm _ _ H2)) (Beqb_Bleb _ _ (Beqb_symm _ _ H1))).
+Qed.
+
+Lemma Bleb_false_Bltb :
+ forall x y:float, is_nan x = false -> is_nan y = false -> Bleb x y = false -> Bltb y x = true.
+Proof.
+ intros x y Hx Hy Hxy.
+ destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
+ unfold Bleb, SpecFloat.SFleb in Hxy;
+ replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in Hxy by auto;
+ assert (Fx: is_finite x = true) by (rewrite Ex; auto);
+ assert (Fy: is_finite y = true) by (rewrite Ey; auto);
+ rewrite (Bcompare_correct _ _ x y Fx Fy) in Hxy; auto;
+ destruct (Raux.Rcompare _ _) eqn:E; try easy;
+ apply Raux.Rcompare_Gt_inv in E;
+ apply Rlt_Bltb; auto.
+Qed.
+
+Lemma Bltb_false_Bleb :
+ forall x y:float, is_nan x = false -> is_nan y = false -> Bltb x y = false -> Bleb y x = true.
+Proof.
+ intros x y Hx Hy Hxy.
+ destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
+ unfold Bltb, SpecFloat.SFltb in Hxy;
+ replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in Hxy by auto;
+ assert (Fx: is_finite x = true) by (rewrite Ex; auto);
+ assert (Fy: is_finite y = true) by (rewrite Ey; auto);
+ rewrite (Bcompare_correct _ _ x y Fx Fy) in Hxy; auto;
+ destruct (Raux.Rcompare _ _) eqn:E; try easy;
+ (apply Raux.Rcompare_Eq_inv in E || apply Raux.Rcompare_Gt_inv in E);
+ apply Rle_Bleb; auto; lra.
+Qed.
+
+Lemma Bltb_true_Bleb :
+ forall x y:float, is_nan x = false -> is_nan y = false -> Bltb x y = true -> Bleb y x = false.
+Proof.
+ intros x y Hx Hy Hxy.
+ destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
+ assert (Fx: is_finite x = true) by (rewrite Ex; auto);
+ assert (Fy: is_finite y = true) by (rewrite Ey; auto);
+ apply (Bltb_Rlt _ _ Fx Fy) in Hxy;
+ apply not_true_is_false; intros Hcontr;
+ apply (Bleb_Rle _ _ Fy Fx) in Hcontr;
+ lra.
+Qed.
+
+Lemma Bleb_true_Bltb :
+ forall x y:float, is_nan x = false -> is_nan y = false -> Bleb x y = true -> Bltb y x = false.
+Proof.
+ intros x y Hx Hy Hxy.
+ destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
+ assert (Fx: is_finite x = true) by (rewrite Ex; auto);
+ assert (Fy: is_finite y = true) by (rewrite Ey; auto);
+ apply (Bleb_Rle _ _ Fx Fy) in Hxy;
+ apply not_true_is_false; intros Hcontr;
+ apply (Bltb_Rlt _ _ Fy Fx) in Hcontr;
+ lra.
+Qed.
+
+Definition Bmax (f1 f2 : float) : float :=
+ if is_nan f1 || is_nan f2 then NaN
+ else if Bleb f1 f2 then f2
+ else f1.
+
+Definition Bmin (f1 f2 : float) : float :=
+ if is_nan f1 || is_nan f2 then NaN
+ else if Bleb f1 f2 then f1
+ else f2.
+
+Lemma Bmax_max_1 :
+ forall x y, (Bmax x y = x \/ Bmax x y = y).
+Proof.
+ intros [ ] [ ]; unfold Bmax; destruct Bleb; intuition.
+Qed.
+
+Lemma Bmax_max_2 :
+ forall x y, is_finite x = true -> is_finite y = true -> x <= Bmax x y /\ y <= Bmax x y.
+Proof.
+ intros x y Fx Fy; unfold Bmax.
+ assert (HnanX: is_nan x = false) by fdestruct x.
+ assert (HnanY: is_nan y = false) by fdestruct y.
+ rewrite HnanX, HnanY; simpl.
+ split.
+ - destruct (Bleb x y) eqn:?; auto.
+ apply Bleb_refl; fdestruct x.
+ - destruct (Bleb x y) eqn:E.
+ + apply Bleb_refl; fdestruct y.
+ + apply Bleb_false_Bltb in E; auto.
+ now apply Bltb_Bleb in E.
+Qed.
+
+Lemma Bmax_le :
+ forall x y z : float, x <= z -> y <= z -> Bmax x y <= z.
+Proof.
+ intros x y z Hxz Hyz.
+ assert (HnanX: is_nan x = false) by fdestruct x.
+ assert (HnanY: is_nan y = false) by fdestruct y.
+ unfold Bmax.
+ rewrite HnanX, HnanY; simpl.
+ now destruct (Bleb x y).
+Qed.
+
+Lemma Bmax_not_nan_inv :
+ forall x y, is_nan (Bmax x y) = false -> is_nan x = false /\ is_nan y = false.
+Proof.
+ intros; split.
+ + fdestruct x.
+ + fdestruct x; fdestruct y.
+Qed.
+
+Lemma Bmin_not_nan_inv :
+ forall x y, is_nan (Bmin x y) = false -> is_nan x = false /\ is_nan y = false.
+Proof.
+ intros; split.
+ + fdestruct x.
+ + fdestruct x; fdestruct y.
+Qed.
+
+Lemma Bmax_le_inv :
+ forall x y z : float, Bmax x y <= z -> x <= z /\ y <= z.
+Proof.
+ intros x y z Hxyz.
+ assert (is_nan (Bmax x y) = false) by (fdestruct (Bmax x y)).
+ unfold Bmax in Hxyz.
+ apply Bmax_not_nan_inv in H.
+ destruct H as [H1 H2].
+ rewrite H1, H2 in Hxyz.
+ simpl in *.
+ destruct (Bleb x y) eqn:E; split; auto.
+ - now apply (Bleb_trans x y z).
+ - apply Bleb_false_Bltb in E; auto.
+ apply Bltb_Bleb in E; auto.
+ now apply (Bleb_trans y x z).
+Qed.
+
+Lemma Bmin_min_1 :
+ forall x y, (Bmin x y = x \/ Bmin x y = y).
+Proof.
+ intros [ ] [ ]; unfold Bmin; destruct Bleb; intuition.
+Qed.
+
+Lemma Bmin_min_2 :
+ forall x y, is_finite x = true -> is_finite y = true -> Bmin x y <= x /\ Bmin x y <= y.
+Proof.
+ intros x y Fx Fy; unfold Bmin.
+ assert (HnanX: is_nan x = false) by fdestruct x.
+ assert (HnanY: is_nan y = false) by fdestruct y.
+ rewrite HnanX, HnanY; simpl.
+ split.
+ - destruct (Bleb x y) eqn:?.
+ + apply Bleb_refl; fdestruct x.
+ + assert (Hx : is_nan x = false) by (fdestruct x).
+ assert (Hy : is_nan y = false) by (fdestruct y).
+ apply Bleb_false_Bltb in Heqb; auto.
+ apply Bltb_Rlt in Heqb; auto.
+ apply Rle_Bleb; auto.
+ lra.
+ - destruct (Bleb x y) eqn:E; auto.
+ apply Bleb_refl; fdestruct y.
+Qed.
+
+Lemma Bmin_le :
+ forall x y z : float, z <= x -> z <= y -> z <= Bmin x y.
+Proof.
+ intros x y z Hxz Hyz.
+ assert (HnanX: is_nan x = false) by (fdestruct z; fdestruct x).
+ assert (HnanY: is_nan y = false) by (fdestruct z; fdestruct y).
+ unfold Bmin.
+ rewrite HnanX, HnanY; simpl.
+ now destruct (Bleb x y).
+Qed.
+
+Lemma Bmin_le_inv :
+ forall x y z : float, z <= Bmin x y -> z <= x /\ z <= y.
+Proof.
+ intros x y z Hxyz.
+ assert (is_nan (Bmin x y) = false) by (fdestruct (Bmin x y); fdestruct z).
+ unfold Bmin in Hxyz.
+ apply Bmin_not_nan_inv in H.
+ destruct H as [H1 H2].
+ rewrite H1, H2 in Hxyz.
+ simpl in *.
+ destruct (Bleb x y) eqn:E; split; auto.
+ - now apply (Bleb_trans z x y).
+ - apply Bleb_false_Bltb in E; auto.
+ apply Bltb_Bleb in E.
+ now apply (Bleb_trans z y x).
+Qed.
+
+Lemma Bpred_not_nan :
+ forall (x : float), is_nan x = false -> is_nan (Bpred x) = false.
+Proof.
+ intros x <-.
+ apply is_nan_Bpred.
+Qed.
+
+End Utils.
+
+Arguments le_not_nan {prec} {emax}.
+Arguments le_not_nan_l {prec} {emax}.
+Arguments le_not_nan_r {prec} {emax}.
+Arguments is_nan_inv {prec} {emax}.
+Arguments is_infm {prec} {emax}.
+Arguments is_infp {prec} {emax}.
+Arguments is_inf {prec} {emax}.
+Arguments Bplus_not_nan_inv {prec} {emax} {Hprec} {Hemax}.
+Arguments Bplus_nan_inv {prec} {emax} {Hprec} {Hemax}.
+Arguments Bmin {prec} {emax}.
+Arguments Bmax {prec} {emax}.
+Arguments Bmax_max_1 {prec} {emax}.
+Arguments Bmax_max_2 {prec} {emax}.
+Arguments Bmin_min_1 {prec} {emax}.
+Arguments Bmin_min_2 {prec} {emax}.
+Arguments Bleb_trans {prec} {emax}.
+Arguments Bltb_Bleb_trans {prec} {emax}.
diff --git a/src_colibri2/tests/solve/smt_fp/sat/_head b/src_colibri2/tests/solve/smt_fp/sat/_head
new file mode 100644
index 0000000000000000000000000000000000000000..96c0283fac14b3394a77cd8dba745eadd3f18f88
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/_head
@@ -0,0 +1,2 @@
+\begin{figure}[h!]
+ \centering\begin{minted}{scheme}
diff --git a/src_colibri2/tests/solve/smt_fp/sat/_tail b/src_colibri2/tests/solve/smt_fp/sat/_tail
new file mode 100644
index 0000000000000000000000000000000000000000..026e1a6bee0be18ba149e5ad30b9f780a6868dce
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/_tail
@@ -0,0 +1,3 @@
+ \end{minted}
+ \caption{Incompatibilité de l'égalité flottante avec l'égalité usuelle}
+\end{figure}
diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
index 0a776eab81b6bd13f4f5a1c7a787873ac7be0bda..f0216026c8d36e97ea490cf09e2b42bc28de066b 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
@@ -17,9 +17,6 @@
--dont-print-result %{dep:recognize_float32.smt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_float32.smt2})))
(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat
---dont-print-result %{dep:recognize_float64.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_float64.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat
--dont-print-result %{dep:recognize_rounding_mode.smt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_rounding_mode.smt2})))
(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat
diff --git a/src_colibri2/tests/solve/smt_fp/sat/recognize_float64.smt2 b/src_colibri2/tests/solve/smt_fp/sat/recognize_float64.smt2
deleted file mode 100644
index 51b3b30b78cb09def79d66167969933518883501..0000000000000000000000000000000000000000
--- a/src_colibri2/tests/solve/smt_fp/sat/recognize_float64.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-(set-logic ALL)
-(declare-fun x () (_ FloatingPoint 11 53))
-(declare-fun y () (_ FloatingPoint 11 53))
-(assert (= x y))
-(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2 b/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
index f881999439bff2f9f5f5ca1f62afe46b6336c187..0dbb523e8e067bef2968c69f1c45f8fc3ed1f79d 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
+++ b/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
@@ -3,5 +3,5 @@
(declare-fun y () (_ FloatingPoint 8 24))
(declare-fun m () RoundingMode)
(assert (not (= RNE m)))
-(assert (= (fp.add m x y) x))
-(check-sat)
\ No newline at end of file
+(assert (fp.eq (fp.add m x y) x))
+(check-sat)
diff --git a/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
index 6f0a55c4ef55157052764d0a2b7c12ed868ede9b..3f47b356d83306c7cd6936488b9c0ac5fbac61cb 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
+++ b/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
@@ -1,5 +1,6 @@
(set-logic ALL)
(declare-fun x () (_ FloatingPoint 8 24))
(declare-fun y () (_ FloatingPoint 8 24))
-(assert (= (fp.add RNE x y) x))
-(check-sat)
\ No newline at end of file
+(assert (= (fp.add RNE (_ NaN 8 24) y) (_ NaN 8 24)))
+(assert (fp.eq (fp.add RNE x y) x))
+(check-sat)
diff --git a/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2
index e0e38f6736112c5a4924579cd4cfa9b4897845de..3fa2e8949b29f856d6533ffe93f1b2cf135bb910 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2
+++ b/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2
@@ -1,5 +1,6 @@
(set-logic ALL)
(declare-fun x () (_ FloatingPoint 8 24))
(declare-fun y () (_ FloatingPoint 8 24))
-(assert (= (fp.mul RNE x y) x))
-(check-sat)
\ No newline at end of file
+(assert (= (fp.mul RNE (_ NaN 8 24) y) (_ NaN 8 24)))
+(assert (fp.eq (fp.mul RNE x y) x))
+(check-sat)
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
index d6d0be9784a0b61dfd60878c8aed847242c0da22..5d8594119d983e5c74dfa5044d3723bcca6d6187 100644
--- a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
@@ -7,3 +7,6 @@
(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:nan_neq_float32.smt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat
+--dont-print-result %{dep:propagate_le_ge.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:propagate_le_ge.smt2})))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/propagate_le_ge.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/propagate_le_ge.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..67a89a5d33987285dc5e6d5fab567a4aef0aa4bd
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/propagate_le_ge.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x Float32)
+(assert (fp.leq x ((_ to_fp 8 24) RNE 1.0)))
+(assert (fp.geq x ((_ to_fp 8 24) RNE 3.0)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/theories/FP/dom_interval.ml b/src_colibri2/theories/FP/dom_interval.ml
index c95cbb4d8ba547900962adbc80c4d82ed78cdcb0..0551468dd3241f2e8e59170cfaa87cbcebd5edf2 100644
--- a/src_colibri2/theories/FP/dom_interval.ml
+++ b/src_colibri2/theories/FP/dom_interval.ml
@@ -20,261 +20,97 @@
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 floating points theory"
- "FP.interval"
+ ~desc:"for intervals for the arithmetic theory"
+ "FP.interval"
-module D = Colibri2_theories_LRA_stages.Interval_domain
+module D = Interval32
let dom = Dom.Kind.create (module struct type t = D.t let name = "FP_ARITH" end)
-let () = Dom.register(module struct
+include (Dom.Lattice(struct
include D
+ let equal (x : t) (y : t) = Stdlib.(=) x y
+ let pp fmt x = Format.fprintf fmt "%s" (D.to_string x)
let key = dom
- let merged i1 i2 =
- match i1, i2 with
- | None, None -> true
- | Some i1, Some i2 -> D.equal i1 i2
- | _ -> false
+ let inter _ d1 d2 = inter d1 d2
+ let is_singleton _ d =
+ Option.map (fun x -> Float32.nodevalue @@ Float32.index x) (D.is_singleton d)
+ end
+))
- let merge d (i1,cl1) (i2,cl2) _ =
- assert (not (Egraph.is_equal d cl1 cl2));
- match i1, cl1, i2, cl2 with
- | Some i1,_, Some i2,_ ->
- begin match D.inter i1 i2 with
- | None ->
- Debug.dprintf8 Debug.contradiction
- "[FP/Dom] The intersection of %a and %a is empty when merging %a and %a"
- D.pp i1 D.pp i2
- Node.pp cl1
- Node.pp cl2;
- Egraph.contradiction d
- | Some i ->
- if not (D.equal i i1) then
- Egraph.set_dom d dom cl1 i;
- if not (D.equal i i2) then
- Egraph.set_dom d dom cl2 i
- end
- | Some i1, _, _, cl2 | _, cl2, Some i1, _ ->
- Egraph.set_dom d dom cl2 i1
- | None,_,None,_ -> raise Impossible
- end)
-
-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
-
-let is_not_zero d n =
- match Egraph.get_dom d dom n with
- | None -> false
- | Some p -> D.absent Q.zero p
-
-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
-
-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
-
-let is_integer d n =
- match Egraph.get_dom d dom n with
- | None -> false
- | Some p -> D.is_integer p
-
-let set_dom d node v =
- match D.is_singleton v with
- | Some q ->
- let cst = Float32.cst' (Farith.B32.(of_q NE q)) in
- Egraph.set_value d node (Float32.nodevalue cst)
- | None ->
- (** the pexp must be in the dom *)
- Egraph.set_dom d dom node v
-
-
-module ChoLRA = struct
- let make_decision node v env =
- Debug.dprintf4 Debug.decision
- "[FP] decide %a on %a" D.pp v Node.pp node;
- set_dom env node v
-
- let choose_decision node env =
- let v = Opt.get_def D.reals (Egraph.get_dom env dom node) in
- match D.split_heuristic v with
- | Singleton _ -> Choice.DecNo
- | Splitted (v1,v2) ->
- DecTodo (List.map (make_decision node) (Shuffle.shufflel [v1;v2]))
- | NotSplitted ->
- DecTodo [make_decision node (D.singleton (D.choose v))]
-
- let choice n = {
- Choice.prio = 1;
- choice = choose_decision n;
- print_cho = "FP.Dom_interval.ChoLRA";
- }
-
-end
-
-let choice = ChoLRA.choice
-
-let upd_dom d n' v' =
- match Egraph.get_dom d dom n' with
- | None -> Egraph.set_dom d dom n' v'
- | Some old ->
- match D.inter old v' with
- | None ->
- Debug.dprintf6 Debug.contradiction
- "[FP/Dom] The intersection of %a with %a is empty when updating %a"
- D.pp old D.pp v'
- Node.pp n';
- Egraph.contradiction d
- | Some d' ->
- if not (D.equal old d')
- then Egraph.set_dom d dom n' d'
-
-module Monad : sig
- type 'a monad = Egraph.wt -> Node.t -> 'a
- val get: Node.t -> D.t option monad
- val set: Node.t -> D.t option monad -> unit monad
- val getb: Node.t -> bool option monad
- val setb: Node.t -> bool option option monad -> unit monad
- val (let+): 'b option monad -> ('b -> 'c) -> 'c option monad
- val (and+): 'b option monad -> 'c option monad -> ('b * 'c) option monad
- val (&&): unit monad -> unit monad -> unit monad
-end = struct
- type 'a monad = Egraph.wt -> Node.t -> 'a
- let [@ocaml.always inline] get_dom dom n' = fun d _ ->
- Egraph.get_dom d dom n'
- let [@ocaml.always inline] set_dom (type b) (dom:b Dom.Kind.t) n' v' d n =
- if Node.equal n n' then () else
- Option.iter
- (fun (v':b) -> Egraph.set_dom d dom n' v')
- (v' d n)
- let [@ocaml.always inline] set n' v' d n =
- if Node.equal n n' then () else
- Option.iter
- (fun v' -> upd_dom d n' v' )
- (v' d n)
- let [@ocaml.always inline] get a = get_dom dom a
- let [@ocaml.always inline] get_value key n' = fun d _ ->
- let open CCOpt in
- let* v = Egraph.get_value d n' in
- Value.value key v
- let [@ocaml.always inline] set_value (type b)
- (value:(module Value.S with type s = b))
- n' (v':b option option monad) : unit monad =
- fun d n ->
- if Node.equal n n' then () else
- let module V = (val value) in
- Option.iter
- (Option.iter (fun v' -> Egraph.set_value d n' (V.nodevalue (V.index v'))))
- (v' d n)
- let getb a = get_value Boolean.dom a
- let setb a = set_value (module Boolean.BoolValue) a
- let [@ocaml.always inline] (let+) a (f:'b -> 'a) = fun d n -> Option.map f (a d n)
- let [@ocaml.always inline] (and+) a b = fun d n -> match a d n, b d n with
- | Some a, Some b -> Some (a,b) | _ -> None
- let [@ocaml.always inline] (&&) a b = fun d n -> a d n; b d n
-
-end
-
-let neg_cmp = function
- | `Lt -> `Ge
- | `Le -> `Gt
- | `Ge -> `Lt
- | `Gt -> `Le
-
-let com_cmp = function
- | `Lt -> `Gt
- | `Le -> `Ge
- | `Ge -> `Le
- | `Gt -> `Lt
-
-let backward = function
- | `Lt -> D.lt'
- | `Gt -> D.gt'
- | `Le -> D.le'
- | `Ge -> D.ge'
+let (!<) e = function
+ | Some x -> x
+ | None -> Egraph.contradiction e
(** {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 cmp test cmp a b =
+ (* let setb = setv Boolean.dom in *)
+ let getb = getv Boolean.dom in
+ let set = updd upd_dom in
+ let get = getd dom in
+ let getm = getv Rounding_mode.key in
+ (* let fget x = CCOpt.get_exn_or "bad" (Egraph.get_dom d dom x) in *)
+ let propagate prop a b =
reg a; reg b;
- let wakeup =
- setb r (let+ va = get a and+ vb = get b in
- test (D.is_comparable va vb)) &&
- set b (let+ va = get a and+ vr = getb r in
- backward (if vr then (com_cmp cmp) else (com_cmp (neg_cmp cmp))) va) &&
- set a (let+ vb = get b and+ vr = getb r in
- backward (if vr then cmp else (neg_cmp cmp)) vb)
- in
- List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a;b];
- Daemon.attach_value d r Boolean.BoolValue.key (fun d n _ -> wakeup d n)
+ (match Egraph.get_dom d dom a with
+ | Some _ -> ()
+ | None -> Egraph.set_dom d dom a (D.top));
+ (match Egraph.get_dom d dom b with
+ | Some _ -> ()
+ | None -> Egraph.set_dom d dom b (D.top));
+ attach d (
+ (* set a (let+ vr = getb r in Debug.dprintf2 debug "[FP] set top %a" Format.pp_print_bool vr; D.top) && *)
+ (* set b (let+ vr = getb r in Debug.dprintf2 debug "[FP] set top %a" Format.pp_print_bool vr; D.top) && *)
+ (* setb r (let+ vr = getb r in Debug.dprintf4 debug "[FP] domains : a = %a, b = %a" D.pp (fget a) D.pp (fget b); vr) && *)
+ set a (let+ vr = getb r and+ va = get a and+ vb = get b in
+ Debug.dprintf4 debug "[FP] domains : a = %a, b = %a" D.pp va D.pp vb;
+ if vr then !< d (fst (prop va vb)) else va) &&
+ set b (let+ vr = getb r and+ va = get a and+ vb = get b in
+ Debug.dprintf4 debug "[FP] domains : a = %a, b = %a" D.pp va D.pp vb;
+ if vr then !< d (snd (prop va vb)) else vb)
+ )
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;
- let wakeup =
- set r (let+ va = get a and+ vb = get b in D.add va vb)
- in
- List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a; b; r]
- | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
- let (a,b) = IArray.extract2_exn args in
- reg a; reg b;
- let wakeup =
- set r (let+ va = get a and+ vb = get b in D.minus va vb)
- in
- List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a; b; r]
- | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
- let a = IArray.extract1_exn args in
- reg a;
- let wakeup =
- 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)
- in
- List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a;r]
- | { 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
+ | { 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+ vm = getm m and+ va = get a and+ vb = get b in D.add (D.to_mode vm) va vb)
+ )
+ | { app = {builtin = Expr.Fp_eq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ propagate D.eq_inv a b
+ | { app = {builtin = Expr.Fp_leq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ propagate D.le_inv a b
+ | { app = {builtin = Expr.Fp_lt (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ propagate D.lt_inv a b
+ | { app = {builtin = Expr.Fp_geq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ propagate D.ge_inv a b
+ | { app = {builtin = Expr.Fp_gt (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ propagate D.gt_inv a b
| _ -> ()
let init env =
+ Ground.register_converter env converter;
Daemon.attach_reg_value env
Float32.key
(fun d value ->
let v = Float32.value value in
- let s = D.singleton (Farith.B32.to_q v) in
- Egraph.set_dom d dom (Float32.node value) s
- );
- Ground.register_converter env converter
+ if not Farith.B32.(eq v (zero true) || eq v (zero false)) then begin
+ (** An ugly way to fix a bug with the singleton {0} *)
+ let s = D.singleton (D.float32_of_B32 v) in
+ Debug.dprintf4 debug "[FP] set dom %a for %a" D.pp s Node.pp (Float32.node value);
+ Egraph.set_dom d dom (Float32.node value) s
+ end
+ )
+
\ No newline at end of file
diff --git a/src_colibri2/theories/FP/dune b/src_colibri2/theories/FP/dune
index cbb3f787cb459924a1feec6571f6578d90eac56b..09f9db029f87ace159cb599eaecaa0f73d3533cb 100644
--- a/src_colibri2/theories/FP/dune
+++ b/src_colibri2/theories/FP/dune
@@ -5,6 +5,7 @@
(libraries
containers
farith
+ farith2
colibri2.stdlib
colibri2.popop_lib
colibri2.theories.bool
diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml
index 9e42756c13cd597094b4a1ce907f7649a887edc0..16ffe354cf2c1e2b872f999b2d3e6433f40fcabd 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -32,6 +32,10 @@ let cst' c = index c
let cst c = node (cst' c)
+let debug = Debug.register_info_flag
+ ~desc:"for float32 for the FP theory"
+ "FP.float32"
+
(** Initialise type interpretation
TODO : fix bounds (there is a finite set of 32 bits floats)
*)
@@ -158,6 +162,7 @@ let converter d (f:Ground.t) =
| {app={builtin=Expr.Real_to_fp (8, 24); _}; args; _} ->
let m, a = IArray.extract2_exn args in
reg m; reg a;
+ Debug.dprintf2 debug "[FP] assign a value to %a" Node.pp a;
attach d (set r (let+ va = getq a in Farith.B32.of_q !>>m va));
| {app={builtin=Expr.NaN (8, 24); _}; args; _} ->
assert (IArray.is_empty args);
@@ -214,7 +219,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/float64.ml b/src_colibri2/theories/FP/float64.ml
deleted file mode 100644
index 803b353b0fa34c8ce90c3ae5040c1bb11b9e871c..0000000000000000000000000000000000000000
--- a/src_colibri2/theories/FP/float64.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibri2. *)
-(* *)
-(* Copyright (C) 2014-2021 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-open Fp_value
-module N64 = struct let name = "Float64" end
-module Float64 = Value.Register(MakeFloat(Farith.B64)(N64))
-
-include Float64
-
-(** Initialise type interpretation
- TODO : fix bounds (there is a finite set of 64 bits floats)
-*)
-let init_ty d =
- Interp.Register.ty d (fun d ty ->
- match ty with
- | {app={builtin = Builtin.Float(11, 53);_};_} ->
- let seq =
- let open Interp.SeqLim in
- let+ e = of_seq d posint_sequence in
- (Farith.B64.of_bits e |> index |> nodevalue)
- in
- Some seq
- | _ -> None)
-
-(* TO DO : Initialise check *)
-(* let init_check d = Interp.Register.check d (...) *)
-
-let init env =
- init_ty env
diff --git a/src_colibri2/theories/FP/float64.mli b/src_colibri2/theories/FP/float64.mli
deleted file mode 100644
index 908b52f61c02a6f79cab51f3bae8fa5156861146..0000000000000000000000000000000000000000
--- a/src_colibri2/theories/FP/float64.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibri2. *)
-(* *)
-(* Copyright (C) 2014-2021 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-include Value.S with type s = Farith.B64.t
-
-val init : Egraph.wt -> unit
diff --git a/src_colibri2/theories/FP/fp.ml b/src_colibri2/theories/FP/fp.ml
index edd102b7cf47e01221870a9610de44a6e8a5ea3c..cdee9a24e8412d4a20c0fa92862ef8269b595902 100644
--- a/src_colibri2/theories/FP/fp.ml
+++ b/src_colibri2/theories/FP/fp.ml
@@ -21,8 +21,7 @@
let th_register env =
Rounding_mode.init env;
Dom_interval.init env;
- Float32.init env;
- Float64.init env
+ Float32.init env
(* Add the theory to defaults *)
let () =
diff --git a/src_colibri2/theories/FP/interval32.ml b/src_colibri2/theories/FP/interval32.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f0684baed16da75506f0cceff33b08199e8e1c3f
--- /dev/null
+++ b/src_colibri2/theories/FP/interval32.ml
@@ -0,0 +1,54 @@
+include Farith2.Intv32.Intv32
+
+let float32_to_B32 f =
+ (Farith.B32.of_bits (Farith2.B32.B32.to_bits f))
+
+let float32_of_B32 f =
+ (Farith2.B32.B32.of_bits (Farith.B32.to_bits f))
+
+let to_mode (m : Farith.mode) : Farith2.Farith_Big.mode =
+ match m with
+ | Farith.NE -> Farith2.Farith_Big.NE
+ | Farith.ZR -> Farith2.Farith_Big.ZR
+ | Farith.DN -> Farith2.Farith_Big.DN
+ | Farith.UP -> Farith2.Farith_Big.UP
+ | Farith.NA -> Farith2.Farith_Big.NA
+
+(* let is_singleton = function
+ | Farith2.Interval.Inan -> Some Farith.B32.default_nan
+ | Intv (a, b, n) ->
+ if (&&) (Farith2.BinarySingleNaN.coq_Beqb prec emax a b) (not n)
+ then Some (float32_to_B32 a)
+ else None *)
+
+let to_string = function
+ | Farith2.Interval.Inan -> "{ NaN }"
+ | Intv (a, b, nan) ->
+ if nan then
+ Format.sprintf "[%a, %a] + NaN"
+ Farith.B32.pp (float32_to_B32 a)
+ Farith.B32.pp (float32_to_B32 b)
+ else
+ Format.sprintf "[%a, %a]"
+ Farith.B32.pp (float32_to_B32 a)
+ Farith.B32.pp (float32_to_B32 b)
+
+let debug = Debug.register_info_flag
+ ~desc:"trash"
+ "FP.trash"
+
+let pp fmt x = Format.fprintf fmt "%s" (to_string x)
+
+let inter a b =
+ let r = inter a b in
+ match r with
+ | Some x -> Debug.dprintf6 debug "INTER %a %a = %a" pp a pp b pp x; r
+ | None -> Debug.dprintf4 debug "INTER %a %a = BOT" pp a pp b; r
+
+let is_singleton d =
+ match is_singleton d with
+ | None -> None
+ | Some x ->
+ if Farith2.B32.B32.eq x (Farith2.B32.B32.of_q NE Q.zero) then
+ None
+ else failwith "assert false" (* failSome (float32_to_B32 x) *)
\ No newline at end of file