source: extracted/rTLabs_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: 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 Exp
38
39open Arithmetic
40
41open Vector
42
43open Div_and_mod
44
45open Jmeq
46
47open Russell
48
49open List
50
51open Util
52
53open FoldStuff
54
55open BitVector
56
57open Extranat
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Integers
66
67open Types
68
69open AST
70
71open BitVectorTrie
72
73open CostLabel
74
75open FrontEndVal
76
77open Hide
78
79open ByteValues
80
81open GenMem
82
83open FrontEndMem
84
85open Division
86
87open Z
88
89open BitVectorZ
90
91open Pointers
92
93open Coqlib
94
95open Values
96
97open FrontEndOps
98
99open Order
100
101open Registers
102
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
141| St_skip x_14738 -> h_St_skip x_14738
142| St_cost (x_14740, x_14739) -> h_St_cost x_14740 x_14739
143| St_const (t, x_14743, x_14742, x_14741) ->
144  h_St_const t x_14743 x_14742 x_14741
145| St_op1 (t', t, x_14747, x_14746, x_14745, x_14744) ->
146  h_St_op1 t' t x_14747 x_14746 x_14745 x_14744
147| St_op2 (t', t1, t2, x_14752, x_14751, x_14750, x_14749, x_14748) ->
148  h_St_op2 t' t1 t2 x_14752 x_14751 x_14750 x_14749 x_14748
149| St_load (x_14756, x_14755, x_14754, x_14753) ->
150  h_St_load x_14756 x_14755 x_14754 x_14753
151| St_store (x_14760, x_14759, x_14758, x_14757) ->
152  h_St_store x_14760 x_14759 x_14758 x_14757
153| St_call_id (x_14764, x_14763, x_14762, x_14761) ->
154  h_St_call_id x_14764 x_14763 x_14762 x_14761
155| St_call_ptr (x_14768, x_14767, x_14766, x_14765) ->
156  h_St_call_ptr x_14768 x_14767 x_14766 x_14765
157| St_cond (x_14771, x_14770, x_14769) -> h_St_cond x_14771 x_14770 x_14769
158| St_return -> h_St_return
159
160(** val statement_rect_Type5 :
161    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
162    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
163    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
164    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
165    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
166    Registers.register -> Registers.register -> Registers.register ->
167    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
168    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
169    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
170    (AST.ident -> Registers.register List.list -> Registers.register
171    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
172    Registers.register List.list -> Registers.register Types.option ->
173    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
174    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
175let 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
176| St_skip x_14784 -> h_St_skip x_14784
177| St_cost (x_14786, x_14785) -> h_St_cost x_14786 x_14785
178| St_const (t, x_14789, x_14788, x_14787) ->
179  h_St_const t x_14789 x_14788 x_14787
180| St_op1 (t', t, x_14793, x_14792, x_14791, x_14790) ->
181  h_St_op1 t' t x_14793 x_14792 x_14791 x_14790
182| St_op2 (t', t1, t2, x_14798, x_14797, x_14796, x_14795, x_14794) ->
183  h_St_op2 t' t1 t2 x_14798 x_14797 x_14796 x_14795 x_14794
184| St_load (x_14802, x_14801, x_14800, x_14799) ->
185  h_St_load x_14802 x_14801 x_14800 x_14799
186| St_store (x_14806, x_14805, x_14804, x_14803) ->
187  h_St_store x_14806 x_14805 x_14804 x_14803
188| St_call_id (x_14810, x_14809, x_14808, x_14807) ->
189  h_St_call_id x_14810 x_14809 x_14808 x_14807
190| St_call_ptr (x_14814, x_14813, x_14812, x_14811) ->
191  h_St_call_ptr x_14814 x_14813 x_14812 x_14811
192| St_cond (x_14817, x_14816, x_14815) -> h_St_cond x_14817 x_14816 x_14815
193| St_return -> h_St_return
194
195(** val statement_rect_Type3 :
196    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
197    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
198    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
199    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
200    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
201    Registers.register -> Registers.register -> Registers.register ->
202    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
203    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
204    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
205    (AST.ident -> Registers.register List.list -> Registers.register
206    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
207    Registers.register List.list -> Registers.register Types.option ->
208    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
209    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
210let 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
211| St_skip x_14830 -> h_St_skip x_14830
212| St_cost (x_14832, x_14831) -> h_St_cost x_14832 x_14831
213| St_const (t, x_14835, x_14834, x_14833) ->
214  h_St_const t x_14835 x_14834 x_14833
215| St_op1 (t', t, x_14839, x_14838, x_14837, x_14836) ->
216  h_St_op1 t' t x_14839 x_14838 x_14837 x_14836
217| St_op2 (t', t1, t2, x_14844, x_14843, x_14842, x_14841, x_14840) ->
218  h_St_op2 t' t1 t2 x_14844 x_14843 x_14842 x_14841 x_14840
219| St_load (x_14848, x_14847, x_14846, x_14845) ->
220  h_St_load x_14848 x_14847 x_14846 x_14845
221| St_store (x_14852, x_14851, x_14850, x_14849) ->
222  h_St_store x_14852 x_14851 x_14850 x_14849
223| St_call_id (x_14856, x_14855, x_14854, x_14853) ->
224  h_St_call_id x_14856 x_14855 x_14854 x_14853
225| St_call_ptr (x_14860, x_14859, x_14858, x_14857) ->
226  h_St_call_ptr x_14860 x_14859 x_14858 x_14857
227| St_cond (x_14863, x_14862, x_14861) -> h_St_cond x_14863 x_14862 x_14861
228| St_return -> h_St_return
229
230(** val statement_rect_Type2 :
231    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
232    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
233    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
234    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
235    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
236    Registers.register -> Registers.register -> Registers.register ->
237    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
238    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
239    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
240    (AST.ident -> Registers.register List.list -> Registers.register
241    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
242    Registers.register List.list -> Registers.register Types.option ->
243    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
244    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
245let 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
246| St_skip x_14876 -> h_St_skip x_14876
247| St_cost (x_14878, x_14877) -> h_St_cost x_14878 x_14877
248| St_const (t, x_14881, x_14880, x_14879) ->
249  h_St_const t x_14881 x_14880 x_14879
250| St_op1 (t', t, x_14885, x_14884, x_14883, x_14882) ->
251  h_St_op1 t' t x_14885 x_14884 x_14883 x_14882
252| St_op2 (t', t1, t2, x_14890, x_14889, x_14888, x_14887, x_14886) ->
253  h_St_op2 t' t1 t2 x_14890 x_14889 x_14888 x_14887 x_14886
254| St_load (x_14894, x_14893, x_14892, x_14891) ->
255  h_St_load x_14894 x_14893 x_14892 x_14891
256| St_store (x_14898, x_14897, x_14896, x_14895) ->
257  h_St_store x_14898 x_14897 x_14896 x_14895
258| St_call_id (x_14902, x_14901, x_14900, x_14899) ->
259  h_St_call_id x_14902 x_14901 x_14900 x_14899
260| St_call_ptr (x_14906, x_14905, x_14904, x_14903) ->
261  h_St_call_ptr x_14906 x_14905 x_14904 x_14903
262| St_cond (x_14909, x_14908, x_14907) -> h_St_cond x_14909 x_14908 x_14907
263| St_return -> h_St_return
264
265(** val statement_rect_Type1 :
266    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
267    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
268    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
269    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
270    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
271    Registers.register -> Registers.register -> Registers.register ->
272    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
273    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
274    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
275    (AST.ident -> Registers.register List.list -> Registers.register
276    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
277    Registers.register List.list -> Registers.register Types.option ->
278    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
279    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
280let 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
281| St_skip x_14922 -> h_St_skip x_14922
282| St_cost (x_14924, x_14923) -> h_St_cost x_14924 x_14923
283| St_const (t, x_14927, x_14926, x_14925) ->
284  h_St_const t x_14927 x_14926 x_14925
285| St_op1 (t', t, x_14931, x_14930, x_14929, x_14928) ->
286  h_St_op1 t' t x_14931 x_14930 x_14929 x_14928
287| St_op2 (t', t1, t2, x_14936, x_14935, x_14934, x_14933, x_14932) ->
288  h_St_op2 t' t1 t2 x_14936 x_14935 x_14934 x_14933 x_14932
289| St_load (x_14940, x_14939, x_14938, x_14937) ->
290  h_St_load x_14940 x_14939 x_14938 x_14937
291| St_store (x_14944, x_14943, x_14942, x_14941) ->
292  h_St_store x_14944 x_14943 x_14942 x_14941
293| St_call_id (x_14948, x_14947, x_14946, x_14945) ->
294  h_St_call_id x_14948 x_14947 x_14946 x_14945
295| St_call_ptr (x_14952, x_14951, x_14950, x_14949) ->
296  h_St_call_ptr x_14952 x_14951 x_14950 x_14949
297| St_cond (x_14955, x_14954, x_14953) -> h_St_cond x_14955 x_14954 x_14953
298| St_return -> h_St_return
299
300(** val statement_rect_Type0 :
301    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
302    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
303    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
304    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
305    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
306    Registers.register -> Registers.register -> Registers.register ->
307    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
308    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
309    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
310    (AST.ident -> Registers.register List.list -> Registers.register
311    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
312    Registers.register List.list -> Registers.register Types.option ->
313    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
314    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
315let 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
316| St_skip x_14968 -> h_St_skip x_14968
317| St_cost (x_14970, x_14969) -> h_St_cost x_14970 x_14969
318| St_const (t, x_14973, x_14972, x_14971) ->
319  h_St_const t x_14973 x_14972 x_14971
320| St_op1 (t', t, x_14977, x_14976, x_14975, x_14974) ->
321  h_St_op1 t' t x_14977 x_14976 x_14975 x_14974
322| St_op2 (t', t1, t2, x_14982, x_14981, x_14980, x_14979, x_14978) ->
323  h_St_op2 t' t1 t2 x_14982 x_14981 x_14980 x_14979 x_14978
324| St_load (x_14986, x_14985, x_14984, x_14983) ->
325  h_St_load x_14986 x_14985 x_14984 x_14983
326| St_store (x_14990, x_14989, x_14988, x_14987) ->
327  h_St_store x_14990 x_14989 x_14988 x_14987
328| St_call_id (x_14994, x_14993, x_14992, x_14991) ->
329  h_St_call_id x_14994 x_14993 x_14992 x_14991
330| St_call_ptr (x_14998, x_14997, x_14996, x_14995) ->
331  h_St_call_ptr x_14998 x_14997 x_14996 x_14995
332| St_cond (x_15001, x_15000, x_14999) -> h_St_cond x_15001 x_15000 x_14999
333| St_return -> h_St_return
334
335(** val statement_inv_rect_Type4 :
336    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
337    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
338    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
339    -> FrontEndOps.unary_operation -> Registers.register ->
340    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
341    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
342    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
343    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
344    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
345    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
346    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
347    (Registers.register -> Registers.register List.list -> Registers.register
348    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
349    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
350let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
351  let hcut = statement_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
352  hcut __
353
354(** val statement_inv_rect_Type3 :
355    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
356    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
357    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
358    -> FrontEndOps.unary_operation -> Registers.register ->
359    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
360    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
361    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
362    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
363    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
364    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
365    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
366    (Registers.register -> Registers.register List.list -> Registers.register
367    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
368    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
369let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
370  let hcut = statement_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
371  hcut __
372
373(** val statement_inv_rect_Type2 :
374    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
375    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
376    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
377    -> FrontEndOps.unary_operation -> Registers.register ->
378    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
379    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
380    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
381    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
382    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
383    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
384    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
385    (Registers.register -> Registers.register List.list -> Registers.register
386    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
387    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
388let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
389  let hcut = statement_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
390  hcut __
391
392(** val statement_inv_rect_Type1 :
393    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
394    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
395    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
396    -> FrontEndOps.unary_operation -> Registers.register ->
397    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
398    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
399    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
400    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
401    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
402    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
403    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
404    (Registers.register -> Registers.register List.list -> Registers.register
405    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
406    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
407let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
408  let hcut = statement_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
409  hcut __
410
411(** val statement_inv_rect_Type0 :
412    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
413    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
414    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
415    -> FrontEndOps.unary_operation -> Registers.register ->
416    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
417    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
418    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
419    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
420    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
421    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
422    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
423    (Registers.register -> Registers.register List.list -> Registers.register
424    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
425    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
426let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
427  let hcut = statement_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
428  hcut __
429
430(** val statement_jmdiscr : statement -> statement -> __ **)
431let statement_jmdiscr x y =
432  Logic.eq_rect_Type2 x
433    (match x with
434     | St_skip a0 -> Obj.magic (fun _ dH -> dH __)
435     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
436     | St_const (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
437     | St_op1 (a0, a1, a2, a3, a4, a5) ->
438       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
439     | St_op2 (a0, a1, a2, a3, a4, a5, a6, a7) ->
440       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
441     | St_load (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
442     | St_store (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
443     | St_call_id (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
444     | St_call_ptr (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
445     | St_cond (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
446     | St_return -> Obj.magic (fun _ dH -> dH)) y
447
448type internal_function = { f_labgen : Identifiers.universe;
449                           f_reggen : Identifiers.universe;
450                           f_result : (Registers.register, AST.typ)
451                                      Types.prod Types.option;
452                           f_params : (Registers.register, AST.typ)
453                                      Types.prod List.list;
454                           f_locals : (Registers.register, AST.typ)
455                                      Types.prod List.list;
456                           f_stacksize : Nat.nat;
457                           f_graph : statement Graphs.graph;
458                           f_entry : Graphs.label Types.sig0;
459                           f_exit : Graphs.label Types.sig0 }
460
461(** val internal_function_rect_Type4 :
462    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
463    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
464    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
465    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
466    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
467    internal_function -> 'a1 **)
468let rec internal_function_rect_Type4 h_mk_internal_function x_15291 =
469  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
470    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
471    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15291
472  in
473  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
474    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
475
476(** val internal_function_rect_Type5 :
477    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
478    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
479    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
480    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
481    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
482    internal_function -> 'a1 **)
483let rec internal_function_rect_Type5 h_mk_internal_function x_15293 =
484  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
485    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
486    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15293
487  in
488  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
489    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
490
491(** val internal_function_rect_Type3 :
492    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
493    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
494    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
495    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
496    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
497    internal_function -> 'a1 **)
498let rec internal_function_rect_Type3 h_mk_internal_function x_15295 =
499  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
500    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
501    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15295
502  in
503  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
504    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
505
506(** val internal_function_rect_Type2 :
507    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
508    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
509    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
510    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
511    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
512    internal_function -> 'a1 **)
513let rec internal_function_rect_Type2 h_mk_internal_function x_15297 =
514  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
515    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
516    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15297
517  in
518  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
519    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
520
521(** val internal_function_rect_Type1 :
522    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
523    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
524    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
525    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
526    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
527    internal_function -> 'a1 **)
528let rec internal_function_rect_Type1 h_mk_internal_function x_15299 =
529  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
530    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
531    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15299
532  in
533  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
534    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
535
536(** val internal_function_rect_Type0 :
537    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
538    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
539    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
540    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
541    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
542    internal_function -> 'a1 **)
543let rec internal_function_rect_Type0 h_mk_internal_function x_15301 =
544  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
545    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
546    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15301
547  in
548  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
549    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
550
551(** val f_labgen : internal_function -> Identifiers.universe **)
552let rec f_labgen xxx =
553  xxx.f_labgen
554
555(** val f_reggen : internal_function -> Identifiers.universe **)
556let rec f_reggen xxx =
557  xxx.f_reggen
558
559(** val f_result :
560    internal_function -> (Registers.register, AST.typ) Types.prod
561    Types.option **)
562let rec f_result xxx =
563  xxx.f_result
564
565(** val f_params :
566    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
567let rec f_params xxx =
568  xxx.f_params
569
570(** val f_locals :
571    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
572let rec f_locals xxx =
573  xxx.f_locals
574
575(** val f_stacksize : internal_function -> Nat.nat **)
576let rec f_stacksize xxx =
577  xxx.f_stacksize
578
579(** val f_graph : internal_function -> statement Graphs.graph **)
580let rec f_graph xxx =
581  xxx.f_graph
582
583(** val f_entry : internal_function -> Graphs.label Types.sig0 **)
584let rec f_entry xxx =
585  xxx.f_entry
586
587(** val f_exit : internal_function -> Graphs.label Types.sig0 **)
588let rec f_exit xxx =
589  xxx.f_exit
590
591(** val internal_function_inv_rect_Type4 :
592    internal_function -> (Identifiers.universe -> Identifiers.universe ->
593    (Registers.register, AST.typ) Types.prod Types.option ->
594    (Registers.register, AST.typ) Types.prod List.list ->
595    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
596    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
597    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
598let internal_function_inv_rect_Type4 hterm h1 =
599  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
600
601(** val internal_function_inv_rect_Type3 :
602    internal_function -> (Identifiers.universe -> Identifiers.universe ->
603    (Registers.register, AST.typ) Types.prod Types.option ->
604    (Registers.register, AST.typ) Types.prod List.list ->
605    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
606    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
607    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
608let internal_function_inv_rect_Type3 hterm h1 =
609  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
610
611(** val internal_function_inv_rect_Type2 :
612    internal_function -> (Identifiers.universe -> Identifiers.universe ->
613    (Registers.register, AST.typ) Types.prod Types.option ->
614    (Registers.register, AST.typ) Types.prod List.list ->
615    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
616    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
617    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
618let internal_function_inv_rect_Type2 hterm h1 =
619  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
620
621(** val internal_function_inv_rect_Type1 :
622    internal_function -> (Identifiers.universe -> Identifiers.universe ->
623    (Registers.register, AST.typ) Types.prod Types.option ->
624    (Registers.register, AST.typ) Types.prod List.list ->
625    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
626    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
627    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
628let internal_function_inv_rect_Type1 hterm h1 =
629  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
630
631(** val internal_function_inv_rect_Type0 :
632    internal_function -> (Identifiers.universe -> Identifiers.universe ->
633    (Registers.register, AST.typ) Types.prod Types.option ->
634    (Registers.register, AST.typ) Types.prod List.list ->
635    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
636    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
637    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
638let internal_function_inv_rect_Type0 hterm h1 =
639  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
640
641(** val internal_function_jmdiscr :
642    internal_function -> internal_function -> __ **)
643let internal_function_jmdiscr x y =
644  Logic.eq_rect_Type2 x
645    (let { f_labgen = a0; f_reggen = a1; f_result = a2; f_params = a3;
646       f_locals = a4; f_stacksize = a5; f_graph = a6; f_entry = a9; f_exit =
647       a10 } = x
648     in
649    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
650
651type rTLabs_program = (internal_function AST.fundef, Nat.nat) AST.program
652
Note: See TracBrowser for help on using the repository browser.