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

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

Common definition for animation semantics, and factor out IO definitions.

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