blob: 332d3e3d30522662a0deb5d985ba62815908dd5d (
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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* Xavier Leroy INRIA Paris-Rocquencourt *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
Binary Round_odd.
Require Import Floats Integers ZArith.
Module ExtFloat.
(** TODO check with the actual KVX;
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.
Definition one := Float.of_int (Int.repr (1%Z)).
End ExtFloat.
Module ExtFloat32.
(** TODO check with the actual KVX *)
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.
|
