source: extracted/cminor_syntax.ml @ 2731

Last change on this file since 2731 was 2730, checked in by sacerdot, 7 years ago

Exported again.

File size: 41.1 KB
RevLine 
[2601]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
[2717]31open Exp
32
[2601]33open Arithmetic
34
35open Extranat
36
37open Vector
38
39open FoldStuff
40
41open BitVector
42
43open Z
44
45open BitVectorZ
46
47open Pointers
48
[2649]49open ErrorMessages
50
[2601]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
[2717]95open BitVectorTrie
96
[2601]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 **)
[2730]117let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2569 = function
118| Id (t, x_2571) -> h_Id t x_2571
119| Cst (t, x_2572) -> h_Cst t x_2572
120| Op1 (t, t', x_2574, x_2573) ->
121  h_Op1 t t' x_2574 x_2573
122    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2573)
123| Op2 (t1, t2, t', x_2577, x_2576, x_2575) ->
124  h_Op2 t1 t2 t' x_2577 x_2576 x_2575
125    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2576)
126    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2575)
127| Mem (t, x_2578) ->
128  h_Mem t x_2578
[2601]129    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
[2730]130      x_2578)
131| Cond (sz, sg, t, x_2581, x_2580, x_2579) ->
132  h_Cond sz sg t x_2581 x_2580 x_2579
[2601]133    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
[2730]134      (sz, sg)) x_2581)
135    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2580)
136    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2579)
137| Ecost (t, x_2583, x_2582) ->
138  h_Ecost t x_2583 x_2582
139    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2582)
[2601]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 **)
[2730]149let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2613 = function
150| Id (t, x_2615) -> h_Id t x_2615
151| Cst (t, x_2616) -> h_Cst t x_2616
152| Op1 (t, t', x_2618, x_2617) ->
153  h_Op1 t t' x_2618 x_2617
154    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2617)
155| Op2 (t1, t2, t', x_2621, x_2620, x_2619) ->
156  h_Op2 t1 t2 t' x_2621 x_2620 x_2619
157    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2620)
158    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2619)
159| Mem (t, x_2622) ->
160  h_Mem t x_2622
[2601]161    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
[2730]162      x_2622)
163| Cond (sz, sg, t, x_2625, x_2624, x_2623) ->
164  h_Cond sz sg t x_2625 x_2624 x_2623
[2601]165    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
[2730]166      (sz, sg)) x_2625)
167    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2624)
168    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2623)
169| Ecost (t, x_2627, x_2626) ->
170  h_Ecost t x_2627 x_2626
171    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2626)
[2601]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 **)
[2730]181let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2635 = function
182| Id (t, x_2637) -> h_Id t x_2637
183| Cst (t, x_2638) -> h_Cst t x_2638
184| Op1 (t, t', x_2640, x_2639) ->
185  h_Op1 t t' x_2640 x_2639
186    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2639)
187| Op2 (t1, t2, t', x_2643, x_2642, x_2641) ->
188  h_Op2 t1 t2 t' x_2643 x_2642 x_2641
189    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2642)
190    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2641)
191| Mem (t, x_2644) ->
192  h_Mem t x_2644
[2601]193    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
[2730]194      x_2644)
195| Cond (sz, sg, t, x_2647, x_2646, x_2645) ->
196  h_Cond sz sg t x_2647 x_2646 x_2645
[2601]197    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
[2730]198      (sz, sg)) x_2647)
199    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2646)
200    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2645)
201| Ecost (t, x_2649, x_2648) ->
202  h_Ecost t x_2649 x_2648
203    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2648)
[2601]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 **)
[2730]213let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2657 = function
214| Id (t, x_2659) -> h_Id t x_2659
215| Cst (t, x_2660) -> h_Cst t x_2660
216| Op1 (t, t', x_2662, x_2661) ->
217  h_Op1 t t' x_2662 x_2661
218    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2661)
219| Op2 (t1, t2, t', x_2665, x_2664, x_2663) ->
220  h_Op2 t1 t2 t' x_2665 x_2664 x_2663
221    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2664)
222    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2663)
223| Mem (t, x_2666) ->
224  h_Mem t x_2666
[2601]225    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
[2730]226      x_2666)
227| Cond (sz, sg, t, x_2669, x_2668, x_2667) ->
228  h_Cond sz sg t x_2669 x_2668 x_2667
[2601]229    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
[2730]230      (sz, sg)) x_2669)
231    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2668)
232    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2667)
233| Ecost (t, x_2671, x_2670) ->
234  h_Ecost t x_2671 x_2670
235    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2670)
[2601]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 **)
[2730]245let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2679 = function
246| Id (t, x_2681) -> h_Id t x_2681
247| Cst (t, x_2682) -> h_Cst t x_2682
248| Op1 (t, t', x_2684, x_2683) ->
249  h_Op1 t t' x_2684 x_2683
250    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2683)
251| Op2 (t1, t2, t', x_2687, x_2686, x_2685) ->
252  h_Op2 t1 t2 t' x_2687 x_2686 x_2685
253    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2686)
254    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2685)
255| Mem (t, x_2688) ->
256  h_Mem t x_2688
[2601]257    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
[2730]258      x_2688)
259| Cond (sz, sg, t, x_2691, x_2690, x_2689) ->
260  h_Cond sz sg t x_2691 x_2690 x_2689
[2601]261    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
[2730]262      (sz, sg)) x_2691)
263    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2690)
264    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2689)
265| Ecost (t, x_2693, x_2692) ->
266  h_Ecost t x_2693 x_2692
267    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2692)
[2601]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
[2730]379| St_assign (t, x_2864, x_2863) -> h_St_assign t x_2864 x_2863
380| St_store (t, x_2866, x_2865) -> h_St_store t x_2866 x_2865
381| St_call (x_2869, x_2868, x_2867) -> h_St_call x_2869 x_2868 x_2867
382| St_seq (x_2871, x_2870) ->
383  h_St_seq x_2871 x_2870
[2601]384    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]385      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2871)
[2601]386    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]387      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2870)
388| St_ifthenelse (sz, sg, x_2874, x_2873, x_2872) ->
389  h_St_ifthenelse sz sg x_2874 x_2873 x_2872
[2601]390    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]391      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2873)
[2601]392    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]393      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2872)
394| St_return x_2875 -> h_St_return x_2875
395| St_label (x_2877, x_2876) ->
396  h_St_label x_2877 x_2876
[2601]397    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]398      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2876)
399| St_goto x_2878 -> h_St_goto x_2878
400| St_cost (x_2880, x_2879) ->
401  h_St_cost x_2880 x_2879
[2601]402    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]403      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2879)
[2601]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
[2730]416| St_assign (t, x_2922, x_2921) -> h_St_assign t x_2922 x_2921
417| St_store (t, x_2924, x_2923) -> h_St_store t x_2924 x_2923
418| St_call (x_2927, x_2926, x_2925) -> h_St_call x_2927 x_2926 x_2925
419| St_seq (x_2929, x_2928) ->
420  h_St_seq x_2929 x_2928
[2601]421    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]422      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2929)
[2601]423    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]424      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2928)
425| St_ifthenelse (sz, sg, x_2932, x_2931, x_2930) ->
426  h_St_ifthenelse sz sg x_2932 x_2931 x_2930
[2601]427    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]428      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2931)
[2601]429    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]430      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2930)
431| St_return x_2933 -> h_St_return x_2933
432| St_label (x_2935, x_2934) ->
433  h_St_label x_2935 x_2934
[2601]434    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]435      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2934)
436| St_goto x_2936 -> h_St_goto x_2936
437| St_cost (x_2938, x_2937) ->
438  h_St_cost x_2938 x_2937
[2601]439    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]440      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2937)
[2601]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
[2730]453| St_assign (t, x_2951, x_2950) -> h_St_assign t x_2951 x_2950
454| St_store (t, x_2953, x_2952) -> h_St_store t x_2953 x_2952
455| St_call (x_2956, x_2955, x_2954) -> h_St_call x_2956 x_2955 x_2954
456| St_seq (x_2958, x_2957) ->
457  h_St_seq x_2958 x_2957
[2601]458    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]459      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2958)
[2601]460    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]461      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2957)
462| St_ifthenelse (sz, sg, x_2961, x_2960, x_2959) ->
463  h_St_ifthenelse sz sg x_2961 x_2960 x_2959
[2601]464    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]465      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2960)
[2601]466    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]467      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2959)
468| St_return x_2962 -> h_St_return x_2962
469| St_label (x_2964, x_2963) ->
470  h_St_label x_2964 x_2963
[2601]471    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]472      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2963)
473| St_goto x_2965 -> h_St_goto x_2965
474| St_cost (x_2967, x_2966) ->
475  h_St_cost x_2967 x_2966
[2601]476    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]477      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2966)
[2601]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
[2730]490| St_assign (t, x_2980, x_2979) -> h_St_assign t x_2980 x_2979
491| St_store (t, x_2982, x_2981) -> h_St_store t x_2982 x_2981
492| St_call (x_2985, x_2984, x_2983) -> h_St_call x_2985 x_2984 x_2983
493| St_seq (x_2987, x_2986) ->
494  h_St_seq x_2987 x_2986
[2601]495    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]496      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2987)
[2601]497    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]498      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2986)
499| St_ifthenelse (sz, sg, x_2990, x_2989, x_2988) ->
500  h_St_ifthenelse sz sg x_2990 x_2989 x_2988
[2601]501    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]502      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2989)
[2601]503    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]504      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2988)
505| St_return x_2991 -> h_St_return x_2991
506| St_label (x_2993, x_2992) ->
507  h_St_label x_2993 x_2992
[2601]508    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]509      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2992)
510| St_goto x_2994 -> h_St_goto x_2994
511| St_cost (x_2996, x_2995) ->
512  h_St_cost x_2996 x_2995
[2601]513    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]514      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2995)
[2601]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
[2730]527| St_assign (t, x_3009, x_3008) -> h_St_assign t x_3009 x_3008
528| St_store (t, x_3011, x_3010) -> h_St_store t x_3011 x_3010
529| St_call (x_3014, x_3013, x_3012) -> h_St_call x_3014 x_3013 x_3012
530| St_seq (x_3016, x_3015) ->
531  h_St_seq x_3016 x_3015
[2601]532    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]533      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3016)
[2601]534    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]535      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3015)
536| St_ifthenelse (sz, sg, x_3019, x_3018, x_3017) ->
537  h_St_ifthenelse sz sg x_3019 x_3018 x_3017
[2601]538    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]539      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3018)
[2601]540    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]541      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3017)
542| St_return x_3020 -> h_St_return x_3020
543| St_label (x_3022, x_3021) ->
544  h_St_label x_3022 x_3021
[2601]545    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]546      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3021)
547| St_goto x_3023 -> h_St_goto x_3023
548| St_cost (x_3025, x_3024) ->
549  h_St_cost x_3025 x_3024
[2601]550    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
[2730]551      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3024)
[2601]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 **)
[2730]765let rec internal_function_rect_Type4 h_mk_internal_function x_3320 =
[2601]766  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
[2730]767    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3320
[2601]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 **)
[2730]776let rec internal_function_rect_Type5 h_mk_internal_function x_3322 =
[2601]777  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
[2730]778    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3322
[2601]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 **)
[2730]787let rec internal_function_rect_Type3 h_mk_internal_function x_3324 =
[2601]788  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
[2730]789    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3324
[2601]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 **)
[2730]798let rec internal_function_rect_Type2 h_mk_internal_function x_3326 =
[2601]799  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
[2730]800    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3326
[2601]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 **)
[2730]809let rec internal_function_rect_Type1 h_mk_internal_function x_3328 =
[2601]810  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
[2730]811    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3328
[2601]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 **)
[2730]820let rec internal_function_rect_Type0 h_mk_internal_function x_3330 =
[2601]821  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
[2730]822    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3330
[2601]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.