1 | include "RTLabs/import.ma". |
---|
2 | include "common/Animation.ma". |
---|
3 | |
---|
4 | |
---|
5 | |
---|
6 | |
---|
7 | definition id_search := ident_of_nat 0. |
---|
8 | definition search9 := 50. |
---|
9 | definition search8 := 49. |
---|
10 | definition search7 := 48. |
---|
11 | definition search6 := 47. |
---|
12 | definition search50 := 46. |
---|
13 | definition search5 := 45. |
---|
14 | definition search49 := 44. |
---|
15 | definition search48 := 43. |
---|
16 | definition search47 := 42. |
---|
17 | definition search46 := 41. |
---|
18 | definition search45 := 40. |
---|
19 | definition search44 := 39. |
---|
20 | definition search43 := 38. |
---|
21 | definition search42 := 37. |
---|
22 | definition search41 := 36. |
---|
23 | definition search40 := 35. |
---|
24 | definition search4 := 34. |
---|
25 | definition search39 := 33. |
---|
26 | definition search38 := 32. |
---|
27 | definition search37 := 31. |
---|
28 | definition search36 := 30. |
---|
29 | definition search35 := 29. |
---|
30 | definition search34 := 28. |
---|
31 | definition search33 := 27. |
---|
32 | definition search32 := 26. |
---|
33 | definition search31 := 25. |
---|
34 | definition search30 := 24. |
---|
35 | definition search3 := 23. |
---|
36 | definition search29 := 22. |
---|
37 | definition search28 := 21. |
---|
38 | definition search27 := 20. |
---|
39 | definition search26 := 19. |
---|
40 | definition search25 := 18. |
---|
41 | definition search24 := 17. |
---|
42 | definition search23 := 16. |
---|
43 | definition search22 := 15. |
---|
44 | definition search21 := 14. |
---|
45 | definition search20 := 13. |
---|
46 | definition search2 := 12. |
---|
47 | definition search19 := 11. |
---|
48 | definition search18 := 10. |
---|
49 | definition search17 := 9. |
---|
50 | definition search16 := 8. |
---|
51 | definition search15 := 7. |
---|
52 | definition search14 := 6. |
---|
53 | definition search13 := 5. |
---|
54 | definition search12 := 4. |
---|
55 | definition search11 := 3. |
---|
56 | definition search10 := 2. |
---|
57 | definition search1 := 1. |
---|
58 | definition search0 := 0. |
---|
59 | definition C_cost1 := costlabel_of_nat 8. |
---|
60 | definition C_cost8 := costlabel_of_nat 7. |
---|
61 | definition C_cost6 := costlabel_of_nat 6. |
---|
62 | definition C_cost7 := costlabel_of_nat 5. |
---|
63 | definition C_cost4 := costlabel_of_nat 4. |
---|
64 | definition C_cost5 := costlabel_of_nat 3. |
---|
65 | definition C_cost2 := costlabel_of_nat 2. |
---|
66 | definition C_cost3 := costlabel_of_nat 1. |
---|
67 | definition C_cost0 := costlabel_of_nat 0. |
---|
68 | |
---|
69 | |
---|
70 | definition pre_search := mk_pre_internal_function |
---|
71 | (Some ? (pair ?? 6 (ASTint I8 Unsigned))) |
---|
72 | [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))] |
---|
73 | [(pair ?? 3 (ASTint I8 Unsigned)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTint I8 Signed)); (pair ?? 9 (ASTint I8 Unsigned)); (pair ?? 10 (ASTint I8 Unsigned)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Unsigned)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I8 Unsigned)); (pair ?? 15 (ASTint I8 Unsigned)); (pair ?? 16 (ASTint I8 Unsigned)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTint I8 Unsigned)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTptr Any)); (pair ?? 21 (ASTint I8 Unsigned)); (pair ?? 22 (ASTint I8 Unsigned)); (pair ?? 23 (ASTint I8 Unsigned)); (pair ?? 24 (ASTint I8 Unsigned)); (pair ?? 25 (ASTptr Any)); (pair ?? 26 (ASTint I8 Unsigned)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTint I8 Unsigned)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I8 Unsigned)); (pair ?? 32 (ASTint I8 Unsigned)); (pair ?? 33 (ASTint I8 Unsigned)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTint I8 Signed))] |
---|
74 | 0 |
---|
75 | [ |
---|
76 | (pair ?? search9 (make_St_const 10 (Ointconst I8 (repr ? 1)) search8)); |
---|
77 | (pair ?? search8 (make_St_op2 Oadd 9 4 10 search7)); |
---|
78 | (pair ?? search7 (make_St_op1 (Ocastint Unsigned I8) 5 9 search5)); |
---|
79 | (pair ?? search6 (make_St_cost C_cost1 search5)); |
---|
80 | (pair ?? search50 (make_St_cost C_cost8 search49)); |
---|
81 | (pair ?? search5 (make_St_skip search44)); |
---|
82 | (pair ?? search49 (make_St_const 35 (Ointconst I8 (repr ? 0)) search48)); |
---|
83 | (pair ?? search48 (make_St_op1 (Ocastint Signed I8) 5 35 search47)); |
---|
84 | (pair ?? search47 (make_St_const 34 (Ointconst I8 (repr ? 1)) search46)); |
---|
85 | (pair ?? search46 (make_St_op2 Osub 33 1 34 search45)); |
---|
86 | (pair ?? search45 (make_St_op1 (Ocastint Unsigned I8) 3 33 search5)); |
---|
87 | (pair ?? search44 (make_St_op2 (Ocmpu Cge) 32 3 5 search43)); |
---|
88 | (pair ?? search43 (make_St_op1 Onotbool 31 32 search42)); |
---|
89 | (pair ?? search42 (make_St_cond 31 search4 search41)); |
---|
90 | (pair ?? search41 (make_St_cost C_cost6 search40)); |
---|
91 | (pair ?? search40 (make_St_op2 Oadd 29 3 5 search39)); |
---|
92 | (pair ?? search4 (make_St_cost C_cost7 search3)); |
---|
93 | (pair ?? search39 (make_St_const 30 (Ointconst I8 (repr ? 2)) search38)); |
---|
94 | (pair ?? search38 (make_St_op2 Odivu 28 29 30 search37)); |
---|
95 | (pair ?? search37 (make_St_op1 (Ocastint Unsigned I8) 4 28 search36)); |
---|
96 | (pair ?? search36 (make_St_const 27 (Ointconst I8 (repr ? 1)) search35)); |
---|
97 | (pair ?? search35 (make_St_op2 Omul 26 4 27 search34)); |
---|
98 | (pair ?? search34 (make_St_op2 Oaddp 25 0 26 search33)); |
---|
99 | (pair ?? search33 (make_St_load Mint8unsigned 25 24 search32)); |
---|
100 | (pair ?? search32 (make_St_op2 (Ocmpu Ceq) 23 24 2 search31)); |
---|
101 | (pair ?? search31 (make_St_cond 23 search30 search28)); |
---|
102 | (pair ?? search30 (make_St_cost C_cost4 search29)); |
---|
103 | (pair ?? search3 (make_St_const 8 (Ointconst I8 (repr ? 1)) search2)); |
---|
104 | (pair ?? search29 (make_St_op1 Oid 6 4 search0)); |
---|
105 | (pair ?? search28 (make_St_cost C_cost5 search27)); |
---|
106 | (pair ?? search27 (make_St_const 22 (Ointconst I8 (repr ? 1)) search26)); |
---|
107 | (pair ?? search26 (make_St_op2 Omul 21 4 22 search25)); |
---|
108 | (pair ?? search25 (make_St_op2 Oaddp 20 0 21 search24)); |
---|
109 | (pair ?? search24 (make_St_load Mint8unsigned 20 19 search23)); |
---|
110 | (pair ?? search23 (make_St_op2 (Ocmpu Cgt) 18 19 2 search22)); |
---|
111 | (pair ?? search22 (make_St_cond 18 search21 search17)); |
---|
112 | (pair ?? search21 (make_St_cost C_cost2 search20)); |
---|
113 | (pair ?? search20 (make_St_const 17 (Ointconst I8 (repr ? 1)) search19)); |
---|
114 | (pair ?? search2 (make_St_op1 Onegint 7 8 search1)); |
---|
115 | (pair ?? search19 (make_St_op2 Osub 16 4 17 search18)); |
---|
116 | (pair ?? search18 (make_St_op1 (Ocastint Unsigned I8) 3 16 search16)); |
---|
117 | (pair ?? search17 (make_St_cost C_cost3 search16)); |
---|
118 | (pair ?? search16 (make_St_const 15 (Ointconst I8 (repr ? 1)) search15)); |
---|
119 | (pair ?? search15 (make_St_op2 Omul 14 4 15 search14)); |
---|
120 | (pair ?? search14 (make_St_op2 Oaddp 13 0 14 search13)); |
---|
121 | (pair ?? search13 (make_St_load Mint8unsigned 13 12 search12)); |
---|
122 | (pair ?? search12 (make_St_op2 (Ocmpu Clt) 11 12 2 search11)); |
---|
123 | (pair ?? search11 (make_St_cond 11 search10 search6)); |
---|
124 | (pair ?? search10 (make_St_cost C_cost0 search9)); |
---|
125 | (pair ?? search1 (make_St_op1 (Ocastint Signed I8) 6 7 search0)); |
---|
126 | (pair ?? search0 (make_St_return)) |
---|
127 | ] |
---|
128 | |
---|
129 | search50 |
---|
130 | search0. |
---|
131 | |
---|
132 | definition id_main := ident_of_nat 1. |
---|
133 | definition main9 := 61. |
---|
134 | definition main8 := 60. |
---|
135 | definition main7 := 59. |
---|
136 | definition main61 := 58. |
---|
137 | definition main60 := 57. |
---|
138 | definition main6 := 56. |
---|
139 | definition main59 := 55. |
---|
140 | definition main58 := 54. |
---|
141 | definition main57 := 53. |
---|
142 | definition main56 := 52. |
---|
143 | definition main55 := 51. |
---|
144 | definition main54 := 50. |
---|
145 | definition main53 := 49. |
---|
146 | definition main52 := 48. |
---|
147 | definition main51 := 47. |
---|
148 | definition main50 := 46. |
---|
149 | definition main5 := 45. |
---|
150 | definition main49 := 44. |
---|
151 | definition main48 := 43. |
---|
152 | definition main47 := 42. |
---|
153 | definition main46 := 41. |
---|
154 | definition main45 := 40. |
---|
155 | definition main44 := 39. |
---|
156 | definition main43 := 38. |
---|
157 | definition main42 := 37. |
---|
158 | definition main41 := 36. |
---|
159 | definition main40 := 35. |
---|
160 | definition main4 := 34. |
---|
161 | definition main39 := 33. |
---|
162 | definition main38 := 32. |
---|
163 | definition main37 := 31. |
---|
164 | definition main36 := 30. |
---|
165 | definition main35 := 29. |
---|
166 | definition main34 := 28. |
---|
167 | definition main33 := 27. |
---|
168 | definition main32 := 26. |
---|
169 | definition main31 := 25. |
---|
170 | definition main30 := 24. |
---|
171 | definition main3 := 23. |
---|
172 | definition main29 := 22. |
---|
173 | definition main28 := 21. |
---|
174 | definition main27 := 20. |
---|
175 | definition main26 := 19. |
---|
176 | definition main25 := 18. |
---|
177 | definition main24 := 17. |
---|
178 | definition main23 := 16. |
---|
179 | definition main22 := 15. |
---|
180 | definition main21 := 14. |
---|
181 | definition main20 := 13. |
---|
182 | definition main2 := 12. |
---|
183 | definition main19 := 11. |
---|
184 | definition main18 := 10. |
---|
185 | definition main17 := 9. |
---|
186 | definition main16 := 8. |
---|
187 | definition main15 := 7. |
---|
188 | definition main14 := 6. |
---|
189 | definition main13 := 5. |
---|
190 | definition main12 := 4. |
---|
191 | definition main11 := 3. |
---|
192 | definition main10 := 2. |
---|
193 | definition main1 := 1. |
---|
194 | definition main0 := 0. |
---|
195 | definition C_cost9 := costlabel_of_nat 0. |
---|
196 | |
---|
197 | |
---|
198 | definition pre_main := mk_pre_internal_function |
---|
199 | (Some ? (pair ?? 2 (ASTint I32 Signed))) |
---|
200 | [] |
---|
201 | [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I8 Signed)); (pair ?? 15 (ASTint I8 Signed)); (pair ?? 16 (ASTint I8 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I8 Signed)); (pair ?? 24 (ASTint I8 Signed)); (pair ?? 25 (ASTint I8 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I8 Signed)); (pair ?? 33 (ASTint I8 Signed)); (pair ?? 34 (ASTint I8 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I8 Signed)); (pair ?? 42 (ASTint I8 Signed)); (pair ?? 43 (ASTint I8 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I8 Signed)); (pair ?? 51 (ASTint I8 Signed)); (pair ?? 52 (ASTint I8 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))] |
---|
202 | 5 |
---|
203 | [ |
---|
204 | (pair ?? main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) main8)); |
---|
205 | (pair ?? main8 (make_St_op2 Oaddp 3 8 9 main7)); |
---|
206 | (pair ?? main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) main6)); |
---|
207 | (pair ?? main61 (make_St_cost C_cost9 main60)); |
---|
208 | (pair ?? main60 (make_St_const 53 (Oaddrstack 0) main59)); |
---|
209 | (pair ?? main6 (make_St_op1 (Ocastint Signed I8) 4 7 main5)); |
---|
210 | (pair ?? main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) main58)); |
---|
211 | (pair ?? main58 (make_St_op2 Oaddp 49 53 54 main57)); |
---|
212 | (pair ?? main57 (make_St_const 51 (Ointconst I8 (repr ? 0)) main56)); |
---|
213 | (pair ?? main56 (make_St_const 52 (Ointconst I8 (repr ? 1)) main55)); |
---|
214 | (pair ?? main55 (make_St_op2 Omul 50 51 52 main54)); |
---|
215 | (pair ?? main54 (make_St_op2 Oaddp 46 49 50 main53)); |
---|
216 | (pair ?? main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) main52)); |
---|
217 | (pair ?? main52 (make_St_op1 (Ocastint Signed I8) 47 48 main51)); |
---|
218 | (pair ?? main51 (make_St_store Mint8unsigned 46 47 main50)); |
---|
219 | (pair ?? main50 (make_St_const 44 (Oaddrstack 0) main49)); |
---|
220 | (pair ?? main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) main4)); |
---|
221 | (pair ?? main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) main48)); |
---|
222 | (pair ?? main48 (make_St_op2 Oaddp 40 44 45 main47)); |
---|
223 | (pair ?? main47 (make_St_const 42 (Ointconst I8 (repr ? 1)) main46)); |
---|
224 | (pair ?? main46 (make_St_const 43 (Ointconst I8 (repr ? 1)) main45)); |
---|
225 | (pair ?? main45 (make_St_op2 Omul 41 42 43 main44)); |
---|
226 | (pair ?? main44 (make_St_op2 Oaddp 37 40 41 main43)); |
---|
227 | (pair ?? main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) main42)); |
---|
228 | (pair ?? main42 (make_St_op1 (Ocastint Signed I8) 38 39 main41)); |
---|
229 | (pair ?? main41 (make_St_store Mint8unsigned 37 38 main40)); |
---|
230 | (pair ?? main40 (make_St_const 35 (Oaddrstack 0) main39)); |
---|
231 | (pair ?? main4 (make_St_op1 (Ocastint Signed I8) 5 6 main3)); |
---|
232 | (pair ?? main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) main38)); |
---|
233 | (pair ?? main38 (make_St_op2 Oaddp 31 35 36 main37)); |
---|
234 | (pair ?? main37 (make_St_const 33 (Ointconst I8 (repr ? 2)) main36)); |
---|
235 | (pair ?? main36 (make_St_const 34 (Ointconst I8 (repr ? 1)) main35)); |
---|
236 | (pair ?? main35 (make_St_op2 Omul 32 33 34 main34)); |
---|
237 | (pair ?? main34 (make_St_op2 Oaddp 28 31 32 main33)); |
---|
238 | (pair ?? main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) main32)); |
---|
239 | (pair ?? main32 (make_St_op1 (Ocastint Signed I8) 29 30 main31)); |
---|
240 | (pair ?? main31 (make_St_store Mint8unsigned 28 29 main30)); |
---|
241 | (pair ?? main30 (make_St_const 26 (Oaddrstack 0) main29)); |
---|
242 | (pair ?? main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) main2)); |
---|
243 | (pair ?? main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) main28)); |
---|
244 | (pair ?? main28 (make_St_op2 Oaddp 22 26 27 main27)); |
---|
245 | (pair ?? main27 (make_St_const 24 (Ointconst I8 (repr ? 3)) main26)); |
---|
246 | (pair ?? main26 (make_St_const 25 (Ointconst I8 (repr ? 1)) main25)); |
---|
247 | (pair ?? main25 (make_St_op2 Omul 23 24 25 main24)); |
---|
248 | (pair ?? main24 (make_St_op2 Oaddp 19 22 23 main23)); |
---|
249 | (pair ?? main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) main22)); |
---|
250 | (pair ?? main22 (make_St_op1 (Ocastint Signed I8) 20 21 main21)); |
---|
251 | (pair ?? main21 (make_St_store Mint8unsigned 19 20 main20)); |
---|
252 | (pair ?? main20 (make_St_const 17 (Oaddrstack 0) main19)); |
---|
253 | (pair ?? main2 (make_St_op1 Oid 0 1 main1)); |
---|
254 | (pair ?? main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) main18)); |
---|
255 | (pair ?? main18 (make_St_op2 Oaddp 13 17 18 main17)); |
---|
256 | (pair ?? main17 (make_St_const 15 (Ointconst I8 (repr ? 4)) main16)); |
---|
257 | (pair ?? main16 (make_St_const 16 (Ointconst I8 (repr ? 1)) main15)); |
---|
258 | (pair ?? main15 (make_St_op2 Omul 14 15 16 main14)); |
---|
259 | (pair ?? main14 (make_St_op2 Oaddp 10 13 14 main13)); |
---|
260 | (pair ?? main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) main12)); |
---|
261 | (pair ?? main12 (make_St_op1 (Ocastint Signed I8) 11 12 main11)); |
---|
262 | (pair ?? main11 (make_St_store Mint8unsigned 10 11 main10)); |
---|
263 | (pair ?? main10 (make_St_const 8 (Oaddrstack 0) main9)); |
---|
264 | (pair ?? main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 main0)); |
---|
265 | (pair ?? main0 (make_St_return)) |
---|
266 | ] |
---|
267 | |
---|
268 | main61 |
---|
269 | main0. |
---|
270 | |
---|
271 | |
---|
272 | |
---|
273 | definition prog : res RTLabs_program := |
---|
274 | do f_main \larr make_internal_function pre_main; |
---|
275 | do f_search \larr make_internal_function pre_search; |
---|
276 | |
---|
277 | OK ? (mk_program ?? |
---|
278 | ( (pair ?? id_main f_main):: |
---|
279 | (pair ?? id_search f_search):: |
---|
280 | (nil ?)) |
---|
281 | id_main |
---|
282 | (*globals:*) |
---|
283 | [] |
---|
284 | ). |
---|
285 | |
---|
286 | example exec: finishes_with (repr I32 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r). |
---|
287 | normalize (* you can examine the result here *) |
---|
288 | @refl qed. |
---|
289 | |
---|