From 5312915c1b29929f82e1f8de80609a277584913f Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 28 Jun 2012 07:59:03 +0000 Subject: Use Flocq for floats git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Camlcoq.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'lib/Camlcoq.ml') 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 *) (* -- cgit