source: extracted/cminor_syntax.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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 BitVectorTrie
96
97open CostLabel
98
99type expr =
100| Id of AST.typ * AST.ident
101| Cst of AST.typ * FrontEndOps.constant
102| Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
103| Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation * 
104   expr * expr
105| Mem of AST.typ * expr
106| Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
107| Ecost of AST.typ * CostLabel.costlabel * expr
108
109(** val expr_rect_Type4 :
110    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
111    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
112    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
113    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
114    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
115    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
116    -> 'a1) -> AST.typ -> expr -> 'a1 **)
117let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13707 = function
118| Id (t, x_13709) -> h_Id t x_13709
119| Cst (t, x_13710) -> h_Cst t x_13710
120| Op1 (t, t', x_13712, x_13711) ->
121  h_Op1 t t' x_13712 x_13711
122    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13711)
123| Op2 (t1, t2, t', x_13715, x_13714, x_13713) ->
124  h_Op2 t1 t2 t' x_13715 x_13714 x_13713
125    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13714)
126    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13713)
127| Mem (t, x_13716) ->
128  h_Mem t x_13716
129    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
130      x_13716)
131| Cond (sz, sg, t, x_13719, x_13718, x_13717) ->
132  h_Cond sz sg t x_13719 x_13718 x_13717
133    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
134      (sz, sg)) x_13719)
135    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13718)
136    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13717)
137| Ecost (t, x_13721, x_13720) ->
138  h_Ecost t x_13721 x_13720
139    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13720)
140
141(** val expr_rect_Type3 :
142    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
143    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
144    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
145    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
146    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
147    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
148    -> 'a1) -> AST.typ -> expr -> 'a1 **)
149let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13751 = function
150| Id (t, x_13753) -> h_Id t x_13753
151| Cst (t, x_13754) -> h_Cst t x_13754
152| Op1 (t, t', x_13756, x_13755) ->
153  h_Op1 t t' x_13756 x_13755
154    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13755)
155| Op2 (t1, t2, t', x_13759, x_13758, x_13757) ->
156  h_Op2 t1 t2 t' x_13759 x_13758 x_13757
157    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13758)
158    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13757)
159| Mem (t, x_13760) ->
160  h_Mem t x_13760
161    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
162      x_13760)
163| Cond (sz, sg, t, x_13763, x_13762, x_13761) ->
164  h_Cond sz sg t x_13763 x_13762 x_13761
165    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
166      (sz, sg)) x_13763)
167    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13762)
168    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13761)
169| Ecost (t, x_13765, x_13764) ->
170  h_Ecost t x_13765 x_13764
171    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13764)
172
173(** val expr_rect_Type2 :
174    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
175    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
176    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
177    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
178    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
179    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
180    -> 'a1) -> AST.typ -> expr -> 'a1 **)
181let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13773 = function
182| Id (t, x_13775) -> h_Id t x_13775
183| Cst (t, x_13776) -> h_Cst t x_13776
184| Op1 (t, t', x_13778, x_13777) ->
185  h_Op1 t t' x_13778 x_13777
186    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13777)
187| Op2 (t1, t2, t', x_13781, x_13780, x_13779) ->
188  h_Op2 t1 t2 t' x_13781 x_13780 x_13779
189    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13780)
190    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13779)
191| Mem (t, x_13782) ->
192  h_Mem t x_13782
193    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
194      x_13782)
195| Cond (sz, sg, t, x_13785, x_13784, x_13783) ->
196  h_Cond sz sg t x_13785 x_13784 x_13783
197    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
198      (sz, sg)) x_13785)
199    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13784)
200    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13783)
201| Ecost (t, x_13787, x_13786) ->
202  h_Ecost t x_13787 x_13786
203    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13786)
204
205(** val expr_rect_Type1 :
206    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
207    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
208    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
209    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
210    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
211    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
212    -> 'a1) -> AST.typ -> expr -> 'a1 **)
213let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13795 = function
214| Id (t, x_13797) -> h_Id t x_13797
215| Cst (t, x_13798) -> h_Cst t x_13798
216| Op1 (t, t', x_13800, x_13799) ->
217  h_Op1 t t' x_13800 x_13799
218    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13799)
219| Op2 (t1, t2, t', x_13803, x_13802, x_13801) ->
220  h_Op2 t1 t2 t' x_13803 x_13802 x_13801
221    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13802)
222    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13801)
223| Mem (t, x_13804) ->
224  h_Mem t x_13804
225    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
226      x_13804)
227| Cond (sz, sg, t, x_13807, x_13806, x_13805) ->
228  h_Cond sz sg t x_13807 x_13806 x_13805
229    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
230      (sz, sg)) x_13807)
231    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13806)
232    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13805)
233| Ecost (t, x_13809, x_13808) ->
234  h_Ecost t x_13809 x_13808
235    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13808)
236
237(** val expr_rect_Type0 :
238    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
239    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
240    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
241    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
242    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
243    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
244    -> 'a1) -> AST.typ -> expr -> 'a1 **)
245let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13817 = function
246| Id (t, x_13819) -> h_Id t x_13819
247| Cst (t, x_13820) -> h_Cst t x_13820
248| Op1 (t, t', x_13822, x_13821) ->
249  h_Op1 t t' x_13822 x_13821
250    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13821)
251| Op2 (t1, t2, t', x_13825, x_13824, x_13823) ->
252  h_Op2 t1 t2 t' x_13825 x_13824 x_13823
253    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13824)
254    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13823)
255| Mem (t, x_13826) ->
256  h_Mem t x_13826
257    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
258      x_13826)
259| Cond (sz, sg, t, x_13829, x_13828, x_13827) ->
260  h_Cond sz sg t x_13829 x_13828 x_13827
261    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
262      (sz, sg)) x_13829)
263    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13828)
264    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13827)
265| Ecost (t, x_13831, x_13830) ->
266  h_Ecost t x_13831 x_13830
267    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13830)
268
269(** val expr_inv_rect_Type4 :
270    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
271    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
272    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
273    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
274    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
275    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
276    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
277    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
278    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
279    __ -> __ -> 'a1) -> 'a1 **)
280let expr_inv_rect_Type4 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
281  let hcut = expr_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
282
283(** val expr_inv_rect_Type3 :
284    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
285    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
286    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
287    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
288    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
289    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
290    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
291    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
292    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
293    __ -> __ -> 'a1) -> 'a1 **)
294let expr_inv_rect_Type3 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
295  let hcut = expr_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
296
297(** val expr_inv_rect_Type2 :
298    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
299    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
300    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
301    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
302    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
303    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
304    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
305    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
306    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
307    __ -> __ -> 'a1) -> 'a1 **)
308let expr_inv_rect_Type2 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
309  let hcut = expr_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
310
311(** val expr_inv_rect_Type1 :
312    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
313    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
314    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
315    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
316    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
317    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
318    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
319    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
320    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
321    __ -> __ -> 'a1) -> 'a1 **)
322let expr_inv_rect_Type1 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
323  let hcut = expr_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
324
325(** val expr_inv_rect_Type0 :
326    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
327    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
328    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
329    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
330    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
331    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
332    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
333    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
334    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
335    __ -> __ -> 'a1) -> 'a1 **)
336let expr_inv_rect_Type0 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
337  let hcut = expr_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
338
339(** val expr_jmdiscr : AST.typ -> expr -> expr -> __ **)
340let expr_jmdiscr a1 x y =
341  Logic.eq_rect_Type2 x
342    (match x with
343     | Id (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
344     | Cst (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
345     | Op1 (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
346     | Op2 (a0, a10, a2, a3, a4, a5) ->
347       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
348     | Mem (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
349     | Cond (a0, a10, a2, a3, a4, a5) ->
350       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
351     | Ecost (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
352
353type expr_vars = __
354
355type stmt =
356| St_skip
357| St_assign of AST.typ * AST.ident * expr
358| St_store of AST.typ * expr * expr
359| St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
360   * (AST.typ, expr) Types.dPair List.list
361| St_seq of stmt * stmt
362| St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
363| St_return of (AST.typ, expr) Types.dPair Types.option
364| St_label of PreIdentifiers.identifier * stmt
365| St_goto of PreIdentifiers.identifier
366| St_cost of CostLabel.costlabel * stmt
367
368(** val stmt_rect_Type4 :
369    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
370    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
371    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
372    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
373    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
374    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
375    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
376    -> 'a1) -> stmt -> 'a1 **)
377let 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
378| St_skip -> h_St_skip
379| St_assign (t, x_14002, x_14001) -> h_St_assign t x_14002 x_14001
380| St_store (t, x_14004, x_14003) -> h_St_store t x_14004 x_14003
381| St_call (x_14007, x_14006, x_14005) -> h_St_call x_14007 x_14006 x_14005
382| St_seq (x_14009, x_14008) ->
383  h_St_seq x_14009 x_14008
384    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
385      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14009)
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_14008)
388| St_ifthenelse (sz, sg, x_14012, x_14011, x_14010) ->
389  h_St_ifthenelse sz sg x_14012 x_14011 x_14010
390    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
391      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14011)
392    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
393      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14010)
394| St_return x_14013 -> h_St_return x_14013
395| St_label (x_14015, x_14014) ->
396  h_St_label x_14015 x_14014
397    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
398      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14014)
399| St_goto x_14016 -> h_St_goto x_14016
400| St_cost (x_14018, x_14017) ->
401  h_St_cost x_14018 x_14017
402    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
403      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14017)
404
405(** val stmt_rect_Type3 :
406    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
407    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
408    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
409    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
410    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
411    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
412    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
413    -> 'a1) -> stmt -> 'a1 **)
414let 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
415| St_skip -> h_St_skip
416| St_assign (t, x_14060, x_14059) -> h_St_assign t x_14060 x_14059
417| St_store (t, x_14062, x_14061) -> h_St_store t x_14062 x_14061
418| St_call (x_14065, x_14064, x_14063) -> h_St_call x_14065 x_14064 x_14063
419| St_seq (x_14067, x_14066) ->
420  h_St_seq x_14067 x_14066
421    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
422      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14067)
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_14066)
425| St_ifthenelse (sz, sg, x_14070, x_14069, x_14068) ->
426  h_St_ifthenelse sz sg x_14070 x_14069 x_14068
427    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
428      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14069)
429    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
430      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14068)
431| St_return x_14071 -> h_St_return x_14071
432| St_label (x_14073, x_14072) ->
433  h_St_label x_14073 x_14072
434    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
435      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14072)
436| St_goto x_14074 -> h_St_goto x_14074
437| St_cost (x_14076, x_14075) ->
438  h_St_cost x_14076 x_14075
439    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
440      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14075)
441
442(** val stmt_rect_Type2 :
443    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
444    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
445    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
446    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
447    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
448    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
449    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
450    -> 'a1) -> stmt -> 'a1 **)
451let 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
452| St_skip -> h_St_skip
453| St_assign (t, x_14089, x_14088) -> h_St_assign t x_14089 x_14088
454| St_store (t, x_14091, x_14090) -> h_St_store t x_14091 x_14090
455| St_call (x_14094, x_14093, x_14092) -> h_St_call x_14094 x_14093 x_14092
456| St_seq (x_14096, x_14095) ->
457  h_St_seq x_14096 x_14095
458    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
459      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14096)
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_14095)
462| St_ifthenelse (sz, sg, x_14099, x_14098, x_14097) ->
463  h_St_ifthenelse sz sg x_14099 x_14098 x_14097
464    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
465      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14098)
466    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
467      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14097)
468| St_return x_14100 -> h_St_return x_14100
469| St_label (x_14102, x_14101) ->
470  h_St_label x_14102 x_14101
471    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
472      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14101)
473| St_goto x_14103 -> h_St_goto x_14103
474| St_cost (x_14105, x_14104) ->
475  h_St_cost x_14105 x_14104
476    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
477      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14104)
478
479(** val stmt_rect_Type1 :
480    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
481    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
482    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
483    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
484    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
485    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
486    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
487    -> 'a1) -> stmt -> 'a1 **)
488let 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
489| St_skip -> h_St_skip
490| St_assign (t, x_14118, x_14117) -> h_St_assign t x_14118 x_14117
491| St_store (t, x_14120, x_14119) -> h_St_store t x_14120 x_14119
492| St_call (x_14123, x_14122, x_14121) -> h_St_call x_14123 x_14122 x_14121
493| St_seq (x_14125, x_14124) ->
494  h_St_seq x_14125 x_14124
495    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
496      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14125)
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_14124)
499| St_ifthenelse (sz, sg, x_14128, x_14127, x_14126) ->
500  h_St_ifthenelse sz sg x_14128 x_14127 x_14126
501    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
502      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14127)
503    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
504      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14126)
505| St_return x_14129 -> h_St_return x_14129
506| St_label (x_14131, x_14130) ->
507  h_St_label x_14131 x_14130
508    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
509      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14130)
510| St_goto x_14132 -> h_St_goto x_14132
511| St_cost (x_14134, x_14133) ->
512  h_St_cost x_14134 x_14133
513    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
514      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14133)
515
516(** val stmt_rect_Type0 :
517    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
518    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
519    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
520    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
521    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
522    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
523    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
524    -> 'a1) -> stmt -> 'a1 **)
525let 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
526| St_skip -> h_St_skip
527| St_assign (t, x_14147, x_14146) -> h_St_assign t x_14147 x_14146
528| St_store (t, x_14149, x_14148) -> h_St_store t x_14149 x_14148
529| St_call (x_14152, x_14151, x_14150) -> h_St_call x_14152 x_14151 x_14150
530| St_seq (x_14154, x_14153) ->
531  h_St_seq x_14154 x_14153
532    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
533      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14154)
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_14153)
536| St_ifthenelse (sz, sg, x_14157, x_14156, x_14155) ->
537  h_St_ifthenelse sz sg x_14157 x_14156 x_14155
538    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
539      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14156)
540    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
541      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14155)
542| St_return x_14158 -> h_St_return x_14158
543| St_label (x_14160, x_14159) ->
544  h_St_label x_14160 x_14159
545    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
546      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14159)
547| St_goto x_14161 -> h_St_goto x_14161
548| St_cost (x_14163, x_14162) ->
549  h_St_cost x_14163 x_14162
550    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
551      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14162)
552
553(** val stmt_inv_rect_Type4 :
554    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
555    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
556    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
557    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
558    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
559    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
560    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
561    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
562    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
563let stmt_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
564  let hcut = stmt_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
565
566(** val stmt_inv_rect_Type3 :
567    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
568    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
569    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
570    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
571    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
572    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
573    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
574    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
575    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
576let stmt_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
577  let hcut = stmt_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
578
579(** val stmt_inv_rect_Type2 :
580    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
581    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
582    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
583    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
584    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
585    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
586    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
587    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
588    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
589let stmt_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
590  let hcut = stmt_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
591
592(** val stmt_inv_rect_Type1 :
593    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
594    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
595    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
596    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
597    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
598    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
599    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
600    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
601    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
602let stmt_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
603  let hcut = stmt_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
604
605(** val stmt_inv_rect_Type0 :
606    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
607    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
608    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
609    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
610    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
611    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
612    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
613    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
614    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
615let stmt_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
616  let hcut = stmt_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
617
618(** val stmt_discr : stmt -> stmt -> __ **)
619let stmt_discr x y =
620  Logic.eq_rect_Type2 x
621    (match x with
622     | St_skip -> Obj.magic (fun _ dH -> dH)
623     | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
624     | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
625     | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
626     | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
627     | St_ifthenelse (a0, a1, a2, a3, a4) ->
628       Obj.magic (fun _ dH -> dH __ __ __ __ __)
629     | St_return a0 -> Obj.magic (fun _ dH -> dH __)
630     | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
631     | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
632     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
633
634(** val stmt_jmdiscr : stmt -> stmt -> __ **)
635let stmt_jmdiscr x y =
636  Logic.eq_rect_Type2 x
637    (match x with
638     | St_skip -> Obj.magic (fun _ dH -> dH)
639     | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
640     | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
641     | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
642     | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
643     | St_ifthenelse (a0, a1, a2, a3, a4) ->
644       Obj.magic (fun _ dH -> dH __ __ __ __ __)
645     | St_return a0 -> Obj.magic (fun _ dH -> dH __)
646     | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
647     | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
648     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
649
650type stmt_P = __
651
652(** val labels_of : stmt -> PreIdentifiers.identifier List.list **)
653let rec labels_of = function
654| St_skip -> List.Nil
655| St_assign (x, x0, x1) -> List.Nil
656| St_store (x, x0, x1) -> List.Nil
657| St_call (x, x0, x1) -> List.Nil
658| St_seq (s1, s2) -> List.append (labels_of s1) (labels_of s2)
659| St_ifthenelse (x, x0, x1, s1, s2) ->
660  List.append (labels_of s1) (labels_of s2)
661| St_return x -> List.Nil
662| St_label (l, s0) -> List.Cons (l, (labels_of s0))
663| St_goto x -> List.Nil
664| St_cost (x, s0) -> labels_of s0
665
666(** val cminor_stmt_inv_rect_Type4 :
667    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
668    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
669    'a1 **)
670let rec cminor_stmt_inv_rect_Type4 env labels rettyp s h_mk_cminor_stmt_inv =
671  h_mk_cminor_stmt_inv __ __ __
672
673(** val cminor_stmt_inv_rect_Type5 :
674    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
675    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
676    'a1 **)
677let rec cminor_stmt_inv_rect_Type5 env labels rettyp s h_mk_cminor_stmt_inv =
678  h_mk_cminor_stmt_inv __ __ __
679
680(** val cminor_stmt_inv_rect_Type3 :
681    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
682    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
683    'a1 **)
684let rec cminor_stmt_inv_rect_Type3 env labels rettyp s h_mk_cminor_stmt_inv =
685  h_mk_cminor_stmt_inv __ __ __
686
687(** val cminor_stmt_inv_rect_Type2 :
688    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
689    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
690    'a1 **)
691let rec cminor_stmt_inv_rect_Type2 env labels rettyp s h_mk_cminor_stmt_inv =
692  h_mk_cminor_stmt_inv __ __ __
693
694(** val cminor_stmt_inv_rect_Type1 :
695    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
696    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
697    'a1 **)
698let rec cminor_stmt_inv_rect_Type1 env labels rettyp s h_mk_cminor_stmt_inv =
699  h_mk_cminor_stmt_inv __ __ __
700
701(** val cminor_stmt_inv_rect_Type0 :
702    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
703    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
704    'a1 **)
705let rec cminor_stmt_inv_rect_Type0 env labels rettyp s h_mk_cminor_stmt_inv =
706  h_mk_cminor_stmt_inv __ __ __
707
708(** val cminor_stmt_inv_inv_rect_Type4 :
709    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
710    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
711    'a1) -> 'a1 **)
712let cminor_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
713  let hcut = cminor_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __
714
715(** val cminor_stmt_inv_inv_rect_Type3 :
716    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
717    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
718    'a1) -> 'a1 **)
719let cminor_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
720  let hcut = cminor_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __
721
722(** val cminor_stmt_inv_inv_rect_Type2 :
723    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
724    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
725    'a1) -> 'a1 **)
726let cminor_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
727  let hcut = cminor_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __
728
729(** val cminor_stmt_inv_inv_rect_Type1 :
730    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
731    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
732    'a1) -> 'a1 **)
733let cminor_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
734  let hcut = cminor_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __
735
736(** val cminor_stmt_inv_inv_rect_Type0 :
737    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
738    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
739    'a1) -> 'a1 **)
740let cminor_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
741  let hcut = cminor_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __
742
743(** val cminor_stmt_inv_discr :
744    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
745    List.list -> AST.typ Types.option -> stmt -> __ **)
746let cminor_stmt_inv_discr a1 a2 a3 a4 =
747  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
748
749(** val cminor_stmt_inv_jmdiscr :
750    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
751    List.list -> AST.typ Types.option -> stmt -> __ **)
752let cminor_stmt_inv_jmdiscr a1 a2 a3 a4 =
753  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
754
755type internal_function = { f_return : AST.typ Types.option;
756                           f_params : (AST.ident, AST.typ) Types.prod
757                                      List.list;
758                           f_vars : (AST.ident, AST.typ) Types.prod List.list;
759                           f_stacksize : Nat.nat; f_body : stmt }
760
761(** val internal_function_rect_Type4 :
762    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
763    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
764    -> 'a1) -> internal_function -> 'a1 **)
765let rec internal_function_rect_Type4 h_mk_internal_function x_14458 =
766  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
767    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14458
768  in
769  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
770    __
771
772(** val internal_function_rect_Type5 :
773    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
774    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
775    -> 'a1) -> internal_function -> 'a1 **)
776let rec internal_function_rect_Type5 h_mk_internal_function x_14460 =
777  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
778    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14460
779  in
780  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
781    __
782
783(** val internal_function_rect_Type3 :
784    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
785    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
786    -> 'a1) -> internal_function -> 'a1 **)
787let rec internal_function_rect_Type3 h_mk_internal_function x_14462 =
788  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
789    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14462
790  in
791  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
792    __
793
794(** val internal_function_rect_Type2 :
795    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
796    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
797    -> 'a1) -> internal_function -> 'a1 **)
798let rec internal_function_rect_Type2 h_mk_internal_function x_14464 =
799  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
800    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14464
801  in
802  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
803    __
804
805(** val internal_function_rect_Type1 :
806    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
807    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
808    -> 'a1) -> internal_function -> 'a1 **)
809let rec internal_function_rect_Type1 h_mk_internal_function x_14466 =
810  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
811    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14466
812  in
813  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
814    __
815
816(** val internal_function_rect_Type0 :
817    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
818    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
819    -> 'a1) -> internal_function -> 'a1 **)
820let rec internal_function_rect_Type0 h_mk_internal_function x_14468 =
821  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
822    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14468
823  in
824  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
825    __
826
827(** val f_return : internal_function -> AST.typ Types.option **)
828let rec f_return xxx =
829  xxx.f_return
830
831(** val f_params :
832    internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
833let rec f_params xxx =
834  xxx.f_params
835
836(** val f_vars :
837    internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
838let rec f_vars xxx =
839  xxx.f_vars
840
841(** val f_stacksize : internal_function -> Nat.nat **)
842let rec f_stacksize xxx =
843  xxx.f_stacksize
844
845(** val f_body : internal_function -> stmt **)
846let rec f_body xxx =
847  xxx.f_body
848
849(** val internal_function_inv_rect_Type4 :
850    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
851    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
852    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
853let internal_function_inv_rect_Type4 hterm h1 =
854  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
855
856(** val internal_function_inv_rect_Type3 :
857    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
858    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
859    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
860let internal_function_inv_rect_Type3 hterm h1 =
861  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
862
863(** val internal_function_inv_rect_Type2 :
864    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
865    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
866    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
867let internal_function_inv_rect_Type2 hterm h1 =
868  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
869
870(** val internal_function_inv_rect_Type1 :
871    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
872    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
873    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
874let internal_function_inv_rect_Type1 hterm h1 =
875  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
876
877(** val internal_function_inv_rect_Type0 :
878    internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
879    Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
880    -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
881let internal_function_inv_rect_Type0 hterm h1 =
882  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
883
884(** val internal_function_jmdiscr :
885    internal_function -> internal_function -> __ **)
886let internal_function_jmdiscr x y =
887  Logic.eq_rect_Type2 x
888    (let { f_return = a0; f_params = a1; f_vars = a2; f_stacksize = a4;
889       f_body = a5 } = x
890     in
891    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
892
893type cminor_program =
894  (internal_function AST.fundef, AST.init_data List.list) AST.program
895
896type cminor_noinit_program =
897  (internal_function AST.fundef, Nat.nat) AST.program
898
Note: See TracBrowser for help on using the repository browser.