source: src/RTLabs/test/search.ma @ 2254

Last change on this file since 2254 was 879, checked in by campbell, 10 years ago

Refine "AST" types to include size/signedness information.
File size: 10.5 KB
Line 
1include "RTLabs/import.ma".
2include "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 I8 Signed; ASTint I8 Signed] (Some ? (ASTint I8 Signed)))
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))
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 I32 Signed)))
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) 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)
236]
237
238    main41
239    main0.
240
241
242
243definition 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
247OK ? (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.
Note: See TracBrowser for help on using the repository browser.