diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
commit | d71a5cfd10378301b71d32659d5936e01d72ae50 (patch) | |
tree | 9b6a7cc437ab205b7e0bf5bf90585451d8a8c367 /lib/Camlcoq.ml | |
parent | 913c1bcc4b2204afd447edd723e06b905fd1f47f (diff) | |
download | compcert-d71a5cfd10378301b71d32659d5936e01d72ae50.tar.gz compcert-d71a5cfd10378301b71d32659d5936e01d72ae50.zip |
Revised encoding/decoding of floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Camlcoq.ml')
-rw-r--r-- | lib/Camlcoq.ml | 33 |
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) |