source: extracted/csyntax.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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