From b0a4ae7406b23bfa2f77e8ce948d99e9d9147e54 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr> Date: Fri, 27 May 2022 15:41:21 +0200 Subject: [PATCH] Remove farith --- Makefile | 2 +- dune-project | 9 - farith.opam | 30 - farith/.gitignore | 10 - farith/F.ml | 364 ------ farith/F.mli | 119 -- farith/F_aux.v | 1108 ------------------ farith/LGPLv2.1 | 502 -------- farith/LGPLv3 | 165 --- farith/META | 9 - farith/Makefile | 124 -- farith/README.md | 30 - farith/_tags | 5 - farith/bench/micro.ml | 49 - farith/bench/valgrind.ml | 16 - farith/ceatech.css | 122 -- farith/dune | 15 - farith/extract.sh | 29 - farith/extract.v | 293 ----- farith/extracted/dune | 7 - farith/extracted/farith_BinInt.ml | 91 -- farith/extracted/farith_BinInt.mli | 33 - farith/extracted/farith_BinPos.ml | 222 ---- farith/extracted/farith_BinPos.mli | 60 - farith/extracted/farith_BinPosDef.ml | 26 - farith/extracted/farith_BinPosDef.mli | 26 - farith/extracted/farith_Bool.ml | 23 - farith/extracted/farith_Bool.mli | 20 - farith/extracted/farith_Datatypes.ml | 35 - farith/extracted/farith_Datatypes.mli | 27 - farith/extracted/farith_F_aux.ml | 1021 ---------------- farith/extracted/farith_F_aux.mli | 452 ------- farith/extracted/farith_Fappli_IEEE.ml | 554 --------- farith/extracted/farith_Fappli_IEEE.mli | 138 --- farith/extracted/farith_Fappli_IEEE_bits.ml | 135 --- farith/extracted/farith_Fappli_IEEE_bits.mli | 41 - farith/extracted/farith_Fcalc_bracket.ml | 70 -- farith/extracted/farith_Fcalc_bracket.mli | 34 - farith/extracted/farith_Fcalc_round.ml | 48 - farith/extracted/farith_Fcalc_round.mli | 29 - farith/extracted/farith_Fcore_FLT.ml | 25 - farith/extracted/farith_Fcore_FLT.mli | 22 - farith/extracted/farith_Fcore_Zaux.ml | 143 --- farith/extracted/farith_Fcore_Zaux.mli | 39 - farith/extracted/farith_Fcore_digits.ml | 42 - farith/extracted/farith_Fcore_digits.mli | 22 - farith/extracted/farith_Flocq_version.ml | 27 - farith/extracted/farith_Flocq_version.mli | 20 - farith/extracted/farith_Specif.ml | 22 - farith/extracted/farith_Specif.mli | 22 - farith/extracted/farith_Zpower.ml | 26 - farith/extracted/farith_Zpower.mli | 23 - farith/farith.ml | 190 --- farith/farith.mli | 294 ----- farith/farith.mltop | 20 - farith/farith_Big.ml | 238 ---- farith/farith_top.ml | 17 - farith/headers/CEA_LGPL | 18 - farith/headers/FLOCQ | 16 - farith/headers/header.config | 16 - farith/opam | 27 - farith/tests/Makefile | 57 - farith/tests/_tags | 0 farith/tests/issue_005.ml | 17 - farith/tests/issue_005.oracle | 2 - farith/tests/mode.ml | 47 - farith/tests/mode.oracle | 88 -- farith/tests/subnormal.ml | 41 - farith/tests/subnormal.oracle | 28 - farith/tests/test.ml | 46 - farith/tests/test.oracle | 35 - farith/tests/tie.ml | 46 - farith/tests/tie.oracle | 22 - 73 files changed, 1 insertion(+), 7790 deletions(-) delete mode 100644 farith.opam delete mode 100644 farith/.gitignore delete mode 100644 farith/F.ml delete mode 100644 farith/F.mli delete mode 100644 farith/F_aux.v delete mode 100644 farith/LGPLv2.1 delete mode 100644 farith/LGPLv3 delete mode 100644 farith/META delete mode 100644 farith/Makefile delete mode 100644 farith/README.md delete mode 100644 farith/_tags delete mode 100644 farith/bench/micro.ml delete mode 100644 farith/bench/valgrind.ml delete mode 100644 farith/ceatech.css delete mode 100644 farith/dune delete mode 100755 farith/extract.sh delete mode 100644 farith/extract.v delete mode 100644 farith/extracted/dune delete mode 100644 farith/extracted/farith_BinInt.ml delete mode 100644 farith/extracted/farith_BinInt.mli delete mode 100644 farith/extracted/farith_BinPos.ml delete mode 100644 farith/extracted/farith_BinPos.mli delete mode 100644 farith/extracted/farith_BinPosDef.ml delete mode 100644 farith/extracted/farith_BinPosDef.mli delete mode 100644 farith/extracted/farith_Bool.ml delete mode 100644 farith/extracted/farith_Bool.mli delete mode 100644 farith/extracted/farith_Datatypes.ml delete mode 100644 farith/extracted/farith_Datatypes.mli delete mode 100644 farith/extracted/farith_F_aux.ml delete mode 100644 farith/extracted/farith_F_aux.mli delete mode 100644 farith/extracted/farith_Fappli_IEEE.ml delete mode 100644 farith/extracted/farith_Fappli_IEEE.mli delete mode 100644 farith/extracted/farith_Fappli_IEEE_bits.ml delete mode 100644 farith/extracted/farith_Fappli_IEEE_bits.mli delete mode 100644 farith/extracted/farith_Fcalc_bracket.ml delete mode 100644 farith/extracted/farith_Fcalc_bracket.mli delete mode 100644 farith/extracted/farith_Fcalc_round.ml delete mode 100644 farith/extracted/farith_Fcalc_round.mli delete mode 100644 farith/extracted/farith_Fcore_FLT.ml delete mode 100644 farith/extracted/farith_Fcore_FLT.mli delete mode 100644 farith/extracted/farith_Fcore_Zaux.ml delete mode 100644 farith/extracted/farith_Fcore_Zaux.mli delete mode 100644 farith/extracted/farith_Fcore_digits.ml delete mode 100644 farith/extracted/farith_Fcore_digits.mli delete mode 100644 farith/extracted/farith_Flocq_version.ml delete mode 100644 farith/extracted/farith_Flocq_version.mli delete mode 100644 farith/extracted/farith_Specif.ml delete mode 100644 farith/extracted/farith_Specif.mli delete mode 100644 farith/extracted/farith_Zpower.ml delete mode 100644 farith/extracted/farith_Zpower.mli delete mode 100644 farith/farith.ml delete mode 100644 farith/farith.mli delete mode 100644 farith/farith.mltop delete mode 100644 farith/farith_Big.ml delete mode 100644 farith/farith_top.ml delete mode 100644 farith/headers/CEA_LGPL delete mode 100644 farith/headers/FLOCQ delete mode 100644 farith/headers/header.config delete mode 100644 farith/opam delete mode 100644 farith/tests/Makefile delete mode 100644 farith/tests/_tags delete mode 100644 farith/tests/issue_005.ml delete mode 100644 farith/tests/issue_005.oracle delete mode 100644 farith/tests/mode.ml delete mode 100644 farith/tests/mode.oracle delete mode 100644 farith/tests/subnormal.ml delete mode 100644 farith/tests/subnormal.oracle delete mode 100644 farith/tests/test.ml delete mode 100644 farith/tests/test.oracle delete mode 100644 farith/tests/tie.ml delete mode 100644 farith/tests/tie.oracle diff --git a/Makefile b/Makefile index 36572129f..d2546a483 100644 --- a/Makefile +++ b/Makefile @@ -19,7 +19,7 @@ ########################################################################## all: - dune build --root=$$(pwd) @install colibri2.opam colibrics.opam farith.opam + dune build --root=$$(pwd) @install colibri2.opam colibrics.opam test: dune runtest --root=$$(pwd) diff --git a/dune-project b/dune-project index df06c2291..aeebd5a47 100644 --- a/dune-project +++ b/dune-project @@ -60,15 +60,6 @@ ) ) -(package (name farith) - (authors "François Bobot" "Loïc Correnson") - (maintainers "François Bobot") - (license LGPL-3.0-only) - (synopsis "A Library for IEEE floating points number with fixed arbitary exponent and mantissa size") - (description "Obtained from extraction of the Flocq library proved in Coq") - (depends "zarith") -) - (package (name farith2) (synopsis "formaly verified floating-points valuations based on Flocq")) diff --git a/farith.opam b/farith.opam deleted file mode 100644 index 8c0790509..000000000 --- a/farith.opam +++ /dev/null @@ -1,30 +0,0 @@ -# This file is generated by dune, edit dune-project instead -opam-version: "2.0" -synopsis: - "A Library for IEEE floating points number with fixed arbitary exponent and mantissa size" -description: "Obtained from extraction of the Flocq library proved in Coq" -maintainer: ["François Bobot"] -authors: ["François Bobot" "Loïc Correnson"] -license: "LGPL-3.0-only" -homepage: "https://git.frama-c.com/bobot/colibrics" -bug-reports: "https://git.frama-c.com/bobot/colibrics/issues" -depends: [ - "dune" {>= "3.0"} - "zarith" - "odoc" {with-doc} -] -build: [ - ["dune" "subst"] {dev} - [ - "dune" - "build" - "-p" - name - "-j" - jobs - "@install" - "@runtest" {with-test} - "@doc" {with-doc} - ] -] -dev-repo: "git+https://git.frama-c.com/bobot/colibrics.git" diff --git a/farith/.gitignore b/farith/.gitignore deleted file mode 100644 index 4c8875a74..000000000 --- a/farith/.gitignore +++ /dev/null @@ -1,10 +0,0 @@ -/html/ -/tests/_local -/tests/*.log -/tests/*.diff -_build/ -*.native -*.vo -*.glob -.local -/farith.top diff --git a/farith/F.ml b/farith/F.ml deleted file mode 100644 index bb684ee40..000000000 --- a/farith/F.ml +++ /dev/null @@ -1,364 +0,0 @@ -(**************************************************************************) -(* *) -(* 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 deleted file mode 100644 index 3894d0da0..000000000 --- a/farith/F.mli +++ /dev/null @@ -1,119 +0,0 @@ -(**************************************************************************) -(* *) -(* 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 deleted file mode 100644 index 69eb01524..000000000 --- a/farith/F_aux.v +++ /dev/null @@ -1,1108 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 4362b4915..000000000 --- a/farith/LGPLv2.1 +++ /dev/null @@ -1,502 +0,0 @@ - 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 deleted file mode 100644 index 65c5ca88a..000000000 --- a/farith/LGPLv3 +++ /dev/null @@ -1,165 +0,0 @@ - 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 deleted file mode 100644 index f3930e802..000000000 --- a/farith/META +++ /dev/null @@ -1,9 +0,0 @@ -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 deleted file mode 100644 index ee311beef..000000000 --- a/farith/Makefile +++ /dev/null @@ -1,124 +0,0 @@ -########################################################################## -# 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 deleted file mode 100644 index b0a46e6e8..000000000 --- a/farith/README.md +++ /dev/null @@ -1,30 +0,0 @@ -## 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 deleted file mode 100644 index 57c38c965..000000000 --- a/farith/_tags +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index 9306a38cc..000000000 --- a/farith/bench/micro.ml +++ /dev/null @@ -1,49 +0,0 @@ -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 deleted file mode 100644 index 1b190ab2d..000000000 --- a/farith/bench/valgrind.ml +++ /dev/null @@ -1,16 +0,0 @@ - - -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 deleted file mode 100644 index 8a9db5b06..000000000 --- a/farith/ceatech.css +++ /dev/null @@ -1,122 +0,0 @@ -* { 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 deleted file mode 100644 index 8538a39b5..000000000 --- a/farith/dune +++ /dev/null @@ -1,15 +0,0 @@ -(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/extract.sh b/farith/extract.sh deleted file mode 100755 index 202c6663d..000000000 --- a/farith/extract.sh +++ /dev/null @@ -1,29 +0,0 @@ -#!/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 deleted file mode 100644 index a0138b9bf..000000000 --- a/farith/extract.v +++ /dev/null @@ -1,293 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index a7efb1802..000000000 --- a/farith/extracted/dune +++ /dev/null @@ -1,7 +0,0 @@ -(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 deleted file mode 100644 index 69bcab00b..000000000 --- a/farith/extracted/farith_BinInt.ml +++ /dev/null @@ -1,91 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 6027a4c38..000000000 --- a/farith/extracted/farith_BinInt.mli +++ /dev/null @@ -1,33 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index cd7efe482..000000000 --- a/farith/extracted/farith_BinPos.ml +++ /dev/null @@ -1,222 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index ad1aa2cfe..000000000 --- a/farith/extracted/farith_BinPos.mli +++ /dev/null @@ -1,60 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index a85d842db..000000000 --- a/farith/extracted/farith_BinPosDef.ml +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 281d371e6..000000000 --- a/farith/extracted/farith_BinPosDef.mli +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 5ef6467c1..000000000 --- a/farith/extracted/farith_Bool.ml +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index dcac38d25..000000000 --- a/farith/extracted/farith_Bool.mli +++ /dev/null @@ -1,20 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 73c632d33..000000000 --- a/farith/extracted/farith_Datatypes.ml +++ /dev/null @@ -1,35 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index c9d882304..000000000 --- a/farith/extracted/farith_Datatypes.mli +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 55f0d277f..000000000 --- a/farith/extracted/farith_F_aux.ml +++ /dev/null @@ -1,1021 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index d16b9643a..000000000 --- a/farith/extracted/farith_F_aux.mli +++ /dev/null @@ -1,452 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 7940996c8..000000000 --- a/farith/extracted/farith_Fappli_IEEE.ml +++ /dev/null @@ -1,554 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index a77cf11c2..000000000 --- a/farith/extracted/farith_Fappli_IEEE.mli +++ /dev/null @@ -1,138 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 009e9bf27..000000000 --- a/farith/extracted/farith_Fappli_IEEE_bits.ml +++ /dev/null @@ -1,135 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 2f54c6c96..000000000 --- a/farith/extracted/farith_Fappli_IEEE_bits.mli +++ /dev/null @@ -1,41 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 7a22213d3..000000000 --- a/farith/extracted/farith_Fcalc_bracket.ml +++ /dev/null @@ -1,70 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 71932c134..000000000 --- a/farith/extracted/farith_Fcalc_bracket.mli +++ /dev/null @@ -1,34 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 8d36dadee..000000000 --- a/farith/extracted/farith_Fcalc_round.ml +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index ced81c22d..000000000 --- a/farith/extracted/farith_Fcalc_round.mli +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 98258927b..000000000 --- a/farith/extracted/farith_Fcore_FLT.ml +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 46303759f..000000000 --- a/farith/extracted/farith_Fcore_FLT.mli +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 3bec89d99..000000000 --- a/farith/extracted/farith_Fcore_Zaux.ml +++ /dev/null @@ -1,143 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 19b3e8761..000000000 --- a/farith/extracted/farith_Fcore_Zaux.mli +++ /dev/null @@ -1,39 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index b109d4c3b..000000000 --- a/farith/extracted/farith_Fcore_digits.ml +++ /dev/null @@ -1,42 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index d7a5d5533..000000000 --- a/farith/extracted/farith_Fcore_digits.mli +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 87d0558b9..000000000 --- a/farith/extracted/farith_Flocq_version.ml +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 6df42bb46..000000000 --- a/farith/extracted/farith_Flocq_version.mli +++ /dev/null @@ -1,20 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 9566937cf..000000000 --- a/farith/extracted/farith_Specif.ml +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 9566937cf..000000000 --- a/farith/extracted/farith_Specif.mli +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 5bb7f690b..000000000 --- a/farith/extracted/farith_Zpower.ml +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index a16c84bb8..000000000 --- a/farith/extracted/farith_Zpower.mli +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index bb7f79f54..000000000 --- a/farith/farith.ml +++ /dev/null @@ -1,190 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 1e5bdd1ea..000000000 --- a/farith/farith.mli +++ /dev/null @@ -1,294 +0,0 @@ -(**************************************************************************) -(* 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 deleted file mode 100644 index 9271ca987..000000000 --- a/farith/farith.mltop +++ /dev/null @@ -1,20 +0,0 @@ -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_Big.ml b/farith/farith_Big.ml deleted file mode 100644 index 8ed2ad80c..000000000 --- a/farith/farith_Big.ml +++ /dev/null @@ -1,238 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 7ad8a6a59..000000000 --- a/farith/farith_top.ml +++ /dev/null @@ -1,17 +0,0 @@ -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 deleted file mode 100644 index 4e1e48826..000000000 --- a/farith/headers/CEA_LGPL +++ /dev/null @@ -1,18 +0,0 @@ -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 deleted file mode 100644 index 206e9cc72..000000000 --- a/farith/headers/FLOCQ +++ /dev/null @@ -1,16 +0,0 @@ -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 deleted file mode 100644 index 5a3b16f2c..000000000 --- a/farith/headers/header.config +++ /dev/null @@ -1,16 +0,0 @@ -################## -# 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 deleted file mode 100644 index 82dd924ae..000000000 --- a/farith/opam +++ /dev/null @@ -1,27 +0,0 @@ -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 deleted file mode 100644 index 5253f9a26..000000000 --- a/farith/tests/Makefile +++ /dev/null @@ -1,57 +0,0 @@ -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 deleted file mode 100644 index e69de29bb..000000000 diff --git a/farith/tests/issue_005.ml b/farith/tests/issue_005.ml deleted file mode 100644 index 2c7f66d49..000000000 --- a/farith/tests/issue_005.ml +++ /dev/null @@ -1,17 +0,0 @@ -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 deleted file mode 100644 index 393a46758..000000000 --- a/farith/tests/issue_005.oracle +++ /dev/null @@ -1,2 +0,0 @@ -[G] 0.100000 : +3602879701896397p-55 -[F] 0.100000 : +3602879701896397p-55 diff --git a/farith/tests/mode.ml b/farith/tests/mode.ml deleted file mode 100644 index 9d394fe10..000000000 --- a/farith/tests/mode.ml +++ /dev/null @@ -1,47 +0,0 @@ - -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 deleted file mode 100644 index 6e11103a8..000000000 --- a/farith/tests/mode.oracle +++ /dev/null @@ -1,88 +0,0 @@ -[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 deleted file mode 100644 index 8a3e2f60b..000000000 --- a/farith/tests/subnormal.ml +++ /dev/null @@ -1,41 +0,0 @@ - -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 deleted file mode 100644 index 8936ea17c..000000000 --- a/farith/tests/subnormal.oracle +++ /dev/null @@ -1,28 +0,0 @@ -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 deleted file mode 100644 index 1d2a73629..000000000 --- a/farith/tests/test.ml +++ /dev/null @@ -1,46 +0,0 @@ -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 deleted file mode 100644 index ec6223604..000000000 --- a/farith/tests/test.oracle +++ /dev/null @@ -1,35 +0,0 @@ -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 deleted file mode 100644 index 092cfbef3..000000000 --- a/farith/tests/tie.ml +++ /dev/null @@ -1,46 +0,0 @@ - -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 deleted file mode 100644 index 8b916f281..000000000 --- a/farith/tests/tie.oracle +++ /dev/null @@ -1,22 +0,0 @@ ------------------------------------------- - - +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) -- GitLab