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