source: extracted/rTLabs_syntax.ml @ 3001

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

New extraction.

File size: 30.0 KB
RevLine 
[2601]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
[2649]17open ErrorMessages
18
[2601]19open PreIdentifiers
20
21open Errors
22
23open Extralib
24
25open Lists
26
27open Positive
28
29open Identifiers
30
[2717]31open Exp
32
[2601]33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
[2773]39open Util
40
41open FoldStuff
42
43open BitVector
44
[2601]45open Jmeq
46
47open Russell
48
49open List
50
[2773]51open Setoids
[2601]52
[2773]53open Monad
[2601]54
[2773]55open Option
[2601]56
57open Extranat
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Integers
66
67open Types
68
69open AST
70
71open CostLabel
72
73open FrontEndVal
74
75open Hide
76
77open ByteValues
78
79open GenMem
80
81open FrontEndMem
82
83open Division
84
85open Z
86
87open BitVectorZ
88
89open Pointers
90
[2649]91open Coqlib
92
[2601]93open Values
94
95open FrontEndOps
96
97open Order
98
99open Registers
100
[2773]101open BitVectorTrie
102
[2601]103open Graphs
104
105type statement =
106| St_skip of Graphs.label
107| St_cost of CostLabel.costlabel * Graphs.label
108| St_const of AST.typ * Registers.register * FrontEndOps.constant
109   * Graphs.label
110| St_op1 of AST.typ * AST.typ * FrontEndOps.unary_operation
111   * Registers.register * Registers.register * Graphs.label
112| St_op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation
113   * Registers.register * Registers.register * Registers.register
114   * Graphs.label
115| St_load of AST.typ * Registers.register * Registers.register * Graphs.label
116| St_store of AST.typ * Registers.register * Registers.register
117   * Graphs.label
118| St_call_id of AST.ident * Registers.register List.list
119   * Registers.register Types.option * Graphs.label
120| St_call_ptr of Registers.register * Registers.register List.list
121   * Registers.register Types.option * Graphs.label
122| St_cond of Registers.register * Graphs.label * Graphs.label
123| St_return
124
125(** val statement_rect_Type4 :
126    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
127    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
128    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
129    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
130    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
131    Registers.register -> Registers.register -> Registers.register ->
132    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
133    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
134    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
135    (AST.ident -> Registers.register List.list -> Registers.register
136    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
137    Registers.register List.list -> Registers.register Types.option ->
138    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
139    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
140let 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
[3001]141| St_skip x_6699 -> h_St_skip x_6699
142| St_cost (x_6701, x_6700) -> h_St_cost x_6701 x_6700
143| St_const (t, x_6704, x_6703, x_6702) -> h_St_const t x_6704 x_6703 x_6702
144| St_op1 (t', t, x_6708, x_6707, x_6706, x_6705) ->
145  h_St_op1 t' t x_6708 x_6707 x_6706 x_6705
146| St_op2 (t', t1, t2, x_6713, x_6712, x_6711, x_6710, x_6709) ->
147  h_St_op2 t' t1 t2 x_6713 x_6712 x_6711 x_6710 x_6709
148| St_load (x_6717, x_6716, x_6715, x_6714) ->
149  h_St_load x_6717 x_6716 x_6715 x_6714
150| St_store (x_6721, x_6720, x_6719, x_6718) ->
151  h_St_store x_6721 x_6720 x_6719 x_6718
152| St_call_id (x_6725, x_6724, x_6723, x_6722) ->
153  h_St_call_id x_6725 x_6724 x_6723 x_6722
154| St_call_ptr (x_6729, x_6728, x_6727, x_6726) ->
155  h_St_call_ptr x_6729 x_6728 x_6727 x_6726
156| St_cond (x_6732, x_6731, x_6730) -> h_St_cond x_6732 x_6731 x_6730
[2601]157| St_return -> h_St_return
158
159(** val statement_rect_Type5 :
160    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
161    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
162    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
163    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
164    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
165    Registers.register -> Registers.register -> Registers.register ->
166    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
167    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
168    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
169    (AST.ident -> Registers.register List.list -> Registers.register
170    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
171    Registers.register List.list -> Registers.register Types.option ->
172    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
173    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
174let 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
[3001]175| St_skip x_6745 -> h_St_skip x_6745
176| St_cost (x_6747, x_6746) -> h_St_cost x_6747 x_6746
177| St_const (t, x_6750, x_6749, x_6748) -> h_St_const t x_6750 x_6749 x_6748
178| St_op1 (t', t, x_6754, x_6753, x_6752, x_6751) ->
179  h_St_op1 t' t x_6754 x_6753 x_6752 x_6751
180| St_op2 (t', t1, t2, x_6759, x_6758, x_6757, x_6756, x_6755) ->
181  h_St_op2 t' t1 t2 x_6759 x_6758 x_6757 x_6756 x_6755
182| St_load (x_6763, x_6762, x_6761, x_6760) ->
183  h_St_load x_6763 x_6762 x_6761 x_6760
184| St_store (x_6767, x_6766, x_6765, x_6764) ->
185  h_St_store x_6767 x_6766 x_6765 x_6764
186| St_call_id (x_6771, x_6770, x_6769, x_6768) ->
187  h_St_call_id x_6771 x_6770 x_6769 x_6768
188| St_call_ptr (x_6775, x_6774, x_6773, x_6772) ->
189  h_St_call_ptr x_6775 x_6774 x_6773 x_6772
190| St_cond (x_6778, x_6777, x_6776) -> h_St_cond x_6778 x_6777 x_6776
[2601]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
[3001]209| St_skip x_6791 -> h_St_skip x_6791
210| St_cost (x_6793, x_6792) -> h_St_cost x_6793 x_6792
211| St_const (t, x_6796, x_6795, x_6794) -> h_St_const t x_6796 x_6795 x_6794
212| St_op1 (t', t, x_6800, x_6799, x_6798, x_6797) ->
213  h_St_op1 t' t x_6800 x_6799 x_6798 x_6797
214| St_op2 (t', t1, t2, x_6805, x_6804, x_6803, x_6802, x_6801) ->
215  h_St_op2 t' t1 t2 x_6805 x_6804 x_6803 x_6802 x_6801
216| St_load (x_6809, x_6808, x_6807, x_6806) ->
217  h_St_load x_6809 x_6808 x_6807 x_6806
218| St_store (x_6813, x_6812, x_6811, x_6810) ->
219  h_St_store x_6813 x_6812 x_6811 x_6810
220| St_call_id (x_6817, x_6816, x_6815, x_6814) ->
221  h_St_call_id x_6817 x_6816 x_6815 x_6814
222| St_call_ptr (x_6821, x_6820, x_6819, x_6818) ->
223  h_St_call_ptr x_6821 x_6820 x_6819 x_6818
224| St_cond (x_6824, x_6823, x_6822) -> h_St_cond x_6824 x_6823 x_6822
[2601]225| St_return -> h_St_return
226
227(** val statement_rect_Type2 :
228    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
229    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
230    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
231    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
232    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
233    Registers.register -> Registers.register -> Registers.register ->
234    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
235    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
236    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
237    (AST.ident -> Registers.register List.list -> Registers.register
238    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
239    Registers.register List.list -> Registers.register Types.option ->
240    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
241    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
242let 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
[3001]243| St_skip x_6837 -> h_St_skip x_6837
244| St_cost (x_6839, x_6838) -> h_St_cost x_6839 x_6838
245| St_const (t, x_6842, x_6841, x_6840) -> h_St_const t x_6842 x_6841 x_6840
246| St_op1 (t', t, x_6846, x_6845, x_6844, x_6843) ->
247  h_St_op1 t' t x_6846 x_6845 x_6844 x_6843
248| St_op2 (t', t1, t2, x_6851, x_6850, x_6849, x_6848, x_6847) ->
249  h_St_op2 t' t1 t2 x_6851 x_6850 x_6849 x_6848 x_6847
250| St_load (x_6855, x_6854, x_6853, x_6852) ->
251  h_St_load x_6855 x_6854 x_6853 x_6852
252| St_store (x_6859, x_6858, x_6857, x_6856) ->
253  h_St_store x_6859 x_6858 x_6857 x_6856
254| St_call_id (x_6863, x_6862, x_6861, x_6860) ->
255  h_St_call_id x_6863 x_6862 x_6861 x_6860
256| St_call_ptr (x_6867, x_6866, x_6865, x_6864) ->
257  h_St_call_ptr x_6867 x_6866 x_6865 x_6864
258| St_cond (x_6870, x_6869, x_6868) -> h_St_cond x_6870 x_6869 x_6868
[2601]259| St_return -> h_St_return
260
261(** val statement_rect_Type1 :
262    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
263    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
264    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
265    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
266    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
267    Registers.register -> Registers.register -> Registers.register ->
268    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
269    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
270    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
271    (AST.ident -> Registers.register List.list -> Registers.register
272    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
273    Registers.register List.list -> Registers.register Types.option ->
274    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
275    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
276let 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
[3001]277| St_skip x_6883 -> h_St_skip x_6883
278| St_cost (x_6885, x_6884) -> h_St_cost x_6885 x_6884
279| St_const (t, x_6888, x_6887, x_6886) -> h_St_const t x_6888 x_6887 x_6886
280| St_op1 (t', t, x_6892, x_6891, x_6890, x_6889) ->
281  h_St_op1 t' t x_6892 x_6891 x_6890 x_6889
282| St_op2 (t', t1, t2, x_6897, x_6896, x_6895, x_6894, x_6893) ->
283  h_St_op2 t' t1 t2 x_6897 x_6896 x_6895 x_6894 x_6893
284| St_load (x_6901, x_6900, x_6899, x_6898) ->
285  h_St_load x_6901 x_6900 x_6899 x_6898
286| St_store (x_6905, x_6904, x_6903, x_6902) ->
287  h_St_store x_6905 x_6904 x_6903 x_6902
288| St_call_id (x_6909, x_6908, x_6907, x_6906) ->
289  h_St_call_id x_6909 x_6908 x_6907 x_6906
290| St_call_ptr (x_6913, x_6912, x_6911, x_6910) ->
291  h_St_call_ptr x_6913 x_6912 x_6911 x_6910
292| St_cond (x_6916, x_6915, x_6914) -> h_St_cond x_6916 x_6915 x_6914
[2601]293| St_return -> h_St_return
294
295(** val statement_rect_Type0 :
296    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
297    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
298    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
299    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
300    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
301    Registers.register -> Registers.register -> Registers.register ->
302    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
303    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
304    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
305    (AST.ident -> Registers.register List.list -> Registers.register
306    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
307    Registers.register List.list -> Registers.register Types.option ->
308    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
309    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
310let 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
[3001]311| St_skip x_6929 -> h_St_skip x_6929
312| St_cost (x_6931, x_6930) -> h_St_cost x_6931 x_6930
313| St_const (t, x_6934, x_6933, x_6932) -> h_St_const t x_6934 x_6933 x_6932
314| St_op1 (t', t, x_6938, x_6937, x_6936, x_6935) ->
315  h_St_op1 t' t x_6938 x_6937 x_6936 x_6935
316| St_op2 (t', t1, t2, x_6943, x_6942, x_6941, x_6940, x_6939) ->
317  h_St_op2 t' t1 t2 x_6943 x_6942 x_6941 x_6940 x_6939
318| St_load (x_6947, x_6946, x_6945, x_6944) ->
319  h_St_load x_6947 x_6946 x_6945 x_6944
320| St_store (x_6951, x_6950, x_6949, x_6948) ->
321  h_St_store x_6951 x_6950 x_6949 x_6948
322| St_call_id (x_6955, x_6954, x_6953, x_6952) ->
323  h_St_call_id x_6955 x_6954 x_6953 x_6952
324| St_call_ptr (x_6959, x_6958, x_6957, x_6956) ->
325  h_St_call_ptr x_6959 x_6958 x_6957 x_6956
326| St_cond (x_6962, x_6961, x_6960) -> h_St_cond x_6962 x_6961 x_6960
[2601]327| St_return -> h_St_return
328
329(** val statement_inv_rect_Type4 :
330    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
331    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
332    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
333    -> FrontEndOps.unary_operation -> Registers.register ->
334    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
335    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
336    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
337    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
338    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
339    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
340    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
341    (Registers.register -> Registers.register List.list -> Registers.register
342    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
343    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
344let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
345  let hcut = statement_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
346  hcut __
347
348(** val statement_inv_rect_Type3 :
349    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
350    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
351    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
352    -> FrontEndOps.unary_operation -> Registers.register ->
353    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
354    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
355    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
356    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
357    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
358    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
359    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
360    (Registers.register -> Registers.register List.list -> Registers.register
361    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
362    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
363let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
364  let hcut = statement_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
365  hcut __
366
367(** val statement_inv_rect_Type2 :
368    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
369    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
370    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
371    -> FrontEndOps.unary_operation -> Registers.register ->
372    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
373    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
374    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
375    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
376    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
377    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
378    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
379    (Registers.register -> Registers.register List.list -> Registers.register
380    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
381    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
382let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
383  let hcut = statement_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
384  hcut __
385
386(** val statement_inv_rect_Type1 :
387    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
388    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
389    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
390    -> FrontEndOps.unary_operation -> Registers.register ->
391    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
392    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
393    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
394    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
395    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
396    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
397    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
398    (Registers.register -> Registers.register List.list -> Registers.register
399    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
400    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
401let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
402  let hcut = statement_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
403  hcut __
404
405(** val statement_inv_rect_Type0 :
406    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
407    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
408    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
409    -> FrontEndOps.unary_operation -> Registers.register ->
410    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
411    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
412    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
413    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
414    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
415    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
416    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
417    (Registers.register -> Registers.register List.list -> Registers.register
418    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
419    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
420let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
421  let hcut = statement_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
422  hcut __
423
424(** val statement_jmdiscr : statement -> statement -> __ **)
425let statement_jmdiscr x y =
426  Logic.eq_rect_Type2 x
427    (match x with
428     | St_skip a0 -> Obj.magic (fun _ dH -> dH __)
429     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
430     | St_const (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
431     | St_op1 (a0, a1, a2, a3, a4, a5) ->
432       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
433     | St_op2 (a0, a1, a2, a3, a4, a5, a6, a7) ->
434       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
435     | St_load (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
436     | St_store (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
437     | St_call_id (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
438     | St_call_ptr (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
439     | St_cond (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
440     | St_return -> Obj.magic (fun _ dH -> dH)) y
441
442type internal_function = { f_labgen : Identifiers.universe;
443                           f_reggen : Identifiers.universe;
444                           f_result : (Registers.register, AST.typ)
445                                      Types.prod Types.option;
446                           f_params : (Registers.register, AST.typ)
447                                      Types.prod List.list;
448                           f_locals : (Registers.register, AST.typ)
449                                      Types.prod List.list;
450                           f_stacksize : Nat.nat;
451                           f_graph : statement Graphs.graph;
452                           f_entry : Graphs.label Types.sig0;
453                           f_exit : Graphs.label Types.sig0 }
454
455(** val internal_function_rect_Type4 :
456    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
457    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
458    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
459    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
[2997]460    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
[2601]461    internal_function -> 'a1 **)
[3001]462let rec internal_function_rect_Type4 h_mk_internal_function x_7252 =
[2601]463  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
464    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
[3001]465    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7252
[2601]466  in
467  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
[2997]468    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
[2601]469
470(** val internal_function_rect_Type5 :
471    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
472    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
473    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
474    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
[2997]475    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
[2601]476    internal_function -> 'a1 **)
[3001]477let rec internal_function_rect_Type5 h_mk_internal_function x_7254 =
[2601]478  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
479    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
[3001]480    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7254
[2601]481  in
482  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
[2997]483    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
[2601]484
485(** val internal_function_rect_Type3 :
486    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
487    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
488    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
489    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
[2997]490    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
[2601]491    internal_function -> 'a1 **)
[3001]492let rec internal_function_rect_Type3 h_mk_internal_function x_7256 =
[2601]493  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
494    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
[3001]495    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7256
[2601]496  in
497  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
[2997]498    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
[2601]499
500(** val internal_function_rect_Type2 :
501    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
502    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
503    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
504    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
[2997]505    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
[2601]506    internal_function -> 'a1 **)
[3001]507let rec internal_function_rect_Type2 h_mk_internal_function x_7258 =
[2601]508  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
509    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
[3001]510    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7258
[2601]511  in
512  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
[2997]513    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
[2601]514
515(** val internal_function_rect_Type1 :
516    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
517    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
518    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
519    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
[2997]520    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
[2601]521    internal_function -> 'a1 **)
[3001]522let rec internal_function_rect_Type1 h_mk_internal_function x_7260 =
[2601]523  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
524    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
[3001]525    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7260
[2601]526  in
527  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
[2997]528    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
[2601]529
530(** val internal_function_rect_Type0 :
531    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
532    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
533    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
534    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
[2997]535    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
[2601]536    internal_function -> 'a1 **)
[3001]537let rec internal_function_rect_Type0 h_mk_internal_function x_7262 =
[2601]538  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
539    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
[3001]540    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_7262
[2601]541  in
542  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
[2997]543    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
[2601]544
545(** val f_labgen : internal_function -> Identifiers.universe **)
546let rec f_labgen xxx =
547  xxx.f_labgen
548
549(** val f_reggen : internal_function -> Identifiers.universe **)
550let rec f_reggen xxx =
551  xxx.f_reggen
552
553(** val f_result :
554    internal_function -> (Registers.register, AST.typ) Types.prod
555    Types.option **)
556let rec f_result xxx =
557  xxx.f_result
558
559(** val f_params :
560    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
561let rec f_params xxx =
562  xxx.f_params
563
564(** val f_locals :
565    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
566let rec f_locals xxx =
567  xxx.f_locals
568
569(** val f_stacksize : internal_function -> Nat.nat **)
570let rec f_stacksize xxx =
571  xxx.f_stacksize
572
573(** val f_graph : internal_function -> statement Graphs.graph **)
574let rec f_graph xxx =
575  xxx.f_graph
576
577(** val f_entry : internal_function -> Graphs.label Types.sig0 **)
578let rec f_entry xxx =
579  xxx.f_entry
580
581(** val f_exit : internal_function -> Graphs.label Types.sig0 **)
582let rec f_exit xxx =
583  xxx.f_exit
584
585(** val internal_function_inv_rect_Type4 :
586    internal_function -> (Identifiers.universe -> Identifiers.universe ->
587    (Registers.register, AST.typ) Types.prod Types.option ->
588    (Registers.register, AST.typ) Types.prod List.list ->
589    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
590    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
[2997]591    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
[2601]592let internal_function_inv_rect_Type4 hterm h1 =
593  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
594
595(** val internal_function_inv_rect_Type3 :
596    internal_function -> (Identifiers.universe -> Identifiers.universe ->
597    (Registers.register, AST.typ) Types.prod Types.option ->
598    (Registers.register, AST.typ) Types.prod List.list ->
599    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
600    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
[2997]601    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
[2601]602let internal_function_inv_rect_Type3 hterm h1 =
603  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
604
605(** val internal_function_inv_rect_Type2 :
606    internal_function -> (Identifiers.universe -> Identifiers.universe ->
607    (Registers.register, AST.typ) Types.prod Types.option ->
608    (Registers.register, AST.typ) Types.prod List.list ->
609    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
610    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
[2997]611    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
[2601]612let internal_function_inv_rect_Type2 hterm h1 =
613  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
614
615(** val internal_function_inv_rect_Type1 :
616    internal_function -> (Identifiers.universe -> Identifiers.universe ->
617    (Registers.register, AST.typ) Types.prod Types.option ->
618    (Registers.register, AST.typ) Types.prod List.list ->
619    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
620    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
[2997]621    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
[2601]622let internal_function_inv_rect_Type1 hterm h1 =
623  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
624
625(** val internal_function_inv_rect_Type0 :
626    internal_function -> (Identifiers.universe -> Identifiers.universe ->
627    (Registers.register, AST.typ) Types.prod Types.option ->
628    (Registers.register, AST.typ) Types.prod List.list ->
629    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
630    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
[2997]631    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
[2601]632let internal_function_inv_rect_Type0 hterm h1 =
633  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
634
635(** val internal_function_jmdiscr :
636    internal_function -> internal_function -> __ **)
637let internal_function_jmdiscr x y =
638  Logic.eq_rect_Type2 x
639    (let { f_labgen = a0; f_reggen = a1; f_result = a2; f_params = a3;
640       f_locals = a4; f_stacksize = a5; f_graph = a6; f_entry = a9; f_exit =
641       a10 } = x
642     in
[2997]643    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y
[2601]644
[2951]645type rTLabs_program =
646  (internal_function AST.fundef, AST.init_data List.list) AST.program
[2601]647
Note: See TracBrowser for help on using the repository browser.