begin implementing minf/maxf

1 files changed, 33 insertions, 0 deletions

diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v
new file mode 100644
index 00000000..efea278b
--- /dev/null
+++ b/mppa_k1c/ExtFloats.v
@@ -0,0 +1,33 @@
+Require Import Floats.
+
+Module ExtFloat.
+(** TODO check with the actual K1c *)
+
+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.
+End ExtFloat32.