source: extracted/csyntax.ml @ 2968

Last change on this file since 2968 was 2827, checked in by sacerdot, 7 years ago

Everything extracted again.

File size: 56.6 KB
RevLine 
[2601]1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
[2649]9open ErrorMessages
10
[2601]11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Lists
18
19open Positive
20
21open Identifiers
22
[2717]23open Exp
24
[2601]25open Arithmetic
26
27open Vector
28
29open Div_and_mod
30
[2773]31open Util
32
33open FoldStuff
34
35open BitVector
36
[2601]37open Jmeq
38
39open Russell
40
41open List
42
[2773]43open Setoids
[2601]44
[2773]45open Monad
[2601]46
[2773]47open Option
[2601]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
[2649]71open Coqlib
72
[2601]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
[2773]446| One
[2601]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
[2773]467| One -> h_One
[2601]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
[2773]488| One -> h_One
[2601]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
[2773]509| One -> h_One
[2601]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
[2773]530| One -> h_One
[2601]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
[2773]551| One -> h_One
[2601]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
[2773]572| One -> h_One
[2601]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)
[2773]654     | One -> Obj.magic (fun _ dH -> dH)
[2601]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)
[2773]676     | One -> Obj.magic (fun _ dH -> dH)
[2601]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 **)
[2827]1205let rec function_rect_Type4 h_mk_function x_4482 =
[2601]1206  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
[2827]1207    fn_body = fn_body0 } = x_4482
[2601]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 **)
[2827]1214let rec function_rect_Type5 h_mk_function x_4484 =
[2601]1215  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
[2827]1216    fn_body = fn_body0 } = x_4484
[2601]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 **)
[2827]1223let rec function_rect_Type3 h_mk_function x_4486 =
[2601]1224  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
[2827]1225    fn_body = fn_body0 } = x_4486
[2601]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 **)
[2827]1232let rec function_rect_Type2 h_mk_function x_4488 =
[2601]1233  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
[2827]1234    fn_body = fn_body0 } = x_4488
[2601]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 **)
[2827]1241let rec function_rect_Type1 h_mk_function x_4490 =
[2601]1242  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
[2827]1243    fn_body = fn_body0 } = x_4490
[2601]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 **)
[2827]1250let rec function_rect_Type0 h_mk_function x_4492 =
[2601]1251  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
[2827]1252    fn_body = fn_body0 } = x_4492
[2601]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
[2827]1324| CL_Internal x_4514 -> h_CL_Internal x_4514
1325| CL_External (x_4517, x_4516, x_4515) -> h_CL_External x_4517 x_4516 x_4515
[2601]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
[2827]1331| CL_Internal x_4521 -> h_CL_Internal x_4521
1332| CL_External (x_4524, x_4523, x_4522) -> h_CL_External x_4524 x_4523 x_4522
[2601]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
[2827]1338| CL_Internal x_4528 -> h_CL_Internal x_4528
1339| CL_External (x_4531, x_4530, x_4529) -> h_CL_External x_4531 x_4530 x_4529
[2601]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
[2827]1345| CL_Internal x_4535 -> h_CL_Internal x_4535
1346| CL_External (x_4538, x_4537, x_4536) -> h_CL_External x_4538 x_4537 x_4536
[2601]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
[2827]1352| CL_Internal x_4542 -> h_CL_Internal x_4542
1353| CL_External (x_4545, x_4544, x_4543) -> h_CL_External x_4545 x_4544 x_4543
[2601]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
[2827]1359| CL_Internal x_4549 -> h_CL_Internal x_4549
1360| CL_External (x_4552, x_4551, x_4550) -> h_CL_External x_4552 x_4551 x_4550
[2601]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
[2773]1424| CL_External (id, args, res) -> Tfunction (args, res)
[2601]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 **)
[2773]1462and sizeof_struct fld pos =
[2601]1463  match fld with
[2773]1464  | Fnil -> pos
[2601]1465  | Fcons (id, t, fld') ->
[2773]1466    sizeof_struct fld' (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t))
[2601]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 **)
[2773]1474let rec field_offset_rec id fld pos =
[2601]1475  match fld with
1476  | Fnil ->
[2649]1477    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1478      (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
[2601]1479  | Fcons (id', t, fld') ->
1480    (match AST.ident_eq id id' with
[2773]1481     | Types.Inl _ -> Errors.OK (Coqlib.align pos (alignof t))
[2601]1482     | Types.Inr _ ->
1483       field_offset_rec id fld'
[2773]1484         (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t)))
[2601]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 ->
[2649]1493  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1494    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
[2601]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
[2773]1525| Tcons (hd, tl0) -> List.Cons ((typ_of_type hd), (typlist_of_typelist tl0))
[2601]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 **)
[2827]1534let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_4602 = function
[2601]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 **)
[2827]1541let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_4607 = function
[2601]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 **)
[2827]1548let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_4612 = function
[2601]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 **)
[2827]1555let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_4617 = function
[2601]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 **)
[2827]1562let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_4622 = function
[2601]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 **)
[2827]1569let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_4627 = function
[2601]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 **)
[2773]1632let signature_of_type args res =
[2601]1633  { AST.sig_args = (typlist_of_typelist args); AST.sig_res =
[2773]1634    (opttyp_of_type res) }
[2601]1635
[2773]1636(** val external_function :
[2601]1637    AST.ident -> typelist -> type0 -> AST.external_function **)
[2773]1638let external_function id targs tres =
[2601]1639  { AST.ef_id = id; AST.ef_sig = (signature_of_type targs tres) }
1640
Note: See TracBrowser for help on using the repository browser.