blob: 81cf53b961d41b16d77fcf94576e4db576a08524 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
Require Wfsimpl.
Require Iteration.
Require Floats.
Require RTLgen.
Require Inlining.
Require Constprop.
Require Coloring.
Require Allocation.
Require Compiler.
Require Initializers.
(* Standard lib *)
Require Import ExtrOcamlBasic.
Require Import ExtrOcamlString.
(* Wfsimpl *)
Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm.
(* Memdata *)
Extract Constant Memdata.big_endian => "Memdataaux.big_endian".
(* Memory - work around an extraction bug. *)
Extraction NoInline Memory.Mem.valid_pointer.
(* Errors *)
Extraction Inline Errors.bind Errors.bind2.
(* Iteration *)
Extract Constant Iteration.GenIter.iterate =>
"let rec iter f a =
match f a with Coq_inl b -> Some b | Coq_inr a' -> iter f a'
in iter".
(* RTLgen *)
Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch".
Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely".
Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2.
(* Inlining *)
Extract Inlined Constant Inlining.should_inline => "Inliningaux.should_inline".
Extraction Inline Inlining.ret Inlining.bind.
(* RTLtyping *)
Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_environment".
(* Constprop *)
Extract Constant ConstpropOp.propagate_float_constants =>
"fun _ -> !Clflags.option_ffloatconstprop >= 1".
Extract Constant Constprop.generate_float_constants =>
"fun _ -> !Clflags.option_ffloatconstprop >= 2".
(* Coloring *)
Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring".
(* Linearize *)
Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
(* SimplExpr *)
Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2.
(* Compiler *)
Extract Constant Compiler.print_Clight => "PrintClight.print_if".
Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
Extract Constant Compiler.print_RTL => "PrintRTL.print_rtl".
Extract Constant Compiler.print_RTL_tailcall => "PrintRTL.print_tailcall".
Extract Constant Compiler.print_RTL_inline => "PrintRTL.print_inlining".
Extract Constant Compiler.print_RTL_constprop => "PrintRTL.print_constprop".
Extract Constant Compiler.print_RTL_cse => "PrintRTL.print_cse".
Extract Constant Compiler.print_LTLin => "PrintLTLin.print_if".
Extract Constant Compiler.print_Mach => "PrintMach.print_if".
Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
(*Extraction Inline Compiler.apply_total Compiler.apply_partial.*)
(* Processor-specific extraction directives *)
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.
|
