source: src/RTLabs/test/sum.RTLabs.ma @ 1157

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

Update RTLabs pretty printer and examples.

File size: 7.7 KB
Line 
1include "RTLabs/import.ma".
2include "common/Animation.ma".
3
4definition id_src := ident_of_nat 1.
5
6
7
8  definition id_main := ident_of_nat 0.
9  definition main9 := 59.
10  definition main8 := 58.
11  definition main7 := 57.
12  definition main6 := 56.
13  definition main59 := 55.
14  definition main58 := 54.
15  definition main57 := 53.
16  definition main56 := 52.
17  definition main55 := 51.
18  definition main54 := 50.
19  definition main53 := 49.
20  definition main52 := 48.
21  definition main51 := 47.
22  definition main50 := 46.
23  definition main5 := 45.
24  definition main49 := 44.
25  definition main48 := 43.
26  definition main47 := 42.
27  definition main46 := 41.
28  definition main45 := 40.
29  definition main44 := 39.
30  definition main43 := 38.
31  definition main42 := 37.
32  definition main41 := 36.
33  definition main40 := 35.
34  definition main4 := 34.
35  definition main39 := 33.
36  definition main38 := 32.
37  definition main37 := 31.
38  definition main36 := 30.
39  definition main35 := 29.
40  definition main34 := 28.
41  definition main33 := 27.
42  definition main32 := 26.
43  definition main31 := 25.
44  definition main30 := 24.
45  definition main3 := 23.
46  definition main29 := 22.
47  definition main28 := 21.
48  definition main27 := 20.
49  definition main26 := 19.
50  definition main25 := 18.
51  definition main24 := 17.
52  definition main23 := 16.
53  definition main22 := 15.
54  definition main21 := 14.
55  definition main20 := 13.
56  definition main2 := 12.
57  definition main19 := 11.
58  definition main18 := 10.
59  definition main17 := 9.
60  definition main16 := 8.
61  definition main15 := 7.
62  definition main14 := 6.
63  definition main13 := 5.
64  definition main12 := 4.
65  definition main11 := 3.
66  definition main10 := 2.
67  definition main1 := 1.
68  definition main0 := 0.
69  definition C_cost2 := costlabel_of_nat 2.
70  definition C_cost1 := costlabel_of_nat 1.
71  definition C_cost0 := costlabel_of_nat 0.
72
73
74  definition pre_main := mk_pre_internal_function
75    (Some ? (pair ?? 2 (ASTint I32 Signed)))
76    []
77    [(pair ?? 0 (ASTint I32 Signed)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTptr Any)); (pair ?? 7 (ASTptr Any)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Unsigned)); (pair ?? 11 (ASTint I32 Unsigned)); (pair ?? 12 (ASTint I32 Unsigned)); (pair ?? 13 (ASTint I32 Unsigned)); (pair ?? 14 (ASTint I8 Unsigned)); (pair ?? 15 (ASTint I8 Signed)); (pair ?? 16 (ASTint I8 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I8 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I32 Unsigned)); (pair ?? 21 (ASTint I32 Unsigned)); (pair ?? 22 (ASTint I32 Unsigned)); (pair ?? 23 (ASTptr Any)); (pair ?? 24 (ASTint I8 Unsigned)); (pair ?? 25 (ASTptr Any)); (pair ?? 26 (ASTint I32 Unsigned)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTint I32 Unsigned)); (pair ?? 29 (ASTptr Any)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I32 Unsigned)); (pair ?? 33 (ASTint I32 Unsigned)); (pair ?? 34 (ASTint I32 Unsigned)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I8 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I32 Unsigned)); (pair ?? 39 (ASTint I32 Unsigned)); (pair ?? 40 (ASTint I32 Unsigned)); (pair ?? 41 (ASTptr Any)); (pair ?? 42 (ASTint I8 Unsigned)); (pair ?? 43 (ASTptr Any)); (pair ?? 44 (ASTint I32 Unsigned)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTint I32 Unsigned))]
78    0
79    [
80    (pair ?? main9 (make_St_op2 Oaddp 6 7 8 main8));
81    (pair ?? main8 (make_St_load Mint8unsigned 6 5 main7));
82    (pair ?? main7 (make_St_op2 Oadd 4 1 5 main6));
83    (pair ?? main6 (make_St_op1 (Ocastint Unsigned I8) 1 4 main5));
84    (pair ?? main59 (make_St_const 43 (Oaddrsymbol id_src 0) main58));
85    (pair ?? main58 (make_St_const 45 (Ointconst I32 (repr ? 0)) main57));
86    (pair ?? main57 (make_St_const 46 (Ointconst I32 (repr ? 0)) main56));
87    (pair ?? main56 (make_St_op2 Oadd 44 45 46 main55));
88    (pair ?? main55 (make_St_op2 Oaddp 41 43 44 main54));
89    (pair ?? main54 (make_St_const 42 (Ointconst I8 (repr ? 28)) main53));
90    (pair ?? main53 (make_St_store Mint8unsigned 41 42 main52));
91    (pair ?? main52 (make_St_const 37 (Oaddrsymbol id_src 0) main51));
92    (pair ?? main51 (make_St_const 39 (Ointconst I32 (repr ? 0)) main50));
93    (pair ?? main50 (make_St_const 40 (Ointconst I32 (repr ? 1)) main49));
94    (pair ?? main5 (make_St_const 3 (Ointconst I32 (repr ? 1)) main4));
95    (pair ?? main49 (make_St_op2 Oadd 38 39 40 main48));
96    (pair ?? main48 (make_St_op2 Oaddp 35 37 38 main47));
97    (pair ?? main47 (make_St_const 36 (Ointconst I8 (repr ? 17)) main46));
98    (pair ?? main46 (make_St_store Mint8unsigned 35 36 main45));
99    (pair ?? main45 (make_St_const 31 (Oaddrsymbol id_src 0) main44));
100    (pair ?? main44 (make_St_const 33 (Ointconst I32 (repr ? 0)) main43));
101    (pair ?? main43 (make_St_const 34 (Ointconst I32 (repr ? 2)) main42));
102    (pair ?? main42 (make_St_op2 Oadd 32 33 34 main41));
103    (pair ?? main41 (make_St_op2 Oaddp 29 31 32 main40));
104    (pair ?? main40 (make_St_const 30 (Ointconst I8 (repr ? 17)) main39));
105    (pair ?? main4 (make_St_op2 Oadd 0 0 3 main3));
106    (pair ?? main39 (make_St_store Mint8unsigned 29 30 main38));
107    (pair ?? main38 (make_St_const 25 (Oaddrsymbol id_src 0) main37));
108    (pair ?? main37 (make_St_const 27 (Ointconst I32 (repr ? 0)) main36));
109    (pair ?? main36 (make_St_const 28 (Ointconst I32 (repr ? 3)) main35));
110    (pair ?? main35 (make_St_op2 Oadd 26 27 28 main34));
111    (pair ?? main34 (make_St_op2 Oaddp 23 25 26 main33));
112    (pair ?? main33 (make_St_const 24 (Ointconst I8 (repr ? 8)) main32));
113    (pair ?? main32 (make_St_store Mint8unsigned 23 24 main31));
114    (pair ?? main31 (make_St_const 19 (Oaddrsymbol id_src 0) main30));
115    (pair ?? main30 (make_St_const 21 (Ointconst I32 (repr ? 0)) main29));
116    (pair ?? main3 (make_St_skip main19));
117    (pair ?? main29 (make_St_const 22 (Ointconst I32 (repr ? 4)) main28));
118    (pair ?? main28 (make_St_op2 Oadd 20 21 22 main27));
119    (pair ?? main27 (make_St_op2 Oaddp 17 19 20 main26));
120    (pair ?? main26 (make_St_const 18 (Ointconst I8 (repr ? 4)) main25));
121    (pair ?? main25 (make_St_store Mint8unsigned 17 18 main24));
122    (pair ?? main24 (make_St_cost C_cost2 main23));
123    (pair ?? main23 (make_St_const 16 (Ointconst I8 (repr ? 0)) main22));
124    (pair ?? main22 (make_St_op1 (Ocastint Signed I8) 1 16 main21));
125    (pair ?? main21 (make_St_const 15 (Ointconst I8 (repr ? 0)) main20));
126    (pair ?? main20 (make_St_op1 (Ocastint Signed I32) 0 15 main3));
127    (pair ?? main2 (make_St_cost C_cost1 main1));
128    (pair ?? main19 (make_St_op1 (Ocastint Signed I32) 12 0 main18));
129    (pair ?? main18 (make_St_const 14 (Ointconst I8 (repr ? 5)) main17));
130    (pair ?? main17 (make_St_op1 (Ocastint Unsigned I32) 13 14 main16));
131    (pair ?? main16 (make_St_op2 (Ocmpu Clt) 11 12 13 main15));
132    (pair ?? main15 (make_St_op1 Onotbool 10 11 main14));
133    (pair ?? main14 (make_St_cond 10 main2 main13));
134    (pair ?? main13 (make_St_cost C_cost0 main12));
135    (pair ?? main12 (make_St_const 7 (Oaddrsymbol id_src 0) main11));
136    (pair ?? main11 (make_St_const 9 (Ointconst I32 (repr ? 1)) main10));
137    (pair ?? main10 (make_St_op2 Omul 8 0 9 main9));
138    (pair ?? main1 (make_St_op1 (Ocastint Unsigned I32) 2 1 main0));
139    (pair ?? main0 (make_St_return))
140]
141
142    main59
143    main0.
144
145
146
147definition prog : res RTLabs_program :=
148  do f_main \larr make_internal_function pre_main;
149
150OK ? (mk_program ??
151(  (pair ?? id_main f_main)::
152(nil ?))
153  id_main
154  (*globals:*)
155  [pair ?? (pair ?? (pair ?? id_src [Init_space 5 ]) Any) it]
156).
157
158example exec: finishes_with (repr I32 74) ? (do myprog ← prog; exec_up_to RTLabs_fullexec myprog 1000 [ ]).
159normalize  (* you can examine the result here *)
160@refl
161qed.
162
Note: See TracBrowser for help on using the repository browser.