From 1ecddb62bc5aa8e6a1f6c1a1a2da2e2a8e2b100f Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Sun, 12 Dec 2021 15:18:18 +0100
Subject: Values: conversions to nearest int

---
 common/Values.v | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index 87ebea00..cf5a1255 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -244,6 +244,18 @@ Definition intuoffloat (v: val) : option val :=
   | _ => None
   end.
 
+Definition intoffloat_ne (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vint (Float.to_int_ne f)
+  | _ => None
+  end.
+
+Definition intuoffloat_ne (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vint (Float.to_intu_ne f)
+  | _ => None
+  end.
+
 Definition floatofint (v: val) : option val :=
   match v with
   | Vint n => Some (Vfloat (Float.of_int n))
@@ -268,6 +280,18 @@ Definition intuofsingle (v: val) : option val :=
   | _ => None
   end.
 
+Definition intofsingle_ne (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vint (Float32.to_int_ne f)
+  | _ => None
+  end.
+
+Definition intuofsingle_ne (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vint (Float32.to_intu_ne f)
+  | _ => None
+  end.
+
 Definition singleofint (v: val) : option val :=
   match v with
   | Vint n => Some (Vsingle (Float32.of_int n))
@@ -623,6 +647,30 @@ Definition longuofsingle (v: val) : option val :=
   | _ => None
   end.
 
+Definition longoffloat_ne (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vlong (Float.to_long_ne f)
+  | _ => None
+  end.
+
+Definition longuoffloat_ne (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vlong (Float.to_longu_ne f)
+  | _ => None
+  end.
+
+Definition longofsingle_ne (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vlong (Float32.to_long_ne f)
+  | _ => None
+  end.
+
+Definition longuofsingle_ne (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vlong (Float32.to_longu_ne f)
+  | _ => None
+  end.
+
 Definition floatoflong (v: val) : option val :=
   match v with
   | Vlong n => Some (Vfloat (Float.of_long n))
-- 
cgit