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

Last change on this file since 967 was 967, checked in by campbell, 9 years ago

Update RTLabs pretty printer and examples.

File size: 14.4 KB
Line 
1include "RTLabs/import.ma".
2include "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
273definition 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
277OK ? (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
Note: See TracBrowser for help on using the repository browser.