blob: d9b9d3a6b932215ab1ef4355a7ef13d4de8541ef (
plain)
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
|
Require Import Floats Integers ZArith.
Module ExtFloat.
(** TODO check with the actual K1c;
this is what happens on x86 and may be inappropriate. *)
Definition min (x : float) (y : float) : float :=
match Float.compare x y with
| Some Eq | Some Lt => x
| Some Gt | None => y
end.
Definition max (x : float) (y : float) : float :=
match Float.compare x y with
| Some Eq | Some Gt => x
| Some Lt | None => y
end.
End ExtFloat.
Module ExtFloat32.
(** TODO check with the actual K1c *)
Definition min (x : float32) (y : float32) : float32 :=
match Float32.compare x y with
| Some Eq | Some Lt => x
| Some Gt | None => y
end.
Definition max (x : float32) (y : float32) : float32 :=
match Float32.compare x y with
| Some Eq | Some Gt => x
| Some Lt | None => y
end.
Definition one := Float32.of_int (Int.repr (1%Z)).
Definition inv (x : float32) : float32 :=
Float32.div one x.
End ExtFloat32.
|
