source: extracted/cminor_syntax.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 41.5 KB
Line 
1open Preamble
2
3open FrontEndVal
4
5open Hide
6
7open ByteValues
8
9open GenMem
10
11open FrontEndMem
12
13open Proper
14
15open PositiveMap
16
17open Deqsets
18
19open Extralib
20
21open Lists
22
23open Identifiers
24
25open Integers
26
27open AST
28
29open Division
30
31open Exp
32
33open Arithmetic
34
35open Extranat
36
37open Vector
38
39open FoldStuff
40
41open BitVector
42
43open Z
44
45open BitVectorZ
46
47open Pointers
48
49open ErrorMessages
50
51open Option
52
53open Setoids
54
55open Monad
56
57open Positive
58
59open PreIdentifiers
60
61open Errors
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open Util
70
71open Bool
72
73open Relations
74
75open Nat
76
77open List
78
79open Hints_declaration
80
81open Core_notation
82
83open Pts
84
85open Logic
86
87open Types
88
89open Coqlib
90
91open Values
92
93open FrontEndOps
94
95open BitVectorTrie
96
97open CostLabel
98
99type expr =
100| Id of AST.typ * AST.ident
101| Cst of AST.typ * FrontEndOps.constant
102| Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
103| Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation * 
104   expr * expr
105| Mem of AST.typ * expr
106| Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
107| Ecost of AST.typ * CostLabel.costlabel * expr
108
109(** val expr_rect_Type4 :
110    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
111    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
112    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
113    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
114    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
115    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
116    -> 'a1) -> AST.typ -> expr -> 'a1 **)
117let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13681 = function
118| Id (t, x_13683) -> h_Id t x_13683
119| Cst (t, x_13684) -> h_Cst t x_13684
120| Op1 (t, t', x_13686, x_13685) ->
121  h_Op1 t t' x_13686 x_13685
122    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13685)
123| Op2 (t1, t2, t', x_13689, x_13688, x_13687) ->
124  h_Op2 t1 t2 t' x_13689 x_13688 x_13687
125    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13688)
126    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13687)
127| Mem (t, x_13690) ->
128  h_Mem t x_13690
129    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
130      x_13690)
131| Cond (sz, sg, t, x_13693, x_13692, x_13691) ->
132  h_Cond sz sg t x_13693 x_13692 x_13691
133    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
134      (sz, sg)) x_13693)
135    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13692)
136    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13691)
137| Ecost (t, x_13695, x_13694) ->
138  h_Ecost t x_13695 x_13694
139    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13694)
140
141(** val expr_rect_Type3 :
142    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
143    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
144    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
145    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
146    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
147    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
148    -> 'a1) -> AST.typ -> expr -> 'a1 **)
149let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13725 = function
150| Id (t, x_13727) -> h_Id t x_13727
151| Cst (t, x_13728) -> h_Cst t x_13728
152| Op1 (t, t', x_13730, x_13729) ->
153  h_Op1 t t' x_13730 x_13729
154    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13729)
155| Op2 (t1, t2, t', x_13733, x_13732, x_13731) ->
156  h_Op2 t1 t2 t' x_13733 x_13732 x_13731
157    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13732)
158    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13731)
159| Mem (t, x_13734) ->
160  h_Mem t x_13734
161    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
162      x_13734)
163| Cond (sz, sg, t, x_13737, x_13736, x_13735) ->
164  h_Cond sz sg t x_13737 x_13736 x_13735
165    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
166      (sz, sg)) x_13737)
167    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13736)
168    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13735)
169| Ecost (t, x_13739, x_13738) ->
170  h_Ecost t x_13739 x_13738
171    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13738)
172
173(** val expr_rect_Type2 :
174    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
175    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
176    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
177    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
178    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
179    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
180    -> 'a1) -> AST.typ -> expr -> 'a1 **)
181let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13747 = function
182| Id (t, x_13749) -> h_Id t x_13749
183| Cst (t, x_13750) -> h_Cst t x_13750
184| Op1 (t, t', x_13752, x_13751) ->
185  h_Op1 t t' x_13752 x_13751
186    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13751)
187| Op2 (t1, t2, t', x_13755, x_13754, x_13753) ->
188  h_Op2 t1 t2 t' x_13755 x_13754 x_13753
189    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13754)
190    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13753)
191| Mem (t, x_13756) ->
192  h_Mem t x_13756
193    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
194      x_13756)
195| Cond (sz, sg, t, x_13759, x_13758, x_13757) ->
196  h_Cond sz sg t x_13759 x_13758 x_13757
197    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
198      (sz, sg)) x_13759)
199    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13758)
200    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13757)
201| Ecost (t, x_13761, x_13760) ->
202  h_Ecost t x_13761 x_13760
203    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13760)
204
205(** val expr_rect_Type1 :
206    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
207    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
208    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
209    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
210    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
211    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
212    -> 'a1) -> AST.typ -> expr -> 'a1 **)
213let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13769 = function
214| Id (t, x_13771) -> h_Id t x_13771
215| Cst (t, x_13772) -> h_Cst t x_13772
216| Op1 (t, t', x_13774, x_13773) ->
217  h_Op1 t t' x_13774 x_13773
218    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13773)
219| Op2 (t1, t2, t', x_13777, x_13776, x_13775) ->
220  h_Op2 t1 t2 t' x_13777 x_13776 x_13775
221    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13776)
222    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13775)
223| Mem (t, x_13778) ->
224  h_Mem t x_13778
225    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
226      x_13778)
227| Cond (sz, sg, t, x_13781, x_13780, x_13779) ->
228  h_Cond sz sg t x_13781 x_13780 x_13779
229    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
230      (sz, sg)) x_13781)
231    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13780)
232    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13779)
233| Ecost (t, x_13783, x_13782) ->
234  h_Ecost t x_13783 x_13782
235    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13782)
236
237(** val expr_rect_Type0 :
238    (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
239    -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
240    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
241    expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
242    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
243    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
244    -> 'a1) -> AST.typ -> expr -> 'a1 **)
245let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13791 = function
246| Id (t, x_13793) -> h_Id t x_13793
247| Cst (t, x_13794) -> h_Cst t x_13794
248| Op1 (t, t', x_13796, x_13795) ->
249  h_Op1 t t' x_13796 x_13795
250    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13795)
251| Op2 (t1, t2, t', x_13799, x_13798, x_13797) ->
252  h_Op2 t1 t2 t' x_13799 x_13798 x_13797
253    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13798)
254    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13797)
255| Mem (t, x_13800) ->
256  h_Mem t x_13800
257    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
258      x_13800)
259| Cond (sz, sg, t, x_13803, x_13802, x_13801) ->
260  h_Cond sz sg t x_13803 x_13802 x_13801
261    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
262      (sz, sg)) x_13803)
263    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13802)
264    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13801)
265| Ecost (t, x_13805, x_13804) ->
266  h_Ecost t x_13805 x_13804
267    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13804)
268
269(** val expr_inv_rect_Type4 :
270    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
271    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
272    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
273    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
274    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
275    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
276    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
277    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
278    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
279    __ -> __ -> 'a1) -> 'a1 **)
280let expr_inv_rect_Type4 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
281  let hcut = expr_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
282
283(** val expr_inv_rect_Type3 :
284    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
285    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
286    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
287    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
288    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
289    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
290    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
291    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
292    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
293    __ -> __ -> 'a1) -> 'a1 **)
294let expr_inv_rect_Type3 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
295  let hcut = expr_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
296
297(** val expr_inv_rect_Type2 :
298    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
299    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
300    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
301    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
302    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
303    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
304    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
305    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
306    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
307    __ -> __ -> 'a1) -> 'a1 **)
308let expr_inv_rect_Type2 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
309  let hcut = expr_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
310
311(** val expr_inv_rect_Type1 :
312    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
313    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
314    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
315    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
316    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
317    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
318    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
319    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
320    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
321    __ -> __ -> 'a1) -> 'a1 **)
322let expr_inv_rect_Type1 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
323  let hcut = expr_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
324
325(** val expr_inv_rect_Type0 :
326    AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
327    -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
328    FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
329    'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
330    expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
331    'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
332    (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
333    -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
334    'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
335    __ -> __ -> 'a1) -> 'a1 **)
336let expr_inv_rect_Type0 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
337  let hcut = expr_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
338
339(** val expr_jmdiscr : AST.typ -> expr -> expr -> __ **)
340let expr_jmdiscr a1 x y =
341  Logic.eq_rect_Type2 x
342    (match x with
343     | Id (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
344     | Cst (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
345     | Op1 (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
346     | Op2 (a0, a10, a2, a3, a4, a5) ->
347       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
348     | Mem (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
349     | Cond (a0, a10, a2, a3, a4, a5) ->
350       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
351     | Ecost (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
352
353type expr_vars = __
354
355type stmt =
356| St_skip
357| St_assign of AST.typ * AST.ident * expr
358| St_store of AST.typ * expr * expr
359| St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
360   * (AST.typ, expr) Types.dPair List.list
361| St_seq of stmt * stmt
362| St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
363| St_return of (AST.typ, expr) Types.dPair Types.option
364| St_label of PreIdentifiers.identifier * stmt
365| St_goto of PreIdentifiers.identifier
366| St_cost of CostLabel.costlabel * stmt
367
368(** val stmt_rect_Type4 :
369    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
370    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
371    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
372    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
373    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
374    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
375    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
376    -> 'a1) -> stmt -> 'a1 **)
377let rec stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
378| St_skip -> h_St_skip
379| St_assign (t, x_13976, x_13975) -> h_St_assign t x_13976 x_13975
380| St_store (t, x_13978, x_13977) -> h_St_store t x_13978 x_13977
381| St_call (x_13981, x_13980, x_13979) -> h_St_call x_13981 x_13980 x_13979
382| St_seq (x_13983, x_13982) ->
383  h_St_seq x_13983 x_13982
384    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
385      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13983)
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_13982)
388| St_ifthenelse (sz, sg, x_13986, x_13985, x_13984) ->
389  h_St_ifthenelse sz sg x_13986 x_13985 x_13984
390    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
391      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13985)
392    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
393      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13984)
394| St_return x_13987 -> h_St_return x_13987
395| St_label (x_13989, x_13988) ->
396  h_St_label x_13989 x_13988
397    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
398      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13988)
399| St_goto x_13990 -> h_St_goto x_13990
400| St_cost (x_13992, x_13991) ->
401  h_St_cost x_13992 x_13991
402    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
403      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13991)
404
405(** val stmt_rect_Type3 :
406    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
407    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
408    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
409    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
410    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
411    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
412    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
413    -> 'a1) -> stmt -> 'a1 **)
414let rec stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
415| St_skip -> h_St_skip
416| St_assign (t, x_14034, x_14033) -> h_St_assign t x_14034 x_14033
417| St_store (t, x_14036, x_14035) -> h_St_store t x_14036 x_14035
418| St_call (x_14039, x_14038, x_14037) -> h_St_call x_14039 x_14038 x_14037
419| St_seq (x_14041, x_14040) ->
420  h_St_seq x_14041 x_14040
421    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
422      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14041)
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_14040)
425| St_ifthenelse (sz, sg, x_14044, x_14043, x_14042) ->
426  h_St_ifthenelse sz sg x_14044 x_14043 x_14042
427    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
428      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14043)
429    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
430      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14042)
431| St_return x_14045 -> h_St_return x_14045
432| St_label (x_14047, x_14046) ->
433  h_St_label x_14047 x_14046
434    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
435      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14046)
436| St_goto x_14048 -> h_St_goto x_14048
437| St_cost (x_14050, x_14049) ->
438  h_St_cost x_14050 x_14049
439    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
440      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14049)
441
442(** val stmt_rect_Type2 :
443    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
444    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
445    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
446    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
447    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
448    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
449    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
450    -> 'a1) -> stmt -> 'a1 **)
451let rec stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
452| St_skip -> h_St_skip
453| St_assign (t, x_14063, x_14062) -> h_St_assign t x_14063 x_14062
454| St_store (t, x_14065, x_14064) -> h_St_store t x_14065 x_14064
455| St_call (x_14068, x_14067, x_14066) -> h_St_call x_14068 x_14067 x_14066
456| St_seq (x_14070, x_14069) ->
457  h_St_seq x_14070 x_14069
458    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
459      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14070)
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_14069)
462| St_ifthenelse (sz, sg, x_14073, x_14072, x_14071) ->
463  h_St_ifthenelse sz sg x_14073 x_14072 x_14071
464    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
465      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14072)
466    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
467      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14071)
468| St_return x_14074 -> h_St_return x_14074
469| St_label (x_14076, x_14075) ->
470  h_St_label x_14076 x_14075
471    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
472      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14075)
473| St_goto x_14077 -> h_St_goto x_14077
474| St_cost (x_14079, x_14078) ->
475  h_St_cost x_14079 x_14078
476    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
477      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14078)
478
479(** val stmt_rect_Type1 :
480    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
481    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
482    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
483    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
484    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
485    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
486    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
487    -> 'a1) -> stmt -> 'a1 **)
488let rec stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
489| St_skip -> h_St_skip
490| St_assign (t, x_14092, x_14091) -> h_St_assign t x_14092 x_14091
491| St_store (t, x_14094, x_14093) -> h_St_store t x_14094 x_14093
492| St_call (x_14097, x_14096, x_14095) -> h_St_call x_14097 x_14096 x_14095
493| St_seq (x_14099, x_14098) ->
494  h_St_seq x_14099 x_14098
495    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
496      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14099)
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_14098)
499| St_ifthenelse (sz, sg, x_14102, x_14101, x_14100) ->
500  h_St_ifthenelse sz sg x_14102 x_14101 x_14100
501    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
502      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14101)
503    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
504      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14100)
505| St_return x_14103 -> h_St_return x_14103
506| St_label (x_14105, x_14104) ->
507  h_St_label x_14105 x_14104
508    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
509      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14104)
510| St_goto x_14106 -> h_St_goto x_14106
511| St_cost (x_14108, x_14107) ->
512  h_St_cost x_14108 x_14107
513    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
514      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14107)
515
516(** val stmt_rect_Type0 :
517    'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
518    -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
519    (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
520    'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
521    'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
522    -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
523    (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
524    -> 'a1) -> stmt -> 'a1 **)
525let rec stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
526| St_skip -> h_St_skip
527| St_assign (t, x_14121, x_14120) -> h_St_assign t x_14121 x_14120
528| St_store (t, x_14123, x_14122) -> h_St_store t x_14123 x_14122
529| St_call (x_14126, x_14125, x_14124) -> h_St_call x_14126 x_14125 x_14124
530| St_seq (x_14128, x_14127) ->
531  h_St_seq x_14128 x_14127
532    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
533      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14128)
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_14127)
536| St_ifthenelse (sz, sg, x_14131, x_14130, x_14129) ->
537  h_St_ifthenelse sz sg x_14131 x_14130 x_14129
538    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
539      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14130)
540    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
541      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14129)
542| St_return x_14132 -> h_St_return x_14132
543| St_label (x_14134, x_14133) ->
544  h_St_label x_14134 x_14133
545    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
546      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14133)
547| St_goto x_14135 -> h_St_goto x_14135
548| St_cost (x_14137, x_14136) ->
549  h_St_cost x_14137 x_14136
550    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
551      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14136)
552
553(** val stmt_inv_rect_Type4 :
554    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
555    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
556    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
557    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
558    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
559    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
560    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
561    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
562    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
563let stmt_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
564  let hcut = stmt_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
565
566(** val stmt_inv_rect_Type3 :
567    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
568    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
569    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
570    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
571    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
572    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
573    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
574    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
575    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
576let stmt_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
577  let hcut = stmt_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
578
579(** val stmt_inv_rect_Type2 :
580    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
581    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
582    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
583    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
584    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
585    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
586    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
587    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
588    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
589let stmt_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
590  let hcut = stmt_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
591
592(** val stmt_inv_rect_Type1 :
593    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
594    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
595    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
596    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
597    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
598    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
599    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
600    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
601    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
602let stmt_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
603  let hcut = stmt_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
604
605(** val stmt_inv_rect_Type0 :
606    stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
607    (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
608    Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
609    -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
610    'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
611    'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
612    Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
613    -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
614    (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
615let stmt_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
616  let hcut = stmt_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
617
618(** val stmt_discr : stmt -> stmt -> __ **)
619let stmt_discr x y =
620  Logic.eq_rect_Type2 x
621    (match x with
622     | St_skip -> Obj.magic (fun _ dH -> dH)
623     | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
624     | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
625     | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
626     | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
627     | St_ifthenelse (a0, a1, a2, a3, a4) ->
628       Obj.magic (fun _ dH -> dH __ __ __ __ __)
629     | St_return a0 -> Obj.magic (fun _ dH -> dH __)
630     | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
631     | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
632     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
633
634(** val stmt_jmdiscr : stmt -> stmt -> __ **)
635let stmt_jmdiscr x y =
636  Logic.eq_rect_Type2 x
637    (match x with
638     | St_skip -> Obj.magic (fun _ dH -> dH)
639     | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
640     | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
641     | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
642     | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
643     | St_ifthenelse (a0, a1, a2, a3, a4) ->
644       Obj.magic (fun _ dH -> dH __ __ __ __ __)
645     | St_return a0 -> Obj.magic (fun _ dH -> dH __)
646     | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
647     | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
648     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
649
650type stmt_P = __
651
652(** val labels_of : stmt -> PreIdentifiers.identifier List.list **)
653let rec labels_of = function
654| St_skip -> List.Nil
655| St_assign (x, x0, x1) -> List.Nil
656| St_store (x, x0, x1) -> List.Nil
657| St_call (x, x0, x1) -> List.Nil
658| St_seq (s1, s2) -> List.append (labels_of s1) (labels_of s2)
659| St_ifthenelse (x, x0, x1, s1, s2) ->
660  List.append (labels_of s1) (labels_of s2)
661| St_return x -> List.Nil
662| St_label (l, s0) -> List.Cons (l, (labels_of s0))
663| St_goto x -> List.Nil
664| St_cost (x, s0) -> labels_of s0
665
666(** val cminor_stmt_inv_rect_Type4 :
667    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
668    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
669    'a1 **)
670let rec cminor_stmt_inv_rect_Type4 env labels rettyp s h_mk_cminor_stmt_inv =
671  h_mk_cminor_stmt_inv __ __ __
672
673(** val cminor_stmt_inv_rect_Type5 :
674    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
675    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
676    'a1 **)
677let rec cminor_stmt_inv_rect_Type5 env labels rettyp s h_mk_cminor_stmt_inv =
678  h_mk_cminor_stmt_inv __ __ __
679
680(** val cminor_stmt_inv_rect_Type3 :
681    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
682    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
683    'a1 **)
684let rec cminor_stmt_inv_rect_Type3 env labels rettyp s h_mk_cminor_stmt_inv =
685  h_mk_cminor_stmt_inv __ __ __
686
687(** val cminor_stmt_inv_rect_Type2 :
688    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
689    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
690    'a1 **)
691let rec cminor_stmt_inv_rect_Type2 env labels rettyp s h_mk_cminor_stmt_inv =
692  h_mk_cminor_stmt_inv __ __ __
693
694(** val cminor_stmt_inv_rect_Type1 :
695    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
696    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
697    'a1 **)
698let rec cminor_stmt_inv_rect_Type1 env labels rettyp s h_mk_cminor_stmt_inv =
699  h_mk_cminor_stmt_inv __ __ __
700
701(** val cminor_stmt_inv_rect_Type0 :
702    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
703    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
704    'a1 **)
705let rec cminor_stmt_inv_rect_Type0 env labels rettyp s h_mk_cminor_stmt_inv =
706  h_mk_cminor_stmt_inv __ __ __
707
708(** val cminor_stmt_inv_inv_rect_Type4 :
709    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
710    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
711    'a1) -> 'a1 **)
712let cminor_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
713  let hcut = cminor_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __
714
715(** val cminor_stmt_inv_inv_rect_Type3 :
716    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
717    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
718    'a1) -> 'a1 **)
719let cminor_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
720  let hcut = cminor_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __
721
722(** val cminor_stmt_inv_inv_rect_Type2 :
723    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
724    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
725    'a1) -> 'a1 **)
726let cminor_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
727  let hcut = cminor_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __
728
729(** val cminor_stmt_inv_inv_rect_Type1 :
730    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
731    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
732    'a1) -> 'a1 **)
733let cminor_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
734  let hcut = cminor_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __
735
736(** val cminor_stmt_inv_inv_rect_Type0 :
737    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
738    List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
739    'a1) -> 'a1 **)
740let cminor_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
741  let hcut = cminor_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __
742
743(** val cminor_stmt_inv_discr :
744    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
745    List.list -> AST.typ Types.option -> stmt -> __ **)
746let cminor_stmt_inv_discr a1 a2 a3 a4 =
747  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
748
749(** val cminor_stmt_inv_jmdiscr :
750    (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
751    List.list -> AST.typ Types.option -> stmt -> __ **)
752let cminor_stmt_inv_jmdiscr a1 a2 a3 a4 =
753  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
754
755type internal_function = { f_return : AST.typ Types.option;
756                           f_params : (AST.ident, AST.typ) Types.prod
757                                      List.list;
758                           f_vars : (AST.ident, AST.typ) Types.prod List.list;
759                           f_stacksize : Nat.nat; f_body : stmt }
760
761(** val internal_function_rect_Type4 :
762    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
763    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
764    -> 'a1) -> internal_function -> 'a1 **)
765let rec internal_function_rect_Type4 h_mk_internal_function x_14432 =
766  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
767    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14432
768  in
769  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
770    __
771
772(** val internal_function_rect_Type5 :
773    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
774    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
775    -> 'a1) -> internal_function -> 'a1 **)
776let rec internal_function_rect_Type5 h_mk_internal_function x_14434 =
777  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
778    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14434
779  in
780  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
781    __
782
783(** val internal_function_rect_Type3 :
784    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
785    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
786    -> 'a1) -> internal_function -> 'a1 **)
787let rec internal_function_rect_Type3 h_mk_internal_function x_14436 =
788  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
789    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14436
790  in
791  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
792    __
793
794(** val internal_function_rect_Type2 :
795    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
796    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
797    -> 'a1) -> internal_function -> 'a1 **)
798let rec internal_function_rect_Type2 h_mk_internal_function x_14438 =
799  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
800    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14438
801  in
802  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
803    __
804
805(** val internal_function_rect_Type1 :
806    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
807    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
808    -> 'a1) -> internal_function -> 'a1 **)
809let rec internal_function_rect_Type1 h_mk_internal_function x_14440 =
810  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
811    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14440
812  in
813  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
814    __
815
816(** val internal_function_rect_Type0 :
817    (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
818    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
819    -> 'a1) -> internal_function -> 'a1 **)
820let rec internal_function_rect_Type0 h_mk_internal_function x_14442 =
821  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
822    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14442
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.