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

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

Refine "AST" types to include size/signedness information.

File size: 3.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 := 30.
10  definition main8 := 29.
11  definition main7 := 28.
12  definition main6 := 27.
13  definition main5 := 26.
14  definition main4 := 25.
15  definition main30 := 24.
16  definition main3 := 23.
17  definition main29 := 22.
18  definition main28 := 21.
19  definition main27 := 20.
20  definition main26 := 19.
21  definition main25 := 18.
22  definition main24 := 17.
23  definition main23 := 16.
24  definition main22 := 15.
25  definition main21 := 14.
26  definition main20 := 13.
27  definition main2 := 12.
28  definition main19 := 11.
29  definition main18 := 10.
30  definition main17 := 9.
31  definition main16 := 8.
32  definition main15 := 7.
33  definition main14 := 6.
34  definition main13 := 5.
35  definition main12 := 4.
36  definition main11 := 3.
37  definition main10 := 2.
38  definition main1 := 1.
39  definition main0 := 0.
40  definition C_cost2 := costlabel_of_nat 2.
41  definition C_cost1 := costlabel_of_nat 1.
42  definition C_cost0 := costlabel_of_nat 0.
43
44
45  definition pre_main := mk_pre_internal_function
46    (mk_signature [] (Some ? (ASTint I32 Signed)))
47    (Some ? 3)
48    []
49    [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18]
50    [8; 9]
51    0
52    [
53    (pair ?? main9 (make_St_op2 Oaddp 8 9 10 main8));
54    (pair ?? main8 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[8]] 7 main7));
55    (pair ?? main7 (make_St_op1 Ocast8unsigned 6 7 main6));
56    (pair ?? main6 (make_St_op2 Oadd 1 5 6 main5));
57    (pair ?? main5 (make_St_const 4 (Ointconst (repr 1)) main4));
58    (pair ?? main4 (make_St_op2 Oadd 2 2 4 main3));
59    (pair ?? main30 (make_St_const 18 (Ointconst (repr 28)) main29));
60    (pair ?? main3 (make_St_skip main17));
61    (pair ?? main29 (make_St_store Mint8unsigned (Aglobal id_src (repr 0)) [[]] 18 main28));
62    (pair ?? main28 (make_St_const 17 (Ointconst (repr 17)) main27));
63    (pair ?? main27 (make_St_store Mint8unsigned (Aglobal id_src (repr 1)) [[]] 17 main26));
64    (pair ?? main26 (make_St_const 16 (Ointconst (repr 17)) main25));
65    (pair ?? main25 (make_St_store Mint8unsigned (Aglobal id_src (repr 2)) [[]] 16 main24));
66    (pair ?? main24 (make_St_const 15 (Ointconst (repr 8)) main23));
67    (pair ?? main23 (make_St_store Mint8unsigned (Aglobal id_src (repr 3)) [[]] 15 main22));
68    (pair ?? main22 (make_St_const 14 (Ointconst (repr 4)) main21));
69    (pair ?? main21 (make_St_store Mint8unsigned (Aglobal id_src (repr 4)) [[]] 14 main20));
70    (pair ?? main20 (make_St_cost C_cost2 main19));
71    (pair ?? main2 (make_St_cost C_cost1 main1));
72    (pair ?? main19 (make_St_const 1 (Ointconst (repr 0)) main18));
73    (pair ?? main18 (make_St_const 2 (Ointconst (repr 0)) main3));
74    (pair ?? main17 (make_St_const 13 (Ointconst (repr 5)) main16));
75    (pair ?? main16 (make_St_op2 (Ocmpu Clt) 12 2 13 main15));
76    (pair ?? main15 (make_St_cond1 Onotbool 12 main2 main14));
77    (pair ?? main14 (make_St_cost C_cost0 main13));
78    (pair ?? main13 (make_St_op1 Ocast8unsigned 5 1 main12));
79    (pair ?? main12 (make_St_const 9 (Oaddrsymbol id_src (repr 0)) main11));
80    (pair ?? main11 (make_St_const 11 (Ointconst (repr 1)) main10));
81    (pair ?? main10 (make_St_op2 Omul 10 2 11 main9));
82    (pair ?? main1 (make_St_op1 Ocast8unsigned 3 1 main0));
83    (pair ?? main0 (make_St_return))
84]
85
86    main30
87    main0.
88
89
90
91definition prog : res RTLabs_program :=
92  do f_main \larr make_internal_function pre_main;
93
94OK ? (mk_program ??
95(  (pair ?? id_main f_main)::
96(nil ?))
97  id_main
98  (*globals:*)
99  [pair ?? (pair ?? (pair ?? id_src [Init_space 8 ]) Any) it]
100).
101
102example exec: finishes_with (repr 74) ? (do myprog ← prog; exec_up_to RTLabs_fullexec myprog 1000 [ ]).
103normalize  (* you can examine the result here *)
104@refl
105qed.
106
Note: See TracBrowser for help on using the repository browser.