source: extracted/cminor_syntax.ml @ 2649

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

...

File size: 41.5 KB
Line 
1open Preamble
2
3open FrontEndVal
4
5open Hide
6
7open ByteValues
8
9open GenMem
10
11open FrontEndMem
12
13open Proper
14
15open PositiveMap
16
17open Deqsets
18
19open Extralib
20
21open Lists
22
23open Identifiers
24
25open Integers
26
27open AST
28
29open Division
30
31open Arithmetic
32
33open Extranat
34
35open Vector
36
37open FoldStuff
38
39open BitVector
40
41open Z
42
43open BitVectorZ
44
45open Pointers
46
47open ErrorMessages
48
49open Option
50
51open Setoids
52
53open Monad
54
55open Positive
56
57open PreIdentifiers
58
59open Errors
60
61open Div_and_mod
62
63open Jmeq
64
65open Russell
66
67open Util
68
69open Bool
70
71open Relations
72
73open Nat
74
75open List
76
77open Hints_declaration
78
79open Core_notation
80
81open Pts
82
83open Logic
84
85open Types
86
87open Coqlib
88
89open Values
90
91open FrontEndOps
92
93open CostLabel
94
95type expr =
96| Id of AST.typ * AST.ident
97| Cst of AST.typ * FrontEndOps.constant
98| Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
99| Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation * 
100   expr * expr
101| Mem of AST.typ * expr
102| Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
103| Ecost of AST.typ * CostLabel.costlabel * expr
104
105(** val expr_rect_Type4 :
106    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
107    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
108    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
109    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
110    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
111    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
112    -> 'a1) -> AST.typ -> expr -> 'a1 **)
113let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10365 = function
114| Id (t, x_10367) -> h_Id t x_10367
115| Cst (t, x_10368) -> h_Cst t x_10368
116| Op1 (t, t', x_10370, x_10369) ->
117  h_Op1 t t' x_10370 x_10369
118    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10369)
119| Op2 (t1, t2, t', x_10373, x_10372, x_10371) ->
120  h_Op2 t1 t2 t' x_10373 x_10372 x_10371
121    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10372)
122    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10371)
123| Mem (t, x_10374) ->
124  h_Mem t x_10374
125    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
126      x_10374)
127| Cond (sz, sg, t, x_10377, x_10376, x_10375) ->
128  h_Cond sz sg t x_10377 x_10376 x_10375
129    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
130      (sz, sg)) x_10377)
131    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10376)
132    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10375)
133| Ecost (t, x_10379, x_10378) ->
134  h_Ecost t x_10379 x_10378
135    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10378)
136
137(** val expr_rect_Type3 :
138    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
139    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
140    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
141    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
142    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
143    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
144    -> 'a1) -> AST.typ -> expr -> 'a1 **)
145let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10409 = function
146| Id (t, x_10411) -> h_Id t x_10411
147| Cst (t, x_10412) -> h_Cst t x_10412
148| Op1 (t, t', x_10414, x_10413) ->
149  h_Op1 t t' x_10414 x_10413
150    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10413)
151| Op2 (t1, t2, t', x_10417, x_10416, x_10415) ->
152  h_Op2 t1 t2 t' x_10417 x_10416 x_10415
153    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10416)
154    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10415)
155| Mem (t, x_10418) ->
156  h_Mem t x_10418
157    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
158      x_10418)
159| Cond (sz, sg, t, x_10421, x_10420, x_10419) ->
160  h_Cond sz sg t x_10421 x_10420 x_10419
161    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
162      (sz, sg)) x_10421)
163    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10420)
164    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10419)
165| Ecost (t, x_10423, x_10422) ->
166  h_Ecost t x_10423 x_10422
167    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10422)
168
169(** val expr_rect_Type2 :
170    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
171    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
172    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
173    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
174    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
175    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
176    -> 'a1) -> AST.typ -> expr -> 'a1 **)
177let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10431 = function
178| Id (t, x_10433) -> h_Id t x_10433
179| Cst (t, x_10434) -> h_Cst t x_10434
180| Op1 (t, t', x_10436, x_10435) ->
181  h_Op1 t t' x_10436 x_10435
182    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10435)
183| Op2 (t1, t2, t', x_10439, x_10438, x_10437) ->
184  h_Op2 t1 t2 t' x_10439 x_10438 x_10437
185    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10438)
186    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10437)
187| Mem (t, x_10440) ->
188  h_Mem t x_10440
189    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
190      x_10440)
191| Cond (sz, sg, t, x_10443, x_10442, x_10441) ->
192  h_Cond sz sg t x_10443 x_10442 x_10441
193    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
194      (sz, sg)) x_10443)
195    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10442)
196    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10441)
197| Ecost (t, x_10445, x_10444) ->
198  h_Ecost t x_10445 x_10444
199    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10444)
200
201(** val expr_rect_Type1 :
202    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
203    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
204    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
205    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
206    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
207    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
208    -> 'a1) -> AST.typ -> expr -> 'a1 **)
209let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10453 = function
210| Id (t, x_10455) -> h_Id t x_10455
211| Cst (t, x_10456) -> h_Cst t x_10456
212| Op1 (t, t', x_10458, x_10457) ->
213  h_Op1 t t' x_10458 x_10457
214    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10457)
215| Op2 (t1, t2, t', x_10461, x_10460, x_10459) ->
216  h_Op2 t1 t2 t' x_10461 x_10460 x_10459
217    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10460)
218    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10459)
219| Mem (t, x_10462) ->
220  h_Mem t x_10462
221    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
222      x_10462)
223| Cond (sz, sg, t, x_10465, x_10464, x_10463) ->
224  h_Cond sz sg t x_10465 x_10464 x_10463
225    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
226      (sz, sg)) x_10465)
227    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10464)
228    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10463)
229| Ecost (t, x_10467, x_10466) ->
230  h_Ecost t x_10467 x_10466
231    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10466)
232
233(** val expr_rect_Type0 :
234    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
235    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
236    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
237    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
238    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
239    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
240    -> 'a1) -> AST.typ -> expr -> 'a1 **)
241let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10475 = function
242| Id (t, x_10477) -> h_Id t x_10477
243| Cst (t, x_10478) -> h_Cst t x_10478
244| Op1 (t, t', x_10480, x_10479) ->
245  h_Op1 t t' x_10480 x_10479
246    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10479)
247| Op2 (t1, t2, t', x_10483, x_10482, x_10481) ->
248  h_Op2 t1 t2 t' x_10483 x_10482 x_10481
249    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10482)
250    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10481)
251| Mem (t, x_10484) ->
252  h_Mem t x_10484
253    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
254      x_10484)
255| Cond (sz, sg, t, x_10487, x_10486, x_10485) ->
256  h_Cond sz sg t x_10487 x_10486 x_10485
257    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
258      (sz, sg)) x_10487)
259    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10486)
260    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10485)
261| Ecost (t, x_10489, x_10488) ->
262  h_Ecost t x_10489 x_10488
263    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10488)
264
265(** val expr_inv_rect_Type4 :
266    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
267    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
268    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
269    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
270    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
271    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
272    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
273    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
274    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
275    __ -> __ -> 'a1) -> 'a1 **)
276let expr_inv_rect_Type4 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
277  let hcut = expr_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
278
279(** val expr_inv_rect_Type3 :
280    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
281    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
282    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
283    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
284    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
285    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
286    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
287    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
288    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
289    __ -> __ -> 'a1) -> 'a1 **)
290let expr_inv_rect_Type3 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
291  let hcut = expr_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
292
293(** val expr_inv_rect_Type2 :
294    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
295    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
296    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
297    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
298    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
299    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
300    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
301    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
302    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
303    __ -> __ -> 'a1) -> 'a1 **)
304let expr_inv_rect_Type2 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
305  let hcut = expr_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
306
307(** val expr_inv_rect_Type1 :
308    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
309    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
310    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
311    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
312    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
313    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
314    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
315    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
316    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
317    __ -> __ -> 'a1) -> 'a1 **)
318let expr_inv_rect_Type1 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
319  let hcut = expr_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
320
321(** val expr_inv_rect_Type0 :
322    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
323    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
324    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
325    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
326    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
327    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
328    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
329    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
330    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
331    __ -> __ -> 'a1) -> 'a1 **)
332let expr_inv_rect_Type0 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
333  let hcut = expr_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
334
335(** val expr_jmdiscr : AST.typ -> expr -> expr -> __ **)
336let expr_jmdiscr a1 x y =
337  Logic.eq_rect_Type2 x
338    (match x with
339     | Id (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
340     | Cst (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
341     | Op1 (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
342     | Op2 (a0, a10, a2, a3, a4, a5) ->
343       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
344     | Mem (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
345     | Cond (a0, a10, a2, a3, a4, a5) ->
346       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
347     | Ecost (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
348
349type expr_vars = __
350
351type stmt =
352| St_skip
353| St_assign of AST.typ * AST.ident * expr
354| St_store of AST.typ * expr * expr
355| St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
356   * (AST.typ, expr) Types.dPair List.list
357| St_seq of stmt * stmt
358| St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
359| St_return of (AST.typ, expr) Types.dPair Types.option
360| St_label of PreIdentifiers.identifier * stmt
361| St_goto of PreIdentifiers.identifier
362| St_cost of CostLabel.costlabel * stmt
363
364(** val stmt_rect_Type4 :
365    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
366    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
367    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
368    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
369    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
370    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
371    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
372    -> 'a1) -> stmt -> 'a1 **)
373let rec stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
374| St_skip -> h_St_skip
375| St_assign (t, x_10660, x_10659) -> h_St_assign t x_10660 x_10659
376| St_store (t, x_10662, x_10661) -> h_St_store t x_10662 x_10661
377| St_call (x_10665, x_10664, x_10663) -> h_St_call x_10665 x_10664 x_10663
378| St_seq (x_10667, x_10666) ->
379  h_St_seq x_10667 x_10666
380    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
381      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10667)
382    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
383      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10666)
384| St_ifthenelse (sz, sg, x_10670, x_10669, x_10668) ->
385  h_St_ifthenelse sz sg x_10670 x_10669 x_10668
386    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
387      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10669)
388    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
389      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10668)
390| St_return x_10671 -> h_St_return x_10671
391| St_label (x_10673, x_10672) ->
392  h_St_label x_10673 x_10672
393    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
394      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10672)
395| St_goto x_10674 -> h_St_goto x_10674
396| St_cost (x_10676, x_10675) ->
397  h_St_cost x_10676 x_10675
398    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
399      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10675)
400
401(** val stmt_rect_Type3 :
402    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
403    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
404    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
405    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
406    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
407    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
408    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
409    -> 'a1) -> stmt -> 'a1 **)
410let rec stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
411| St_skip -> h_St_skip
412| St_assign (t, x_10718, x_10717) -> h_St_assign t x_10718 x_10717
413| St_store (t, x_10720, x_10719) -> h_St_store t x_10720 x_10719
414| St_call (x_10723, x_10722, x_10721) -> h_St_call x_10723 x_10722 x_10721
415| St_seq (x_10725, x_10724) ->
416  h_St_seq x_10725 x_10724
417    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
418      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10725)
419    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
420      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10724)
421| St_ifthenelse (sz, sg, x_10728, x_10727, x_10726) ->
422  h_St_ifthenelse sz sg x_10728 x_10727 x_10726
423    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
424      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10727)
425    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
426      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10726)
427| St_return x_10729 -> h_St_return x_10729
428| St_label (x_10731, x_10730) ->
429  h_St_label x_10731 x_10730
430    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
431      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10730)
432| St_goto x_10732 -> h_St_goto x_10732
433| St_cost (x_10734, x_10733) ->
434  h_St_cost x_10734 x_10733
435    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
436      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10733)
437
438(** val stmt_rect_Type2 :
439    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
440    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
441    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
442    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
443    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
444    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
445    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
446    -> 'a1) -> stmt -> 'a1 **)
447let rec stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
448| St_skip -> h_St_skip
449| St_assign (t, x_10747, x_10746) -> h_St_assign t x_10747 x_10746
450| St_store (t, x_10749, x_10748) -> h_St_store t x_10749 x_10748
451| St_call (x_10752, x_10751, x_10750) -> h_St_call x_10752 x_10751 x_10750
452| St_seq (x_10754, x_10753) ->
453  h_St_seq x_10754 x_10753
454    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
455      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10754)
456    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
457      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10753)
458| St_ifthenelse (sz, sg, x_10757, x_10756, x_10755) ->
459  h_St_ifthenelse sz sg x_10757 x_10756 x_10755
460    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
461      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10756)
462    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
463      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10755)
464| St_return x_10758 -> h_St_return x_10758
465| St_label (x_10760, x_10759) ->
466  h_St_label x_10760 x_10759
467    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
468      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10759)
469| St_goto x_10761 -> h_St_goto x_10761
470| St_cost (x_10763, x_10762) ->
471  h_St_cost x_10763 x_10762
472    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
473      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10762)
474
475(** val stmt_rect_Type1 :
476    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
477    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
478    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
479    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
480    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
481    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
482    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
483    -> 'a1) -> stmt -> 'a1 **)
484let rec stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
485| St_skip -> h_St_skip
486| St_assign (t, x_10776, x_10775) -> h_St_assign t x_10776 x_10775
487| St_store (t, x_10778, x_10777) -> h_St_store t x_10778 x_10777
488| St_call (x_10781, x_10780, x_10779) -> h_St_call x_10781 x_10780 x_10779
489| St_seq (x_10783, x_10782) ->
490  h_St_seq x_10783 x_10782
491    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
492      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10783)
493    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
494      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10782)
495| St_ifthenelse (sz, sg, x_10786, x_10785, x_10784) ->
496  h_St_ifthenelse sz sg x_10786 x_10785 x_10784
497    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
498      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10785)
499    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
500      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10784)
501| St_return x_10787 -> h_St_return x_10787
502| St_label (x_10789, x_10788) ->
503  h_St_label x_10789 x_10788
504    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
505      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10788)
506| St_goto x_10790 -> h_St_goto x_10790
507| St_cost (x_10792, x_10791) ->
508  h_St_cost x_10792 x_10791
509    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
510      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10791)
511
512(** val stmt_rect_Type0 :
513    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
514    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
515    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
516    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
517    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
518    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
519    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
520    -> 'a1) -> stmt -> 'a1 **)
521let rec stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
522| St_skip -> h_St_skip
523| St_assign (t, x_10805, x_10804) -> h_St_assign t x_10805 x_10804
524| St_store (t, x_10807, x_10806) -> h_St_store t x_10807 x_10806
525| St_call (x_10810, x_10809, x_10808) -> h_St_call x_10810 x_10809 x_10808
526| St_seq (x_10812, x_10811) ->
527  h_St_seq x_10812 x_10811
528    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
529      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10812)
530    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
531      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10811)
532| St_ifthenelse (sz, sg, x_10815, x_10814, x_10813) ->
533  h_St_ifthenelse sz sg x_10815 x_10814 x_10813
534    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
535      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10814)
536    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
537      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10813)
538| St_return x_10816 -> h_St_return x_10816
539| St_label (x_10818, x_10817) ->
540  h_St_label x_10818 x_10817
541    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
542      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10817)
543| St_goto x_10819 -> h_St_goto x_10819
544| St_cost (x_10821, x_10820) ->
545  h_St_cost x_10821 x_10820
546    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
547      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10820)
548
549(** val stmt_inv_rect_Type4 :
550    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
551    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
552    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
553    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
554    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
555    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
556    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
557    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
558    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
559let stmt_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
560  let hcut = stmt_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
561
562(** val stmt_inv_rect_Type3 :
563    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
564    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
565    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
566    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
567    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
568    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
569    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
570    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
571    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
572let stmt_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
573  let hcut = stmt_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
574
575(** val stmt_inv_rect_Type2 :
576    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
577    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
578    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
579    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
580    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
581    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
582    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
583    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
584    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
585let stmt_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
586  let hcut = stmt_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
587
588(** val stmt_inv_rect_Type1 :
589    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
590    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
591    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
592    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
593    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
594    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
595    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
596    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
597    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
598let stmt_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
599  let hcut = stmt_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
600
601(** val stmt_inv_rect_Type0 :
602    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
603    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
604    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
605    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
606    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
607    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
608    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
609    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
610    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
611let stmt_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
612  let hcut = stmt_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
613
614(** val stmt_discr : stmt -> stmt -> __ **)
615let stmt_discr x y =
616  Logic.eq_rect_Type2 x
617    (match x with
618     | St_skip -> Obj.magic (fun _ dH -> dH)
619     | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
620     | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
621     | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
622     | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
623     | St_ifthenelse (a0, a1, a2, a3, a4) ->
624       Obj.magic (fun _ dH -> dH __ __ __ __ __)
625     | St_return a0 -> Obj.magic (fun _ dH -> dH __)
626     | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
627     | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
628     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
629
630(** val stmt_jmdiscr : stmt -> stmt -> __ **)
631let stmt_jmdiscr x y =
632  Logic.eq_rect_Type2 x
633    (match x with
634     | St_skip -> Obj.magic (fun _ dH -> dH)
635     | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
636     | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
637     | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
638     | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
639     | St_ifthenelse (a0, a1, a2, a3, a4) ->
640       Obj.magic (fun _ dH -> dH __ __ __ __ __)
641     | St_return a0 -> Obj.magic (fun _ dH -> dH __)
642     | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
643     | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
644     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
645
646type stmt_P = __
647
648(** val labels_of : stmt -> PreIdentifiers.identifier List.list **)
649let rec labels_of = function
650| St_skip -> List.Nil
651| St_assign (x, x0, x1) -> List.Nil
652| St_store (x, x0, x1) -> List.Nil
653| St_call (x, x0, x1) -> List.Nil
654| St_seq (s1, s2) -> List.append (labels_of s1) (labels_of s2)
655| St_ifthenelse (x, x0, x1, s1, s2) ->
656  List.append (labels_of s1) (labels_of s2)
657| St_return x -> List.Nil
658| St_label (l, s0) -> List.Cons (l, (labels_of s0))
659| St_goto x -> List.Nil
660| St_cost (x, s0) -> labels_of s0
661
662(** val cminor_stmt_inv_rect_Type4 :
663    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
664    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
665    'a1 **)
666let rec cminor_stmt_inv_rect_Type4 env labels rettyp s h_mk_cminor_stmt_inv =
667  h_mk_cminor_stmt_inv __ __ __
668
669(** val cminor_stmt_inv_rect_Type5 :
670    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
671    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
672    'a1 **)
673let rec cminor_stmt_inv_rect_Type5 env labels rettyp s h_mk_cminor_stmt_inv =
674  h_mk_cminor_stmt_inv __ __ __
675
676(** val cminor_stmt_inv_rect_Type3 :
677    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
678    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
679    'a1 **)
680let rec cminor_stmt_inv_rect_Type3 env labels rettyp s h_mk_cminor_stmt_inv =
681  h_mk_cminor_stmt_inv __ __ __
682
683(** val cminor_stmt_inv_rect_Type2 :
684    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
685    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
686    'a1 **)
687let rec cminor_stmt_inv_rect_Type2 env labels rettyp s h_mk_cminor_stmt_inv =
688  h_mk_cminor_stmt_inv __ __ __
689
690(** val cminor_stmt_inv_rect_Type1 :
691    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
692    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
693    'a1 **)
694let rec cminor_stmt_inv_rect_Type1 env labels rettyp s h_mk_cminor_stmt_inv =
695  h_mk_cminor_stmt_inv __ __ __
696
697(** val cminor_stmt_inv_rect_Type0 :
698    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
699    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
700    'a1 **)
701let rec cminor_stmt_inv_rect_Type0 env labels rettyp s h_mk_cminor_stmt_inv =
702  h_mk_cminor_stmt_inv __ __ __
703
704(** val cminor_stmt_inv_inv_rect_Type4 :
705    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
706    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
707    'a1) -> 'a1 **)
708let cminor_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
709  let hcut = cminor_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __
710
711(** val cminor_stmt_inv_inv_rect_Type3 :
712    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
713    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
714    'a1) -> 'a1 **)
715let cminor_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
716  let hcut = cminor_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __
717
718(** val cminor_stmt_inv_inv_rect_Type2 :
719    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
720    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
721    'a1) -> 'a1 **)
722let cminor_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
723  let hcut = cminor_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __
724
725(** val cminor_stmt_inv_inv_rect_Type1 :
726    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
727    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
728    'a1) -> 'a1 **)
729let cminor_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
730  let hcut = cminor_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __
731
732(** val cminor_stmt_inv_inv_rect_Type0 :
733    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
734    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
735    'a1) -> 'a1 **)
736let cminor_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
737  let hcut = cminor_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __
738
739(** val cminor_stmt_inv_discr :
740    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
741    List.list -> AST.typ Types.option -> stmt -> __ **)
742let cminor_stmt_inv_discr a1 a2 a3 a4 =
743  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
744
745(** val cminor_stmt_inv_jmdiscr :
746    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
747    List.list -> AST.typ Types.option -> stmt -> __ **)
748let cminor_stmt_inv_jmdiscr a1 a2 a3 a4 =
749  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
750
751type internal_function = { f_return : AST.typ Types.option;
752                           f_params : (AST.ident, AST.typ) Types.prod
753                                      List.list;
754                           f_vars : (AST.ident, AST.typ) Types.prod List.list;
755                           f_stacksize : Nat.nat; f_body : stmt }
756
757(** val internal_function_rect_Type4 :
758    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
759    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
760    -> 'a1) -> internal_function -> 'a1 **)
761let rec internal_function_rect_Type4 h_mk_internal_function x_11116 =
762  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
763    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11116
764  in
765  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
766    __
767
768(** val internal_function_rect_Type5 :
769    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
770    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
771    -> 'a1) -> internal_function -> 'a1 **)
772let rec internal_function_rect_Type5 h_mk_internal_function x_11118 =
773  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
774    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11118
775  in
776  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
777    __
778
779(** val internal_function_rect_Type3 :
780    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
781    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
782    -> 'a1) -> internal_function -> 'a1 **)
783let rec internal_function_rect_Type3 h_mk_internal_function x_11120 =
784  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
785    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11120
786  in
787  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
788    __
789
790(** val internal_function_rect_Type2 :
791    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
792    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
793    -> 'a1) -> internal_function -> 'a1 **)
794let rec internal_function_rect_Type2 h_mk_internal_function x_11122 =
795  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
796    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11122
797  in
798  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
799    __
800
801(** val internal_function_rect_Type1 :
802    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
803    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
804    -> 'a1) -> internal_function -> 'a1 **)
805let rec internal_function_rect_Type1 h_mk_internal_function x_11124 =
806  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
807    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11124
808  in
809  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
810    __
811
812(** val internal_function_rect_Type0 :
813    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
814    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
815    -> 'a1) -> internal_function -> 'a1 **)
816let rec internal_function_rect_Type0 h_mk_internal_function x_11126 =
817  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
818    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11126
819  in
820  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
821    __
822
823(** val f_return : internal_function -> AST.typ Types.option **)
824let rec f_return xxx =
825  xxx.f_return
826
827(** val f_params :
828    internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
829let rec f_params xxx =
830  xxx.f_params
831
832(** val f_vars :
833    internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
834let rec f_vars xxx =
835  xxx.f_vars
836
837(** val f_stacksize : internal_function -> Nat.nat **)
838let rec f_stacksize xxx =
839  xxx.f_stacksize
840
841(** val f_body : internal_function -> stmt **)
842let rec f_body xxx =
843  xxx.f_body
844
845(** val internal_function_inv_rect_Type4 :
846    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
847    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
848    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
849let internal_function_inv_rect_Type4 hterm h1 =
850  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
851
852(** val internal_function_inv_rect_Type3 :
853    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
854    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
855    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
856let internal_function_inv_rect_Type3 hterm h1 =
857  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
858
859(** val internal_function_inv_rect_Type2 :
860    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
861    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
862    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
863let internal_function_inv_rect_Type2 hterm h1 =
864  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
865
866(** val internal_function_inv_rect_Type1 :
867    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
868    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
869    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
870let internal_function_inv_rect_Type1 hterm h1 =
871  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
872
873(** val internal_function_inv_rect_Type0 :
874    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
875    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
876    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
877let internal_function_inv_rect_Type0 hterm h1 =
878  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
879
880(** val internal_function_jmdiscr :
881    internal_function -> internal_function -> __ **)
882let internal_function_jmdiscr x y =
883  Logic.eq_rect_Type2 x
884    (let { f_return = a0; f_params = a1; f_vars = a2; f_stacksize = a4;
885       f_body = a5 } = x
886     in
887    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
888
889type cminor_program =
890  (internal_function AST.fundef, AST.init_data List.list) AST.program
891
892type cminor_noinit_program =
893  (internal_function AST.fundef, Nat.nat) AST.program
894
Note: See TracBrowser for help on using the repository browser.