1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
File "./output/FloatExtraction.v", line 25, characters 8-12:
Warning: The constant 0.01 is not a binary64 floating-point value. A closest
value 0x1.47ae147ae147bp-7 will be used and unambiguously printed 0.01.
[inexact-float,parsing]
File "./output/FloatExtraction.v", line 25, characters 20-25:
Warning: The constant -0.01 is not a binary64 floating-point value. A closest
value -0x1.47ae147ae147bp-7 will be used and unambiguously printed -0.01.
[inexact-float,parsing]
File "./output/FloatExtraction.v", line 25, characters 27-35:
Warning: The constant 1.7e+308 is not a binary64 floating-point value. A
closest value 0x1.e42d130773b76p+1023 will be used and unambiguously printed
1.6999999999999999e+308. [inexact-float,parsing]
File "./output/FloatExtraction.v", line 25, characters 37-46:
Warning: The constant -1.7e-308 is not a binary64 floating-point value. A
closest value -0x0.c396c98f8d899p-1022 will be used and unambiguously printed
-1.7000000000000002e-308. [inexact-float,parsing]
(** 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)
|
