source: driver/extracted/csyntax.ml @ 3106

Last change on this file since 3106 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

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 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_4495 =
1206  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1207    fn_body = fn_body0 } = x_4495
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_4497 =
1215  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1216    fn_body = fn_body0 } = x_4497
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_4499 =
1224  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1225    fn_body = fn_body0 } = x_4499
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_4501 =
1233  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1234    fn_body = fn_body0 } = x_4501
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_4503 =
1242  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1243    fn_body = fn_body0 } = x_4503
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_4505 =
1251  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1252    fn_body = fn_body0 } = x_4505
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_4527 -> h_CL_Internal x_4527
1325| CL_External (x_4530, x_4529, x_4528) -> h_CL_External x_4530 x_4529 x_4528
1326
1327(** val clight_fundef_rect_Type5 :
1328    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1329    clight_fundef -> 'a1 **)
1330let rec clight_fundef_rect_Type5 h_CL_Internal h_CL_External = function
1331| CL_Internal x_4534 -> h_CL_Internal x_4534
1332| CL_External (x_4537, x_4536, x_4535) -> h_CL_External x_4537 x_4536 x_4535
1333
1334(** val clight_fundef_rect_Type3 :
1335    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1336    clight_fundef -> 'a1 **)
1337let rec clight_fundef_rect_Type3 h_CL_Internal h_CL_External = function
1338| CL_Internal x_4541 -> h_CL_Internal x_4541
1339| CL_External (x_4544, x_4543, x_4542) -> h_CL_External x_4544 x_4543 x_4542
1340
1341(** val clight_fundef_rect_Type2 :
1342    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1343    clight_fundef -> 'a1 **)
1344let rec clight_fundef_rect_Type2 h_CL_Internal h_CL_External = function
1345| CL_Internal x_4548 -> h_CL_Internal x_4548
1346| CL_External (x_4551, x_4550, x_4549) -> h_CL_External x_4551 x_4550 x_4549
1347
1348(** val clight_fundef_rect_Type1 :
1349    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1350    clight_fundef -> 'a1 **)
1351let rec clight_fundef_rect_Type1 h_CL_Internal h_CL_External = function
1352| CL_Internal x_4555 -> h_CL_Internal x_4555
1353| CL_External (x_4558, x_4557, x_4556) -> h_CL_External x_4558 x_4557 x_4556
1354
1355(** val clight_fundef_rect_Type0 :
1356    (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1357    clight_fundef -> 'a1 **)
1358let rec clight_fundef_rect_Type0 h_CL_Internal h_CL_External = function
1359| CL_Internal x_4562 -> h_CL_Internal x_4562
1360| CL_External (x_4565, x_4564, x_4563) -> h_CL_External x_4565 x_4564 x_4563
1361
1362(** val clight_fundef_inv_rect_Type4 :
1363    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1364    type0 -> __ -> 'a1) -> 'a1 **)
1365let clight_fundef_inv_rect_Type4 hterm h1 h2 =
1366  let hcut = clight_fundef_rect_Type4 h1 h2 hterm in hcut __
1367
1368(** val clight_fundef_inv_rect_Type3 :
1369    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1370    type0 -> __ -> 'a1) -> 'a1 **)
1371let clight_fundef_inv_rect_Type3 hterm h1 h2 =
1372  let hcut = clight_fundef_rect_Type3 h1 h2 hterm in hcut __
1373
1374(** val clight_fundef_inv_rect_Type2 :
1375    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1376    type0 -> __ -> 'a1) -> 'a1 **)
1377let clight_fundef_inv_rect_Type2 hterm h1 h2 =
1378  let hcut = clight_fundef_rect_Type2 h1 h2 hterm in hcut __
1379
1380(** val clight_fundef_inv_rect_Type1 :
1381    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1382    type0 -> __ -> 'a1) -> 'a1 **)
1383let clight_fundef_inv_rect_Type1 hterm h1 h2 =
1384  let hcut = clight_fundef_rect_Type1 h1 h2 hterm in hcut __
1385
1386(** val clight_fundef_inv_rect_Type0 :
1387    clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1388    type0 -> __ -> 'a1) -> 'a1 **)
1389let clight_fundef_inv_rect_Type0 hterm h1 h2 =
1390  let hcut = clight_fundef_rect_Type0 h1 h2 hterm in hcut __
1391
1392(** val clight_fundef_discr : clight_fundef -> clight_fundef -> __ **)
1393let clight_fundef_discr x y =
1394  Logic.eq_rect_Type2 x
1395    (match x with
1396     | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
1397     | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1398
1399(** val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __ **)
1400let clight_fundef_jmdiscr x y =
1401  Logic.eq_rect_Type2 x
1402    (match x with
1403     | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
1404     | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1405
1406type clight_program =
1407  (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program
1408
1409(** val type_of_params :
1410    (AST.ident, type0) Types.prod List.list -> typelist **)
1411let rec type_of_params = function
1412| List.Nil -> Tnil
1413| List.Cons (h, rem) ->
1414  let { Types.fst = id; Types.snd = ty } = h in
1415  Tcons (ty, (type_of_params rem))
1416
1417(** val type_of_function : function0 -> type0 **)
1418let type_of_function f =
1419  Tfunction ((type_of_params f.fn_params), f.fn_return)
1420
1421(** val type_of_fundef : clight_fundef -> type0 **)
1422let type_of_fundef = function
1423| CL_Internal fd -> type_of_function fd
1424| CL_External (id, args, res) -> Tfunction (args, res)
1425
1426(** val alignof : type0 -> Nat.nat **)
1427let rec alignof = function
1428| Tvoid -> Nat.S Nat.O
1429| Tint (sz, x) ->
1430  (match sz with
1431   | AST.I8 -> Nat.S Nat.O
1432   | AST.I16 -> Nat.S (Nat.S Nat.O)
1433   | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1434| Tpointer x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
1435| Tarray (t', n) -> alignof t'
1436| Tfunction (x, x0) -> Nat.S Nat.O
1437| Tstruct (x, fld) -> alignof_fields fld
1438| Tunion (x, fld) -> alignof_fields fld
1439| Tcomp_ptr x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
1440(** val alignof_fields : fieldlist -> Nat.nat **)
1441and alignof_fields = function
1442| Fnil -> Nat.S Nat.O
1443| Fcons (id, t, f') -> Nat.max (alignof t) (alignof_fields f')
1444
1445(** val sizeof : type0 -> Nat.nat **)
1446let rec sizeof t = match t with
1447| Tvoid -> Nat.S Nat.O
1448| Tint (i, x) ->
1449  (match i with
1450   | AST.I8 -> Nat.S Nat.O
1451   | AST.I16 -> Nat.S (Nat.S Nat.O)
1452   | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1453| Tpointer x -> AST.size_pointer
1454| Tarray (t', n) -> Nat.times (sizeof t') (Nat.max (Nat.S Nat.O) n)
1455| Tfunction (x, x0) -> Nat.S Nat.O
1456| Tstruct (x, fld) ->
1457  Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_struct fld Nat.O)) (alignof t)
1458| Tunion (x, fld) ->
1459  Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_union fld)) (alignof t)
1460| Tcomp_ptr x -> AST.size_pointer
1461(** val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat **)
1462and sizeof_struct fld pos =
1463  match fld with
1464  | Fnil -> pos
1465  | Fcons (id, t, fld') ->
1466    sizeof_struct fld' (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t))
1467(** val sizeof_union : fieldlist -> Nat.nat **)
1468and sizeof_union = function
1469| Fnil -> Nat.O
1470| Fcons (id, t, fld') -> Nat.max (sizeof t) (sizeof_union fld')
1471
1472(** val field_offset_rec :
1473    AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res **)
1474let rec field_offset_rec id fld pos =
1475  match fld with
1476  | Fnil ->
1477    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1478      (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
1479  | Fcons (id', t, fld') ->
1480    (match AST.ident_eq id id' with
1481     | Types.Inl _ -> Errors.OK (Coqlib.align pos (alignof t))
1482     | Types.Inr _ ->
1483       field_offset_rec id fld'
1484         (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t)))
1485
1486(** val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res **)
1487let field_offset id fld =
1488  field_offset_rec id fld Nat.O
1489
1490(** val field_type : AST.ident -> fieldlist -> type0 Errors.res **)
1491let rec field_type id = function
1492| Fnil ->
1493  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1494    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
1495| Fcons (id', t, fld') ->
1496  (match AST.ident_eq id id' with
1497   | Types.Inl _ -> Errors.OK t
1498   | Types.Inr _ -> field_type id fld')
1499
1500(** val typ_of_type : type0 -> AST.typ **)
1501let typ_of_type = function
1502| Tvoid -> AST.ASTint (AST.I32, AST.Unsigned)
1503| Tint (sz, sg) -> AST.ASTint (sz, sg)
1504| Tpointer x -> AST.ASTptr
1505| Tarray (x, x0) -> AST.ASTptr
1506| Tfunction (x, x0) -> AST.ASTptr
1507| Tstruct (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
1508| Tunion (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
1509| Tcomp_ptr x -> AST.ASTptr
1510
1511(** val opttyp_of_type : type0 -> AST.typ Types.option **)
1512let opttyp_of_type = function
1513| Tvoid -> Types.None
1514| Tint (sz, sg) -> Types.Some (AST.ASTint (sz, sg))
1515| Tpointer x -> Types.Some AST.ASTptr
1516| Tarray (x, x0) -> Types.Some AST.ASTptr
1517| Tfunction (x, x0) -> Types.Some AST.ASTptr
1518| Tstruct (x, x0) -> Types.None
1519| Tunion (x, x0) -> Types.None
1520| Tcomp_ptr x -> Types.Some AST.ASTptr
1521
1522(** val typlist_of_typelist : typelist -> AST.typ List.list **)
1523let rec typlist_of_typelist = function
1524| Tnil -> List.Nil
1525| Tcons (hd, tl0) -> List.Cons ((typ_of_type hd), (typlist_of_typelist tl0))
1526
1527type mode =
1528| By_value of AST.typ
1529| By_reference
1530| By_nothing of AST.typ
1531
1532(** val mode_rect_Type4 :
1533    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1534let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_4615 = function
1535| By_value t -> h_By_value t
1536| By_reference -> h_By_reference
1537| By_nothing t -> h_By_nothing t
1538
1539(** val mode_rect_Type5 :
1540    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1541let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_4620 = function
1542| By_value t -> h_By_value t
1543| By_reference -> h_By_reference
1544| By_nothing t -> h_By_nothing t
1545
1546(** val mode_rect_Type3 :
1547    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1548let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_4625 = function
1549| By_value t -> h_By_value t
1550| By_reference -> h_By_reference
1551| By_nothing t -> h_By_nothing t
1552
1553(** val mode_rect_Type2 :
1554    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1555let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_4630 = function
1556| By_value t -> h_By_value t
1557| By_reference -> h_By_reference
1558| By_nothing t -> h_By_nothing t
1559
1560(** val mode_rect_Type1 :
1561    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1562let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_4635 = function
1563| By_value t -> h_By_value t
1564| By_reference -> h_By_reference
1565| By_nothing t -> h_By_nothing t
1566
1567(** val mode_rect_Type0 :
1568    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1569let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_4640 = function
1570| By_value t -> h_By_value t
1571| By_reference -> h_By_reference
1572| By_nothing t -> h_By_nothing t
1573
1574(** val mode_inv_rect_Type4 :
1575    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1576    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1577let mode_inv_rect_Type4 x1 hterm h1 h2 h3 =
1578  let hcut = mode_rect_Type4 h1 h2 h3 x1 hterm in hcut __ __
1579
1580(** val mode_inv_rect_Type3 :
1581    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1582    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1583let mode_inv_rect_Type3 x1 hterm h1 h2 h3 =
1584  let hcut = mode_rect_Type3 h1 h2 h3 x1 hterm in hcut __ __
1585
1586(** val mode_inv_rect_Type2 :
1587    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1588    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1589let mode_inv_rect_Type2 x1 hterm h1 h2 h3 =
1590  let hcut = mode_rect_Type2 h1 h2 h3 x1 hterm in hcut __ __
1591
1592(** val mode_inv_rect_Type1 :
1593    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1594    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1595let mode_inv_rect_Type1 x1 hterm h1 h2 h3 =
1596  let hcut = mode_rect_Type1 h1 h2 h3 x1 hterm in hcut __ __
1597
1598(** val mode_inv_rect_Type0 :
1599    AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1600    (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1601let mode_inv_rect_Type0 x1 hterm h1 h2 h3 =
1602  let hcut = mode_rect_Type0 h1 h2 h3 x1 hterm in hcut __ __
1603
1604(** val mode_discr : AST.typ -> mode -> mode -> __ **)
1605let mode_discr a1 x y =
1606  Logic.eq_rect_Type2 x
1607    (match x with
1608     | By_value a0 -> Obj.magic (fun _ dH -> dH __)
1609     | By_reference -> Obj.magic (fun _ dH -> dH)
1610     | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y
1611
1612(** val mode_jmdiscr : AST.typ -> mode -> mode -> __ **)
1613let mode_jmdiscr a1 x y =
1614  Logic.eq_rect_Type2 x
1615    (match x with
1616     | By_value a0 -> Obj.magic (fun _ dH -> dH __)
1617     | By_reference -> Obj.magic (fun _ dH -> dH)
1618     | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y
1619
1620(** val access_mode : type0 -> mode **)
1621let access_mode = function
1622| Tvoid -> By_nothing (typ_of_type Tvoid)
1623| Tint (i, s) -> By_value (AST.ASTint (i, s))
1624| Tpointer x -> By_value AST.ASTptr
1625| Tarray (x, x0) -> By_reference
1626| Tfunction (x, x0) -> By_reference
1627| Tstruct (x, fList) -> By_nothing (typ_of_type (Tstruct (x, fList)))
1628| Tunion (x, fList) -> By_nothing (typ_of_type (Tunion (x, fList)))
1629| Tcomp_ptr x -> By_value AST.ASTptr
1630
1631(** val signature_of_type : typelist -> type0 -> AST.signature **)
1632let signature_of_type args res =
1633  { AST.sig_args = (typlist_of_typelist args); AST.sig_res =
1634    (opttyp_of_type res) }
1635
1636(** val external_function :
1637    AST.ident -> typelist -> type0 -> AST.external_function **)
1638let external_function id targs tres =
1639  { AST.ef_id = id; AST.ef_sig = (signature_of_type targs tres) }
1640
Note: See TracBrowser for help on using the repository browser.