Merge PR #9867: Add primitive floats (binary64 floating-point numbers)

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl

1 files changed, 33 insertions, 0 deletions

diff --git a/test-suite/output/FloatExtraction.v b/test-suite/output/FloatExtraction.v
new file mode 100644
index 0000000000..f296e8e871
--- /dev/null
+++ b/test-suite/output/FloatExtraction.v
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import Floats ExtrOCamlFloats.
+
+Require Import List. Import ListNotations.
+
+(* from Require Import ExtrOcamlBasic. *)
+Extract Inductive list => list [ "[]" "( :: )" ].
+
+Local Open Scope float_scope.
+
+(* Avoid exponents with less than three digits as they are usually
+   displayed with two digits (1e7 is displayed 1e+07) except on
+   Windows where three digits are used (1e+007). *)
+Definition list_floats :=
+  [nan; infinity; neg_infinity; zero; one; two;
+   0.5; 0.01; -0.5; -0.01; 1.7e+308; -1.7e-308].
+
+Recursive Extraction list_floats.
+
+Definition discr a b c := b * b - 4.0 * a * c.
+
+Definition x1 a b c := (- b - sqrt (discr a b c)) / (2.0 * a).
+
+Recursive Extraction x1.