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