source: extracted/csyntax.ml @ 2997

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

New extraction.

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