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