diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
| commit | 5312915c1b29929f82e1f8de80609a277584913f (patch) | |
| tree | 0f7ee475743f0eb05d352148a9e1f0b861ee9d34 /lib/Camlcoq.ml | |
| parent | f3250c32ff42ae18fd03a5311c1f0caec3415aba (diff) | |
| download | compcert-kvx-5312915c1b29929f82e1f8de80609a277584913f.tar.gz compcert-kvx-5312915c1b29929f82e1f8de80609a277584913f.zip | |
Use Flocq for floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Camlcoq.ml')
| -rw-r--r-- | lib/Camlcoq.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index cfbca6e6..57b1b560 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -18,6 +18,7 @@ open Datatypes open BinPos open BinInt +open Floats (* Integers *) @@ -116,6 +117,13 @@ let camlstring_of_coqstring (s: char list) = | c :: s -> r.[pos] <- c; fill (pos + 1) s in fill 0 s +(* Floats *) + +let coqfloat_of_camlfloat f = + Float.double_of_bits(coqint_of_camlint64(Int64.bits_of_float f)) +let camlfloat_of_coqfloat f = + Int64.float_of_bits(camlint64_of_coqint(Float.bits_of_double f)) + (* Timing facility *) (* |