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 --- extraction/extraction.v | 28 +++++++--------------------- 1 file changed, 7 insertions(+), 21 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 1156d04..81cf53b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -28,27 +28,6 @@ Require Import ExtrOcamlString. (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. -(* Float *) -Extract Inlined Constant Floats.float => "float". -Extract Constant Floats.Float.zero => "0.". -Extract Constant Floats.Float.neg => "( ~-. )". -Extract Constant Floats.Float.abs => "abs_float". -Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat". -Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat". -Extract Constant Floats.Float.intuoffloat => "Floataux.intuoffloat". -Extract Constant Floats.Float.floatofint => "Floataux.floatofint". -Extract Constant Floats.Float.floatofintu => "Floataux.floatofintu". -Extract Constant Floats.Float.add => "( +. )". -Extract Constant Floats.Float.sub => "( -. )". -Extract Constant Floats.Float.mul => "( *. )". -Extract Constant Floats.Float.div => "( /. )". -Extract Constant Floats.Float.cmp => "Floataux.cmp". -Extract Constant Floats.Float.eq_dec => "fun (x: float) (y: float) -> x = y". -Extract Constant Floats.Float.bits_of_double => "Floataux.bits_of_double". -Extract Constant Floats.Float.double_of_bits => "Floataux.double_of_bits". -Extract Constant Floats.Float.bits_of_single => "Floataux.bits_of_single". -Extract Constant Floats.Float.single_of_bits => "Floataux.single_of_bits". - (* Memdata *) Extract Constant Memdata.big_endian => "Memdataaux.big_endian". @@ -112,6 +91,13 @@ Load extractionMachdep. (* Avoid name clashes *) Extraction Blacklist List String Int. +(* Cutting the dependancy to R. *) +Extract Inlined Constant Fcore_defs.F2R => "fun _ -> assert false". +Extract Inlined Constant Fappli_IEEE.FF2R => "fun _ -> assert false". +Extract Inlined Constant Fappli_IEEE.B2R => "fun _ -> assert false". +Extract Inlined Constant Fappli_IEEE.round_mode => "fun _ -> assert false". +Extract Inlined Constant Fcalc_bracket.inbetween_loc => "fun _ -> assert false". + (* Go! *) Cd "extraction". Recursive Extraction Library Compiler. -- cgit v1.2.3