source: extracted/rTLabs_syntax.ml @ 2716

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

...

File size: 30.3 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Proper
12
13open PositiveMap
14
15open Deqsets
16
17open ErrorMessages
18
19open PreIdentifiers
20
21open Errors
22
23open Extralib
24
25open Setoids
26
27open Monad
28
29open Option
30
31open Lists
32
33open Positive
34
35open Identifiers
36
37open Arithmetic
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Types
66
67open AST
68
69open CostLabel
70
71open FrontEndVal
72
73open Hide
74
75open ByteValues
76
77open GenMem
78
79open FrontEndMem
80
81open Division
82
83open Z
84
85open BitVectorZ
86
87open Pointers
88
89open Coqlib
90
91open Values
92
93open FrontEndOps
94
95open Order
96
97open Registers
98
99open BitVectorTrie
100
101open Graphs
102
103type statement =
104| St_skip of Graphs.label
105| St_cost of CostLabel.costlabel * Graphs.label
106| St_const of AST.typ * Registers.register * FrontEndOps.constant
107   * Graphs.label
108| St_op1 of AST.typ * AST.typ * FrontEndOps.unary_operation
109   * Registers.register * Registers.register * Graphs.label
110| St_op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation
111   * Registers.register * Registers.register * Registers.register
112   * Graphs.label
113| St_load of AST.typ * Registers.register * Registers.register * Graphs.label
114| St_store of AST.typ * Registers.register * Registers.register
115   * Graphs.label
116| St_call_id of AST.ident * Registers.register List.list
117   * Registers.register Types.option * Graphs.label
118| St_call_ptr of Registers.register * Registers.register List.list
119   * Registers.register Types.option * Graphs.label
120| St_cond of Registers.register * Graphs.label * Graphs.label
121| St_return
122
123(** val statement_rect_Type4 :
124    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
125    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
126    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
127    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
128    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
129    Registers.register -> Registers.register -> Registers.register ->
130    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
131    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
132    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
133    (AST.ident -> Registers.register List.list -> Registers.register
134    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
135    Registers.register List.list -> Registers.register Types.option ->
136    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
137    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
138let rec statement_rect_Type4 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
139| St_skip x_11448 -> h_St_skip x_11448
140| St_cost (x_11450, x_11449) -> h_St_cost x_11450 x_11449
141| St_const (t, x_11453, x_11452, x_11451) ->
142  h_St_const t x_11453 x_11452 x_11451
143| St_op1 (t', t, x_11457, x_11456, x_11455, x_11454) ->
144  h_St_op1 t' t x_11457 x_11456 x_11455 x_11454
145| St_op2 (t', t1, t2, x_11462, x_11461, x_11460, x_11459, x_11458) ->
146  h_St_op2 t' t1 t2 x_11462 x_11461 x_11460 x_11459 x_11458
147| St_load (x_11466, x_11465, x_11464, x_11463) ->
148  h_St_load x_11466 x_11465 x_11464 x_11463
149| St_store (x_11470, x_11469, x_11468, x_11467) ->
150  h_St_store x_11470 x_11469 x_11468 x_11467
151| St_call_id (x_11474, x_11473, x_11472, x_11471) ->
152  h_St_call_id x_11474 x_11473 x_11472 x_11471
153| St_call_ptr (x_11478, x_11477, x_11476, x_11475) ->
154  h_St_call_ptr x_11478 x_11477 x_11476 x_11475
155| St_cond (x_11481, x_11480, x_11479) -> h_St_cond x_11481 x_11480 x_11479
156| St_return -> h_St_return
157
158(** val statement_rect_Type5 :
159    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
160    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
161    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
162    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
163    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
164    Registers.register -> Registers.register -> Registers.register ->
165    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
166    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
167    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
168    (AST.ident -> Registers.register List.list -> Registers.register
169    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
170    Registers.register List.list -> Registers.register Types.option ->
171    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
172    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
173let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
174| St_skip x_11494 -> h_St_skip x_11494
175| St_cost (x_11496, x_11495) -> h_St_cost x_11496 x_11495
176| St_const (t, x_11499, x_11498, x_11497) ->
177  h_St_const t x_11499 x_11498 x_11497
178| St_op1 (t', t, x_11503, x_11502, x_11501, x_11500) ->
179  h_St_op1 t' t x_11503 x_11502 x_11501 x_11500
180| St_op2 (t', t1, t2, x_11508, x_11507, x_11506, x_11505, x_11504) ->
181  h_St_op2 t' t1 t2 x_11508 x_11507 x_11506 x_11505 x_11504
182| St_load (x_11512, x_11511, x_11510, x_11509) ->
183  h_St_load x_11512 x_11511 x_11510 x_11509
184| St_store (x_11516, x_11515, x_11514, x_11513) ->
185  h_St_store x_11516 x_11515 x_11514 x_11513
186| St_call_id (x_11520, x_11519, x_11518, x_11517) ->
187  h_St_call_id x_11520 x_11519 x_11518 x_11517
188| St_call_ptr (x_11524, x_11523, x_11522, x_11521) ->
189  h_St_call_ptr x_11524 x_11523 x_11522 x_11521
190| St_cond (x_11527, x_11526, x_11525) -> h_St_cond x_11527 x_11526 x_11525
191| St_return -> h_St_return
192
193(** val statement_rect_Type3 :
194    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
195    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
196    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
197    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
198    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
199    Registers.register -> Registers.register -> Registers.register ->
200    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
201    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
202    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
203    (AST.ident -> Registers.register List.list -> Registers.register
204    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
205    Registers.register List.list -> Registers.register Types.option ->
206    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
207    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
208let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
209| St_skip x_11540 -> h_St_skip x_11540
210| St_cost (x_11542, x_11541) -> h_St_cost x_11542 x_11541
211| St_const (t, x_11545, x_11544, x_11543) ->
212  h_St_const t x_11545 x_11544 x_11543
213| St_op1 (t', t, x_11549, x_11548, x_11547, x_11546) ->
214  h_St_op1 t' t x_11549 x_11548 x_11547 x_11546
215| St_op2 (t', t1, t2, x_11554, x_11553, x_11552, x_11551, x_11550) ->
216  h_St_op2 t' t1 t2 x_11554 x_11553 x_11552 x_11551 x_11550
217| St_load (x_11558, x_11557, x_11556, x_11555) ->
218  h_St_load x_11558 x_11557 x_11556 x_11555
219| St_store (x_11562, x_11561, x_11560, x_11559) ->
220  h_St_store x_11562 x_11561 x_11560 x_11559
221| St_call_id (x_11566, x_11565, x_11564, x_11563) ->
222  h_St_call_id x_11566 x_11565 x_11564 x_11563
223| St_call_ptr (x_11570, x_11569, x_11568, x_11567) ->
224  h_St_call_ptr x_11570 x_11569 x_11568 x_11567
225| St_cond (x_11573, x_11572, x_11571) -> h_St_cond x_11573 x_11572 x_11571
226| St_return -> h_St_return
227
228(** val statement_rect_Type2 :
229    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
230    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
231    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
232    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
233    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
234    Registers.register -> Registers.register -> Registers.register ->
235    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
236    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
237    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
238    (AST.ident -> Registers.register List.list -> Registers.register
239    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
240    Registers.register List.list -> Registers.register Types.option ->
241    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
242    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
243let rec statement_rect_Type2 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
244| St_skip x_11586 -> h_St_skip x_11586
245| St_cost (x_11588, x_11587) -> h_St_cost x_11588 x_11587
246| St_const (t, x_11591, x_11590, x_11589) ->
247  h_St_const t x_11591 x_11590 x_11589
248| St_op1 (t', t, x_11595, x_11594, x_11593, x_11592) ->
249  h_St_op1 t' t x_11595 x_11594 x_11593 x_11592
250| St_op2 (t', t1, t2, x_11600, x_11599, x_11598, x_11597, x_11596) ->
251  h_St_op2 t' t1 t2 x_11600 x_11599 x_11598 x_11597 x_11596
252| St_load (x_11604, x_11603, x_11602, x_11601) ->
253  h_St_load x_11604 x_11603 x_11602 x_11601
254| St_store (x_11608, x_11607, x_11606, x_11605) ->
255  h_St_store x_11608 x_11607 x_11606 x_11605
256| St_call_id (x_11612, x_11611, x_11610, x_11609) ->
257  h_St_call_id x_11612 x_11611 x_11610 x_11609
258| St_call_ptr (x_11616, x_11615, x_11614, x_11613) ->
259  h_St_call_ptr x_11616 x_11615 x_11614 x_11613
260| St_cond (x_11619, x_11618, x_11617) -> h_St_cond x_11619 x_11618 x_11617
261| St_return -> h_St_return
262
263(** val statement_rect_Type1 :
264    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
265    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
266    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
267    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
268    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
269    Registers.register -> Registers.register -> Registers.register ->
270    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
271    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
272    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
273    (AST.ident -> Registers.register List.list -> Registers.register
274    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
275    Registers.register List.list -> Registers.register Types.option ->
276    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
277    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
278let rec statement_rect_Type1 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
279| St_skip x_11632 -> h_St_skip x_11632
280| St_cost (x_11634, x_11633) -> h_St_cost x_11634 x_11633
281| St_const (t, x_11637, x_11636, x_11635) ->
282  h_St_const t x_11637 x_11636 x_11635
283| St_op1 (t', t, x_11641, x_11640, x_11639, x_11638) ->
284  h_St_op1 t' t x_11641 x_11640 x_11639 x_11638
285| St_op2 (t', t1, t2, x_11646, x_11645, x_11644, x_11643, x_11642) ->
286  h_St_op2 t' t1 t2 x_11646 x_11645 x_11644 x_11643 x_11642
287| St_load (x_11650, x_11649, x_11648, x_11647) ->
288  h_St_load x_11650 x_11649 x_11648 x_11647
289| St_store (x_11654, x_11653, x_11652, x_11651) ->
290  h_St_store x_11654 x_11653 x_11652 x_11651
291| St_call_id (x_11658, x_11657, x_11656, x_11655) ->
292  h_St_call_id x_11658 x_11657 x_11656 x_11655
293| St_call_ptr (x_11662, x_11661, x_11660, x_11659) ->
294  h_St_call_ptr x_11662 x_11661 x_11660 x_11659
295| St_cond (x_11665, x_11664, x_11663) -> h_St_cond x_11665 x_11664 x_11663
296| St_return -> h_St_return
297
298(** val statement_rect_Type0 :
299    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
300    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
301    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
302    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
303    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
304    Registers.register -> Registers.register -> Registers.register ->
305    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
306    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
307    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
308    (AST.ident -> Registers.register List.list -> Registers.register
309    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
310    Registers.register List.list -> Registers.register Types.option ->
311    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
312    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
313let rec statement_rect_Type0 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
314| St_skip x_11678 -> h_St_skip x_11678
315| St_cost (x_11680, x_11679) -> h_St_cost x_11680 x_11679
316| St_const (t, x_11683, x_11682, x_11681) ->
317  h_St_const t x_11683 x_11682 x_11681
318| St_op1 (t', t, x_11687, x_11686, x_11685, x_11684) ->
319  h_St_op1 t' t x_11687 x_11686 x_11685 x_11684
320| St_op2 (t', t1, t2, x_11692, x_11691, x_11690, x_11689, x_11688) ->
321  h_St_op2 t' t1 t2 x_11692 x_11691 x_11690 x_11689 x_11688
322| St_load (x_11696, x_11695, x_11694, x_11693) ->
323  h_St_load x_11696 x_11695 x_11694 x_11693
324| St_store (x_11700, x_11699, x_11698, x_11697) ->
325  h_St_store x_11700 x_11699 x_11698 x_11697
326| St_call_id (x_11704, x_11703, x_11702, x_11701) ->
327  h_St_call_id x_11704 x_11703 x_11702 x_11701
328| St_call_ptr (x_11708, x_11707, x_11706, x_11705) ->
329  h_St_call_ptr x_11708 x_11707 x_11706 x_11705
330| St_cond (x_11711, x_11710, x_11709) -> h_St_cond x_11711 x_11710 x_11709
331| St_return -> h_St_return
332
333(** val statement_inv_rect_Type4 :
334    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
335    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
336    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
337    -> FrontEndOps.unary_operation -> Registers.register ->
338    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
339    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
340    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
341    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
342    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
343    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
344    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
345    (Registers.register -> Registers.register List.list -> Registers.register
346    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
347    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
348let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
349  let hcut = statement_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
350  hcut __
351
352(** val statement_inv_rect_Type3 :
353    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
354    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
355    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
356    -> FrontEndOps.unary_operation -> Registers.register ->
357    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
358    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
359    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
360    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
361    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
362    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
363    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
364    (Registers.register -> Registers.register List.list -> Registers.register
365    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
366    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
367let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
368  let hcut = statement_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
369  hcut __
370
371(** val statement_inv_rect_Type2 :
372    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
373    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
374    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
375    -> FrontEndOps.unary_operation -> Registers.register ->
376    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
377    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
378    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
379    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
380    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
381    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
382    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
383    (Registers.register -> Registers.register List.list -> Registers.register
384    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
385    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
386let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
387  let hcut = statement_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
388  hcut __
389
390(** val statement_inv_rect_Type1 :
391    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
392    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
393    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
394    -> FrontEndOps.unary_operation -> Registers.register ->
395    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
396    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
397    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
398    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
399    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
400    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
401    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
402    (Registers.register -> Registers.register List.list -> Registers.register
403    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
404    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
405let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
406  let hcut = statement_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
407  hcut __
408
409(** val statement_inv_rect_Type0 :
410    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
411    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
412    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
413    -> FrontEndOps.unary_operation -> Registers.register ->
414    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
415    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
416    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
417    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
418    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
419    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
420    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
421    (Registers.register -> Registers.register List.list -> Registers.register
422    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
423    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
424let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
425  let hcut = statement_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
426  hcut __
427
428(** val statement_jmdiscr : statement -> statement -> __ **)
429let statement_jmdiscr x y =
430  Logic.eq_rect_Type2 x
431    (match x with
432     | St_skip a0 -> Obj.magic (fun _ dH -> dH __)
433     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
434     | St_const (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
435     | St_op1 (a0, a1, a2, a3, a4, a5) ->
436       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
437     | St_op2 (a0, a1, a2, a3, a4, a5, a6, a7) ->
438       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
439     | St_load (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
440     | St_store (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
441     | St_call_id (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
442     | St_call_ptr (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
443     | St_cond (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
444     | St_return -> Obj.magic (fun _ dH -> dH)) y
445
446type internal_function = { f_labgen : Identifiers.universe;
447                           f_reggen : Identifiers.universe;
448                           f_result : (Registers.register, AST.typ)
449                                      Types.prod Types.option;
450                           f_params : (Registers.register, AST.typ)
451                                      Types.prod List.list;
452                           f_locals : (Registers.register, AST.typ)
453                                      Types.prod List.list;
454                           f_stacksize : Nat.nat;
455                           f_graph : statement Graphs.graph;
456                           f_entry : Graphs.label Types.sig0;
457                           f_exit : Graphs.label Types.sig0 }
458
459(** val internal_function_rect_Type4 :
460    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
461    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
462    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
463    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
464    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
465    internal_function -> 'a1 **)
466let rec internal_function_rect_Type4 h_mk_internal_function x_12001 =
467  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
468    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
469    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12001
470  in
471  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
472    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
473
474(** val internal_function_rect_Type5 :
475    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
476    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
477    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
478    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
479    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
480    internal_function -> 'a1 **)
481let rec internal_function_rect_Type5 h_mk_internal_function x_12003 =
482  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
483    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
484    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12003
485  in
486  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
487    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
488
489(** val internal_function_rect_Type3 :
490    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
491    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
492    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
493    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
494    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
495    internal_function -> 'a1 **)
496let rec internal_function_rect_Type3 h_mk_internal_function x_12005 =
497  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
498    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
499    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12005
500  in
501  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
502    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
503
504(** val internal_function_rect_Type2 :
505    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
506    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
507    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
508    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
509    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
510    internal_function -> 'a1 **)
511let rec internal_function_rect_Type2 h_mk_internal_function x_12007 =
512  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
513    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
514    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12007
515  in
516  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
517    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
518
519(** val internal_function_rect_Type1 :
520    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
521    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
522    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
523    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
524    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
525    internal_function -> 'a1 **)
526let rec internal_function_rect_Type1 h_mk_internal_function x_12009 =
527  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
528    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
529    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12009
530  in
531  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
532    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
533
534(** val internal_function_rect_Type0 :
535    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
536    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
537    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
538    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
539    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
540    internal_function -> 'a1 **)
541let rec internal_function_rect_Type0 h_mk_internal_function x_12011 =
542  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
543    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
544    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_12011
545  in
546  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
547    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
548
549(** val f_labgen : internal_function -> Identifiers.universe **)
550let rec f_labgen xxx =
551  xxx.f_labgen
552
553(** val f_reggen : internal_function -> Identifiers.universe **)
554let rec f_reggen xxx =
555  xxx.f_reggen
556
557(** val f_result :
558    internal_function -> (Registers.register, AST.typ) Types.prod
559    Types.option **)
560let rec f_result xxx =
561  xxx.f_result
562
563(** val f_params :
564    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
565let rec f_params xxx =
566  xxx.f_params
567
568(** val f_locals :
569    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
570let rec f_locals xxx =
571  xxx.f_locals
572
573(** val f_stacksize : internal_function -> Nat.nat **)
574let rec f_stacksize xxx =
575  xxx.f_stacksize
576
577(** val f_graph : internal_function -> statement Graphs.graph **)
578let rec f_graph xxx =
579  xxx.f_graph
580
581(** val f_entry : internal_function -> Graphs.label Types.sig0 **)
582let rec f_entry xxx =
583  xxx.f_entry
584
585(** val f_exit : internal_function -> Graphs.label Types.sig0 **)
586let rec f_exit xxx =
587  xxx.f_exit
588
589(** val internal_function_inv_rect_Type4 :
590    internal_function -> (Identifiers.universe -> Identifiers.universe ->
591    (Registers.register, AST.typ) Types.prod Types.option ->
592    (Registers.register, AST.typ) Types.prod List.list ->
593    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
594    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
595    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
596let internal_function_inv_rect_Type4 hterm h1 =
597  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
598
599(** val internal_function_inv_rect_Type3 :
600    internal_function -> (Identifiers.universe -> Identifiers.universe ->
601    (Registers.register, AST.typ) Types.prod Types.option ->
602    (Registers.register, AST.typ) Types.prod List.list ->
603    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
604    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
605    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
606let internal_function_inv_rect_Type3 hterm h1 =
607  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
608
609(** val internal_function_inv_rect_Type2 :
610    internal_function -> (Identifiers.universe -> Identifiers.universe ->
611    (Registers.register, AST.typ) Types.prod Types.option ->
612    (Registers.register, AST.typ) Types.prod List.list ->
613    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
614    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
615    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
616let internal_function_inv_rect_Type2 hterm h1 =
617  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
618
619(** val internal_function_inv_rect_Type1 :
620    internal_function -> (Identifiers.universe -> Identifiers.universe ->
621    (Registers.register, AST.typ) Types.prod Types.option ->
622    (Registers.register, AST.typ) Types.prod List.list ->
623    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
624    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
625    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
626let internal_function_inv_rect_Type1 hterm h1 =
627  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
628
629(** val internal_function_inv_rect_Type0 :
630    internal_function -> (Identifiers.universe -> Identifiers.universe ->
631    (Registers.register, AST.typ) Types.prod Types.option ->
632    (Registers.register, AST.typ) Types.prod List.list ->
633    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
634    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
635    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
636let internal_function_inv_rect_Type0 hterm h1 =
637  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
638
639(** val internal_function_jmdiscr :
640    internal_function -> internal_function -> __ **)
641let internal_function_jmdiscr x y =
642  Logic.eq_rect_Type2 x
643    (let { f_labgen = a0; f_reggen = a1; f_result = a2; f_params = a3;
644       f_locals = a4; f_stacksize = a5; f_graph = a6; f_entry = a9; f_exit =
645       a10 } = x
646     in
647    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
648
649type rTLabs_program = (internal_function AST.fundef, Nat.nat) AST.program
650
Note: See TracBrowser for help on using the repository browser.