source: extracted/cminor_syntax.ml @ 2960

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

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_13785 = function
116| Id (t, x_13787) -> h_Id t x_13787
117| Cst (t, x_13788) -> h_Cst t x_13788
118| Op1 (t, t', x_13790, x_13789) ->
119  h_Op1 t t' x_13790 x_13789
120    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13789)
121| Op2 (t1, t2, t', x_13793, x_13792, x_13791) ->
122  h_Op2 t1 t2 t' x_13793 x_13792 x_13791
123    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13792)
124    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13791)
125| Mem (t, x_13794) ->
126  h_Mem t x_13794
127    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
128      x_13794)
129| Cond (sz, sg, t, x_13797, x_13796, x_13795) ->
130  h_Cond sz sg t x_13797 x_13796 x_13795
131    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
132      (sz, sg)) x_13797)
133    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13796)
134    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13795)
135| Ecost (t, x_13799, x_13798) ->
136  h_Ecost t x_13799 x_13798
137    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13798)
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_13829 = function
148| Id (t, x_13831) -> h_Id t x_13831
149| Cst (t, x_13832) -> h_Cst t x_13832
150| Op1 (t, t', x_13834, x_13833) ->
151  h_Op1 t t' x_13834 x_13833
152    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13833)
153| Op2 (t1, t2, t', x_13837, x_13836, x_13835) ->
154  h_Op2 t1 t2 t' x_13837 x_13836 x_13835
155    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13836)
156    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13835)
157| Mem (t, x_13838) ->
158  h_Mem t x_13838
159    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
160      x_13838)
161| Cond (sz, sg, t, x_13841, x_13840, x_13839) ->
162  h_Cond sz sg t x_13841 x_13840 x_13839
163    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
164      (sz, sg)) x_13841)
165    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13840)
166    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13839)
167| Ecost (t, x_13843, x_13842) ->
168  h_Ecost t x_13843 x_13842
169    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13842)
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_13851 = function
180| Id (t, x_13853) -> h_Id t x_13853
181| Cst (t, x_13854) -> h_Cst t x_13854
182| Op1 (t, t', x_13856, x_13855) ->
183  h_Op1 t t' x_13856 x_13855
184    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13855)
185| Op2 (t1, t2, t', x_13859, x_13858, x_13857) ->
186  h_Op2 t1 t2 t' x_13859 x_13858 x_13857
187    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13858)
188    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13857)
189| Mem (t, x_13860) ->
190  h_Mem t x_13860
191    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
192      x_13860)
193| Cond (sz, sg, t, x_13863, x_13862, x_13861) ->
194  h_Cond sz sg t x_13863 x_13862 x_13861
195    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
196      (sz, sg)) x_13863)
197    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13862)
198    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13861)
199| Ecost (t, x_13865, x_13864) ->
200  h_Ecost t x_13865 x_13864
201    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13864)
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_13873 = function
212| Id (t, x_13875) -> h_Id t x_13875
213| Cst (t, x_13876) -> h_Cst t x_13876
214| Op1 (t, t', x_13878, x_13877) ->
215  h_Op1 t t' x_13878 x_13877
216    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13877)
217| Op2 (t1, t2, t', x_13881, x_13880, x_13879) ->
218  h_Op2 t1 t2 t' x_13881 x_13880 x_13879
219    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13880)
220    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13879)
221| Mem (t, x_13882) ->
222  h_Mem t x_13882
223    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
224      x_13882)
225| Cond (sz, sg, t, x_13885, x_13884, x_13883) ->
226  h_Cond sz sg t x_13885 x_13884 x_13883
227    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
228      (sz, sg)) x_13885)
229    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13884)
230    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13883)
231| Ecost (t, x_13887, x_13886) ->
232  h_Ecost t x_13887 x_13886
233    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13886)
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_13895 = function
244| Id (t, x_13897) -> h_Id t x_13897
245| Cst (t, x_13898) -> h_Cst t x_13898
246| Op1 (t, t', x_13900, x_13899) ->
247  h_Op1 t t' x_13900 x_13899
248    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13899)
249| Op2 (t1, t2, t', x_13903, x_13902, x_13901) ->
250  h_Op2 t1 t2 t' x_13903 x_13902 x_13901
251    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13902)
252    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13901)
253| Mem (t, x_13904) ->
254  h_Mem t x_13904
255    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
256      x_13904)
257| Cond (sz, sg, t, x_13907, x_13906, x_13905) ->
258  h_Cond sz sg t x_13907 x_13906 x_13905
259    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
260      (sz, sg)) x_13907)
261    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13906)
262    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13905)
263| Ecost (t, x_13909, x_13908) ->
264  h_Ecost t x_13909 x_13908
265    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13908)
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_14080, x_14079) -> h_St_assign t x_14080 x_14079
376| St_store (t, x_14082, x_14081) -> h_St_store t x_14082 x_14081
377| St_call (x_14085, x_14084, x_14083) -> h_St_call x_14085 x_14084 x_14083
378| St_seq (x_14087, x_14086) ->
379  h_St_seq x_14087 x_14086
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_14087)
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_14086)
384| St_ifthenelse (sz, sg, x_14090, x_14089, x_14088) ->
385  h_St_ifthenelse sz sg x_14090 x_14089 x_14088
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_14089)
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_14088)
390| St_return x_14091 -> h_St_return x_14091
391| St_label (x_14093, x_14092) ->
392  h_St_label x_14093 x_14092
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_14092)
395| St_goto x_14094 -> h_St_goto x_14094
396| St_cost (x_14096, x_14095) ->
397  h_St_cost x_14096 x_14095
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_14095)
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_14138, x_14137) -> h_St_assign t x_14138 x_14137
413| St_store (t, x_14140, x_14139) -> h_St_store t x_14140 x_14139
414| St_call (x_14143, x_14142, x_14141) -> h_St_call x_14143 x_14142 x_14141
415| St_seq (x_14145, x_14144) ->
416  h_St_seq x_14145 x_14144
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_14145)
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_14144)
421| St_ifthenelse (sz, sg, x_14148, x_14147, x_14146) ->
422  h_St_ifthenelse sz sg x_14148 x_14147 x_14146
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_14147)
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_14146)
427| St_return x_14149 -> h_St_return x_14149
428| St_label (x_14151, x_14150) ->
429  h_St_label x_14151 x_14150
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_14150)
432| St_goto x_14152 -> h_St_goto x_14152
433| St_cost (x_14154, x_14153) ->
434  h_St_cost x_14154 x_14153
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_14153)
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_14167, x_14166) -> h_St_assign t x_14167 x_14166
450| St_store (t, x_14169, x_14168) -> h_St_store t x_14169 x_14168
451| St_call (x_14172, x_14171, x_14170) -> h_St_call x_14172 x_14171 x_14170
452| St_seq (x_14174, x_14173) ->
453  h_St_seq x_14174 x_14173
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_14174)
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_14173)
458| St_ifthenelse (sz, sg, x_14177, x_14176, x_14175) ->
459  h_St_ifthenelse sz sg x_14177 x_14176 x_14175
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_14176)
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_14175)
464| St_return x_14178 -> h_St_return x_14178
465| St_label (x_14180, x_14179) ->
466  h_St_label x_14180 x_14179
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_14179)
469| St_goto x_14181 -> h_St_goto x_14181
470| St_cost (x_14183, x_14182) ->
471  h_St_cost x_14183 x_14182
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_14182)
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_14196, x_14195) -> h_St_assign t x_14196 x_14195
487| St_store (t, x_14198, x_14197) -> h_St_store t x_14198 x_14197
488| St_call (x_14201, x_14200, x_14199) -> h_St_call x_14201 x_14200 x_14199
489| St_seq (x_14203, x_14202) ->
490  h_St_seq x_14203 x_14202
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_14203)
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_14202)
495| St_ifthenelse (sz, sg, x_14206, x_14205, x_14204) ->
496  h_St_ifthenelse sz sg x_14206 x_14205 x_14204
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_14205)
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_14204)
501| St_return x_14207 -> h_St_return x_14207
502| St_label (x_14209, x_14208) ->
503  h_St_label x_14209 x_14208
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_14208)
506| St_goto x_14210 -> h_St_goto x_14210
507| St_cost (x_14212, x_14211) ->
508  h_St_cost x_14212 x_14211
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_14211)
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_14225, x_14224) -> h_St_assign t x_14225 x_14224
524| St_store (t, x_14227, x_14226) -> h_St_store t x_14227 x_14226
525| St_call (x_14230, x_14229, x_14228) -> h_St_call x_14230 x_14229 x_14228
526| St_seq (x_14232, x_14231) ->
527  h_St_seq x_14232 x_14231
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_14232)
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_14231)
532| St_ifthenelse (sz, sg, x_14235, x_14234, x_14233) ->
533  h_St_ifthenelse sz sg x_14235 x_14234 x_14233
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_14234)
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_14233)
538| St_return x_14236 -> h_St_return x_14236
539| St_label (x_14238, x_14237) ->
540  h_St_label x_14238 x_14237
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_14237)
543| St_goto x_14239 -> h_St_goto x_14239
544| St_cost (x_14241, x_14240) ->
545  h_St_cost x_14241 x_14240
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_14240)
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_14536 =
760  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
761    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14536
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_14538 =
771  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
772    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14538
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_14540 =
782  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
783    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14540
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_14542 =
793  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
794    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14542
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_14544 =
804  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
805    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14544
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_14546 =
815  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
816    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14546
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.