1(*
2use "prelim";
3*)
4
5(*---------------------------------------------------------------------------*)
6(* This example demonstrates how the compiler works step by step.            *)
7(* It is the one given in the CADE-21 paper.                                 *)
8(*---------------------------------------------------------------------------*)
9
10(*---------------------------------------------------------------------------*)
11(* Source programs.                                                          *)
12(*---------------------------------------------------------------------------*)
13
14val fact_def = Define
15   `fact i = if i = 0 then 1 else i * fact (i - 1)`;
16
17val f1_def = Define
18   `f1 (k0,k1,k2)  =
19        let y = k2 + 100 in
20        let g = (\(x,y). y - (x * k0)) in
21        let z = if fact 3 < 10 /\ y + 2 * k1 > k0 then g (k1, k2)
22                else y
23        in
24        z * y`;
25
26(*****************************************************************************)
27(* Front End                                                                 *)
28(*****************************************************************************)
29
30(*---------------------------------------------------------------------------*)
31(* Normalization and optimization of the normal forms.                       *)
32(*---------------------------------------------------------------------------*)
33
34val lem1 = SSA_RULE (SIMP_RULE std_ss [Once LET_THM] (normalize fact_def));
35
36(*
37 |- fact =
38       (\v1.
39          (if v1 = 0 then
40             1
41           else
42             (let v2 = v1 - 1 in
43              let v3 = fact v2 in
44              let v4 = v1 * v3 in
45                v4)))
46*)
47
48val lem2 = SSA_RULE (normalize f1_def);
49
50(*
51|- f1 =
52       (\(v1,v2,v3).
53          (let v4 = v3 + 100 in
54           let v5 (v13,v14) =
55                 (let v15 = v1 * v13 in let v16 = v14 - v15 in v16)
56           in
57           let v6 = fact 3 in
58           let v7 =
59                 (if 10 <= v6 then
60                    v4
61                  else
62                    (let v9 = 2 * v2 in
63                     let v10 = v9 + v4 in
64                     let v11 =
65                           (if v10 <= v1 then
66                              v4
67                            else
68                              (let v12 = v5 (v2,v3) in v12))
69                     in
70                       v11))
71           in
72           let v8 = v4 * v7 in
73             v8))
74*)
75
76val env = [lem1];
77val th1 = SSA_RULE (optimize_norm env lem2);
78(*
79 |- f1 =
80       (\(v1,v2,v3).
81          (let v4 = v3 + 100 in
82           let v5 (v11,v12) =
83                 (let v13 = v1 * v11 in let v14 = v12 - v13 in v14)
84           in
85           let v6 = 2 * v2 in
86           let v7 = v4 + v6 in
87           let v8 = (if v7 <= v1 then v4 else (let v10 = v5 (v2,v3) in v10))
88           in
89           let v9 = v4 * v8 in
90             v9))
91
92*)
93
94(*---------------------------------------------------------------------------*)
95(* Closure Conversion and subsequent optimization                            *)
96(*---------------------------------------------------------------------------*)
97
98val th2 = closure_convert th1;
99(*
100 |- f1 =
101       (\(v1,v2,v3).
102          (let v4 =
103                 fun
104                   (\v11 (v12,v13).
105                      (let v14 = v11 * v12 in let v15 = v13 - v14 in v15))
106           in
107           let v5 = v3 + 100 in
108           let v6 = 2 * v2 in
109           let v7 = v5 + v6 in
110           let v8 =
111                 (if v7 <= v1 then v5 else (let v10 = v4 v1 (v2,v3) in v10))
112           in
113           let v9 = v5 * v8 in
114             v9))
115*)
116
117val th3 = SSA_RULE (optimize_norm []
118                     (SIMP_RULE std_ss [Once LET_THM, NormalTheory.fun_def] th2));
119
120(*
121 |- f1 =
122       (\(v1,v2,v3).
123          (let v4 = v3 + 100 in
124           let v5 = 2 * v2 in
125           let v6 = v4 + v5 in
126           let v7 =
127                 (if v6 <= v1 then
128                    v4
129                  else
130                    (let v9 = v1 * v2 in let v10 = v3 - v9 in v10))
131           in
132           let v8 = v4 * v7 in
133             v8))
134*)
135
136(*---------------------------------------------------------------------------*)
137(* Register Allocation                                                       *)
138(*---------------------------------------------------------------------------*)
139
140regAlloc.numRegs := 3;             (* this causes the spilling to occur *)
141val th4 = reg_alloc th3;
142
143(*
144    |- f1 =
145       (\(r0,r1,r2).
146          (let m1 = r0 in
147           let r0 = r2 + 100 in
148           let m2 = r0 in
149           let r0 = 2 * r1 in
150           let m3 = r1 in
151           let r1 = m2 in
152           let r0 = r1 + r0 in
153           let r1 = m1 in
154           let r0 =
155                 (if r0 <= r1 then
156                    (let r0 = m2 in r0)
157                  else
158                    (let r0 = m3 in
159                     let r0 = r1 * r0 in
160                     let r0 = r2 - r0 in
161                       r0))
162           in
163           let r1 = m2 in
164           let r0 = r1 * r0 in
165             r0)) : thm
166*)
167
168regAlloc.numRegs := 5;        (* no spilling is needed *)
169val th5 = reg_alloc th3;
170
171(*
172  |- f1 =
173       (\(r0,r1,r2).
174          (let r3 = r2 + 100 in
175           let r4 = 2 * r1 in
176           let r4 = r3 + r4 in
177           let r0 =
178                 (if r4 <= r0 then
179                    r3
180                  else
181                    (let r0 = r0 * r1 in let r0 = r2 - r0 in r0))
182           in
183           let r0 = r3 * r0 in
184             r0)) : thm
185*)
186
187(*****************************************************************************)
188(* Front End                                                                 *)
189(*****************************************************************************)
190
191(*---------------------------------------------------------------------------*)
192(* Generating code in Structured Assembly Language (SAL)                     *)
193(*---------------------------------------------------------------------------*)
194
195(* First try the one without spilling *)
196
197val sal_1 = certified_gen th5;
198printSAL (#code sal_1);
199
200(*
201 val sal_1 =
202    {code = ... (see below )
203     thm =
204       |- Reduce
205            (L 1,
206             ASG (L 1) r3 (r2 + 100) (L 3) |++|
207             (ASG (L 3) r4 (2 * r1) (L 4) |++|
208              (ASG (L 4) r4 (r3 + r4) (L 5) |++|
209               (IFGOTO (L 5) (\r0. r4 <= r0) (L 7) (L 8) |++|
210                ASG (L 7) r0 r3 (L 6) |++|
211                (ASG (L 8) r0 (r0 * r1) (L 9) |++|
212                 ASG (L 9) r0 (r2 - r0) (L 6)) |++|
213                ASG (L 6) r0 (r3 * r0) (L 2)))),L 2)
214            ((let r3 = r2 + 100 in
215              let r4 = 2 * r1 in
216              let r4 = r3 + r4 in
217              let r0 = (if r4 <= r0 then r3 else (let r0 = r0 * r1 in r2 - r0))
218              in
219                r3 * r0),r0)} : {code : term, thm : thm}
220
221    l1:   r3 := r2 + 100  (goto l3)
222    l3:   r4 := 2 * r1  (goto l4)
223    l4:   r4 := r3 + r4  (goto l5)
224    l5:   ifgoto r4 <= r0 l7 l8
225    l7:   r0 := r3  (goto l6)
226    l8:   r0 := r0 * r1  (goto l9)
227    l9:   r0 := r2 - r0  (goto l6)
228    l6:   r0 := r3 * r0  (goto l2)
229*)
230
231(*  Then try the spilling one *)
232
233val sal_2 = certified_gen th4;
234printSAL (#code sal_2);
235
236(*
237> val sal_2 =
238    {code = ...
239     thm =
240       |- Reduce
241            (L 1,
242             ASG (L 1) m1 r0 (L 3) |++|
243             (ASG (L 3) r0 (r2 + 100) (L 4) |++|
244              (ASG (L 4) m2 r0 (L 5) |++|
245               (ASG (L 5) r0 (2 * r1) (L 6) |++|
246                (ASG (L 6) m3 r1 (L 7) |++|
247                 (ASG (L 7) r1 m2 (L 8) |++|
248                  (ASG (L 8) r0 (r1 + r0) (L 9) |++|
249                   (ASG (L 9) r1 m1 (L 10) |++|
250                    (IFGOTO (L 10) (\r1. r0 <= r1) (L 12) (L 13) |++|
251                     ASG (L 12) r0 m2 (L 11) |++|
252                     (ASG (L 13) r0 m3 (L 15) |++|
253                      (ASG (L 15) r0 (r1 * r0) (L 16) |++|
254                       ASG (L 16) r0 (r2 - r0) (L 11))) |++|
255                     (ASG (L 11) r1 m2 (L 18) |++|
256                      ASG (L 18) r0 (r1 * r0) (L 2)))))))))),L 2)
257            ((let m1 = r0 in
258              let r0 = r2 + 100 in
259              let m2 = r0 in
260              let r0 = 2 * r1 in
261              let m3 = r1 in
262              let r1 = m2 in
263              let r0 = r1 + r0 in
264              let r1 = m1 in
265              let r0 =
266                    (if r0 <= r1 then
267                       m2
268                     else
269                       (let r0 = m3 in let r0 = r1 * r0 in r2 - r0))
270              in
271              let r1 = m2 in
272                r1 * r0),r0)} : {code : term, thm : thm}
273
274    l1:   m1 := r0  (goto l3)
275    l3:   r0 := r2 + 100  (goto l4)
276    l4:   m2 := r0  (goto l5)
277    l5:   r0 := 2 * r1  (goto l6)
278    l6:   m3 := r1  (goto l7)
279    l7:   r1 := m2  (goto l8)
280    l8:   r0 := r1 + r0  (goto l9)
281    l9:   r1 := m1  (goto l10)
282    l10:  ifgoto r0 <= r1 l12 l13
283    l12:  r0 := m2  (goto l11)
284    l13:  r0 := m3  (goto l15)
285    l15:  r0 := r1 * r0  (goto l16)
286    l16:  r0 := r2 - r0  (goto l11)
287    l11:  r1 := m2  (goto l18)
288    l18:  r0 := r1 * r0  (goto l2)
289
290*)
291