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, 67 insertions, 0 deletions

diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out
new file mode 100644
index 0000000000..cfd6633752
--- /dev/null
+++ b/test-suite/output/FloatExtraction.out
@@ -0,0 +1,67 @@
+
+(** val infinity : Float64.t **)
+
+let infinity =
+  (Float64.of_float (infinity))
+
+(** val neg_infinity : Float64.t **)
+
+let neg_infinity =
+  (Float64.of_float (neg_infinity))
+
+(** val nan : Float64.t **)
+
+let nan =
+  (Float64.of_float (nan))
+
+(** val one : Float64.t **)
+
+let one =
+  (Float64.of_float (0x1p+0))
+
+(** val zero : Float64.t **)
+
+let zero =
+  (Float64.of_float (0x0p+0))
+
+(** val two : Float64.t **)
+
+let two =
+  (Float64.of_float (0x1p+1))
+
+(** val list_floats : Float64.t list **)
+
+let list_floats =
+  nan :: (infinity :: (neg_infinity :: (zero :: (one :: (two :: ((Float64.of_float (0x1p-1)) :: ((Float64.of_float (0x1.47ae147ae147bp-7)) :: ((Float64.of_float (-0x1p-1)) :: ((Float64.of_float (-0x1.47ae147ae147bp-7)) :: ((Float64.of_float (0x1.e42d130773b76p+1023)) :: ((Float64.of_float (-0x0.c396c98f8d899p-1022)) :: [])))))))))))
+
+
+(** val sqrt : Float64.t -> Float64.t **)
+
+let sqrt = Float64.sqrt
+
+(** val opp : Float64.t -> Float64.t **)
+
+let opp = Float64.opp
+
+(** val mul : Float64.t -> Float64.t -> Float64.t **)
+
+let mul = Float64.mul
+
+(** val sub : Float64.t -> Float64.t -> Float64.t **)
+
+let sub = Float64.sub
+
+(** val div : Float64.t -> Float64.t -> Float64.t **)
+
+let div = Float64.div
+
+(** val discr : Float64.t -> Float64.t -> Float64.t -> Float64.t **)
+
+let discr a b c =
+  sub (mul b b) (mul (mul (Float64.of_float (0x1p+2)) a) c)
+
+(** val x1 : Float64.t -> Float64.t -> Float64.t -> Float64.t **)
+
+let x1 a b c =
+  div (sub (opp b) (sqrt (discr a b c))) (mul (Float64.of_float (0x1p+1)) a)
+