source: extracted/switchRemoval.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 7.5 KB
Line 
1open Preamble
2
3open Deqsets
4
5open Sets
6
7open Bool
8
9open Relations
10
11open Nat
12
13open Hints_declaration
14
15open Core_notation
16
17open Pts
18
19open Logic
20
21open Types
22
23open List
24
25open Listb
26
27open Proper
28
29open PositiveMap
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Div_and_mod
46
47open Jmeq
48
49open Russell
50
51open Util
52
53open Lists
54
55open Positive
56
57open Identifiers
58
59open BitVectorTrie
60
61open CostLabel
62
63open Coqlib
64
65open Exp
66
67open Arithmetic
68
69open Vector
70
71open FoldStuff
72
73open BitVector
74
75open Extranat
76
77open Integers
78
79open AST
80
81open Csyntax
82
83open Fresh
84
85open CexecInd
86
87open SmallstepExec
88
89open Cexec
90
91open IO
92
93open IOMonad
94
95open Star
96
97open ClassifyOp
98
99open Events
100
101open Smallstep
102
103open Extra_bool
104
105open Values
106
107open FrontEndVal
108
109open Hide
110
111open ByteValues
112
113open Division
114
115open Z
116
117open BitVectorZ
118
119open Pointers
120
121open GenMem
122
123open FrontEndMem
124
125open Globalenvs
126
127open Csem
128
129open TypeComparison
130
131open Frontend_misc
132
133open MemProperties
134
135open MemoryInjections
136
137type switch_free = __
138
139type branches_switch_free = __
140
141val convert_break_to_goto :
142  Csyntax.statement -> Csyntax.label -> Csyntax.statement
143
144val produce_cond :
145  Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
146  Csyntax.label -> ((Csyntax.statement, Csyntax.label) Types.prod,
147  Identifiers.universe) Types.prod
148
149val simplify_switch :
150  Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
151  (Csyntax.statement, Identifiers.universe) Types.prod
152
153val switch_removal_branches :
154  Csyntax.labeled_statements -> Identifiers.universe ->
155  ((Csyntax.labeled_statements, (AST.ident, Csyntax.type0) Types.prod
156  List.list) Types.prod, Identifiers.universe) Types.prod
157
158val switch_removal :
159  Csyntax.statement -> Identifiers.universe -> ((Csyntax.statement,
160  (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
161  Identifiers.universe) Types.prod
162
163val ret_st :
164  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
165  Identifiers.universe) Types.prod -> 'a1
166
167val ret_vars :
168  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
169  Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
170  List.list
171
172val ret_u :
173  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
174  Identifiers.universe) Types.prod -> Identifiers.universe
175
176val least_identifier : PreIdentifiers.identifier
177
178val max_of_expr : Csyntax.expr -> AST.ident
179
180val max_of_ls : Csyntax.labeled_statements -> AST.ident
181
182val max_of_statement : Csyntax.statement -> AST.ident
183
184val max_id_of_function : Csyntax.function0 -> AST.ident
185
186val function_switch_removal :
187  Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
188  Types.prod List.list) Types.prod
189
190val fundef_switch_removal : Csyntax.clight_fundef -> Csyntax.clight_fundef
191
192val program_switch_removal : Csyntax.clight_program -> Csyntax.clight_program
193
194type substatement_ls = __
195
196type substatement_P = __
197
198val nonempty_block_rect_Type4 :
199  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
200
201val nonempty_block_rect_Type5 :
202  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
203
204val nonempty_block_rect_Type3 :
205  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
206
207val nonempty_block_rect_Type2 :
208  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
209
210val nonempty_block_rect_Type1 :
211  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
212
213val nonempty_block_rect_Type0 :
214  GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
215
216val nonempty_block_inv_rect_Type4 :
217  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
218
219val nonempty_block_inv_rect_Type3 :
220  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
221
222val nonempty_block_inv_rect_Type2 :
223  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
224
225val nonempty_block_inv_rect_Type1 :
226  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
227
228val nonempty_block_inv_rect_Type0 :
229  GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
230
231val nonempty_block_discr : GenMem.mem1 -> Pointers.block -> __
232
233val nonempty_block_jmdiscr : GenMem.mem1 -> Pointers.block -> __
234
235val sr_memext_rect_Type4 :
236  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
237  -> 'a1) -> 'a1
238
239val sr_memext_rect_Type5 :
240  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
241  -> 'a1) -> 'a1
242
243val sr_memext_rect_Type3 :
244  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
245  -> 'a1) -> 'a1
246
247val sr_memext_rect_Type2 :
248  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
249  -> 'a1) -> 'a1
250
251val sr_memext_rect_Type1 :
252  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
253  -> 'a1) -> 'a1
254
255val sr_memext_rect_Type0 :
256  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
257  -> 'a1) -> 'a1
258
259val sr_memext_inv_rect_Type4 :
260  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
261  -> __ -> 'a1) -> 'a1
262
263val sr_memext_inv_rect_Type3 :
264  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
265  -> __ -> 'a1) -> 'a1
266
267val sr_memext_inv_rect_Type2 :
268  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
269  -> __ -> 'a1) -> 'a1
270
271val sr_memext_inv_rect_Type1 :
272  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
273  -> __ -> 'a1) -> 'a1
274
275val sr_memext_inv_rect_Type0 :
276  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
277  -> __ -> 'a1) -> 'a1
278
279val sr_memext_discr :
280  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __
281
282val sr_memext_jmdiscr :
283  GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __
284
285val env_codomain :
286  Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
287  Pointers.block Frontend_misc.lset
288
289val switch_removal_globals_rect_Type4 :
290  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
291  -> __ -> 'a2) -> 'a2
292
293val switch_removal_globals_rect_Type5 :
294  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
295  -> __ -> 'a2) -> 'a2
296
297val switch_removal_globals_rect_Type3 :
298  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
299  -> __ -> 'a2) -> 'a2
300
301val switch_removal_globals_rect_Type2 :
302  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
303  -> __ -> 'a2) -> 'a2
304
305val switch_removal_globals_rect_Type1 :
306  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
307  -> __ -> 'a2) -> 'a2
308
309val switch_removal_globals_rect_Type0 :
310  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
311  -> __ -> 'a2) -> 'a2
312
313val switch_removal_globals_inv_rect_Type4 :
314  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
315  -> __ -> __ -> 'a2) -> 'a2
316
317val switch_removal_globals_inv_rect_Type3 :
318  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
319  -> __ -> __ -> 'a2) -> 'a2
320
321val switch_removal_globals_inv_rect_Type2 :
322  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
323  -> __ -> __ -> 'a2) -> 'a2
324
325val switch_removal_globals_inv_rect_Type1 :
326  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
327  -> __ -> __ -> 'a2) -> 'a2
328
329val switch_removal_globals_inv_rect_Type0 :
330  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
331  -> __ -> __ -> 'a2) -> 'a2
332
333val switch_removal_globals_discr :
334  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
335
336val switch_removal_globals_jmdiscr :
337  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
338
Note: See TracBrowser for help on using the repository browser.