source: extracted/csyntax.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 8 years ago

...

File size: 56.6 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 Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Jmeq
36
37open Russell
38
39open List
40
41open Util
42
43open FoldStuff
44
45open BitVector
46
47open Extranat
48
49open Bool
50
51open Relations
52
53open Nat
54
55open Integers
56
57open Hints_declaration
58
59open Core_notation
60
61open Pts
62
63open Logic
64
65open Types
66
67open AST
68
69open Coqlib
70
71open CostLabel
72
73type type0 =
74| Tvoid
75| Tint of AST.intsize * AST.signedness
76| Tpointer of type0
77| Tarray of type0 * Nat.nat
78| Tfunction of typelist * type0
79| Tstruct of AST.ident * fieldlist
80| Tunion of AST.ident * fieldlist
81| Tcomp_ptr of AST.ident
82and typelist =
83| Tnil
84| Tcons of type0 * typelist
85and fieldlist =
86| Fnil
87| Fcons of AST.ident * type0 * fieldlist
88
89(** val type_inv_rect_Type4 :
90    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
91    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
92    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
93    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
94let type_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
95  let hcut =
96    match hterm with
97    | Tvoid -> h1
98    | Tint (x, x0) -> h2 x x0
99    | Tpointer x -> h3 x
100    | Tarray (x, x0) -> h4 x x0
101    | Tfunction (x, x0) -> h5 x x0
102    | Tstruct (x, x0) -> h6 x x0
103    | Tunion (x, x0) -> h7 x x0
104    | Tcomp_ptr x -> h8 x
105  in
106  hcut __
107
108(** val type_inv_rect_Type3 :
109    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
110    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
111    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
112    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
113let type_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
114  let hcut =
115    match hterm with
116    | Tvoid -> h1
117    | Tint (x, x0) -> h2 x x0
118    | Tpointer x -> h3 x
119    | Tarray (x, x0) -> h4 x x0
120    | Tfunction (x, x0) -> h5 x x0
121    | Tstruct (x, x0) -> h6 x x0
122    | Tunion (x, x0) -> h7 x x0
123    | Tcomp_ptr x -> h8 x
124  in
125  hcut __
126
127(** val type_inv_rect_Type2 :
128    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
129    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
130    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
131    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
132let type_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
133  let hcut =
134    match hterm with
135    | Tvoid -> h1
136    | Tint (x, x0) -> h2 x x0
137    | Tpointer x -> h3 x
138    | Tarray (x, x0) -> h4 x x0
139    | Tfunction (x, x0) -> h5 x x0
140    | Tstruct (x, x0) -> h6 x x0
141    | Tunion (x, x0) -> h7 x x0
142    | Tcomp_ptr x -> h8 x
143  in
144  hcut __
145
146(** val type_inv_rect_Type1 :
147    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
148    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
149    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
150    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
151let type_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
152  let hcut =
153    match hterm with
154    | Tvoid -> h1
155    | Tint (x, x0) -> h2 x x0
156    | Tpointer x -> h3 x
157    | Tarray (x, x0) -> h4 x x0
158    | Tfunction (x, x0) -> h5 x x0
159    | Tstruct (x, x0) -> h6 x x0
160    | Tunion (x, x0) -> h7 x x0
161    | Tcomp_ptr x -> h8 x
162  in
163  hcut __
164
165(** val type_inv_rect_Type0 :
166    type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
167    (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
168    type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
169    (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
170let type_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
171  let hcut =
172    match hterm with
173    | Tvoid -> h1
174    | Tint (x, x0) -> h2 x x0
175    | Tpointer x -> h3 x
176    | Tarray (x, x0) -> h4 x x0
177    | Tfunction (x, x0) -> h5 x x0
178    | Tstruct (x, x0) -> h6 x x0
179    | Tunion (x, x0) -> h7 x x0
180    | Tcomp_ptr x -> h8 x
181  in
182  hcut __
183
184(** val typelist_inv_rect_Type4 :
185    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
186let typelist_inv_rect_Type4 hterm h1 h2 =
187  let hcut =
188    match hterm with
189    | Tnil -> h1
190    | Tcons (x, x0) -> h2 x x0
191  in
192  hcut __
193
194(** val typelist_inv_rect_Type3 :
195    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
196let typelist_inv_rect_Type3 hterm h1 h2 =
197  let hcut =
198    match hterm with
199    | Tnil -> h1
200    | Tcons (x, x0) -> h2 x x0
201  in
202  hcut __
203
204(** val typelist_inv_rect_Type2 :
205    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
206let typelist_inv_rect_Type2 hterm h1 h2 =
207  let hcut =
208    match hterm with
209    | Tnil -> h1
210    | Tcons (x, x0) -> h2 x x0
211  in
212  hcut __
213
214(** val typelist_inv_rect_Type1 :
215    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
216let typelist_inv_rect_Type1 hterm h1 h2 =
217  let hcut =
218    match hterm with
219    | Tnil -> h1
220    | Tcons (x, x0) -> h2 x x0
221  in
222  hcut __
223
224(** val typelist_inv_rect_Type0 :
225    typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
226let typelist_inv_rect_Type0 hterm h1 h2 =
227  let hcut =
228    match hterm with
229    | Tnil -> h1
230    | Tcons (x, x0) -> h2 x x0
231  in
232  hcut __
233
234(** val fieldlist_inv_rect_Type4 :
235    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
236    'a1) -> 'a1 **)
237let fieldlist_inv_rect_Type4 hterm h1 h2 =
238  let hcut =
239    match hterm with
240    | Fnil -> h1
241    | Fcons (x, x0, x1) -> h2 x x0 x1
242  in
243  hcut __
244
245(** val fieldlist_inv_rect_Type3 :
246    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
247    'a1) -> 'a1 **)
248let fieldlist_inv_rect_Type3 hterm h1 h2 =
249  let hcut =
250    match hterm with
251    | Fnil -> h1
252    | Fcons (x, x0, x1) -> h2 x x0 x1
253  in
254  hcut __
255
256(** val fieldlist_inv_rect_Type2 :
257    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
258    'a1) -> 'a1 **)
259let fieldlist_inv_rect_Type2 hterm h1 h2 =
260  let hcut =
261    match hterm with
262    | Fnil -> h1
263    | Fcons (x, x0, x1) -> h2 x x0 x1
264  in
265  hcut __
266
267(** val fieldlist_inv_rect_Type1 :
268    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
269    'a1) -> 'a1 **)
270let fieldlist_inv_rect_Type1 hterm h1 h2 =
271  let hcut =
272    match hterm with
273    | Fnil -> h1
274    | Fcons (x, x0, x1) -> h2 x x0 x1
275  in
276  hcut __
277
278(** val fieldlist_inv_rect_Type0 :
279    fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
280    'a1) -> 'a1 **)
281let fieldlist_inv_rect_Type0 hterm h1 h2 =
282  let hcut =
283    match hterm with
284    | Fnil -> h1
285    | Fcons (x, x0, x1) -> h2 x x0 x1
286  in
287  hcut __
288
289(** val type_discr : type0 -> type0 -> __ **)
290let type_discr x y =
291  Logic.eq_rect_Type2 x
292    (match x with
293     | Tvoid -> Obj.magic (fun _ dH -> dH)
294     | Tint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
295     | Tpointer a0 -> Obj.magic (fun _ dH -> dH __)
296     | Tarray (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
297     | Tfunction (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
298     | Tstruct (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
299     | Tunion (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
300     | Tcomp_ptr a0 -> Obj.magic (fun _ dH -> dH __)) y
301
302(** val typelist_discr : typelist -> typelist -> __ **)
303let typelist_discr x y =
304  Logic.eq_rect_Type2 x
305    (match x with
306     | Tnil -> Obj.magic (fun _ dH -> dH)
307     | Tcons (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
308
309(** val fieldlist_discr : fieldlist -> fieldlist -> __ **)
310let fieldlist_discr x y =
311  Logic.eq_rect_Type2 x
312    (match x with
313     | Fnil -> Obj.magic (fun _ dH -> dH)
314     | Fcons (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
315
316(** val type_jmdiscr : type0 -> type0 -> __ **)
317let type_jmdiscr x y =
318  Logic.eq_rect_Type2 x
319    (match x with
320     | Tvoid -> Obj.magic (fun _ dH -> dH)
321     | Tint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
322     | Tpointer a0 -> Obj.magic (fun _ dH -> dH __)
323     | Tarray (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
324     | Tfunction (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
325     | Tstruct (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
326     | Tunion (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
327     | Tcomp_ptr a0 -> Obj.magic (fun _ dH -> dH __)) y
328
329(** val typelist_jmdiscr : typelist -> typelist -> __ **)
330let typelist_jmdiscr x y =
331  Logic.eq_rect_Type2 x
332    (match x with
333     | Tnil -> Obj.magic (fun _ dH -> dH)
334     | Tcons (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
335
336(** val fieldlist_jmdiscr : fieldlist -> fieldlist -> __ **)
337let fieldlist_jmdiscr x y =
338  Logic.eq_rect_Type2 x
339    (match x with
340     | Fnil -> Obj.magic (fun _ dH -> dH)
341     | Fcons (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
342
343type unary_operation =
344| Onotbool
345| Onotint
346| Oneg
347
348(** val unary_operation_rect_Type4 :
349    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
350let rec unary_operation_rect_Type4 h_Onotbool h_Onotint h_Oneg = function
351| Onotbool -> h_Onotbool
352| Onotint -> h_Onotint
353| Oneg -> h_Oneg
354
355(** val unary_operation_rect_Type5 :
356    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
357let rec unary_operation_rect_Type5 h_Onotbool h_Onotint h_Oneg = function
358| Onotbool -> h_Onotbool
359| Onotint -> h_Onotint
360| Oneg -> h_Oneg
361
362(** val unary_operation_rect_Type3 :
363    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
364let rec unary_operation_rect_Type3 h_Onotbool h_Onotint h_Oneg = function
365| Onotbool -> h_Onotbool
366| Onotint -> h_Onotint
367| Oneg -> h_Oneg
368
369(** val unary_operation_rect_Type2 :
370    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
371let rec unary_operation_rect_Type2 h_Onotbool h_Onotint h_Oneg = function
372| Onotbool -> h_Onotbool
373| Onotint -> h_Onotint
374| Oneg -> h_Oneg
375
376(** val unary_operation_rect_Type1 :
377    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
378let rec unary_operation_rect_Type1 h_Onotbool h_Onotint h_Oneg = function
379| Onotbool -> h_Onotbool
380| Onotint -> h_Onotint
381| Oneg -> h_Oneg
382
383(** val unary_operation_rect_Type0 :
384    'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
385let rec unary_operation_rect_Type0 h_Onotbool h_Onotint h_Oneg = function
386| Onotbool -> h_Onotbool
387| Onotint -> h_Onotint
388| Oneg -> h_Oneg
389
390(** val unary_operation_inv_rect_Type4 :
391    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
392let unary_operation_inv_rect_Type4 hterm h1 h2 h3 =
393  let hcut = unary_operation_rect_Type4 h1 h2 h3 hterm in hcut __
394
395(** val unary_operation_inv_rect_Type3 :
396    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
397let unary_operation_inv_rect_Type3 hterm h1 h2 h3 =
398  let hcut = unary_operation_rect_Type3 h1 h2 h3 hterm in hcut __
399
400(** val unary_operation_inv_rect_Type2 :
401    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
402let unary_operation_inv_rect_Type2 hterm h1 h2 h3 =
403  let hcut = unary_operation_rect_Type2 h1 h2 h3 hterm in hcut __
404
405(** val unary_operation_inv_rect_Type1 :
406    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
407let unary_operation_inv_rect_Type1 hterm h1 h2 h3 =
408  let hcut = unary_operation_rect_Type1 h1 h2 h3 hterm in hcut __
409
410(** val unary_operation_inv_rect_Type0 :
411    unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
412let unary_operation_inv_rect_Type0 hterm h1 h2 h3 =
413  let hcut = unary_operation_rect_Type0 h1 h2 h3 hterm in hcut __
414
415(** val unary_operation_discr : unary_operation -> unary_operation -> __ **)
416let unary_operation_discr x y =
417  Logic.eq_rect_Type2 x
418    (match x with
419     | Onotbool -> Obj.magic (fun _ dH -> dH)
420     | Onotint -> Obj.magic (fun _ dH -> dH)
421     | Oneg -> Obj.magic (fun _ dH -> dH)) y
422
423(** val unary_operation_jmdiscr :
424    unary_operation -> unary_operation -> __ **)
425let unary_operation_jmdiscr x y =
426  Logic.eq_rect_Type2 x
427    (match x with
428     | Onotbool -> Obj.magic (fun _ dH -> dH)
429     | Onotint -> Obj.magic (fun _ dH -> dH)
430     | Oneg -> Obj.magic (fun _ dH -> dH)) y
431
432type binary_operation =
433| Oadd
434| Osub
435| Omul
436| Odiv
437| Omod
438| Oand
439| Oor
440| Oxor
441| Oshl
442| Oshr
443| Oeq
444| One0
445| Olt
446| Ogt
447| Ole
448| Oge
449
450(** val binary_operation_rect_Type4 :
451    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
452    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
453let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
454| Oadd -> h_Oadd
455| Osub -> h_Osub
456| Omul -> h_Omul
457| Odiv -> h_Odiv
458| Omod -> h_Omod
459| Oand -> h_Oand
460| Oor -> h_Oor
461| Oxor -> h_Oxor
462| Oshl -> h_Oshl
463| Oshr -> h_Oshr
464| Oeq -> h_Oeq
465| One0 -> h_One
466| Olt -> h_Olt
467| Ogt -> h_Ogt
468| Ole -> h_Ole
469| Oge -> h_Oge
470
471(** val binary_operation_rect_Type5 :
472    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
473    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
474let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
475| Oadd -> h_Oadd
476| Osub -> h_Osub
477| Omul -> h_Omul
478| Odiv -> h_Odiv
479| Omod -> h_Omod
480| Oand -> h_Oand
481| Oor -> h_Oor
482| Oxor -> h_Oxor
483| Oshl -> h_Oshl
484| Oshr -> h_Oshr
485| Oeq -> h_Oeq
486| One0 -> h_One
487| Olt -> h_Olt
488| Ogt -> h_Ogt
489| Ole -> h_Ole
490| Oge -> h_Oge
491
492(** val binary_operation_rect_Type3 :
493    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
494    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
495let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
496| Oadd -> h_Oadd
497| Osub -> h_Osub
498| Omul -> h_Omul
499| Odiv -> h_Odiv
500| Omod -> h_Omod
501| Oand -> h_Oand
502| Oor -> h_Oor
503| Oxor -> h_Oxor
504| Oshl -> h_Oshl
505| Oshr -> h_Oshr
506| Oeq -> h_Oeq
507| One0 -> h_One
508| Olt -> h_Olt
509| Ogt -> h_Ogt
510| Ole -> h_Ole
511| Oge -> h_Oge
512
513(** val binary_operation_rect_Type2 :
514    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
515    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
516let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
517| Oadd -> h_Oadd
518| Osub -> h_Osub
519| Omul -> h_Omul
520| Odiv -> h_Odiv
521| Omod -> h_Omod
522| Oand -> h_Oand
523| Oor -> h_Oor
524| Oxor -> h_Oxor
525| Oshl -> h_Oshl
526| Oshr -> h_Oshr
527| Oeq -> h_Oeq
528| One0 -> h_One
529| Olt -> h_Olt
530| Ogt -> h_Ogt
531| Ole -> h_Ole
532| Oge -> h_Oge
533
534(** val binary_operation_rect_Type1 :
535    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
536    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
537let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
538| Oadd -> h_Oadd
539| Osub -> h_Osub
540| Omul -> h_Omul
541| Odiv -> h_Odiv
542| Omod -> h_Omod
543| Oand -> h_Oand
544| Oor -> h_Oor
545| Oxor -> h_Oxor
546| Oshl -> h_Oshl
547| Oshr -> h_Oshr
548| Oeq -> h_Oeq
549| One0 -> h_One
550| Olt -> h_Olt
551| Ogt -> h_Ogt
552| Ole -> h_Ole
553| Oge -> h_Oge
554
555(** val binary_operation_rect_Type0 :
556    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
557    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
558let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
559| Oadd -> h_Oadd
560| Osub -> h_Osub
561| Omul -> h_Omul
562| Odiv -> h_Odiv
563| Omod -> h_Omod
564| Oand -> h_Oand
565| Oor -> h_Oor
566| Oxor -> h_Oxor
567| Oshl -> h_Oshl
568| Oshr -> h_Oshr
569| Oeq -> h_Oeq
570| One0 -> h_One
571| Olt -> h_Olt
572| Ogt -> h_Ogt
573| Ole -> h_Ole
574| Oge -> h_Oge
575
576(** val binary_operation_inv_rect_Type4 :
577    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
578    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
579    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
580    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
581let binary_operation_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
582  let hcut =
583    binary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
584      h14 h15 h16 hterm
585  in
586  hcut __
587
588(** val binary_operation_inv_rect_Type3 :
589    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
590    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
591    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
592    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
593let binary_operation_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
594  let hcut =
595    binary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
596      h14 h15 h16 hterm
597  in
598  hcut __
599
600(** val binary_operation_inv_rect_Type2 :
601    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
602    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
603    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
604    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
605let binary_operation_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
606  let hcut =
607    binary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
608      h14 h15 h16 hterm
609  in
610  hcut __
611
612(** val binary_operation_inv_rect_Type1 :
613    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
614    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
615    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
616    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
617let binary_operation_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
618  let hcut =
619    binary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
620      h14 h15 h16 hterm
621  in
622  hcut __
623
624(** val binary_operation_inv_rect_Type0 :
625    binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
626    'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
627    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
628    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
629let binary_operation_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
630  let hcut =
631    binary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
632      h14 h15 h16 hterm
633  in
634  hcut __
635
636(** val binary_operation_discr :
637    binary_operation -> binary_operation -> __ **)
638let binary_operation_discr x y =
639  Logic.eq_rect_Type2 x
640    (match x with
641     | Oadd -> Obj.magic (fun _ dH -> dH)
642     | Osub -> Obj.magic (fun _ dH -> dH)
643     | Omul -> Obj.magic (fun _ dH -> dH)
644     | Odiv -> Obj.magic (fun _ dH -> dH)
645     | Omod -> Obj.magic (fun _ dH -> dH)
646     | Oand -> Obj.magic (fun _ dH -> dH)
647     | Oor -> Obj.magic (fun _ dH -> dH)
648     | Oxor -> Obj.magic (fun _ dH -> dH)
649     | Oshl -> Obj.magic (fun _ dH -> dH)
650     | Oshr -> Obj.magic (fun _ dH -> dH)
651     | Oeq -> Obj.magic (fun _ dH -> dH)
652     | One0 -> Obj.magic (fun _ dH -> dH)
653     | Olt -> Obj.magic (fun _ dH -> dH)
654     | Ogt -> Obj.magic (fun _ dH -> dH)
655     | Ole -> Obj.magic (fun _ dH -> dH)
656     | Oge -> Obj.magic (fun _ dH -> dH)) y
657
658(** val binary_operation_jmdiscr :
659    binary_operation -> binary_operation -> __ **)
660let binary_operation_jmdiscr x y =
661  Logic.eq_rect_Type2 x
662    (match x with
663     | Oadd -> Obj.magic (fun _ dH -> dH)
664     | Osub -> Obj.magic (fun _ dH -> dH)
665     | Omul -> Obj.magic (fun _ dH -> dH)
666     | Odiv -> Obj.magic (fun _ dH -> dH)
667     | Omod -> Obj.magic (fun _ dH -> dH)
668     | Oand -> Obj.magic (fun _ dH -> dH)
669     | Oor -> Obj.magic (fun _ dH -> dH)
670     | Oxor -> Obj.magic (fun _ dH -> dH)
671     | Oshl -> Obj.magic (fun _ dH -> dH)
672     | Oshr -> Obj.magic (fun _ dH -> dH)
673     | Oeq -> Obj.magic (fun _ dH -> dH)
674     | One0 -> Obj.magic (fun _ dH -> dH)
675     | Olt -> Obj.magic (fun _ dH -> dH)
676     | Ogt -> Obj.magic (fun _ dH -> dH)
677     | Ole -> Obj.magic (fun _ dH -> dH)
678     | Oge -> Obj.magic (fun _ dH -> dH)) y
679
680type expr =
681| Expr of expr_descr * type0
682and expr_descr =
683| Econst_int of AST.intsize * AST.bvint
684| Evar of AST.ident
685| Ederef of expr
686| Eaddrof of expr
687| Eunop of unary_operation * expr
688| Ebinop of binary_operation * expr * expr
689| Ecast of type0 * expr
690| Econdition of expr * expr * expr
691| Eandbool of expr * expr
692| Eorbool of expr * expr
693| Esizeof of type0
694| Efield of expr * AST.ident
695| Ecost of CostLabel.costlabel * expr
696
697(** val expr_inv_rect_Type4 :
698    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
699let expr_inv_rect_Type4 hterm h1 =
700  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
701
702(** val expr_inv_rect_Type3 :
703    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
704let expr_inv_rect_Type3 hterm h1 =
705  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
706
707(** val expr_inv_rect_Type2 :
708    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
709let expr_inv_rect_Type2 hterm h1 =
710  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
711
712(** val expr_inv_rect_Type1 :
713    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
714let expr_inv_rect_Type1 hterm h1 =
715  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
716
717(** val expr_inv_rect_Type0 :
718    expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
719let expr_inv_rect_Type0 hterm h1 =
720  let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
721
722(** val expr_descr_inv_rect_Type4 :
723    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
724    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
725    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
726    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
727    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
728    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
729    expr -> __ -> 'a1) -> 'a1 **)
730let expr_descr_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
731  let hcut =
732    match hterm with
733    | Econst_int (x, x0) -> h1 x x0
734    | Evar x -> h2 x
735    | Ederef x -> h3 x
736    | Eaddrof x -> h4 x
737    | Eunop (x, x0) -> h5 x x0
738    | Ebinop (x, x0, x1) -> h6 x x0 x1
739    | Ecast (x, x0) -> h7 x x0
740    | Econdition (x, x0, x1) -> h8 x x0 x1
741    | Eandbool (x, x0) -> h9 x x0
742    | Eorbool (x, x0) -> h10 x x0
743    | Esizeof x -> h11 x
744    | Efield (x, x0) -> h12 x x0
745    | Ecost (x, x0) -> h13 x x0
746  in
747  hcut __
748
749(** val expr_descr_inv_rect_Type3 :
750    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
751    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
752    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
753    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
754    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
755    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
756    expr -> __ -> 'a1) -> 'a1 **)
757let expr_descr_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
758  let hcut =
759    match hterm with
760    | Econst_int (x, x0) -> h1 x x0
761    | Evar x -> h2 x
762    | Ederef x -> h3 x
763    | Eaddrof x -> h4 x
764    | Eunop (x, x0) -> h5 x x0
765    | Ebinop (x, x0, x1) -> h6 x x0 x1
766    | Ecast (x, x0) -> h7 x x0
767    | Econdition (x, x0, x1) -> h8 x x0 x1
768    | Eandbool (x, x0) -> h9 x x0
769    | Eorbool (x, x0) -> h10 x x0
770    | Esizeof x -> h11 x
771    | Efield (x, x0) -> h12 x x0
772    | Ecost (x, x0) -> h13 x x0
773  in
774  hcut __
775
776(** val expr_descr_inv_rect_Type2 :
777    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
778    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
779    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
780    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
781    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
782    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
783    expr -> __ -> 'a1) -> 'a1 **)
784let expr_descr_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
785  let hcut =
786    match hterm with
787    | Econst_int (x, x0) -> h1 x x0
788    | Evar x -> h2 x
789    | Ederef x -> h3 x
790    | Eaddrof x -> h4 x
791    | Eunop (x, x0) -> h5 x x0
792    | Ebinop (x, x0, x1) -> h6 x x0 x1
793    | Ecast (x, x0) -> h7 x x0
794    | Econdition (x, x0, x1) -> h8 x x0 x1
795    | Eandbool (x, x0) -> h9 x x0
796    | Eorbool (x, x0) -> h10 x x0
797    | Esizeof x -> h11 x
798    | Efield (x, x0) -> h12 x x0
799    | Ecost (x, x0) -> h13 x x0
800  in
801  hcut __
802
803(** val expr_descr_inv_rect_Type1 :
804    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
805    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
806    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
807    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
808    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
809    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
810    expr -> __ -> 'a1) -> 'a1 **)
811let expr_descr_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
812  let hcut =
813    match hterm with
814    | Econst_int (x, x0) -> h1 x x0
815    | Evar x -> h2 x
816    | Ederef x -> h3 x
817    | Eaddrof x -> h4 x
818    | Eunop (x, x0) -> h5 x x0
819    | Ebinop (x, x0, x1) -> h6 x x0 x1
820    | Ecast (x, x0) -> h7 x x0
821    | Econdition (x, x0, x1) -> h8 x x0 x1
822    | Eandbool (x, x0) -> h9 x x0
823    | Eorbool (x, x0) -> h10 x x0
824    | Esizeof x -> h11 x
825    | Efield (x, x0) -> h12 x x0
826    | Ecost (x, x0) -> h13 x x0
827  in
828  hcut __
829
830(** val expr_descr_inv_rect_Type0 :
831    expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
832    -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
833    -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
834    -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
835    (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
836    __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
837    expr -> __ -> 'a1) -> 'a1 **)
838let expr_descr_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
839  let hcut =
840    match hterm with
841    | Econst_int (x, x0) -> h1 x x0
842    | Evar x -> h2 x
843    | Ederef x -> h3 x
844    | Eaddrof x -> h4 x
845    | Eunop (x, x0) -> h5 x x0
846    | Ebinop (x, x0, x1) -> h6 x x0 x1
847    | Ecast (x, x0) -> h7 x x0
848    | Econdition (x, x0, x1) -> h8 x x0 x1
849    | Eandbool (x, x0) -> h9 x x0
850    | Eorbool (x, x0) -> h10 x x0
851    | Esizeof x -> h11 x
852    | Efield (x, x0) -> h12 x x0
853    | Ecost (x, x0) -> h13 x x0
854  in
855  hcut __
856
857(** val expr_discr : expr -> expr -> __ **)
858let expr_discr x y =
859  Logic.eq_rect_Type2 x
860    (let Expr (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
861
862(** val expr_descr_discr : expr_descr -> expr_descr -> __ **)
863let expr_descr_discr x y =
864  Logic.eq_rect_Type2 x
865    (match x with
866     | Econst_int (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
867     | Evar a0 -> Obj.magic (fun _ dH -> dH __)
868     | Ederef a0 -> Obj.magic (fun _ dH -> dH __)
869     | Eaddrof a0 -> Obj.magic (fun _ dH -> dH __)
870     | Eunop (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
871     | Ebinop (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
872     | Ecast (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
873     | Econdition (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
874     | Eandbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
875     | Eorbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
876     | Esizeof a0 -> Obj.magic (fun _ dH -> dH __)
877     | Efield (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
878     | Ecost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
879
880(** val expr_jmdiscr : expr -> expr -> __ **)
881let expr_jmdiscr x y =
882  Logic.eq_rect_Type2 x
883    (let Expr (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
884
885(** val expr_descr_jmdiscr : expr_descr -> expr_descr -> __ **)
886let expr_descr_jmdiscr x y =
887  Logic.eq_rect_Type2 x
888    (match x with
889     | Econst_int (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
890     | Evar a0 -> Obj.magic (fun _ dH -> dH __)
891     | Ederef a0 -> Obj.magic (fun _ dH -> dH __)
892     | Eaddrof a0 -> Obj.magic (fun _ dH -> dH __)
893     | Eunop (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
894     | Ebinop (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
895     | Ecast (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
896     | Econdition (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
897     | Eandbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
898     | Eorbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
899     | Esizeof a0 -> Obj.magic (fun _ dH -> dH __)
900     | Efield (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
901     | Ecost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
902
903(** val typeof : expr -> type0 **)
904let typeof = function
905| Expr (de, te) -> te
906
907type label = AST.ident
908
909type statement =
910| Sskip
911| Sassign of expr * expr
912| Scall of expr Types.option * expr * expr List.list
913| Ssequence of statement * statement
914| Sifthenelse of expr * statement * statement
915| Swhile of expr * statement
916| Sdowhile of expr * statement
917| Sfor of statement * expr * statement * statement
918| Sbreak
919| Scontinue
920| Sreturn of expr Types.option
921| Sswitch of expr * labeled_statements
922| Slabel of label * statement
923| Sgoto of label
924| Scost of CostLabel.costlabel * statement
925and labeled_statements =
926| LSdefault of statement
927| LScase of AST.intsize * AST.bvint * statement * labeled_statements
928
929(** val statement_inv_rect_Type4 :
930    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
931    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
932    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
933    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
934    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
935    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
936    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
937    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
938    -> 'a1 **)
939let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
940  let hcut =
941    match hterm with
942    | Sskip -> h1
943    | Sassign (x, x0) -> h2 x x0
944    | Scall (x, x0, x1) -> h3 x x0 x1
945    | Ssequence (x, x0) -> h4 x x0
946    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
947    | Swhile (x, x0) -> h6 x x0
948    | Sdowhile (x, x0) -> h7 x x0
949    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
950    | Sbreak -> h9
951    | Scontinue -> h10
952    | Sreturn x -> h11 x
953    | Sswitch (x, x0) -> h12 x x0
954    | Slabel (x, x0) -> h13 x x0
955    | Sgoto x -> h14 x
956    | Scost (x, x0) -> h15 x x0
957  in
958  hcut __
959
960(** val statement_inv_rect_Type3 :
961    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
962    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
963    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
964    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
965    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
966    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
967    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
968    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
969    -> 'a1 **)
970let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
971  let hcut =
972    match hterm with
973    | Sskip -> h1
974    | Sassign (x, x0) -> h2 x x0
975    | Scall (x, x0, x1) -> h3 x x0 x1
976    | Ssequence (x, x0) -> h4 x x0
977    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
978    | Swhile (x, x0) -> h6 x x0
979    | Sdowhile (x, x0) -> h7 x x0
980    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
981    | Sbreak -> h9
982    | Scontinue -> h10
983    | Sreturn x -> h11 x
984    | Sswitch (x, x0) -> h12 x x0
985    | Slabel (x, x0) -> h13 x x0
986    | Sgoto x -> h14 x
987    | Scost (x, x0) -> h15 x x0
988  in
989  hcut __
990
991(** val statement_inv_rect_Type2 :
992    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
993    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
994    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
995    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
996    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
997    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
998    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
999    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
1000    -> 'a1 **)
1001let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
1002  let hcut =
1003    match hterm with
1004    | Sskip -> h1
1005    | Sassign (x, x0) -> h2 x x0
1006    | Scall (x, x0, x1) -> h3 x x0 x1
1007    | Ssequence (x, x0) -> h4 x x0
1008    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
1009    | Swhile (x, x0) -> h6 x x0
1010    | Sdowhile (x, x0) -> h7 x x0
1011    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
1012    | Sbreak -> h9
1013    | Scontinue -> h10
1014    | Sreturn x -> h11 x
1015    | Sswitch (x, x0) -> h12 x x0
1016    | Slabel (x, x0) -> h13 x x0
1017    | Sgoto x -> h14 x
1018    | Scost (x, x0) -> h15 x x0
1019  in
1020  hcut __
1021
1022(** val statement_inv_rect_Type1 :
1023    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
1024    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
1025    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
1026    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
1027    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
1028    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
1029    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
1030    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
1031    -> 'a1 **)
1032let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
1033  let hcut =
1034    match hterm with
1035    | Sskip -> h1
1036    | Sassign (x, x0) -> h2 x x0
1037    | Scall (x, x0, x1) -> h3 x x0 x1
1038    | Ssequence (x, x0) -> h4 x x0
1039    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
1040    | Swhile (x, x0) -> h6 x x0
1041    | Sdowhile (x, x0) -> h7 x x0
1042    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
1043    | Sbreak -> h9
1044    | Scontinue -> h10
1045    | Sreturn x -> h11 x
1046    | Sswitch (x, x0) -> h12 x x0
1047    | Slabel (x, x0) -> h13 x x0
1048    | Sgoto x -> h14 x
1049    | Scost (x, x0) -> h15 x x0
1050  in
1051  hcut __
1052
1053(** val statement_inv_rect_Type0 :
1054    statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
1055    Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
1056    statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
1057    -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
1058    -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
1059    'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
1060    labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
1061    (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
1062    -> 'a1 **)
1063let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
1064  let hcut =
1065    match hterm with
1066    | Sskip -> h1
1067    | Sassign (x, x0) -> h2 x x0
1068    | Scall (x, x0, x1) -> h3 x x0 x1
1069    | Ssequence (x, x0) -> h4 x x0
1070    | Sifthenelse (x, x0, x1) -> h5 x x0 x1
1071    | Swhile (x, x0) -> h6 x x0
1072    | Sdowhile (x, x0) -> h7 x x0
1073    | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
1074    | Sbreak -> h9
1075    | Scontinue -> h10
1076    | Sreturn x -> h11 x
1077    | Sswitch (x, x0) -> h12 x x0
1078    | Slabel (x, x0) -> h13 x x0
1079    | Sgoto x -> h14 x
1080    | Scost (x, x0) -> h15 x x0
1081  in
1082  hcut __
1083
1084(** val labeled_statements_inv_rect_Type4 :
1085    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1086    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1087let labeled_statements_inv_rect_Type4 hterm h1 h2 =
1088  let hcut =
1089    match hterm with
1090    | LSdefault x -> h1 x
1091    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1092  in
1093  hcut __
1094
1095(** val labeled_statements_inv_rect_Type3 :
1096    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1097    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1098let labeled_statements_inv_rect_Type3 hterm h1 h2 =
1099  let hcut =
1100    match hterm with
1101    | LSdefault x -> h1 x
1102    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1103  in
1104  hcut __
1105
1106(** val labeled_statements_inv_rect_Type2 :
1107    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1108    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1109let labeled_statements_inv_rect_Type2 hterm h1 h2 =
1110  let hcut =
1111    match hterm with
1112    | LSdefault x -> h1 x
1113    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1114  in
1115  hcut __
1116
1117(** val labeled_statements_inv_rect_Type1 :
1118    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1119    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1120let labeled_statements_inv_rect_Type1 hterm h1 h2 =
1121  let hcut =
1122    match hterm with
1123    | LSdefault x -> h1 x
1124    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1125  in
1126  hcut __
1127
1128(** val labeled_statements_inv_rect_Type0 :
1129    labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1130    AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1131let labeled_statements_inv_rect_Type0 hterm h1 h2 =
1132  let hcut =
1133    match hterm with
1134    | LSdefault x -> h1 x
1135    | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1136  in
1137  hcut __
1138
1139(** val statement_discr : statement -> statement -> __ **)
1140let statement_discr x y =
1141  Logic.eq_rect_Type2 x
1142    (match x with
1143     | Sskip -> Obj.magic (fun _ dH -> dH)
1144     | Sassign (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1145     | Scall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1146     | Ssequence (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1147     | Sifthenelse (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1148     | Swhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1149     | Sdowhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1150     | Sfor (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1151     | Sbreak -> Obj.magic (fun _ dH -> dH)
1152     | Scontinue -> Obj.magic (fun _ dH -> dH)
1153     | Sreturn a0 -> Obj.magic (fun _ dH -> dH __)
1154     | Sswitch (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1155     | Slabel (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1156     | Sgoto a0 -> Obj.magic (fun _ dH -> dH __)
1157     | Scost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1158
1159(** val labeled_statements_discr :
1160    labeled_statements -> labeled_statements -> __ **)
1161let labeled_statements_discr x y =
1162  Logic.eq_rect_Type2 x
1163    (match x with
1164     | LSdefault a0 -> Obj.magic (fun _ dH -> dH __)
1165     | LScase (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1166
1167(** val statement_jmdiscr : statement -> statement -> __ **)
1168let statement_jmdiscr x y =
1169  Logic.eq_rect_Type2 x
1170    (match x with
1171     | Sskip -> Obj.magic (fun _ dH -> dH)
1172     | Sassign (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1173     | Scall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1174     | Ssequence (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1175     | Sifthenelse (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1176     | Swhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1177     | Sdowhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1178     | Sfor (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1179     | Sbreak -> Obj.magic (fun _ dH -> dH)
1180     | Scontinue -> Obj.magic (fun _ dH -> dH)
1181     | Sreturn a0 -> Obj.magic (fun _ dH -> dH __)
1182     | Sswitch (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1183     | Slabel (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1184     | Sgoto a0 -> Obj.magic (fun _ dH -> dH __)
1185     | Scost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1186
1187(** val labeled_statements_jmdiscr :
1188    labeled_statements -> labeled_statements -> __ **)
1189let labeled_statements_jmdiscr x y =
1190  Logic.eq_rect_Type2 x
1191    (match x with
1192     | LSdefault a0 -> Obj.magic (fun _ dH -> dH __)
1193     | LScase (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1194
1195type function0 = { fn_return : type0;
1196                   fn_params : (AST.ident, type0) Types.prod List.list;
1197                   fn_vars : (AST.ident, type0) Types.prod List.list;
1198                   fn_body : statement }
1199
1200(** val function_rect_Type4 :
1201    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1202    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1203let rec function_rect_Type4 h_mk_function x_2206 =
1204  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1205    fn_body = fn_body0 } = x_2206
1206  in
1207  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1208
1209(** val function_rect_Type5 :
1210    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1211    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1212let rec function_rect_Type5 h_mk_function x_2208 =
1213  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1214    fn_body = fn_body0 } = x_2208
1215  in
1216  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1217
1218(** val function_rect_Type3 :
1219    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1220    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1221let rec function_rect_Type3 h_mk_function x_2210 =
1222  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1223    fn_body = fn_body0 } = x_2210
1224  in
1225  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1226
1227(** val function_rect_Type2 :
1228    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1229    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1230let rec function_rect_Type2 h_mk_function x_2212 =
1231  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1232    fn_body = fn_body0 } = x_2212
1233  in
1234  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1235
1236(** val function_rect_Type1 :
1237    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1238    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1239let rec function_rect_Type1 h_mk_function x_2214 =
1240  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1241    fn_body = fn_body0 } = x_2214
1242  in
1243  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1244
1245(** val function_rect_Type0 :
1246    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1247    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1248let rec function_rect_Type0 h_mk_function x_2216 =
1249  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1250    fn_body = fn_body0 } = x_2216
1251  in
1252  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1253
1254(** val fn_return : function0 -> type0 **)
1255let rec fn_return xxx =
1256  xxx.fn_return
1257
1258(** val fn_params : function0 -> (AST.ident, type0) Types.prod List.list **)
1259let rec fn_params xxx =
1260  xxx.fn_params
1261
1262(** val fn_vars : function0 -> (AST.ident, type0) Types.prod List.list **)
1263let rec fn_vars xxx =
1264  xxx.fn_vars
1265
1266(** val fn_body : function0 -> statement **)
1267let rec fn_body xxx =
1268  xxx.fn_body
1269
1270(** val function_inv_rect_Type4 :
1271    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1272    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1273let function_inv_rect_Type4 hterm h1 =
1274  let hcut = function_rect_Type4 h1 hterm in hcut __
1275
1276(** val function_inv_rect_Type3 :
1277    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1278    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1279let function_inv_rect_Type3 hterm h1 =
1280  let hcut = function_rect_Type3 h1 hterm in hcut __
1281
1282(** val function_inv_rect_Type2 :
1283    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1284    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1285let function_inv_rect_Type2 hterm h1 =
1286  let hcut = function_rect_Type2 h1 hterm in hcut __
1287
1288(** val function_inv_rect_Type1 :
1289    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1290    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1291let function_inv_rect_Type1 hterm h1 =
1292  let hcut = function_rect_Type1 h1 hterm in hcut __
1293
1294(** val function_inv_rect_Type0 :
1295    function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1296    (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1297let function_inv_rect_Type0 hterm h1 =
1298  let hcut = function_rect_Type0 h1 hterm in hcut __
1299
1300(** val function_discr : function0 -> function0 -> __ **)
1301let function_discr x y =
1302  Logic.eq_rect_Type2 x
1303    (let { fn_return = a0; fn_params = a1; fn_vars = a2; fn_body = a3 } = x
1304     in
1305    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1306
1307(** val function_jmdiscr : function0 -> function0 -> __ **)
1308let function_jmdiscr x y =
1309  Logic.eq_rect_Type2 x
1310    (let { fn_return = a0; fn_params = a1; fn_vars = a2; fn_body = a3 } = x
1311     in
1312    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1313
1314type clight_fundef =
1315| CL_Internal of function0
1316| CL_External of AST.ident * typelist * type0
1317
1318(** val clight_fundef_rect_Type4 :
1319    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1320    clight_fundef -> 'a1 **)
1321let rec clight_fundef_rect_Type4 h_CL_Internal h_CL_External = function
1322| CL_Internal x_2238 -> h_CL_Internal x_2238
1323| CL_External (x_2241, x_2240, x_2239) -> h_CL_External x_2241 x_2240 x_2239
1324
1325(** val clight_fundef_rect_Type5 :
1326    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1327    clight_fundef -> 'a1 **)
1328let rec clight_fundef_rect_Type5 h_CL_Internal h_CL_External = function
1329| CL_Internal x_2245 -> h_CL_Internal x_2245
1330| CL_External (x_2248, x_2247, x_2246) -> h_CL_External x_2248 x_2247 x_2246
1331
1332(** val clight_fundef_rect_Type3 :
1333    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1334    clight_fundef -> 'a1 **)
1335let rec clight_fundef_rect_Type3 h_CL_Internal h_CL_External = function
1336| CL_Internal x_2252 -> h_CL_Internal x_2252
1337| CL_External (x_2255, x_2254, x_2253) -> h_CL_External x_2255 x_2254 x_2253
1338
1339(** val clight_fundef_rect_Type2 :
1340    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1341    clight_fundef -> 'a1 **)
1342let rec clight_fundef_rect_Type2 h_CL_Internal h_CL_External = function
1343| CL_Internal x_2259 -> h_CL_Internal x_2259
1344| CL_External (x_2262, x_2261, x_2260) -> h_CL_External x_2262 x_2261 x_2260
1345
1346(** val clight_fundef_rect_Type1 :
1347    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1348    clight_fundef -> 'a1 **)
1349let rec clight_fundef_rect_Type1 h_CL_Internal h_CL_External = function
1350| CL_Internal x_2266 -> h_CL_Internal x_2266
1351| CL_External (x_2269, x_2268, x_2267) -> h_CL_External x_2269 x_2268 x_2267
1352
1353(** val clight_fundef_rect_Type0 :
1354    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1355    clight_fundef -> 'a1 **)
1356let rec clight_fundef_rect_Type0 h_CL_Internal h_CL_External = function
1357| CL_Internal x_2273 -> h_CL_Internal x_2273
1358| CL_External (x_2276, x_2275, x_2274) -> h_CL_External x_2276 x_2275 x_2274
1359
1360(** val clight_fundef_inv_rect_Type4 :
1361    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1362    type0 -> __ -> 'a1) -> 'a1 **)
1363let clight_fundef_inv_rect_Type4 hterm h1 h2 =
1364  let hcut = clight_fundef_rect_Type4 h1 h2 hterm in hcut __
1365
1366(** val clight_fundef_inv_rect_Type3 :
1367    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1368    type0 -> __ -> 'a1) -> 'a1 **)
1369let clight_fundef_inv_rect_Type3 hterm h1 h2 =
1370  let hcut = clight_fundef_rect_Type3 h1 h2 hterm in hcut __
1371
1372(** val clight_fundef_inv_rect_Type2 :
1373    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1374    type0 -> __ -> 'a1) -> 'a1 **)
1375let clight_fundef_inv_rect_Type2 hterm h1 h2 =
1376  let hcut = clight_fundef_rect_Type2 h1 h2 hterm in hcut __
1377
1378(** val clight_fundef_inv_rect_Type1 :
1379    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1380    type0 -> __ -> 'a1) -> 'a1 **)
1381let clight_fundef_inv_rect_Type1 hterm h1 h2 =
1382  let hcut = clight_fundef_rect_Type1 h1 h2 hterm in hcut __
1383
1384(** val clight_fundef_inv_rect_Type0 :
1385    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1386    type0 -> __ -> 'a1) -> 'a1 **)
1387let clight_fundef_inv_rect_Type0 hterm h1 h2 =
1388  let hcut = clight_fundef_rect_Type0 h1 h2 hterm in hcut __
1389
1390(** val clight_fundef_discr : clight_fundef -> clight_fundef -> __ **)
1391let clight_fundef_discr x y =
1392  Logic.eq_rect_Type2 x
1393    (match x with
1394     | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
1395     | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1396
1397(** val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __ **)
1398let clight_fundef_jmdiscr x y =
1399  Logic.eq_rect_Type2 x
1400    (match x with
1401     | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
1402     | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1403
1404type clight_program =
1405  (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program
1406
1407(** val type_of_params :
1408    (AST.ident, type0) Types.prod List.list -> typelist **)
1409let rec type_of_params = function
1410| List.Nil -> Tnil
1411| List.Cons (h, rem) ->
1412  let { Types.fst = id; Types.snd = ty } = h in
1413  Tcons (ty, (type_of_params rem))
1414
1415(** val type_of_function : function0 -> type0 **)
1416let type_of_function f =
1417  Tfunction ((type_of_params f.fn_params), f.fn_return)
1418
1419(** val type_of_fundef : clight_fundef -> type0 **)
1420let type_of_fundef = function
1421| CL_Internal fd -> type_of_function fd
1422| CL_External (id, args, res1) -> Tfunction (args, res1)
1423
1424(** val alignof : type0 -> Nat.nat **)
1425let rec alignof = function
1426| Tvoid -> Nat.S Nat.O
1427| Tint (sz, x) ->
1428  (match sz with
1429   | AST.I8 -> Nat.S Nat.O
1430   | AST.I16 -> Nat.S (Nat.S Nat.O)
1431   | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1432| Tpointer x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
1433| Tarray (t', n) -> alignof t'
1434| Tfunction (x, x0) -> Nat.S Nat.O
1435| Tstruct (x, fld) -> alignof_fields fld
1436| Tunion (x, fld) -> alignof_fields fld
1437| Tcomp_ptr x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
1438(** val alignof_fields : fieldlist -> Nat.nat **)
1439and alignof_fields = function
1440| Fnil -> Nat.S Nat.O
1441| Fcons (id, t, f') -> Nat.max (alignof t) (alignof_fields f')
1442
1443(** val sizeof : type0 -> Nat.nat **)
1444let rec sizeof t = match t with
1445| Tvoid -> Nat.S Nat.O
1446| Tint (i, x) ->
1447  (match i with
1448   | AST.I8 -> Nat.S Nat.O
1449   | AST.I16 -> Nat.S (Nat.S Nat.O)
1450   | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1451| Tpointer x -> AST.size_pointer
1452| Tarray (t', n) -> Nat.times (sizeof t') (Nat.max (Nat.S Nat.O) n)
1453| Tfunction (x, x0) -> Nat.S Nat.O
1454| Tstruct (x, fld) ->
1455  Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_struct fld Nat.O)) (alignof t)
1456| Tunion (x, fld) ->
1457  Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_union fld)) (alignof t)
1458| Tcomp_ptr x -> AST.size_pointer
1459(** val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat **)
1460and sizeof_struct fld pos0 =
1461  match fld with
1462  | Fnil -> pos0
1463  | Fcons (id, t, fld') ->
1464    sizeof_struct fld' (Nat.plus (Coqlib.align pos0 (alignof t)) (sizeof t))
1465(** val sizeof_union : fieldlist -> Nat.nat **)
1466and sizeof_union = function
1467| Fnil -> Nat.O
1468| Fcons (id, t, fld') -> Nat.max (sizeof t) (sizeof_union fld')
1469
1470(** val field_offset_rec :
1471    AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res **)
1472let rec field_offset_rec id fld pos0 =
1473  match fld with
1474  | Fnil ->
1475    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1476      (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
1477  | Fcons (id', t, fld') ->
1478    (match AST.ident_eq id id' with
1479     | Types.Inl _ -> Errors.OK (Coqlib.align pos0 (alignof t))
1480     | Types.Inr _ ->
1481       field_offset_rec id fld'
1482         (Nat.plus (Coqlib.align pos0 (alignof t)) (sizeof t)))
1483
1484(** val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res **)
1485let field_offset id fld =
1486  field_offset_rec id fld Nat.O
1487
1488(** val field_type : AST.ident -> fieldlist -> type0 Errors.res **)
1489let rec field_type id = function
1490| Fnil ->
1491  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1492    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
1493| Fcons (id', t, fld') ->
1494  (match AST.ident_eq id id' with
1495   | Types.Inl _ -> Errors.OK t
1496   | Types.Inr _ -> field_type id fld')
1497
1498(** val typ_of_type : type0 -> AST.typ **)
1499let typ_of_type = function
1500| Tvoid -> AST.ASTint (AST.I32, AST.Unsigned)
1501| Tint (sz, sg) -> AST.ASTint (sz, sg)
1502| Tpointer x -> AST.ASTptr
1503| Tarray (x, x0) -> AST.ASTptr
1504| Tfunction (x, x0) -> AST.ASTptr
1505| Tstruct (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
1506| Tunion (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
1507| Tcomp_ptr x -> AST.ASTptr
1508
1509(** val opttyp_of_type : type0 -> AST.typ Types.option **)
1510let opttyp_of_type = function
1511| Tvoid -> Types.None
1512| Tint (sz, sg) -> Types.Some (AST.ASTint (sz, sg))
1513| Tpointer x -> Types.Some AST.ASTptr
1514| Tarray (x, x0) -> Types.Some AST.ASTptr
1515| Tfunction (x, x0) -> Types.Some AST.ASTptr
1516| Tstruct (x, x0) -> Types.None
1517| Tunion (x, x0) -> Types.None
1518| Tcomp_ptr x -> Types.Some AST.ASTptr
1519
1520(** val typlist_of_typelist : typelist -> AST.typ List.list **)
1521let rec typlist_of_typelist = function
1522| Tnil -> List.Nil
1523| Tcons (hd0, tl0) ->
1524  List.Cons ((typ_of_type hd0), (typlist_of_typelist tl0))
1525
1526type mode =
1527| By_value of AST.typ
1528| By_reference
1529| By_nothing of AST.typ
1530
1531(** val mode_rect_Type4 :
1532    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1533let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_2326 = function
1534| By_value t -> h_By_value t
1535| By_reference -> h_By_reference
1536| By_nothing t -> h_By_nothing t
1537
1538(** val mode_rect_Type5 :
1539    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1540let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_2331 = function
1541| By_value t -> h_By_value t
1542| By_reference -> h_By_reference
1543| By_nothing t -> h_By_nothing t
1544
1545(** val mode_rect_Type3 :
1546    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1547let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_2336 = function
1548| By_value t -> h_By_value t
1549| By_reference -> h_By_reference
1550| By_nothing t -> h_By_nothing t
1551
1552(** val mode_rect_Type2 :
1553    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1554let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_2341 = function
1555| By_value t -> h_By_value t
1556| By_reference -> h_By_reference
1557| By_nothing t -> h_By_nothing t
1558
1559(** val mode_rect_Type1 :
1560    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1561let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_2346 = function
1562| By_value t -> h_By_value t
1563| By_reference -> h_By_reference
1564| By_nothing t -> h_By_nothing t
1565
1566(** val mode_rect_Type0 :
1567    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1568let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_2351 = function
1569| By_value t -> h_By_value t
1570| By_reference -> h_By_reference
1571| By_nothing t -> h_By_nothing t
1572
1573(** val mode_inv_rect_Type4 :
1574    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1575    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1576let mode_inv_rect_Type4 x1 hterm h1 h2 h3 =
1577  let hcut = mode_rect_Type4 h1 h2 h3 x1 hterm in hcut __ __
1578
1579(** val mode_inv_rect_Type3 :
1580    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1581    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1582let mode_inv_rect_Type3 x1 hterm h1 h2 h3 =
1583  let hcut = mode_rect_Type3 h1 h2 h3 x1 hterm in hcut __ __
1584
1585(** val mode_inv_rect_Type2 :
1586    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1587    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1588let mode_inv_rect_Type2 x1 hterm h1 h2 h3 =
1589  let hcut = mode_rect_Type2 h1 h2 h3 x1 hterm in hcut __ __
1590
1591(** val mode_inv_rect_Type1 :
1592    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1593    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1594let mode_inv_rect_Type1 x1 hterm h1 h2 h3 =
1595  let hcut = mode_rect_Type1 h1 h2 h3 x1 hterm in hcut __ __
1596
1597(** val mode_inv_rect_Type0 :
1598    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1599    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1600let mode_inv_rect_Type0 x1 hterm h1 h2 h3 =
1601  let hcut = mode_rect_Type0 h1 h2 h3 x1 hterm in hcut __ __
1602
1603(** val mode_discr : AST.typ -> mode -> mode -> __ **)
1604let mode_discr a1 x y =
1605  Logic.eq_rect_Type2 x
1606    (match x with
1607     | By_value a0 -> Obj.magic (fun _ dH -> dH __)
1608     | By_reference -> Obj.magic (fun _ dH -> dH)
1609     | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y
1610
1611(** val mode_jmdiscr : AST.typ -> mode -> mode -> __ **)
1612let mode_jmdiscr a1 x y =
1613  Logic.eq_rect_Type2 x
1614    (match x with
1615     | By_value a0 -> Obj.magic (fun _ dH -> dH __)
1616     | By_reference -> Obj.magic (fun _ dH -> dH)
1617     | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y
1618
1619(** val access_mode : type0 -> mode **)
1620let access_mode = function
1621| Tvoid -> By_nothing (typ_of_type Tvoid)
1622| Tint (i, s) -> By_value (AST.ASTint (i, s))
1623| Tpointer x -> By_value AST.ASTptr
1624| Tarray (x, x0) -> By_reference
1625| Tfunction (x, x0) -> By_reference
1626| Tstruct (x, fList) -> By_nothing (typ_of_type (Tstruct (x, fList)))
1627| Tunion (x, fList) -> By_nothing (typ_of_type (Tunion (x, fList)))
1628| Tcomp_ptr x -> By_value AST.ASTptr
1629
1630(** val signature_of_type : typelist -> type0 -> AST.signature **)
1631let signature_of_type args res1 =
1632  { AST.sig_args = (typlist_of_typelist args); AST.sig_res =
1633    (opttyp_of_type res1) }
1634
1635(** val external_function0 :
1636    AST.ident -> typelist -> type0 -> AST.external_function **)
1637let external_function0 id targs tres =
1638  { AST.ef_id = id; AST.ef_sig = (signature_of_type targs tres) }
1639
Note: See TracBrowser for help on using the repository browser.