diff options
Diffstat (limited to 'mppa_k1c/ExtFloats.v')
-rw-r--r-- | mppa_k1c/ExtFloats.v | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v new file mode 100644 index 00000000..d9b9d3a6 --- /dev/null +++ b/mppa_k1c/ExtFloats.v @@ -0,0 +1,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. |