source: extracted/csyntax.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: 22.4 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open ErrorMessages
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Lists
24
25open Positive
26
27open Identifiers
28
29open Exp
30
31open Arithmetic
32
33open Vector
34
35open Div_and_mod
36
37open Jmeq
38
39open Russell
40
41open List
42
43open Util
44
45open FoldStuff
46
47open BitVector
48
49open Extranat
50
51open Bool
52
53open Relations
54
55open Nat
56
57open Integers
58
59open Hints_declaration
60
61open Core_notation
62
63open Pts
64
65open Logic
66
67open Types
68
69open AST
70
71open Coqlib
72
73open BitVectorTrie
74
75open CostLabel
76
77type type0 =
78| Tvoid
79| Tint of AST.intsize * AST.signedness
80| Tpointer of type0
81| Tarray of type0 * Nat.nat
82| Tfunction of typelist * type0
83| Tstruct of AST.ident * fieldlist
84| Tunion of AST.ident * fieldlist
85| Tcomp_ptr of AST.ident
86and typelist =
87| Tnil
88| Tcons of type0 * typelist
89and fieldlist =
90| Fnil
91| Fcons of AST.ident * type0 * fieldlist
92
93val type_inv_rect_Type4 :
94  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
95  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
96  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
97  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
98
99val type_inv_rect_Type3 :
100  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
101  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
102  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
103  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
104
105val type_inv_rect_Type2 :
106  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
107  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
108  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
109  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
110
111val type_inv_rect_Type1 :
112  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
113  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
114  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
115  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
116
117val type_inv_rect_Type0 :
118  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
119  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
120  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
121  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
122
123val typelist_inv_rect_Type4 :
124  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
125
126val typelist_inv_rect_Type3 :
127  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
128
129val typelist_inv_rect_Type2 :
130  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
131
132val typelist_inv_rect_Type1 :
133  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
134
135val typelist_inv_rect_Type0 :
136  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
137
138val fieldlist_inv_rect_Type4 :
139  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
140  -> 'a1
141
142val fieldlist_inv_rect_Type3 :
143  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
144  -> 'a1
145
146val fieldlist_inv_rect_Type2 :
147  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
148  -> 'a1
149
150val fieldlist_inv_rect_Type1 :
151  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
152  -> 'a1
153
154val fieldlist_inv_rect_Type0 :
155  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
156  -> 'a1
157
158val type_discr : type0 -> type0 -> __
159
160val typelist_discr : typelist -> typelist -> __
161
162val fieldlist_discr : fieldlist -> fieldlist -> __
163
164val type_jmdiscr : type0 -> type0 -> __
165
166val typelist_jmdiscr : typelist -> typelist -> __
167
168val fieldlist_jmdiscr : fieldlist -> fieldlist -> __
169
170type unary_operation =
171| Onotbool
172| Onotint
173| Oneg
174
175val unary_operation_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
176
177val unary_operation_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
178
179val unary_operation_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
180
181val unary_operation_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
182
183val unary_operation_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
184
185val unary_operation_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
186
187val unary_operation_inv_rect_Type4 :
188  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
189
190val unary_operation_inv_rect_Type3 :
191  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
192
193val unary_operation_inv_rect_Type2 :
194  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
195
196val unary_operation_inv_rect_Type1 :
197  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
198
199val unary_operation_inv_rect_Type0 :
200  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
201
202val unary_operation_discr : unary_operation -> unary_operation -> __
203
204val unary_operation_jmdiscr : unary_operation -> unary_operation -> __
205
206type binary_operation =
207| Oadd
208| Osub
209| Omul
210| Odiv
211| Omod
212| Oand
213| Oor
214| Oxor
215| Oshl
216| Oshr
217| Oeq
218| One0
219| Olt
220| Ogt
221| Ole
222| Oge
223
224val binary_operation_rect_Type4 :
225  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
226  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
227
228val binary_operation_rect_Type5 :
229  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
230  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
231
232val binary_operation_rect_Type3 :
233  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
234  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
235
236val binary_operation_rect_Type2 :
237  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
238  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
239
240val binary_operation_rect_Type1 :
241  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
242  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
243
244val binary_operation_rect_Type0 :
245  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
246  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
247
248val binary_operation_inv_rect_Type4 :
249  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
250  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
251  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
252  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
253
254val binary_operation_inv_rect_Type3 :
255  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
256  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
257  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
258  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
259
260val binary_operation_inv_rect_Type2 :
261  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
262  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
263  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
264  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
265
266val binary_operation_inv_rect_Type1 :
267  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
268  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
269  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
270  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
271
272val binary_operation_inv_rect_Type0 :
273  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
274  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
275  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
276  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
277
278val binary_operation_discr : binary_operation -> binary_operation -> __
279
280val binary_operation_jmdiscr : binary_operation -> binary_operation -> __
281
282type expr =
283| Expr of expr_descr * type0
284and expr_descr =
285| Econst_int of AST.intsize * AST.bvint
286| Evar of AST.ident
287| Ederef of expr
288| Eaddrof of expr
289| Eunop of unary_operation * expr
290| Ebinop of binary_operation * expr * expr
291| Ecast of type0 * expr
292| Econdition of expr * expr * expr
293| Eandbool of expr * expr
294| Eorbool of expr * expr
295| Esizeof of type0
296| Efield of expr * AST.ident
297| Ecost of CostLabel.costlabel * expr
298
299val expr_inv_rect_Type4 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
300
301val expr_inv_rect_Type3 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
302
303val expr_inv_rect_Type2 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
304
305val expr_inv_rect_Type1 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
306
307val expr_inv_rect_Type0 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
308
309val expr_descr_inv_rect_Type4 :
310  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
311  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
312  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
313  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
314  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
315  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
316  -> __ -> 'a1) -> 'a1
317
318val expr_descr_inv_rect_Type3 :
319  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
320  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
321  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
322  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
323  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
324  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
325  -> __ -> 'a1) -> 'a1
326
327val expr_descr_inv_rect_Type2 :
328  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
329  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
330  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
331  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
332  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
333  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
334  -> __ -> 'a1) -> 'a1
335
336val expr_descr_inv_rect_Type1 :
337  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
338  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
339  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
340  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
341  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
342  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
343  -> __ -> 'a1) -> 'a1
344
345val expr_descr_inv_rect_Type0 :
346  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
347  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
348  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
349  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
350  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
351  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
352  -> __ -> 'a1) -> 'a1
353
354val expr_discr : expr -> expr -> __
355
356val expr_descr_discr : expr_descr -> expr_descr -> __
357
358val expr_jmdiscr : expr -> expr -> __
359
360val expr_descr_jmdiscr : expr_descr -> expr_descr -> __
361
362val typeof : expr -> type0
363
364type label = AST.ident
365
366type statement =
367| Sskip
368| Sassign of expr * expr
369| Scall of expr Types.option * expr * expr List.list
370| Ssequence of statement * statement
371| Sifthenelse of expr * statement * statement
372| Swhile of expr * statement
373| Sdowhile of expr * statement
374| Sfor of statement * expr * statement * statement
375| Sbreak
376| Scontinue
377| Sreturn of expr Types.option
378| Sswitch of expr * labeled_statements
379| Slabel of label * statement
380| Sgoto of label
381| Scost of CostLabel.costlabel * statement
382and labeled_statements =
383| LSdefault of statement
384| LScase of AST.intsize * AST.bvint * statement * labeled_statements
385
386val statement_inv_rect_Type4 :
387  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
388  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
389  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
390  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
391  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
392  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
393  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
394  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
395  'a1
396
397val statement_inv_rect_Type3 :
398  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
399  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
400  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
401  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
402  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
403  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
404  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
405  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
406  'a1
407
408val statement_inv_rect_Type2 :
409  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
410  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
411  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
412  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
413  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
414  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
415  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
416  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
417  'a1
418
419val statement_inv_rect_Type1 :
420  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
421  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
422  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
423  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
424  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
425  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
426  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
427  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
428  'a1
429
430val statement_inv_rect_Type0 :
431  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
432  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
433  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
434  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
435  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
436  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
437  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
438  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
439  'a1
440
441val labeled_statements_inv_rect_Type4 :
442  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
443  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
444
445val labeled_statements_inv_rect_Type3 :
446  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
447  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
448
449val labeled_statements_inv_rect_Type2 :
450  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
451  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
452
453val labeled_statements_inv_rect_Type1 :
454  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
455  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
456
457val labeled_statements_inv_rect_Type0 :
458  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
459  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
460
461val statement_discr : statement -> statement -> __
462
463val labeled_statements_discr : labeled_statements -> labeled_statements -> __
464
465val statement_jmdiscr : statement -> statement -> __
466
467val labeled_statements_jmdiscr :
468  labeled_statements -> labeled_statements -> __
469
470type function0 = { fn_return : type0;
471                   fn_params : (AST.ident, type0) Types.prod List.list;
472                   fn_vars : (AST.ident, type0) Types.prod List.list;
473                   fn_body : statement }
474
475val function_rect_Type4 :
476  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
477  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
478
479val function_rect_Type5 :
480  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
481  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
482
483val function_rect_Type3 :
484  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
485  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
486
487val function_rect_Type2 :
488  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
489  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
490
491val function_rect_Type1 :
492  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
493  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
494
495val function_rect_Type0 :
496  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
497  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
498
499val fn_return : function0 -> type0
500
501val fn_params : function0 -> (AST.ident, type0) Types.prod List.list
502
503val fn_vars : function0 -> (AST.ident, type0) Types.prod List.list
504
505val fn_body : function0 -> statement
506
507val function_inv_rect_Type4 :
508  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
509  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
510
511val function_inv_rect_Type3 :
512  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
513  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
514
515val function_inv_rect_Type2 :
516  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
517  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
518
519val function_inv_rect_Type1 :
520  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
521  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
522
523val function_inv_rect_Type0 :
524  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
525  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
526
527val function_discr : function0 -> function0 -> __
528
529val function_jmdiscr : function0 -> function0 -> __
530
531type clight_fundef =
532| CL_Internal of function0
533| CL_External of AST.ident * typelist * type0
534
535val clight_fundef_rect_Type4 :
536  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
537  clight_fundef -> 'a1
538
539val clight_fundef_rect_Type5 :
540  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
541  clight_fundef -> 'a1
542
543val clight_fundef_rect_Type3 :
544  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
545  clight_fundef -> 'a1
546
547val clight_fundef_rect_Type2 :
548  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
549  clight_fundef -> 'a1
550
551val clight_fundef_rect_Type1 :
552  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
553  clight_fundef -> 'a1
554
555val clight_fundef_rect_Type0 :
556  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
557  clight_fundef -> 'a1
558
559val clight_fundef_inv_rect_Type4 :
560  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
561  type0 -> __ -> 'a1) -> 'a1
562
563val clight_fundef_inv_rect_Type3 :
564  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
565  type0 -> __ -> 'a1) -> 'a1
566
567val clight_fundef_inv_rect_Type2 :
568  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
569  type0 -> __ -> 'a1) -> 'a1
570
571val clight_fundef_inv_rect_Type1 :
572  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
573  type0 -> __ -> 'a1) -> 'a1
574
575val clight_fundef_inv_rect_Type0 :
576  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
577  type0 -> __ -> 'a1) -> 'a1
578
579val clight_fundef_discr : clight_fundef -> clight_fundef -> __
580
581val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __
582
583type clight_program =
584  (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program
585
586val type_of_params : (AST.ident, type0) Types.prod List.list -> typelist
587
588val type_of_function : function0 -> type0
589
590val type_of_fundef : clight_fundef -> type0
591
592val alignof_fields : fieldlist -> Nat.nat
593
594val alignof : type0 -> Nat.nat
595
596val sizeof_union : fieldlist -> Nat.nat
597
598val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat
599
600val sizeof : type0 -> Nat.nat
601
602val field_offset_rec :
603  AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res
604
605val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res
606
607val field_type : AST.ident -> fieldlist -> type0 Errors.res
608
609val typ_of_type : type0 -> AST.typ
610
611val opttyp_of_type : type0 -> AST.typ Types.option
612
613val typlist_of_typelist : typelist -> AST.typ List.list
614
615type mode =
616| By_value of AST.typ
617| By_reference
618| By_nothing of AST.typ
619
620val mode_rect_Type4 :
621  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
622
623val mode_rect_Type5 :
624  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
625
626val mode_rect_Type3 :
627  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
628
629val mode_rect_Type2 :
630  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
631
632val mode_rect_Type1 :
633  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
634
635val mode_rect_Type0 :
636  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
637
638val mode_inv_rect_Type4 :
639  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
640  (AST.typ -> __ -> __ -> 'a1) -> 'a1
641
642val mode_inv_rect_Type3 :
643  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
644  (AST.typ -> __ -> __ -> 'a1) -> 'a1
645
646val mode_inv_rect_Type2 :
647  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
648  (AST.typ -> __ -> __ -> 'a1) -> 'a1
649
650val mode_inv_rect_Type1 :
651  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
652  (AST.typ -> __ -> __ -> 'a1) -> 'a1
653
654val mode_inv_rect_Type0 :
655  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
656  (AST.typ -> __ -> __ -> 'a1) -> 'a1
657
658val mode_discr : AST.typ -> mode -> mode -> __
659
660val mode_jmdiscr : AST.typ -> mode -> mode -> __
661
662val access_mode : type0 -> mode
663
664val signature_of_type : typelist -> type0 -> AST.signature
665
666val external_function0 :
667  AST.ident -> typelist -> type0 -> AST.external_function
668
Note: See TracBrowser for help on using the repository browser.