source: extracted/cminor_syntax.ml @ 3015

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

New extraction.

File size: 41.1 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_7767 = function
116| Id (t, x_7769) -> h_Id t x_7769
117| Cst (t, x_7770) -> h_Cst t x_7770
118| Op1 (t, t', x_7772, x_7771) ->
119  h_Op1 t t' x_7772 x_7771
120    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7771)
121| Op2 (t1, t2, t', x_7775, x_7774, x_7773) ->
122  h_Op2 t1 t2 t' x_7775 x_7774 x_7773
123    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_7774)
124    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_7773)
125| Mem (t, x_7776) ->
126  h_Mem t x_7776
127    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
128      x_7776)
129| Cond (sz, sg, t, x_7779, x_7778, x_7777) ->
130  h_Cond sz sg t x_7779 x_7778 x_7777
131    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
132      (sz, sg)) x_7779)
133    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7778)
134    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7777)
135| Ecost (t, x_7781, x_7780) ->
136  h_Ecost t x_7781 x_7780
137    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7780)
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_7811 = function
148| Id (t, x_7813) -> h_Id t x_7813
149| Cst (t, x_7814) -> h_Cst t x_7814
150| Op1 (t, t', x_7816, x_7815) ->
151  h_Op1 t t' x_7816 x_7815
152    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7815)
153| Op2 (t1, t2, t', x_7819, x_7818, x_7817) ->
154  h_Op2 t1 t2 t' x_7819 x_7818 x_7817
155    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_7818)
156    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_7817)
157| Mem (t, x_7820) ->
158  h_Mem t x_7820
159    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
160      x_7820)
161| Cond (sz, sg, t, x_7823, x_7822, x_7821) ->
162  h_Cond sz sg t x_7823 x_7822 x_7821
163    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
164      (sz, sg)) x_7823)
165    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7822)
166    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7821)
167| Ecost (t, x_7825, x_7824) ->
168  h_Ecost t x_7825 x_7824
169    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7824)
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_7833 = function
180| Id (t, x_7835) -> h_Id t x_7835
181| Cst (t, x_7836) -> h_Cst t x_7836
182| Op1 (t, t', x_7838, x_7837) ->
183  h_Op1 t t' x_7838 x_7837
184    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7837)
185| Op2 (t1, t2, t', x_7841, x_7840, x_7839) ->
186  h_Op2 t1 t2 t' x_7841 x_7840 x_7839
187    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_7840)
188    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_7839)
189| Mem (t, x_7842) ->
190  h_Mem t x_7842
191    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
192      x_7842)
193| Cond (sz, sg, t, x_7845, x_7844, x_7843) ->
194  h_Cond sz sg t x_7845 x_7844 x_7843
195    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
196      (sz, sg)) x_7845)
197    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7844)
198    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7843)
199| Ecost (t, x_7847, x_7846) ->
200  h_Ecost t x_7847 x_7846
201    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7846)
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_7855 = function
212| Id (t, x_7857) -> h_Id t x_7857
213| Cst (t, x_7858) -> h_Cst t x_7858
214| Op1 (t, t', x_7860, x_7859) ->
215  h_Op1 t t' x_7860 x_7859
216    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7859)
217| Op2 (t1, t2, t', x_7863, x_7862, x_7861) ->
218  h_Op2 t1 t2 t' x_7863 x_7862 x_7861
219    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_7862)
220    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_7861)
221| Mem (t, x_7864) ->
222  h_Mem t x_7864
223    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
224      x_7864)
225| Cond (sz, sg, t, x_7867, x_7866, x_7865) ->
226  h_Cond sz sg t x_7867 x_7866 x_7865
227    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
228      (sz, sg)) x_7867)
229    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7866)
230    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7865)
231| Ecost (t, x_7869, x_7868) ->
232  h_Ecost t x_7869 x_7868
233    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7868)
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_7877 = function
244| Id (t, x_7879) -> h_Id t x_7879
245| Cst (t, x_7880) -> h_Cst t x_7880
246| Op1 (t, t', x_7882, x_7881) ->
247  h_Op1 t t' x_7882 x_7881
248    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7881)
249| Op2 (t1, t2, t', x_7885, x_7884, x_7883) ->
250  h_Op2 t1 t2 t' x_7885 x_7884 x_7883
251    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_7884)
252    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_7883)
253| Mem (t, x_7886) ->
254  h_Mem t x_7886
255    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
256      x_7886)
257| Cond (sz, sg, t, x_7889, x_7888, x_7887) ->
258  h_Cond sz sg t x_7889 x_7888 x_7887
259    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
260      (sz, sg)) x_7889)
261    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7888)
262    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7887)
263| Ecost (t, x_7891, x_7890) ->
264  h_Ecost t x_7891 x_7890
265    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_7890)
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_8062, x_8061) -> h_St_assign t x_8062 x_8061
376| St_store (t, x_8064, x_8063) -> h_St_store t x_8064 x_8063
377| St_call (x_8067, x_8066, x_8065) -> h_St_call x_8067 x_8066 x_8065
378| St_seq (x_8069, x_8068) ->
379  h_St_seq x_8069 x_8068
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_8069)
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_8068)
384| St_ifthenelse (sz, sg, x_8072, x_8071, x_8070) ->
385  h_St_ifthenelse sz sg x_8072 x_8071 x_8070
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_8071)
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_8070)
390| St_return x_8073 -> h_St_return x_8073
391| St_label (x_8075, x_8074) ->
392  h_St_label x_8075 x_8074
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_8074)
395| St_goto x_8076 -> h_St_goto x_8076
396| St_cost (x_8078, x_8077) ->
397  h_St_cost x_8078 x_8077
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_8077)
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_8120, x_8119) -> h_St_assign t x_8120 x_8119
413| St_store (t, x_8122, x_8121) -> h_St_store t x_8122 x_8121
414| St_call (x_8125, x_8124, x_8123) -> h_St_call x_8125 x_8124 x_8123
415| St_seq (x_8127, x_8126) ->
416  h_St_seq x_8127 x_8126
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_8127)
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_8126)
421| St_ifthenelse (sz, sg, x_8130, x_8129, x_8128) ->
422  h_St_ifthenelse sz sg x_8130 x_8129 x_8128
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_8129)
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_8128)
427| St_return x_8131 -> h_St_return x_8131
428| St_label (x_8133, x_8132) ->
429  h_St_label x_8133 x_8132
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_8132)
432| St_goto x_8134 -> h_St_goto x_8134
433| St_cost (x_8136, x_8135) ->
434  h_St_cost x_8136 x_8135
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_8135)
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_8149, x_8148) -> h_St_assign t x_8149 x_8148
450| St_store (t, x_8151, x_8150) -> h_St_store t x_8151 x_8150
451| St_call (x_8154, x_8153, x_8152) -> h_St_call x_8154 x_8153 x_8152
452| St_seq (x_8156, x_8155) ->
453  h_St_seq x_8156 x_8155
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_8156)
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_8155)
458| St_ifthenelse (sz, sg, x_8159, x_8158, x_8157) ->
459  h_St_ifthenelse sz sg x_8159 x_8158 x_8157
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_8158)
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_8157)
464| St_return x_8160 -> h_St_return x_8160
465| St_label (x_8162, x_8161) ->
466  h_St_label x_8162 x_8161
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_8161)
469| St_goto x_8163 -> h_St_goto x_8163
470| St_cost (x_8165, x_8164) ->
471  h_St_cost x_8165 x_8164
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_8164)
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_8178, x_8177) -> h_St_assign t x_8178 x_8177
487| St_store (t, x_8180, x_8179) -> h_St_store t x_8180 x_8179
488| St_call (x_8183, x_8182, x_8181) -> h_St_call x_8183 x_8182 x_8181
489| St_seq (x_8185, x_8184) ->
490  h_St_seq x_8185 x_8184
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_8185)
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_8184)
495| St_ifthenelse (sz, sg, x_8188, x_8187, x_8186) ->
496  h_St_ifthenelse sz sg x_8188 x_8187 x_8186
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_8187)
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_8186)
501| St_return x_8189 -> h_St_return x_8189
502| St_label (x_8191, x_8190) ->
503  h_St_label x_8191 x_8190
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_8190)
506| St_goto x_8192 -> h_St_goto x_8192
507| St_cost (x_8194, x_8193) ->
508  h_St_cost x_8194 x_8193
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_8193)
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_8207, x_8206) -> h_St_assign t x_8207 x_8206
524| St_store (t, x_8209, x_8208) -> h_St_store t x_8209 x_8208
525| St_call (x_8212, x_8211, x_8210) -> h_St_call x_8212 x_8211 x_8210
526| St_seq (x_8214, x_8213) ->
527  h_St_seq x_8214 x_8213
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_8214)
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_8213)
532| St_ifthenelse (sz, sg, x_8217, x_8216, x_8215) ->
533  h_St_ifthenelse sz sg x_8217 x_8216 x_8215
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_8216)
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_8215)
538| St_return x_8218 -> h_St_return x_8218
539| St_label (x_8220, x_8219) ->
540  h_St_label x_8220 x_8219
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_8219)
543| St_goto x_8221 -> h_St_goto x_8221
544| St_cost (x_8223, x_8222) ->
545  h_St_cost x_8223 x_8222
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_8222)
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_8518 =
760  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
761    f_stacksize = f_stacksize0; f_body = f_body0 } = x_8518
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_8520 =
771  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
772    f_stacksize = f_stacksize0; f_body = f_body0 } = x_8520
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_8522 =
782  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
783    f_stacksize = f_stacksize0; f_body = f_body0 } = x_8522
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_8524 =
793  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
794    f_stacksize = f_stacksize0; f_body = f_body0 } = x_8524
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_8526 =
804  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
805    f_stacksize = f_stacksize0; f_body = f_body0 } = x_8526
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_8528 =
815  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
816    f_stacksize = f_stacksize0; f_body = f_body0 } = x_8528
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.