Revised encoding/decoding of floats

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

1 files changed, 30 insertions, 3 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 51915fd5..34aaa0fd 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)