source: extracted/cminor_syntax.ml @ 2890

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

Everything extracted again.

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_13746 = function
116| Id (t, x_13748) -> h_Id t x_13748
117| Cst (t, x_13749) -> h_Cst t x_13749
118| Op1 (t, t', x_13751, x_13750) ->
119  h_Op1 t t' x_13751 x_13750
120    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13750)
121| Op2 (t1, t2, t', x_13754, x_13753, x_13752) ->
122  h_Op2 t1 t2 t' x_13754 x_13753 x_13752
123    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13753)
124    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13752)
125| Mem (t, x_13755) ->
126  h_Mem t x_13755
127    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
128      x_13755)
129| Cond (sz, sg, t, x_13758, x_13757, x_13756) ->
130  h_Cond sz sg t x_13758 x_13757 x_13756
131    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
132      (sz, sg)) x_13758)
133    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13757)
134    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13756)
135| Ecost (t, x_13760, x_13759) ->
136  h_Ecost t x_13760 x_13759
137    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13759)
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_13790 = function
148| Id (t, x_13792) -> h_Id t x_13792
149| Cst (t, x_13793) -> h_Cst t x_13793
150| Op1 (t, t', x_13795, x_13794) ->
151  h_Op1 t t' x_13795 x_13794
152    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13794)
153| Op2 (t1, t2, t', x_13798, x_13797, x_13796) ->
154  h_Op2 t1 t2 t' x_13798 x_13797 x_13796
155    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13797)
156    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13796)
157| Mem (t, x_13799) ->
158  h_Mem t x_13799
159    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
160      x_13799)
161| Cond (sz, sg, t, x_13802, x_13801, x_13800) ->
162  h_Cond sz sg t x_13802 x_13801 x_13800
163    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
164      (sz, sg)) x_13802)
165    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13801)
166    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13800)
167| Ecost (t, x_13804, x_13803) ->
168  h_Ecost t x_13804 x_13803
169    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13803)
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_13812 = function
180| Id (t, x_13814) -> h_Id t x_13814
181| Cst (t, x_13815) -> h_Cst t x_13815
182| Op1 (t, t', x_13817, x_13816) ->
183  h_Op1 t t' x_13817 x_13816
184    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13816)
185| Op2 (t1, t2, t', x_13820, x_13819, x_13818) ->
186  h_Op2 t1 t2 t' x_13820 x_13819 x_13818
187    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13819)
188    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13818)
189| Mem (t, x_13821) ->
190  h_Mem t x_13821
191    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
192      x_13821)
193| Cond (sz, sg, t, x_13824, x_13823, x_13822) ->
194  h_Cond sz sg t x_13824 x_13823 x_13822
195    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
196      (sz, sg)) x_13824)
197    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13823)
198    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13822)
199| Ecost (t, x_13826, x_13825) ->
200  h_Ecost t x_13826 x_13825
201    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13825)
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_13834 = function
212| Id (t, x_13836) -> h_Id t x_13836
213| Cst (t, x_13837) -> h_Cst t x_13837
214| Op1 (t, t', x_13839, x_13838) ->
215  h_Op1 t t' x_13839 x_13838
216    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13838)
217| Op2 (t1, t2, t', x_13842, x_13841, x_13840) ->
218  h_Op2 t1 t2 t' x_13842 x_13841 x_13840
219    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13841)
220    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13840)
221| Mem (t, x_13843) ->
222  h_Mem t x_13843
223    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
224      x_13843)
225| Cond (sz, sg, t, x_13846, x_13845, x_13844) ->
226  h_Cond sz sg t x_13846 x_13845 x_13844
227    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
228      (sz, sg)) x_13846)
229    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13845)
230    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13844)
231| Ecost (t, x_13848, x_13847) ->
232  h_Ecost t x_13848 x_13847
233    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13847)
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_13856 = function
244| Id (t, x_13858) -> h_Id t x_13858
245| Cst (t, x_13859) -> h_Cst t x_13859
246| Op1 (t, t', x_13861, x_13860) ->
247  h_Op1 t t' x_13861 x_13860
248    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13860)
249| Op2 (t1, t2, t', x_13864, x_13863, x_13862) ->
250  h_Op2 t1 t2 t' x_13864 x_13863 x_13862
251    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13863)
252    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13862)
253| Mem (t, x_13865) ->
254  h_Mem t x_13865
255    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
256      x_13865)
257| Cond (sz, sg, t, x_13868, x_13867, x_13866) ->
258  h_Cond sz sg t x_13868 x_13867 x_13866
259    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
260      (sz, sg)) x_13868)
261    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13867)
262    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13866)
263| Ecost (t, x_13870, x_13869) ->
264  h_Ecost t x_13870 x_13869
265    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13869)
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_14041, x_14040) -> h_St_assign t x_14041 x_14040
376| St_store (t, x_14043, x_14042) -> h_St_store t x_14043 x_14042
377| St_call (x_14046, x_14045, x_14044) -> h_St_call x_14046 x_14045 x_14044
378| St_seq (x_14048, x_14047) ->
379  h_St_seq x_14048 x_14047
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_14048)
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_14047)
384| St_ifthenelse (sz, sg, x_14051, x_14050, x_14049) ->
385  h_St_ifthenelse sz sg x_14051 x_14050 x_14049
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_14050)
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_14049)
390| St_return x_14052 -> h_St_return x_14052
391| St_label (x_14054, x_14053) ->
392  h_St_label x_14054 x_14053
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_14053)
395| St_goto x_14055 -> h_St_goto x_14055
396| St_cost (x_14057, x_14056) ->
397  h_St_cost x_14057 x_14056
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_14056)
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_14099, x_14098) -> h_St_assign t x_14099 x_14098
413| St_store (t, x_14101, x_14100) -> h_St_store t x_14101 x_14100
414| St_call (x_14104, x_14103, x_14102) -> h_St_call x_14104 x_14103 x_14102
415| St_seq (x_14106, x_14105) ->
416  h_St_seq x_14106 x_14105
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_14106)
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_14105)
421| St_ifthenelse (sz, sg, x_14109, x_14108, x_14107) ->
422  h_St_ifthenelse sz sg x_14109 x_14108 x_14107
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_14108)
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_14107)
427| St_return x_14110 -> h_St_return x_14110
428| St_label (x_14112, x_14111) ->
429  h_St_label x_14112 x_14111
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_14111)
432| St_goto x_14113 -> h_St_goto x_14113
433| St_cost (x_14115, x_14114) ->
434  h_St_cost x_14115 x_14114
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_14114)
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_14128, x_14127) -> h_St_assign t x_14128 x_14127
450| St_store (t, x_14130, x_14129) -> h_St_store t x_14130 x_14129
451| St_call (x_14133, x_14132, x_14131) -> h_St_call x_14133 x_14132 x_14131
452| St_seq (x_14135, x_14134) ->
453  h_St_seq x_14135 x_14134
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_14135)
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_14134)
458| St_ifthenelse (sz, sg, x_14138, x_14137, x_14136) ->
459  h_St_ifthenelse sz sg x_14138 x_14137 x_14136
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_14137)
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_14136)
464| St_return x_14139 -> h_St_return x_14139
465| St_label (x_14141, x_14140) ->
466  h_St_label x_14141 x_14140
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_14140)
469| St_goto x_14142 -> h_St_goto x_14142
470| St_cost (x_14144, x_14143) ->
471  h_St_cost x_14144 x_14143
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_14143)
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_14157, x_14156) -> h_St_assign t x_14157 x_14156
487| St_store (t, x_14159, x_14158) -> h_St_store t x_14159 x_14158
488| St_call (x_14162, x_14161, x_14160) -> h_St_call x_14162 x_14161 x_14160
489| St_seq (x_14164, x_14163) ->
490  h_St_seq x_14164 x_14163
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_14164)
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_14163)
495| St_ifthenelse (sz, sg, x_14167, x_14166, x_14165) ->
496  h_St_ifthenelse sz sg x_14167 x_14166 x_14165
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_14166)
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_14165)
501| St_return x_14168 -> h_St_return x_14168
502| St_label (x_14170, x_14169) ->
503  h_St_label x_14170 x_14169
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_14169)
506| St_goto x_14171 -> h_St_goto x_14171
507| St_cost (x_14173, x_14172) ->
508  h_St_cost x_14173 x_14172
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_14172)
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_14186, x_14185) -> h_St_assign t x_14186 x_14185
524| St_store (t, x_14188, x_14187) -> h_St_store t x_14188 x_14187
525| St_call (x_14191, x_14190, x_14189) -> h_St_call x_14191 x_14190 x_14189
526| St_seq (x_14193, x_14192) ->
527  h_St_seq x_14193 x_14192
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_14193)
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_14192)
532| St_ifthenelse (sz, sg, x_14196, x_14195, x_14194) ->
533  h_St_ifthenelse sz sg x_14196 x_14195 x_14194
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_14195)
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_14194)
538| St_return x_14197 -> h_St_return x_14197
539| St_label (x_14199, x_14198) ->
540  h_St_label x_14199 x_14198
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_14198)
543| St_goto x_14200 -> h_St_goto x_14200
544| St_cost (x_14202, x_14201) ->
545  h_St_cost x_14202 x_14201
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_14201)
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_14497 =
760  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
761    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14497
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_14499 =
771  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
772    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14499
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_14501 =
782  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
783    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14501
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_14503 =
793  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
794    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14503
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_14505 =
804  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
805    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14505
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_14507 =
815  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
816    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14507
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.