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

[Farith] Extract generic version of floats and intervals

and use it in Fp theory for defining all formats
parent 2bdd961a
(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*)
......
(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))
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.
......@@ -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
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
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
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 ->