diff --git a/farith/.gitignore b/farith/.gitignore new file mode 100644 index 0000000000000000000000000000000000000000..4c8875a74a8327a1e83b505975f5a62ce2238ffc --- /dev/null +++ b/farith/.gitignore @@ -0,0 +1,10 @@ +/html/ +/tests/_local +/tests/*.log +/tests/*.diff +_build/ +*.native +*.vo +*.glob +.local +/farith.top diff --git a/farith/F.ml b/farith/F.ml new file mode 100644 index 0000000000000000000000000000000000000000..bb684ee401132876ad43e04f2f753d4100d62e24 --- /dev/null +++ b/farith/F.ml @@ -0,0 +1,364 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2007-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). *) +(* *) +(**************************************************************************) + +(* -------------------------------------------------------------------------- *) +(* --- Constructors --- *) +(* -------------------------------------------------------------------------- *) + +type t = Z.t * int + +let mantissa = fst +let exponent = snd + +let zero = Z.zero,0 +let one = Z.one,0 +let two = Z.one,1 + +let m8 = Z.of_int 255 (* mask for 8 1-bits 0b11111111 *) +let m4 = Z.of_int 15 (* mask for 4 1-bits 0b00001111 *) +let m2 = Z.of_int 3 (* mask for 2 1-bits 0b00000011 *) + +(* 0 is uniquely represented by [zero] *) + +let is_0mask a mask = Z.equal (Z.logand a mask) Z.zero + +let oddify a p = + if Z.equal a Z.zero then zero else + let reduce_1 a p = (* 1 zero-bit or less *) + if is_0mask a Z.one + then (Z.shift_right_trunc a 1 , p+1 ) + else (a,p) in + let reduce_2 a p = (* 3 zero-bits or less *) + if is_0mask a m2 + then reduce_1 (Z.shift_right_trunc a 2) (p+2) + else reduce_1 a p in + let reduce_4 a p = (* 7 zero-bits or less *) + if is_0mask a m4 + then reduce_2 (Z.shift_right_trunc a 4) (p+4) + else reduce_2 a p in + let rec reduce_8 a p = (* any number of zero-bits *) + if is_0mask a m8 + then reduce_8 (Z.shift_right_trunc a 8) (p+8) + else reduce_4 a p + in reduce_8 a p + +let equal (a,p) (b,q) = Z.equal a b && p = q + +let compare (a,p) (b,q) = + if a==b then compare p q else + let sa = Z.sign a in + let sb = Z.sign b in + if sa < 0 && sb > 0 then (-1) else + if sa > 0 && sb < 0 then 1 else + if p > q then Z.compare (Z.shift_left a (p-q)) b else + if p < q then Z.compare a (Z.shift_left b (q-p)) else + Z.compare a b + +let make = oddify + +(* -------------------------------------------------------------------------- *) +(* --- Ring Operations --- *) +(* -------------------------------------------------------------------------- *) + +let neg (a,p) = if Z.equal a Z.zero then zero else Z.neg a,p + +let add u v = + if u == zero then v else + if v == zero then u else + let (a,p) = u in + let (b,q) = v in + (* shift is even, mantissa is odd, + result is necessary odd (and non-null) *) + if p > q then Z.add (Z.shift_left a (p-q)) b , q else + if p < q then Z.add (Z.shift_left b (q-p)) a , p else + oddify (Z.add a b) p + +let sub u v = + if v == zero then u else + let (b,q) = v in + if u == zero then (Z.neg b,q) else + let (a,p) = u in + (* shift is even, mantissa is odd, + result is necessary odd (and non-null) *) + if p > q then Z.sub (Z.shift_left a (p-q)) b , q else + if p < q then Z.sub a (Z.shift_left b (q-p)) , p else + oddify (Z.sub a b) p + +let mul u v = + if u == zero || v == zero then zero else + let (a,p) = u in + let (b,q) = v in + (* multiplying two odds returns an odd *) + Z.mul a b , p+q + +let shift_left u n = if u == zero then zero else (fst u,snd u+n) +let shift_right u n = if u == zero then zero else (fst u,snd u-n) + +let power2 n = (Z.one,n) + +let cache = 128 +let powers = Array.init cache (Z.shift_left Z.one) +let zp2 k = if k < cache then powers.(k) else Z.shift_left Z.one k +let b32 = 24 +let b64 = 53 +let m32 = powers.(b32) +let m64 = powers.(b64) + +let rec log2_dicho a p q = + let r = (p + q) / 2 in + if r = p then q else + if Z.lt a (zp2 r) + then log2_dicho a p r + else log2_dicho a r q + +let log2_mantissa a = + let n = Z.size a in + let p = (n-1) lsl 6 in (* x64 *) + let q = n lsl 6 in + log2_dicho a p q + +let log2 (a,p) = + if Z.equal a Z.zero then 0 else + if Z.equal a Z.one then p else + p + log2_mantissa (Z.abs a) + +(* -------------------------------------------------------------------------- *) +(* --- Rounding Mode --- *) +(* -------------------------------------------------------------------------- *) + +let is_even z = is_0mask z Z.one + +type mode = + | NE (* Nearest to even *) + | ZR (* Toward zero *) + | DN (* Toward minus infinity *) + | UP (* Toward plus infinity *) + | NA (* Nearest away from zero *) + +type tie = Floor | Tie | Ceil (* positive tie-break *) + [@@ deriving show] + +let sign s a = if s then a else Z.neg a + +(* s:sign, a: absolute truncated *) +let choose mode tie s a = + match mode , tie with + | ZR , _ -> sign s a + | DN , _ -> if s then a else Z.neg (Z.succ a) + | UP , _ -> if s then Z.succ a else Z.neg a + | NA , Tie -> sign s (Z.succ a) + | NE , Tie -> sign s (if is_even a then a else Z.succ a) + | (NE|NA) , Floor -> sign s a + | (NE|NA) , Ceil -> sign s (Z.succ a) + +(* requires 2^n <= a *) +let truncate n a p tie = + let d = log2_mantissa a - n in + let mask = Z.pred (zp2 d) in + let half = zp2 (d-1) in + let r = Z.logand a mask in + let tie = + if Z.lt r half then Floor else + if Z.lt half r then Ceil else tie in + let a0 = Z.shift_right_trunc a d in + a0 , p + d , tie + +(* requires m = 2^n *) +let rounding mode n m ((a,p) as u) = + let a0 = Z.abs a in + (* a is odd, m is even *) + if Z.lt a0 m then u (* EXACT *) + else + let a0,p,tie = truncate n a0 p Tie in + let a = choose mode tie (0 < Z.sign a) a0 in + oddify a p + +let round ?(mode=NE) ?(bits=80) u = + rounding mode bits (zp2 bits) u + +let round_f32 ?(mode=NE) u = rounding mode b32 m32 u +let round_f64 ?(mode=NE) u = rounding mode b64 m64 u + +let seizing n m ((a,p) as u) = + let a0 = Z.abs a in + (* a is odd, m is even *) + if Z.lt a0 m then u,u (* EXACT *) + else + let a0,p,_ = truncate n a0 p Tie in + if 0 < Z.sign a then + oddify a0 p , oddify (Z.succ a0) p + else + let a0 = Z.neg a0 in + oddify (Z.pred a0) p , oddify a0 p + +let seize ?(bits=80) u = seizing bits (zp2 bits) u +let seize_f32 = seizing b32 m32 +let seize_f64 = seizing b64 m64 + +(* -------------------------------------------------------------------------- *) +(* --- Z Conversion --- *) +(* -------------------------------------------------------------------------- *) + +let of_zint a = oddify a 0 + +let to_zint (a,n) = + if n > 0 then Z.shift_left a n else + if n < 0 then Z.shift_right_trunc a n else a + +let of_int a = oddify (Z.of_int a) 0 +let to_int a = Z.to_int (to_zint a) + +(* -------------------------------------------------------------------------- *) +(* --- Q conversion --- *) +(* -------------------------------------------------------------------------- *) + +let to_qint (a,n) = + if n > 0 then Q.mul_2exp (Q.of_bigint a) n else + if n < 0 then Q.div_2exp (Q.of_bigint a) (-n) else + Q.of_bigint a + +let q_two = Q.of_int 2 + +(* invariant q.2^n, ensures 1 <= q < 2 *) +let rec magnitude q n = + if Q.lt q Q.one then magnitude (Q.mul_2exp q 1) (pred n) else + if Q.geq q q_two then magnitude (Q.div_2exp q 1) (succ n) else + (q,n) + +(* invariant m + q.2^n && 0 <= q < 1 *) +let rec decompose bits m q n = + if Q.equal q Q.zero || bits=0 then m,q else + let q = Q.mul_2exp q 1 in + let n = pred n in + let bits = pred bits in + if Q.lt q Q.one + then + decompose bits m q n + else + let m = add m (power2 n) in + let q = Q.sub q Q.one in + decompose bits m q n + +exception Undefined + +let half = Q.make Z.one (Z.of_int 2) + +let of_qexp ~mode ~bits r n = + (* having one more bit for further rounding *) + let q,n = magnitude (Q.abs r) n in + (* have r = q.2^n /\ 1 <= q < 2 *) + let ((a,p) as m),e = decompose bits (power2 n) (Q.sub q Q.one) n in + (* returns (m,e) such that m + e = 2^n + (q-1).2^n = r, 0<=e<1 *) + let sign = 0 < Q.sign r in + let tie = + if Q.lt e half then Floor else + if Q.gt e half then Ceil else Tie in + let m = zp2 bits in + let a,p,tie = + if Z.lt a m then a,p,tie + else truncate bits a p tie in + oddify (choose mode tie sign a) p + +let of_qint ?(mode=NE) ?(bits=80) r = + match Q.classify r with + | Q.ZERO -> zero + | Q.INF | Q.MINF | Q.UNDEF -> raise Undefined + | Q.NZERO -> of_qexp ~mode ~bits r 0 + +let div ?(mode=NE) ?(bits=80) a b = + if a == zero then zero else + if b == zero then raise Undefined else + if b = one then a else + let p,n = a in let q,m = b in + of_qexp ~mode ~bits (Q.make p q) (n-m) + +(* -------------------------------------------------------------------------- *) +(* --- Float Conversion --- *) +(* -------------------------------------------------------------------------- *) + +let f_sign = Int64.shift_left 1L 63 +let f_unit = Int64.shift_left 1L 52 +let f_mantissa = Int64.(sub f_unit 1L) +let f_exponent = Int64.(sub (shift_left 1L 11) 1L) + +let of_float u = + match classify_float u with + | FP_zero -> zero + | FP_nan | FP_infinite -> raise Undefined + | FP_normal -> + let a = Int64.bits_of_float u in + let m = Z.of_int64 (Int64.(add f_unit (logand a f_mantissa))) in + let e = Int64.(sub (logand (shift_right_logical a 52) f_exponent) 1075L) in + let s = Int64.(logand a f_sign) <> 0L in + oddify (if s then Z.neg m else m) (Int64.to_int e) + | FP_subnormal -> + let a = Int64.bits_of_float u in + let m = Z.of_int64 (Int64.(logand a f_mantissa)) in + let s = Int64.(logand a f_sign) <> 0L in + oddify (if s then Z.neg m else m) (-1074) + +let to_float ?(mode=NE) u = + if u == zero then 0.0 else + let (a,n) = rounding NE b64 m64 u in + Stdlib.ldexp (Z.to_float a) n + +(* -------------------------------------------------------------------------- *) +(* --- String Conversion --- *) +(* -------------------------------------------------------------------------- *) + +let pretty fmt (a,n) = + let s = Z.sign a in + if s = 0 then Format.pp_print_char fmt '0' else + begin + if s > 0 then Format.pp_print_char fmt '+' ; + Z.pp_print fmt a ; + if n <> 0 then + ( Format.pp_print_char fmt 'p' ; + Format.pp_print_int fmt n ) + end + +let to_string (a,n) = + let s = Z.sign a in + if s = 0 then "0" else + let buffer = Buffer.create 80 in + if s > 0 then Buffer.add_char buffer '-' ; + Z.bprint buffer a ; + if n <> 0 then + ( Buffer.add_char buffer 'p' ; + Buffer.add_string buffer (string_of_int n) ) ; + Buffer.contents buffer + +let of_string s = + try + let k = String.index s 'p' in + let m = String.sub s 0 k in + let e = String.sub s (succ k) (String.length s - k - 1) in + oddify (Z.of_string m) (int_of_string e) + with Not_found -> + oddify (Z.of_string s) 0 + +(* -------------------------------------------------------------------------- *) +(* --- Deriving --- *) +(* -------------------------------------------------------------------------- *) + +let pp = pretty +let show = to_string + +(* -------------------------------------------------------------------------- *) diff --git a/farith/F.mli b/farith/F.mli new file mode 100644 index 0000000000000000000000000000000000000000..3894d0da07041ac2cfdddb90cfd12f94cd624e40 --- /dev/null +++ b/farith/F.mli @@ -0,0 +1,119 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2007-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 [Zarith]) *) + +(** Rational numbers [m.2^n] where [m] is a [Zarith] integer and [n] an OCaml integer. *) +type t + +val zero : t +val one : t +val two : t + +val make : Z.t -> int -> t +(** The number [p.2^n]. *) + +val mantissa : t -> Z.t +val exponent : t -> int + +val equal : t -> t -> bool +val compare : t -> t -> int + +exception Undefined (** for undefined operations *) + +(** {3 Rounding} *) + +(** 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 *) + +val b32 : int (** mantissa of IEEE-32 [~bits:b32=24] *) +val b64 : int (** mantissa of IEEE-64 [~bits:b64=53] *) + +val round : ?mode:mode -> ?bits:int -> t -> t +(** Rounded to [bits] binary significant digits, twoard zero (defaults to 80). + Default rounding mode is [NE]. *) + +val round_f32 : ?mode:mode -> t -> t +(** Round to an IEEE float. Same as [round ~bits:28]. *) + +val round_f64 : ?mode:mode -> t -> t +(** Round to an IEEE double. Same as [round ~bits:54]. *) + +val seize : ?bits:int -> t -> t*t +(** Returns the two consecutive floats with [bits] precision around the given float. *) + +(** {3 Arithmetics} *) + +val neg : t -> t +val add : t -> t -> t +val sub : t -> t -> t +val mul : t -> t -> t +val div : ?mode:mode -> ?bits:int -> t -> t -> t +(** Division rounded to [bits] digits (default is 80). + The default rounding mode is [NE]. + @raise Undefined for division by zero. +*) + +val shift_left : t -> int -> t (** Multiply with a positive or negative power of 2. *) +val shift_right : t -> int -> t (** Divide by a positive or negative power of 2. *) + +val power2 : int -> t (** Return the positive or negative power of 2. *) +val log2 : t -> int (** Return the smallest upper bound in power of 2. *) + +(** {3 Conversion with Z} *) + +val of_zint : Z.t -> t (** Exact. *) +val to_zint : t -> Z.t (** Rounded towards 0. *) + +(** {3 Conversion with Q} *) + +val of_qint : ?mode:mode -> ?bits:int -> Q.t -> t +(** Rounded to [bits] binary digits (default 80). *) + +val to_qint : t -> Q.t (** Exact. *) + +(** {3 Conversion with OCaml integers} *) + +val of_int : int -> t (** Exact. *) +val to_int : t -> int (** Fractional part is truncated. *) + +(** {3 Conversion with OCaml floats} *) + +val of_float : float -> t (** Exact. @raise Undefined for NaN and infinites. *) +val to_float : ?mode:mode -> t -> float (** Rounded with default mode [NE]. *) + +(** {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 of_string : string -> t +val to_string : t -> string +val pretty : Format.formatter -> t -> unit + +val pp : Format.formatter -> t -> unit (** Alias for pretty (deriving) *) +val show : t -> string (** Alias for to_string (deriving) *) diff --git a/farith/F_aux.v b/farith/F_aux.v new file mode 100644 index 0000000000000000000000000000000000000000..69eb015244fbf34c28adeab16cf0ae516fa7ff92 --- /dev/null +++ b/farith/F_aux.v @@ -0,0 +1,1108 @@ +(**************************************************************************) +(* 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). *) +(* *) +(**************************************************************************) + +Require Import Flocq.Core.Fcore. +Require Import Flocq.Appli.Fappli_IEEE. +Require Import Flocq.Appli.Fappli_IEEE_bits. +Require Import QArith. +Require Import Qreals. +Require Import Reals. +Require Import ZBits. +Require Coq.Arith.Wf_nat. + +Parameter assert : forall (b:bool) (t:Type), ((b=true) -> t) -> t. + +Fixpoint least_bit_Pnat (n : positive) := + match n with + | xH => O + | xO p => S (least_bit_Pnat p) + | xI p => O + end. + +Definition shiftr_pos a p := Wf_nat.iter_nat p _ Z.div2 a. + +Lemma shiftr_pos_is_shiftr : + forall a p, shiftr_pos a p = Z.shiftr a (Z.of_nat p). +Proof. + intros. + destruct p. + reflexivity. + unfold shiftr_pos, Z.shiftr, Z.shiftl, Z.of_nat, Z.opp. + rewrite Pos2Nat.inj_iter. + rewrite SuccNat2Pos.id_succ. + reflexivity. +Qed. + +(** Q of ocaml zarith *) +Record Qz := Qzmake { num : Z.t; den : Z.t; + Hden1 : (0 <=? den)%Z = true; + Hden2 : (if den =? 0 then orb (orb (num =? -1) (num =? 0)) (num =? 1) else Z.gcd num den =? 1)%Z = true + }. + +Lemma Hden2' : + forall q, (den q = 0 -> num q = -1 \/ num q = 0 \/ num q = 1)%Z. +Proof. + intros q H. + rewrite <- !Z.eqb_eq in *. + assert (H2 := Hden2 q). + rewrite H in H2. + destruct (num q =? -1)%Z; destruct (num q =? 0)%Z; destruct (num q =? 1)%Z; + tauto. +Qed. + +Definition Qz_zero := Qzmake 0%Z 1%Z (refl_equal _) (refl_equal _). +Definition Qz_undef := Qzmake 0%Z 0%Z (refl_equal _) (refl_equal _). +Definition Qz_inf := Qzmake 1%Z 0%Z (refl_equal _) (refl_equal _). +Definition Qz_minus_inf := Qzmake (-1)%Z 0%Z (refl_equal _) (refl_equal _). + +Inductive Rplus {A:Type} := + | Rp_finite : R -> Rplus + | Rp_nan : A -> Rplus + | Rp_infinity : bool -> Rplus. + +Definition Qz2Rplus q : Rplus := + if (den q =? 0)%Z then + if (num q =? 0)%Z then Rp_nan tt + else Rp_infinity (num q <? 0)%Z + else Rp_finite (Q2R (Qmake (num q) (Z.to_pos (den q)))). + +Fact Qz_zero_correct : Qz2Rplus Qz_zero = Rp_finite 0%R. +Proof. + compute; rewrite Rmult_0_l; reflexivity. +Qed. + +Fact Qz_undef_correct : Qz2Rplus Qz_undef = Rp_nan tt. +Proof. + compute. reflexivity. +Qed. + +Fact Qz_inf_correct : Qz2Rplus Qz_inf = Rp_infinity false. +Proof. + compute. reflexivity. +Qed. + +Fact Qz_minus_inf_correct : Qz2Rplus Qz_minus_inf = Rp_infinity true. +Proof. + compute. reflexivity. +Qed. + +Inductive Qz_kind (q:Qz) := (* cf Q of Zarith *) + | Qz_INF: (num q = 1)%Z -> (den q = 0)%Z -> Qz_kind q + | Qz_MINF: (num q = -1)%Z -> (den q = 0)%Z -> Qz_kind q + | Qz_UNDEF: (num q = 0)%Z -> (den q = 0)%Z -> Qz_kind q + | Qz_ZERO: (num q = 0)%Z -> forall pq, (den q = Z.pos pq)%Z -> Qz_kind q + | Qz_NZERO: forall nq (s:{num q = Z.pos nq} + {num q = Z.neg nq}) pq, (den q = Z.pos pq)%Z -> Qz_kind q. + +Extraction Implicit Qz_ZERO [pq]. +Extraction Implicit Qz_NZERO [nq s pq]. + +Lemma Qz_classify (q:Qz) : Qz_kind q. +Proof. + intros. + case_eq (den q); [intros Hd | intros pd Hd| intros nd Hd]. + - case_eq (num q); [intros Hn | intros pn Hn| intros nn Hn]. + * exact (Qz_UNDEF q Hn Hd). + * assert (H: num q = ( 1)%Z) by (destruct (Hden2' q Hd) as [H|[H|H]]; rewrite Hn in *; + [discriminate H| discriminate H | assumption ]). + exact (Qz_INF q H Hd). + * assert (H: num q = (-1)%Z) by (destruct (Hden2' q Hd) as [H|[H|H]]; rewrite Hn in *; + [assumption| discriminate H | discriminate H]). + exact (Qz_MINF q H Hd). + - case_eq (num q); [intros Hn | intros nq Hn| intros nq Hn]. + * exact (Qz_ZERO q Hn pd Hd). + * exact (Qz_NZERO q nq (left Hn) pd Hd). + * exact (Qz_NZERO q nq (right Hn) pd Hd). + - assert (A := Hden1 q). + rewrite Hd in A. + discriminate A. +Defined. + +Definition B2Rplus prec emax (f:binary_float prec emax) : Rplus := + match f with + | B754_zero _ _ _ => Rp_finite 0%R + | B754_infinity _ _ b => Rp_infinity b + | B754_nan _ _ b pl => Rp_nan (b,pl) + | B754_finite _ _ _ _ _ _ => Rp_finite (B2R prec emax f) + end. + +Definition int_native bw := { i | match Z.shiftr i (bw-1) with + | 0%Z | (-1)%Z => True + | _ => False + end }. +Definition int31 := int_native 31. +Definition int31_zero : int31 := exist _ 0%Z I. +Definition int31_one : int31 := exist _ 1%Z I. +Definition int31_minus_one : int31 := exist _ (-1)%Z I. + +(* +Definition int31_max_int : int63 := exist _ (iter_nat Z.succ_double 62 0)%Z I. +Definition int31_min_int : int63 := exist _ (iter_nat Z.pred_double 62 0 - 1)%Z I. + +Definition int63 := int_native 63. +Definition int63_zero : int63 := exist _ 0%Z I. +Definition int63_one : int63 := exist _ 1%Z I. +Definition int63_minus_one : int63 := exist _ (-1)%Z I. +Definition int63_max_int : int63 := exist _ (iter_nat Z.succ_double 62 0)%Z I. +Definition int63_min_int : int63 := exist _ (iter_nat Z.pred_double 62 0 - 1)%Z I. +*) + +(** 31 or 63 *) +Parameter nativeint : Type. +Parameter nativeint_zero : nativeint. +Parameter nativeint_one : nativeint. +Parameter nativeint_three : nativeint. +Parameter nativeint_five : nativeint. +Parameter hash_z: Z.t -> nativeint. +Parameter hash_bool: bool -> nativeint. +Parameter hash_combine: nativeint -> nativeint -> nativeint. + + +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. *) + +Record fconf (t:Type) := + FConf { mw : Z ; + ew : Z; + Hmw : (0 < mw)%Z; + Hew : (0 < ew)%Z; + Hemax : (cprec mw < cemax ew)%Z; + Hprec : (0 < cprec mw)%Z; + Ht : t = binary_float (cprec mw) (cemax ew) + }. + +Definition check_param mw ew := + andb (andb (0 <? mw)%Z (0 <? ew)%Z) (cprec mw <? cemax ew)%Z. + +Definition mk_conf : forall mw ew, check_param mw ew = true -> fconf (binary_float (cprec mw) (cemax ew)). +Proof. + intros mw ew H. + refine (FConf _ mw ew _ _ _ _ (refl_equal _)); + unfold check_param in H; + rewrite !Bool.andb_true_iff in H; + rewrite <- !Zlt_is_lt_bool in H; + intuition. +Defined. + + +(** +We defined two way to access the library +D: by function application (ew, mw in conf) +Make: by functor application (ew, mw in the parameter module) + +The code is factorized in Aux that is used by the two solutions. + +*) + +Module Aux. + +Section Direct. + Variable t' : Type. + Variable conf : fconf t'. + + + Let mw : Z := mw t' conf. + Let ew : Z := ew t' conf. + Let prec := cprec mw. + Let emax := cemax ew. + Let t := binary_float prec emax. + + Implicit Arguments B754_nan [[prec] [emax]]. + Implicit Arguments B754_zero [[prec] [emax]]. + Implicit Arguments B754_infinity [[prec] [emax]]. + Implicit Arguments B754_finite [[prec] [emax]]. + + Let Hmw : (0 < mw)%Z := Hmw t' conf. + Let Hew : (0 < ew)%Z := Hew t' conf. + Let Hemax : (cprec mw < cemax ew)%Z := Hemax t' conf. + Let Hprec : (0 < cprec mw)%Z := Hprec t' conf. + + Definition pl_cst := (Fcore_Zaux.iter_nat xO (Z.to_nat (Z.pred mw)) xH)%Z. + + Lemma pl_valid : (Z.pos (Fcore_digits.digits2_pos pl_cst) <? prec)%Z = true. + Proof. + assert (G:forall n, Fcore_digits.digits2_Pnat (iter_nat xO n xH)%Z = n). + - induction n. + * reflexivity. + * rewrite iter_nat_S; simpl. + rewrite IHn; reflexivity. + - rewrite Fcore_digits.Zpos_digits2_pos. + rewrite <- Fcore_digits.Z_of_nat_S_digits2_Pnat. + unfold pl_cst, prec, cprec. + rewrite G;clear G. + rewrite Nat2Z.inj_succ. + rewrite Z2Nat.id;[rewrite Z.ltb_lt | ]; omega. + Qed. + + Definition default_nan_pl : bool * nan_pl prec := + (false, exist _ pl_cst pl_valid). + + Definition unop_nan_pl (f : t) : bool * nan_pl prec := + match f with + | B754_nan s pl => (s, pl) + | _ => default_nan_pl + end. + + Definition binop_nan_pl (f1 f2 : t) : bool * nan_pl prec := + match f1, f2 with + | B754_nan s1 pl1, _ => (s1, pl1) + | _, B754_nan s2 pl2 => (s2, pl2) + | _, _ => default_nan_pl + end. + + Definition opp := Bopp prec emax pair. + Definition add := Bplus _ _ Hprec Hemax binop_nan_pl. + Definition sub := Bminus _ _ Hprec Hemax binop_nan_pl. + Definition mul := Bmult _ _ Hprec Hemax binop_nan_pl. + Definition div := Bdiv _ _ Hprec Hemax binop_nan_pl. + Definition sqrt := Bsqrt _ _ Hprec Hemax unop_nan_pl. + Definition abs := Babs prec emax (fun b x => (b,x)). + + Definition of_bits := binary_float_of_bits mw ew Hmw Hew Hemax. + Definition to_bits := bits_of_binary_float mw ew. + + Let emin := (3 - emax - prec)%Z. + Let fexp := FLT_exp emin prec. + + Definition of_correct mode szero r (f:t) := + if Rlt_bool (Rabs (round radix2 fexp (round_mode mode) r)) (bpow radix2 emax) then + B2R _ _ f = round radix2 fexp (round_mode mode) r /\ + is_finite _ _ f = true /\ + Bsign _ _ f = + match Rcompare r 0 with + | Eq => szero + | Lt => true + | Gt => false + end + else + B2FF _ _ f = binary_overflow prec emax mode + (match Rcompare r 0 with Lt => true | _ => false end). + + (** just check that we have the good definition *) + Lemma binary_normalize_correct': + forall m mx ex szero, + of_correct m szero + (F2R (Float radix2 mx ex)) + (binary_normalize _ _ Hprec Hemax m mx ex szero). + Proof. + exact (binary_normalize_correct _ _ Hprec Hemax). + Qed. + + Lemma F2R_neg: + forall radix px ex, + Rcompare (F2R (Float radix (Z.neg px) ex)) 0%R = Lt. + Proof. + intros; apply Rcompare_Lt; apply F2R_lt_0_compat; reflexivity. + Qed. + + Lemma F2R_pos: + forall radix px ex, + Rcompare (F2R (Float radix (Z.pos px) ex)) 0%R = Gt. + Proof. + intros; apply Rcompare_Gt; apply F2R_gt_0_compat; reflexivity. + Qed. + + Lemma Rcompare_div_compat: + forall x y, + (y <> 0 -> Rcompare (x / y) 0 = + match (Rcompare x 0, Rcompare y 0) with + | (Eq, _) => Eq + | (Lt, Lt) => Gt + | (Gt, Gt) => Gt + | (Lt, Gt) => Lt + | (Gt, Lt) => Lt + | (_,Eq) => Eq (* absurd *) + end)%R. + Proof. + intros x y Py. + destruct (Rcompare_spec x 0) as [Hx|Hx|Hx]; + destruct (Rcompare_spec y 0) as [Hy|Hy|Hy]; + (try (apply Rcompare_Gt); try (apply Rcompare_Lt); try (apply Rcompare_Eq)). + - apply Rgt_lt. + rewrite <- (Rmult_0_r x). + apply (Rmult_lt_gt_compat_neg_l x (/y)%R 0%R Hx). + exact (Rinv_lt_0_compat _ Hy). + - rewrite Hy in Py. + destruct (Py (refl_equal _)). + - apply Rgt_lt. + rewrite <- (Rmult_0_l (/y)). + refine (Rmult_lt_compat_r _ _ _ _ Hx). + exact (Rinv_0_lt_compat _ Hy). + - rewrite Hx. unfold Rdiv. + rewrite Rmult_0_l. + reflexivity. + - rewrite Hx. unfold Rdiv. + rewrite Rmult_0_l. + reflexivity. + - rewrite Hx. unfold Rdiv. + rewrite Rmult_0_l. + reflexivity. + - rewrite <- (Rmult_0_r x). + refine (Rmult_lt_compat_l _ _ _ Hx _). + exact (Rinv_lt_0_compat _ Hy). + - rewrite Hy in Py. + destruct (Py (refl_equal _)). + - rewrite <- (Rmult_0_r x). + refine (Rmult_lt_compat_l _ _ _ Hx _). + exact (Rinv_0_lt_compat _ Hy). + Qed. + + Lemma Bdiv_correct_aux' : + forall m sx mx ex sy my ey, + let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in + let y := F2R (Float radix2 (cond_Zopp sy (Zpos my)) ey) in + of_correct m false (x/y) + (FF2B _ _ _ (proj1 (Bdiv_correct_aux _ _ Hprec Hemax + m sx mx ex sy my ey))). + Proof. + intros. + destruct Bdiv_correct_aux as [valid correct]. + unfold of_correct. + fold x y emax prec emin fexp in valid, correct |- *. + set (z := match Fdiv_core_binary prec (' mx) ex (' my) ey with + | (0%Z, _, _) => F754_nan false 1 + | ((' mz0)%Z, ez, lz) => + binary_round_aux prec emax m (xorb sx sy) mz0 ez lz + | (Z.neg _, _, _) => F754_nan false 1 + end) in *. + destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode m) (x / y))) + (bpow radix2 emax)). + destruct correct as [ cround [cfinite csign] ]. + split;[|split]. + - rewrite <- cround. + apply B2R_FF2B. + - destruct z; trivial. + - destruct sx; destruct sy; + assert (Hy : (y <> 0)%R) by (destruct (Req_dec y 0%R) as [H|H];[apply F2R_eq_0_reg in H; discriminate| assumption]); simpl in *; + rewrite (Rcompare_div_compat _ _ Hy); + (unfold x, y; + try rewrite (F2R_neg radix2 mx ex); try rewrite (F2R_pos radix2 mx ex); + try rewrite (F2R_neg radix2 my ey); try rewrite (F2R_pos radix2 my ey); + (** *) + rewrite Bsign_FF2B; + exact csign). + - destruct sx; destruct sy; + assert (Hy : (y <> 0)%R) by (destruct (Req_dec y 0%R) as [H|H];[apply F2R_eq_0_reg in H; discriminate| assumption]); simpl in *; + rewrite (Rcompare_div_compat _ _ Hy); + unfold x, y; + try rewrite (F2R_neg radix2 mx ex); try rewrite (F2R_pos radix2 mx ex); + try rewrite (F2R_neg radix2 my ey); try rewrite (F2R_pos radix2 my ey); + (** *) + rewrite B2FF_FF2B; + exact correct. + Qed. + + + Definition of_z mode z : t := binary_normalize _ _ Hprec Hemax mode z 0%Z false. + + Theorem of_z_correct : + forall mode z, of_correct mode false (Z2R z) (of_z mode z). + Proof. + intros mode z. + replace (Z2R z) with (F2R (Float radix2 z 0%Z)). + exact (binary_normalize_correct _ _ Hprec Hemax mode z 0%Z false). + unfold F2R; simpl. + apply Rmult_1_r. + Qed. + + Definition default_nan : t := B754_nan (fst default_nan_pl) (snd default_nan_pl). + + Definition of_q mode q : t := + match Qz_classify q with + | Qz_ZERO _ _ _ _ => B754_zero false + | Qz_INF _ _ _ => B754_infinity false + | Qz_MINF _ _ _ => B754_infinity true + | Qz_UNDEF _ _ _ => default_nan + | Qz_NZERO _ _ _ _ _ => + match num q with + | Z0 => default_nan (** absurd *) + | Z.pos pn => + FF2B _ _ _ (proj1 (Bdiv_correct_aux _ _ Hprec Hemax + mode + false pn 0%Z + false (Z.to_pos (den q)) 0%Z)) + | Z.neg nn => + FF2B _ _ _ (proj1 (Bdiv_correct_aux _ _ Hprec Hemax + mode + true nn 0%Z + false (Z.to_pos (den q)) 0%Z)) + end + end. + + Theorem of_q_correct : + forall mode q, + match Qz2Rplus q with + | Rp_nan tt => of_q mode q = default_nan + | Rp_infinity b => of_q mode q = B754_infinity b + | Rp_finite r => of_correct mode false r (of_q mode q) + end. + Proof. + intros. + unfold of_q, Qz2Rplus; destruct (Qz_classify q). + - rewrite e; rewrite e0. + reflexivity. + - rewrite e; rewrite e0. + reflexivity. + - rewrite e; rewrite e0. + reflexivity. + - rewrite e; rewrite e0; clear e e0. + unfold Q2R; simpl. + rewrite Rmult_0_l. + unfold of_correct. + rewrite (round_0 radix2 fexp (round_mode mode)). + rewrite Rabs_R0. + assert (H := bpow_gt_0 radix2 emax). + apply Rlt_bool_true in H. + rewrite H. + rewrite (Rcompare_Eq _ _ (refl_equal _)). + tauto. + - destruct s; rewrite e0; rewrite e; simpl. + * replace (Q2R (' 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. + + Lemma least_bit_shiftr_pos : + forall m (b:bool), + let e' := least_bit_Pnat m in + let m' := if b then Z.neg m else Z.pos m in + let m'' := shiftr_pos m' e' in + Z.odd m'' = true. + Proof. + induction m; intro b. + - destruct b;reflexivity. + - assert (H:= IHm b); + destruct b; + replace (least_bit_Pnat m~0) with (S (least_bit_Pnat m)) in * by reflexivity; + intros e' m'; + replace (shiftr_pos m' e') with (shiftr_pos (Z.div2 m') (least_bit_Pnat m)) by + (unfold shiftr_pos, e'; rewrite nat_rect_succ_r; reflexivity). + * replace (Z.div2 m') with (Z.neg m) by reflexivity. + exact H. + * replace (Z.div2 m') with (Z.pos m) by reflexivity. + exact H. + - destruct b; reflexivity. + Qed. + + Lemma gcd_odd_pow_2: + forall (m:positive) n, + match m with xO _ => False | _ => True end -> + Pos.gcd m (Pos.shiftl 1%positive (Npos n)) = 1%positive. + Proof. + destruct m as [p|p|]; intros n H; destruct H; simpl. + - induction n using Pos.peano_ind. + * compute [Pos.iter Z.mul Pos.mul]. + unfold Pos.gcd. + replace (Pos.size_nat 2) with 2 by reflexivity. + simpl. + replace (Pos.size_nat p + 2)%nat with (S (S (Pos.size_nat p))) by auto with *. + reflexivity. + * rewrite Pos.iter_succ. + unfold Pos.gcd. + simpl. + replace (Pos.size_nat p + S (Pos.size_nat (Pos.iter xO 1%positive n)))%nat + with (S (Pos.size_nat p + Pos.size_nat (Pos.iter xO 1%positive n))) by auto with *. + exact IHn. + - unfold Pos.gcd. + reflexivity. + Qed. + + Lemma to_q (f:t) : Qz. + Proof. + refine (match f with + | B754_zero _ => Qz_zero + | B754_infinity b => if b then Qz_minus_inf else Qz_inf + | B754_nan _ _ => Qz_undef + | B754_finite b m e _ => + let e' := least_bit_Pnat m in + let m' := if b then Z.neg m else Z.pos m in + let e'' := (e + (Z.of_nat e'))%Z in + match e'' with + | Z0 => Qzmake (shiftr_pos m' e') 1%Z (refl_equal _) _ + | Z.pos _ => Qzmake (Z.shiftl m' e)%Z 1%Z (refl_equal _) _ + | Z.neg p => Qzmake (shiftr_pos m' e') (Z.shiftl 1%Z (Z.pos p)) _ _ + end + end + ). + - rewrite Z.gcd_1_r. + reflexivity. + - rewrite Z.gcd_1_r. + reflexivity. + - rewrite Z.shiftl_1_l. + apply Z.leb_le. + apply Z.lt_le_incl. + apply Zpower_pos_gt_0. + reflexivity. + - assert (Z.shiftl 1 (Z.pos p) =? 0 = false)%Z by + (rewrite Z.shiftl_1_l; + apply Z.eqb_neq; + apply Z.neq_sym; + apply Z.lt_neq; + exact (Zpower_pos_gt_0 2%Z p (refl_equal _))). + rewrite H. + assert (Z.odd (shiftr_pos m' e') = true) by (exact (least_bit_shiftr_pos m b)). + destruct (shiftr_pos m' e'); clear H e0 e' m' e''. + discriminate H0. + rewrite <- (shift_equiv _ _ (Pos2Z.is_nonneg _)). + replace (shift (' p) 1) with (shift_pos p 1%positive) by reflexivity. + rewrite shift_pos_equiv. + compute [Z.gcd]. + rewrite gcd_odd_pow_2. + reflexivity. + unfold Z.odd in H0. + destruct p0; [exact I| discriminate H0| exact I]. + rewrite <- (shift_equiv _ _ (Pos2Z.is_nonneg _)). + replace (shift (' p) 1) with (shift_pos p 1%positive) by reflexivity. + rewrite shift_pos_equiv. + compute [Z.gcd]. + rewrite gcd_odd_pow_2. + reflexivity. + unfold Z.odd in H0. + destruct p0; [exact I| discriminate H0| exact I]. + Defined. + + (* + Lemma to_q_correct: + forall (f:t), + is_finite _ _ f = true -> + Qz2Rplus (to_q f) = Rp_finite (B2R _ _ f). + Proof. + intros f H; destruct f; try discriminate H; clear H. + - exact Qz_zero_correct. + - compute [B2R to_q]. + case_eq (e + Z.of_nat (least_bit_Pnat m))%Z; intro H. + * rewrite shiftr_pos_is_shiftr. + rewrite Z.shiftr_div_pow2. + compute [cond_Zopp Z.opp]. + compute [Qz2Rplus den num Z.eqb Z.to_pos]. + compute [Q2R F2R Fnum Fexp Qnum Qden]. + rewrite <- Z2R_IZR. + rewrite <- Z2R_IZR. + + rewrite Rinv_1. + rewrite Rmult_1_r. + rewrite Z2R_div. + replace 2%Z with (radix_val radix2) by reflexivity. + rewrite Z2R_Zpower. + simpl. + reflexivity. + simpl. + rewrite Z2R_Zpower_pos. + bpow_powerRZ + compute [F2R Fnu]. + simpl. + unfold cond_Zopp. + fold cond_Zopp. + destruct e. + simpl. + auto with *. + compute. + rewrite shifl_pos_is_shiftl_on_pos. + rewrite Z.shiftl_1_l. + simpl. + + rewrite Z.shiftl_mul_pow2. + rewrite Z.shiftl_1_l. + compute [Qz2Rplus den num Z.eqb Z.to_pos]. + destruct b. + compute [Q2R F2R Fnum Fexp Qnum Qden]. + rewrite shiftr_pos_is_shiftr. + Qed. + *) + + Definition compare_aux (f1 f2 : t) : comparison := + let cmp_bool b1 b2 := + match b1,b2 with + | true, true | false, false => Eq + | true, false => Lt + | false, true => Gt + end in + match f1, f2 with + | B754_nan b1 (exist _ pl1 _),B754_nan b2 (exist _ pl2 _) => + match cmp_bool b1 b2 with + | Eq => Pos.compare pl1 pl2 + | r => r + end + | B754_nan _ _,_ => Lt + | _,B754_nan _ _ => Gt + | B754_infinity true, B754_infinity true + | B754_infinity false, B754_infinity false => Eq + | B754_infinity true, _ => Lt + | B754_infinity false, _ => Gt + | _, B754_infinity true => Gt + | _, B754_infinity false => Lt + | B754_finite true _ _ _, B754_zero _ => Lt + | B754_finite false _ _ _, B754_zero _ => Gt + | B754_zero _, B754_finite true _ _ _ => Gt + | B754_zero _, B754_finite false _ _ _ => Lt + | B754_zero b1, B754_zero b2 => cmp_bool b1 b2 + | B754_finite s1 m1 e1 _, B754_finite s2 m2 e2 _ => + match s1, s2 with + | true, false => Lt + | false, true => Gt + | false, false => + match Zcompare e1 e2 with + | Lt => Lt + | Gt => Gt + | Eq => (Pos.compare m1 m2) + end + | true, true => + match Zcompare e1 e2 with + | Lt => Gt + | Gt => Lt + | Eq => (CompOpp (Pos.compare m1 m2)) + end + end + end. + + + Theorem Bcompare2_correct : + forall f1 f2, + is_finite prec emax f1 = true -> is_finite prec emax f2 = true -> + match f1,f2 with B754_zero _, B754_zero _ => False | _,_ => True end -> + compare_aux f1 f2 = Rcompare (B2R prec emax f1) (B2R prec emax f2). + Proof. + intros f1 f2 Hf1 Hf2 NoZeroZero. + assert (T := Bcompare_correct prec emax f1 f2 Hf1 Hf2). + destruct f1; destruct f2; try (destruct NoZeroZero); + try discriminate; + destruct b; destruct b0; try (injection T; trivial); + simpl in *; try destruct (e ?= e1)%Z; try (injection T; trivial). + Qed. + + Theorem compare_antisym : + forall f1 f2, compare_aux f1 f2 = CompOpp (compare_aux f2 f1). + Proof. + intros f1 f2. + destruct f1; destruct f2; simpl; try reflexivity; + destruct b; destruct b0; simpl; try reflexivity; + (** nan nan *) + try destruct n; try destruct n0; try exact (Pos.compare_antisym x0 x); + (** finite *) + try (rewrite (Z.compare_antisym e e1); destruct (e ?= e1)%Z); simpl; try reflexivity; + try (rewrite (Pos.compare_antisym m0 m); destruct (Pos.compare_antisym m m0)%Z); try reflexivity. + Qed. + + Theorem compare_refl : + forall f, compare_aux f f = Eq. + Proof. + intros f. + destruct f; simpl; try reflexivity; + destruct b; simpl; try reflexivity; + (** nan nan *) + try destruct n; try destruct n0; try exact (Pos.compare_refl x); + (** finite *) + rewrite Z.compare_refl; rewrite Pos.compare_refl; try reflexivity. + Qed. + + Definition compare f1 f2 := match compare_aux f1 f2 with + | Eq => int31_zero + | Lt => int31_minus_one + | Gt => int31_one + end. + + Theorem compare_correct : + forall f1 f2, + let (x,_) := compare f1 f2 in + Z.compare x 0 = compare_aux f1 f2. + Proof. + intros. unfold compare. + destruct (compare_aux f1 f2); reflexivity. + Qed. + + Definition equal f1 f2 := match compare_aux f1 f2 with + | Eq => true + | _ => false + end. + + Definition hash (f1:t) := + match f1 with + | B754_zero b => + hash_bool b + | B754_infinity b => + hash_combine nativeint_three (hash_bool b) + | B754_nan b (exist _ n _) => + hash_combine nativeint_five (hash_combine (hash_z (Z.pos n)) (hash_bool b)) + | B754_finite b m e _ => + hash_combine (hash_z (Z.pos m)) (hash_combine (hash_z e) (hash_bool b)) + end. + + Theorem hash_correct : + forall f1 f2, compare_aux f1 f2 = Eq -> hash f1 = hash f2. + Proof. + intros f1 f2 H. + destruct f1 as [[ ] | [ ] | [ ] [nan1 ] | [ ] m1 e1 ]; destruct f2 as [[ ] | [ ] | [ ] [nan2 ] | [ ] m2 e2 ]; compute -[Pos.compare Zcompare] in H; try discriminate; try reflexivity; compute. + + rewrite (Pos.compare_eq _ _ H). reflexivity. + + rewrite (Pos.compare_eq _ _ H). reflexivity. + + destruct (Z.compare_spec e1 e2). + * rewrite H0. rewrite (Pos.compare_eq m1 m2). reflexivity. + destruct (m1 ?= m2)%positive; try discriminate; try reflexivity. + * discriminate. + * discriminate. + + destruct (Z.compare_spec e1 e2). + * rewrite H0. rewrite (Pos.compare_eq m1 m2). reflexivity. + destruct (m1 ?= m2)%positive; try discriminate; try reflexivity. + * discriminate. + * discriminate. + Qed. + + Definition fcompare f1 f2 := match Bcompare prec emax f1 f2 with + | None => None + | Some Eq => Some int31_zero + | Some Lt => Some int31_minus_one + | Some Gt => Some int31_one + end. + + Theorem fcompare_correct : + forall f1 f2, + is_finite prec emax f1 = true -> is_finite prec emax f2 = true -> + match fcompare f1 f2 with + | Some (exist _ x _) => Z.compare x 0 = Rcompare (B2R prec emax f1) (B2R prec emax f2) + | None => False + end. + Proof. + intros f1 f2 Hf1 Hf2. + unfold fcompare. + assert (T := Bcompare_correct prec emax f1 f2 Hf1 Hf2). + destruct (Bcompare prec emax f1 f2) as [ o | ]. + - injection T; clear T; intro T; rewrite <- T; clear T. + destruct o as [e|e|e]; reflexivity. + - discriminate T. + Qed. + + Definition cmp_correct (fcmp : t -> t -> bool) rcmp := + forall f1 f2, + is_finite prec emax f1 = true -> is_finite prec emax f2 = true -> + (fcmp f1 f2 = true <-> rcmp (B2R prec emax f1) (B2R prec emax f2)). + + Ltac cmp_correct_fast fcmp rcmp := + intros f1 f2 Hf1 Hf2; + assert (T := Bcompare_correct prec emax f1 f2 Hf1 Hf2); + unfold fcmp; try unfold rcmp; + destruct (Rcompare_spec (B2R prec emax f1) (B2R prec emax f2)); + rewrite T; + assert (antisym := Rlt_asym (B2R prec emax f1) (B2R prec emax f2)); + assert (notrefl1 := Rlt_not_eq (B2R prec emax f1) (B2R prec emax f2)); + assert (notrefl2 := Rgt_not_eq (B2R prec emax f1) (B2R prec emax f2)); + intuition (try discriminate; trivial). + + Definition le f1 f2 := match Bcompare prec emax f1 f2 with + | None => false + | Some Eq => true + | Some Lt => true + | Some Gt => false + end. + + Theorem le_correct : cmp_correct le Rle. + Proof. + cmp_correct_fast le Rle. + Qed. + + Definition lt f1 f2 := match Bcompare prec emax f1 f2 with + | None => false + | Some Eq => false + | Some Lt => true + | Some Gt => false + end. + + Theorem lt_correct : cmp_correct lt Rlt. + Proof. + cmp_correct_fast lt Rlt. + Qed. + + Definition ge f1 f2 := match Bcompare prec emax f1 f2 with + | None => false + | Some Eq => true + | Some Lt => false + | Some Gt => true + end. + + Theorem ge_correct : cmp_correct ge Rge. + Proof. + cmp_correct_fast ge Rge. + Qed. + + Definition gt f1 f2 := match Bcompare prec emax f1 f2 with + | None => false + | Some Eq => false + | Some Lt => false + | Some Gt => true + end. + + Theorem gt_correct : cmp_correct gt Rgt. + Proof. + cmp_correct_fast gt Rgt. + Qed. + + Definition eq f1 f2 := match Bcompare prec emax f1 f2 with + | None => false + | Some Eq => true + | Some Lt => false + | Some Gt => false + end. + + Theorem eq_correct : cmp_correct eq Logic.eq. + Proof. + cmp_correct_fast eq (Logic.eq R R). + Qed. + + Definition neq f1 f2 := match Bcompare prec emax f1 f2 with + | None => true + | Some Eq => false + | Some Lt => true + | Some Gt => true + end. + + Theorem neq_correct : cmp_correct neq (fun r1 r2 => ~Logic.eq r1 r2). + Proof. + cmp_correct_fast neq (fun (r1:R) (r2:R) => ~Logic.eq r1 r2). + Qed. + + Definition infinity b : t := B754_infinity b. + Definition infp : t := B754_infinity false. + Definition infm : t := B754_infinity true. + Definition zero b : t := B754_zero b. + Definition zerop : t := B754_zero false. + Definition nan b pl : t := + let pl := assert ( 0 <? pl )%Z _ + (fun _ => Z.to_pos pl) in + let pl := assert (Zpos (Fcore_digits.digits2_pos pl) <? prec)%Z _ + (fun H => exist _ pl H) in + B754_nan b pl. + + Definition finite mode m e : t := + binary_normalize _ _ Hprec Hemax mode m e false. + + Definition classify : t -> Fappli_IEEE.full_float := B2FF prec emax. +End Direct. +End Aux. + +Module D. +Section Direct. + Variable t : Type. + Variable conf: fconf t. + + Ltac rewrite_type f := + rewrite (Ht t conf); exact (f t conf). + + Definition opp : t -> t. Proof. rewrite_type Aux.opp. Defined. + Definition add : mode -> t -> t -> t. Proof. rewrite_type Aux.add. Defined. + Definition sub : mode -> t -> t -> t. Proof. rewrite_type Aux.sub. Defined. + Definition mul : mode -> t -> t -> t. Proof. rewrite_type Aux.mul. Defined. + Definition div : mode -> t -> t -> t. Proof. rewrite_type Aux.div. Defined. + Definition sqrt : mode -> t -> t. Proof. rewrite_type Aux.sqrt. Defined. + Definition abs : t -> t. Proof. rewrite_type Aux.abs. Defined. + Definition of_bits : Z -> t. Proof. rewrite_type Aux.of_bits. Defined. + Definition to_bits : t -> Z. Proof. rewrite_type Aux.to_bits. Defined. + + Definition of_z : mode -> Z -> t. Proof. rewrite_type Aux.of_z. Defined. + Definition of_q : mode -> Qz -> t. Proof. rewrite_type Aux.of_q. Defined. + Definition to_q : t -> Qz. Proof. rewrite_type Aux.to_q. Defined. + + Definition compare : t -> t -> int31. Proof. rewrite_type Aux.compare. Defined. + Definition equal : t -> t -> bool. Proof. rewrite_type Aux.equal. Defined. + Definition hash : t -> nativeint. Proof. rewrite_type Aux.hash. Defined. + + Definition lt : t -> t -> bool. Proof. rewrite_type Aux.lt. Defined. + Definition le : t -> t -> bool. Proof. rewrite_type Aux.ge. Defined. + Definition gt : t -> t -> bool. Proof. rewrite_type Aux.gt. Defined. + Definition ge : t -> t -> bool. Proof. rewrite_type Aux.ge. Defined. + Definition eq : t -> t -> bool. Proof. rewrite_type Aux.eq. Defined. + Definition neq : t -> t -> bool. Proof. rewrite_type Aux.neq. Defined. + + Definition fcompare : t -> t -> option int31. Proof. rewrite_type Aux.fcompare. Defined. + + Definition infinity : bool -> t. Proof. rewrite_type Aux.infinity. Defined. + Definition zero : bool -> t. Proof. rewrite_type Aux.zero. Defined. + Definition nan : bool -> Z -> t. Proof. rewrite_type Aux.nan. Defined. + Definition infp : t. Proof. rewrite_type Aux.infp. Defined. + Definition infm : t. Proof. rewrite_type Aux.infm. Defined. + Definition zerop : t. Proof. rewrite_type Aux.zerop. Defined. + Definition default_nan : t. Proof. rewrite_type Aux.default_nan. Defined. + Definition finite : mode -> Z.t -> Z.t -> t. Proof. rewrite_type Aux.finite. Defined. + Definition classify : t -> Fappli_IEEE.full_float. Proof. rewrite_type Aux.classify. Defined. + + Definition cast_to_t (t:Type) (x:fconf t) : t -> binary_float (cprec (mw t x)) (cemax (ew t x)) := + match Ht t x in Logic.eq _ x return t -> x with + | refl_equal => (fun x => x) + end. + + + Definition conv (t1:Type) (conf1: fconf t1) (t2:Type) (conf2:fconf t2) (mode:mode) : t1 -> t2. + Proof. + rewrite (Ht t2 conf2). + rewrite (Ht t1 conf1). + exact (fun f => + match f with + | B754_zero _ _ b => B754_zero _ _ b + | B754_nan _ _ b _ => B754_nan _ _ b (snd (Aux.default_nan_pl _ conf2)) + | B754_infinity _ _ b => B754_infinity _ _ b + | B754_finite _ _ sx mx ex _ => FF2B _ _ _ (proj1 (binary_round_correct (cprec (mw _ conf2)) (cemax (ew _ conf2)) (Hprec _ conf2) (Hemax _ conf2) mode sx mx ex)) + end). + Defined. + +End Direct. + + Definition roundq mw ew mode (x:Qz) := + let conf := assert (check_param mw ew) _ (mk_conf mw ew) in + to_q _ conf (of_q _ conf mode x). + +End D. + +Module Type S. + Parameter t: Type. + Parameter conf: fconf t. + + Parameter opp: t -> t. + Parameter add: mode -> t -> t -> t. + Parameter sub: mode -> t -> t -> t. + Parameter mul: mode -> t -> t -> t. + Parameter div: mode -> t -> t -> t. + Parameter sqrt: mode -> t -> t. + Parameter abs: t -> t. + + Parameter of_bits: Z -> t. + Parameter to_bits: t -> Z. + + Parameter of_z: mode -> Z -> t. + + Parameter of_q: mode -> Qz -> t. + Parameter to_q: t -> Qz. + + Parameter compare: t -> t -> int31. + Parameter equal : t -> t -> bool. + Parameter hash : t -> nativeint. + + Parameter lt : t -> t -> bool. + Parameter le : t -> t -> bool. + Parameter gt : t -> t -> bool. + Parameter ge : t -> t -> bool. + Parameter eq : t -> t -> bool. + Parameter neq : t -> t -> bool. + + Parameter fcompare : t -> t -> option int31. + Parameter conv : forall (t':Type), fconf t' -> mode -> t -> t'. + + Parameter infinity : bool -> t. + Parameter zero : bool -> t. + Parameter nan : bool -> Z -> t. + Parameter infp : t. + Parameter infm : t. + Parameter zerop : t. + Parameter default_nan : t. + Parameter finite : mode -> Z.t -> Z.t -> t. + Parameter classify : t -> Fappli_IEEE.full_float. +End S. + +Module Type P. + Parameter mw: Z. + Parameter ew : Z. + Hypothesis valid_param : check_param mw ew = true. +End P. + +Module Make(Import P: P) : S + with Definition t := binary_float (cprec P.mw) (cemax P.ew). + + Definition t := binary_float (cprec P.mw) (cemax P.ew). + + (** The boolean is used for forbidding the extraction to remove the call to assert *) + Definition valid_param := assert (check_param mw ew) _ (fun H => (H,true)). + + Definition conf : fconf t := mk_conf mw ew (fst valid_param). + + Definition opp := Aux.opp t conf. + Definition add := Aux.add t conf. + Definition sub := Aux.sub t conf. + Definition mul := Aux.mul t conf. + Definition div := Aux.div t conf. + Definition sqrt := Aux.sqrt t conf. + Definition abs := Aux.abs t conf. + + Definition of_bits := Aux.of_bits t conf. + Definition to_bits := Aux.to_bits t conf. + + Definition of_z := Aux.of_z t conf. + + Definition of_q := Aux.of_q t conf. + Definition to_q := Aux.to_q t conf. + + Definition compare := Aux.compare t conf. + Definition equal := Aux.equal t conf. + Definition hash := Aux.hash t conf. + + Definition lt := Aux.lt t conf. + Definition le := Aux.le t conf. + Definition gt := Aux.gt t conf. + Definition ge := Aux.ge t conf. + Definition eq := Aux.eq t conf. + Definition neq := Aux.neq t conf. + + Definition fcompare := Aux.fcompare t conf. + + Definition conv := D.conv _ conf. + + Definition infinity := Aux.infinity t conf. + Definition zero := Aux.zero t conf. + Definition nan := Aux.nan t conf. + Definition infp := Aux.infp t conf. + Definition infm := Aux.infm t conf. + Definition zerop := Aux.zerop t conf. + Definition default_nan := Aux.default_nan t conf. + Definition finite := Aux.finite t conf. + Definition classify := Aux.classify t conf. + +End Make. + + +Module P_B32. + Definition mw := 23%Z. + Definition ew := 8%Z. + Lemma valid_param : check_param mw ew = true. + Proof. + reflexivity. + Qed. +End P_B32. + +Module P_B64. + Definition mw := 52%Z. + Definition ew := 11%Z. + Lemma valid_param : check_param mw ew = true. + Proof. + reflexivity. + Qed. +End P_B64. + +Module B32 := Make(P_B32). +Module B64 := Make(P_B64). diff --git a/farith/LGPLv2.1 b/farith/LGPLv2.1 new file mode 100644 index 0000000000000000000000000000000000000000..4362b49151d7b34ef83b3067a8f9c9f877d72a0e --- /dev/null +++ b/farith/LGPLv2.1 @@ -0,0 +1,502 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 2.1, February 1999 + + Copyright (C) 1991, 1999 Free Software Foundation, Inc. + 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + +[This is the first released version of the Lesser GPL. It also counts + as the successor of the GNU Library Public License, version 2, hence + the version number 2.1.] + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +Licenses are intended to guarantee your freedom to share and change +free software--to make sure the software is free for all its users. + + This license, the Lesser General Public License, applies to some +specially designated software packages--typically libraries--of the +Free Software Foundation and other authors who decide to use it. You +can use it too, but we suggest you first think carefully about whether +this license or the ordinary General Public License is the better +strategy to use in any particular case, based on the explanations below. + + When we speak of free software, we are referring to freedom of use, +not price. Our General Public Licenses are designed to make sure that +you have the freedom to distribute copies of free software (and charge +for this service if you wish); that you receive source code or can get +it if you want it; that you can change the software and use pieces of +it in new free programs; and that you are informed that you can do +these things. + + To protect your rights, we need to make restrictions that forbid +distributors to deny you these rights or to ask you to surrender these +rights. These restrictions translate to certain responsibilities for +you if you distribute copies of the library or if you modify it. + + For example, if you distribute copies of the library, whether gratis +or for a fee, you must give the recipients all the rights that we gave +you. You must make sure that they, too, receive or can get the source +code. If you link other code with the library, you must provide +complete object files to the recipients, so that they can relink them +with the library after making changes to the library and recompiling +it. And you must show them these terms so they know their rights. + + We protect your rights with a two-step method: (1) we copyright the +library, and (2) we offer you this license, which gives you legal +permission to copy, distribute and/or modify the library. + + To protect each distributor, we want to make it very clear that +there is no warranty for the free library. Also, if the library is +modified by someone else and passed on, the recipients should know +that what they have is not the original version, so that the original +author's reputation will not be affected by problems that might be +introduced by others. + + Finally, software patents pose a constant threat to the existence of +any free program. We wish to make sure that a company cannot +effectively restrict the users of a free program by obtaining a +restrictive license from a patent holder. Therefore, we insist that +any patent license obtained for a version of the library must be +consistent with the full freedom of use specified in this license. + + Most GNU software, including some libraries, is covered by the +ordinary GNU General Public License. This license, the GNU Lesser +General Public License, applies to certain designated libraries, and +is quite different from the ordinary General Public License. We use +this license for certain libraries in order to permit linking those +libraries into non-free programs. + + When a program is linked with a library, whether statically or using +a shared library, the combination of the two is legally speaking a +combined work, a derivative of the original library. The ordinary +General Public License therefore permits such linking only if the +entire combination fits its criteria of freedom. The Lesser General +Public License permits more lax criteria for linking other code with +the library. + + We call this license the "Lesser" General Public License because it +does Less to protect the user's freedom than the ordinary General +Public License. It also provides other free software developers Less +of an advantage over competing non-free programs. These disadvantages +are the reason we use the ordinary General Public License for many +libraries. However, the Lesser license provides advantages in certain +special circumstances. + + For example, on rare occasions, there may be a special need to +encourage the widest possible use of a certain library, so that it becomes +a de-facto standard. To achieve this, non-free programs must be +allowed to use the library. A more frequent case is that a free +library does the same job as widely used non-free libraries. In this +case, there is little to gain by limiting the free library to free +software only, so we use the Lesser General Public License. + + In other cases, permission to use a particular library in non-free +programs enables a greater number of people to use a large body of +free software. For example, permission to use the GNU C Library in +non-free programs enables many more people to use the whole GNU +operating system, as well as its variant, the GNU/Linux operating +system. + + Although the Lesser General Public License is Less protective of the +users' freedom, it does ensure that the user of a program that is +linked with the Library has the freedom and the wherewithal to run +that program using a modified version of the Library. + + The precise terms and conditions for copying, distribution and +modification follow. Pay close attention to the difference between a +"work based on the library" and a "work that uses the library". The +former contains code derived from the library, whereas the latter must +be combined with the library in order to run. + + GNU LESSER GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License Agreement applies to any software library or other +program which contains a notice placed by the copyright holder or +other authorized party saying it may be distributed under the terms of +this Lesser General Public License (also called "this License"). +Each licensee is addressed as "you". + + A "library" means a collection of software functions and/or data +prepared so as to be conveniently linked with application programs +(which use some of those functions and data) to form executables. + + The "Library", below, refers to any such software library or work +which has been distributed under these terms. A "work based on the +Library" means either the Library or any derivative work under +copyright law: that is to say, a work containing the Library or a +portion of it, either verbatim or with modifications and/or translated +straightforwardly into another language. (Hereinafter, translation is +included without limitation in the term "modification".) + + "Source code" for a work means the preferred form of the work for +making modifications to it. For a library, complete source code means +all the source code for all modules it contains, plus any associated +interface definition files, plus the scripts used to control compilation +and installation of the library. + + Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running a program using the Library is not restricted, and output from +such a program is covered only if its contents constitute a work based +on the Library (independent of the use of the Library in a tool for +writing it). Whether that is true depends on what the Library does +and what the program that uses the Library does. + + 1. You may copy and distribute verbatim copies of the Library's +complete source code as you receive it, in any medium, provided that +you conspicuously and appropriately publish on each copy an +appropriate copyright notice and disclaimer of warranty; keep intact +all the notices that refer to this License and to the absence of any +warranty; and distribute a copy of this License along with the +Library. + + You may charge a fee for the physical act of transferring a copy, +and you may at your option offer warranty protection in exchange for a +fee. + + 2. You may modify your copy or copies of the Library or any portion +of it, thus forming a work based on the Library, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) The modified work must itself be a software library. + + b) You must cause the files modified to carry prominent notices + stating that you changed the files and the date of any change. + + c) You must cause the whole of the work to be licensed at no + charge to all third parties under the terms of this License. + + d) If a facility in the modified Library refers to a function or a + table of data to be supplied by an application program that uses + the facility, other than as an argument passed when the facility + is invoked, then you must make a good faith effort to ensure that, + in the event an application does not supply such function or + table, the facility still operates, and performs whatever part of + its purpose remains meaningful. + + (For example, a function in a library to compute square roots has + a purpose that is entirely well-defined independent of the + application. Therefore, Subsection 2d requires that any + application-supplied function or table used by this function must + be optional: if the application does not supply it, the square + root function must still compute square roots.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Library, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Library, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote +it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Library. + +In addition, mere aggregation of another work not based on the Library +with the Library (or with a work based on the Library) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may opt to apply the terms of the ordinary GNU General Public +License instead of this License to a given copy of the Library. To do +this, you must alter all the notices that refer to this License, so +that they refer to the ordinary GNU General Public License, version 2, +instead of to this License. (If a newer version than version 2 of the +ordinary GNU General Public License has appeared, then you can specify +that version instead if you wish.) Do not make any other change in +these notices. + + Once this change is made in a given copy, it is irreversible for +that copy, so the ordinary GNU General Public License applies to all +subsequent copies and derivative works made from that copy. + + This option is useful when you wish to copy part of the code of +the Library into a program that is not a library. + + 4. You may copy and distribute the Library (or a portion or +derivative of it, under Section 2) in object code or executable form +under the terms of Sections 1 and 2 above provided that you accompany +it with the complete corresponding machine-readable source code, which +must be distributed under the terms of Sections 1 and 2 above on a +medium customarily used for software interchange. + + If distribution of object code is made by offering access to copy +from a designated place, then offering equivalent access to copy the +source code from the same place satisfies the requirement to +distribute the source code, even though third parties are not +compelled to copy the source along with the object code. + + 5. A program that contains no derivative of any portion of the +Library, but is designed to work with the Library by being compiled or +linked with it, is called a "work that uses the Library". Such a +work, in isolation, is not a derivative work of the Library, and +therefore falls outside the scope of this License. + + However, linking a "work that uses the Library" with the Library +creates an executable that is a derivative of the Library (because it +contains portions of the Library), rather than a "work that uses the +library". The executable is therefore covered by this License. +Section 6 states terms for distribution of such executables. + + When a "work that uses the Library" uses material from a header file +that is part of the Library, the object code for the work may be a +derivative work of the Library even though the source code is not. +Whether this is true is especially significant if the work can be +linked without the Library, or if the work is itself a library. The +threshold for this to be true is not precisely defined by law. + + If such an object file uses only numerical parameters, data +structure layouts and accessors, and small macros and small inline +functions (ten lines or less in length), then the use of the object +file is unrestricted, regardless of whether it is legally a derivative +work. (Executables containing this object code plus portions of the +Library will still fall under Section 6.) + + Otherwise, if the work is a derivative of the Library, you may +distribute the object code for the work under the terms of Section 6. +Any executables containing that work also fall under Section 6, +whether or not they are linked directly with the Library itself. + + 6. As an exception to the Sections above, you may also combine or +link a "work that uses the Library" with the Library to produce a +work containing portions of the Library, and distribute that work +under terms of your choice, provided that the terms permit +modification of the work for the customer's own use and reverse +engineering for debugging such modifications. + + You must give prominent notice with each copy of the work that the +Library is used in it and that the Library and its use are covered by +this License. You must supply a copy of this License. If the work +during execution displays copyright notices, you must include the +copyright notice for the Library among them, as well as a reference +directing the user to the copy of this License. Also, you must do one +of these things: + + a) Accompany the work with the complete corresponding + machine-readable source code for the Library including whatever + changes were used in the work (which must be distributed under + Sections 1 and 2 above); and, if the work is an executable linked + with the Library, with the complete machine-readable "work that + uses the Library", as object code and/or source code, so that the + user can modify the Library and then relink to produce a modified + executable containing the modified Library. (It is understood + that the user who changes the contents of definitions files in the + Library will not necessarily be able to recompile the application + to use the modified definitions.) + + b) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (1) uses at run time a + copy of the library already present on the user's computer system, + rather than copying library functions into the executable, and (2) + will operate properly with a modified version of the library, if + the user installs one, as long as the modified version is + interface-compatible with the version that the work was made with. + + c) Accompany the work with a written offer, valid for at + least three years, to give the same user the materials + specified in Subsection 6a, above, for a charge no more + than the cost of performing this distribution. + + d) If distribution of the work is made by offering access to copy + from a designated place, offer equivalent access to copy the above + specified materials from the same place. + + e) Verify that the user has already received a copy of these + materials or that you have already sent this user a copy. + + For an executable, the required form of the "work that uses the +Library" must include any data and utility programs needed for +reproducing the executable from it. However, as a special exception, +the materials to be distributed need not include anything that is +normally distributed (in either source or binary form) with the major +components (compiler, kernel, and so on) of the operating system on +which the executable runs, unless that component itself accompanies +the executable. + + It may happen that this requirement contradicts the license +restrictions of other proprietary libraries that do not normally +accompany the operating system. Such a contradiction means you cannot +use both them and the Library together in an executable that you +distribute. + + 7. You may place library facilities that are a work based on the +Library side-by-side in a single library together with other library +facilities not covered by this License, and distribute such a combined +library, provided that the separate distribution of the work based on +the Library and of the other library facilities is otherwise +permitted, and provided that you do these two things: + + a) Accompany the combined library with a copy of the same work + based on the Library, uncombined with any other library + facilities. This must be distributed under the terms of the + Sections above. + + b) Give prominent notice with the combined library of the fact + that part of it is a work based on the Library, and explaining + where to find the accompanying uncombined form of the same work. + + 8. You may not copy, modify, sublicense, link with, or distribute +the Library except as expressly provided under this License. Any +attempt otherwise to copy, modify, sublicense, link with, or +distribute the Library is void, and will automatically terminate your +rights under this License. However, parties who have received copies, +or rights, from you under this License will not have their licenses +terminated so long as such parties remain in full compliance. + + 9. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Library or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Library (or any work based on the +Library), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Library or works based on it. + + 10. Each time you redistribute the Library (or any work based on the +Library), the recipient automatically receives a license from the +original licensor to copy, distribute, link with or modify the Library +subject to these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties with +this License. + + 11. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Library at all. For example, if a patent +license would not permit royalty-free redistribution of the Library by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Library. + +If any portion of this section is held invalid or unenforceable under any +particular circumstance, the balance of the section is intended to apply, +and the section as a whole is intended to apply in other circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 12. If the distribution and/or use of the Library is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Library under this License may add +an explicit geographical distribution limitation excluding those countries, +so that distribution is permitted only in or among countries not thus +excluded. In such case, this License incorporates the limitation as if +written in the body of this License. + + 13. The Free Software Foundation may publish revised and/or new +versions of the Lesser General Public License from time to time. +Such new versions will be similar in spirit to the present version, +but may differ in detail to address new problems or concerns. + +Each version is given a distinguishing version number. If the Library +specifies a version number of this License which applies to it and +"any later version", you have the option of following the terms and +conditions either of that version or of any later version published by +the Free Software Foundation. If the Library does not specify a +license version number, you may choose any version ever published by +the Free Software Foundation. + + 14. If you wish to incorporate parts of the Library into other free +programs whose distribution conditions are incompatible with these, +write to the author to ask for permission. For software which is +copyrighted by the Free Software Foundation, write to the Free +Software Foundation; we sometimes make exceptions for this. Our +decision will be guided by the two goals of preserving the free status +of all derivatives of our free software and of promoting the sharing +and reuse of software generally. + + NO WARRANTY + + 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO +WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW. +EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR +OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY +KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE +LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME +THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN +WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY +AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU +FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR +CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE +LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING +RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A +FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF +SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH +DAMAGES. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Libraries + + If you develop a new library, and you want it to be of the greatest +possible use to the public, we recommend making it free software that +everyone can redistribute and change. You can do so by permitting +redistribution under these terms (or, alternatively, under the terms of the +ordinary General Public License). + + To apply these terms, attach the following notices to the library. It is +safest to attach them to the start of each source file to most effectively +convey the exclusion of warranty; and each file should have at least the +"copyright" line and a pointer to where the full notice is found. + + <one line to give the library's name and a brief idea of what it does.> + Copyright (C) <year> <name of author> + + This library is free software; 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; either + version 2.1 of the License, or (at your option) any later version. + + This library 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. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, write to the Free Software + Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + +Also add information on how to contact you by electronic and paper mail. + +You should also get your employer (if you work as a programmer) or your +school, if any, to sign a "copyright disclaimer" for the library, if +necessary. Here is a sample; alter the names: + + Yoyodyne, Inc., hereby disclaims all copyright interest in the + library `Frob' (a library for tweaking knobs) written by James Random Hacker. + + <signature of Ty Coon>, 1 April 1990 + Ty Coon, President of Vice + +That's all there is to it! diff --git a/farith/LGPLv3 b/farith/LGPLv3 new file mode 100644 index 0000000000000000000000000000000000000000..65c5ca88a67c30becee01c5a8816d964b03862f9 --- /dev/null +++ b/farith/LGPLv3 @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/> + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + + This version of the GNU Lesser General Public License incorporates +the terms and conditions of version 3 of the GNU General Public +License, supplemented by the additional permissions listed below. + + 0. Additional Definitions. + + As used herein, "this License" refers to version 3 of the GNU Lesser +General Public License, and the "GNU GPL" refers to version 3 of the GNU +General Public License. + + "The Library" refers to a covered work governed by this License, +other than an Application or a Combined Work as defined below. + + An "Application" is any work that makes use of an interface provided +by the Library, but which is not otherwise based on the Library. +Defining a subclass of a class defined by the Library is deemed a mode +of using an interface provided by the Library. + + A "Combined Work" is a work produced by combining or linking an +Application with the Library. The particular version of the Library +with which the Combined Work was made is also called the "Linked +Version". + + The "Minimal Corresponding Source" for a Combined Work means the +Corresponding Source for the Combined Work, excluding any source code +for portions of the Combined Work that, considered in isolation, are +based on the Application, and not on the Linked Version. + + The "Corresponding Application Code" for a Combined Work means the +object code and/or source code for the Application, including any data +and utility programs needed for reproducing the Combined Work from the +Application, but excluding the System Libraries of the Combined Work. + + 1. Exception to Section 3 of the GNU GPL. + + You may convey a covered work under sections 3 and 4 of this License +without being bound by section 3 of the GNU GPL. + + 2. Conveying Modified Versions. + + If you modify a copy of the Library, and, in your modifications, a +facility refers to a function or data to be supplied by an Application +that uses the facility (other than as an argument passed when the +facility is invoked), then you may convey a copy of the modified +version: + + a) under this License, provided that you make a good faith effort to + ensure that, in the event an Application does not supply the + function or data, the facility still operates, and performs + whatever part of its purpose remains meaningful, or + + b) under the GNU GPL, with none of the additional permissions of + this License applicable to that copy. + + 3. Object Code Incorporating Material from Library Header Files. + + The object code form of an Application may incorporate material from +a header file that is part of the Library. You may convey such object +code under terms of your choice, provided that, if the incorporated +material is not limited to numerical parameters, data structure +layouts and accessors, or small macros, inline functions and templates +(ten or fewer lines in length), you do both of the following: + + a) Give prominent notice with each copy of the object code that the + Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the object code with a copy of the GNU GPL and this license + document. + + 4. Combined Works. + + You may convey a Combined Work under terms of your choice that, +taken together, effectively do not restrict modification of the +portions of the Library contained in the Combined Work and reverse +engineering for debugging such modifications, if you also do each of +the following: + + a) Give prominent notice with each copy of the Combined Work that + the Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the Combined Work with a copy of the GNU GPL and this license + document. + + c) For a Combined Work that displays copyright notices during + execution, include the copyright notice for the Library among + these notices, as well as a reference directing the user to the + copies of the GNU GPL and this license document. + + d) Do one of the following: + + 0) Convey the Minimal Corresponding Source under the terms of this + License, and the Corresponding Application Code in a form + suitable for, and under terms that permit, the user to + recombine or relink the Application with a modified version of + the Linked Version to produce a modified Combined Work, in the + manner specified by section 6 of the GNU GPL for conveying + Corresponding Source. + + 1) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (a) uses at run time + a copy of the Library already present on the user's computer + system, and (b) will operate properly with a modified version + of the Library that is interface-compatible with the Linked + Version. + + e) Provide Installation Information, but only if you would otherwise + be required to provide such information under section 6 of the + GNU GPL, and only to the extent that such information is + necessary to install and execute a modified version of the + Combined Work produced by recombining or relinking the + Application with a modified version of the Linked Version. (If + you use option 4d0, the Installation Information must accompany + the Minimal Corresponding Source and Corresponding Application + Code. If you use option 4d1, you must provide the Installation + Information in the manner specified by section 6 of the GNU GPL + for conveying Corresponding Source.) + + 5. Combined Libraries. + + You may place library facilities that are a work based on the +Library side by side in a single library together with other library +facilities that are not Applications and are not covered by this +License, and convey such a combined library under terms of your +choice, if you do both of the following: + + a) Accompany the combined library with a copy of the same work based + on the Library, uncombined with any other library facilities, + conveyed under the terms of this License. + + b) Give prominent notice with the combined library that part of it + is a work based on the Library, and explaining where to find the + accompanying uncombined form of the same work. + + 6. Revised Versions of the GNU Lesser General Public License. + + The Free Software Foundation may publish revised and/or new versions +of the GNU Lesser General Public License from time to time. Such new +versions will be similar in spirit to the present version, but may +differ in detail to address new problems or concerns. + + Each version is given a distinguishing version number. If the +Library as you received it specifies that a certain numbered version +of the GNU Lesser General Public License "or any later version" +applies to it, you have the option of following the terms and +conditions either of that published version or of any later version +published by the Free Software Foundation. If the Library as you +received it does not specify a version number of the GNU Lesser +General Public License, you may choose any version of the GNU Lesser +General Public License ever published by the Free Software Foundation. + + If the Library as you received it specifies that a proxy can decide +whether future versions of the GNU Lesser General Public License shall +apply, that proxy's public statement of acceptance of any version is +permanent authorization for you to choose that version for the +Library. diff --git a/farith/META b/farith/META new file mode 100644 index 0000000000000000000000000000000000000000..f3930e802daa09248e370fab7dd1ac5b62176fb9 --- /dev/null +++ b/farith/META @@ -0,0 +1,9 @@ +description = "Float Arithmetic" +version = "0.1" +requires = "zarith" + +archive(byte) = "farith.cma F.cma" +archive(native) = "farith.cmxa F.cmxa" +archive(plugin) = "farith.cmxs F.cmxs" +plugin(byte) = "farith.cma F.cma" +plugin(native) = "farith.cmxs F.cmxs" diff --git a/farith/Makefile b/farith/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..ee311beef1a749a0101d871e83d08c6af332caa1 --- /dev/null +++ b/farith/Makefile @@ -0,0 +1,124 @@ +########################################################################## +# 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). # +# # +########################################################################## + +.PHONY: all doc clean depend install uninstall headers tests bench force top + +# -------------------------------------------------------------------------- +# --- Compilation +# -------------------------------------------------------------------------- + +OCAMLSUFFIX= .cma .cmxa .cmxs .cmi .a .mli +TOINSTALL=$(addprefix farith,$(OCAMLSUFFIX)) $(addprefix F,$(OCAMLSUFFIX)) + +FLAGS= -cflags -w,PSUZL+7+33-27,-warn-error,PSUZL+7-27 -use-ocamlfind -I extracted -tag debug + +all: + ocamlbuild ${FLAGS} $(TOINSTALL) + +%.native: force + ocamlbuild ${FLAGS} $@ + +# -------------------------------------------------------------------------- +# --- Local Install for Tests +# -------------------------------------------------------------------------- + +LOCALINSTALL=$(shell pwd)/tests/_local + +localinstall: all .local + +.local: META $(addprefix _build/,$(TOINSTALL)) + @echo "Local Installation" + @make -C tests clean + @rm -fr $(LOCALINSTALL) + @mkdir -p $(LOCALINSTALL) + @ocamlfind install -destdir $(LOCALINSTALL) \ + farith META $(addprefix _build/,$(TOINSTALL)) + @touch .local + +# -------------------------------------------------------------------------- +# --- Tests +# -------------------------------------------------------------------------- + +%.meld: + make -C tests $@ + +tests: localinstall + @echo "Running Tests" + @make -C tests all + +bench: + @echo Compile micro.native + @ocamlbuild ${FLAGS} -package zarith bench/micro.native + @echo Run micro.native + @./micro.native -q 1 + +# -------------------------------------------------------------------------- +# --- Toplevel (requires utop) +# -------------------------------------------------------------------------- + +top: + ocamlbuild ${FLAGS} farith.top + +# -------------------------------------------------------------------------- +# --- Documentation +# -------------------------------------------------------------------------- + +doc: + @echo "Generate documentation" + @mkdir -p html + @rm -fr html/* + @ocamlfind ocamldoc -package zarith -I _build -short-functors \ + -t "Float Arithmetics" -d html -html F.mli farith.mli + @cp -f ceatech.css html/style.css + +# -------------------------------------------------------------------------- +# --- Release +# -------------------------------------------------------------------------- + +CEA_LGPL=farith.ml farith.mli F_aux.v extract.v Makefile + +headers: + headache -c headers/header.config -h headers/CEA_LGPL $(CEA_LGPL) + ocp-indent -i *.ml *.mli + +# -------------------------------------------------------------------------- +# --- Installation +# -------------------------------------------------------------------------- + +install: + @if [ -e $(shell ocamlfind printconf destdir)/farith ] ; then ocamlfind remove farith ; fi + @ocamlfind install farith META $(addprefix _build/,$(TOINSTALL)) + +uninstall: + @ocamlfind remove farith + +# -------------------------------------------------------------------------- +# --- Cleaning +# -------------------------------------------------------------------------- + +depend: + @echo "Ocambuild dependencies (nothing to do)" + +clean: + @echo "Cleaning" + @make -C tests clean + @rm -fr html .local + @ocamlbuild -clean diff --git a/farith/README.md b/farith/README.md new file mode 100644 index 0000000000000000000000000000000000000000..b0a46e6e832f2fbc976bd9717ab0aaeb98f13a3f --- /dev/null +++ b/farith/README.md @@ -0,0 +1,30 @@ +## Farith Library + +`Farith` is a formally proved OCaml library to manipulate IEEE floating point numbers. +The library is extracted from the `Flocq` library developped at INRIA by Guillaume Melquiond +and Sylvie Boldo with the Coq proof assistant. However, for better performances, computations +over `Z` integers are implemented with the `Zarith` OCaml library +developped by Antoine Miné and Xavier Leroy and based on either `MPIR` or `GMP` libraries. + +## Installation + +Compilation and installation is standard: simply type `make all` and `make install`. +No configuration is required. Compilation is performed by `ocamlbuild` and installation with `ocamlfind` +under package name `farith`. + +There is no need to have `Flocq` and `Coq` installed to compile `Farith`, since the archive +contains the extracted OCaml files. Extraction can be replayed by running the `extract.sh` script. + +## Documentation + +The HTML documentation is generated with `make doc`, rooted at `html/index.html`. +See also `tests` directory for examples of usage. + +## License + +The `Farith` OCaml API is authored by CEA and distributed under the LGPL v1.2 licence. +The `Flocq` extracted files are authored by INRIA and distributed under the LGPL v3 licence. + +Copyright (c) 2015 CEA-LIST -- All right reserved +Copyright (C) 2010-2013 Sylvie Boldo +Copyright (C) 2010-2013 Guillaume Melquiond diff --git a/farith/_tags b/farith/_tags new file mode 100644 index 0000000000000000000000000000000000000000..57c38c965efd9c1976754f06569d9d7e4b0ea50e --- /dev/null +++ b/farith/_tags @@ -0,0 +1,5 @@ +true:package(zarith) +<bench/*> : thread, package(core_bench) +<tests>: -traverse +<tests>: not_hygienic +<farith_top.*> or <farith.top>: package(threads), package(utop), package(compiler-libs), thread \ No newline at end of file diff --git a/farith/bench/micro.ml b/farith/bench/micro.ml new file mode 100644 index 0000000000000000000000000000000000000000..9306a38cc95135f4b0d839fc2ccacb118cc0a7de --- /dev/null +++ b/farith/bench/micro.ml @@ -0,0 +1,49 @@ +open Core.Std +open Core_bench.Std + +module B64 = Farith.B64 + +let bench_add x y = + let qx = Q.of_float x in + let qy = Q.of_float y in + let fx = B64.of_float x in + let fy = B64.of_float y in + let qfx = F.of_float x in + let qfy = F.of_float y in + let add = F.add qfx qfy in + (** use x' and y' otherwise ocaml do constant propagation *) + let x' = B64.to_float fx in + let y' = B64.to_float fy in + let u = x' +. y' in + assert (x = x' && y = y'); + Bench.Test.create_group ~name:(Printf.sprintf "%.2e+.%.2e" x y) + [ + Bench.Test.create ~name:"Float add" (fun () -> + ignore (x' +. y')); + Bench.Test.create ~name:"Q.add+roundq" (fun () -> + ignore (Farith.D.roundq ~mw:52 ~ew:11 Farith.NE (Q.add qx qy))); + Bench.Test.create ~name:"Farith.B64.add" (fun () -> + ignore (B64.add Farith.NE fx fy)); + Bench.Test.create ~name:"Farith.B64.round" (fun () -> + ignore (B64.of_float u)); + Bench.Test.create ~name:"F.add+F.round" (fun () -> + ignore (F.round_f64 (F.add qfx qfy))); + Bench.Test.create ~name:"F.add" (fun () -> + ignore (F.add qfx qfy)); + Bench.Test.create ~name:"F.log2" (fun () -> + ignore (F.log2 add)); + Bench.Test.create ~name:"F.round" (fun () -> + ignore (F.round_f64 add)); + Bench.Test.create ~name:"F.of_float" (fun () -> + ignore (F.of_float u)); + Bench.Test.create ~name:"Q.of_float" (fun () -> + ignore (Q.of_float u)); + ] + +let main () = + Command.run (Bench.make_command [ + (*(bench_add 1.0 1.0);*) + (bench_add 1.0 0.00000001) + ]) + +let () = main () diff --git a/farith/bench/valgrind.ml b/farith/bench/valgrind.ml new file mode 100644 index 0000000000000000000000000000000000000000..1b190ab2d161002ff473745e524b5647199c737f --- /dev/null +++ b/farith/bench/valgrind.ml @@ -0,0 +1,16 @@ + + +module B64 = Farith.B64 + +let () = + let x = 1.0 in + let y = 0.1 in + let fx = B64.of_float x in + let fy = B64.of_float y in + (** use x' and y' otherwise ocaml do constant propagation *) + let x' = B64.to_float fx in + let y' = B64.to_float fy in + assert (x = x' && y = y'); + for i=0 to 100 do + ignore (B64.add Farith.NE fx fy) + done diff --git a/farith/ceatech.css b/farith/ceatech.css new file mode 100644 index 0000000000000000000000000000000000000000..8a9db5b061135d259267efcb7f8fc93acb6e02f7 --- /dev/null +++ b/farith/ceatech.css @@ -0,0 +1,122 @@ +* { margin: 0; padding: 0 } + +body { + font-family: "Verdana", sans ; + font-size: 10pt; + position: relative; + padding: 0.7cm; + margin: auto; + width: 20cm; + background-color: white +} + +h1 { + margin-top: 5mm; + margin-bottom: 3mm; + font-size: 16pt; + font-weight: bold +} + +h2 { + margin-top: 5mm; + margin-bottom: 1mm; + font-size: 12pt; + font-weight: bold +} + +h3 { + margin-top: 5mm; + margin-bottom: 1mm; + font-size: 10pt; + font-weight: bold +} + +h4,h5,h6, div.h7, div.h8, div.h9 { + margin-left: 4mm; + margin-top: 1mm; + margin-bottom: 1mm; + font-size: 10pt; + font-style: italic; + font-weight: bold; + color: darkgreen +} + +hr { border: thin solid firebrick ; margin: 2mm 0 2mm 0 } + +a img { vertical-align: middle; background-color: inherit } + +a:visited { color: maroon; text-decoration: none } +a:link { color: maroon; text-decoration: none } +a:hover { background-color: lightgray } +a:active { background-color: orange } +:target { background-color: orange } + +.navbar { + padding-bottom: 2mm ; + font-size: 8pt ; +} + +.navbar a { color: darkgreen } + +.keyword { font-weight : bold; color: darkgoldenrod } +.keywordsign { color : #C04600 } +.superscript { font-size: 7pt } +.subscript { font-size: 7pt } +.warning { color: firebrick ; font-style: italic; margin-right:1ex } + +td.typefieldcomment { padding: 0 0 0 1em; color: darkgreen } +td.module { padding: 0 1em 0 0 } +td div.info { + color: inherit; + display: inline; + margin: 0 ; + padding: 0; + border: none +} + +div.info { + color: #585858; + display: block; + padding: 1pt 0 1pt 0.4em; + margin-left: 1em; + border-left: thin solid darkgreen +} + +div.param_info { + color: #585858; + display: block; + text-indent: -1em; + padding: 1pt 0 1pt 2em; + margin-left: 1em; + border-left: thin solid darkgreen +} + +.typetable { border-style : hidden } +.indextable { + margin-top: 2mm ; + padding: 2mm 6mm 2mm 4mm ; + border-style : hidden ; + border-top: darkgreen thin solid ; + border-bottom: darkgreen thin solid +} +.paramstable { border-style : hidden ; padding: 5pt 5pt } +tr { font-size: 10pt } +pre { color : #263F71 ; font-size: 10pt; font-family: monospace; margin-top: 1mm } +pre.codepre, pre.verbatim { margin-left: 1em; padding:2pt; background-color: #f0f0f0 } +pre.codepre br { display:none } +.code { color : #465F91 ; font-size: 10pt; font-family: monospace } +.comment { color : darkgreen } +.constructor { color : darkblue } +.type { color: #5C6585 } +.string { color: navy } +div.sig_block {margin-left: 2em} +li { margin-left: 2em } +p { margin-top: 2mm ; margin-bottom: 2mm } +ul { margin-top: 2mm ; margin-bottom: 2mm } +body:after { + position: relative; + bottom: -2em ; + color: gray ; + font-size: small ; + content: "\00a9 CEA-LIST 2015 - All rights reserved" +} diff --git a/farith/dune b/farith/dune new file mode 100644 index 0000000000000000000000000000000000000000..8538a39b5236a14b7036911108824daf46722d75 --- /dev/null +++ b/farith/dune @@ -0,0 +1,15 @@ +(library + (name farith) + (public_name farith) + (modules farith) + (libraries zarith farith_extracted) + (wrapped false) +) + +(library + (name farith_big) + (public_name farith._big) + (modules farith_Big) + (libraries zarith) + (wrapped false) +) diff --git a/farith/dune-project b/farith/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..de4fc20920050d2aa187123f17080218ff2ac041 --- /dev/null +++ b/farith/dune-project @@ -0,0 +1 @@ +(lang dune 1.0) diff --git a/farith/extract.sh b/farith/extract.sh new file mode 100755 index 0000000000000000000000000000000000000000..202c6663ddeb25ca6f4cbc659239710f0375bf7a --- /dev/null +++ b/farith/extract.sh @@ -0,0 +1,29 @@ +#!/bin/sh -exu + +cd $(dirname $0) + +coqc F_aux.v + +rm -rf extracted +mkdir extracted + +cd extracted +cp ../F_aux.vo . +coqtop -batch -l ../extract.v + +rm -f Peano.ml* Zbool.ml* BinNums.ml* + +for file in *.ml*; do + case $file in + F_aux.ml*) + headache -c ../headers/header.config -h ../headers/CEA_LGPL $file + mv $file farith_$file + ;; + *) + headache -c ../headers/header.config -h ../headers/FLOCQ $file + mv $file farith_$file + esac + +done + +sed -i -e "s/^open /open Farith_/" * diff --git a/farith/extract.v b/farith/extract.v new file mode 100644 index 0000000000000000000000000000000000000000..a0138b9bf0735896c695bb375ab5d6274aedb336 --- /dev/null +++ b/farith/extract.v @@ -0,0 +1,293 @@ +(**************************************************************************) +(* 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). *) +(* *) +(**************************************************************************) + +Require Import Sumbool. + +Extract Inlined Constant bool_of_sumbool => "Farith_Big.identity". +Extract Inlined Constant sumbool_of_bool => "Farith_Big.identity". + + +(** From ExtrOcamlNatBigInt of coq archive *) + +Require Import Arith Even Div2 EqNat Euclid. +Require Import ExtrOcamlBasic. + +Extract Inlined Constant Datatypes.negb => "Pervasives.not". +Extract Inlined Constant Datatypes.fst => "Pervasives.fst". +Extract Inlined Constant Datatypes.snd => "Pervasives.snd". + + +(** NB: The extracted code should be linked with [nums.cm(x)a] + from ocaml's stdlib and with the wrapper [big.ml] that + simplifies the use of [Big_int] (it can be found in the sources + of Coq). *) + +(** Disclaimer: trying to obtain efficient certified programs + by extracting [nat] into [big_int] isn't necessarily a good idea. + See comments in [ExtrOcamlNatInt.v]. +*) + + +(** Mapping of [nat] into [big_int]. The last string corresponds to + a [nat_case], see documentation of [Extract Inductive]. *) + +Extract Inductive nat => "Farith_Big.big_int" [ "Farith_Big.zero" "Farith_Big.succ" ] + "Farith_Big.nat_case". + +(** Efficient (but uncertified) versions for usual [nat] functions *) + +Extract Inlined Constant plus => "Farith_Big.add". +Extract Inlined Constant mult => "Farith_Big.mult". +Extract Constant pred => "fun n -> Farith_Big.max Farith_Big.zero (Farith_Big.pred n)". +Extract Constant minus => "fun n m -> Farith_Big.max Farith_Big.zero (Farith_Big.sub n m)". +Extract Inlined Constant max => "Farith_Big.max". +Extract Inlined Constant min => "Farith_Big.min". +(*Extract Constant nat_beq => "Farith_Big.eq".*) +Extract Constant EqNat.beq_nat => "Farith_Big.eq". +Extract Constant EqNat.eq_nat_decide => "Farith_Big.eq". + +Extract Constant Peano_dec.eq_nat_dec => "Farith_Big.eq". + +Extract Constant Compare_dec.nat_compare => + "Farith_Big.compare_case Eq Lt Gt". + +Extract Constant Compare_dec.leb => "Farith_Big.le". +Extract Constant Compare_dec.le_lt_dec => "Farith_Big.le". +Extract Constant Compare_dec.lt_eq_lt_dec => + "Farith_Big.compare_case (Some false) (Some true) None". + +Extract Constant Even.even_odd_dec => + "fun n -> Farith_Big.sign (Farith_Big.mod n Farith_Big.two) = 0". +Extract Constant Div2.div2 => "fun n -> Farith_Big.div n Farith_Big.two". + +Extract Inductive Euclid.diveucl => "(Farith_Big.big_int * Farith_Big.big_int)" [""]. +Extract Constant Euclid.eucl_dev => "fun n m -> Farith_Big.quomod m n". +Extract Constant Euclid.quotient => "fun n m -> Farith_Big.div m n". +Extract Constant Euclid.modulo => "fun n m -> Farith_Big.modulo m n". + + +(** From ExtrOcamlZBigInt of coq archive *) + +Require Import ZArith NArith. +Require Import ExtrOcamlBasic. + +(** NB: The extracted code should be linked with [nums.cm(x)a] + from ocaml's stdlib and with the wrapper [big.ml] that + simplifies the use of [Big_int] (it can be found in the sources + of Coq). *) + +(** Disclaimer: trying to obtain efficient certified programs + by extracting [Z] into [big_int] isn't necessarily a good idea. + See the Disclaimer in [ExtrOcamlNatInt]. *) + +(** Mapping of [positive], [Z], [N] into [big_int]. The last strings + emulate the matching, see documentation of [Extract Inductive]. *) + +Extract Inductive positive => "Farith_Big.big_int" + [ "Farith_Big.succ_double" "Farith_Big.double" "Farith_Big.one" ] "Farith_Big.positive_case". + +Extract Inductive Z => "Farith_Big.big_int" + [ "Farith_Big.zero" "" "Farith_Big.opp" ] "Farith_Big.z_case". + +Extract Inductive N => "Farith_Big.big_int" + [ "Farith_Big.zero" "" ] "Farith_Big.n_case". + +(** Nota: the "" above is used as an identity function "(fun p->p)" *) + +(** Efficient (but uncertified) versions for usual functions *) + +Extract Inlined Constant Pos.add => "Farith_Big.add". +Extract Inlined Constant Pos.succ => "Farith_Big.succ". +Extract Constant Pos.pred => "fun n -> Farith_Big.max Farith_Big.one (Farith_Big.pred n)". +Extract Constant Pos.sub => "fun n m -> Farith_Big.max Farith_Big.one (Farith_Big.sub n m)". +Extract Inlined Constant Pos.pred_double => "Farith_Big.pred_double". +Extract Inlined Constant Pos.mul => "Farith_Big.mult". +Extract Inlined Constant Pos.min => "Farith_Big.min". +Extract Inlined Constant Pos.max => "Farith_Big.max". +Extract Inlined Constant Pos.compare => "(Farith_Big.compare_case Eq Lt Gt)". +Extract Constant Pos.compare_cont => + "fun c x y -> Farith_Big.compare_case c Lt Gt x y". +Extract Inlined Constant Pos.eqb => "Farith_Big.eq". +Extract Inlined Constant Pos.leb => "Farith_Big.le". +Extract Inlined Constant Pos.ltb => "Farith_Big.lt". +Extract Inlined Constant Pos.to_nat => "Farith_Big.identity". +Extract Inlined Constant Pos.of_nat => "Farith_Big.identity". +Extract Inlined Constant Pos.of_succ_nat => "Farith_Big.succ". +Extract Constant Pos.add_carry => "fun p q -> Farith_Big.succ (Farith_Big.add p q)". +Extract Inlined Constant Pos.sqrt => "Farith_Big.Z.sqrt". +Extract Inlined Constant Pos.square => "Farith_Big.square". +Extract Inlined Constant Pos.eq_dec => "Farith_Big.Z.equal". +Extract Inlined Constant Pos.pow => "Farith_Big.pow_pos". +Extract Inlined Constant Pos.gcd => "Farith_Big.Z.gcd". +Extract Inlined Constant Pos.lor => "Farith_Big.Z.logor". +Extract Inlined Constant Pos.land => "Farith_Big.Z.logand". +Extract Inlined Constant Pos.lxor => "Farith_Big.Z.logxor". +Extract Inlined Constant Pos.ldiff => "Farith_Big.ldiff". +Extract Inlined Constant Pos.shiftl_nat => "Farith_Big.shiftl". +Extract Inlined Constant Pos.shiftr_nat => "Farith_Big.shiftr". +Extract Inlined Constant Pos.shiftl => "Farith_Big.shiftl". +Extract Inlined Constant Pos.shiftr => "Farith_Big.shiftr". + + +Extract Inlined Constant N.add => "Farith_Big.add". +Extract Inlined Constant N.succ => "Farith_Big.succ". +Extract Constant N.pred => "fun n -> Farith_Big.max Farith_Big.zero (Farith_Big.pred n)". +Extract Constant N.sub => "fun n m -> Farith_Big.max Farith_Big.zero (Farith_Big.sub n m)". +Extract Inlined Constant N.mul => "Farith_Big.mult". +Extract Inlined Constant N.min => "Farith_Big.min". +Extract Inlined Constant N.max => "Farith_Big.max". +Extract Constant N.div => + "fun a b -> if Farith_Big.eq b Farith_Big.zero then Farith_Big.zero else Farith_Big.div a b". +Extract Constant N.modulo => + "fun a b -> if Farith_Big.eq b Farith_Big.zero then Farith_Big.zero else Farith_Big.modulo a b". +Extract Constant N.compare => "Farith_Big.compare_case Eq Lt Gt". +Extract Inlined Constant N.succ_double => "Farith_Big.succ_double". +Extract Inlined Constant N.double => "Farith_Big.double". +Extract Inlined Constant Pos.Nsucc_double => "Farith_Big.succ_double". +Extract Inlined Constant Pos.Ndouble => "Farith_Big.double". + +Extract Inlined Constant Z.add => "Farith_Big.add". +Extract Inlined Constant Z.succ => "Farith_Big.succ". +Extract Inlined Constant Z.pred => "Farith_Big.pred". +Extract Inlined Constant Z.sub => "Farith_Big.sub". +Extract Inlined Constant Z.mul => "Farith_Big.mult". +Extract Inlined Constant Z.opp => "Farith_Big.opp". +Extract Inlined Constant Z.abs => "Farith_Big.abs". +Extract Inlined Constant Z.min => "Farith_Big.min". +Extract Inlined Constant Z.max => "Farith_Big.max". +Extract Inlined Constant Z.eqb => "Farith_Big.eq". +Extract Inlined Constant Z.leb => "Farith_Big.le". +Extract Inlined Constant Z.ltb => "Farith_Big.lt". +Extract Inlined Constant Z.geb => "Farith_Big.ge". +Extract Inlined Constant Z.gtb => "Farith_Big.gt". +Extract Inlined Constant Z.compare => "(Farith_Big.compare_case Eq Lt Gt)". +Extract Inlined Constant Z.double => "Farith_Big.double". +Extract Inlined Constant Z.succ_double => "Farith_Big.succ_double". +Extract Inlined Constant Z.pred_double => "Farith_Big.pred_double". +Extract Inlined Constant Z.pos_sub => "Farith_Big.sub". +Extract Inlined Constant Z.gcd => "Farith_Big.Z.gcd". +Extract Inlined Constant Z.sqrt => "Farith_Big.Z.sqrt". +Extract Inlined Constant Z.sqrtrem => "Farith_Big.Z.sqrt_rem". +Extract Inlined Constant Z.square => "Farith_Big.square". +Extract Inlined Constant Z.lnot => "Farith_Big.Z.lognot". +Extract Inlined Constant Z.lor => "Farith_Big.Z.logor". +Extract Inlined Constant Z.land => "Farith_Big.Z.logand". +Extract Inlined Constant Z.lxor => "Farith_Big.Z.logxor". +Extract Inlined Constant Z.ldiff => "Farith_Big.ldiff". +Extract Inlined Constant Z.eq_dec => "Farith_Big.Z.equal". +Extract Inlined Constant Z.shiftr => "Farith_Big.shiftr". +Extract Inlined Constant Z.shiftl => "Farith_Big.shiftl". +Extract Inlined Constant Z.sgn => "Farith_Big.sgn". + +Extract Inlined Constant Z.of_N => "Farith_Big.identity". +Extract Inlined Constant Z.of_nat => "Farith_Big.identity". + +Extract Inlined Constant Z.abs_N => "Farith_Big.abs". +Extract Inlined Constant Z.abs_nat => "Farith_Big.abs". + +Extract Inlined Constant Zeq_bool => "Farith_Big.eq". + +(** trunc convention *) +Extract Inlined Constant Z.rem => "Farith_Big.Z.rem". +Extract Inlined Constant Z.quot => "Farith_Big.Z.div". +Extract Inlined Constant Z.quot2 => "Farith_Big.div2_trunc". +Extract Inlined Constant Z.quotrem => "Farith_Big.Z.div_rem". + +(** floor convention *) +Extract Inlined Constant Z.modulo => "Farith_Big.mod_floor". +Extract Inlined Constant Z.div => "Farith_Big.div_floor". +Extract Inlined Constant Z.div_eucl => "Farith_Big.div_mod_floor". +Extract Inlined Constant Z.div2 => "Farith_Big.div2_floor". + +(** euclid convention *) +Require Import Zeuclid. +Extract Inlined Constant ZEuclid.modulo => "Farith_Big.Z.erem". +Extract Inlined Constant ZEuclid.div => "Farith_Big.Z.ediv". + +Extract Inlined Constant Z.pow_pos => "Farith_Big.pow_pos". + + + +Require Import Flocq.Core.Fcore_Zaux. +Require Coq.Arith.Wf_nat. +(* Extract Inlined Constant shiftl_pos => "Farith_Big.shiftl_pos". *) +Extract Inlined Constant Fcore_Zaux.iter_nat => "Farith_Big.iter_nat". +Extract Inlined Constant nat_rect => "Farith_Big.nat_rect". + + +(** Some proofs used in function realization *) + +Definition div_mod_floor a b := + let (q,r) := Z.quotrem a b in + if orb (Z.lxor (Z.sgn a) (Z.sgn b) >=? 0)%Z (r =? 0)%Z + then (q,r) + else (Z.pred q,b+r)%Z. + +Lemma Floor_of_Trunc: + forall a b, (b <> 0)%Z -> Z.div_eucl a b = div_mod_floor a b. +Proof. + intros a' b' Hb. + unfold div_mod_floor. + assert (Lmod := Z.rem_mod a' b' Hb). + assert (Ldiv := Z.quot_div a' b' Hb). + replace (Z.quotrem a' b') with ((Z.quot a' b',Z.rem a' b')) by + (compute [Z.quot Z.rem]; destruct (Z.quotrem a' b'); trivial). + replace (Z.pred (Z.quot a' b'))%Z with (-(Z.opp (Z.quot a' b')+1))%Z by omega. + rewrite Lmod. rewrite Ldiv. + pose (a := a'). pose (b := b'). + destruct a'; destruct b'; unfold Z.modulo, Z.div; simpl; trivial; + destruct (Z.pos_div_eucl p (Z.pos p0)) as [[|pq|nq] [|pr|nr]]; trivial. +Qed. + + +(* Avoid name clashes *) +Extraction Blacklist Big List String Int Z Q. + +Require Import Flocq.Flocq_version F_aux. + +Extract Inductive F_aux.Qz => "Q.t" [ "Farith_Big.q_mk" ] "Farith_Big.q_case". +Extract Inlined Constant F_aux.den => "Farith_Big.q_den". +Extract Inlined Constant F_aux.num => "Farith_Big.q_num". +Extract Inlined Constant F_aux.Qz_classify => "Q.classify". + +Extract Inductive Qz_kind => "Q.kind" [ "Q.INF" "Q.MINF" "Q.UNDEF" "Q.ZERO" "Q.NZERO" ]. +Extract Inlined Constant Qz_classify => "Q.classify". + +Extract Inlined Constant F_aux.int31 => "int". +Extract Inlined Constant F_aux.int31_zero => "0". +Extract Inlined Constant F_aux.int31_one => "1". +Extract Inlined Constant F_aux.int31_minus_one => "(-1)". + +Extract Inlined Constant F_aux.nativeint => "int". +Extract Inlined Constant F_aux.nativeint_zero => "0". +Extract Inlined Constant F_aux.nativeint_one => "1". +Extract Inlined Constant F_aux.nativeint_three => "3". +Extract Inlined Constant F_aux.nativeint_five => "5". +Extract Inlined Constant F_aux.hash_z => "Farith_Big.Z.hash". +Extract Inlined Constant F_aux.hash_bool => "Hashtbl.hash". +Extract Inlined Constant F_aux.hash_combine => "Farith_Big.combine_hash". + +Extract Inductive Fappli_IEEE.mode => "Farith_Big.mode" ["Farith_Big.NE" "Farith_Big.ZR" "Farith_Big.DN" "Farith_Big.UP" "Farith_Big.NA" ]. +Extract Inductive Fappli_IEEE.full_float => "Farith_Big.classify" ["Farith_Big.Zero" "Farith_Big.Infinity" "Farith_Big.NaN" "Farith_Big.Finite"]. + +Extract Inlined Constant F_aux.assert => "(fun b f -> assert b; f ())". + +Separate Extraction F_aux.Make F_aux.B32 F_aux.B64 Flocq.Flocq_version F_aux.check_param Fappli_IEEE.mode F_aux.D. diff --git a/farith/extracted/dune b/farith/extracted/dune new file mode 100644 index 0000000000000000000000000000000000000000..a7efb180240fab524dcc9b4c85c40e1460c0038f --- /dev/null +++ b/farith/extracted/dune @@ -0,0 +1,7 @@ +(library + (name farith_extracted) + (public_name farith._extracted) + (libraries zarith farith_big) + (wrapped false) + (flags "-w" "-33") +) diff --git a/farith/extracted/farith_BinInt.ml b/farith/extracted/farith_BinInt.ml new file mode 100644 index 0000000000000000000000000000000000000000..69bcab00b25cacc6bf8138222a0c218e7af48168 --- /dev/null +++ b/farith/extracted/farith_BinInt.ml @@ -0,0 +1,91 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +module Z = + struct + type t = Farith_Big.big_int + + (** val pow : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **) + + let pow x y = + Farith_Big.z_case + (fun _ -> + Farith_Big.one) + (fun p -> + Farith_Big.pow_pos x p) + (fun _ -> + Farith_Big.zero) + y + + (** val to_nat : Farith_Big.big_int -> Farith_Big.big_int **) + + let to_nat z = + Farith_Big.z_case + (fun _ -> + Farith_Big.zero) + (fun p -> + Farith_Big.identity p) + (fun _ -> + Farith_Big.zero) + z + + (** val to_pos : Farith_Big.big_int -> Farith_Big.big_int **) + + let to_pos z = + Farith_Big.z_case + (fun _ -> + Farith_Big.one) + (fun p -> + p) + (fun _ -> + Farith_Big.one) + z + + (** val pos_div_eucl : + Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int **) + + let rec pos_div_eucl a b = + Farith_Big.positive_case + (fun a' -> + let (q, r) = pos_div_eucl a' b in + let r' = + Farith_Big.add (Farith_Big.mult (Farith_Big.double Farith_Big.one) r) + Farith_Big.one + in + if Farith_Big.lt r' b + then ((Farith_Big.mult (Farith_Big.double Farith_Big.one) q), r') + else ((Farith_Big.add + (Farith_Big.mult (Farith_Big.double Farith_Big.one) q) + Farith_Big.one), (Farith_Big.sub r' b))) + (fun a' -> + let (q, r) = pos_div_eucl a' b in + let r' = Farith_Big.mult (Farith_Big.double Farith_Big.one) r in + if Farith_Big.lt r' b + then ((Farith_Big.mult (Farith_Big.double Farith_Big.one) q), r') + else ((Farith_Big.add + (Farith_Big.mult (Farith_Big.double Farith_Big.one) q) + Farith_Big.one), (Farith_Big.sub r' b))) + (fun _ -> + if Farith_Big.le (Farith_Big.double Farith_Big.one) b + then (Farith_Big.zero, Farith_Big.one) + else (Farith_Big.one, Farith_Big.zero)) + a + end diff --git a/farith/extracted/farith_BinInt.mli b/farith/extracted/farith_BinInt.mli new file mode 100644 index 0000000000000000000000000000000000000000..6027a4c384799ad8eb323b1e3dd6cfe1dca29979 --- /dev/null +++ b/farith/extracted/farith_BinInt.mli @@ -0,0 +1,33 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +module Z : + sig + type t = Farith_Big.big_int + + val pow : Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int + + val to_nat : Farith_Big.big_int -> Farith_Big.big_int + + val to_pos : Farith_Big.big_int -> Farith_Big.big_int + + val pos_div_eucl : + Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int + end diff --git a/farith/extracted/farith_BinPos.ml b/farith/extracted/farith_BinPos.ml new file mode 100644 index 0000000000000000000000000000000000000000..cd7efe4826199fbe24fa1b0c6f47de720f6c99d5 --- /dev/null +++ b/farith/extracted/farith_BinPos.ml @@ -0,0 +1,222 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinPosDef +open Farith_Datatypes + +module Pos = + struct + (** val add_carry : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **) + + let rec add_carry = fun p q -> Farith_Big.succ (Farith_Big.add p q) + + type mask = Pos.mask = + | IsNul + | IsPos of Farith_Big.big_int + | IsNeg + + (** val succ_double_mask : mask -> mask **) + + let succ_double_mask = function + | IsNul -> IsPos Farith_Big.one + | IsPos p -> IsPos (Farith_Big.succ_double p) + | IsNeg -> IsNeg + + (** val double_mask : mask -> mask **) + + let double_mask = function + | IsPos p -> IsPos (Farith_Big.double p) + | x0 -> x0 + + (** val double_pred_mask : Farith_Big.big_int -> mask **) + + let double_pred_mask x = + Farith_Big.positive_case + (fun p -> IsPos (Farith_Big.double (Farith_Big.double + p))) + (fun p -> IsPos (Farith_Big.double + (Farith_Big.pred_double p))) + (fun _ -> + IsNul) + x + + (** val sub_mask : Farith_Big.big_int -> Farith_Big.big_int -> mask **) + + let rec sub_mask x y = + Farith_Big.positive_case + (fun p -> + Farith_Big.positive_case + (fun q -> + double_mask (sub_mask p q)) + (fun q -> + succ_double_mask (sub_mask p q)) + (fun _ -> IsPos (Farith_Big.double + p)) + y) + (fun p -> + Farith_Big.positive_case + (fun q -> + succ_double_mask (sub_mask_carry p q)) + (fun q -> + double_mask (sub_mask p q)) + (fun _ -> IsPos + (Farith_Big.pred_double p)) + y) + (fun _ -> + Farith_Big.positive_case + (fun _ -> + IsNeg) + (fun _ -> + IsNeg) + (fun _ -> + IsNul) + y) + x + + (** val sub_mask_carry : + Farith_Big.big_int -> Farith_Big.big_int -> mask **) + + and sub_mask_carry x y = + Farith_Big.positive_case + (fun p -> + Farith_Big.positive_case + (fun q -> + succ_double_mask (sub_mask_carry p q)) + (fun q -> + double_mask (sub_mask p q)) + (fun _ -> IsPos + (Farith_Big.pred_double p)) + y) + (fun p -> + Farith_Big.positive_case + (fun q -> + double_mask (sub_mask_carry p q)) + (fun q -> + succ_double_mask (sub_mask_carry p q)) + (fun _ -> + double_pred_mask p) + y) + (fun _ -> + IsNeg) + x + + (** val iter : ('a1 -> 'a1) -> 'a1 -> Farith_Big.big_int -> 'a1 **) + + let rec iter f x n = + Farith_Big.positive_case + (fun n' -> + f (iter f (iter f x n') n')) + (fun n' -> + iter f (iter f x n') n') + (fun _ -> + f x) + n + + (** val div2 : Farith_Big.big_int -> Farith_Big.big_int **) + + let div2 p = + Farith_Big.positive_case + (fun p0 -> + p0) + (fun p0 -> + p0) + (fun _ -> + Farith_Big.one) + p + + (** val div2_up : Farith_Big.big_int -> Farith_Big.big_int **) + + let div2_up p = + Farith_Big.positive_case + (fun p0 -> + Farith_Big.succ p0) + (fun p0 -> + p0) + (fun _ -> + Farith_Big.one) + p + + (** val compare_cont : + comparison -> Farith_Big.big_int -> Farith_Big.big_int -> comparison **) + + let rec compare_cont = fun c x y -> Farith_Big.compare_case c Lt Gt x y + + (** val sqrtrem_step : + (Farith_Big.big_int -> Farith_Big.big_int) -> (Farith_Big.big_int -> + Farith_Big.big_int) -> (Farith_Big.big_int * mask) -> + Farith_Big.big_int * mask **) + + let sqrtrem_step f g = function + | (s, y) -> + (match y with + | IsPos r -> + let s' = Farith_Big.succ_double (Farith_Big.double s) in + let r' = g (f r) in + if Farith_Big.le s' r' + then ((Farith_Big.succ_double s), (sub_mask r' s')) + else ((Farith_Big.double s), (IsPos r')) + | _ -> + ((Farith_Big.double s), + (sub_mask (g (f Farith_Big.one)) (Farith_Big.double + (Farith_Big.double Farith_Big.one))))) + + (** val sqrtrem : Farith_Big.big_int -> Farith_Big.big_int * mask **) + + let rec sqrtrem p = + Farith_Big.positive_case + (fun p0 -> + Farith_Big.positive_case + (fun p1 -> + sqrtrem_step (fun x -> Farith_Big.succ_double x) (fun x -> + Farith_Big.succ_double x) (sqrtrem p1)) + (fun p1 -> + sqrtrem_step (fun x -> Farith_Big.double x) (fun x -> + Farith_Big.succ_double x) (sqrtrem p1)) + (fun _ -> (Farith_Big.one, (IsPos (Farith_Big.double + Farith_Big.one)))) + p0) + (fun p0 -> + Farith_Big.positive_case + (fun p1 -> + sqrtrem_step (fun x -> Farith_Big.succ_double x) (fun x -> + Farith_Big.double x) (sqrtrem p1)) + (fun p1 -> + sqrtrem_step (fun x -> Farith_Big.double x) (fun x -> + Farith_Big.double x) (sqrtrem p1)) + (fun _ -> (Farith_Big.one, (IsPos + Farith_Big.one))) + p0) + (fun _ -> (Farith_Big.one, + IsNul)) + p + + (** val iter_op : + ('a1 -> 'a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1 **) + + let rec iter_op op p a = + Farith_Big.positive_case + (fun p0 -> + op a (iter_op op p0 (op a a))) + (fun p0 -> + iter_op op p0 (op a a)) + (fun _ -> + a) + p + end diff --git a/farith/extracted/farith_BinPos.mli b/farith/extracted/farith_BinPos.mli new file mode 100644 index 0000000000000000000000000000000000000000..ad1aa2cfef49bd79dbc7aa57dad496c1ecb7b7b8 --- /dev/null +++ b/farith/extracted/farith_BinPos.mli @@ -0,0 +1,60 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinPosDef +open Farith_Datatypes + +module Pos : + sig + val add_carry : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int + + type mask = Pos.mask = + | IsNul + | IsPos of Farith_Big.big_int + | IsNeg + + val succ_double_mask : mask -> mask + + val double_mask : mask -> mask + + val double_pred_mask : Farith_Big.big_int -> mask + + val sub_mask : Farith_Big.big_int -> Farith_Big.big_int -> mask + + val sub_mask_carry : Farith_Big.big_int -> Farith_Big.big_int -> mask + + val iter : ('a1 -> 'a1) -> 'a1 -> Farith_Big.big_int -> 'a1 + + val div2 : Farith_Big.big_int -> Farith_Big.big_int + + val div2_up : Farith_Big.big_int -> Farith_Big.big_int + + val compare_cont : + comparison -> Farith_Big.big_int -> Farith_Big.big_int -> comparison + + val sqrtrem_step : + (Farith_Big.big_int -> Farith_Big.big_int) -> (Farith_Big.big_int -> + Farith_Big.big_int) -> (Farith_Big.big_int * mask) -> + Farith_Big.big_int * mask + + val sqrtrem : Farith_Big.big_int -> Farith_Big.big_int * mask + + val iter_op : ('a1 -> 'a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1 + end diff --git a/farith/extracted/farith_BinPosDef.ml b/farith/extracted/farith_BinPosDef.ml new file mode 100644 index 0000000000000000000000000000000000000000..a85d842db196202a9791bc6860295e8d10b9325e --- /dev/null +++ b/farith/extracted/farith_BinPosDef.ml @@ -0,0 +1,26 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +module Pos = + struct + type mask = + | IsNul + | IsPos of Farith_Big.big_int + | IsNeg + end diff --git a/farith/extracted/farith_BinPosDef.mli b/farith/extracted/farith_BinPosDef.mli new file mode 100644 index 0000000000000000000000000000000000000000..281d371e633715f4b0d2d3c66e0a6f8f5c7d1944 --- /dev/null +++ b/farith/extracted/farith_BinPosDef.mli @@ -0,0 +1,26 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +module Pos : + sig + type mask = + | IsNul + | IsPos of Farith_Big.big_int + | IsNeg + end diff --git a/farith/extracted/farith_Bool.ml b/farith/extracted/farith_Bool.ml new file mode 100644 index 0000000000000000000000000000000000000000..5ef6467c1e8d80c503e05e78d5b37807d43801bb --- /dev/null +++ b/farith/extracted/farith_Bool.ml @@ -0,0 +1,23 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +(** val eqb : bool -> bool -> bool **) + +let eqb b1 b2 = + if b1 then b2 else if b2 then false else true diff --git a/farith/extracted/farith_Bool.mli b/farith/extracted/farith_Bool.mli new file mode 100644 index 0000000000000000000000000000000000000000..dcac38d257adec1e982f126756aad803f4e452c9 --- /dev/null +++ b/farith/extracted/farith_Bool.mli @@ -0,0 +1,20 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +val eqb : bool -> bool -> bool diff --git a/farith/extracted/farith_Datatypes.ml b/farith/extracted/farith_Datatypes.ml new file mode 100644 index 0000000000000000000000000000000000000000..73c632d335d8a460f5bd9b11358b804b2976a3c9 --- /dev/null +++ b/farith/extracted/farith_Datatypes.ml @@ -0,0 +1,35 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +(** val xorb : bool -> bool -> bool **) + +let xorb b1 b2 = + if b1 then if b2 then false else true else b2 + +type comparison = +| Eq +| Lt +| Gt + +(** val coq_CompOpp : comparison -> comparison **) + +let coq_CompOpp = function +| Eq -> Eq +| Lt -> Gt +| Gt -> Lt diff --git a/farith/extracted/farith_Datatypes.mli b/farith/extracted/farith_Datatypes.mli new file mode 100644 index 0000000000000000000000000000000000000000..c9d8823044135117f8cb75ed43f819f1890f096f --- /dev/null +++ b/farith/extracted/farith_Datatypes.mli @@ -0,0 +1,27 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +val xorb : bool -> bool -> bool + +type comparison = +| Eq +| Lt +| Gt + +val coq_CompOpp : comparison -> comparison diff --git a/farith/extracted/farith_F_aux.ml b/farith/extracted/farith_F_aux.ml new file mode 100644 index 0000000000000000000000000000000000000000..55f0d277ff98faff0507879ff412f11336a28fc9 --- /dev/null +++ b/farith/extracted/farith_F_aux.ml @@ -0,0 +1,1021 @@ +(**************************************************************************) +(* 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 Farith_BinInt +open Farith_Datatypes +open Farith_Fappli_IEEE +open Farith_Fappli_IEEE_bits +open Farith_Fcore_digits + +type __ = Obj.t + +(** val least_bit_Pnat : Farith_Big.big_int -> Farith_Big.big_int **) + +let rec least_bit_Pnat n = + Farith_Big.positive_case + (fun _ -> + Farith_Big.zero) + (fun p -> Farith_Big.succ + (least_bit_Pnat p)) + (fun _ -> + Farith_Big.zero) + n + +(** val shiftr_pos : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **) + +let shiftr_pos a p = + Farith_Big.nat_rect a (fun _ -> Farith_Big.div2_floor) p + +(** val coq_Qz_zero : Q.t **) + +let coq_Qz_zero = + Farith_Big.q_mk (Farith_Big.zero, Farith_Big.one) + +(** val coq_Qz_undef : Q.t **) + +let coq_Qz_undef = + Farith_Big.q_mk (Farith_Big.zero, Farith_Big.zero) + +(** val coq_Qz_inf : Q.t **) + +let coq_Qz_inf = + Farith_Big.q_mk (Farith_Big.one, Farith_Big.zero) + +(** val coq_Qz_minus_inf : Q.t **) + +let coq_Qz_minus_inf = + Farith_Big.q_mk ((Farith_Big.opp Farith_Big.one), Farith_Big.zero) + +(** val cprec : Farith_Big.big_int -> Farith_Big.big_int **) + +let cprec mw0 = + Farith_Big.succ mw0 + +(** 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) + +type 't fconf = { mw : Farith_Big.big_int; ew : Farith_Big.big_int } + +(** val mw : 'a1 fconf -> Farith_Big.big_int **) + +let mw x = x.mw + +(** val ew : 'a1 fconf -> Farith_Big.big_int **) + +let ew x = x.ew + +(** 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)) + +(** val mk_conf : + Farith_Big.big_int -> Farith_Big.big_int -> binary_float fconf **) + +let mk_conf mw0 ew0 = + { mw = mw0; ew = ew0 } + +module Aux = + struct + (** val pl_cst : 'a1 fconf -> Farith_Big.big_int **) + + let pl_cst conf0 = + let mw0 = conf0.mw in + Farith_Big.iter_nat (fun x -> Farith_Big.double x) + (Z.to_nat (Farith_Big.pred mw0)) Farith_Big.one + + (** val default_nan_pl : 'a1 fconf -> bool * nan_pl **) + + let default_nan_pl conf0 = + (false, (pl_cst conf0)) + + (** val unop_nan_pl : 'a1 fconf -> binary_float -> bool * nan_pl **) + + let unop_nan_pl conf0 = function + | B754_nan (s, pl) -> (s, pl) + | _ -> default_nan_pl conf0 + + (** val binop_nan_pl : + 'a1 fconf -> binary_float -> binary_float -> bool * nan_pl **) + + let binop_nan_pl conf0 f1 f2 = + match f1 with + | B754_nan (s1, pl1) -> (s1, pl1) + | _ -> + (match f2 with + | B754_nan (s2, pl2) -> (s2, pl2) + | _ -> default_nan_pl conf0) + + (** val opp : 'a1 fconf -> binary_float -> binary_float **) + + let opp conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in + let emax = cemax ew0 in coq_Bopp prec emax (fun x x0 -> (x, x0)) + + (** val add : + 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float **) + + let add conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + coq_Bplus (cprec mw0) (cemax ew0) (binop_nan_pl conf0) + + (** val sub : + 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float **) + + let sub conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + coq_Bminus (cprec mw0) (cemax ew0) (binop_nan_pl conf0) + + (** val mul : + 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float **) + + let mul conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + coq_Bmult (cprec mw0) (cemax ew0) (binop_nan_pl conf0) + + (** val div : + 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float **) + + let div conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + coq_Bdiv (cprec mw0) (cemax ew0) (binop_nan_pl conf0) + + (** val sqrt : + 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float **) + + let sqrt conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + coq_Bsqrt (cprec mw0) (cemax ew0) (unop_nan_pl conf0) + + (** val abs : 'a1 fconf -> binary_float -> binary_float **) + + let abs conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in + let emax = cemax ew0 in coq_Babs prec emax (fun b x -> (b, x)) + + (** val of_bits : 'a1 fconf -> Farith_Big.big_int -> binary_float **) + + let of_bits conf0 = + let mw0 = conf0.mw in let ew0 = conf0.ew in binary_float_of_bits mw0 ew0 + + (** val to_bits : 'a1 fconf -> binary_float -> Farith_Big.big_int **) + + let to_bits conf0 = + let mw0 = conf0.mw in let ew0 = conf0.ew in bits_of_binary_float mw0 ew0 + + (** val of_z : + 'a1 fconf -> Farith_Big.mode -> Farith_Big.big_int -> binary_float **) + + let of_z conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + (fun mode z -> + binary_normalize (cprec mw0) (cemax ew0) mode z Farith_Big.zero false) + + (** val default_nan : 'a1 fconf -> binary_float **) + + let default_nan conf0 = + B754_nan ((Stdlib.fst (default_nan_pl conf0)), + (Stdlib.snd (default_nan_pl conf0))) + + (** val of_q : 'a1 fconf -> Farith_Big.mode -> Q.t -> binary_float **) + + let of_q conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + (fun mode q -> + match Q.classify q with + | Q.INF -> B754_infinity false + | Q.MINF -> B754_infinity true + | Q.UNDEF -> default_nan conf0 + | Q.ZERO -> B754_zero false + | Q.NZERO -> + (Farith_Big.z_case + (fun _ -> + default_nan conf0) + (fun pn -> + coq_FF2B (cprec mw0) (cemax ew0) + (let (p, lz) = + coq_Fdiv_core_binary (cprec mw0) pn Farith_Big.zero + (Z.to_pos (Farith_Big.q_den q)) Farith_Big.zero + in + let (mz, ez) = p in + (Farith_Big.z_case + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + (fun mz0 -> + binary_round_aux (cprec mw0) (cemax ew0) mode + (xorb false false) mz0 ez lz) + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + mz))) + (fun nn -> + coq_FF2B (cprec mw0) (cemax ew0) + (let (p, lz) = + coq_Fdiv_core_binary (cprec mw0) nn Farith_Big.zero + (Z.to_pos (Farith_Big.q_den q)) Farith_Big.zero + in + let (mz, ez) = p in + (Farith_Big.z_case + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + (fun mz0 -> + binary_round_aux (cprec mw0) (cemax ew0) mode + (xorb true false) mz0 ez lz) + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + mz))) + (Farith_Big.q_num q))) + + (** val to_q : 'a1 fconf -> binary_float -> Q.t **) + + let to_q _ = function + | B754_zero _ -> coq_Qz_zero + | B754_infinity b -> if b then coq_Qz_minus_inf else coq_Qz_inf + | B754_nan (_, _) -> coq_Qz_undef + | B754_finite (b, m, e) -> + let e' = least_bit_Pnat m in + let m' = if b then Farith_Big.opp m else m in + let e'' = Farith_Big.add e (Farith_Big.identity e') in + (Farith_Big.z_case + (fun _ -> Farith_Big.q_mk ((shiftr_pos m' e'), + Farith_Big.one)) + (fun _ -> Farith_Big.q_mk ((Farith_Big.shiftl m' e), + Farith_Big.one)) + (fun p -> Farith_Big.q_mk ((shiftr_pos m' e'), + (Farith_Big.shiftl Farith_Big.one p))) + e'') + + (** val compare_aux : + 'a1 fconf -> binary_float -> binary_float -> comparison **) + + let compare_aux _ f1 f2 = + let cmp_bool = fun b1 b2 -> + if b1 then if b2 then Eq else Lt else if b2 then Gt else Eq + in + (match f1 with + | B754_zero b1 -> + (match f2 with + | B754_zero b2 -> cmp_bool b1 b2 + | B754_infinity b -> if b then Gt else Lt + | B754_nan (_, _) -> Gt + | B754_finite (b, _, _) -> if b then Gt else Lt) + | B754_infinity b -> + if b + then (match f2 with + | B754_infinity b0 -> if b0 then Eq else Lt + | B754_nan (_, _) -> Gt + | _ -> Lt) + else (match f2 with + | B754_infinity b0 -> if b0 then Gt else Eq + | _ -> Gt) + | B754_nan (b1, n) -> + (match f2 with + | B754_nan (b2, n0) -> + (match cmp_bool b1 b2 with + | Eq -> (Farith_Big.compare_case Eq Lt Gt) n n0 + | x -> x) + | _ -> Lt) + | B754_finite (s1, m1, e1) -> + if s1 + then (match f2 with + | B754_zero _ -> Lt + | B754_infinity b -> if b then Gt else Lt + | B754_nan (_, _) -> Gt + | B754_finite (s2, m2, e2) -> + if s1 + then if s2 + then (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with + | Eq -> + coq_CompOpp + ((Farith_Big.compare_case Eq Lt Gt) m1 m2) + | Lt -> Gt + | Gt -> Lt) + else Lt + else if s2 + then Gt + else (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with + | Eq -> (Farith_Big.compare_case Eq Lt Gt) m1 m2 + | x -> x)) + else (match f2 with + | B754_infinity b -> if b then Gt else Lt + | B754_finite (s2, m2, e2) -> + if s1 + then if s2 + then (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with + | Eq -> + coq_CompOpp + ((Farith_Big.compare_case Eq Lt Gt) m1 m2) + | Lt -> Gt + | Gt -> Lt) + else Lt + else if s2 + then Gt + else (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with + | Eq -> (Farith_Big.compare_case Eq Lt Gt) m1 m2 + | x -> x) + | _ -> Gt)) + + (** val compare : 'a1 fconf -> binary_float -> binary_float -> int **) + + let compare conf0 f1 f2 = + match compare_aux conf0 f1 f2 with + | Eq -> 0 + | Lt -> (-1) + | Gt -> 1 + + (** val equal : 'a1 fconf -> binary_float -> binary_float -> bool **) + + let equal conf0 f1 f2 = + match compare_aux conf0 f1 f2 with + | Eq -> true + | _ -> false + + (** val hash : 'a1 fconf -> binary_float -> int **) + + let hash _ = function + | B754_zero b -> Hashtbl.hash b + | B754_infinity b -> Farith_Big.combine_hash 3 (Hashtbl.hash b) + | B754_nan (b, n0) -> + Farith_Big.combine_hash 5 + (Farith_Big.combine_hash (Farith_Big.Z.hash n0) (Hashtbl.hash b)) + | B754_finite (b, m, e) -> + Farith_Big.combine_hash (Farith_Big.Z.hash m) + (Farith_Big.combine_hash (Farith_Big.Z.hash e) (Hashtbl.hash b)) + + (** val fcompare : + 'a1 fconf -> binary_float -> binary_float -> int option **) + + let fcompare conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in + let emax = cemax ew0 in + (fun f1 f2 -> + match coq_Bcompare prec emax f1 f2 with + | Some c -> + (match c with + | Eq -> Some 0 + | Lt -> Some (-1) + | Gt -> Some 1) + | None -> None) + + (** val le : 'a1 fconf -> binary_float -> binary_float -> bool **) + + let le conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in + let emax = cemax ew0 in + (fun f1 f2 -> + match coq_Bcompare prec emax f1 f2 with + | Some c -> + (match c with + | Gt -> false + | _ -> true) + | None -> false) + + (** val lt : 'a1 fconf -> binary_float -> binary_float -> bool **) + + let lt conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in + let emax = cemax ew0 in + (fun f1 f2 -> + match coq_Bcompare prec emax f1 f2 with + | Some c -> + (match c with + | Lt -> true + | _ -> false) + | None -> false) + + (** val ge : 'a1 fconf -> binary_float -> binary_float -> bool **) + + let ge conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in + let emax = cemax ew0 in + (fun f1 f2 -> + match coq_Bcompare prec emax f1 f2 with + | Some c -> + (match c with + | Lt -> false + | _ -> true) + | None -> false) + + (** val gt : 'a1 fconf -> binary_float -> binary_float -> bool **) + + let gt conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in + let emax = cemax ew0 in + (fun f1 f2 -> + match coq_Bcompare prec emax f1 f2 with + | Some c -> + (match c with + | Gt -> true + | _ -> false) + | None -> false) + + (** val eq : 'a1 fconf -> binary_float -> binary_float -> bool **) + + let eq conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in + let emax = cemax ew0 in + (fun f1 f2 -> + match coq_Bcompare prec emax f1 f2 with + | Some c -> + (match c with + | Eq -> true + | _ -> false) + | None -> false) + + (** val neq : 'a1 fconf -> binary_float -> binary_float -> bool **) + + let neq conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in + let emax = cemax ew0 in + (fun f1 f2 -> + match coq_Bcompare prec emax f1 f2 with + | Some c -> + (match c with + | Eq -> false + | _ -> true) + | None -> true) + + (** val infinity : 'a1 fconf -> bool -> binary_float **) + + let infinity _ b = + B754_infinity b + + (** val infp : 'a1 fconf -> binary_float **) + + let infp _ = + B754_infinity false + + (** val infm : 'a1 fconf -> binary_float **) + + let infm _ = + B754_infinity true + + (** val zero : 'a1 fconf -> bool -> binary_float **) + + let zero _ b = + B754_zero b + + (** val zerop : 'a1 fconf -> binary_float **) + + let zerop _ = + B754_zero false + + (** val nan : 'a1 fconf -> bool -> Farith_Big.big_int -> binary_float **) + + let nan conf0 = + let mw0 = conf0.mw in + let prec = cprec mw0 in + (fun b pl -> + let pl0 = + (fun b f -> assert b; f ()) (Farith_Big.lt Farith_Big.zero pl) + (fun _ -> Z.to_pos pl) + in + let pl1 = + (fun b f -> assert b; f ()) (Farith_Big.lt (digits2_pos pl0) prec) + (fun _ -> pl0) + in + B754_nan (b, pl1)) + + (** val finite : + 'a1 fconf -> Farith_Big.mode -> Farith_Big.big_int -> + Farith_Big.big_int -> binary_float **) + + let finite conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + (fun mode m e -> binary_normalize (cprec mw0) (cemax ew0) mode m e false) + + (** val classify : 'a1 fconf -> binary_float -> Farith_Big.classify **) + + let classify conf0 = + let mw0 = conf0.mw in + let ew0 = conf0.ew in + let prec = cprec mw0 in let emax = cemax ew0 in coq_B2FF prec emax + end + +module D = + struct + (** val opp : 'a1 fconf -> 'a1 -> 'a1 **) + + let opp conf0 = + Obj.magic Aux.opp conf0 + + (** val add : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 -> 'a1 **) + + let add conf0 = + Obj.magic Aux.add conf0 + + (** val sub : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 -> 'a1 **) + + let sub conf0 = + Obj.magic Aux.sub conf0 + + (** val mul : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 -> 'a1 **) + + let mul conf0 = + Obj.magic Aux.mul conf0 + + (** val div : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 -> 'a1 **) + + let div conf0 = + Obj.magic Aux.div conf0 + + (** val sqrt : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 **) + + let sqrt conf0 = + Obj.magic Aux.sqrt conf0 + + (** val abs : 'a1 fconf -> 'a1 -> 'a1 **) + + let abs conf0 = + Obj.magic Aux.abs conf0 + + (** val of_bits : 'a1 fconf -> Farith_Big.big_int -> 'a1 **) + + let of_bits conf0 = + Obj.magic Aux.of_bits conf0 + + (** val to_bits : 'a1 fconf -> 'a1 -> Farith_Big.big_int **) + + let to_bits conf0 = + Obj.magic Aux.to_bits conf0 + + (** val of_z : 'a1 fconf -> Farith_Big.mode -> Farith_Big.big_int -> 'a1 **) + + let of_z conf0 = + Obj.magic Aux.of_z conf0 + + (** val of_q : 'a1 fconf -> Farith_Big.mode -> Q.t -> 'a1 **) + + let of_q conf0 = + Obj.magic Aux.of_q conf0 + + (** val to_q : 'a1 fconf -> 'a1 -> Q.t **) + + let to_q conf0 = + Obj.magic Aux.to_q conf0 + + (** val compare : 'a1 fconf -> 'a1 -> 'a1 -> int **) + + let compare conf0 = + Obj.magic Aux.compare conf0 + + (** val equal : 'a1 fconf -> 'a1 -> 'a1 -> bool **) + + let equal conf0 = + Obj.magic Aux.equal conf0 + + (** val hash : 'a1 fconf -> 'a1 -> int **) + + let hash conf0 = + Obj.magic Aux.hash conf0 + + (** val lt : 'a1 fconf -> 'a1 -> 'a1 -> bool **) + + let lt conf0 = + Obj.magic Aux.lt conf0 + + (** val le : 'a1 fconf -> 'a1 -> 'a1 -> bool **) + + let le conf0 = + Obj.magic Aux.ge conf0 + + (** val gt : 'a1 fconf -> 'a1 -> 'a1 -> bool **) + + let gt conf0 = + Obj.magic Aux.gt conf0 + + (** val ge : 'a1 fconf -> 'a1 -> 'a1 -> bool **) + + let ge conf0 = + Obj.magic Aux.ge conf0 + + (** val eq : 'a1 fconf -> 'a1 -> 'a1 -> bool **) + + let eq conf0 = + Obj.magic Aux.eq conf0 + + (** val neq : 'a1 fconf -> 'a1 -> 'a1 -> bool **) + + let neq conf0 = + Obj.magic Aux.neq conf0 + + (** val fcompare : 'a1 fconf -> 'a1 -> 'a1 -> int option **) + + let fcompare conf0 = + Obj.magic Aux.fcompare conf0 + + (** val infinity : 'a1 fconf -> bool -> 'a1 **) + + let infinity conf0 = + Obj.magic Aux.infinity conf0 + + (** val zero : 'a1 fconf -> bool -> 'a1 **) + + let zero conf0 = + Obj.magic Aux.zero conf0 + + (** val nan : 'a1 fconf -> bool -> Farith_Big.big_int -> 'a1 **) + + let nan conf0 = + Obj.magic Aux.nan conf0 + + (** val infp : 'a1 fconf -> 'a1 **) + + let infp conf0 = + Obj.magic Aux.infp conf0 + + (** val infm : 'a1 fconf -> 'a1 **) + + let infm conf0 = + Obj.magic Aux.infm conf0 + + (** val zerop : 'a1 fconf -> 'a1 **) + + let zerop conf0 = + Obj.magic Aux.zerop conf0 + + (** val default_nan : 'a1 fconf -> 'a1 **) + + let default_nan conf0 = + Obj.magic Aux.default_nan conf0 + + (** val finite : 'a1 fconf -> Farith_Big.mode -> Z.t -> Z.t -> 'a1 **) + + let finite conf0 = + Obj.magic Aux.finite conf0 + + (** val classify : 'a1 fconf -> 'a1 -> Farith_Big.classify **) + + let classify conf0 = + Obj.magic Aux.classify conf0 + + (** val cast_to_t : 'a1 fconf -> 'a1 -> binary_float **) + + let cast_to_t _ x = + Obj.magic x + + (** val conv : 'a1 fconf -> 'a2 fconf -> Farith_Big.mode -> 'a1 -> 'a2 **) + + let conv _ conf2 mode f = + match Obj.magic f with + | B754_nan (b, _) -> + Obj.magic (B754_nan (b, (Stdlib.snd (Aux.default_nan_pl conf2)))) + | B754_finite (sx, mx, ex) -> + Obj.magic coq_FF2B (cprec conf2.mw) (cemax conf2.ew) + (binary_round (cprec conf2.mw) (cemax conf2.ew) mode sx mx ex) + | x -> Obj.magic x + + (** val roundq : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> Q.t -> + Q.t **) + + let roundq mw0 ew0 mode x = + let conf0 = + (fun b f -> assert b; f ()) (check_param mw0 ew0) (fun _ -> + mk_conf mw0 ew0) + in + to_q conf0 (of_q conf0 mode x) + end + +module type S = + sig + type t + + val conf : t fconf + + val opp : 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 of_bits : Farith_Big.big_int -> t + + val to_bits : t -> Farith_Big.big_int + + val of_z : Farith_Big.mode -> Farith_Big.big_int -> t + + val of_q : Farith_Big.mode -> Q.t -> t + + val to_q : t -> Q.t + + val compare : t -> t -> int + + val equal : t -> t -> bool + + val hash : t -> int + + val lt : t -> t -> bool + + val le : t -> t -> bool + + val gt : t -> t -> bool + + val ge : t -> t -> bool + + val eq : t -> t -> bool + + val neq : t -> t -> bool + + val fcompare : t -> t -> int option + + val conv : 'a1 fconf -> Farith_Big.mode -> t -> 'a1 + + val infinity : bool -> t + + val zero : bool -> t + + val nan : bool -> Farith_Big.big_int -> t + + val infp : t + + val infm : t + + val zerop : t + + val default_nan : t + + val finite : Farith_Big.mode -> Z.t -> Z.t -> t + + val classify : t -> Farith_Big.classify + end + +module type P = + sig + val mw : Farith_Big.big_int + + val ew : Farith_Big.big_int + end + +module Make = + functor (P__0:P) -> + struct + type t = binary_float + + (** val conf : t fconf **) + + let conf = + mk_conf P__0.mw P__0.ew + + (** val opp : binary_float -> binary_float **) + + let opp = + Aux.opp conf + + (** val add : + Farith_Big.mode -> binary_float -> binary_float -> binary_float **) + + let add = + Aux.add conf + + (** val sub : + Farith_Big.mode -> binary_float -> binary_float -> binary_float **) + + let sub = + Aux.sub conf + + (** val mul : + Farith_Big.mode -> binary_float -> binary_float -> binary_float **) + + let mul = + Aux.mul conf + + (** val div : + Farith_Big.mode -> binary_float -> binary_float -> binary_float **) + + let div = + Aux.div conf + + (** val sqrt : Farith_Big.mode -> binary_float -> binary_float **) + + let sqrt = + Aux.sqrt conf + + (** val abs : binary_float -> binary_float **) + + let abs = + Aux.abs conf + + (** val of_bits : Farith_Big.big_int -> binary_float **) + + let of_bits = + Aux.of_bits conf + + (** val to_bits : binary_float -> Farith_Big.big_int **) + + let to_bits = + Aux.to_bits conf + + (** val of_z : Farith_Big.mode -> Farith_Big.big_int -> binary_float **) + + let of_z = + Aux.of_z conf + + (** val of_q : Farith_Big.mode -> Q.t -> binary_float **) + + let of_q = + Aux.of_q conf + + (** val to_q : binary_float -> Q.t **) + + let to_q = + Aux.to_q conf + + (** val compare : binary_float -> binary_float -> int **) + + let compare = + Aux.compare conf + + (** val equal : binary_float -> binary_float -> bool **) + + let equal = + Aux.equal conf + + (** val hash : binary_float -> int **) + + let hash = + Aux.hash conf + + (** val lt : binary_float -> binary_float -> bool **) + + let lt = + Aux.lt conf + + (** val le : binary_float -> binary_float -> bool **) + + let le = + Aux.le conf + + (** val gt : binary_float -> binary_float -> bool **) + + let gt = + Aux.gt conf + + (** val ge : binary_float -> binary_float -> bool **) + + let ge = + Aux.ge conf + + (** val eq : binary_float -> binary_float -> bool **) + + let eq = + Aux.eq conf + + (** val neq : binary_float -> binary_float -> bool **) + + let neq = + Aux.neq conf + + (** val fcompare : binary_float -> binary_float -> int option **) + + let fcompare = + Aux.fcompare conf + + (** val conv : 'a1 fconf -> Farith_Big.mode -> t -> 'a1 **) + + let conv conf2 mode x = + D.conv conf conf2 mode x + + (** val infinity : bool -> binary_float **) + + let infinity = + Aux.infinity conf + + (** val zero : bool -> binary_float **) + + let zero = + Aux.zero conf + + (** val nan : bool -> Farith_Big.big_int -> binary_float **) + + let nan = + Aux.nan conf + + (** val infp : binary_float **) + + let infp = + Aux.infp conf + + (** val infm : binary_float **) + + let infm = + Aux.infm conf + + (** val zerop : binary_float **) + + let zerop = + Aux.zerop conf + + (** val default_nan : binary_float **) + + let default_nan = + Aux.default_nan conf + + (** val finite : + Farith_Big.mode -> Farith_Big.big_int -> Farith_Big.big_int -> + binary_float **) + + let finite = + Aux.finite conf + + (** val classify : binary_float -> Farith_Big.classify **) + + let classify = + Aux.classify conf + end + +module P_B32 = + struct + (** 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))) + end + +module P_B64 = + struct + (** val mw : Farith_Big.big_int **) + + let mw = + (Farith_Big.double (Farith_Big.double (Farith_Big.succ_double + (Farith_Big.double (Farith_Big.succ_double Farith_Big.one))))) + + (** val ew : Farith_Big.big_int **) + + let ew = + (Farith_Big.succ_double (Farith_Big.succ_double (Farith_Big.double + Farith_Big.one))) + end + +module B32 = Make(P_B32) + +module B64 = Make(P_B64) diff --git a/farith/extracted/farith_F_aux.mli b/farith/extracted/farith_F_aux.mli new file mode 100644 index 0000000000000000000000000000000000000000..d16b9643a14a9df259c6ef6bc8f69b415162a2e3 --- /dev/null +++ b/farith/extracted/farith_F_aux.mli @@ -0,0 +1,452 @@ +(**************************************************************************) +(* 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 Farith_BinInt +open Farith_Datatypes +open Farith_Fappli_IEEE +open Farith_Fappli_IEEE_bits +open Farith_Fcore_digits + +type __ = Obj.t + +val least_bit_Pnat : Farith_Big.big_int -> Farith_Big.big_int + +val shiftr_pos : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int + +val coq_Qz_zero : Q.t + +val coq_Qz_undef : Q.t + +val coq_Qz_inf : Q.t + +val coq_Qz_minus_inf : Q.t + +val cprec : Farith_Big.big_int -> Farith_Big.big_int + +val cemax : Farith_Big.big_int -> Farith_Big.big_int + +type 't fconf = { mw : Farith_Big.big_int; ew : Farith_Big.big_int } + +val mw : 'a1 fconf -> Farith_Big.big_int + +val ew : 'a1 fconf -> Farith_Big.big_int + +val check_param : Farith_Big.big_int -> Farith_Big.big_int -> bool + +val mk_conf : Farith_Big.big_int -> Farith_Big.big_int -> binary_float fconf + +module Aux : + sig + val pl_cst : 'a1 fconf -> Farith_Big.big_int + + val default_nan_pl : 'a1 fconf -> bool * nan_pl + + val unop_nan_pl : 'a1 fconf -> binary_float -> bool * nan_pl + + val binop_nan_pl : + 'a1 fconf -> binary_float -> binary_float -> bool * nan_pl + + val opp : 'a1 fconf -> binary_float -> binary_float + + val add : + 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float + + val sub : + 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float + + val mul : + 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float + + val div : + 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float + + val sqrt : 'a1 fconf -> Farith_Big.mode -> binary_float -> binary_float + + val abs : 'a1 fconf -> binary_float -> binary_float + + val of_bits : 'a1 fconf -> Farith_Big.big_int -> binary_float + + val to_bits : 'a1 fconf -> binary_float -> Farith_Big.big_int + + val of_z : + 'a1 fconf -> Farith_Big.mode -> Farith_Big.big_int -> binary_float + + val default_nan : 'a1 fconf -> binary_float + + val of_q : 'a1 fconf -> Farith_Big.mode -> Q.t -> binary_float + + val to_q : 'a1 fconf -> binary_float -> Q.t + + val compare_aux : 'a1 fconf -> binary_float -> binary_float -> comparison + + val compare : 'a1 fconf -> binary_float -> binary_float -> int + + val equal : 'a1 fconf -> binary_float -> binary_float -> bool + + val hash : 'a1 fconf -> binary_float -> int + + val fcompare : 'a1 fconf -> binary_float -> binary_float -> int option + + val le : 'a1 fconf -> binary_float -> binary_float -> bool + + val lt : 'a1 fconf -> binary_float -> binary_float -> bool + + val ge : 'a1 fconf -> binary_float -> binary_float -> bool + + val gt : 'a1 fconf -> binary_float -> binary_float -> bool + + val eq : 'a1 fconf -> binary_float -> binary_float -> bool + + val neq : 'a1 fconf -> binary_float -> binary_float -> bool + + val infinity : 'a1 fconf -> bool -> binary_float + + val infp : 'a1 fconf -> binary_float + + val infm : 'a1 fconf -> binary_float + + val zero : 'a1 fconf -> bool -> binary_float + + val zerop : 'a1 fconf -> binary_float + + val nan : 'a1 fconf -> bool -> Farith_Big.big_int -> binary_float + + val finite : + 'a1 fconf -> Farith_Big.mode -> Farith_Big.big_int -> Farith_Big.big_int + -> binary_float + + val classify : 'a1 fconf -> binary_float -> Farith_Big.classify + end + +module D : + sig + val opp : 'a1 fconf -> 'a1 -> 'a1 + + val add : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 -> 'a1 + + val sub : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 -> 'a1 + + val mul : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 -> 'a1 + + val div : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 -> 'a1 + + val sqrt : 'a1 fconf -> Farith_Big.mode -> 'a1 -> 'a1 + + val abs : 'a1 fconf -> 'a1 -> 'a1 + + val of_bits : 'a1 fconf -> Farith_Big.big_int -> 'a1 + + val to_bits : 'a1 fconf -> 'a1 -> Farith_Big.big_int + + val of_z : 'a1 fconf -> Farith_Big.mode -> Farith_Big.big_int -> 'a1 + + val of_q : 'a1 fconf -> Farith_Big.mode -> Q.t -> 'a1 + + val to_q : 'a1 fconf -> 'a1 -> Q.t + + val compare : 'a1 fconf -> 'a1 -> 'a1 -> int + + val equal : 'a1 fconf -> 'a1 -> 'a1 -> bool + + val hash : 'a1 fconf -> 'a1 -> int + + val lt : 'a1 fconf -> 'a1 -> 'a1 -> bool + + val le : 'a1 fconf -> 'a1 -> 'a1 -> bool + + val gt : 'a1 fconf -> 'a1 -> 'a1 -> bool + + val ge : 'a1 fconf -> 'a1 -> 'a1 -> bool + + val eq : 'a1 fconf -> 'a1 -> 'a1 -> bool + + val neq : 'a1 fconf -> 'a1 -> 'a1 -> bool + + val fcompare : 'a1 fconf -> 'a1 -> 'a1 -> int option + + val infinity : 'a1 fconf -> bool -> 'a1 + + val zero : 'a1 fconf -> bool -> 'a1 + + val nan : 'a1 fconf -> bool -> Farith_Big.big_int -> 'a1 + + val infp : 'a1 fconf -> 'a1 + + val infm : 'a1 fconf -> 'a1 + + val zerop : 'a1 fconf -> 'a1 + + val default_nan : 'a1 fconf -> 'a1 + + val finite : 'a1 fconf -> Farith_Big.mode -> Z.t -> Z.t -> 'a1 + + val classify : 'a1 fconf -> 'a1 -> Farith_Big.classify + + val cast_to_t : 'a1 fconf -> 'a1 -> binary_float + + val conv : 'a1 fconf -> 'a2 fconf -> Farith_Big.mode -> 'a1 -> 'a2 + + val roundq : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> Q.t -> Q.t + end + +module type S = + sig + type t + + val conf : t fconf + + val opp : 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 of_bits : Farith_Big.big_int -> t + + val to_bits : t -> Farith_Big.big_int + + val of_z : Farith_Big.mode -> Farith_Big.big_int -> t + + val of_q : Farith_Big.mode -> Q.t -> t + + val to_q : t -> Q.t + + val compare : t -> t -> int + + val equal : t -> t -> bool + + val hash : t -> int + + val lt : t -> t -> bool + + val le : t -> t -> bool + + val gt : t -> t -> bool + + val ge : t -> t -> bool + + val eq : t -> t -> bool + + val neq : t -> t -> bool + + val fcompare : t -> t -> int option + + val conv : 'a1 fconf -> Farith_Big.mode -> t -> 'a1 + + val infinity : bool -> t + + val zero : bool -> t + + val nan : bool -> Farith_Big.big_int -> t + + val infp : t + + val infm : t + + val zerop : t + + val default_nan : t + + val finite : Farith_Big.mode -> Z.t -> Z.t -> t + + val classify : t -> Farith_Big.classify + end + +module type P = + sig + val mw : Farith_Big.big_int + + val ew : Farith_Big.big_int + end + +module Make : + functor (P__0:P) -> + S with type t = binary_float + +module P_B32 : + sig + val mw : Farith_Big.big_int + + val ew : Farith_Big.big_int + end + +module P_B64 : + sig + val mw : Farith_Big.big_int + + val ew : Farith_Big.big_int + end + +module B32 : + sig + type t = binary_float + + val conf : t fconf + + val opp : 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 of_bits : Farith_Big.big_int -> t + + val to_bits : t -> Farith_Big.big_int + + val of_z : Farith_Big.mode -> Farith_Big.big_int -> t + + val of_q : Farith_Big.mode -> Q.t -> t + + val to_q : t -> Q.t + + val compare : t -> t -> int + + val equal : t -> t -> bool + + val hash : t -> int + + val lt : t -> t -> bool + + val le : t -> t -> bool + + val gt : t -> t -> bool + + val ge : t -> t -> bool + + val eq : t -> t -> bool + + val neq : t -> t -> bool + + val fcompare : t -> t -> int option + + val conv : 'a1 fconf -> Farith_Big.mode -> t -> 'a1 + + val infinity : bool -> t + + val zero : bool -> t + + val nan : bool -> Farith_Big.big_int -> t + + val infp : t + + val infm : t + + val zerop : t + + val default_nan : t + + val finite : Farith_Big.mode -> Z.t -> Z.t -> t + + val classify : t -> Farith_Big.classify + end + +module B64 : + sig + type t = binary_float + + val conf : t fconf + + val opp : 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 of_bits : Farith_Big.big_int -> t + + val to_bits : t -> Farith_Big.big_int + + val of_z : Farith_Big.mode -> Farith_Big.big_int -> t + + val of_q : Farith_Big.mode -> Q.t -> t + + val to_q : t -> Q.t + + val compare : t -> t -> int + + val equal : t -> t -> bool + + val hash : t -> int + + val lt : t -> t -> bool + + val le : t -> t -> bool + + val gt : t -> t -> bool + + val ge : t -> t -> bool + + val eq : t -> t -> bool + + val neq : t -> t -> bool + + val fcompare : t -> t -> int option + + val conv : 'a1 fconf -> Farith_Big.mode -> t -> 'a1 + + val infinity : bool -> t + + val zero : bool -> t + + val nan : bool -> Farith_Big.big_int -> t + + val infp : t + + val infm : t + + val zerop : t + + val default_nan : t + + val finite : Farith_Big.mode -> Z.t -> Z.t -> t + + val classify : t -> Farith_Big.classify + end diff --git a/farith/extracted/farith_Fappli_IEEE.ml b/farith/extracted/farith_Fappli_IEEE.ml new file mode 100644 index 0000000000000000000000000000000000000000..7940996c878c22bfe056b51414e4e04e4c7645a8 --- /dev/null +++ b/farith/extracted/farith_Fappli_IEEE.ml @@ -0,0 +1,554 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinInt +open Farith_BinPos +open Farith_Bool +open Farith_Datatypes +open Farith_Fcalc_bracket +open Farith_Fcalc_round +open Farith_Fcore_FLT +open Farith_Fcore_Zaux +open Farith_Fcore_digits +open Farith_Zpower + +type nan_pl = Farith_Big.big_int + +type binary_float = +| B754_zero of bool +| B754_infinity of bool +| B754_nan of bool * nan_pl +| B754_finite of bool * Farith_Big.big_int * Farith_Big.big_int + +(** val coq_FF2B : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.classify -> + binary_float **) + +let coq_FF2B _ _ = function +| Farith_Big.Zero s -> B754_zero s +| Farith_Big.Infinity s -> B754_infinity s +| Farith_Big.NaN (b, pl) -> B754_nan (b, pl) +| Farith_Big.Finite (s, m, e) -> B754_finite (s, m, e) + +(** val coq_B2FF : + Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> + Farith_Big.classify **) + +let coq_B2FF _ _ = function +| B754_zero s -> Farith_Big.Zero s +| B754_infinity s -> Farith_Big.Infinity s +| B754_nan (b, n) -> Farith_Big.NaN (b, n) +| B754_finite (s, m, e) -> Farith_Big.Finite (s, m, e) + +(** val coq_Bopp : + Farith_Big.big_int -> Farith_Big.big_int -> (bool -> nan_pl -> + bool * nan_pl) -> binary_float -> binary_float **) + +let coq_Bopp _ _ opp_nan = function +| B754_zero sx -> B754_zero (Stdlib.not sx) +| B754_infinity sx -> B754_infinity (Stdlib.not sx) +| B754_nan (sx, plx) -> + let (sres, plres) = opp_nan sx plx in B754_nan (sres, plres) +| B754_finite (sx, mx, ex) -> B754_finite ((Stdlib.not sx), mx, ex) + +(** val coq_Babs : + Farith_Big.big_int -> Farith_Big.big_int -> (bool -> nan_pl -> + bool * nan_pl) -> binary_float -> binary_float **) + +let coq_Babs _ _ abs_nan = function +| B754_zero _ -> B754_zero false +| B754_infinity _ -> B754_infinity false +| B754_nan (sx, plx) -> + let (sres, plres) = abs_nan sx plx in B754_nan (sres, plres) +| B754_finite (_, mx, ex) -> B754_finite (false, mx, ex) + +(** val coq_Bcompare : + Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float + -> comparison option **) + +let coq_Bcompare _ _ f1 f2 = + match f1 with + | B754_zero _ -> + (match f2 with + | B754_zero _ -> Some Eq + | B754_infinity b -> if b then Some Gt else Some Lt + | B754_nan (_, _) -> None + | B754_finite (b, _, _) -> if b then Some Gt else Some Lt) + | B754_infinity b -> + if b + then (match f2 with + | B754_infinity b0 -> if b0 then Some Eq else Some Lt + | B754_nan (_, _) -> None + | _ -> Some Lt) + else (match f2 with + | B754_infinity b0 -> if b0 then Some Gt else Some Eq + | B754_nan (_, _) -> None + | _ -> Some Gt) + | B754_nan (_, _) -> None + | B754_finite (s1, m1, e1) -> + if s1 + then (match f2 with + | B754_zero _ -> Some Lt + | B754_infinity b -> if b then Some Gt else Some Lt + | B754_nan (_, _) -> None + | B754_finite (s2, m2, e2) -> + if s1 + then if s2 + then (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with + | Eq -> Some (coq_CompOpp (Pos.compare_cont Eq m1 m2)) + | Lt -> Some Gt + | Gt -> Some Lt) + else Some Lt + else if s2 + then Some Gt + else (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with + | Eq -> Some (Pos.compare_cont Eq m1 m2) + | x -> Some x)) + else (match f2 with + | B754_zero _ -> Some Gt + | B754_infinity b -> if b then Some Gt else Some Lt + | B754_nan (_, _) -> None + | B754_finite (s2, m2, e2) -> + if s1 + then if s2 + then (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with + | Eq -> Some (coq_CompOpp (Pos.compare_cont Eq m1 m2)) + | Lt -> Some Gt + | Gt -> Some Lt) + else Some Lt + else if s2 + then Some Gt + else (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with + | Eq -> Some (Pos.compare_cont Eq m1 m2) + | x -> Some x)) + +type shr_record = { shr_m : Farith_Big.big_int; shr_r : bool; shr_s : bool } + +(** val shr_m : shr_record -> Farith_Big.big_int **) + +let shr_m x = x.shr_m + +(** val shr_1 : shr_record -> shr_record **) + +let shr_1 mrs = + let { shr_m = m; shr_r = r; shr_s = s } = mrs in + let s0 = (||) r s in + (Farith_Big.z_case + (fun _ -> { shr_m = Farith_Big.zero; shr_r = false; shr_s = + s0 }) + (fun p0 -> + Farith_Big.positive_case + (fun p -> { shr_m = p; shr_r = true; shr_s = + s0 }) + (fun p -> { shr_m = p; shr_r = false; shr_s = + s0 }) + (fun _ -> { shr_m = Farith_Big.zero; shr_r = true; shr_s = + s0 }) + p0) + (fun p0 -> + Farith_Big.positive_case + (fun p -> { shr_m = (Farith_Big.opp p); shr_r = true; shr_s = + s0 }) + (fun p -> { shr_m = (Farith_Big.opp p); shr_r = false; shr_s = + s0 }) + (fun _ -> { shr_m = Farith_Big.zero; shr_r = true; shr_s = + s0 }) + p0) + m) + +(** val loc_of_shr_record : shr_record -> location **) + +let loc_of_shr_record mrs = + let { shr_m = _; shr_r = shr_r0; shr_s = shr_s0 } = mrs in + if shr_r0 + then if shr_s0 then Coq_loc_Inexact Gt else Coq_loc_Inexact Eq + else if shr_s0 then Coq_loc_Inexact Lt else Coq_loc_Exact + +(** val shr_record_of_loc : Farith_Big.big_int -> location -> shr_record **) + +let shr_record_of_loc m = function +| Coq_loc_Exact -> { shr_m = m; shr_r = false; shr_s = false } +| Coq_loc_Inexact c -> + (match c with + | Eq -> { shr_m = m; shr_r = true; shr_s = false } + | Lt -> { shr_m = m; shr_r = false; shr_s = true } + | Gt -> { shr_m = m; shr_r = true; shr_s = true }) + +(** val shr : + shr_record -> Farith_Big.big_int -> Farith_Big.big_int -> + shr_record * Farith_Big.big_int **) + +let shr mrs e n = + Farith_Big.z_case + (fun _ -> (mrs, + e)) + (fun p -> ((iter_pos shr_1 p mrs), + (Farith_Big.add e n))) + (fun _ -> (mrs, + e)) + n + +(** val shr_fexp : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int -> location -> shr_record * Farith_Big.big_int **) + +let shr_fexp prec emax = + let emin = + Farith_Big.sub + (Farith_Big.sub (Farith_Big.succ_double Farith_Big.one) emax) prec + in + let fexp = coq_FLT_exp emin prec in + (fun m e l -> + shr (shr_record_of_loc m l) e + (Farith_Big.sub (fexp (Farith_Big.add (coq_Zdigits2 m) e)) e)) + +(** val choice_mode : + Farith_Big.mode -> bool -> Farith_Big.big_int -> location -> + Farith_Big.big_int **) + +let choice_mode m sx mx lx = + match m with + | Farith_Big.NE -> + cond_incr (round_N (Stdlib.not (coq_Zeven mx)) lx) mx + | Farith_Big.ZR -> mx + | Farith_Big.DN -> cond_incr (round_sign_DN sx lx) mx + | Farith_Big.UP -> cond_incr (round_sign_UP sx lx) mx + | Farith_Big.NA -> cond_incr (round_N true lx) mx + +(** val overflow_to_inf : Farith_Big.mode -> bool -> bool **) + +let overflow_to_inf m s = + match m with + | Farith_Big.ZR -> false + | Farith_Big.DN -> s + | Farith_Big.UP -> Stdlib.not s + | _ -> true + +(** val binary_overflow : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool -> + Farith_Big.classify **) + +let binary_overflow prec emax m s = + if overflow_to_inf m s + then Farith_Big.Infinity s + else Farith_Big.Finite (s, + (Farith_Big.z_case + (fun _ -> + Farith_Big.one) + (fun p -> + p) + (fun _ -> + Farith_Big.one) + (Farith_Big.sub (Z.pow (Farith_Big.double Farith_Big.one) prec) + Farith_Big.one)), (Farith_Big.sub emax prec)) + +(** val binary_round_aux : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool -> + Farith_Big.big_int -> Farith_Big.big_int -> location -> + Farith_Big.classify **) + +let binary_round_aux prec emax mode sx mx ex lx = + let (mrs', e') = shr_fexp prec emax mx ex lx in + let (mrs'', e'') = + shr_fexp prec emax + (choice_mode mode sx mrs'.shr_m (loc_of_shr_record mrs')) e' + Coq_loc_Exact + in + (Farith_Big.z_case + (fun _ -> Farith_Big.Zero + sx) + (fun m -> + if Farith_Big.le e'' (Farith_Big.sub emax prec) + then Farith_Big.Finite (sx, m, e'') + else binary_overflow prec emax mode sx) + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + mrs''.shr_m) + +(** val coq_Bmult : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> binary_float + -> bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float **) + +let coq_Bmult prec emax mult_nan m x y = + match x with + | B754_zero sx -> + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match y with + | B754_zero sy -> B754_zero (xorb sx sy) + | B754_finite (sy, _, _) -> B754_zero (xorb sx sy) + | _ -> f (mult_nan x y)) + | B754_infinity sx -> + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match y with + | B754_infinity sy -> B754_infinity (xorb sx sy) + | B754_finite (sy, _, _) -> B754_infinity (xorb sx sy) + | _ -> f (mult_nan x y)) + | B754_nan (_, _) -> + let pl = mult_nan x y in + B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) + | B754_finite (sx, mx, ex) -> + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match y with + | B754_zero sy -> B754_zero (xorb sx sy) + | B754_infinity sy -> B754_infinity (xorb sx sy) + | B754_nan (_, _) -> f (mult_nan x y) + | B754_finite (sy, my, ey) -> + coq_FF2B prec emax + (binary_round_aux prec emax m (xorb sx sy) (Farith_Big.mult mx my) + (Farith_Big.add ex ey) Coq_loc_Exact)) + +(** val shl_align : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int **) + +let shl_align mx ex ex' = + Farith_Big.z_case + (fun _ -> (mx, + ex)) + (fun _ -> (mx, + ex)) + (fun d -> ((shift_pos d mx), + ex')) + (Farith_Big.sub ex' ex) + +(** val shl_align_fexp : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int -> Farith_Big.big_int * Farith_Big.big_int **) + +let shl_align_fexp prec emax = + let emin = + Farith_Big.sub + (Farith_Big.sub (Farith_Big.succ_double Farith_Big.one) emax) prec + in + let fexp = coq_FLT_exp emin prec in + (fun mx ex -> shl_align mx ex (fexp (Farith_Big.add (digits2_pos mx) ex))) + +(** val binary_round : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool -> + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.classify **) + +let binary_round prec emax m sx mx ex = + let (mz, ez) = shl_align_fexp prec emax mx ex in + binary_round_aux prec emax m sx mz ez Coq_loc_Exact + +(** val binary_normalize : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> + Farith_Big.big_int -> Farith_Big.big_int -> bool -> binary_float **) + +let binary_normalize prec emax mode m e szero = + Farith_Big.z_case + (fun _ -> B754_zero + szero) + (fun m0 -> + coq_FF2B prec emax (binary_round prec emax mode false m0 e)) + (fun m0 -> + coq_FF2B prec emax (binary_round prec emax mode true m0 e)) + m + +(** val coq_Bplus : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> binary_float + -> bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float **) + +let coq_Bplus prec emax plus_nan m x y = + match x with + | B754_zero sx -> + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match y with + | B754_zero sy -> + if eqb sx sy + then x + else (match m with + | Farith_Big.DN -> B754_zero true + | _ -> B754_zero false) + | B754_nan (_, _) -> f (plus_nan x y) + | _ -> y) + | B754_infinity sx -> + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match y with + | B754_infinity sy -> if eqb sx sy then x else f (plus_nan x y) + | B754_nan (_, _) -> f (plus_nan x y) + | _ -> x) + | B754_nan (_, _) -> + let pl = plus_nan x y in + B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) + | B754_finite (sx, mx, ex) -> + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match y with + | B754_zero _ -> x + | B754_infinity _ -> y + | B754_nan (_, _) -> f (plus_nan x y) + | B754_finite (sy, my, ey) -> + let ez = Farith_Big.min ex ey in + binary_normalize prec emax m + (Farith_Big.add (cond_Zopp sx (Stdlib.fst (shl_align mx ex ez))) + (cond_Zopp sy (Stdlib.fst (shl_align my ey ez)))) ez + (match m with + | Farith_Big.DN -> true + | _ -> false)) + +(** val coq_Bminus : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> binary_float + -> bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float **) + +let coq_Bminus prec emax minus_nan m x y = + coq_Bplus prec emax minus_nan m x + (coq_Bopp prec emax (fun x0 x1 -> (x0, x1)) y) + +(** val coq_Fdiv_core_binary : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int -> Farith_Big.big_int -> + (Farith_Big.big_int * Farith_Big.big_int) * location **) + +let coq_Fdiv_core_binary prec m1 e1 m2 e2 = + let d1 = coq_Zdigits2 m1 in + let d2 = coq_Zdigits2 m2 in + let e = Farith_Big.sub e1 e2 in + (Farith_Big.z_case + (fun _ -> + let (q, r) = coq_Zfast_div_eucl m1 m2 in + ((q, e), (new_location m2 r Coq_loc_Exact))) + (fun p -> + let m = Farith_Big.shiftl m1 p in + let e' = Farith_Big.add e (Farith_Big.opp p) in + let (q, r) = coq_Zfast_div_eucl m m2 in + ((q, e'), (new_location m2 r Coq_loc_Exact))) + (fun _ -> + let (q, r) = coq_Zfast_div_eucl m1 m2 in + ((q, e), (new_location m2 r Coq_loc_Exact))) + (Farith_Big.sub (Farith_Big.add d2 prec) d1)) + +(** val coq_Bdiv : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> binary_float + -> bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float **) + +let coq_Bdiv prec emax div_nan m x y = + match x with + | B754_zero sx -> + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match y with + | B754_infinity sy -> B754_zero (xorb sx sy) + | B754_finite (sy, _, _) -> B754_zero (xorb sx sy) + | _ -> f (div_nan x y)) + | B754_infinity sx -> + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match y with + | B754_zero sy -> B754_infinity (xorb sx sy) + | B754_finite (sy, _, _) -> B754_infinity (xorb sx sy) + | _ -> f (div_nan x y)) + | B754_nan (_, _) -> + let pl = div_nan x y in + B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) + | B754_finite (sx, mx, ex) -> + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match y with + | B754_zero sy -> B754_infinity (xorb sx sy) + | B754_infinity sy -> B754_zero (xorb sx sy) + | B754_nan (_, _) -> f (div_nan x y) + | B754_finite (sy, my, ey) -> + coq_FF2B prec emax + (let (p, lz) = coq_Fdiv_core_binary prec mx ex my ey in + let (mz, ez) = p in + (Farith_Big.z_case + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + (fun mz0 -> + binary_round_aux prec emax m (xorb sx sy) mz0 ez lz) + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + mz))) + +(** val coq_Fsqrt_core_binary : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + (Farith_Big.big_int * Farith_Big.big_int) * location **) + +let coq_Fsqrt_core_binary prec m e = + let d = coq_Zdigits2 m in + let s = + Farith_Big.max + (Farith_Big.sub + (Farith_Big.mult (Farith_Big.double Farith_Big.one) prec) d) + Farith_Big.zero + in + let e' = Farith_Big.sub e s in + if coq_Zeven e' + then let m' = + Farith_Big.z_case + (fun _ -> + m) + (fun p -> + Farith_Big.shiftl m p) + (fun _ -> + m) + s + in + let (q, r) = Farith_Big.Z.sqrt_rem m' in + let l = + if Farith_Big.eq r Farith_Big.zero + then Coq_loc_Exact + else Coq_loc_Inexact (if Farith_Big.le r q then Lt else Gt) + in + ((q, (Farith_Big.div2_floor e')), l) + else let s' = Farith_Big.add s Farith_Big.one in + let e'' = Farith_Big.sub e' Farith_Big.one in + let m' = + Farith_Big.z_case + (fun _ -> + m) + (fun p -> + Farith_Big.shiftl m p) + (fun _ -> + m) + s' + in + let (q, r) = Farith_Big.Z.sqrt_rem m' in + let l = + if Farith_Big.eq r Farith_Big.zero + then Coq_loc_Exact + else Coq_loc_Inexact (if Farith_Big.le r q then Lt else Gt) + in + ((q, (Farith_Big.div2_floor e'')), l) + +(** val coq_Bsqrt : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> + bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float **) + +let coq_Bsqrt prec emax sqrt_nan m x = + let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in + (match x with + | B754_zero _ -> x + | B754_infinity b -> if b then f (sqrt_nan x) else x + | B754_nan (_, _) -> f (sqrt_nan x) + | B754_finite (sx, mx, ex) -> + if sx + then f (sqrt_nan x) + else coq_FF2B prec emax + (let (p, lz) = coq_Fsqrt_core_binary prec mx ex in + let (mz, ez) = p in + (Farith_Big.z_case + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + (fun mz0 -> + binary_round_aux prec emax m false mz0 ez lz) + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + mz))) diff --git a/farith/extracted/farith_Fappli_IEEE.mli b/farith/extracted/farith_Fappli_IEEE.mli new file mode 100644 index 0000000000000000000000000000000000000000..a77cf11c2b2bee4a693bd6c0d8c4c19bc4ca7dbe --- /dev/null +++ b/farith/extracted/farith_Fappli_IEEE.mli @@ -0,0 +1,138 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinInt +open Farith_BinPos +open Farith_Bool +open Farith_Datatypes +open Farith_Fcalc_bracket +open Farith_Fcalc_round +open Farith_Fcore_FLT +open Farith_Fcore_Zaux +open Farith_Fcore_digits +open Farith_Zpower + +type nan_pl = Farith_Big.big_int + +type binary_float = +| B754_zero of bool +| B754_infinity of bool +| B754_nan of bool * nan_pl +| B754_finite of bool * Farith_Big.big_int * Farith_Big.big_int + +val coq_FF2B : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.classify -> + binary_float + +val coq_B2FF : + Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> + Farith_Big.classify + +val coq_Bopp : + Farith_Big.big_int -> Farith_Big.big_int -> (bool -> nan_pl -> + bool * nan_pl) -> binary_float -> binary_float + +val coq_Babs : + Farith_Big.big_int -> Farith_Big.big_int -> (bool -> nan_pl -> + bool * nan_pl) -> binary_float -> binary_float + +val coq_Bcompare : + Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float -> + comparison option + +type shr_record = { shr_m : Farith_Big.big_int; shr_r : bool; shr_s : bool } + +val shr_m : shr_record -> Farith_Big.big_int + +val shr_1 : shr_record -> shr_record + +val loc_of_shr_record : shr_record -> location + +val shr_record_of_loc : Farith_Big.big_int -> location -> shr_record + +val shr : + shr_record -> Farith_Big.big_int -> Farith_Big.big_int -> + shr_record * Farith_Big.big_int + +val shr_fexp : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int -> location -> shr_record * Farith_Big.big_int + +val choice_mode : + Farith_Big.mode -> bool -> Farith_Big.big_int -> location -> + Farith_Big.big_int + +val overflow_to_inf : Farith_Big.mode -> bool -> bool + +val binary_overflow : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool -> + Farith_Big.classify + +val binary_round_aux : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool -> + Farith_Big.big_int -> Farith_Big.big_int -> location -> Farith_Big.classify + +val coq_Bmult : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> binary_float + -> bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float + +val shl_align : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int + +val shl_align_fexp : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int -> Farith_Big.big_int * Farith_Big.big_int + +val binary_round : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> bool -> + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.classify + +val binary_normalize : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> + Farith_Big.big_int -> Farith_Big.big_int -> bool -> binary_float + +val coq_Bplus : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> binary_float + -> bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float + +val coq_Bminus : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> binary_float + -> bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float + +val coq_Fdiv_core_binary : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int -> Farith_Big.big_int -> + (Farith_Big.big_int * Farith_Big.big_int) * location + +val coq_Bdiv : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> binary_float + -> bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float -> + binary_float + +val coq_Fsqrt_core_binary : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + (Farith_Big.big_int * Farith_Big.big_int) * location + +val coq_Bsqrt : + Farith_Big.big_int -> Farith_Big.big_int -> (binary_float -> bool * nan_pl) + -> Farith_Big.mode -> binary_float -> binary_float diff --git a/farith/extracted/farith_Fappli_IEEE_bits.ml b/farith/extracted/farith_Fappli_IEEE_bits.ml new file mode 100644 index 0000000000000000000000000000000000000000..009e9bf27c828831de98ce75b8481f688a764d1b --- /dev/null +++ b/farith/extracted/farith_Fappli_IEEE_bits.ml @@ -0,0 +1,135 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinInt +open Farith_Fappli_IEEE + +(** val join_bits : + Farith_Big.big_int -> Farith_Big.big_int -> bool -> Farith_Big.big_int -> + Farith_Big.big_int -> Farith_Big.big_int **) + +let join_bits mw ew s m e = + Farith_Big.add + (Farith_Big.shiftl + (Farith_Big.add + (if s + then Z.pow (Farith_Big.double Farith_Big.one) ew + else Farith_Big.zero) e) mw) m + +(** val split_bits : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + (bool * Farith_Big.big_int) * Farith_Big.big_int **) + +let split_bits mw ew x = + let mm = Z.pow (Farith_Big.double Farith_Big.one) mw in + let em = Z.pow (Farith_Big.double Farith_Big.one) ew in + (((Farith_Big.le (Farith_Big.mult mm em) x), (Farith_Big.mod_floor x mm)), + (Farith_Big.mod_floor (Farith_Big.div_floor x mm) em)) + +(** val bits_of_binary_float : + Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> + Farith_Big.big_int **) + +let bits_of_binary_float mw ew = + let emax = + Z.pow (Farith_Big.double Farith_Big.one) + (Farith_Big.sub ew Farith_Big.one) + in + let prec = Farith_Big.add mw Farith_Big.one in + let emin = + Farith_Big.sub + (Farith_Big.sub (Farith_Big.succ_double Farith_Big.one) emax) prec + in + (fun x -> + match x with + | B754_zero sx -> join_bits mw ew sx Farith_Big.zero Farith_Big.zero + | B754_infinity sx -> + join_bits mw ew sx Farith_Big.zero + (Farith_Big.sub (Z.pow (Farith_Big.double Farith_Big.one) ew) + Farith_Big.one) + | B754_nan (sx, n) -> + join_bits mw ew sx n + (Farith_Big.sub (Z.pow (Farith_Big.double Farith_Big.one) ew) + Farith_Big.one) + | B754_finite (sx, mx, ex) -> + let m = Farith_Big.sub mx (Z.pow (Farith_Big.double Farith_Big.one) mw) + in + if Farith_Big.le Farith_Big.zero m + then join_bits mw ew sx m + (Farith_Big.add (Farith_Big.sub ex emin) Farith_Big.one) + else join_bits mw ew sx mx Farith_Big.zero) + +(** val binary_float_of_bits_aux : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.classify **) + +let binary_float_of_bits_aux mw ew = + let emax = + Z.pow (Farith_Big.double Farith_Big.one) + (Farith_Big.sub ew Farith_Big.one) + in + let prec = Farith_Big.add mw Farith_Big.one in + let emin = + Farith_Big.sub + (Farith_Big.sub (Farith_Big.succ_double Farith_Big.one) emax) prec + in + (fun x -> + let (p, ex) = split_bits mw ew x in + let (sx, mx) = p in + if Farith_Big.eq ex Farith_Big.zero + then (Farith_Big.z_case + (fun _ -> Farith_Big.Zero + sx) + (fun px -> Farith_Big.Finite (sx, px, + emin)) + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + mx) + else if Farith_Big.eq ex + (Farith_Big.sub (Z.pow (Farith_Big.double Farith_Big.one) ew) + Farith_Big.one) + then (Farith_Big.z_case + (fun _ -> Farith_Big.Infinity + sx) + (fun plx -> Farith_Big.NaN (sx, + plx)) + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + mx) + else (Farith_Big.z_case + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + (fun px -> Farith_Big.Finite (sx, px, + (Farith_Big.sub (Farith_Big.add ex emin) Farith_Big.one))) + (fun _ -> Farith_Big.NaN (false, + Farith_Big.one)) + (Farith_Big.add mx + (Z.pow (Farith_Big.double Farith_Big.one) mw)))) + +(** val binary_float_of_bits : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + binary_float **) + +let binary_float_of_bits mw ew x = + let emax = + Z.pow (Farith_Big.double Farith_Big.one) + (Farith_Big.sub ew Farith_Big.one) + in + let prec = Farith_Big.add mw Farith_Big.one in + coq_FF2B prec emax (binary_float_of_bits_aux mw ew x) diff --git a/farith/extracted/farith_Fappli_IEEE_bits.mli b/farith/extracted/farith_Fappli_IEEE_bits.mli new file mode 100644 index 0000000000000000000000000000000000000000..2f54c6c961e774a1c1245e0806b41722123260ba --- /dev/null +++ b/farith/extracted/farith_Fappli_IEEE_bits.mli @@ -0,0 +1,41 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinInt +open Farith_Fappli_IEEE + +val join_bits : + Farith_Big.big_int -> Farith_Big.big_int -> bool -> Farith_Big.big_int -> + Farith_Big.big_int -> Farith_Big.big_int + +val split_bits : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + (bool * Farith_Big.big_int) * Farith_Big.big_int + +val bits_of_binary_float : + Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> + Farith_Big.big_int + +val binary_float_of_bits_aux : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.classify + +val binary_float_of_bits : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + binary_float diff --git a/farith/extracted/farith_Fcalc_bracket.ml b/farith/extracted/farith_Fcalc_bracket.ml new file mode 100644 index 0000000000000000000000000000000000000000..7a22213d3b8cf8c3c58057cc357659f344081c32 --- /dev/null +++ b/farith/extracted/farith_Fcalc_bracket.ml @@ -0,0 +1,70 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_Datatypes +open Farith_Fcore_Zaux + +type location = +| Coq_loc_Exact +| Coq_loc_Inexact of comparison + +(** val new_location_even : + Farith_Big.big_int -> Farith_Big.big_int -> location -> location **) + +let new_location_even nb_steps k l = + if Farith_Big.eq k Farith_Big.zero + then (match l with + | Coq_loc_Exact -> l + | Coq_loc_Inexact _ -> Coq_loc_Inexact Lt) + else Coq_loc_Inexact + (match (Farith_Big.compare_case Eq Lt Gt) + (Farith_Big.mult (Farith_Big.double Farith_Big.one) k) + nb_steps with + | Eq -> + (match l with + | Coq_loc_Exact -> Eq + | Coq_loc_Inexact _ -> Gt) + | x -> x) + +(** val new_location_odd : + Farith_Big.big_int -> Farith_Big.big_int -> location -> location **) + +let new_location_odd nb_steps k l = + if Farith_Big.eq k Farith_Big.zero + then (match l with + | Coq_loc_Exact -> l + | Coq_loc_Inexact _ -> Coq_loc_Inexact Lt) + else Coq_loc_Inexact + (match (Farith_Big.compare_case Eq Lt Gt) + (Farith_Big.add + (Farith_Big.mult (Farith_Big.double Farith_Big.one) k) + Farith_Big.one) nb_steps with + | Eq -> + (match l with + | Coq_loc_Exact -> Lt + | Coq_loc_Inexact l0 -> l0) + | x -> x) + +(** val new_location : + Farith_Big.big_int -> Farith_Big.big_int -> location -> location **) + +let new_location nb_steps = + if coq_Zeven nb_steps + then new_location_even nb_steps + else new_location_odd nb_steps diff --git a/farith/extracted/farith_Fcalc_bracket.mli b/farith/extracted/farith_Fcalc_bracket.mli new file mode 100644 index 0000000000000000000000000000000000000000..71932c134b8983b20584bc0245b8734accc43bee --- /dev/null +++ b/farith/extracted/farith_Fcalc_bracket.mli @@ -0,0 +1,34 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_Datatypes +open Farith_Fcore_Zaux + +type location = +| Coq_loc_Exact +| Coq_loc_Inexact of comparison + +val new_location_even : + Farith_Big.big_int -> Farith_Big.big_int -> location -> location + +val new_location_odd : + Farith_Big.big_int -> Farith_Big.big_int -> location -> location + +val new_location : + Farith_Big.big_int -> Farith_Big.big_int -> location -> location diff --git a/farith/extracted/farith_Fcalc_round.ml b/farith/extracted/farith_Fcalc_round.ml new file mode 100644 index 0000000000000000000000000000000000000000..8d36dadee7ab44ab2a4f9b52e5f0aad19c47546d --- /dev/null +++ b/farith/extracted/farith_Fcalc_round.ml @@ -0,0 +1,48 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_Datatypes +open Farith_Fcalc_bracket + +(** val cond_incr : bool -> Farith_Big.big_int -> Farith_Big.big_int **) + +let cond_incr b m = + if b then Farith_Big.add m Farith_Big.one else m + +(** val round_sign_DN : bool -> location -> bool **) + +let round_sign_DN s = function +| Coq_loc_Exact -> false +| Coq_loc_Inexact _ -> s + +(** val round_sign_UP : bool -> location -> bool **) + +let round_sign_UP s = function +| Coq_loc_Exact -> false +| Coq_loc_Inexact _ -> Stdlib.not s + +(** val round_N : bool -> location -> bool **) + +let round_N p = function +| Coq_loc_Exact -> false +| Coq_loc_Inexact c -> + (match c with + | Eq -> p + | Lt -> false + | Gt -> true) diff --git a/farith/extracted/farith_Fcalc_round.mli b/farith/extracted/farith_Fcalc_round.mli new file mode 100644 index 0000000000000000000000000000000000000000..ced81c22d0335f86fc289a2621975b1e087c7944 --- /dev/null +++ b/farith/extracted/farith_Fcalc_round.mli @@ -0,0 +1,29 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_Datatypes +open Farith_Fcalc_bracket + +val cond_incr : bool -> Farith_Big.big_int -> Farith_Big.big_int + +val round_sign_DN : bool -> location -> bool + +val round_sign_UP : bool -> location -> bool + +val round_N : bool -> location -> bool diff --git a/farith/extracted/farith_Fcore_FLT.ml b/farith/extracted/farith_Fcore_FLT.ml new file mode 100644 index 0000000000000000000000000000000000000000..98258927b7b80fef789264ebadcd9870a5660d5f --- /dev/null +++ b/farith/extracted/farith_Fcore_FLT.ml @@ -0,0 +1,25 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +(** val coq_FLT_exp : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int **) + +let coq_FLT_exp emin prec e = + Farith_Big.max (Farith_Big.sub e prec) emin diff --git a/farith/extracted/farith_Fcore_FLT.mli b/farith/extracted/farith_Fcore_FLT.mli new file mode 100644 index 0000000000000000000000000000000000000000..46303759f51e6e0d4f099b94480ba1a76920ec45 --- /dev/null +++ b/farith/extracted/farith_Fcore_FLT.mli @@ -0,0 +1,22 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +val coq_FLT_exp : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int diff --git a/farith/extracted/farith_Fcore_Zaux.ml b/farith/extracted/farith_Fcore_Zaux.ml new file mode 100644 index 0000000000000000000000000000000000000000..3bec89d997a5a99eedb782d5efa1bb981f0f3e13 --- /dev/null +++ b/farith/extracted/farith_Fcore_Zaux.ml @@ -0,0 +1,143 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinInt +open Farith_Datatypes + +(** val coq_Zeven : Farith_Big.big_int -> bool **) + +let coq_Zeven n = + Farith_Big.z_case + (fun _ -> + true) + (fun p -> + Farith_Big.positive_case + (fun _ -> + false) + (fun _ -> + true) + (fun _ -> + false) + p) + (fun p -> + Farith_Big.positive_case + (fun _ -> + false) + (fun _ -> + true) + (fun _ -> + false) + p) + n + +(** val cond_Zopp : bool -> Farith_Big.big_int -> Farith_Big.big_int **) + +let cond_Zopp b m = + if b then Farith_Big.opp m else m + +(** val coq_Zpos_div_eucl_aux1 : + Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int **) + +let rec coq_Zpos_div_eucl_aux1 a b = + Farith_Big.positive_case + (fun _ -> + Z.pos_div_eucl a b) + (fun b' -> + Farith_Big.positive_case + (fun a' -> + let (q, r) = coq_Zpos_div_eucl_aux1 a' b' in + (q, + (Farith_Big.add (Farith_Big.mult (Farith_Big.double Farith_Big.one) r) + Farith_Big.one))) + (fun a' -> + let (q, r) = coq_Zpos_div_eucl_aux1 a' b' in + (q, (Farith_Big.mult (Farith_Big.double Farith_Big.one) r))) + (fun _ -> (Farith_Big.zero, + a)) + a) + (fun _ -> (a, + Farith_Big.zero)) + b + +(** val coq_Zpos_div_eucl_aux : + Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int **) + +let coq_Zpos_div_eucl_aux a b = + match (Farith_Big.compare_case Eq Lt Gt) a b with + | Eq -> (Farith_Big.one, Farith_Big.zero) + | Lt -> (Farith_Big.zero, a) + | Gt -> coq_Zpos_div_eucl_aux1 a b + +(** val coq_Zfast_div_eucl : + Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int **) + +let coq_Zfast_div_eucl a b = + Farith_Big.z_case + (fun _ -> (Farith_Big.zero, + Farith_Big.zero)) + (fun a' -> + Farith_Big.z_case + (fun _ -> (Farith_Big.zero, + Farith_Big.zero)) + (fun b' -> + coq_Zpos_div_eucl_aux a' b') + (fun b' -> + let (q, r) = coq_Zpos_div_eucl_aux a' b' in + (Farith_Big.z_case + (fun _ -> ((Farith_Big.opp q), + Farith_Big.zero)) + (fun _ -> ((Farith_Big.opp (Farith_Big.add q Farith_Big.one)), + (Farith_Big.add b r))) + (fun _ -> ((Farith_Big.opp (Farith_Big.add q Farith_Big.one)), + (Farith_Big.add b r))) + r)) + b) + (fun a' -> + Farith_Big.z_case + (fun _ -> (Farith_Big.zero, + Farith_Big.zero)) + (fun b' -> + let (q, r) = coq_Zpos_div_eucl_aux a' b' in + (Farith_Big.z_case + (fun _ -> ((Farith_Big.opp q), + Farith_Big.zero)) + (fun _ -> ((Farith_Big.opp (Farith_Big.add q Farith_Big.one)), + (Farith_Big.sub b r))) + (fun _ -> ((Farith_Big.opp (Farith_Big.add q Farith_Big.one)), + (Farith_Big.sub b r))) + r)) + (fun b' -> + let (q, r) = coq_Zpos_div_eucl_aux a' b' in (q, (Farith_Big.opp r))) + b) + a + +(** val iter_pos : ('a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1 **) + +let rec iter_pos f n x = + Farith_Big.positive_case + (fun n' -> + iter_pos f n' (iter_pos f n' (f x))) + (fun n' -> + iter_pos f n' (iter_pos f n' x)) + (fun _ -> + f x) + n diff --git a/farith/extracted/farith_Fcore_Zaux.mli b/farith/extracted/farith_Fcore_Zaux.mli new file mode 100644 index 0000000000000000000000000000000000000000..19b3e876114a774583a0b72c860941813c9f1119 --- /dev/null +++ b/farith/extracted/farith_Fcore_Zaux.mli @@ -0,0 +1,39 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinInt +open Farith_Datatypes + +val coq_Zeven : Farith_Big.big_int -> bool + +val cond_Zopp : bool -> Farith_Big.big_int -> Farith_Big.big_int + +val coq_Zpos_div_eucl_aux1 : + Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int + +val coq_Zpos_div_eucl_aux : + Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int + +val coq_Zfast_div_eucl : + Farith_Big.big_int -> Farith_Big.big_int -> + Farith_Big.big_int * Farith_Big.big_int + +val iter_pos : ('a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1 diff --git a/farith/extracted/farith_Fcore_digits.ml b/farith/extracted/farith_Fcore_digits.ml new file mode 100644 index 0000000000000000000000000000000000000000..b109d4c3bdcf350c854742d4d18876e57cdbfb59 --- /dev/null +++ b/farith/extracted/farith_Fcore_digits.ml @@ -0,0 +1,42 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +(** val digits2_pos : Farith_Big.big_int -> Farith_Big.big_int **) + +let rec digits2_pos n = + Farith_Big.positive_case + (fun p -> + Farith_Big.succ (digits2_pos p)) + (fun p -> + Farith_Big.succ (digits2_pos p)) + (fun _ -> + Farith_Big.one) + n + +(** val coq_Zdigits2 : Farith_Big.big_int -> Farith_Big.big_int **) + +let coq_Zdigits2 n = + Farith_Big.z_case + (fun _ -> + n) + (fun p -> + (digits2_pos p)) + (fun p -> + (digits2_pos p)) + n diff --git a/farith/extracted/farith_Fcore_digits.mli b/farith/extracted/farith_Fcore_digits.mli new file mode 100644 index 0000000000000000000000000000000000000000..d7a5d5533fee3bb9c3c13013c6961ad48d7e9e1a --- /dev/null +++ b/farith/extracted/farith_Fcore_digits.mli @@ -0,0 +1,22 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +val digits2_pos : Farith_Big.big_int -> Farith_Big.big_int + +val coq_Zdigits2 : Farith_Big.big_int -> Farith_Big.big_int diff --git a/farith/extracted/farith_Flocq_version.ml b/farith/extracted/farith_Flocq_version.ml new file mode 100644 index 0000000000000000000000000000000000000000..87d0558b9122ccfe7ca27288024b4f3b51d19071 --- /dev/null +++ b/farith/extracted/farith_Flocq_version.ml @@ -0,0 +1,27 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +(** val coq_Flocq_version : Farith_Big.big_int **) + +let coq_Flocq_version = + (Farith_Big.double (Farith_Big.succ_double (Farith_Big.succ_double + (Farith_Big.double (Farith_Big.succ_double (Farith_Big.double + (Farith_Big.double (Farith_Big.double (Farith_Big.double + (Farith_Big.double (Farith_Big.double (Farith_Big.double + (Farith_Big.succ_double (Farith_Big.double Farith_Big.one)))))))))))))) diff --git a/farith/extracted/farith_Flocq_version.mli b/farith/extracted/farith_Flocq_version.mli new file mode 100644 index 0000000000000000000000000000000000000000..6df42bb46b5f543472089eb5c541ca703595a53d --- /dev/null +++ b/farith/extracted/farith_Flocq_version.mli @@ -0,0 +1,20 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +val coq_Flocq_version : Farith_Big.big_int diff --git a/farith/extracted/farith_Specif.ml b/farith/extracted/farith_Specif.ml new file mode 100644 index 0000000000000000000000000000000000000000..9566937cf1ec0495cd5f16ff2442f496b9b99fdd --- /dev/null +++ b/farith/extracted/farith_Specif.ml @@ -0,0 +1,22 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +type 'a coq_sig = + 'a + (* singleton inductive, whose constructor was exist *) diff --git a/farith/extracted/farith_Specif.mli b/farith/extracted/farith_Specif.mli new file mode 100644 index 0000000000000000000000000000000000000000..9566937cf1ec0495cd5f16ff2442f496b9b99fdd --- /dev/null +++ b/farith/extracted/farith_Specif.mli @@ -0,0 +1,22 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +type 'a coq_sig = + 'a + (* singleton inductive, whose constructor was exist *) diff --git a/farith/extracted/farith_Zpower.ml b/farith/extracted/farith_Zpower.ml new file mode 100644 index 0000000000000000000000000000000000000000..5bb7f690bdc6e91fca52e4ed3951b1d5b481abc7 --- /dev/null +++ b/farith/extracted/farith_Zpower.ml @@ -0,0 +1,26 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinPos + +(** val shift_pos : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **) + +let shift_pos n z = + Pos.iter (fun x -> Farith_Big.double x) z n diff --git a/farith/extracted/farith_Zpower.mli b/farith/extracted/farith_Zpower.mli new file mode 100644 index 0000000000000000000000000000000000000000..a16c84bb8acfbe3c99e0882dfd1994e09256e62b --- /dev/null +++ b/farith/extracted/farith_Zpower.mli @@ -0,0 +1,23 @@ +(**************************************************************************) +(* This file is part of the extraction of the Flocq formalization of *) +(* floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ *) +(* *) +(* Copyright (C) 2010-2013 Sylvie Boldo *) +(* *) +(* Copyright (C) 2010-2013 Guillaume Melquiond *) +(* *) +(* This library is free software; 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; either *) +(* version 3 of the License, or (at your option) any later version. *) +(* *) +(* This library 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 *) +(* COPYING file for more details. *) +(**************************************************************************) + +open Farith_BinPos + +val shift_pos : + Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int diff --git a/farith/farith.ml b/farith/farith.ml new file mode 100644 index 0000000000000000000000000000000000000000..bb7f79f54ce865f0ec03cae1cd675504c4db8b97 --- /dev/null +++ b/farith/farith.ml @@ -0,0 +1,190 @@ +(**************************************************************************) +(* 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). *) +(* *) +(**************************************************************************) + + +type mode = Farith_Big.mode = + | NE + | ZR + | DN + | UP + | NA + +type classify = Farith_Big.classify = + | Zero of bool + | Infinity of bool + | NaN of bool * Z.t + | Finite of bool * Z.t * Z.t + +module Common = struct + open Format + open Farith_Fappli_IEEE + + let pp_sign fmt b = pp_print_string fmt (if b then "-" else "+") + let pp fmt = function + | B754_zero b -> fprintf fmt "%a0" pp_sign b + | B754_infinity b -> fprintf fmt "%a∞" pp_sign b + | B754_nan (b,pl) -> fprintf fmt "%aNAN(%a)" pp_sign b Z.pp_print pl + | B754_finite (b,m,e) -> + let rec oddify a p = + if 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 + fprintf fmt "%a%ap%a" pp_sign b Z.pp_print m Z.pp_print e + + (** lexer for finite float *) + let lex_float s = + try + let k = String.index s 'p' in + let m = String.sub s 0 k in + let e = String.sub s (succ k) (String.length s - k - 1) in + (Z.of_string m), (Z.of_string e) + with Not_found -> + (Z.of_string s), Z.zero +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 = Farith_Flocq_version.coq_Flocq_version diff --git a/farith/farith.mli b/farith/farith.mli new file mode 100644 index 0000000000000000000000000000000000000000..1e5bdd1ea09190c0b6f62620bf4c524c0e4354a6 --- /dev/null +++ b/farith/farith.mli @@ -0,0 +1,294 @@ +(**************************************************************************) +(* 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 *) + +(** Type used for classifying floating points *) +type classify = + | Zero of bool + | Infinity of bool + | NaN of bool * Z.t + | Finite of bool * Z.t * Z.t + +(** {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/farith/farith.mltop b/farith/farith.mltop new file mode 100644 index 0000000000000000000000000000000000000000..9271ca98797d1ed2ad3c6aa727aeb0180be1b254 --- /dev/null +++ b/farith/farith.mltop @@ -0,0 +1,20 @@ +F +Farith +Farith_BinInt +Farith_BinNat +Farith_BinPosDef +Farith_BinPos +Farith_Bool +Farith_Datatypes +Farith_Fappli_IEEE_bits +Farith_Fappli_IEEE +Farith_F_aux +Farith_Fcalc_bracket +Farith_Fcalc_round +Farith_Fcore_digits +Farith_Fcore_FLT +Farith_Fcore_Zaux +Farith_Flocq_version +Farith_Specif +Farith_Big +Farith_top diff --git a/farith/farith.opam b/farith/farith.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/farith/farith_Big.ml b/farith/farith_Big.ml new file mode 100644 index 0000000000000000000000000000000000000000..8ed2ad80c7f2fe17020e800bee1fabd883aae142 --- /dev/null +++ b/farith/farith_Big.ml @@ -0,0 +1,238 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** [Big] : a wrapper around ocaml [Big_int] with nicer names, + and a few extraction-specific constructions *) + +(** To be linked with [nums.(cma|cmxa)] *) + +open Big_int_Z + +type big_int = Big_int_Z.big_int +(* The type of big integers. *) +let zero = zero_big_int +(* The big integer [0]. *) +let one = unit_big_int +(* The big integer [1]. *) +let two = big_int_of_int 2 +(* The big integer [2]. *) + +(* {6 Arithmetic operations} *) + +let opp = minus_big_int +(* Unary negation. *) +let abs = abs_big_int +(* Absolute value. *) +let add = add_big_int +(* Addition. *) +let succ = succ_big_int +(* Successor (add 1). *) +let add_int = add_int_big_int +(* Addition of a small integer to a big integer. *) +let sub = sub_big_int +(* Subtraction. *) +let pred = pred_big_int +(* Predecessor (subtract 1). *) +let mult = mult_big_int +(* Multiplication of two big integers. *) +let mult_int = mult_int_big_int +(* Multiplication of a big integer by a small integer *) +let _square = square_big_int +(* Return the square of the given big integer *) +let sqrt = sqrt_big_int +(* [sqrt_big_int a] returns the integer square root of [a], + that is, the largest big integer [r] such that [r * r <= a]. + Raise [Invalid_argument] if [a] is negative. *) +let quomod = quomod_big_int +(* Euclidean division of two big integers. + The first part of the result is the quotient, + the second part is the remainder. + Writing [(q,r) = quomod_big_int a b], we have + [a = q * b + r] and [0 <= r < |b|]. + Raise [Division_by_zero] if the divisor is zero. *) +let div = div_big_int +(* Euclidean quotient of two big integers. + This is the first result [q] of [quomod_big_int] (see above). *) +let modulo = mod_big_int +(* Euclidean modulus of two big integers. + This is the second result [r] of [quomod_big_int] (see above). *) +let gcd = gcd_big_int +(* Greatest common divisor of two big integers. *) +let power = power_big_int_positive_big_int +(* Exponentiation functions. Return the big integer + representing the first argument [a] raised to the power [b] + (the second argument). Depending + on the function, [a] and [b] can be either small integers + or big integers. Raise [Invalid_argument] if [b] is negative. *) + +(* {6 Comparisons and tests} *) + +let sign = sign_big_int +(* Return [0] if the given big integer is zero, + [1] if it is positive, and [-1] if it is negative. *) +let compare = compare_big_int +(* [compare_big_int a b] returns [0] if [a] and [b] are equal, + [1] if [a] is greater than [b], and [-1] if [a] is smaller + than [b]. *) +let eq = eq_big_int +let le = le_big_int +let ge = ge_big_int +let lt = lt_big_int +let gt = gt_big_int +(* Usual boolean comparisons between two big integers. *) +let max = max_big_int +(* Return the greater of its two arguments. *) +let min = min_big_int +(* Return the smaller of its two arguments. *) +(* {6 Conversions to and from strings} *) + +let to_string = string_of_big_int +(* Return the string representation of the given big integer, + in decimal (base 10). *) +let of_string = big_int_of_string +(* Convert a string to a big integer, in decimal. + The string consists of an optional [-] or [+] sign, + followed by one or several decimal digits. *) + +(* {6 Conversions to and from other numerical types} *) + +let of_int = big_int_of_int +(* Convert a small integer to a big integer. *) +let is_int = is_int_big_int +(* Test whether the given big integer is small enough to + be representable as a small integer (type [int]) + without loss of precision. On a 32-bit platform, + [is_int_big_int a] returns [true] if and only if + [a] is between 2{^30} and 2{^30}-1. On a 64-bit platform, + [is_int_big_int a] returns [true] if and only if + [a] is between -2{^62} and 2{^62}-1. *) +let to_int = int_of_big_int +(* Convert a big integer to a small integer (type [int]). + Raises [Failure "int_of_big_int"] if the big integer + is not representable as a small integer. *) + +(* Functions used by extraction *) + +let double n = (Z.shift_left n 1) +let succ_double n = Z.succ (Z.shift_left n 1) +let pred_double n = Z.pred (Z.shift_left n 1) + +let nat_case fO fS n = if sign n <= 0 then fO () else fS (pred n) + +let positive_case f2p1 f2p f1 p = + if le p one then f1 () else + let (q,r) = quomod p two in if eq r zero then f2p q else f2p1 q + +let n_case fO fp n = if sign n <= 0 then fO () else fp n + +let z_case fO fp fn z = + let s = sign z in + if s = 0 then fO () else if s > 0 then fp z else fn (opp z) + +let sgn z = Z.of_int (Z.sign z) + +let compare_case e l g x y = + let s = compare x y in if s = 0 then e else if s<0 then l else g + +let nat_rec fO fS = + let rec loop acc n = + if sign n <= 0 then acc else loop (fS acc) (pred n) + in loop fO + +let positive_rec f2p1 f2p f1 = + let rec loop n = + if le n one then f1 + else + let (q,r) = quomod n two in + if eq r zero then f2p (loop q) else f2p1 (loop q) + in loop + +let z_rec fO fp fn = z_case (fun _ -> fO) fp fn + +let rec nat_rect acc f n = + if sign n <= 0 then acc else nat_rect (f () acc) f (pred n) + +let rec iter_nat f n acc = + if sign n <= 0 then acc else iter_nat f (pred n) (f acc) + +external identity: 'a -> 'a = "%identity" + +let shiftl_pos a p = Z.shift_left a (Z.to_int p) + +let modulo_pos a b = + assert (sign a >= 0); + assert (sign b >= 0); + modulo a b + +let div_pos a b = + assert (sign a >= 0); + assert (sign b > 0); + div a b + +let square a = Z.mul a a + +let pow_pos a p = + Z.pow a (Z.to_int p) + +let div2_trunc n = Z.shift_right_trunc n 1 + +let div_floor = Z.fdiv +let div2_floor n = Z.shift_right n 1 +let mod_floor a b = + let r = Z.rem a b in + if (Stdlib.(lxor) (Z.sign a) (Z.sign b) >= 0) || Z.equal r Z.zero + then r + else Z.add b r + +let div_mod_floor a b = + let p,r as pr = Z.div_rem a b in + if ((Stdlib.(lxor) (Z.sign a) (Z.sign b)) >= 0) || Z.equal r Z.zero + then pr + else Z.pred p, Z.add b r + +let pos_div_eucl a b = + assert (sign a >= 0); + assert (sign b > 0); + Z.div_rem a b + +let shiftl a n = + let n = Z.to_int n in + if n < 0 then Z.shift_right a (-n) + else Z.shift_left a n + +let shiftr a n = + let n = Z.to_int n in + if n < 0 then Z.shift_left a (-n) + else Z.shift_right a n + +let ldiff a b = Z.logand a (Z.lognot b) + +module Z = Z (* zarith *) + + +(* Q *) +(* must be already normalize *) +let q_mk (den,num) = {Q.den; Q.num} +let q_case f q = f q.Q.den q.Q.num +let q_den q = q.Q.den +let q_num q = q.Q.num + +type mode = + | NE + | ZR + | DN + | UP + | NA + +type classify = + | Zero of bool + | Infinity of bool + | NaN of bool * Z.t + | Finite of bool * Z.t * Z.t + +let combine_hash acc n = n * 65599 + acc diff --git a/farith/farith_top.ml b/farith/farith_top.ml new file mode 100644 index 0000000000000000000000000000000000000000..7ad8a6a591c4ffb63a918d289a000dc55a94dfbe --- /dev/null +++ b/farith/farith_top.ml @@ -0,0 +1,17 @@ +open F +open Farith + +let resolve_path s = Filename.concat (Filename.dirname Sys.executable_name) s + +let () = + Topdirs.dir_directory (resolve_path "_build/"); + Topdirs.dir_directory (resolve_path "_build/extracted/"); + Topdirs.dir_install_printer Format.err_formatter + Longident.(Ldot(Ldot(Lident "Farith","B64"),"pp")); + Topdirs.dir_install_printer Format.err_formatter + Longident.(Ldot(Ldot(Lident "Farith","B32"),"pp")); + Topdirs.dir_install_printer Format.err_formatter + Longident.(Ldot(Lident "F","pp")) + + +let () = UTop_main.main () diff --git a/farith/headers/CEA_LGPL b/farith/headers/CEA_LGPL new file mode 100644 index 0000000000000000000000000000000000000000..4e1e488260b54d71fc5a38816b5c286ebaca8e7a --- /dev/null +++ b/farith/headers/CEA_LGPL @@ -0,0 +1,18 @@ +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). + diff --git a/farith/headers/FLOCQ b/farith/headers/FLOCQ new file mode 100644 index 0000000000000000000000000000000000000000..206e9cc7288afd65eeba00e935dc72f85ea0cbfa --- /dev/null +++ b/farith/headers/FLOCQ @@ -0,0 +1,16 @@ +This file is part of the extraction of the Flocq formalization of +floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ + +Copyright (C) 2010-2013 Sylvie Boldo + +Copyright (C) 2010-2013 Guillaume Melquiond + +This library is free software; 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; either +version 3 of the License, or (at your option) any later version. + +This library 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 +COPYING file for more details. diff --git a/farith/headers/header.config b/farith/headers/header.config new file mode 100644 index 0000000000000000000000000000000000000000..5a3b16f2c28e42538e70b5189a8fe106b2cfd6b0 --- /dev/null +++ b/farith/headers/header.config @@ -0,0 +1,16 @@ +################## +# Objective Caml # +################## +| ".*\.mly" -> frame open:"/*" line:"*" close:"*/" +| ".*\.ml[il4]?.*" -> frame open:"(*" line:"*" close:"*)" + +############ +# Makefile # +############ +| ".*Make.*" -> frame open:"#" line:"#" close:"#" + +################## +# Coq # +################## +| ".*\.v" -> frame open:"(*" line:"*" close:"*)" + diff --git a/farith/opam b/farith/opam new file mode 100644 index 0000000000000000000000000000000000000000..82dd924aec4d54202b70e53c6e99fa993e99c2a1 --- /dev/null +++ b/farith/opam @@ -0,0 +1,27 @@ +opam-version: "2.0" +name: "farith" +synopsis: "Formally proven floating point library" +version: "1.0" +maintainer: "francois.bobot@cea.fr" +authors: [ + "François Bobot" + "Sylvie Boldo" + "Loïc Correnson" + "Guillaume Melquiond" +] +license: "GNU Lesser General Public License version 2.1" +homepage: "https://git.frama-c.com/soprano/farith" +bug-reports: "https://git.frama-c.com/soprano/farith/issues" +tags: [ + "floating point" + "formally proved" +] + +build: [[make]] +install: [[make "install"]] +remove: [[make "uninstall"]] + +depends: [ + "ocamlfind" + "zarith" +] diff --git a/farith/tests/Makefile b/farith/tests/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..5253f9a2684ac304f91214e537c34f1b3ef47e0e --- /dev/null +++ b/farith/tests/Makefile @@ -0,0 +1,57 @@ +SOURCES=$(shell ls *.ml) +LOCAL=$(shell pwd)/_local + +.PHONY: all update show compile status clean diff logs + +all: + @$(MAKE) compile + @$(MAKE) update + @$(MAKE) status + +update: + @echo "------------------------------------------------------------" + @echo "Updating Tests" + @$(MAKE) diff + +show: + @echo "------------------------------------------------------------" + @echo "Comparing Tests" + @find . -name "*.diff" -not -size 0 -exec echo "[FAILED] {}" \; \ + -exec cat {} \; + @echo "------------------------------------------------------------" + +compile: + @echo "------------------------------------------------------------" + @echo "Compiling Tests" + @echo "Local = '$(LOCAL)'" + @ OCAMLPATH=$(LOCAL):$$OCAMLPATH \ + OCAMLFIND_IGNORE_DUPS_IN=$(shell ocamlfind printconf path) \ + ocamlbuild -use-ocamlfind -pkg farith -no-links ${SOURCES:.ml=.native} + +status: + @echo "------------------------------------------------------------" + @echo "Comparing Tests" + @find . -name "*.diff" -not -size 0 -exec echo "[FAILED] {}" \; + @echo "------------------------------------------------------------" + +diff: ${SOURCES:.ml=.diff} +logs: ${SOURCES:.ml=.log} + +clean: + ocamlbuild -clean + rm -f *.log *.diff + +.PRECIOUS: %.log %.oracle + +%.log: _build/%.native %.oracle + @echo "Running $(<F)" + @$< >$@ + +%.diff: %.log %.oracle + @diff $+ > $@ || (echo "Failed $+" ; cat $@) + +%.oracle: + @touch $@ + +%.meld: %.log %.oracle + @meld $+ diff --git a/farith/tests/_tags b/farith/tests/_tags new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/farith/tests/issue_005.ml b/farith/tests/issue_005.ml new file mode 100644 index 0000000000000000000000000000000000000000..2c7f66d49a54f2da70687c67a3046fdf0b17a7db --- /dev/null +++ b/farith/tests/issue_005.ml @@ -0,0 +1,17 @@ +open Format + +module G = Farith.B64 + +let f_convert r = + let fp = F.of_float r in + printf "[F] %f : %a@." r F.pp fp ; fp + +let g_convert r = + let fp = G.of_float r in + printf "[G] %f : %a@." r G.pp fp ; fp + +let () = + begin + ignore (g_convert 0.1) ; + ignore (f_convert 0.1) ; + end diff --git a/farith/tests/issue_005.oracle b/farith/tests/issue_005.oracle new file mode 100644 index 0000000000000000000000000000000000000000..393a46758c0ca198d90b6187106650bf7aff6383 --- /dev/null +++ b/farith/tests/issue_005.oracle @@ -0,0 +1,2 @@ +[G] 0.100000 : +3602879701896397p-55 +[F] 0.100000 : +3602879701896397p-55 diff --git a/farith/tests/mode.ml b/farith/tests/mode.ml new file mode 100644 index 0000000000000000000000000000000000000000..9d394fe10b32e007da3623707448617bc6b27663 --- /dev/null +++ b/farith/tests/mode.ml @@ -0,0 +1,47 @@ + +module G = Farith.B64 + +let gpp mode fmt q = G.pp fmt (G.of_q mode q) +let fpp mode fmt q = F.pp fmt (F.of_qint ~mode ~bits:F.b64 q) + +let () = + begin + Format.printf "[G] 3.1 = %a@." G.pp (G.of_float 3.1) ; + Format.printf "[F] 3.1 = %a@." F.pp (F.of_float 3.1) ; + let q = Q.make (Z.of_int 31) (Z.of_int 10) in + Format.printf "[Fp] 3.1 = %a@." F.pp (F.round ~mode:F.ZR ~bits:25 (F.of_float 3.1)) ; + Format.printf "[Fq] 3.1 = %a@." F.pp (F.of_qint ~mode:F.ZR ~bits:25 q) ; + Format.printf "-----------------------@." ; + Format.printf " Simple Roundings@." ; + let job m m1 m2 q = + begin + Format.printf "-----------------------@." ; + Format.printf "Q=%a@." Q.pp_print q ; + Format.printf "[G-%s] %a@." m (gpp m1) q ; + Format.printf "[F-%s] %a@." m (fpp m2) q ; + Format.printf "[G-%s] %a@." m (gpp m1) (Q.neg q) ; + Format.printf "[F-%s] %a@." m (fpp m2) (Q.neg q) ; + end in + job "NE" Farith.NE F.NE q ; + job "NA" Farith.NA F.NA q ; + job "ZR" Farith.ZR F.ZR q ; + job "UP" Farith.UP F.UP q ; + job "DN" Farith.DN F.DN q ; + Format.printf "-----------------------@." ; + Format.printf " Tie Breaks (NE)@." ; + let eps = Z.shift_left Z.one 51 in + let e_ex = Q.make (Z.of_int 0b100) eps in + let e_lo = Q.make (Z.of_int 0b101) eps in + let e_ti = Q.make (Z.of_int 0b110) eps in + let e_up = Q.make (Z.of_int 0b111) eps in + job "NE-ex" Farith.NE F.NE (Q.add Q.one e_ex) ; + job "NE-lo" Farith.NE F.NE (Q.add Q.one e_lo) ; + job "NE-ti" Farith.NE F.NE (Q.add Q.one e_ti) ; + job "NE-up" Farith.NE F.NE (Q.add Q.one e_up) ; + Format.printf "-----------------------@." ; + Format.printf " Tie Breaks (NA)@." ; + job "NA-ex" Farith.NA F.NA (Q.add Q.one e_ex) ; + job "NA-lo" Farith.NA F.NA (Q.add Q.one e_lo) ; + job "NA-ti" Farith.NA F.NA (Q.add Q.one e_ti) ; + job "NA-up" Farith.NA F.NA (Q.add Q.one e_up) ; + end diff --git a/farith/tests/mode.oracle b/farith/tests/mode.oracle new file mode 100644 index 0000000000000000000000000000000000000000..6e11103a880a8d3add7e1536b3923bbc4cb96487 --- /dev/null +++ b/farith/tests/mode.oracle @@ -0,0 +1,88 @@ +[G] 3.1 = +6980579422424269p-51 +[F] 3.1 = +6980579422424269p-51 +[Fp] 3.1 = +6501171p-21 +[Fq] 3.1 = +6501171p-21 +----------------------- + Simple Roundings +----------------------- +Q=31/10 +[G-NE] +6980579422424269p-51 +[F-NE] +6980579422424269p-51 +[G-NE] -6980579422424269p-51 +[F-NE] -6980579422424269p-51 +----------------------- +Q=31/10 +[G-NA] +6980579422424269p-51 +[F-NA] +6980579422424269p-51 +[G-NA] -6980579422424269p-51 +[F-NA] -6980579422424269p-51 +----------------------- +Q=31/10 +[G-ZR] +1745144855606067p-49 +[F-ZR] +1745144855606067p-49 +[G-ZR] -1745144855606067p-49 +[F-ZR] -1745144855606067p-49 +----------------------- +Q=31/10 +[G-UP] +6980579422424269p-51 +[F-UP] +6980579422424269p-51 +[G-UP] -1745144855606067p-49 +[F-UP] -1745144855606067p-49 +----------------------- +Q=31/10 +[G-DN] +1745144855606067p-49 +[F-DN] +1745144855606067p-49 +[G-DN] -6980579422424269p-51 +[F-DN] -6980579422424269p-51 +----------------------- + Tie Breaks (NE) +----------------------- +Q=562949953421313/562949953421312 +[G-NE-ex] +562949953421313p-49 +[F-NE-ex] +562949953421313p-49 +[G-NE-ex] -562949953421313p-49 +[F-NE-ex] -562949953421313p-49 +----------------------- +Q=2251799813685253/2251799813685248 +[G-NE-lo] +2251799813685253p-51 +[F-NE-lo] +2251799813685253p-51 +[G-NE-lo] -2251799813685253p-51 +[F-NE-lo] -2251799813685253p-51 +----------------------- +Q=1125899906842627/1125899906842624 +[G-NE-ti] +1125899906842627p-50 +[F-NE-ti] +1125899906842627p-50 +[G-NE-ti] -1125899906842627p-50 +[F-NE-ti] -1125899906842627p-50 +----------------------- +Q=2251799813685255/2251799813685248 +[G-NE-up] +2251799813685255p-51 +[F-NE-up] +2251799813685255p-51 +[G-NE-up] -2251799813685255p-51 +[F-NE-up] -2251799813685255p-51 +----------------------- + Tie Breaks (NA) +----------------------- +Q=562949953421313/562949953421312 +[G-NA-ex] +562949953421313p-49 +[F-NA-ex] +562949953421313p-49 +[G-NA-ex] -562949953421313p-49 +[F-NA-ex] -562949953421313p-49 +----------------------- +Q=2251799813685253/2251799813685248 +[G-NA-lo] +2251799813685253p-51 +[F-NA-lo] +2251799813685253p-51 +[G-NA-lo] -2251799813685253p-51 +[F-NA-lo] -2251799813685253p-51 +----------------------- +Q=1125899906842627/1125899906842624 +[G-NA-ti] +1125899906842627p-50 +[F-NA-ti] +1125899906842627p-50 +[G-NA-ti] -1125899906842627p-50 +[F-NA-ti] -1125899906842627p-50 +----------------------- +Q=2251799813685255/2251799813685248 +[G-NA-up] +2251799813685255p-51 +[F-NA-up] +2251799813685255p-51 +[G-NA-up] -2251799813685255p-51 +[F-NA-up] -2251799813685255p-51 diff --git a/farith/tests/subnormal.ml b/farith/tests/subnormal.ml new file mode 100644 index 0000000000000000000000000000000000000000..8a3e2f60b1e024c2faf9e627de65a8893a3fbf0e --- /dev/null +++ b/farith/tests/subnormal.ml @@ -0,0 +1,41 @@ + +let eps n = Stdlib.ldexp 1.0 n + +let pp_class fmt u = + Format.pp_print_string fmt + begin + match classify_float u with + | FP_zero -> "zero" + | FP_normal -> "normal" + | FP_subnormal -> "sub-normal" + | FP_infinite -> "infinity" + | FP_nan -> "nan" + end + +let test_of_float n = + let u = eps n in + try + let f = F.of_float u in + Format.printf "of-float 1p%d = %a (%a)@." n F.pp f pp_class u + with F.Undefined -> + Format.printf "of-float 1p%d = undefined (%a)@." n pp_class u + +let test_to_float n = + begin + let u = eps n in + let f = F.power2 n in + let v = F.to_float f in + Format.printf "to-float %a = %f (%a)@." F.pp f v pp_class v ; + let fu,eu = Stdlib.frexp u in + let fv,ev = Stdlib.frexp v in + Format.printf " expected = %fp%d@\n" fu eu ; + Format.printf " obtained = %fp%d@." fv ev ; + end + +let limits = [ 1023;1024;-1022;-1023;-1048;-1074;-1075 ] + +let () = + begin + List.iter test_of_float limits ; + List.iter test_to_float limits ; + end diff --git a/farith/tests/subnormal.oracle b/farith/tests/subnormal.oracle new file mode 100644 index 0000000000000000000000000000000000000000..8936ea17c69f3bf58d0a5636aab6bf768cf50f77 --- /dev/null +++ b/farith/tests/subnormal.oracle @@ -0,0 +1,28 @@ +of-float 1p1023 = +1p1023 (normal) +of-float 1p1024 = undefined (infinity) +of-float 1p-1022 = +1p-1022 (normal) +of-float 1p-1023 = +1p-1023 (sub-normal) +of-float 1p-1048 = +1p-1048 (sub-normal) +of-float 1p-1074 = +1p-1074 (sub-normal) +of-float 1p-1075 = 0 (zero) +to-float +1p1023 = 89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608.000000 (normal) + expected = 0.500000p1024 + obtained = 0.500000p1024 +to-float +1p1024 = inf (infinity) + expected = infp0 + obtained = infp0 +to-float +1p-1022 = 0.000000 (normal) + expected = 0.500000p-1021 + obtained = 0.500000p-1021 +to-float +1p-1023 = 0.000000 (sub-normal) + expected = 0.500000p-1022 + obtained = 0.500000p-1022 +to-float +1p-1048 = 0.000000 (sub-normal) + expected = 0.500000p-1047 + obtained = 0.500000p-1047 +to-float +1p-1074 = 0.000000 (sub-normal) + expected = 0.500000p-1073 + obtained = 0.500000p-1073 +to-float +1p-1075 = 0.000000 (zero) + expected = 0.000000p0 + obtained = 0.000000p0 diff --git a/farith/tests/test.ml b/farith/tests/test.ml new file mode 100644 index 0000000000000000000000000000000000000000..1d2a73629d5694844160d7304e392447be9d7d8d --- /dev/null +++ b/farith/tests/test.ml @@ -0,0 +1,46 @@ +open Format + +let () = + printf "Flocq version: %a@." + Z.pp_print Farith.flocq_version + +module type Tested = sig + val name: string + type t + val of_float : float -> t + val to_float : t -> float + val add : t -> t -> t + val pp : Format.formatter -> t -> unit +end + +module Run(T:Tested) = struct + let () = + printf "@[<3>Run tests with %s@\n" T.name; + let add u v = + let fu = T.of_float u in + let fv = T.of_float v in + let fr = T.add fu fv in + let r = T.to_float fr in + printf "%f + %f = %f@\n" u v r; + printf "%f : %a@\n" u T.pp fu; + printf "%f : %a@\n" v T.pp fv; + printf "%f : %a@]@\n" r T.pp fr; + in + add (0.1) (2.0); + add (-.0.1) (2.0); + add (-.0.1) (-.2.0); + add (0.1) (-.2.0) +end + +module E1 = Run(struct + let name = "Farith" + include Farith.B64 + let add = Farith.B64.add Farith.ZR + end) +module E2 = Run(struct + let name = "F" + include F + let to_float = to_float ~mode:F.NE + let add x y = F.round_f64 ~mode:F.ZR (F.add x y) + let pp = F.pretty + end) diff --git a/farith/tests/test.oracle b/farith/tests/test.oracle new file mode 100644 index 0000000000000000000000000000000000000000..ec622360444871319aa9cacb4932f07f3c7d769c --- /dev/null +++ b/farith/tests/test.oracle @@ -0,0 +1,35 @@ +Flocq version: 20400 +Run tests with Farith + 0.100000 + 2.000000 = 2.100000 + 0.100000 : +3602879701896397p-55 + 2.000000 : +1p1 + 2.100000 : +1182194902184755p-49 +-0.100000 + 2.000000 = 1.900000 +-0.100000 : -3602879701896397p-55 +2.000000 : +1p1 +1.900000 : +4278419646001971p-51 +-0.100000 + -2.000000 = -2.100000 +-0.100000 : -3602879701896397p-55 +-2.000000 : -1p1 +-2.100000 : -1182194902184755p-49 +0.100000 + -2.000000 = -1.900000 +0.100000 : +3602879701896397p-55 +-2.000000 : -1p1 +-1.900000 : -4278419646001971p-51 +Run tests with F + 0.100000 + 2.000000 = 2.100000 + 0.100000 : +3602879701896397p-55 + 2.000000 : +1p1 + 2.100000 : +1182194902184755p-49 +-0.100000 + 2.000000 = 1.900000 +-0.100000 : -3602879701896397p-55 +2.000000 : +1p1 +1.900000 : +4278419646001971p-51 +-0.100000 + -2.000000 = -2.100000 +-0.100000 : -3602879701896397p-55 +-2.000000 : -1p1 +-2.100000 : -1182194902184755p-49 +0.100000 + -2.000000 = -1.900000 +0.100000 : +3602879701896397p-55 +-2.000000 : -1p1 +-1.900000 : -4278419646001971p-51 diff --git a/farith/tests/tie.ml b/farith/tests/tie.ml new file mode 100644 index 0000000000000000000000000000000000000000..092cfbef32a387efea49a100cabe7da72c0ef810 --- /dev/null +++ b/farith/tests/tie.ml @@ -0,0 +1,46 @@ + +let pp fmt z = + let n = F.exponent z in + let a = F.mantissa z in + if 0 <= Z.sign a then Format.pp_print_char fmt '+' ; + if n >= 0 + then + Z.pp_print fmt (Z.shift_left a n) + else + Format.fprintf fmt "%ap%d" Z.pp_print a n + +let tiebreak a b n = + begin + (* Tie breaks at [2^(n-1) + e] with [n] bits precision *) + let m = n-1 in + let up = Q.mul_2exp Q.one m in + let q = Q.(up + Q.make (Z.of_int a) (Z.of_int b)) in + let f0 = F.of_qint ~bits:(n+1) q in (* exact *) + let f1,f2 = F.seize ~bits:n f0 in + Format.printf "------------------------------------------@\n" ; + Format.printf " - %a (%a)@\n" pp f1 F.pp f1 ; + Format.printf "1p%d+%d/%d = %a (%a)@\n" m a b pp f0 F.pp f0 ; + Format.printf " + %a (%a)@\n" pp f2 F.pp f2 ; + Format.printf "mantissa = %a@\n" Z.pp_print (Z.shift_left Z.one n) ; + let f1 = F.neg f0 in + let pos_ne = F.round ~mode:F.NE ~bits:n f0 in + let pos_na = F.round ~mode:F.NA ~bits:n f0 in + let neg_ne = F.round ~mode:F.NE ~bits:n f1 in + let neg_na = F.round ~mode:F.NA ~bits:n f1 in + let module G = Farith.Make(struct let ew = 8 let mw = m end) in + let coq_ne = G.of_q Farith.NE q in + let coq_na = G.of_q Farith.NA q in + Format.printf "=NE %a@\n" G.pp coq_ne ; + Format.printf "+NE %a (%a)@\n" F.pp pos_ne pp pos_ne ; + Format.printf "-NE %a (%a)@\n" F.pp neg_ne pp neg_ne ; + Format.printf "=NA %a@\n" G.pp coq_na ; + Format.printf "+NA %a (%a)@\n" F.pp pos_na pp pos_na ; + Format.printf "-NA %a (%a)@\n" F.pp neg_na pp neg_na ; + Format.print_flush () ; + end + +let () = + begin + tiebreak 1 2 F.b64 ; + tiebreak 3 2 F.b64 ; + end diff --git a/farith/tests/tie.oracle b/farith/tests/tie.oracle new file mode 100644 index 0000000000000000000000000000000000000000..8b916f28184d51a62b34e9a8869e04a5557abad1 --- /dev/null +++ b/farith/tests/tie.oracle @@ -0,0 +1,22 @@ +------------------------------------------ + - +4503599627370496 (+1p52) +1p52+1/2 = +9007199254740993p-1 (+9007199254740993p-1) + + +4503599627370497 (+4503599627370497) +mantissa = 9007199254740992 +=NE +1p52 ++NE +1p52 (+4503599627370496) +-NE -1p52 (-4503599627370496) +=NA +4503599627370497p0 ++NA +4503599627370497 (+4503599627370497) +-NA -4503599627370497 (-4503599627370497) +------------------------------------------ + - +4503599627370497 (+4503599627370497) +1p52+3/2 = +9007199254740995p-1 (+9007199254740995p-1) + + +4503599627370498 (+2251799813685249p1) +mantissa = 9007199254740992 +=NE +2251799813685249p1 ++NE +2251799813685249p1 (+4503599627370498) +-NE -2251799813685249p1 (-4503599627370498) +=NA +2251799813685249p1 ++NA +2251799813685249p1 (+4503599627370498) +-NA -2251799813685249p1 (-4503599627370498)