1 | open Preamble |
---|
2 | |
---|
3 | open Hints_declaration |
---|
4 | |
---|
5 | open Core_notation |
---|
6 | |
---|
7 | open Pts |
---|
8 | |
---|
9 | open Logic |
---|
10 | |
---|
11 | open Proper |
---|
12 | |
---|
13 | open PositiveMap |
---|
14 | |
---|
15 | open Deqsets |
---|
16 | |
---|
17 | open ErrorMessages |
---|
18 | |
---|
19 | open PreIdentifiers |
---|
20 | |
---|
21 | open Errors |
---|
22 | |
---|
23 | open Extralib |
---|
24 | |
---|
25 | open Setoids |
---|
26 | |
---|
27 | open Monad |
---|
28 | |
---|
29 | open Option |
---|
30 | |
---|
31 | open Lists |
---|
32 | |
---|
33 | open Positive |
---|
34 | |
---|
35 | open Identifiers |
---|
36 | |
---|
37 | open Exp |
---|
38 | |
---|
39 | open Arithmetic |
---|
40 | |
---|
41 | open Vector |
---|
42 | |
---|
43 | open Div_and_mod |
---|
44 | |
---|
45 | open Jmeq |
---|
46 | |
---|
47 | open Russell |
---|
48 | |
---|
49 | open List |
---|
50 | |
---|
51 | open Util |
---|
52 | |
---|
53 | open FoldStuff |
---|
54 | |
---|
55 | open BitVector |
---|
56 | |
---|
57 | open Extranat |
---|
58 | |
---|
59 | open Bool |
---|
60 | |
---|
61 | open Relations |
---|
62 | |
---|
63 | open Nat |
---|
64 | |
---|
65 | open Integers |
---|
66 | |
---|
67 | open Types |
---|
68 | |
---|
69 | open AST |
---|
70 | |
---|
71 | open BitVectorTrie |
---|
72 | |
---|
73 | open CostLabel |
---|
74 | |
---|
75 | open FrontEndVal |
---|
76 | |
---|
77 | open Hide |
---|
78 | |
---|
79 | open ByteValues |
---|
80 | |
---|
81 | open GenMem |
---|
82 | |
---|
83 | open FrontEndMem |
---|
84 | |
---|
85 | open Division |
---|
86 | |
---|
87 | open Z |
---|
88 | |
---|
89 | open BitVectorZ |
---|
90 | |
---|
91 | open Pointers |
---|
92 | |
---|
93 | open Coqlib |
---|
94 | |
---|
95 | open Values |
---|
96 | |
---|
97 | open FrontEndOps |
---|
98 | |
---|
99 | open Order |
---|
100 | |
---|
101 | open Registers |
---|
102 | |
---|
103 | open Graphs |
---|
104 | |
---|
105 | type 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 **) |
---|
140 | let 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 **) |
---|
175 | let 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 **) |
---|
210 | let 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 **) |
---|
245 | let 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 **) |
---|
280 | let 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 **) |
---|
315 | let 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 **) |
---|
350 | let 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 **) |
---|
369 | let 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 **) |
---|
388 | let 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 **) |
---|
407 | let 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 **) |
---|
426 | let 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 -> __ **) |
---|
431 | let 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 | |
---|
448 | type 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 **) |
---|
468 | let 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 **) |
---|
483 | let 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 **) |
---|
498 | let 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 **) |
---|
513 | let 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 **) |
---|
528 | let 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 **) |
---|
543 | let 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 **) |
---|
552 | let rec f_labgen xxx = |
---|
553 | xxx.f_labgen |
---|
554 | |
---|
555 | (** val f_reggen : internal_function -> Identifiers.universe **) |
---|
556 | let 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 **) |
---|
562 | let rec f_result xxx = |
---|
563 | xxx.f_result |
---|
564 | |
---|
565 | (** val f_params : |
---|
566 | internal_function -> (Registers.register, AST.typ) Types.prod List.list **) |
---|
567 | let rec f_params xxx = |
---|
568 | xxx.f_params |
---|
569 | |
---|
570 | (** val f_locals : |
---|
571 | internal_function -> (Registers.register, AST.typ) Types.prod List.list **) |
---|
572 | let rec f_locals xxx = |
---|
573 | xxx.f_locals |
---|
574 | |
---|
575 | (** val f_stacksize : internal_function -> Nat.nat **) |
---|
576 | let rec f_stacksize xxx = |
---|
577 | xxx.f_stacksize |
---|
578 | |
---|
579 | (** val f_graph : internal_function -> statement Graphs.graph **) |
---|
580 | let rec f_graph xxx = |
---|
581 | xxx.f_graph |
---|
582 | |
---|
583 | (** val f_entry : internal_function -> Graphs.label Types.sig0 **) |
---|
584 | let rec f_entry xxx = |
---|
585 | xxx.f_entry |
---|
586 | |
---|
587 | (** val f_exit : internal_function -> Graphs.label Types.sig0 **) |
---|
588 | let 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 **) |
---|
598 | let 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 **) |
---|
608 | let 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 **) |
---|
618 | let 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 **) |
---|
628 | let 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 **) |
---|
638 | let 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 -> __ **) |
---|
643 | let 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 | |
---|
651 | type rTLabs_program = (internal_function AST.fundef, Nat.nat) AST.program |
---|
652 | |
---|