source: driver/extracted/cminor_syntax.ml

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

New extraction

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 Exp
32
33open Arithmetic
34
35open Extranat
36
37open Vector
38
39open FoldStuff
40
41open BitVector
42
43open Z
44
45open BitVectorZ
46
47open Pointers
48
49open ErrorMessages
50
51open Option
52
53open Setoids
54
55open Monad
56
57open Positive
58
59open PreIdentifiers
60
61open Errors
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open Util
70
71open Bool
72
73open Relations
74
75open Nat
76
77open List
78
79open Hints_declaration
80
81open Core_notation
82
83open Pts
84
85open Logic
86
87open Types
88
89open Coqlib
90
91open Values
92
93open FrontEndOps
94
95open CostLabel
96
97type expr =
98| Id of AST.typ * AST.ident
99| Cst of AST.typ * FrontEndOps.constant
100| Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
101| Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation * 
102   expr * expr
103| Mem of AST.typ * expr
104| Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
105| Ecost of AST.typ * CostLabel.costlabel * expr
106
107(** val expr_rect_Type4 :
108    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
109    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
110    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
111    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
112    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
113    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
114    -> 'a1) -> AST.typ -> expr -> 'a1 **)
115let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13742 = function
116| Id (t, x_13744) -> h_Id t x_13744
117| Cst (t, x_13745) -> h_Cst t x_13745
118| Op1 (t, t', x_13747, x_13746) ->
119  h_Op1 t t' x_13747 x_13746
120    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13746)
121| Op2 (t1, t2, t', x_13750, x_13749, x_13748) ->
122  h_Op2 t1 t2 t' x_13750 x_13749 x_13748
123    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13749)
124    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13748)
125| Mem (t, x_13751) ->
126  h_Mem t x_13751
127    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
128      x_13751)
129| Cond (sz, sg, t, x_13754, x_13753, x_13752) ->
130  h_Cond sz sg t x_13754 x_13753 x_13752
131    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
132      (sz, sg)) x_13754)
133    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13753)
134    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13752)
135| Ecost (t, x_13756, x_13755) ->
136  h_Ecost t x_13756 x_13755
137    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13755)
138
139(** val expr_rect_Type3 :
140    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
141    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
142    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
143    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
144    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
145    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
146    -> 'a1) -> AST.typ -> expr -> 'a1 **)
147let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13786 = function
148| Id (t, x_13788) -> h_Id t x_13788
149| Cst (t, x_13789) -> h_Cst t x_13789
150| Op1 (t, t', x_13791, x_13790) ->
151  h_Op1 t t' x_13791 x_13790
152    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13790)
153| Op2 (t1, t2, t', x_13794, x_13793, x_13792) ->
154  h_Op2 t1 t2 t' x_13794 x_13793 x_13792
155    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13793)
156    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13792)
157| Mem (t, x_13795) ->
158  h_Mem t x_13795
159    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
160      x_13795)
161| Cond (sz, sg, t, x_13798, x_13797, x_13796) ->
162  h_Cond sz sg t x_13798 x_13797 x_13796
163    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
164      (sz, sg)) x_13798)
165    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13797)
166    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13796)
167| Ecost (t, x_13800, x_13799) ->
168  h_Ecost t x_13800 x_13799
169    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13799)
170
171(** val expr_rect_Type2 :
172    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
173    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
174    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
175    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
176    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
177    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
178    -> 'a1) -> AST.typ -> expr -> 'a1 **)
179let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13808 = function
180| Id (t, x_13810) -> h_Id t x_13810
181| Cst (t, x_13811) -> h_Cst t x_13811
182| Op1 (t, t', x_13813, x_13812) ->
183  h_Op1 t t' x_13813 x_13812
184    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13812)
185| Op2 (t1, t2, t', x_13816, x_13815, x_13814) ->
186  h_Op2 t1 t2 t' x_13816 x_13815 x_13814
187    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13815)
188    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13814)
189| Mem (t, x_13817) ->
190  h_Mem t x_13817
191    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
192      x_13817)
193| Cond (sz, sg, t, x_13820, x_13819, x_13818) ->
194  h_Cond sz sg t x_13820 x_13819 x_13818
195    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
196      (sz, sg)) x_13820)
197    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13819)
198    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13818)
199| Ecost (t, x_13822, x_13821) ->
200  h_Ecost t x_13822 x_13821
201    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13821)
202
203(** val expr_rect_Type1 :
204    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
205    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
206    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
207    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
208    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
209    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
210    -> 'a1) -> AST.typ -> expr -> 'a1 **)
211let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13830 = function
212| Id (t, x_13832) -> h_Id t x_13832
213| Cst (t, x_13833) -> h_Cst t x_13833
214| Op1 (t, t', x_13835, x_13834) ->
215  h_Op1 t t' x_13835 x_13834
216    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13834)
217| Op2 (t1, t2, t', x_13838, x_13837, x_13836) ->
218  h_Op2 t1 t2 t' x_13838 x_13837 x_13836
219    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13837)
220    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13836)
221| Mem (t, x_13839) ->
222  h_Mem t x_13839
223    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
224      x_13839)
225| Cond (sz, sg, t, x_13842, x_13841, x_13840) ->
226  h_Cond sz sg t x_13842 x_13841 x_13840
227    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
228      (sz, sg)) x_13842)
229    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13841)
230    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13840)
231| Ecost (t, x_13844, x_13843) ->
232  h_Ecost t x_13844 x_13843
233    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13843)
234
235(** val expr_rect_Type0 :
236    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
237    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
238    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
239    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
240    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
241    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
242    -> 'a1) -> AST.typ -> expr -> 'a1 **)
243let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13852 = function
244| Id (t, x_13854) -> h_Id t x_13854
245| Cst (t, x_13855) -> h_Cst t x_13855
246| Op1 (t, t', x_13857, x_13856) ->
247  h_Op1 t t' x_13857 x_13856
248    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13856)
249| Op2 (t1, t2, t', x_13860, x_13859, x_13858) ->
250  h_Op2 t1 t2 t' x_13860 x_13859 x_13858
251    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13859)
252    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13858)
253| Mem (t, x_13861) ->
254  h_Mem t x_13861
255    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
256      x_13861)
257| Cond (sz, sg, t, x_13864, x_13863, x_13862) ->
258  h_Cond sz sg t x_13864 x_13863 x_13862
259    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
260      (sz, sg)) x_13864)
261    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13863)
262    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13862)
263| Ecost (t, x_13866, x_13865) ->
264  h_Ecost t x_13866 x_13865
265    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13865)
266
267(** val expr_inv_rect_Type4 :
268    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
269    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
270    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
271    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
272    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
273    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
274    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
275    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
276    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
277    __ -> __ -> 'a1) -> 'a1 **)
278let expr_inv_rect_Type4 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
279  let hcut = expr_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
280
281(** val expr_inv_rect_Type3 :
282    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
283    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
284    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
285    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
286    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
287    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
288    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
289    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
290    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
291    __ -> __ -> 'a1) -> 'a1 **)
292let expr_inv_rect_Type3 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
293  let hcut = expr_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
294
295(** val expr_inv_rect_Type2 :
296    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
297    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
298    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
299    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
300    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
301    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
302    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
303    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
304    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
305    __ -> __ -> 'a1) -> 'a1 **)
306let expr_inv_rect_Type2 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
307  let hcut = expr_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
308
309(** val expr_inv_rect_Type1 :
310    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
311    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
312    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
313    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
314    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
315    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
316    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
317    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
318    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
319    __ -> __ -> 'a1) -> 'a1 **)
320let expr_inv_rect_Type1 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
321  let hcut = expr_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
322
323(** val expr_inv_rect_Type0 :
324    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
325    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
326    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
327    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
328    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
329    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
330    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
331    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
332    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
333    __ -> __ -> 'a1) -> 'a1 **)
334let expr_inv_rect_Type0 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
335  let hcut = expr_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
336
337(** val expr_jmdiscr : AST.typ -> expr -> expr -> __ **)
338let expr_jmdiscr a1 x y =
339  Logic.eq_rect_Type2 x
340    (match x with
341     | Id (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
342     | Cst (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
343     | Op1 (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
344     | Op2 (a0, a10, a2, a3, a4, a5) ->
345       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
346     | Mem (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
347     | Cond (a0, a10, a2, a3, a4, a5) ->
348       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
349     | Ecost (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
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_14037, x_14036) -> h_St_assign t x_14037 x_14036
376| St_store (t, x_14039, x_14038) -> h_St_store t x_14039 x_14038
377| St_call (x_14042, x_14041, x_14040) -> h_St_call x_14042 x_14041 x_14040
378| St_seq (x_14044, x_14043) ->
379  h_St_seq x_14044 x_14043
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_14044)
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_14043)
384| St_ifthenelse (sz, sg, x_14047, x_14046, x_14045) ->
385  h_St_ifthenelse sz sg x_14047 x_14046 x_14045
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_14046)
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_14045)
390| St_return x_14048 -> h_St_return x_14048
391| St_label (x_14050, x_14049) ->
392  h_St_label x_14050 x_14049
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_14049)
395| St_goto x_14051 -> h_St_goto x_14051
396| St_cost (x_14053, x_14052) ->
397  h_St_cost x_14053 x_14052
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_14052)
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_14095, x_14094) -> h_St_assign t x_14095 x_14094
413| St_store (t, x_14097, x_14096) -> h_St_store t x_14097 x_14096
414| St_call (x_14100, x_14099, x_14098) -> h_St_call x_14100 x_14099 x_14098
415| St_seq (x_14102, x_14101) ->
416  h_St_seq x_14102 x_14101
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_14102)
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_14101)
421| St_ifthenelse (sz, sg, x_14105, x_14104, x_14103) ->
422  h_St_ifthenelse sz sg x_14105 x_14104 x_14103
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_14104)
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_14103)
427| St_return x_14106 -> h_St_return x_14106
428| St_label (x_14108, x_14107) ->
429  h_St_label x_14108 x_14107
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_14107)
432| St_goto x_14109 -> h_St_goto x_14109
433| St_cost (x_14111, x_14110) ->
434  h_St_cost x_14111 x_14110
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_14110)
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_14124, x_14123) -> h_St_assign t x_14124 x_14123
450| St_store (t, x_14126, x_14125) -> h_St_store t x_14126 x_14125
451| St_call (x_14129, x_14128, x_14127) -> h_St_call x_14129 x_14128 x_14127
452| St_seq (x_14131, x_14130) ->
453  h_St_seq x_14131 x_14130
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_14131)
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_14130)
458| St_ifthenelse (sz, sg, x_14134, x_14133, x_14132) ->
459  h_St_ifthenelse sz sg x_14134 x_14133 x_14132
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_14133)
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_14132)
464| St_return x_14135 -> h_St_return x_14135
465| St_label (x_14137, x_14136) ->
466  h_St_label x_14137 x_14136
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_14136)
469| St_goto x_14138 -> h_St_goto x_14138
470| St_cost (x_14140, x_14139) ->
471  h_St_cost x_14140 x_14139
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_14139)
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_14153, x_14152) -> h_St_assign t x_14153 x_14152
487| St_store (t, x_14155, x_14154) -> h_St_store t x_14155 x_14154
488| St_call (x_14158, x_14157, x_14156) -> h_St_call x_14158 x_14157 x_14156
489| St_seq (x_14160, x_14159) ->
490  h_St_seq x_14160 x_14159
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_14160)
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_14159)
495| St_ifthenelse (sz, sg, x_14163, x_14162, x_14161) ->
496  h_St_ifthenelse sz sg x_14163 x_14162 x_14161
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_14162)
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_14161)
501| St_return x_14164 -> h_St_return x_14164
502| St_label (x_14166, x_14165) ->
503  h_St_label x_14166 x_14165
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_14165)
506| St_goto x_14167 -> h_St_goto x_14167
507| St_cost (x_14169, x_14168) ->
508  h_St_cost x_14169 x_14168
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_14168)
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_14182, x_14181) -> h_St_assign t x_14182 x_14181
524| St_store (t, x_14184, x_14183) -> h_St_store t x_14184 x_14183
525| St_call (x_14187, x_14186, x_14185) -> h_St_call x_14187 x_14186 x_14185
526| St_seq (x_14189, x_14188) ->
527  h_St_seq x_14189 x_14188
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_14189)
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_14188)
532| St_ifthenelse (sz, sg, x_14192, x_14191, x_14190) ->
533  h_St_ifthenelse sz sg x_14192 x_14191 x_14190
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_14191)
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_14190)
538| St_return x_14193 -> h_St_return x_14193
539| St_label (x_14195, x_14194) ->
540  h_St_label x_14195 x_14194
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_14194)
543| St_goto x_14196 -> h_St_goto x_14196
544| St_cost (x_14198, x_14197) ->
545  h_St_cost x_14198 x_14197
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_14197)
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
646(** val labels_of : stmt -> PreIdentifiers.identifier List.list **)
647let rec labels_of = function
648| St_skip -> List.Nil
649| St_assign (x, x0, x1) -> List.Nil
650| St_store (x, x0, x1) -> List.Nil
651| St_call (x, x0, x1) -> List.Nil
652| St_seq (s1, s2) -> List.append (labels_of s1) (labels_of s2)
653| St_ifthenelse (x, x0, x1, s1, s2) ->
654  List.append (labels_of s1) (labels_of s2)
655| St_return x -> List.Nil
656| St_label (l, s0) -> List.Cons (l, (labels_of s0))
657| St_goto x -> List.Nil
658| St_cost (x, s0) -> labels_of s0
659
660(** val cminor_stmt_inv_rect_Type4 :
661    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
662    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
663    'a1 **)
664let rec cminor_stmt_inv_rect_Type4 env labels rettyp s h_mk_cminor_stmt_inv =
665  h_mk_cminor_stmt_inv __ __ __
666
667(** val cminor_stmt_inv_rect_Type5 :
668    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
669    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
670    'a1 **)
671let rec cminor_stmt_inv_rect_Type5 env labels rettyp s h_mk_cminor_stmt_inv =
672  h_mk_cminor_stmt_inv __ __ __
673
674(** val cminor_stmt_inv_rect_Type3 :
675    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
676    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
677    'a1 **)
678let rec cminor_stmt_inv_rect_Type3 env labels rettyp s h_mk_cminor_stmt_inv =
679  h_mk_cminor_stmt_inv __ __ __
680
681(** val cminor_stmt_inv_rect_Type2 :
682    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
683    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
684    'a1 **)
685let rec cminor_stmt_inv_rect_Type2 env labels rettyp s h_mk_cminor_stmt_inv =
686  h_mk_cminor_stmt_inv __ __ __
687
688(** val cminor_stmt_inv_rect_Type1 :
689    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
690    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
691    'a1 **)
692let rec cminor_stmt_inv_rect_Type1 env labels rettyp s h_mk_cminor_stmt_inv =
693  h_mk_cminor_stmt_inv __ __ __
694
695(** val cminor_stmt_inv_rect_Type0 :
696    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
697    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
698    'a1 **)
699let rec cminor_stmt_inv_rect_Type0 env labels rettyp s h_mk_cminor_stmt_inv =
700  h_mk_cminor_stmt_inv __ __ __
701
702(** val cminor_stmt_inv_inv_rect_Type4 :
703    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
704    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
705    'a1) -> 'a1 **)
706let cminor_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
707  let hcut = cminor_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __
708
709(** val cminor_stmt_inv_inv_rect_Type3 :
710    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
711    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
712    'a1) -> 'a1 **)
713let cminor_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
714  let hcut = cminor_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __
715
716(** val cminor_stmt_inv_inv_rect_Type2 :
717    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
718    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
719    'a1) -> 'a1 **)
720let cminor_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
721  let hcut = cminor_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __
722
723(** val cminor_stmt_inv_inv_rect_Type1 :
724    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
725    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
726    'a1) -> 'a1 **)
727let cminor_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
728  let hcut = cminor_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __
729
730(** val cminor_stmt_inv_inv_rect_Type0 :
731    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
732    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
733    'a1) -> 'a1 **)
734let cminor_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
735  let hcut = cminor_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __
736
737(** val cminor_stmt_inv_discr :
738    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
739    List.list -> AST.typ Types.option -> stmt -> __ **)
740let cminor_stmt_inv_discr a1 a2 a3 a4 =
741  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
742
743(** val cminor_stmt_inv_jmdiscr :
744    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
745    List.list -> AST.typ Types.option -> stmt -> __ **)
746let cminor_stmt_inv_jmdiscr a1 a2 a3 a4 =
747  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
748
749type internal_function = { f_return : AST.typ Types.option;
750                           f_params : (AST.ident, AST.typ) Types.prod
751                                      List.list;
752                           f_vars : (AST.ident, AST.typ) Types.prod List.list;
753                           f_stacksize : Nat.nat; f_body : stmt }
754
755(** val internal_function_rect_Type4 :
756    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
757    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
758    -> 'a1) -> internal_function -> 'a1 **)
759let rec internal_function_rect_Type4 h_mk_internal_function x_14493 =
760  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
761    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14493
762  in
763  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
764    __
765
766(** val internal_function_rect_Type5 :
767    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
768    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
769    -> 'a1) -> internal_function -> 'a1 **)
770let rec internal_function_rect_Type5 h_mk_internal_function x_14495 =
771  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
772    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14495
773  in
774  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
775    __
776
777(** val internal_function_rect_Type3 :
778    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
779    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
780    -> 'a1) -> internal_function -> 'a1 **)
781let rec internal_function_rect_Type3 h_mk_internal_function x_14497 =
782  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
783    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14497
784  in
785  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
786    __
787
788(** val internal_function_rect_Type2 :
789    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
790    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
791    -> 'a1) -> internal_function -> 'a1 **)
792let rec internal_function_rect_Type2 h_mk_internal_function x_14499 =
793  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
794    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14499
795  in
796  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
797    __
798
799(** val internal_function_rect_Type1 :
800    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
801    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
802    -> 'a1) -> internal_function -> 'a1 **)
803let rec internal_function_rect_Type1 h_mk_internal_function x_14501 =
804  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
805    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14501
806  in
807  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
808    __
809
810(** val internal_function_rect_Type0 :
811    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
812    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
813    -> 'a1) -> internal_function -> 'a1 **)
814let rec internal_function_rect_Type0 h_mk_internal_function x_14503 =
815  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
816    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14503
817  in
818  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
819    __
820
821(** val f_return : internal_function -> AST.typ Types.option **)
822let rec f_return xxx =
823  xxx.f_return
824
825(** val f_params :
826    internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
827let rec f_params xxx =
828  xxx.f_params
829
830(** val f_vars :
831    internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
832let rec f_vars xxx =
833  xxx.f_vars
834
835(** val f_stacksize : internal_function -> Nat.nat **)
836let rec f_stacksize xxx =
837  xxx.f_stacksize
838
839(** val f_body : internal_function -> stmt **)
840let rec f_body xxx =
841  xxx.f_body
842
843(** val internal_function_inv_rect_Type4 :
844    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
845    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
846    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
847let internal_function_inv_rect_Type4 hterm h1 =
848  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
849
850(** val internal_function_inv_rect_Type3 :
851    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
852    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
853    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
854let internal_function_inv_rect_Type3 hterm h1 =
855  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
856
857(** val internal_function_inv_rect_Type2 :
858    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
859    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
860    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
861let internal_function_inv_rect_Type2 hterm h1 =
862  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
863
864(** val internal_function_inv_rect_Type1 :
865    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
866    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
867    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
868let internal_function_inv_rect_Type1 hterm h1 =
869  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
870
871(** val internal_function_inv_rect_Type0 :
872    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
873    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
874    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
875let internal_function_inv_rect_Type0 hterm h1 =
876  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
877
878(** val internal_function_jmdiscr :
879    internal_function -> internal_function -> __ **)
880let internal_function_jmdiscr x y =
881  Logic.eq_rect_Type2 x
882    (let { f_return = a0; f_params = a1; f_vars = a2; f_stacksize = a4;
883       f_body = a5 } = x
884     in
885    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
886
887type cminor_program =
888  (internal_function AST.fundef, AST.init_data List.list) AST.program
889
890type cminor_noinit_program =
891  (internal_function AST.fundef, Nat.nat) AST.program
892
Note: See TracBrowser for help on using the repository browser.