1use "prelim";
2
3(* --------------------------------------------------------------------------*)
4(*      Test the pre-processing and normalization                            *)
5(* --------------------------------------------------------------------------*)
6
7val f1_def = Define
8   `f1 (x,s,k0,k1) = (x + k0) * (x + s) * (x + k1)`;
9
10val f2_def =
11 Define
12   `f2 ((y,z),(k0,k1,k2,k3),sum)  =
13        let sum1 = sum + 100 in
14        let v1 = if y > z \/ y + 2 * k0 > z then y + f1 (z, sum1 * 4, k0, k1)
15          else z + f1 (y, sum1, k2 - y, k3)
16        in
17        v1 + sum1`;
18
19(*
20val th1 = normalize f2_def;
21
22 |- f2 ((y,z),(k0,k1,k2,k3),sum) =
23       (let sum1 = sum + 100 in
24        let x = 4 * sum1 in
25        let y1 = f1 (z,x,k0,k1) in
26        let x = y + y1 in
27        let z =
28              (if y <= z then
29                 (let x1 = 2 * k0 in
30                  let p = x1 + y in
31                  let z =
32                        (if p <= z then
33                           (let x = k2 - y in
34                            let y1 = f1 (y,sum1,x,k3) in
35                            let y = z + y1 in
36                              y)
37                         else
38                           x)
39                  in
40                    z)
41               else
42                 x)
43        in
44        let y = sum1 + z in
45          y)
46*)
47
48(*---------------------------------------------------------------------------*)
49(* Test the simplications on normal forms                                    *)
50(* The SSA form transformation                                               *)
51(*---------------------------------------------------------------------------*)
52
53(*
54val th2 = SSA_RULE th1;
55 |- f2 =
56       (\((v1,v2),(v3,v4,v5,v6),v7).
57          (let v8 = v7 + 100 in
58           let v9 = 4 * v8 in
59           let v10 = f1 (v2,v9,v3,v4) in
60           let v11 = v1 + v10 in
61           let v12 =
62                 (if v1 <= v2 then
63                    (let v14 = 2 * v3 in
64                     let v15 = v14 + v1 in
65                     let v16 =
66                           (if v15 <= v2 then
67                              (let v17 = v5 - v1 in
68                               let v18 = f1 (v1,v8,v17,v6) in
69                               let v19 = v2 + v18 in
70                                 v19)
71                            else
72                              v11)
73                     in
74                       v16)
75                  else
76                    v11)
77           in
78           let v13 = v8 + v12 in
79             v13))
80*)
81
82(*---------------------------------------------------------------------------*)
83(* Optimization on Normal Forms:                                             *)
84(*   1. SSA forms                                                            *)
85(*   2. Inline expansion                                                     *)
86(*   3. Simplification of let-expressions (atom_let, flatten_let, useless_let*)
87(*   4. Constant folding                                                     *)
88(*   5. Beta-reduction (a special case of constant folding)                  *)
89(*---------------------------------------------------------------------------*)
90
91(* Inline expansion of anonymous functions                                   *)
92
93val f3_def = Define
94   `f3 (k0,k1,k2,k3)  =
95        let k4 = k0 + 100 in
96        let k5 = (\(x,y). let k6 = x + k1 in k2 * k6) in
97        let k7 = k5 (k3,k2) in
98        let k8 = k5 in
99        let k9 = k8 (k7,k4) in
100         k9`;
101
102(*
103- inline.expand_anonymous f3_def;
104> val it =
105    |- !k0 k1 k2 k3.
106         f3 (k0,k1,k2,k3) =
107         (let k4 = k0 + 100 in
108          let k7 = (let k6 = k3 + k1 in k2 * k6) in
109          let k9 = (let k6 = k7 + k1 in k2 * k6) in
110            k9) : thm
111*)
112
113(* Inline expansion of named functions stored in env                         *)
114
115val g1_def = Define `g1 (k0,k1) = let k2 = k0 + k1 in k2 * 15`;
116
117(* factorial function *)
118
119val g2_def = Define `
120    g2 k0 =
121    if k0 = 0 then 1 else
122      let k1 = k0 - 1 in
123      let k2 = g2 k1 in
124      k0 * k2`;
125
126val g3_def = Define `
127    g3 (k0,k1,k2) =
128       let k3 = g1 (k0, k1) in
129       let k4 = k2 * k0 in
130       let k5 = g2 2 in
131       k5 - k4`;
132
133val env = [g1_def, g2_def];
134
135(*
136- inline.expand_named env g3_def;
137> val it =
138    |- !k0 k1 k2.
139         g3 (k0,k1,k2) =
140         (let k3 = (let k2 = k0 + k1 in k2 * 15) in
141          let k4 = k2 * k0 in
142          let k5 =
143                (if 2 = 0 then
144                   1
145                 else
146                   (let k1 = 2 - 1 in
147                    let k2 =
148                          (if k1 = 0 then
149                             1
150                           else
151                             (let k11 = k1 - 1 in
152                              let k2 =
153                                    (if k11 = 0 then
154                                       1
155                                     else
156                                       (let k1 = k11 - 1 in
157                                        let k2 =
158                                              (if k1 = 0 then
159                                                 1
160                                               else
161                                                 (let k11 = k1 - 1 in
162                                                  let k2 = g2 k11 in
163                                                    k1 * k2))
164                                        in
165                                          k11 * k2))
166                              in
167                                k1 * k2))
168                    in
169                      2 * k2))
170          in
171            k5 - k4) : thm
172*)
173
174(* Optimization on Normal Forms, including inline expansion and
175   other optimizations *)
176
177(*
178- optimize_norm env g3_def;
179> val it =
180    |- g3 =
181       (\(v1,v2,v3).
182          (let k2 = v1 + v2 in
183           let v4 = 15 * k2 in
184           let v5 = v1 * v3 in
185             2 - v5)) : thm
186*)
187
188(*---------------------------------------------------------------------------*)
189(* Closure Conversion                                                        *)
190(*---------------------------------------------------------------------------*)
191
192val f4_def = Define `
193   f4 (k0,k1,k2,k3) =
194     let k5 = (\x. let k6 = x + k1 in k2 * k6) in
195     let k7 = k5 k3 in
196     k7`;
197
198(*
199- closure.close_one_by_one f4_def;
200> val it =
201    |- f4 =
202       (\(k0,k1,k2,k3).
203          (let k5 = fun (\k2 k1 x. (let k6 = x + k1 in k2 * k6)) in
204           let k7 = k5 k2 k1 k3 in
205             k7)) : thm
206*)
207
208val f5_def = Define
209   `f5 (k0,k1,k2,k3)  =
210        let k4 = k0 + 100 in
211        let k5 = (\x. let k6 = x + k1 in k2 * k6) in
212        let k7 = if k4 > k1 then
213           let k8 = (\(x,y). let k9 = x * k1 in y - k0) in k8 (k3,k4)
214           else k0 in
215        let k8 = k5 k7 in
216        k8`;
217(*
218- closure.close_all f5_def;
219  f5 =
220       (\(k0,k1,k2,k3).
221          (let k4 = k0 + 100 in
222           let k5 = fun (\(k1,k2) x. (let k6 = x + k1 in k2 * k6)) in
223           let k7 =
224                 (if k4 > k1 then
225                    (let k8 =
226                           fun (\(k1,k0) (x,y). (let k9 = x * k1 in y - k0))
227                     in
228                       k8 (k1,k0) (k3,k4))
229                  else
230                    k0)
231           in
232           let k8 = k5 (k1,k2) k7 in
233             k8))
234
235- closure.closure_convert f5_def;   (* there is a bug in top-leveling *)
236 |- f5 =
237       (\(v1,v2,v3,v4).
238          (let v5 = fun (\(v15,v16) v17. (let v18 = v17 + v15 in v16 * v18))
239           in
240           let v6 = v1 + 100 in
241           let v7 =
242                 fun
243                   (\(v10,v11) (v12,v13).
244                      (let v14 = v12 * v10 in v13 - v11))
245           in
246           let v8 = (if v6 > v2 then v7 (v2,v1) (v4,v6) else v1) in
247           let v9 = v5 (v2,v3) v8 in
248             v9)) : thm
249*)
250
251
252(*---------------------------------------------------------------------------*)
253(* Register Allocation                                                       *)
254(*---------------------------------------------------------------------------*)
255
256val f6_def = Define
257   `f6 =
258       \(k0,k1,k2,k3).
259        let k4 = k0 - 100 in
260        let k5 = k4 + k2 in
261        let k6 = if k4 > k1 then k0 * k3
262           else let k7 = k0 + k1 in k7 * 2 in
263        let k8 = k5 + k6 in
264        k8`;
265(*
266
267(* the case of insufficent registers that are available *)
268
269- regAlloc.regL;
270> val it = ref [``r0``, ``r1``, ``r2``, ``r3``]
271- regAlloc.reg_alloc f6_def;
272 |- f6 =
273       (\(r0,r1,r2,r3).
274          (let m1 = r1 in
275           let r1 = r0 - 100 in
276           let r2 = r1 + r2 in
277           let m2 = r2 in
278           let r2 = m1 in
279           let r0 =
280                 (if r1 > r2 then r0 * r3 else (let r0 = r0 + r2 in r0 * 2))
281           in
282           let r1 = m2 in
283           let r0 = r1 + r0 in
284             r0)) : thm
285
286
287(*  the case of enough registers that are available *)
288
289- regAlloc.regL := regAlloc.allregs;
290-  !regAlloc.regL;
291    [``r0``, ``r1``, ``r2``, ``r3``, ``r4``, ``r5``, ``r6``, ``r7``, ``r8``]
292
293- regAlloc.reg_alloc f6_def;
294 |- f6 =
295       (\(r0,r1,r2,r3).
296          (let r4 = r0 - 100 in
297           let r2 = r4 + r2 in
298           let r0 =
299                 (if r4 > r1 then r0 * r3 else (let r0 = r0 + r1 in r0 * 2))
300           in
301           let r0 = r2 + r0 in
302             r0)) : thm
303
304*)
305
306