source: extracted/compiler.mli @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 2.9 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77open Label
78
79open Sets
80
81open Listb
82
83open Star
84
85open Frontend_misc
86
87open CexecInd
88
89open CexecSound
90
91open Casts
92
93open ClassifyOp
94
95open Smallstep
96
97open Extra_bool
98
99open FrontEndVal
100
101open Hide
102
103open ByteValues
104
105open GenMem
106
107open FrontEndMem
108
109open Globalenvs
110
111open Csem
112
113open SmallstepExec
114
115open Division
116
117open Z
118
119open BitVectorZ
120
121open Pointers
122
123open Values
124
125open Events
126
127open IOMonad
128
129open IO
130
131open Cexec
132
133open TypeComparison
134
135open SimplifyCasts
136
137open MemProperties
138
139open MemoryInjections
140
141open Fresh
142
143open SwitchRemoval
144
145open FrontEndOps
146
147open Cminor_syntax
148
149open ToCminor
150
151open Initialisation
152
153open BitVectorTrie
154
155open Graphs
156
157open Order
158
159open Registers
160
161open RTLabs_syntax
162
163open ToRTLabs
164
165open Deqsets_extra
166
167open CostMisc
168
169open Listb_extra
170
171open CostSpec
172
173open CostCheck
174
175open Executions
176
177open StructuredTraces
178
179open RTLabs_semantics
180
181open RTLabs_abstract
182
183open RTLabs_traces
184
185open CostInj
186
187val front_end :
188  Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
189  Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res
190
191open State
192
193open Bind_new
194
195open BindLists
196
197open Blocks
198
199open TranslateUtils
200
201open AssocList
202
203open String
204
205open LabelledObjects
206
207open I8051
208
209open BackEndOps
210
211open Joint
212
213open RTL
214
215open RTLabsToRTL
216
217open ERTL
218
219open RegisterSet
220
221open RTLToERTL
222
223open ERTLptr
224
225open ERTLToERTLptr
226
227open Fixpoints
228
229open Set_adt
230
231open Liveness
232
233open Interference
234
235open Joint_LTL_LIN
236
237open LTL
238
239open ERTLptrToLTL
240
241open LIN
242
243open Linearise
244
245open LTLToLIN
246
247open ASM
248
249open BitVectorTrieSet
250
251open LINToASM
252
253val compute_fixpoint : Fixpoints.fixpoint_computer
254
255val colour_graph : Interference.coloured_graph_computer
256
257val back_end :
258  RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program Errors.res
259
260open Assembly
261
262open Status
263
264open Fetch
265
266open PolicyFront
267
268open PolicyStep
269
270open Policy
271
272val assembler :
273  ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res
274
275open AbstractStatus
276
277open StatusProofs
278
279open Interpret
280
281open ASMCosts
282
283val lift_cost_map_back_to_front :
284  Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
285  CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
286  StructuredTraces.as_cost_map -> Label.clight_cost_map
287
288open UtilBranch
289
290open ASMCostsSplit
291
292val compile :
293  Csyntax.clight_program -> (ASM.labelled_object_code,
294  (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
295  Errors.res
296
Note: See TracBrowser for help on using the repository browser.