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 /extraction | |
| parent | f3250c32ff42ae18fd03a5311c1f0caec3415aba (diff) | |
Use Flocq for floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 28 |
1 files changed, 7 insertions, 21 deletions
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. |