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.