Revised encoding/decoding of floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 73 insertions, 11 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 51915fd..34aaa0f 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -18,7 +18,6 @@
 open Datatypes
 open BinPos
 open BinInt
-open Integers
 
 (* Integers *)
 
@@ -32,7 +31,19 @@ let camlint_of_z = function
   | Zpos p -> camlint_of_positive p
   | Zneg p -> Int32.neg (camlint_of_positive p)
 
-let camlint_of_coqint : Int.int -> int32 = camlint_of_z
+let camlint_of_coqint : Integers.Int.int -> int32 = camlint_of_z
+
+let rec camlint64_of_positive = function
+  | Coq_xI p -> Int64.add (Int64.shift_left (camlint64_of_positive p) 1) 1L
+  | Coq_xO p -> Int64.shift_left (camlint64_of_positive p) 1
+  | Coq_xH -> 1L
+
+let camlint64_of_z = function
+  | Z0 -> 0L
+  | Zpos p -> camlint64_of_positive p
+  | Zneg p -> Int64.neg (camlint64_of_positive p)
+
+let camlint64_of_coqint : Integers.Int64.int -> int64 = camlint64_of_z
 
 let rec camlint_of_nat = function
   | O -> 0
@@ -54,10 +65,26 @@ let z_of_camlint n =
   if n > 0l then Zpos (positive_of_camlint n)
   else Zneg (positive_of_camlint (Int32.neg n))
 
-let coqint_of_camlint (n: int32) : Int.int = 
+let coqint_of_camlint (n: int32) : Integers.Int.int = 
   (* Interpret n as unsigned so that resulting Z is in range *)
   if n = 0l then Z0 else Zpos (positive_of_camlint n)
 
+let rec positive_of_camlint64 n =
+  if n = 0L then assert false else
+  if n = 1L then Coq_xH else
+  if Int64.logand n 1L = 0L
+  then Coq_xO (positive_of_camlint64 (Int64.shift_right_logical n 1))
+  else Coq_xI (positive_of_camlint64 (Int64.shift_right_logical n 1))
+
+let z_of_camlint64 n =
+  if n = 0L then Z0 else
+  if n > 0L then Zpos (positive_of_camlint64 n)
+  else Zneg (positive_of_camlint64 (Int64.neg n))
+
+let coqint_of_camlint64 (n: int64) : Integers.Int64.int = 
+  (* Interpret n as unsigned so that resulting Z is in range *)
+  if n = 0L then Z0 else Zpos (positive_of_camlint64 n)
+
 (* Atoms (positive integers representing strings) *)
 
 let atom_of_string = (Hashtbl.create 17 : (string, positive) Hashtbl.t)
diff --git a/lib/Floataux.ml b/lib/Floataux.ml
index 6b3b825..ebea884 100644
--- a/lib/Floataux.ml
+++ b/lib/Floataux.ml
@@ -11,7 +11,6 @@
 (* *********************************************************************)
 
 open Camlcoq
-open Integers
 
 let singleoffloat f =
   Int32.float_of_bits (Int32.bits_of_float f)
@@ -31,9 +30,15 @@ let floatofintu i =
 
 let cmp c (x: float) (y: float) =
   match c with
-  | Ceq -> x = y
-  | Cne -> x <> y
-  | Clt -> x < y
-  | Cle -> x <= y
-  | Cgt -> x > y
-  | Cge -> x >= y
+  | Integers.Ceq -> x = y
+  | Integers.Cne -> x <> y
+  | Integers.Clt -> x < y
+  | Integers.Cle -> x <= y
+  | Integers.Cgt -> x > y
+  | Integers.Cge -> x >= y
+
+let bits_of_single f = coqint_of_camlint (Int32.bits_of_float f)
+let single_of_bits f = Int32.float_of_bits (camlint_of_coqint f)
+
+let bits_of_double f = coqint_of_camlint64 (Int64.bits_of_float f)
+let double_of_bits f = Int64.float_of_bits (camlint64_of_coqint f)
diff --git a/lib/Floats.v b/lib/Floats.v
index 2e60d73..50298f7 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -47,6 +47,12 @@ Parameter cmp: comparison -> float -> float -> bool.
 
 Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}.
 
+Parameter bits_of_double: float -> int64.
+Parameter double_of_bits: int64 -> float.
+
+Parameter bits_of_single: float -> int.
+Parameter single_of_bits: int -> float.
+
 (** Below are the only properties of floating-point arithmetic that we
   rely on in the compiler proof. *)
 
@@ -67,4 +73,16 @@ Axiom cmp_ge_gt_eq:
 Axiom eq_zero_true: cmp Ceq zero zero = true.
 Axiom eq_zero_false: forall f, f <> zero -> cmp Ceq f zero = false.
 
+Axiom bits_of_double_of_bits:
+  forall n, bits_of_double (double_of_bits n) = n.
+Axiom double_of_bits_of_double:
+  forall f, double_of_bits (bits_of_double f) = f.
+Axiom bits_of_single_of_bits:
+  forall n, bits_of_single (single_of_bits n) = n.
+Axiom single_of_bits_of_single:
+  forall f, single_of_bits (bits_of_single f) = singleoffloat f.
+
+Axiom bits_of_singleoffloat:
+  forall f, bits_of_single (singleoffloat f) = bits_of_single f.
+
 End Float.
diff --git a/lib/Integers.v b/lib/Integers.v
index d047199..f2aca96 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -2770,7 +2770,7 @@ Qed.
 
 End Make.
 
-(** * Specialization to 32-bit integers and to bytes. *)
+(** * Specialization to integers of size 8, 32, and 64 bits *)
 
 Module Wordsize_32.
   Definition wordsize := 32%nat.
@@ -2797,3 +2797,15 @@ End Wordsize_8.
 Module Byte := Integers.Make(Wordsize_8).
 
 Notation byte := Byte.int.
+
+Module Wordsize_64.
+  Definition wordsize := 64%nat.
+  Remark wordsize_not_zero: wordsize <> 0%nat.
+  Proof. unfold wordsize; congruence. Qed.
+End Wordsize_64.
+
+Module Int64 := Make(Wordsize_64).
+
+Notation int64 := Int64.int.
+
+