source: extracted/toCminor.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: 15.0 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open Coqlib
8
9open Proper
10
11open PositiveMap
12
13open Deqsets
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Setoids
24
25open Monad
26
27open Option
28
29open Lists
30
31open Positive
32
33open Identifiers
34
35open Exp
36
37open Arithmetic
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open AST
76
77open Csyntax
78
79open TypeComparison
80
81open ClassifyOp
82
83open Fresh
84
85val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set
86
87val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set
88
89val gather_mem_vars_ls :
90  Csyntax.labeled_statements -> Identifiers.identifier_set
91
92val gather_mem_vars_stmt : Csyntax.statement -> Identifiers.identifier_set
93
94type var_type =
95| Global of AST.region
96| Stack of Nat.nat
97| Local
98
99val var_type_rect_Type4 :
100  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
101
102val var_type_rect_Type5 :
103  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
104
105val var_type_rect_Type3 :
106  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
107
108val var_type_rect_Type2 :
109  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
110
111val var_type_rect_Type1 :
112  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
113
114val var_type_rect_Type0 :
115  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
116
117val var_type_inv_rect_Type4 :
118  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
119  'a1) -> 'a1
120
121val var_type_inv_rect_Type3 :
122  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
123  'a1) -> 'a1
124
125val var_type_inv_rect_Type2 :
126  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
127  'a1) -> 'a1
128
129val var_type_inv_rect_Type1 :
130  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
131  'a1) -> 'a1
132
133val var_type_inv_rect_Type0 :
134  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
135  'a1) -> 'a1
136
137val var_type_discr : var_type -> var_type -> __
138
139val var_type_jmdiscr : var_type -> var_type -> __
140
141type var_types =
142  (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map
143
144val lookup' :
145  var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0)
146  Types.prod Errors.res
147
148val always_alloc : Csyntax.type0 -> Bool.bool
149
150val characterise_vars :
151  ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list ->
152  Csyntax.function0 -> (var_types, Nat.nat) Types.prod
153
154open FrontEndVal
155
156open Hide
157
158open ByteValues
159
160open GenMem
161
162open FrontEndMem
163
164open Division
165
166open Z
167
168open BitVectorZ
169
170open Pointers
171
172open Values
173
174open FrontEndOps
175
176open Cminor_syntax
177
178val type_should_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res
179
180val region_should_eq : AST.region -> AST.region -> 'a1 -> 'a1 Errors.res
181
182val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res
183
184val translate_unop :
185  AST.typ -> AST.typ -> Csyntax.unary_operation ->
186  FrontEndOps.unary_operation Errors.res
187
188val fix_ptr_type :
189  Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
190  Cminor_syntax.expr
191
192val translate_add :
193  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
194  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
195
196val translate_sub :
197  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
198  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
199
200val translate_mul :
201  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
202  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
203
204val translate_div :
205  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
206  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
207
208val translate_mod :
209  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
210  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
211
212val translate_shr :
213  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
214  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
215
216val complete_cmp :
217  Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
218
219val translate_cmp :
220  Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 ->
221  Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
222
223val translate_misc_aop :
224  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize ->
225  AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr ->
226  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
227
228val translate_binop :
229  Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr ->
230  Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 -> Cminor_syntax.expr
231  Errors.res
232
233val translate_cast :
234  Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 ->
235  Cminor_syntax.expr Types.sig0 Errors.res
236
237val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr
238
239val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr
240
241val translate_addr :
242  var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res
243
244val translate_expr :
245  var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res
246
247type destination =
248| IdDest of AST.ident * Csyntax.type0
249| MemDest of Cminor_syntax.expr Types.sig0
250
251val destination_rect_Type4 :
252  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
253  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
254
255val destination_rect_Type5 :
256  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
257  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
258
259val destination_rect_Type3 :
260  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
261  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
262
263val destination_rect_Type2 :
264  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
265  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
266
267val destination_rect_Type1 :
268  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
269  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
270
271val destination_rect_Type0 :
272  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
273  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
274
275val destination_inv_rect_Type4 :
276  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
277  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
278
279val destination_inv_rect_Type3 :
280  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
281  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
282
283val destination_inv_rect_Type2 :
284  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
285  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
286
287val destination_inv_rect_Type1 :
288  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
289  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
290
291val destination_inv_rect_Type0 :
292  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
293  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
294
295val destination_discr : var_types -> destination -> destination -> __
296
297val destination_jmdiscr : var_types -> destination -> destination -> __
298
299val translate_dest : var_types -> Csyntax.expr -> __
300
301type lenv = PreIdentifiers.identifier Identifiers.identifier_map
302
303val lookup_label :
304  lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res
305
306type fresh_list_for_univ = __
307
308type labgen = { labuniverse : Identifiers.universe;
309                label_genlist : PreIdentifiers.identifier List.list }
310
311val labgen_rect_Type4 :
312  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
313  -> labgen -> 'a1
314
315val labgen_rect_Type5 :
316  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
317  -> labgen -> 'a1
318
319val labgen_rect_Type3 :
320  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
321  -> labgen -> 'a1
322
323val labgen_rect_Type2 :
324  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
325  -> labgen -> 'a1
326
327val labgen_rect_Type1 :
328  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
329  -> labgen -> 'a1
330
331val labgen_rect_Type0 :
332  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
333  -> labgen -> 'a1
334
335val labuniverse : labgen -> Identifiers.universe
336
337val label_genlist : labgen -> PreIdentifiers.identifier List.list
338
339val labgen_inv_rect_Type4 :
340  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
341  __ -> __ -> 'a1) -> 'a1
342
343val labgen_inv_rect_Type3 :
344  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
345  __ -> __ -> 'a1) -> 'a1
346
347val labgen_inv_rect_Type2 :
348  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
349  __ -> __ -> 'a1) -> 'a1
350
351val labgen_inv_rect_Type1 :
352  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
353  __ -> __ -> 'a1) -> 'a1
354
355val labgen_inv_rect_Type0 :
356  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
357  __ -> __ -> 'a1) -> 'a1
358
359val labgen_discr : labgen -> labgen -> __
360
361val labgen_jmdiscr : labgen -> labgen -> __
362
363val generate_fresh_label :
364  labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0
365
366val labels_defined_switch : Csyntax.labeled_statements -> AST.ident List.list
367
368val labels_defined : Csyntax.statement -> AST.ident List.list
369
370val m_option_map :
371  ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option Errors.res
372
373val translate_expr_sigma :
374  var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
375  Types.sig0 Errors.res
376
377val add_tmps :
378  var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types
379
380type tmpgen = { tmp_universe : Identifiers.universe;
381                tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list }
382
383val tmpgen_rect_Type4 :
384  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
385  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
386
387val tmpgen_rect_Type5 :
388  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
389  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
390
391val tmpgen_rect_Type3 :
392  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
393  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
394
395val tmpgen_rect_Type2 :
396  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
397  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
398
399val tmpgen_rect_Type1 :
400  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
401  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
402
403val tmpgen_rect_Type0 :
404  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
405  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
406
407val tmp_universe : var_types -> tmpgen -> Identifiers.universe
408
409val tmp_env :
410  var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list
411
412val tmpgen_inv_rect_Type4 :
413  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
414  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
415
416val tmpgen_inv_rect_Type3 :
417  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
418  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
419
420val tmpgen_inv_rect_Type2 :
421  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
422  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
423
424val tmpgen_inv_rect_Type1 :
425  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
426  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
427
428val tmpgen_inv_rect_Type0 :
429  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
430  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
431
432val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __
433
434val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __
435
436val alloc_tmp :
437  var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod
438
439val mklabels :
440  labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier)
441  Types.prod, labgen) Types.prod
442
443type convert_flag =
444| DoNotConvert
445| ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier
446
447val convert_flag_rect_Type4 :
448  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
449  convert_flag -> 'a1
450
451val convert_flag_rect_Type5 :
452  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
453  convert_flag -> 'a1
454
455val convert_flag_rect_Type3 :
456  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
457  convert_flag -> 'a1
458
459val convert_flag_rect_Type2 :
460  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
461  convert_flag -> 'a1
462
463val convert_flag_rect_Type1 :
464  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
465  convert_flag -> 'a1
466
467val convert_flag_rect_Type0 :
468  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
469  convert_flag -> 'a1
470
471val convert_flag_inv_rect_Type4 :
472  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
473  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
474
475val convert_flag_inv_rect_Type3 :
476  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
477  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
478
479val convert_flag_inv_rect_Type2 :
480  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
481  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
482
483val convert_flag_inv_rect_Type1 :
484  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
485  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
486
487val convert_flag_inv_rect_Type0 :
488  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
489  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
490
491val convert_flag_discr : convert_flag -> convert_flag -> __
492
493val convert_flag_jmdiscr : convert_flag -> convert_flag -> __
494
495val labels_of_flag : convert_flag -> PreIdentifiers.identifier List.list
496
497val translate_statement :
498  var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ
499  Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
500  Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res
501
502val alloc_params :
503  var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
504  Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
505  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
506  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
507  Errors.res
508
509val populate_lenv :
510  AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
511  Types.prod Errors.res
512
513val build_label_env :
514  Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res
515
516val translate_function :
517  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
518  Types.prod List.list -> Csyntax.function0 ->
519  Cminor_syntax.internal_function Errors.res
520
521val translate_fundef :
522  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
523  Types.prod List.list -> Csyntax.clight_fundef ->
524  Cminor_syntax.internal_function AST.fundef Errors.res
525
526val map_partial_All :
527  ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list Errors.res
528
529val clight_to_cminor :
530  Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res
531
Note: See TracBrowser for help on using the repository browser.