diff --git a/farith2/.ocamlformat b/farith2/.ocamlformat
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/farith2/dune b/farith2/dune
index d5e22754d91cf47e52cc5c78df0148c1aba5cd07..8d6039c4896b8c3bb7a07b07443a80919ec0498b 100644
--- a/farith2/dune
+++ b/farith2/dune
@@ -1,7 +1,9 @@
(library
(name farith2)
(public_name farith2)
- (libraries zarith)
+ (libraries zarith base)
+ (preprocess
+ (pps ppx_deriving.std ppx_hash))
(flags "-w" "-33"))
(copy_files# extracted/*.ml*)
diff --git a/farith2/extract/dune b/farith2/extract/dune
index 86a346fe2db88f1efe868a267c119af7ae075995..5645e69840044ec826f60b4b819cc8ae87c3c75a 100644
--- a/farith2/extract/dune
+++ b/farith2/extract/dune
@@ -1,5 +1,5 @@
(coq.extraction
(prelude extraction)
- (extracted_modules B32 BinNums Bool Qextended Utils Binary BinPosDef Datatypes Round Zaux BinarySingleNaN
- BinPos Interval SpecFloat Zbool BinInt Bits Intv32 Specif Zpower Assert GenericFloat)
+ (extracted_modules BinNums Bool Qextended Utils Binary BinPosDef Datatypes Round Zaux BinarySingleNaN
+ BinPos Interval SpecFloat Zbool BinInt Bits Specif Zpower Assert GenericFloat Version)
(theories Farith2))
diff --git a/farith2/extract/extraction.v b/farith2/extract/extraction.v
index 136f563fb14a6a90e9316d6b8a717cdf853fcf0f..0a05276a59ac9d81ea4e3936bc30d489a3af32e0 100644
--- a/farith2/extract/extraction.v
+++ b/farith2/extract/extraction.v
@@ -1,18 +1,18 @@
-From Flocq Require Import Core.Zaux IEEE754.BinarySingleNaN IEEE754.Bits.
-From Farith2 Require Import Qextended B32 Intv32 GenericFloat.
+From Flocq Require Import Core.Zaux IEEE754.BinarySingleNaN IEEE754.Bits Version.
+From Farith2 Require Import Qextended GenericFloat.
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.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.
+(* 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.
@@ -269,4 +269,4 @@ 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 GenericFloat GenericInterval.
+Separate Extraction GenericFloat GenericInterval Flocq.Version.
diff --git a/farith2/extract/farith_Big.ml b/farith2/extract/farith_Big.ml
index 8ed2ad80c7f2fe17020e800bee1fabd883aae142..3ba55d18b0d35b4687e6acccade4b8aebcc8e0aa 100644
--- a/farith2/extract/farith_Big.ml
+++ b/farith2/extract/farith_Big.ml
@@ -14,10 +14,13 @@
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]. *)
@@ -25,30 +28,42 @@ let two = big_int_of_int 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.
@@ -56,12 +71,15 @@ let quomod = quomod_big_int
[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
@@ -73,25 +91,35 @@ let power = power_big_int_positive_big_int
(* {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
@@ -102,8 +130,10 @@ let of_string = big_int_of_string
(* {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,
@@ -118,15 +148,19 @@ let to_int = int_of_big_int
(* Functions used by extraction *)
-let double n = (Z.shift_left n 1)
+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
+ 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
@@ -137,20 +171,21 @@ let z_case fO fp fn 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 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 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
+ let q, r = quomod n two in
if eq r zero then f2p (loop q) else f2p1 (loop q)
- in loop
+ in
+ loop
let z_rec fO fp fn = z_case (fun _ -> fO) fp fn
@@ -160,7 +195,7 @@ let rec nat_rect acc f 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"
+external identity : 'a -> 'a = "%identity"
let shiftl_pos a p = Z.shift_left a (Z.to_int p)
@@ -176,24 +211,23 @@ let div_pos a b =
let square a = Z.mul a a
-let pow_pos a p =
- Z.pow a (Z.to_int p)
+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
+ 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 ((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);
@@ -202,37 +236,32 @@ let pos_div_eucl 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
+ 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
+ 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_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 mode = NE | ZR | DN | UP | NA
type classify =
| Zero of bool
| Infinity of bool
- | NaN of bool * Z.t
+ | NaN
| Finite of bool * Z.t * Z.t
-let combine_hash acc n = n * 65599 + acc
+let combine_hash acc n = (n * 65599) + acc
diff --git a/farith2/extracted/B32.ml b/farith2/extracted/B32.ml
deleted file mode 100644
index 59a32b73f87cfe42b566455c13a4dc3f12353bef..0000000000000000000000000000000000000000
--- a/farith2/extracted/B32.ml
+++ /dev/null
@@ -1,143 +0,0 @@
-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/extracted/B32.mli b/farith2/extracted/B32.mli
deleted file mode 100644
index e20ce0b7e88057374bc5023cf1911de183703639..0000000000000000000000000000000000000000
--- a/farith2/extracted/B32.mli
+++ /dev/null
@@ -1,49 +0,0 @@
-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/extracted/GenericFloat.ml b/farith2/extracted/GenericFloat.ml
index c74fcbdfd35eeb098b5cee94487cd6e3874ee6b3..6e801d44faf57e305949d315e692c6dc16b8ba4a 100644
--- a/farith2/extracted/GenericFloat.ml
+++ b/farith2/extracted/GenericFloat.ml
@@ -1,11 +1,54 @@
+open BinInt
+open Binary
open BinarySingleNaN
+open Bits
+open Datatypes
open Interval
+open SpecFloat
type __ = Obj.t
+let __ = let rec f _ = Obj.repr f in Obj.repr f
-type 'v coq_Generic = { prec : Farith_Big.big_int; emax : Farith_Big.big_int;
+(** val cprec : Farith_Big.big_int -> Farith_Big.big_int **)
+
+let cprec =
+ Farith_Big.succ
+
+(** val cemax : Farith_Big.big_int -> Farith_Big.big_int **)
+
+let cemax ew0 =
+ Z.pow (Farith_Big.double Farith_Big.one) (Farith_Big.sub ew0 Farith_Big.one)
+
+(** val check_param : Farith_Big.big_int -> Farith_Big.big_int -> bool **)
+
+let check_param mw0 ew0 =
+ (&&)
+ ((&&) (Farith_Big.lt Farith_Big.zero mw0)
+ (Farith_Big.lt Farith_Big.zero ew0))
+ (Farith_Big.lt (cprec mw0) (cemax ew0))
+
+type 'v coq_Generic = { mw : Farith_Big.big_int; ew : Farith_Big.big_int;
value : 'v }
+(** val prec : 'a1 coq_Generic -> Farith_Big.big_int **)
+
+let prec f =
+ cprec f.mw
+
+(** val emax : 'a1 coq_Generic -> Farith_Big.big_int **)
+
+let emax f =
+ cemax f.ew
+
+(** val mk_generic :
+ Farith_Big.big_int -> Farith_Big.big_int -> (Farith_Big.big_int ->
+ Farith_Big.big_int -> __ -> __ -> 'a1) -> 'a1 coq_Generic **)
+
+let mk_generic mw0 ew0 x =
+ let prec0 = cprec mw0 in
+ let emax0 = cemax ew0 in
+ { mw = mw0; ew = ew0; value = (x prec0 emax0 __ __) }
+
(** val same_format_cast :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int -> 'a1 -> 'a1 **)
@@ -16,26 +59,35 @@ let same_format_cast _ _ _ _ f =
(** val same_format : 'a1 coq_Generic -> 'a2 coq_Generic -> bool **)
let same_format x y =
- (&&) (Farith_Big.eq x.prec y.prec) (Farith_Big.eq x.emax y.emax)
+ (&&) (Farith_Big.eq (prec x) (prec y)) (Farith_Big.eq (emax x) (emax y))
(** val mk_with : 'a1 coq_Generic -> 'a2 -> 'a2 coq_Generic **)
let mk_with x y =
- { prec = x.prec; emax = x.emax; value = y }
+ { mw = x.mw; ew = x.ew; value = y }
+
+(** val mk_witho : 'a1 coq_Generic -> 'a2 option -> 'a2 coq_Generic option **)
+
+let mk_witho x = function
+| Some r -> Some (mk_with x r)
+| None -> None
module GenericFloat =
struct
- type coq_F = binary_float coq_Generic
+ module Coq__1 = struct
+ type t = binary_float coq_Generic
+ end
+ include Coq__1
module F_inhab =
struct
- type t = coq_F
+ type t = Coq__1.t
(** val dummy : binary_float coq_Generic **)
let dummy =
- { prec = (Farith_Big.double (Farith_Big.double (Farith_Big.double
- (Farith_Big.succ_double Farith_Big.one)))); emax = (Farith_Big.double
+ { mw = (Farith_Big.double (Farith_Big.double (Farith_Big.double
+ (Farith_Big.succ_double Farith_Big.one)))); ew = (Farith_Big.double
(Farith_Big.double (Farith_Big.double (Farith_Big.double
(Farith_Big.double (Farith_Big.double (Farith_Big.double
Farith_Big.one))))))); value = B754_nan }
@@ -55,53 +107,194 @@ module GenericFloat =
module AssertB = Assert.Assert(B_inhab)
- (** val add :
- Farith_Big.mode -> coq_F -> coq_F -> binary_float coq_Generic option **)
+ (** val of_q' :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> Q.t ->
+ binary_float **)
+
+ let of_q' prec0 emax0 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 prec0 emax0
+ (let (p, lz) =
+ coq_SFdiv_core_binary prec0 emax0 pn Farith_Big.zero
+ (Z.to_pos (Farith_Big.q_den q)) Farith_Big.zero
+ in
+ let (mz, ez) = p in
+ binary_round_aux prec0 emax0 m (xorb false false) mz ez lz))
+ (fun nn ->
+ coq_SF2B prec0 emax0
+ (let (p, lz) =
+ coq_SFdiv_core_binary prec0 emax0 nn Farith_Big.zero
+ (Z.to_pos (Farith_Big.q_den q)) Farith_Big.zero
+ in
+ let (mz, ez) = p in
+ binary_round_aux prec0 emax0 m (xorb true false) mz ez lz))
+ (Farith_Big.q_num q))
+
+ (** val of_q :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> Q.t -> t **)
+
+ let of_q mw0 ew0 m q =
+ (fun x f -> assert x; f ()) (check_param mw0 ew0) (fun _ ->
+ mk_generic mw0 ew0 (fun prec0 emax0 _ _ -> of_q' prec0 emax0 m q))
+
+ (** val add : Farith_Big.mode -> t -> t -> t **)
let add m x y =
- let filtered_var = same_format x y in
- if filtered_var
- then Some { prec = x.prec; emax = x.emax; value =
- (coq_Bplus x.prec x.emax m x.value
- (same_format_cast x.prec x.emax y.prec y.emax y.value)) }
- else None
+ (fun x f -> assert x; f ()) (same_format x y) (fun _ ->
+ mk_with x
+ (coq_Bplus (cprec x.mw) (cemax x.ew) m x.value
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value)))
- (** val coq_Fadd : Farith_Big.mode -> coq_F -> coq_F -> coq_F **)
+ (** val sub : Farith_Big.mode -> t -> t -> t **)
- let coq_Fadd m x y =
+ let sub m x y =
(fun x f -> assert x; f ()) (same_format x y) (fun _ ->
mk_with x
- (coq_Bplus x.prec x.emax m x.value
- (same_format_cast x.prec x.emax y.prec y.emax y.value)))
+ (coq_Bminus (cprec x.mw) (cemax x.ew) m x.value
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value)))
+
+ (** val mul : Farith_Big.mode -> t -> t -> t **)
+
+ let mul m x y =
+ (fun x f -> assert x; f ()) (same_format x y) (fun _ ->
+ mk_with x
+ (coq_Bmult (cprec x.mw) (cemax x.ew) m x.value
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value)))
+
+ (** val div : Farith_Big.mode -> t -> t -> t **)
+
+ let div m x y =
+ (fun x f -> assert x; f ()) (same_format x y) (fun _ ->
+ mk_with x
+ (coq_Bdiv (cprec x.mw) (cemax x.ew) m x.value
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value)))
+
+ (** val sqrt : Farith_Big.mode -> t -> t **)
+
+ let sqrt m x =
+ mk_with x (coq_Bsqrt (cprec x.mw) (cemax x.ew) m x.value)
+
+ (** val abs : t -> t **)
+
+ let abs x =
+ mk_with x (coq_Babs (cprec x.mw) (cemax x.ew) x.value)
+
+ (** val le : t -> t -> bool **)
+
+ let le x y =
+ (fun x f -> assert x; f ()) (same_format x y) (fun _ ->
+ coq_Bleb (cprec x.mw) (cemax x.ew) x.value
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value))
+
+ (** val lt : t -> t -> bool **)
+
+ let lt x y =
+ (fun x f -> assert x; f ()) (same_format x y) (fun _ ->
+ coq_Bltb (cprec x.mw) (cemax x.ew) x.value
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value))
+
+ (** val eq : t -> t -> bool **)
+
+ let eq x y =
+ (fun x f -> assert x; f ()) (same_format x y) (fun _ ->
+ coq_Beqb (cprec x.mw) (cemax x.ew) x.value
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value))
- (** val coq_Fsub : Farith_Big.mode -> coq_F -> coq_F -> coq_F **)
+ (** val ge : t -> t -> bool **)
- let coq_Fsub m x y =
- (fun x f -> assert x; f ()) (same_format x y) (fun _ -> { prec = x.prec;
- emax = x.emax; value =
- (coq_Bminus x.prec x.emax m x.value
- (same_format_cast x.prec x.emax y.prec y.emax y.value)) })
+ let ge x y =
+ (fun x f -> assert x; f ()) (same_format x y) (fun _ ->
+ coq_Bleb (cprec x.mw) (cemax x.ew)
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value) x.value)
+
+ (** val gt : t -> t -> bool **)
+
+ let gt x y =
+ (fun x f -> assert x; f ()) (same_format x y) (fun _ ->
+ coq_Bltb (cprec x.mw) (cemax x.ew)
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value) x.value)
+
+ (** val of_bits' :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ binary_float **)
+
+ let of_bits' mw0 ew0 b =
+ let filtered_var = binary_float_of_bits mw0 ew0 b in
+ (match filtered_var 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 of_bits : Farith_Big.big_int -> Farith_Big.big_int -> Z.t -> t **)
+
+ let of_bits mw0 ew0 z =
+ (fun x f -> assert x; f ()) (check_param mw0 ew0) (fun _ -> { mw = mw0;
+ ew = ew0; value = (of_bits' mw0 ew0 z) })
+
+ (** val pl_cst : Farith_Big.big_int -> Farith_Big.big_int **)
+
+ let pl_cst mw0 =
+ Farith_Big.iter_nat (fun x -> Farith_Big.double x)
+ (Z.to_nat (Farith_Big.pred mw0)) Farith_Big.one
+
+ (** val to_bits : t -> Farith_Big.big_int **)
+
+ let to_bits f =
+ match f.value with
+ | B754_zero s -> bits_of_binary_float f.mw f.ew (Binary.B754_zero s)
+ | B754_infinity s ->
+ bits_of_binary_float f.mw f.ew (Binary.B754_infinity s)
+ | B754_nan ->
+ bits_of_binary_float f.mw f.ew (Binary.B754_nan (true, (pl_cst f.mw)))
+ | B754_finite (s, m, e) ->
+ bits_of_binary_float f.mw f.ew (Binary.B754_finite (s, m, e))
+
+ (** val nan : Farith_Big.big_int -> Farith_Big.big_int -> t **)
+
+ let nan mw0 ew0 =
+ (fun x f -> assert x; f ()) (check_param mw0 ew0) (fun _ ->
+ mk_generic mw0 ew0 (fun _ _ _ _ -> B754_nan))
+
+ (** val zero : Farith_Big.big_int -> Farith_Big.big_int -> bool -> t **)
+
+ let zero mw0 ew0 b =
+ (fun x f -> assert x; f ()) (check_param mw0 ew0) (fun _ ->
+ mk_generic mw0 ew0 (fun _ _ _ _ -> B754_zero b))
+
+ (** val inf : Farith_Big.big_int -> Farith_Big.big_int -> bool -> t **)
+
+ let inf mw0 ew0 b =
+ (fun x f -> assert x; f ()) (check_param mw0 ew0) (fun _ ->
+ mk_generic mw0 ew0 (fun _ _ _ _ -> B754_infinity b))
end
module GenericInterval =
struct
- module Coq__1 = struct
+ module Coq__2 = struct
type t = coq_Interval coq_Generic
end
- include Coq__1
+ include Coq__2
module I_inhab =
struct
- type t = Coq__1.t
+ type t = Coq__2.t
(** val dummy : t **)
let dummy =
- { prec = (Farith_Big.double (Farith_Big.double (Farith_Big.double
- (Farith_Big.succ_double Farith_Big.one)))); emax = (Farith_Big.double
+ { mw = (Farith_Big.succ_double (Farith_Big.succ_double
+ (Farith_Big.succ_double (Farith_Big.double Farith_Big.one)))); ew =
(Farith_Big.double (Farith_Big.double (Farith_Big.double
- (Farith_Big.double (Farith_Big.double (Farith_Big.double
- Farith_Big.one))))))); value = (Intv ((B754_infinity true),
+ Farith_Big.one))); value = (Intv ((B754_infinity true),
(B754_infinity false), true)) }
end
@@ -109,7 +302,7 @@ module GenericInterval =
module O_inhab =
struct
- type t = Coq__1.t option
+ type t = Coq__2.t option
(** val dummy : t **)
@@ -124,10 +317,54 @@ module GenericInterval =
let inter x y =
(fun x f -> assert x; f ()) (same_format x y) (fun _ ->
let r =
- inter x.prec x.emax x.value
- (same_format_cast x.prec x.emax y.prec y.emax y.value)
+ inter (prec x) (emax x) x.value
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value)
in
(match r with
| Some r0 -> Some (mk_with x r0)
| None -> None))
+
+ (** val add : Farith_Big.mode -> t -> t -> t **)
+
+ let add m x y =
+ (fun x f -> assert x; f ()) (same_format x y) (fun _ ->
+ mk_with x
+ (coq_Iadd (prec x) (emax x) m x.value
+ (same_format_cast (prec x) (emax x) (prec y) (emax y) y.value)))
+
+ (** val ge : t -> t option **)
+
+ let ge x =
+ mk_witho x (coq_Ige (prec x) (emax x) x.value)
+
+ (** val gt : t -> t option **)
+
+ let gt x =
+ mk_witho x (coq_Igt (prec x) (emax x) x.value)
+
+ (** val le : t -> t option **)
+
+ let le x =
+ mk_witho x (coq_Ile (prec x) (emax x) x.value)
+
+ (** val lt : t -> t option **)
+
+ let lt x =
+ mk_witho x (coq_Ilt (prec x) (emax x) x.value)
+
+ (** val singleton : GenericFloat.t -> t **)
+
+ let singleton x =
+ mk_with x (singleton (cprec x.mw) (cemax x.ew) x.value)
+
+ (** val is_singleton : t -> GenericFloat.t option **)
+
+ let is_singleton x =
+ mk_witho x (is_singleton (cprec x.mw) (cemax x.ew) x.value)
+
+ (** val top : Farith_Big.big_int -> Farith_Big.big_int -> t **)
+
+ let top mw0 ew0 =
+ (fun x f -> assert x; f ()) (check_param mw0 ew0) (fun _ ->
+ mk_generic mw0 ew0 (fun prec0 emax0 _ _ -> top prec0 emax0))
end
diff --git a/farith2/extracted/GenericFloat.mli b/farith2/extracted/GenericFloat.mli
index 3472c3a41b25d176b23f795d345c45691bea28ed..b0387b2118363e7f80a2a773e0bf88b4c082fc91 100644
--- a/farith2/extracted/GenericFloat.mli
+++ b/farith2/extracted/GenericFloat.mli
@@ -1,11 +1,30 @@
+open BinInt
+open Binary
open BinarySingleNaN
+open Bits
+open Datatypes
open Interval
+open SpecFloat
type __ = Obj.t
-type 'v coq_Generic = { prec : Farith_Big.big_int; emax : Farith_Big.big_int;
+val cprec : Farith_Big.big_int -> Farith_Big.big_int
+
+val cemax : Farith_Big.big_int -> Farith_Big.big_int
+
+val check_param : Farith_Big.big_int -> Farith_Big.big_int -> bool
+
+type 'v coq_Generic = { mw : Farith_Big.big_int; ew : Farith_Big.big_int;
value : 'v }
+val prec : 'a1 coq_Generic -> Farith_Big.big_int
+
+val emax : 'a1 coq_Generic -> Farith_Big.big_int
+
+val mk_generic :
+ Farith_Big.big_int -> Farith_Big.big_int -> (Farith_Big.big_int ->
+ Farith_Big.big_int -> __ -> __ -> 'a1) -> 'a1 coq_Generic
+
val same_format_cast :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int -> 'a1 -> 'a1
@@ -14,13 +33,18 @@ val same_format : 'a1 coq_Generic -> 'a2 coq_Generic -> bool
val mk_with : 'a1 coq_Generic -> 'a2 -> 'a2 coq_Generic
+val mk_witho : 'a1 coq_Generic -> 'a2 option -> 'a2 coq_Generic option
+
module GenericFloat :
sig
- type coq_F = binary_float coq_Generic
+ module Coq__1 : sig
+ type t = binary_float coq_Generic
+ end
+ include module type of struct include Coq__1 end
module F_inhab :
sig
- type t = coq_F
+ type t = Coq__1.t
val dummy : binary_float coq_Generic
end
@@ -40,24 +64,62 @@ module GenericFloat :
sig
end
- val add :
- Farith_Big.mode -> coq_F -> coq_F -> binary_float coq_Generic option
+ val of_q' :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> Q.t ->
+ binary_float
+
+ val of_q :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> Q.t -> t
+
+ val add : Farith_Big.mode -> t -> t -> t
+
+ val sub : Farith_Big.mode -> t -> t -> t
+
+ val mul : 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 coq_Fadd : Farith_Big.mode -> coq_F -> coq_F -> coq_F
+ val eq : t -> t -> bool
- val coq_Fsub : Farith_Big.mode -> coq_F -> coq_F -> coq_F
+ val ge : t -> t -> bool
+
+ val gt : t -> t -> bool
+
+ val of_bits' :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
+ binary_float
+
+ val of_bits : Farith_Big.big_int -> Farith_Big.big_int -> Z.t -> t
+
+ val pl_cst : Farith_Big.big_int -> Farith_Big.big_int
+
+ val to_bits : t -> Farith_Big.big_int
+
+ val nan : Farith_Big.big_int -> Farith_Big.big_int -> t
+
+ val zero : Farith_Big.big_int -> Farith_Big.big_int -> bool -> t
+
+ val inf : Farith_Big.big_int -> Farith_Big.big_int -> bool -> t
end
module GenericInterval :
sig
- module Coq__1 : sig
+ module Coq__2 : sig
type t = coq_Interval coq_Generic
end
- include module type of struct include Coq__1 end
+ include module type of struct include Coq__2 end
module I_inhab :
sig
- type t = Coq__1.t
+ type t = Coq__2.t
val dummy : t
end
@@ -68,7 +130,7 @@ module GenericInterval :
module O_inhab :
sig
- type t = Coq__1.t option
+ type t = Coq__2.t option
val dummy : t
end
@@ -78,4 +140,20 @@ module GenericInterval :
end
val inter : t -> t -> t option
+
+ val add : Farith_Big.mode -> t -> t -> t
+
+ val ge : t -> t option
+
+ val gt : t -> t option
+
+ val le : t -> t option
+
+ val lt : t -> t option
+
+ val singleton : GenericFloat.t -> t
+
+ val is_singleton : t -> GenericFloat.t option
+
+ val top : Farith_Big.big_int -> Farith_Big.big_int -> t
end
diff --git a/farith2/extracted/Interval.ml b/farith2/extracted/Interval.ml
index a252a5c302c5de76d2c3b9f0e68e7a16ba241f25..8f35f75cb22cd83b1ef028429048e49635fefef1 100644
--- a/farith2/extracted/Interval.ml
+++ b/farith2/extracted/Interval.ml
@@ -19,6 +19,31 @@ let to_Interval_opt _ _ = function
| Some j -> Some j
| None -> None
+(** val top : Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval **)
+
+let top _ _ =
+ Intv ((B754_infinity true), (B754_infinity false), true)
+
+(** val is_singleton :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> float option **)
+
+let is_singleton prec emax = 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 singleton :
+ Farith_Big.big_int -> Farith_Big.big_int -> float -> coq_Interval **)
+
+let singleton _ _ x = match x with
+| B754_nan -> Inan
+| _ -> Intv (x, x, false)
+
(** val inter' :
Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval' ->
coq_Interval' -> coq_Interval' option **)
@@ -110,61 +135,3 @@ let coq_Ige _ _ = function
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/extracted/Interval.mli b/farith2/extracted/Interval.mli
index 18d3461764c02fec9548452c12ee35bda43b014a..6a873c01a4e5a53de46a8318891cbbb65dbd7440 100644
--- a/farith2/extracted/Interval.mli
+++ b/farith2/extracted/Interval.mli
@@ -15,6 +15,14 @@ val to_Interval_opt :
Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval' option ->
coq_Interval_opt
+val top : Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval
+
+val is_singleton :
+ Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> float option
+
+val singleton :
+ Farith_Big.big_int -> Farith_Big.big_int -> float -> coq_Interval
+
val inter' :
Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval' -> coq_Interval'
-> coq_Interval' option
@@ -42,30 +50,3 @@ val coq_Ige :
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/extracted/Intv32.ml b/farith2/extracted/Intv32.ml
deleted file mode 100644
index 88fa1f17c182039bdb041ba882dc9e36480c42c1..0000000000000000000000000000000000000000
--- a/farith2/extracted/Intv32.ml
+++ /dev/null
@@ -1,132 +0,0 @@
-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 s00 : t **)
-
- let s00 =
- Intv ((B754_zero false), (B754_zero false), false)
-
- (** val s01 : t **)
-
- let s01 =
- Intv ((B754_zero false), (B754_zero true), false)
-
- (** val s10 : t **)
-
- let s10 =
- Intv ((B754_zero true), (B754_zero false), false)
-
- (** val s11 : t **)
-
- let s11 =
- Intv ((B754_zero true), (B754_zero true), 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/extracted/Intv32.mli b/farith2/extracted/Intv32.mli
deleted file mode 100644
index e44a79c2c97c9a60debfad6f846bb4e0a9c4fe4c..0000000000000000000000000000000000000000
--- a/farith2/extracted/Intv32.mli
+++ /dev/null
@@ -1,55 +0,0 @@
-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 s00 : t
-
- val s01 : t
-
- val s10 : t
-
- val s11 : 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/extracted/Version.ml b/farith2/extracted/Version.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e77689aa7ec1fd0a14f5ba88308be87ef38a3763
--- /dev/null
+++ b/farith2/extracted/Version.ml
@@ -0,0 +1,10 @@
+
+(** val coq_Flocq_version : Farith_Big.big_int **)
+
+let coq_Flocq_version =
+ (Farith_Big.double (Farith_Big.succ_double (Farith_Big.double
+ (Farith_Big.double (Farith_Big.double (Farith_Big.double
+ (Farith_Big.succ_double (Farith_Big.succ_double (Farith_Big.double
+ (Farith_Big.succ_double (Farith_Big.succ_double (Farith_Big.double
+ (Farith_Big.succ_double (Farith_Big.succ_double
+ Farith_Big.one))))))))))))))
diff --git a/farith2/extracted/Version.mli b/farith2/extracted/Version.mli
new file mode 100644
index 0000000000000000000000000000000000000000..dce3905b89ac8474a768899a39c97e7c247937e8
--- /dev/null
+++ b/farith2/extracted/Version.mli
@@ -0,0 +1,2 @@
+
+val coq_Flocq_version : Farith_Big.big_int
diff --git a/farith2/extracted/dune b/farith2/extracted/dune
index cfadeed04bab40ab5d261ab1edbb83a7af611394..a607f0d77a5cc55152f1b3033d7dbe59c1dcb6b2 100644
--- a/farith2/extracted/dune
+++ b/farith2/extracted/dune
@@ -1,9 +1,7 @@
-(rule (action (copy ../extract/B32.ml B32.ml)) (mode promote))
(rule (action (copy ../extract/BinNums.ml BinNums.ml)) (mode promote))
(rule (action (copy ../extract/Bool.ml Bool.ml)) (mode promote))
(rule (action (copy ../extract/Qextended.ml Qextended.ml)) (mode promote))
(rule (action (copy ../extract/Utils.ml Utils.ml)) (mode promote))
-(rule (action (copy ../extract/B32.mli B32.mli)) (mode promote))
(rule (action (copy ../extract/BinNums.mli BinNums.mli)) (mode promote))
(rule (action (copy ../extract/Bool.mli Bool.mli)) (mode promote))
(rule (action (copy ../extract/Qextended.mli Qextended.mli)) (mode promote))
@@ -30,15 +28,15 @@
(rule (action (copy ../extract/Zbool.mli Zbool.mli)) (mode promote))
(rule (action (copy ../extract/BinInt.ml BinInt.ml)) (mode promote))
(rule (action (copy ../extract/Bits.ml Bits.ml)) (mode promote))
-(rule (action (copy ../extract/Intv32.ml Intv32.ml)) (mode promote))
(rule (action (copy ../extract/Specif.ml Specif.ml)) (mode promote))
(rule (action (copy ../extract/Zpower.ml Zpower.ml)) (mode promote))
(rule (action (copy ../extract/BinInt.mli BinInt.mli)) (mode promote))
(rule (action (copy ../extract/Bits.mli Bits.mli)) (mode promote))
-(rule (action (copy ../extract/Intv32.mli Intv32.mli)) (mode promote))
(rule (action (copy ../extract/Specif.mli Specif.mli)) (mode promote))
(rule (action (copy ../extract/Zpower.mli Zpower.mli)) (mode promote))
(rule (action (copy ../extract/Assert.ml Assert.ml)) (mode promote))
(rule (action (copy ../extract/Assert.mli Assert.mli)) (mode promote))
(rule (action (copy ../extract/GenericFloat.ml GenericFloat.ml)) (mode promote))
(rule (action (copy ../extract/GenericFloat.mli GenericFloat.mli)) (mode promote))
+(rule (action (copy ../extract/Version.ml Version.ml)) (mode promote))
+(rule (action (copy ../extract/Version.mli Version.mli)) (mode promote))
diff --git a/farith2/farith2.ml b/farith2/farith2.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7573c9a302236956eb75b199d59db56b214cd934
--- /dev/null
+++ b/farith2/farith2.ml
@@ -0,0 +1,259 @@
+(**************************************************************************)
+(* This file is part of FArith. *)
+(* *)
+(* Copyright (C) 2015-2015 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* 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 *)
+(* (enclosed file LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+open Base
+
+module Z = struct
+ include Z
+
+ let hash_fold_t s t = Base.Hash.fold_int s (hash t)
+end
+
+type mode = Farith_Big.mode = NE | ZR | DN | UP | NA
+[@@deriving eq, ord, hash]
+
+type classify = Farith_Big.classify =
+ | Zero of bool
+ | Infinity of bool
+ | NaN
+ | Finite of bool * Z.t * Z.t
+
+type 'v generic = 'v GenericFloat.coq_Generic = {
+ mw : Z.t;
+ ew : Z.t;
+ value : 'v;
+}
+[@@deriving eq, ord, hash]
+
+module F = struct
+ open GenericFloat
+ include GenericFloat
+
+ let mw t = Z.to_int t.mw
+
+ let ew t = Z.to_int t.ew
+
+ let pp_sign fmt b = Format.pp_print_string fmt (if b then "-" else "+")
+
+ type binary_float = BinarySingleNaN.binary_float =
+ | B754_zero of bool
+ | B754_infinity of bool
+ | B754_nan
+ | B754_finite of bool * Z.t * Z.t
+ [@@deriving eq, ord, hash]
+
+ type t = binary_float generic [@@deriving eq, ord, hash]
+
+ let pp_binary_float fmt (t : binary_float) =
+ match t with
+ | B754_zero b -> Format.fprintf fmt "%a0" pp_sign b
+ | B754_infinity b -> Format.fprintf fmt "%a∞" pp_sign b
+ | B754_nan -> Format.fprintf fmt "NaN"
+ | B754_finite (b, m, e) ->
+ let rec oddify a p =
+ if Z.equal (Z.logand a Z.one) Z.zero then
+ oddify (Z.shift_right_trunc a 1) (Z.succ p)
+ else if Z.equal a Z.zero then (Z.zero, Z.zero)
+ else (a, p)
+ in
+ let m, e = oddify m e in
+ Format.fprintf fmt "%a%ap%a" pp_sign b Z.pp_print m Z.pp_print e
+
+ let pp fmt t = pp_binary_float fmt t.value
+
+ (** lexer for finite float *)
+ let lex_float s =
+ match String.index s 'p' with
+ | Some k ->
+ let m = String.sub s ~pos:0 ~len:k in
+ let e = String.sub s (succ k) (String.length s - k - 1) in
+ (Z.of_string m, Z.of_string e)
+ | None -> (Z.of_string s, Z.zero)
+
+ let of_q ~mw ~ew ~mode q = of_q (Z.of_int mw) (Z.of_int ew) mode q
+
+ let of_bits ~mw ~ew z = of_bits (Z.of_int mw) (Z.of_int ew) z
+
+ let to_bits t = to_bits t
+
+ let nan ~mw ~ew = nan (Z.of_int mw) (Z.of_int ew)
+
+ let zero ~mw ~ew b = zero (Z.of_int mw) (Z.of_int ew) b
+
+ let inf ~mw ~ew b = inf (Z.of_int mw) (Z.of_int ew) b
+
+ let is_zero t = match t.value with B754_zero _ -> true | _ -> false
+end
+
+module I = struct
+ open GenericFloat
+ include GenericInterval
+
+ type interval = Interval.coq_Interval' =
+ | Inan
+ | Intv of F.binary_float * F.binary_float * bool
+ [@@deriving eq, ord, hash]
+
+ type t = interval generic [@@deriving eq, ord, hash]
+
+ let mw t = Z.to_int t.mw
+
+ let ew t = Z.to_int t.ew
+
+ let pp fmt (t : t) =
+ match t.value with
+ | Inan -> Format.fprintf fmt "{ NaN }"
+ | Intv (a, b, nan) ->
+ if nan then
+ Format.fprintf fmt "[%a, %a] + NaN" F.pp_binary_float a
+ F.pp_binary_float b
+ else
+ Format.fprintf fmt "[%a, %a]" F.pp_binary_float a F.pp_binary_float b
+
+ let top ~mw ~ew = top (Z.of_int mw) (Z.of_int ew)
+end
+
+(*
+module D = struct
+ type 't conf = 't Farith_F_aux.fconf
+ include Farith_F_aux.D
+ include Common
+
+ let mw conf = Z.to_int (Farith_F_aux.mw conf)
+ let ew conf = Z.to_int (Farith_F_aux.ew conf)
+
+ let roundq ~mw ~ew mode q = roundq (Z.of_int mw) (Z.of_int ew) mode q
+
+ let pp conf fmt x = pp fmt (cast_to_t conf x)
+
+ (* let of_string conf mode s =
+ * let m,e = lex_float s in
+ * finite conf mode m e *)
+end
+
+module type S = sig
+
+ type t
+ val conf : t D.conf
+
+ val compare: t -> t -> int
+ val equal: t -> t -> bool
+ val hash : t -> int
+
+ val opp : t -> t
+ val add : mode -> t -> t -> t
+ val sub : mode -> t -> t -> t
+ val mul : mode -> t -> t -> t
+ val div : mode -> t -> t -> t
+ val sqrt : mode -> t -> t
+ val abs : t -> t
+
+ val of_bits : Z.t -> t
+ val to_bits : t -> Z.t
+
+ val of_z : mode -> Z.t -> t (** Round. *)
+
+ val of_q : mode -> Q.t -> t (** Round. *)
+
+ val to_q : t -> Q.t (** Exact. *)
+
+ val conv : 't D.conf -> mode -> t -> 't
+
+ val infinity: bool -> t
+ val infp : t
+ val infm : t
+ val zero : bool -> t
+ val zerop: t
+ val nan: bool -> Z.t -> t
+ val default_nan: t
+ val finite: mode -> Z.t -> Z.t -> t
+ val classify: t -> classify
+
+ val le : t -> t -> bool
+ val lt : t -> t -> bool
+ val ge : t -> t -> bool
+ val gt : t -> t -> bool
+ val eq : t -> t -> bool
+ val neq : t -> t -> bool
+
+ val fcompare : t -> t -> int option
+
+ val pp : Format.formatter -> t -> unit
+ val of_string: mode -> string -> t
+
+end
+
+module B32 = struct include Farith_F_aux.B32 include Common
+
+ let of_string mode s =
+ let m,e = lex_float s in
+ finite mode m e
+end
+
+module B64 = struct include Farith_F_aux.B64 include Common
+
+ (** unfortunately of_bits and to_bits wants positive argument (unsigned int64)
+ and Z.of_int64/Z.to_int64 wants signed argument (signed int64)
+ *)
+ let mask_one = Z.pred (Z.shift_left Z.one 64)
+ let of_float f =
+ let fb = (Big_int_Z.big_int_of_int64 (Int64.bits_of_float f)) in
+ let fb = Z.logand mask_one fb in
+ of_bits fb
+
+ let mask_63 = Z.shift_left Z.one 63
+ let intmask_63 = Int64.shift_left Int64.one 63
+ let to_float f =
+ let fb = to_bits f in
+ let i = if Z.logand mask_63 fb = Z.zero then Z.to_int64 fb
+ else Int64.logor intmask_63 (Z.to_int64 (Z.logxor mask_63 fb)) in
+ Int64.float_of_bits i
+
+ let of_string mode s =
+ let m,e = lex_float s in
+ finite mode m e
+
+end
+
+module type Size =
+sig
+ val mw : int (** mantissa size (in bits) *)
+
+ val ew : int (** exponent size (in bits) *)
+end
+
+module Make(Size : Size) =
+struct
+
+ include Farith_F_aux.Make
+ (struct
+ let mw = Z.of_int Size.mw
+ let ew = Z.of_int Size.ew
+ end)
+
+ include Common
+
+ let of_string mode s =
+ let m,e = lex_float s in
+ finite mode m e
+
+end
+*)
+let flocq_version = Version.coq_Flocq_version
diff --git a/farith2/farith2.mli b/farith2/farith2.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c482549024e086896b99e676dfb2428e79f42fc0
--- /dev/null
+++ b/farith2/farith2.mli
@@ -0,0 +1,369 @@
+(**************************************************************************)
+(* This file is part of FArith. *)
+(* *)
+(* Copyright (C) 2015-2015 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* 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 *)
+(* (enclosed file LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Float Arithmetics (based on [Flocq] extraction) *)
+
+(** Supported rounding modes *)
+type mode =
+ | NE (** Nearest to even *)
+ | ZR (** Toward zero *)
+ | DN (** Toward minus infinity *)
+ | UP (** Toward plus infinity *)
+ | NA (** Nearest away from zero *)
+[@@deriving eq, ord, hash]
+
+(** Type used for classifying floating points *)
+type classify =
+ | Zero of bool
+ | Infinity of bool
+ | NaN
+ | Finite of bool * Z.t * Z.t
+
+module F : sig
+ type t [@@deriving eq, ord, hash]
+
+ val ew : t -> int
+
+ val mw : t -> int
+
+ val pp : Format.formatter -> t -> unit
+
+ val of_q : mw:int -> ew:int -> mode:mode -> Q.t -> t
+
+ val add : mode -> t -> t -> t
+
+ val sub : mode -> t -> t -> t
+
+ val mul : mode -> t -> t -> t
+
+ val div : mode -> t -> t -> t
+
+ val sqrt : mode -> t -> t
+
+ val abs : t -> t
+
+ val of_bits : mw:int -> ew:int -> Z.t -> t
+
+ val to_bits : t -> Z.t
+
+ val ge : t -> t -> bool
+
+ val gt : t -> t -> bool
+
+ val le : t -> t -> bool
+
+ val lt : t -> t -> bool
+
+ val eq : t -> t -> bool
+
+ val nan : mw:int -> ew:int -> t
+
+ val zero : mw:int -> ew:int -> bool -> t
+
+ val inf : mw:int -> ew:int -> bool -> t
+
+ val is_zero : t -> bool
+end
+
+module I : sig
+ type t [@@deriving eq, ord, hash]
+
+ val ew : t -> int
+
+ val mw : t -> int
+
+ val pp : Format.formatter -> t -> unit
+
+ val top : mw:int -> ew:int -> t
+
+ val inter : t -> t -> t option
+
+ val add : mode -> t -> t -> t
+
+ val ge : t -> t option
+
+ val gt : t -> t option
+
+ val le : t -> t option
+
+ val lt : t -> t option
+
+ val singleton : F.t -> t
+
+ val is_singleton : t -> F.t option
+end
+
+(* (\** {2 Generic Version } *\)
+ *
+ *
+ * module D : sig
+ *
+ * type 't conf
+ * (\** A configuration links a mantissa and exponent size to a
+ * type which is the set of representable floating point with these sizes.
+ * A value of this type is obtained by application of {!Farith.Make}
+ * *\)
+ *
+ * val mw : 't conf -> int
+ * (\** mantissa size *\)
+ *
+ * val ew : 't conf -> int
+ * (\** exponent size *\)
+ *
+ * (\** {2 Total operators} *\)
+ *
+ * val compare: 't conf -> 't -> 't -> int
+ * val equal: 't conf -> 't -> 't -> bool
+ * val hash : 't conf -> 't -> int
+ *
+ * (\** {2 Floating point operations} *\)
+ *
+ * val opp : 't conf -> 't -> 't
+ * val add : 't conf -> mode -> 't -> 't -> 't
+ * val sub : 't conf -> mode -> 't -> 't -> 't
+ * val mul : 't conf -> mode -> 't -> 't -> 't
+ * val div : 't conf -> mode -> 't -> 't -> 't
+ * val sqrt : 't conf -> mode -> 't -> 't
+ * val abs : 't conf -> 't -> 't
+ *
+ * (\** {2 Conversions} *\)
+ *
+ * val of_bits : 't conf -> Z.t -> 't
+ * (\** Conversions from bitvector representation.
+ * The given bitvector must be positive.
+ * *\)
+ *
+ * val to_bits : 't conf -> 't -> Z.t
+ * (\** Convert the floating point to its bitvector representation *\)
+ *
+ * val of_z : 't conf -> mode -> Z.t -> 't
+ * (\** Convert the integer to the nearest representable integer *\)
+ *
+ * val of_q : 't conf -> mode -> Q.t -> 't
+ * (\** Convert the rational to the nearest representable integer. *\)
+ *
+ * val to_q : 't conf -> 't -> Q.t
+ * (\** Convert the floating-point to its rational representation. *\)
+ *
+ * val conv : 't1 conf -> 't2 conf -> mode -> 't1 -> 't2
+ * (\** Convert the floating point to the nearest representable floating point
+ * having another mantissa and exponent size. *\)
+ *
+ * val roundq : mw:int -> ew:int -> mode -> Q.t -> Q.t
+ * (\** Round the given rational to the nearest representable floating
+ * point with the mantissa width [mw] and exponent width [ew] using
+ * the rounding mode [mode].
+ * *\)
+ *
+ * (\** {2 Floating point constants} *\)
+ * val infinity: 't conf -> bool -> 't
+ * (\** create infinity floating point (true negative, false positive) *\)
+ *
+ * val infp : 't conf -> 't
+ * (\** positive infinity *\)
+ *
+ * val infm : 't conf -> 't
+ * (\** minus infinity *\)
+ *
+ * val zero : 't conf -> bool -> 't
+ * (\** create zero floating point (true negative, false positive) *\)
+ *
+ * val zerop: 't conf -> 't
+ * (\** positive zero *\)
+ *
+ * val nan: 't conf -> bool -> Z.t -> 't
+ * (\** create a nan with the given payload. The payload must fit in the
+ * mantissa *\)
+ *
+ * val default_nan: 't conf -> 't
+ *
+ * val finite: 't conf -> mode -> Z.t -> Z.t -> 't
+ * (\** [finite conf mode m e] return the rounded floating point
+ * corresponding to m*2^e. Beware of the result can be classified
+ * not only as finite but also as infinite or zero because of the
+ * rounding.
+ * *\)
+ *
+ * val classify: 't conf -> 't -> classify
+ * (\** Classify the floating point according to its kind *\)
+ *
+ * (\** {3 IEEE Comparison}
+ *
+ * Respect IEEE behavior for NaN
+ * *\)
+ *
+ * val le : 't conf -> 't -> 't -> bool
+ * val lt : 't conf -> 't -> 't -> bool
+ * val ge : 't conf -> 't -> 't -> bool
+ * val gt : 't conf -> 't -> 't -> bool
+ * val eq : 't conf -> 't -> 't -> bool
+ * val neq : 't conf -> 't -> 't -> bool
+ *
+ * val fcompare : 't conf -> 't -> 't -> int option
+ * (\** return None in the undefined cases (one of the argument is NaN) *\)
+ *
+ * (\** {3 Formatting}
+ *
+ * Format is [<m>[p<e>]] where [<m>] is a signed decimal integer
+ * and [p<e>] an optional exponent in power of 2.
+ * For instance [to_string (of_string "24p-1")] is ["3p2"].
+ * *\)
+ *
+ * val pp : 't conf -> Format.formatter -> 't -> unit
+ * end
+ *
+ * (\** {2 Functorized Version} *\)
+ *
+ *
+ * module type S = sig
+ * type t
+ *
+ * val conf : t D.conf
+ * (\** The configuration for this type of floating-point *\)
+ *
+ * (\** {2 Total operators} *\)
+ *
+ * val compare: t -> t -> int
+ * val equal: t -> t -> bool
+ * val hash : t -> int
+ *
+ * (\** {2 Floating point operations} *\)
+ *
+ * val opp : t -> t
+ * val add : mode -> t -> t -> t
+ * val sub : mode -> t -> t -> t
+ * val mul : mode -> t -> t -> t
+ * val div : mode -> t -> t -> t
+ * val sqrt : mode -> t -> t
+ * val abs : t -> t
+ *
+ * (\** {2 conversions} *\)
+ *
+ * val of_bits : Z.t -> t
+ * (\** Conversions from bitvector representation.
+ * The given bitvector must be positive.
+ * *\)
+ *
+ * val to_bits : t -> Z.t
+ * (\** Convert the floating point to its bitvector representation *\)
+ *
+ * val of_z : mode -> Z.t -> t
+ * (\** Convert the integer to the nearest representable integer *\)
+ *
+ * val of_q : mode -> Q.t -> t
+ * (\** Convert the rational to the nearest representable integer. *\)
+ *
+ * val to_q : t -> Q.t
+ * (\** Convert the floating-point to its rational representation. *\)
+ *
+ * val conv : 't D.conf -> mode -> t -> 't
+ * (\** Convert the floating point to the nearest representable floating point
+ * having another mantissa and exponent size. *\)
+ *
+ * (\** {2 Floating point constants} *\)
+ * val infinity: bool -> t
+ * (\** create infinity floating point (true negative, false positive) *\)
+ *
+ * val infp : t
+ * (\** positive infinity *\)
+ *
+ * val infm : t
+ * (\** minus infinity *\)
+ *
+ * val zero : bool -> t
+ * (\** create zero floating point (true negative, false positive) *\)
+ *
+ * val zerop: t
+ * (\** positive zero *\)
+ *
+ * val nan: bool -> Z.t -> t
+ * (\** create a nan with the given payload. The payload must fit in the
+ * mantissa *\)
+ *
+ * val default_nan: t
+ *
+ * val finite: mode -> Z.t -> Z.t -> t
+ * (\** [finite conf mode m e] return the rounded floating point
+ * corresponding to m*2^e. Beware of the result can be classified
+ * not only as finite but also as infinite or zero because of the
+ * rounding. *\)
+ *
+ * val classify: t -> classify
+ * (\** Classify the floating point according to its kind *\)
+ *
+ * (\** {3 IEEE Comparison}
+ *
+ * Respect IEEE behavior for NaN
+ * *\)
+ *
+ * val le : t -> t -> bool
+ * val lt : t -> t -> bool
+ * val ge : t -> t -> bool
+ * val gt : t -> t -> bool
+ * val eq : t -> t -> bool
+ * val neq : t -> t -> bool
+ *
+ * val fcompare : t -> t -> int option
+ * (\** return None in the undefined cases (one of the argument is NaN) *\)
+ *
+ *
+ * (\** {3 Formatting}
+ *
+ * Format is [<m>[p<e>]] where [<m>] is a signed decimal integer
+ * and [p<e>] an optional exponent in power of 2.
+ * For instance [to_string (of_string "24p-1")] is ["3p2"].
+ * *\)
+ *
+ * val pp : Format.formatter -> t -> unit
+ *
+ *
+ * val of_string: mode -> string -> t
+ * (\** convert string of the shape "[-+][0-9]+p[-+][0-9]+" or "[-+][0-9]+"
+ * to a floating point using the given rounding *\)
+ * end
+ *
+ * module type Size =
+ * sig
+ * val mw : int
+ * (\** mantissa size (in bits) *\)
+ *
+ * val ew : int
+ * (\** exponent size (in bits) *\)
+ * end
+ *
+ * module Make (Size : Size) : S
+ *
+ * (\** {2 Already Applied Versions } *\)
+ *
+ * (\** Simple (mw = 23 ew = 8) *\)
+ * module B32 : S
+ *
+ * (\** Double (mw = 52 ew = 11) *\)
+ * module B64 : sig
+ * include S
+ *
+ * (\** {3 Exact conversion from/to OCaml floats} *\)
+ * val of_float : float -> t
+ * val to_float : t -> float
+ *
+ * end
+ *
+ * val flocq_version: Z.t *)
diff --git a/farith2/thry/B32.v b/farith2/thry/B32.v
index d3e811985799b915aa080cca6704658b9a029ff1..0c3f6367e504de1382e0a6b9f0babba8e09d1af4 100644
--- a/farith2/thry/B32.v
+++ b/farith2/thry/B32.v
@@ -8,7 +8,6 @@ Require Coq.Arith.Wf_nat.
Require Import Extraction.
Require Import Qextended Rextended.
-
(** * An instanciation of Flocq's BinarySingleNan for 32 bits IEEE-754 floating points *)
Module B32.
diff --git a/farith2/thry/GenericFloat.v b/farith2/thry/GenericFloat.v
index 98a473620ef0ca9a54a83f9df3db9d16085c1f6e..d8a92271a7ada9f64f68bbf599c30f0be7285486 100644
--- a/farith2/thry/GenericFloat.v
+++ b/farith2/thry/GenericFloat.v
@@ -1,15 +1,72 @@
-From Flocq Require Import IEEE754.BinarySingleNaN.
-From Coq Require Import Program ZArith Bool.
-Require Import Assert Utils Interval B32.
+From Flocq Require Import Core.Core IEEE754.BinarySingleNaN IEEE754.Bits.
+From Coq Require Import Program ZArith Bool Lia Reals Qreals ZBits.
+Require Import Assert Utils Interval Qextended Rextended.
+
+Definition cprec mw := (Z.succ mw)%Z.
+
+Definition cemax ew := Zpower 2 (ew - 1).
+ (* (if Z.eqb ew 1 then 1 else Z.pow_pos 2 (Z.to_pos (ew - 1)))%Z. *)
+
+Definition check_param mw ew :=
+ andb (andb (0 <? mw)%Z (0 <? ew)%Z) (cprec mw <? cemax ew)%Z.
Record Generic { v } : Type := {
- prec : Z;
- emax : Z;
- Hprec : FLX.Prec_gt_0 prec;
- Hemax : Prec_lt_emax prec emax;
- value : v prec emax;
+ mw : Z;
+ ew : Z;
+ HG: check_param mw ew = true;
+ value : v (cprec mw) (cemax ew);
}.
+Lemma check_param_is_Hprec : forall mw ew, (check_param mw ew = true) -> FLX.Prec_gt_0 (cprec mw).
+Proof.
+ intros mw ew H.
+ unfold check_param in H.
+rewrite !Bool.andb_true_iff in H.
+rewrite <- !Zlt_is_lt_bool in H.
+intuition.
+unfold FLX.Prec_gt_0.
+unfold cprec.
+lia.
+Qed.
+
+Lemma check_param_is_Hw : forall mw ew, (check_param mw ew = true) -> FLX.Prec_gt_0 mw.
+Proof.
+ intros mw ew H.
+ unfold check_param in H.
+rewrite !Bool.andb_true_iff in H.
+rewrite <- !Zlt_is_lt_bool in H.
+intuition.
+Qed.
+
+Lemma check_param_is_Hemax : forall mw ew, (check_param mw ew = true) -> Prec_lt_emax (cprec mw) (cemax ew).
+Proof.
+ intros mw ew H.
+ unfold check_param in H.
+rewrite !Bool.andb_true_iff in H.
+rewrite <- !Zlt_is_lt_bool in H.
+intuition.
+Qed.
+
+Definition prec { v } (f: @Generic v) := cprec (mw f).
+
+Definition emax { v } (f: @Generic v) := cemax (ew f).
+
+Definition Hprec { v } (f: @Generic v) := check_param_is_Hprec (mw f) (ew f) (HG f).
+
+Definition Hemax { v } (f: @Generic v) := check_param_is_Hemax (mw f) (ew f) (HG f).
+
+Definition mk_generic { v } mw ew (H: check_param mw ew = true) (x: forall prec emax, FLX.Prec_gt_0 prec -> Prec_lt_emax prec emax -> v prec emax) : @Generic v :=
+ let prec := cprec mw in
+ let emax := cemax ew in
+ let Hprec : FLX.Prec_gt_0 prec := check_param_is_Hprec _ _ H in
+ let Hemax : Prec_lt_emax prec emax := check_param_is_Hemax _ _ H in
+ {|
+ mw := mw;
+ ew := ew;
+ HG := H;
+ value := x prec emax Hprec Hemax;
+ |}.
+
Program Definition unify { v } (p e p' e' : Z) (f : v p' e') (Hp : p = p') (Hp : e = e') : v p e := f.
Program Definition same_format_cast {v } {p e p' e' : Z} (H : ((p =? p') && (e =? e') = true)%Z) (f : v p' e') : v p e := f.
@@ -22,30 +79,37 @@ Next Obligation.
now rewrite (proj1 (Z.eqb_eq _ _) B).
Defined.
+
Definition same_format { v1 v2 } (x : @Generic v1) (y : @Generic v2) : bool :=
Z.eqb (prec x) (prec y) && Z.eqb (emax x) (emax y).
Definition mk_with {v1 v2} (x : @Generic v1) (y:v2 (prec x) (emax x)) : @Generic v2 :=
{|
- prec := prec x;
- emax := emax x;
- Hprec := Hprec x;
- Hemax := Hemax x;
+ mw := mw x;
+ ew := ew x;
+ HG := HG x;
value := y;
|}.
+
+Definition mk_witho {v1 v2 } (x:@Generic v1) (y:option (v2 (prec x) (emax x))) : option (@Generic v2) :=
+ match y with
+ | Some r => Some (mk_with x r)
+ | None => None
+ end.
+
+
Module GenericFloat.
- Definition F : Type := @Generic binary_float.
+ Definition t : Type := @Generic binary_float.
Module F_inhab.
- Definition t : Type := F.
+ Definition t : Type := t.
Program Definition dummy := {|
- prec := 24;
- emax := 128;
+ mw := 24;
+ ew := 128;
value := BinarySingleNaN.B754_nan;
- Hprec := _;
- Hemax := _;
+ HG := _;
|}.
Solve All Obligations with easy.
End F_inhab.
@@ -60,29 +124,164 @@ Module GenericFloat.
Module AssertB := Assert (B_inhab).
- Program Definition add (m : mode) (x y : F) :=
- match same_format x y with
- | true => Some {|
- prec := prec x;
- emax := emax x;
- Hprec := Hprec x;
- Hemax := Hemax x;
- value := @Bplus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast _ (value y))
- |}
- | false => None
- end.
+ Definition of_q' prec emax Hprec Hemax (m : mode) (q : Qx) : binary_float prec emax :=
+ 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 prec emax Hprec Hemax m false pn 0%Z false (Z.to_pos (den q)) 0%Z))
+ | Z.neg nn =>
+ SF2B _ (proj1 (Bdiv_correct_aux prec emax Hprec Hemax m true nn 0%Z false (Z.to_pos (den q)) 0%Z))
+ end
+ end.
+
+ (* Lemma of_q_correct' : forall prec emax Hprec Hemax m q, Q2Rx q = B2Rx (of_q' prec emax Hprec Hemax m q). *)
+ (* Proof. *)
+ (* intros prec emax Hprec Hemax 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 Rdefinitions.Q2R; simpl. *)
+ (* now rewrite Rmult_0_l. *)
+ (* - rewrite e. destruct s; rewrite e0; simpl. *)
+ (* * replace (Q2R (Z.pos nq # pq)) with *)
+ (* ((F2R (Float radix2 (cond_Zopp false (Z.pos nq)) 0)) *)
+ (* / (F2R (Float radix2 (cond_Zopp false (Z.pos pq)) 0)))%R. *)
+ (* exact (Bdiv_correct_aux' mode false nq 0 false pq 0). *)
+ (* compute [F2R cond_Zopp Q2R]; simpl. *)
+ (* rewrite <- !P2R_INR. *)
+ (* rewrite !Rmult_1_r. *)
+ (* reflexivity. *)
+ (* * replace (Q2R (Z.neg nq # pq)) with *)
+ (* ((F2R (Float radix2 (cond_Zopp true (Z.pos nq)) 0)) *)
+ (* / (F2R (Float radix2 (cond_Zopp false (Z.pos pq)) 0)))%R. *)
+ (* exact (Bdiv_correct_aux' mode true nq 0 false pq 0). *)
+ (* compute [F2R cond_Zopp Q2R]; simpl. *)
+ (* rewrite <- !P2R_INR. *)
+ (* rewrite !Rmult_1_r. *)
+ (* reflexivity. *)
+ (* Qed. *)
+
+ Definition of_q mw ew (m : mode) (q : Qx) : t :=
+ AssertF.assert (check_param mw ew)
+ (fun H => mk_generic mw ew H (fun prec emax Hprec Hemax => of_q' prec emax Hprec Hemax m q)).
- Definition Fadd (m : mode) (x y : F) : F :=
+ Definition add (m : mode) (x y : t) : t :=
AssertF.assert (same_format x y) (fun H => mk_with x (@Bplus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y)))).
- Definition Fsub (m : mode) (x y : F) : F :=
- AssertF.assert (same_format x y) (fun H => {|
- prec := prec x;
- emax := emax x;
- Hprec := Hprec x;
- Hemax := Hemax x;
- value := @Bminus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y));
- |}).
+ Definition sub (m : mode) (x y : t) : t :=
+ AssertF.assert (same_format x y) (fun H => mk_with x (@Bminus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y)))).
+
+ Definition mul (m : mode) (x y : t) : t :=
+ AssertF.assert (same_format x y) (fun H => mk_with x (@Bmult _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y)))).
+
+ Definition div (m : mode) (x y : t) : t :=
+ AssertF.assert (same_format x y) (fun H => mk_with x (@Bdiv _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y)))).
+
+ Definition sqrt (m : mode) (x : t) : t :=
+ mk_with x (@Bsqrt _ _ (Hprec x) (Hemax x) m (value x)).
+
+ Definition abs (x : t) : t :=
+ mk_with x (@Babs _ _ (value x)).
+
+ Definition le (x y : t) : bool :=
+ AssertB.assert (same_format x y) (fun H => (@Bleb _ _ (value x) (same_format_cast H (value y)))).
+
+ Definition lt (x y : t) : bool :=
+ AssertB.assert (same_format x y) (fun H => (@Bltb _ _ (value x) (same_format_cast H (value y)))).
+
+ Definition eq (x y : t) : bool :=
+ AssertB.assert (same_format x y) (fun H => (@Beqb _ _ (value x) (same_format_cast H (value y)))).
+
+ Definition ge (x y : t) : bool :=
+ AssertB.assert (same_format x y) (fun H => (@Bleb _ _ (same_format_cast H (value y)) (value x))).
+
+ Definition gt (x y : t) : bool :=
+ AssertB.assert (same_format x y) (fun H => (@Bltb _ _ (same_format_cast H (value y)) (value x))).
+
+(** ** 4. convertions to and from [Z] and [Q]*)
+
+ Program Definition of_bits' mw ew (H:check_param mw ew = true) (b : Z) : binary_float (cprec mw) (cemax ew) :=
+ match Bits.binary_float_of_bits mw ew _ _ _ 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.
+ Next Obligation.
+ unfold check_param in H.
+ rewrite !Bool.andb_true_iff in H.
+ rewrite <- !Zlt_is_lt_bool in H.
+ intuition.
+ Defined.
+ Next Obligation.
+ unfold check_param in H.
+ rewrite !Bool.andb_true_iff in H.
+ rewrite <- !Zlt_is_lt_bool in H.
+ intuition.
+ Defined.
+ Next Obligation.
+ unfold check_param in H.
+ rewrite !Bool.andb_true_iff in H.
+ rewrite <- !Zlt_is_lt_bool in H.
+ intuition.
+ Defined.
+
+ Definition of_bits mw ew (z : Z.t) : t :=
+ AssertF.assert (check_param mw ew)
+ (fun H =>
+ {|
+ mw := mw;
+ ew := ew;
+ HG := H;
+ value := of_bits' mw ew H z;
+ |}
+).
+
+ Definition pl_cst mw := (Zaux.iter_nat xO (Z.to_nat (Z.pred mw)) xH)%Z.
+
+ Lemma pl_valid mw (Hw:Prec_gt_0 mw) : (Z.pos (Digits.digits2_pos (pl_cst mw)) <? (cprec mw))%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, cprec. unfold Prec_gt_0 in Hw.
+ rewrite G;clear G.
+ rewrite Nat2Z.inj_succ.
+ rewrite Z2Nat.id; [rewrite Z.ltb_lt | ]; lia.
+ Qed.
+
+ Definition to_bits (f : t) : Z :=
+ match value f with
+ | B754_nan =>
+ Bits.bits_of_binary_float (mw f) (ew f) (Binary.B754_nan (prec f) (emax f) true (pl_cst (mw f)) (pl_valid (mw f) (check_param_is_Hw _ _ (HG f))))
+ | B754_zero s => Bits.bits_of_binary_float (mw f) (ew f) (Binary.B754_zero (prec f) (emax f) s)
+ | B754_infinity s => Bits.bits_of_binary_float (mw f) (ew f) (Binary.B754_infinity (prec f) (emax f) s)
+ | B754_finite s m e H => Bits.bits_of_binary_float (mw f) (ew f) (Binary.B754_finite (prec f) (emax f) s m e H)
+ end.
+
+ Definition nan mw ew : t :=
+ AssertF.assert (check_param mw ew) (fun H => mk_generic mw ew H (fun _ _ _ _ => B754_nan)).
+
+ Definition zero mw ew b : t :=
+ AssertF.assert (check_param mw ew) (fun H => mk_generic mw ew H (fun _ _ _ _ => B754_zero b)).
+
+ Definition inf mw ew b : t :=
+ AssertF.assert (check_param mw ew) (fun H => mk_generic mw ew H (fun _ _ _ _ => B754_infinity b)).
+
+
End GenericFloat.
Module GenericInterval.
@@ -92,11 +291,10 @@ Module GenericInterval.
Module I_inhab.
Definition t : Type := t.
Program Definition dummy : t := {|
- prec := 24;
- emax := 128;
+ mw := 23;
+ ew := 8;
value := Intv 24 128 -oo +oo true;
- Hprec := _;
- Hemax := _;
+ HG := _;
|}.
Solve All Obligations with easy.
End I_inhab.
@@ -119,4 +317,24 @@ Module GenericInterval.
| None => None
end ).
+ Definition add (m:mode) (x:t) (y:t) : t :=
+ AssertI.assert (same_format x y) (fun H =>
+ mk_with x (Iadd (prec x) (emax x) (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y)))
+ ).
+
+ Definition ge (x:t) : option t :=
+ mk_witho x (Ige (prec x) (emax x) (value x)).
+ Definition gt (x:t) : option t :=
+ mk_witho x (Igt (prec x) (emax x) (value x)).
+ Definition le (x:t) : option t :=
+ mk_witho x (Ile (prec x) (emax x) (value x)).
+ Definition lt (x:t) : option t :=
+ mk_witho x (Ilt (prec x) (emax x) (value x)).
+ Definition singleton (x:GenericFloat.t) : t :=
+ mk_with x (singleton _ _ (value x)).
+ Definition is_singleton (x:t) : option GenericFloat.t :=
+ mk_witho x (is_singleton _ _ (value x)).
+ Definition top (mw:Z) (ew:Z) : t :=
+ AssertI.assert (check_param mw ew) (fun H => @mk_generic Interval mw ew H (fun prec emax _ _ => top prec emax)).
+
End GenericInterval.
diff --git a/farith2/thry/Interval.v b/farith2/thry/Interval.v
index 10e0b29d695363b02b3ba35f0ba76d94a3184ae6..28dd3c8d6883942f7555eda89f9f7682fea70cbd 100644
--- a/farith2/thry/Interval.v
+++ b/farith2/thry/Interval.v
@@ -67,7 +67,67 @@ Proof.
destruct I;reflexivity.
Qed.
-
+
+ Program Definition top : Interval := Intv -oo +oo true.
+
+ Program Definition bot : Interval_opt := None.
+
+ Lemma top_correct :
+ forall (x : float), contains (proj1_sig top) x.
+ Proof with auto.
+ unfold top, contains; fdestruct x; simpl...
+ Qed.
+
+ Lemma bot_correct :
+ forall (x : float), contains_opt bot x -> False.
+ Proof with auto.
+ unfold bot, contains; fdestruct x.
+ Qed.
+
+ Program Definition is_singleton (I : Interval) : option float :=
+ match proj1_sig 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 := Intv (B754_zero false) (B754_zero true) false.
+
+ Program Theorem is_singleton_correct :
+ forall (I : Interval) (x : float), (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 : float) : Interval :=
+ match x with
+ | B754_nan => Inan
+ | _ => Intv x x false
+ end.
+ Next Obligation.
+ apply Bleb_refl.
+ fdestruct x.
+ Defined.
+
+ Program Theorem singleton_correct :
+ forall (x : float), 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 inter' (I1 I2 : Interval') : option Interval' :=
match I1, I2 with
| Inan, Inan => Some Inan
diff --git a/src_colibri2/theories/FP/.ocamlformat b/src_colibri2/theories/FP/.ocamlformat
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src_colibri2/theories/FP/dom_interval.ml b/src_colibri2/theories/FP/dom_interval.ml
index 7c14b026c2471385a06a017f2f33485ebef30c1b..2623343aca7bddc98b657988e0678ec316ea5d1d 100644
--- a/src_colibri2/theories/FP/dom_interval.ml
+++ b/src_colibri2/theories/FP/dom_interval.ml
@@ -22,31 +22,65 @@ open Colibri2_popop_lib
open Colibri2_core
(* open Colibri2_stdlib.Std *)
-let debug = Debug.register_info_flag
- ~desc:"for intervals for the arithmetic theory"
- "FP.interval"
+let debug =
+ Debug.register_info_flag ~desc:"for intervals for the arithmetic theory"
+ "FP.interval"
-module D = Interval32
+module D = Farith2.I
-let dom = Dom.Kind.create (module struct type t = D.t let name = "FP_ARITH" end)
+let dom =
+ Dom.Kind.create
+ (module struct
+ type t = D.t
-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 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 name = "FP_ARITH"
+ end)
-let (!<) e = function
- | Some x -> x
- | None -> Egraph.contradiction e
+include Dom.Lattice (struct
+ include D
+
+ let key = dom
+
+ let inter _ d1 d2 = inter d1 d2
+
+ let is_singleton _ d =
+ Option.map
+ (fun x -> Fp_value.nodevalue @@ Fp_value.index x)
+ (D.is_singleton d)
+end)
+
+let ( !< ) e = function Some x -> x | None -> Egraph.contradiction e
+
+let neg_cmp = function
+ | `Lt -> `Ge
+ | `Le -> `Gt
+ | `Ge -> `Lt
+ | `Gt -> `Le
+ | `Eq -> `Ne
+ | `Ne -> `Ne
+
+let com_cmp = function
+ | `Lt -> `Gt
+ | `Le -> `Ge
+ | `Ge -> `Le
+ | `Gt -> `Lt
+ | `Eq -> `Eq
+ | `Ne -> `Ne
+
+let backward d c x =
+ let r =
+ match c with
+ | `Lt -> D.lt x
+ | `Gt -> D.gt x
+ | `Le -> D.le x
+ | `Ge -> D.ge x
+ | `Eq -> Some D.(top ~ew:(ew x) ~mw:(mw x))
+ | `Ne -> Some D.(top ~ew:(ew x) ~mw:(mw x))
+ in
+ match r with None -> Egraph.contradiction d | Some r -> r
(** {2 Initialization} *)
-let converter d (f:Ground.t) =
+let converter d (f : Ground.t) =
let r = Ground.node f in
let reg n = Egraph.register d n in
let open Monad in
@@ -55,62 +89,98 @@ let converter d (f:Ground.t) =
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;
- (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)
- )
+ (* let propagate ~mw ~ew prop a b =
+ * reg a; reg b;
+ * (match Egraph.get_dom d dom a with
+ * | Some _ -> ()
+ * | None -> Egraph.set_dom d dom a (D.top ~mw ~ew));
+ * (match Egraph.get_dom d dom b with
+ * | Some _ -> ()
+ * | None -> Egraph.set_dom d dom b (D.top ~mw ~ew));
+ * 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 *)
+ let cmp d cmp ~r ~a ~b =
+ let reg n = Egraph.register d n in
+ (* let test c =
+ * match c with
+ * | D.Uncomparable -> None
+ * | Le -> (
+ * match cmp with
+ * | `Le -> Some true
+ * | `Gt -> Some false
+ * | `Lt | `Ge -> None)
+ * | Lt -> (
+ * match cmp with `Le | `Lt -> Some true | `Ge | `Gt -> Some false)
+ * | Eq -> (
+ * match cmp with `Le | `Ge -> Some true | `Lt | `Gt -> Some false)
+ * | Ge -> (
+ * match cmp with
+ * | `Ge -> Some true
+ * | `Lt -> Some false
+ * | `Gt | `Le -> None)
+ * | Gt -> (
+ * match cmp with `Gt | `Ge -> Some true | `Lt | `Le -> Some false)
+ * in *)
+ reg a;
+ reg b;
+ attach d
+ ((* 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 d (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 d (if vr then cmp else neg_cmp cmp) vb))
in
match Ground.sem f with
- | { 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
+ | { 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 vm va vb))
+ | { app = { builtin = Expr.Fp_eq (8, 24); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp d `Eq ~r ~a ~b
+ | { app = { builtin = Expr.Fp_leq (8, 24); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp d `Le ~r ~a ~b
+ | { app = { builtin = Expr.Fp_lt (8, 24); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp d `Lt ~r ~a ~b
+ | { app = { builtin = Expr.Fp_geq (8, 24); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp d `Ge ~r ~a ~b
+ | { app = { builtin = Expr.Fp_gt (8, 24); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp d `Gt ~r ~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
- 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
- )
-
+ Daemon.attach_reg_value env Fp_value.key (fun d value ->
+ let v = Fp_value.value value in
+ if not (Farith2.F.is_zero v) then (
+ (* An ugly way to fix a bug with the singleton {0} *)
+ let s = D.singleton v in
+ Debug.dprintf4 debug "[FP] set dom %a for %a" D.pp s Node.pp
+ (Fp_value.node value);
+ Egraph.set_dom d dom (Fp_value.node value) s))
diff --git a/src_colibri2/theories/FP/dune b/src_colibri2/theories/FP/dune
index 09f9db029f87ace159cb599eaecaa0f73d3533cb..30caa47cd9b4b4b5a3c73a853565de84b3882aca 100644
--- a/src_colibri2/theories/FP/dune
+++ b/src_colibri2/theories/FP/dune
@@ -4,7 +4,6 @@
(synopsis "theory of floatting points for colibri2")
(libraries
containers
- farith
farith2
colibri2.stdlib
colibri2.popop_lib
diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml
deleted file mode 100644
index 16ffe354cf2c1e2b872f999b2d3e6433f40fcabd..0000000000000000000000000000000000000000
--- a/src_colibri2/theories/FP/float32.ml
+++ /dev/null
@@ -1,225 +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
-open Colibri2_theories_LRA
-open Colibri2_popop_lib
-
-
-module N32 = struct let name = "Float32" end
-module Float32 = Value.Register(MakeFloat(Farith.B32)(N32))
-
-include Float32
-
-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)
-*)
-let init_ty d =
- let specials =
- let open Base.Sequence.Generator in
- let (let*) = (>>=) in
- run (
- let* _ = yield (Farith.B32.default_nan) in
- let* _ = yield (Farith.B32.zero true) in
- let* _ = yield (Farith.B32.zero false) in
- let* _ = yield (Farith.B32.infm) in
- yield (Farith.B32.infp))
- in
- let open Base.Sequence in
- let finites = posint_sequence >>| Farith.B32.of_bits in
- let fp_seq = append specials finites in
- let fp_values = fp_seq >>| Float32.of_value in
- Interp.Register.ty d (fun d ty ->
- match ty with
- | {app={builtin = Builtin.Float(8, 24);_};_} ->
- let open Interp.SeqLim in
- Some (of_seq d fp_values)
- | _ -> None)
-
-let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
-
-let compute_ground d t =
- let (!>>>) t = RealValue.coerce_value (interp d t) in
- let (!>>) t = Rounding_mode.coerce_value (interp d t) in
- let (!>) t = Float32.coerce_value (interp d t) in
- let (!<) v = `Some (Float32.nodevalue (Float32.index v)) in
- let (!<<) v = `Some (Boolean.BoolValue.nodevalue (Boolean.BoolValue.index v)) in
- match Ground.sem t with
- | { app = {builtin = Expr.Real_to_fp (8, 24); _}; args; _} ->
- let m, r = IArray.extract2_exn args in
- !< (Farith.B32.of_q !>>m !>>>r)
- | { app = {builtin = Expr.Plus_infinity (8, 24); _}; args; _} ->
- assert (IArray.is_empty args);
- !< (Farith.B32.infp)
- | { app = {builtin = Expr.Minus_infinity (8, 24); _}; args; _} ->
- assert (IArray.is_empty args);
- !< (Farith.B32.infm)
- | { app = {builtin = Expr.NaN (8, 24); _}; args; _} ->
- assert (IArray.is_empty args);
- !< (Farith.B32.(nan true Z.one))
- | { app = {builtin = Expr.Plus_zero (8, 24); _}; args; _} ->
- assert (IArray.is_empty args);
- !< (Farith.B32.zerop)
- | { app = {builtin = Expr.Minus_zero (8, 24); _}; args; _} ->
- assert (IArray.is_empty args);
- !< (Farith.B32.zero true)
- | { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
- let m, a, b = IArray.extract3_exn args in
- !< (Farith.B32.add !>>m !>a !>b)
- | { app = {builtin = Expr.Fp_sub (8, 24); _}; args; _} ->
- let m, a, b = IArray.extract3_exn args in
- !< (Farith.B32.sub !>>m !>a !>b)
- | { app = {builtin = Expr.Fp_mul (8, 24); _}; args; _} ->
- let m, a, b = IArray.extract3_exn args in
- !< (Farith.B32.mul !>>m !>a !>b)
- | { app = {builtin = Expr.Fp_abs (8, 24); _}; args; _} ->
- let a = IArray.extract1_exn args in
- !< (Farith.B32.abs !>a)
- | { app = {builtin = Expr.Fp_div (8, 24); _}; args; _} ->
- let m, a, b = IArray.extract3_exn args in
- if Farith.B32.(eq !>b (zero true) || eq !>b (zero false)) then `Uninterp
- else !< (Farith.B32.div !>>m !>a !>b)
- | { app = {builtin = Expr.Fp_eq (8, 24); _}; args; _} ->
- let a, b = IArray.extract2_exn args in
- !<< (Farith.B32.eq !>a !>b)
- | { app = {builtin = Expr.Fp_leq (8, 24); _}; args; _} ->
- let a, b = IArray.extract2_exn args in
- !<< (Farith.B32.le !>a !>b)
- | { app = {builtin = Expr.Fp_lt (8, 24); _}; args; _} ->
- let a, b = IArray.extract2_exn args in
- !<< (Farith.B32.lt !>a !>b)
- | { app = {builtin = Expr.Fp_geq (8, 24); _}; args; _} ->
- let a, b = IArray.extract2_exn args in
- !<< (Farith.B32.ge !>a !>b)
- | { app = {builtin = Expr.Fp_gt (8, 24); _}; args; _} ->
- let a, b = IArray.extract2_exn args in
- !<< (Farith.B32.gt !>a !>b)
- | _ -> `None
-
-let init_check d = Interp.Register.check d (fun d t ->
- let check r =
- Value.equal r (interp d (Ground.node t))
- in
- match compute_ground d t with
- | `None -> NA
- | `Some v -> Interp.check_of_bool (check v)
- | `Uninterp ->
- Interp.check_of_bool (Uninterp.On_uninterpreted_domain.check d t)
- )
-
-let attach_interp d g =
- let f d g =
- match compute_ground d g with
- | `None -> raise Impossible
- | `Some v -> Egraph.set_value d (Ground.node g) v
- | `Uninterp -> Uninterp.On_uninterpreted_domain.propagate d g
- in
- Interp.WatchArgs.create d f g
-
-let converter d (f:Ground.t) =
- let r = Ground.node f in
- let reg n = Egraph.register d n in
- let merge n = Egraph.register d n; Egraph.merge d r n in
- let open Monad in
- let get a = Monad.getv Float32.key a in
- let getq a = Monad.getv RealValue.key a in
- let set a = Monad.setv Float32.key a in
- let _getb a = Monad.getv Boolean.BoolValue.key a in
- let setb a = Monad.setv Boolean.BoolValue.key a in
- let (!>>) t = Rounding_mode.value (Rounding_mode.coerce_nodevalue (interp d t )) in
- (* let (!>>>) t = RealValue.value (RealValue.coerce_nodevalue (interp d t )) in *)
- let is_zero v = Farith.B32.(eq v (zero true) || eq v (zero false)) in
- let cmp cmp a b =
- reg a; reg b;
- attach d (setb r (let+ va = get a and+ vb = get b in cmp va vb));
- in
- match Ground.sem f with
- | {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);
- merge (cst (Farith.B32.nan true Z.one))
- | {app={builtin=Expr.Plus_infinity (8, 24); _}; args; _} ->
- assert (IArray.is_empty args);
- merge (cst (Farith.B32.infp))
- | {app={builtin=Expr.Minus_infinity (8, 24); _}; args; _} ->
- assert (IArray.is_empty args);
- merge (cst (Farith.B32.infm))
- | {app={builtin=Expr.Plus_zero (8, 24); _}; args; _} ->
- assert (IArray.is_empty args);
- merge (cst (Farith.B32.zerop))
- | {app={builtin=Expr.Minus_zero (8, 24); _}; args; _} ->
- assert (IArray.is_empty args);
- merge (cst (Farith.B32.zero true))
- | {app={builtin=Expr.Fp_abs (8, 24); _}; args; _} ->
- let a = IArray.extract1_exn args in
- reg a; attach_interp d f;
- attach d (set r (let+ va = get a in Farith.B32.abs va));
- | {app={builtin=Expr.Fp_add (8, 24); _}; args; _} ->
- let m, a, b = IArray.extract3_exn args in
- reg m; reg a; reg b; attach_interp d f;
- attach d (set r (let+ va = get a and+ vb = get b in Farith.B32.add !>>m va vb));
- | {app={builtin=Expr.Fp_sub (8, 24); _}; args; _} ->
- let m, a, b = IArray.extract3_exn args in
- reg m; reg a; reg b; attach_interp d f;
- attach d (set r (let+ va = get a and+ vb = get b in Farith.B32.sub !>>m va vb));
- | {app={builtin=Expr.Fp_mul (8, 24); _}; args; _} ->
- let m, a, b = IArray.extract3_exn args in
- reg m; reg a; reg b; attach_interp d f;
- attach d (
- set r (let* va = get a and+ vb = get b in
- if is_zero vb then None else Some (Farith.B32.mul !>>m va vb))
- );
- | {app={builtin=Expr.Fp_div (8, 24); _}; args; _} ->
- let m, a, b = IArray.extract3_exn args in
- reg m; reg a; reg b; attach_interp d f;
- attach d (
- set r (let* va = get a and+ vb = get b in
- if is_zero vb then None else Some (Farith.B32.div !>>m va vb))
- );
- | {app={builtin=Expr.Fp_leq (8, 24); _}; args; _} ->
- let a, b = IArray.extract2_exn args in
- cmp Farith.B32.le a b; attach_interp d f;
- | {app={builtin=Expr.Fp_gt (8, 24); _}; args; _} ->
- let a, b = IArray.extract2_exn args in
- cmp Farith.B32.gt a b; attach_interp d f;
- | {app={builtin=Expr.Fp_geq (8, 24); _}; args; _} ->
- let a, b = IArray.extract2_exn args in
- cmp Farith.B32.ge a b; attach_interp d f;
- | {app={builtin=Expr.Fp_eq (8, 24); _}; args; _} ->
- let a, b = IArray.extract2_exn args in
- cmp Farith.B32.eq a b; attach_interp d f;
- | _ -> ()
-
-let init env =
- Ground.register_converter env converter;
- init_ty env;
- init_check env
diff --git a/src_colibri2/theories/FP/float32.mli b/src_colibri2/theories/FP/float32.mli
deleted file mode 100644
index 9f3efaae6112d8fd67db119080a51a67bd97f858..0000000000000000000000000000000000000000
--- a/src_colibri2/theories/FP/float32.mli
+++ /dev/null
@@ -1,27 +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.B32.t
-
-val cst': Farith.B32.t -> t
-
-val cst: Farith.B32.t -> Node.t
-
-val init : Egraph.wt -> unit
diff --git a/src_colibri2/theories/FP/fp.ml b/src_colibri2/theories/FP/fp.ml
index cdee9a24e8412d4a20c0fa92862ef8269b595902..051ba09be7be0718ed8902ff23510cf60b145197 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
+ Fp_value.init env
(* Add the theory to defaults *)
-let () =
- Init.add_default_theory th_register
+let () = Init.add_default_theory th_register
diff --git a/src_colibri2/theories/FP/fp_value.ml b/src_colibri2/theories/FP/fp_value.ml
index a40c709cb78884624f70a3a98f9876919677afe0..2f78529956cec2354ec47f9efc3d3d997c012610 100644
--- a/src_colibri2/theories/FP/fp_value.ml
+++ b/src_colibri2/theories/FP/fp_value.ml
@@ -21,35 +21,258 @@
open Colibri2_popop_lib
open Popop_stdlib
-module type FloatName = sig val name : string end
+module F = struct
+ include Farith2.F
+ include MkDatatype (Farith2.F)
-(** Extends a module of type [Farith.S] to be of type [Value.Kind.Value] *)
-module MakeFloat (F : Farith.S) (N : FloatName) = struct
+ let name = "Fp_value"
+end
- (** Extends a module of type [Farith.S] with [hash_fold_t] and [sexp_of_t] *)
- module HF = struct
- include F
- let hash_fold_t s t = Base.Hash.fold_int s (hash t)
- let sexp_of_t = sexp_of_t_of_pp F.pp
- end
+module N = struct
+ let name = "Float"
+end
- include HF
- module M = Map.Make(HF)
- module S = Extset.MakeOfMap(M)
- module H = XHashtbl.Make(HF)
+module Float = Value.Register (F)
+include Float
- let name = N.name
+let cst' c = index c
-end
+let cst c = node (cst' c)
+
+let debug =
+ Debug.register_info_flag ~desc:"for value for the FP theory" "FP.fp_value"
(** Generate the sequence of all positive integers (without 0) *)
let posint_sequence_without_zero =
let open Base.Sequence.Generator in
- let rec loop i =
- yield i >>= (fun () -> loop (Z.succ i))
- in
+ let rec loop i = yield i >>= fun () -> loop (Z.succ i) in
run (loop Z.one)
(** Generate the sequence of positive integers (without 0) *)
let posint_sequence =
Base.Sequence.shift_right posint_sequence_without_zero Z.zero
+
+(** Initialise type interpretation
+ TODO : fix bounds (there is a finite set of 32 bits floats)
+*)
+let init_ty d =
+ let specials ~mw ~ew =
+ let open Base.Sequence.Generator in
+ let ( let* ) = ( >>= ) in
+ run
+ (let* () = yield (F.nan ~mw ~ew) in
+ let* () = yield (F.zero ~mw ~ew true) in
+ let* () = yield (F.zero ~mw ~ew false) in
+ let* () = yield (F.inf ~mw ~ew false) in
+ yield (F.inf ~mw ~ew true))
+ in
+ let open Base.Sequence in
+ let finites ~mw ~ew = posint_sequence >>| F.of_bits ~mw ~ew in
+ let fp_seq ~mw ~ew = append (specials ~mw ~ew) (finites ~mw ~ew) in
+ let fp_values ~mw ~ew = fp_seq ~mw ~ew >>| of_value in
+ Interp.Register.ty d (fun d ty ->
+ match ty with
+ | { app = { builtin = Builtin.Float (ew, prec); _ }; _ } ->
+ let open Interp.SeqLim in
+ Some (of_seq d (fp_values ~ew ~mw:(prec - 1)))
+ | _ -> None)
+
+let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
+
+let compute_ground d t =
+ let ( !>>> ) t = Colibri2_theories_LRA.RealValue.coerce_value (interp d t) in
+ let ( !>> ) t = Rounding_mode.coerce_value (interp d t) in
+ let ( !> ) t = coerce_value (interp d t) in
+ let ( !< ) v = `Some (nodevalue (index v)) in
+ let ( !<< ) v =
+ `Some (Boolean.BoolValue.nodevalue (Boolean.BoolValue.index v))
+ in
+ match Ground.sem t with
+ | { app = { builtin = Expr.Real_to_fp (ew, prec); _ }; args; _ } ->
+ let m, r = IArray.extract2_exn args in
+ !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m !>>>r)
+ | { app = { builtin = Expr.Plus_infinity (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ !<(F.inf ~ew ~mw:(prec - 1) false)
+ | { app = { builtin = Expr.Minus_infinity (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ !<(F.inf ~ew ~mw:(prec - 1) true)
+ | { app = { builtin = Expr.NaN (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ !<(F.nan ~ew ~mw:(prec - 1))
+ | { app = { builtin = Expr.Plus_zero (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ !<(F.zero ~ew ~mw:(prec - 1) false)
+ | { app = { builtin = Expr.Minus_zero (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ !<(F.zero ~ew ~mw:(prec - 1) true)
+ | { app = { builtin = Expr.Fp_add (_ew, _prec); _ }; args; _ } ->
+ let m, a, b = IArray.extract3_exn args in
+ !<(F.add !>>m !>a !>b)
+ | { app = { builtin = Expr.Fp_sub (_ew, _prec); _ }; args; _ } ->
+ let m, a, b = IArray.extract3_exn args in
+ !<(F.sub !>>m !>a !>b)
+ | { app = { builtin = Expr.Fp_mul (_ew, _prec); _ }; args; _ } ->
+ let m, a, b = IArray.extract3_exn args in
+ !<(F.mul !>>m !>a !>b)
+ | { app = { builtin = Expr.Fp_abs (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<(F.abs !>a)
+ | { app = { builtin = Expr.Fp_div (_ew, _prec); _ }; args; _ } ->
+ let m, a, b = IArray.extract3_exn args in
+ !<(F.div !>>m !>a !>b)
+ | { app = { builtin = Expr.Fp_eq (_ew, _prec); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(F.eq !>a !>b)
+ | { app = { builtin = Expr.Fp_leq (_ew, _prec); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(F.le !>a !>b)
+ | { app = { builtin = Expr.Fp_lt (_ew, _prec); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(F.lt !>a !>b)
+ | { app = { builtin = Expr.Fp_geq (_ew, _prec); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(F.ge !>a !>b)
+ | { app = { builtin = Expr.Fp_gt (_ew, _prec); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(F.gt !>a !>b)
+ | _ -> `None
+
+let init_check d =
+ Interp.Register.check d (fun d t ->
+ let check r = Value.equal r (interp d (Ground.node t)) in
+ match compute_ground d t with
+ | `None -> NA
+ | `Some v -> Interp.check_of_bool (check v)
+ | `Uninterp ->
+ Interp.check_of_bool (Uninterp.On_uninterpreted_domain.check d t))
+
+let attach_interp d g =
+ let f d g =
+ match compute_ground d g with
+ | `None -> raise Impossible
+ | `Some v -> Egraph.set_value d (Ground.node g) v
+ | `Uninterp -> Uninterp.On_uninterpreted_domain.propagate d g
+ in
+ Interp.WatchArgs.create d f g
+
+let converter d (f : Ground.t) =
+ let r = Ground.node f in
+ let reg n = Egraph.register d n in
+ let merge n =
+ Egraph.register d n;
+ Egraph.merge d r n
+ in
+ let open Monad in
+ let get a = Monad.getv key a in
+ let getq a = Monad.getv Colibri2_theories_LRA.RealValue.key a in
+ let set a = Monad.setv key a in
+ let _getb a = Monad.getv Boolean.BoolValue.key a in
+ let setb a = Monad.setv Boolean.BoolValue.key a in
+ let ( !>> ) t =
+ Rounding_mode.value (Rounding_mode.coerce_nodevalue (interp d t))
+ in
+ (* let (!>>>) t = RealValue.value (RealValue.coerce_nodevalue (interp d t )) in *)
+ let cmp cmp a b =
+ reg a;
+ reg b;
+ attach d
+ (setb r
+ (let+ va = get a and+ vb = get b in
+ cmp va vb))
+ in
+ match Ground.sem f with
+ | { app = { builtin = Expr.Real_to_fp (ew, prec); _ }; 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
+ F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m va))
+ | { app = { builtin = Expr.NaN (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ merge (cst (F.nan ~ew ~mw:(prec - 1)))
+ | { app = { builtin = Expr.Plus_infinity (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ merge (cst (F.inf ~ew ~mw:(prec - 1) false))
+ | { app = { builtin = Expr.Minus_infinity (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ merge (cst (F.inf ~ew ~mw:(prec - 1) true))
+ | { app = { builtin = Expr.Plus_zero (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ merge (cst (F.zero ~ew ~mw:(prec - 1) false))
+ | { app = { builtin = Expr.Minus_zero (ew, prec); _ }; args; _ } ->
+ assert (IArray.is_empty args);
+ merge (cst (F.zero ~ew ~mw:(prec - 1) true))
+ | { app = { builtin = Expr.Fp_abs (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ attach_interp d f;
+ attach d
+ (set r
+ (let+ va = get a in
+ F.abs va))
+ | { app = { builtin = Expr.Fp_add (_ew, _prec); _ }; args; _ } ->
+ let m, a, b = IArray.extract3_exn args in
+ reg m;
+ reg a;
+ reg b;
+ attach_interp d f;
+ attach d
+ (set r
+ (let+ va = get a and+ vb = get b in
+ F.add !>>m va vb))
+ | { app = { builtin = Expr.Fp_sub (_ew, _prec); _ }; args; _ } ->
+ let m, a, b = IArray.extract3_exn args in
+ reg m;
+ reg a;
+ reg b;
+ attach_interp d f;
+ attach d
+ (set r
+ (let+ va = get a and+ vb = get b in
+ F.sub !>>m va vb))
+ | { app = { builtin = Expr.Fp_mul (_ew, _prec); _ }; args; _ } ->
+ let m, a, b = IArray.extract3_exn args in
+ reg m;
+ reg a;
+ reg b;
+ attach_interp d f;
+ attach d
+ (set r
+ (let* va = get a and+ vb = get b in
+ if F.is_zero vb then None else Some (F.mul !>>m va vb)))
+ | { app = { builtin = Expr.Fp_div (_ew, _prec); _ }; args; _ } ->
+ let m, a, b = IArray.extract3_exn args in
+ reg m;
+ reg a;
+ reg b;
+ attach_interp d f;
+ attach d
+ (set r
+ (let* va = get a and+ vb = get b in
+ if F.is_zero vb then None else Some (F.div !>>m va vb)))
+ | { app = { builtin = Expr.Fp_leq (_ew, _prec); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp F.le a b;
+ attach_interp d f
+ | { app = { builtin = Expr.Fp_gt (_ew, _prec); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp F.gt a b;
+ attach_interp d f
+ | { app = { builtin = Expr.Fp_geq (_ew, _prec); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp Farith2.F.ge a b;
+ attach_interp d f
+ | { app = { builtin = Expr.Fp_eq (_ew, _prec); _ }; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp Farith2.F.eq a b;
+ attach_interp d f
+ | _ -> ()
+
+let init env =
+ Ground.register_converter env converter;
+ init_ty env;
+ init_check env
diff --git a/src_colibri2/theories/FP/fp_value.mli b/src_colibri2/theories/FP/fp_value.mli
index 6c759aa446a375910404bdaba4f48383a5ed0b12..04557f872a38ee1cffb4588f8caaeb8f3d4d21e4 100644
--- a/src_colibri2/theories/FP/fp_value.mli
+++ b/src_colibri2/theories/FP/fp_value.mli
@@ -18,16 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-(** Helpers to generate new interpretations of floating points *)
+include Value.S with type s = Farith2.F.t
+(** Foating points values *)
-(** Sequence of all positive integers *)
-val posint_sequence : Z.t Base.Sequence.t
-
-(** Names (string) wrapped in a module *)
-module type FloatName = sig val name : string end
-
-(**
- Helper to extend a module of type [Farith.S] into a module of
- type [Value.Kind.Value]
-*)
-module MakeFloat (F : Farith.S) (_ : FloatName) : Colibri2_popop_lib.Popop_stdlib.NamedDatatype with type t = F.t
+val init : Egraph.wt -> unit
diff --git a/src_colibri2/theories/FP/interval32.ml b/src_colibri2/theories/FP/interval32.ml
deleted file mode 100644
index a23adc11371f513e416325fc5e3ea5c81ecb2d13..0000000000000000000000000000000000000000
--- a/src_colibri2/theories/FP/interval32.ml
+++ /dev/null
@@ -1,54 +0,0 @@
-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 None (** todo *)
diff --git a/src_colibri2/theories/FP/rounding_mode.ml b/src_colibri2/theories/FP/rounding_mode.ml
index d86092b0eaf0cf28568f3dc4eecb9903f108ecdf..55775b37c90506a61690e3fd89a9b2657a70bac5 100644
--- a/src_colibri2/theories/FP/rounding_mode.ml
+++ b/src_colibri2/theories/FP/rounding_mode.ml
@@ -23,13 +23,13 @@ open Popop_stdlib
module FarithModes = struct
let string_of_mode = function
- | Farith.NE -> "RoundNearestTiesToEven"
- | Farith.NA -> "RoundNearestTiesToAway"
- | Farith.UP -> "RoundTowardPositive"
- | Farith.DN -> "RoundTowardNegative"
- | Farith.ZR -> "RoundTowardZero"
+ | Farith2.NE -> "RoundNearestTiesToEven"
+ | Farith2.NA -> "RoundNearestTiesToAway"
+ | Farith2.UP -> "RoundTowardPositive"
+ | Farith2.DN -> "RoundTowardNegative"
+ | Farith2.ZR -> "RoundTowardZero"
- type t = Farith.mode
+ type t = Farith2.mode
let hash = Hashtbl.hash
@@ -57,11 +57,11 @@ include Modes
let rounding_mode_sequence =
let open Base.Sequence.Generator in
(
- yield Farith.NE >>= fun () ->
- yield Farith.NA >>= fun () ->
- yield Farith.UP >>= fun () ->
- yield Farith.DN >>= fun () ->
- yield Farith.ZR
+ yield Farith2.NE >>= fun () ->
+ yield Farith2.NA >>= fun () ->
+ yield Farith2.UP >>= fun () ->
+ yield Farith2.DN >>= fun () ->
+ yield Farith2.ZR
) |> run
let init_ty d =
@@ -83,15 +83,15 @@ let compute_cst t =
let (!<) v = `Some (Modes.nodevalue (Modes.index v)) in
match Ground.sem t with
| { app = {builtin = Expr.RoundNearestTiesToEven; _}; _} ->
- !< Farith.NE
+ !< Farith2.NE
| { app = {builtin = Expr.RoundNearestTiesToAway; _}; _} ->
- !< Farith.NA
+ !< Farith2.NA
| { app = {builtin = Expr.RoundTowardNegative; _}; _} ->
- !< Farith.DN
+ !< Farith2.DN
| { app = {builtin = Expr.RoundTowardPositive; _}; _} ->
- !< Farith.UP
+ !< Farith2.UP
| { app = {builtin = Expr.RoundTowardZero; _}; _} ->
- !< Farith.ZR
+ !< Farith2.ZR
| _ -> `None
let converter d f =
@@ -100,15 +100,15 @@ let converter d f =
let merge n = Egraph.register d n; Egraph.merge d r n in
match Ground.sem f with
| { app = {builtin = Expr.RoundNearestTiesToEven; _}; _} ->
- merge (cst Farith.NE)
+ merge (cst Farith2.NE)
| { app = {builtin = Expr.RoundNearestTiesToAway; _}; _} ->
- merge (cst Farith.NA)
+ merge (cst Farith2.NA)
| { app = {builtin = Expr.RoundTowardNegative; _}; _} ->
- merge (cst Farith.DN)
+ merge (cst Farith2.DN)
| { app = {builtin = Expr.RoundTowardPositive; _}; _} ->
- merge (cst Farith.UP)
+ merge (cst Farith2.UP)
| { app = {builtin = Expr.RoundTowardZero; _}; _} ->
- merge (cst Farith.ZR)
+ merge (cst Farith2.ZR)
| _ -> ()
let init_check d = Interp.Register.check d (fun d t ->
diff --git a/src_colibri2/theories/FP/rounding_mode.mli b/src_colibri2/theories/FP/rounding_mode.mli
index 07d44840f8cd6f6e13c76968fe8c592c546f77e1..047ea2a1cc05ca046dd153e809df279e9ecb929b 100644
--- a/src_colibri2/theories/FP/rounding_mode.mli
+++ b/src_colibri2/theories/FP/rounding_mode.mli
@@ -18,6 +18,6 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-include Value.S with type s = Farith.mode
+include Value.S with type s = Farith2.mode
val init : Egraph.wt -> unit