e ::= c op(e 1,..., e n ) if e 1 then e 2 else e 3 let x = e 1 in e 2 x let rec x y 1... y n = e 1 in e 2 e e 1... e n (e 1,..., e n ) let (x 1,..., x

Size: px

Start display at page:

Download "e ::= c op(e 1,..., e n ) if e 1 then e 2 else e 3 let x = e 1 in e 2 x let rec x y 1... y n = e 1 in e 2 e e 1... e n (e 1,..., e n ) let (x 1,..., x"

ほのかふしはら
4 years ago
Views:

1 e ::= c op(e 1,..., e n ) if e 1 then e 2 else e 3 let x = e 1 in e 2 x let rec x y 1... y n = e 1 in e 2 e e 1... e n (e 1,..., e n ) let (x 1,..., x n ) = e 1 in e 2 Array.create e 1 e 2 e 1.(e 2 ) e 1.(e 2 ) e 3 1: MinCaml τ ::= π τ 1... τ n τ τ 1... τ n τ array α 2: MinCaml 1

2 c π Γ c : π Γ e 1 : π 1... Γ e n : π n op π 1,..., π n π Γ op(e 1,..., e n ) : π Γ e 1 : bool Γ e 2 : τ Γ e 3 : τ Γ if e 1 then e 2 else e 3 : τ Γ e 1 : τ 1 Γ, x : τ 1 e 2 : τ 2 Γ let x = e 1 in e 2 : τ 2 Γ(x) = τ Γ x : τ Γ, x : τ 1... τ n τ, y 1 : τ 1,..., y n : τ n e 1 : τ Γ, x : τ 1... τ n τ e 2 : τ Γ let rec x y 1... y n = e 1 in e 2 : τ Γ e : τ 1... τ n τ Γ e 1 : τ 1... Γ e n : τ n Γ e e 1... e n : τ Γ e 1 : τ 1... Γ e n : τ n Γ e 1 : τ 1... τ n Γ, x 1 : τ 1,..., x n : τ n e 2 : τ Γ (e 1,..., e n ) : τ 1... τ n Γ let (x 1,..., x n ) = e 1 in e 2 : τ Γ e 1 : int Γ e 2 : τ Γ Array.create e 1 e 2 : τ array Γ e 1 : τ array Γ e 1.(e 2 ) : τ Γ e 2 : int Γ e 1 : τ array Γ e 2 : int Γ e 3 : τ Γ e 1.(e 2 ) e 3 : unit 3: MinCaml e ::= c op(x 1,..., x n ) if x = y then e 1 else e 2 if x y then e 1 else e 2 let x = e 1 in e 2 x let rec x y 1... y n = e 1 in e 2 x y 1... y n (x 1,..., x n ) let (x 1,..., x n ) = y in e x.(y) x.(y) z 4: MinCaml K 2

3 K : Syntax.t KNormal.t K(c) = c K(not(e)) = K(if e then false else true) K(e 1 = e 2 ) = K(if e 1 = e 2 then true else false) K(e 1 e 2 ) = K(if e 1 e 2 then true else false) K(op(e 1,..., e n )) = let x 1 = K(e 1 ) in... let x n = K(e n ) in op(x 1,..., x n ) op K(if not e 1 then e 2 else e 3 ) = K(if e 1 then e 3 else e 2 ) K(if e 1 = e 2 then e 3 else e 4 ) = let x = K(e 1 ) in let y = K(e 2 ) in if x = y then K(e 3 ) else K(e 4 ) K(if e 1 e 2 then e 3 else e 4 ) = let x = K(e 1 ) in let y = K(e 2 ) in if x y then K(e 3 ) else K(e 4 ) K(if e 1 then e 2 else e 3 ) = K(if e 1 = false then e 3 else e 2 ) e 1 K(let x = e 1 in e 2 ) = let x = K(e 1 ) in K(e 2 ) K(x) = x K(let rec x y 1... y n = e 1 in e 2 ) = let rec x y 1... y n = K(e 1 ) in K(e 2 ) K(e e 1... e n ) = let x = K(e) in let y 1 = K(e 1 ) in... let y n = K(e n ) in x y 1... y n K(e 1,..., e n ) = let x 1 = K(e 1 ) in... let x n = K(e n ) in (x 1,..., x n ) K(let (x 1,..., x n ) = e 1 in e 2 ) = let y = K(e 1 ) in let (x 1,..., x n ) = y in K(e 2 ) K(Array.create e 1 e 2 ) = let x = K(e 1 ) in let y = K(e 2 ) in create array x y K(e 1.(e 2 )) = let x = K(e 1 ) in let y = K(e 2 ) in x.(y) K(e 1.(e 2 ) e 3 ) = let x = K(e 1 ) in let y = K(e 2 ) in let z = K(e 3 ) in x.(y) z 5: K insert let (fresh) 3

4 α : Id.t M.t KNormal.t KNormal.t α ε (c) = c α ε (op(x 1,..., x n )) = op(ε(x 1 ),..., ε(x n )) α ε (if x = y then e 1 else e 2 ) = if ε(x) = ε(y) then α ε (e 1 ) else α ε (e 2 ) α ε (if x y then e 1 else e 2 ) = if ε(x) ε(y) then α ε (e 1 ) else α ε (e 2 ) α ε (let x = e 1 in e 2 ) = let x = α ε (e 1 ) in α ε,x x (e 2 ) α ε (x) = ε(x) α ε (let rec x y 1... y n = e 1 in e 2 ) = let rec x y 1... y n = α ε,x x,y 1 y 1,...,y n y n (e 1) in α ε,x x (e 2 ) α ε (x y 1... y n ) = ε(x) ε(y 1 )... ε(y n ) α ε ((x 1,..., x n )) = (ε(x 1 ),..., ε(x n )) α ε (let (x 1,..., x n ) = y in e) = let (x 1,..., x n) = ε(y) in α ε,x1 x (e) 1,...,xn x n α ε (x.(y)) = ε(x).(ε(y)) α ε (x.(y) z) = ε(x).(ε(y)) ε(z) 6: α ε α α x fresh β : Id.t M.t KNormal.t KNormal.t β ε (c) = c β ε (op(x 1,..., x n )) = op(ε(x 1 ),..., ε(x n )) β ε (if x = y then e 1 else e 2 ) = if ε(x) = ε(y) then β ε (e 1 ) else β ε (e 2 ) β ε (if x y then e 1 else e 2 ) = if ε(x) ε(y) then β ε (e 1 ) else β ε (e 2 ) β ε (let x = e 1 in e 2 ) = β ε,x y (e 2 ) β ε (e 1 ) y β ε (let x = e 1 in e 2 ) = let x = β ε (e 1 ) in β ε (e 2 ) β ε (e 1 ) β ε (x) = ε(x) β ε (let rec x y 1... y n = e 1 in e 2 ) = let rec x y 1... y n = β ε (e 1 ) in β ε (e 2 ) β ε (x y 1... y n ) = ε(x) ε(y 1 )... ε(y n ) β ε ((x 1,..., x n )) = (ε(x 1 ),..., ε(x n )) β ε (let (x 1,..., x n ) = y in e) = let (x 1,..., x n ) = ε(y) in β ε (e) β ε (x.(y)) = ε(x).(ε(y)) β ε (x.(y) z) = ε(x).(ε(y)) ε(z) 7: β ε β β ε(x) ε(x) = x 4

5 A : KNormal.t KNormal.t A(c) = c A(op(x 1,..., x n )) = op(x 1,..., x n ) A(if x = y then e 1 else e 2 ) = if x = y then A(e 1 ) else A(e 2 ) A(if x y then e 1 else e 2 ) = if x y then A(e 1 ) else A(e 2 ) A(let x = e 1 in e 2 ) = let... in let x = e 1 in A(e 2 ) A(x) = x A(e 1 ) = let... in e 1 let... in 0 let e 1 let A(let rec x y 1... y n = e 1 in e 2 ) = let rec x y 1... y n = A(e 1 ) in A(e 2 ) A(x y 1... y n ) = x y 1... y n A((x 1,..., x n )) = (x 1,..., x n ) A(let (x 1,..., x n ) = y in e) = let (x 1,..., x n ) = y in A(e) A(x.(y)) = x.(y) A(x.(y) z) = x.(y) z 8: let 5

6 I : (Id.t list KNormal.t) M.t KNormal.t KNormal.t I ε (c) = c I ε (op(x 1,..., x n )) = op(x 1,..., x n ) I ε (if x = y then e 1 else e 2 ) = if x = y then I ε (e 1 ) else I ε (e 2 ) I ε (if x y then e 1 else e 2 ) = if x y then I ε (e 1 ) else I ε (e 2 ) I ε (let x = e 1 in e 2 ) = let x = I ε (e 1 ) in I ε (e 2 ) I ε (x) = x I ε (let rec x y 1... y n = e 1 in e 2 ) = ε = ε, x ((y 1,..., y n ), e 1 ) let rec x y 1... y n = I ε (e 1 ) in I ε (e 2 ) size(e 1 ) th I ε (let rec x y 1... y n = e 1 in e 2 ) = let rec x y 1... y n = I ε (e 1 ) in I ε (e 2 ) size(e 1 ) > th I ε (x y 1... y n ) = α y1 z 1,...,y n z n (e) ε(x) = ((z 1,..., z n ), e) I ε (x y 1... y n ) = x y 1... y n ε(x) I ε ((x 1,..., x n )) = (x 1,..., x n ) I ε (let (x 1,..., x n ) = y in e) = let (x 1,..., x n ) = y in I ε (e) I ε (x.(y)) = x.(y) I ε (x.(y) z) = x.(y) z size(c) = 1 size(op(x 1,..., x n )) = 1 size(if x = y then e 1 else e 2 ) = 1 + size(e 1 ) + size(e 2 ) size(if x y then e 1 else e 2 ) = 1 + size(e 1 ) + size(e 2 ) size(let x = e 1 in e 2 ) = 1 + size(e 1 ) + size(e 2 ) size(x) = 1 size(let rec x y 1... y n = e 1 in e 2 ) = 1 + size(e 1 ) + size(e 2 ) size(x y 1... y n ) = 1 size((x 1,..., x n )) = 1 size(let (x 1,..., x n ) = y in e) = 1 + size(e) size(x.(y)) = 1 size(x.(y) z) = 1 9: ε th 6

7 F : KNormal.t M.t KNormal.t KNormal.t F ε (c) = c F ε (op(x 1,..., x n )) = c op(ε(x 1 ),..., ε(x n )) = c F ε (op(x 1,..., x n )) = op(x 1,..., x n ) F ε (if x = y then e 1 else e 2 ) = F ε (e 1 ) ε(x) ε(y) F ε (if x = y then e 1 else e 2 ) = F ε (e 2 ) ε(x) ε(y) F ε (if x = y then e 1 else e 2 ) = if x = y then F ε (e 1 ) else F ε (e 2 ) F ε (if x y then e 1 else e 2 ) = F ε (e 1 ) ε(x) ε(y) ε(x) ε(y) F ε (if x y then e 1 else e 2 ) = F ε (e 2 ) ε(x) ε(y) ε(x) > ε(y) F ε (if x y then e 1 else e 2 ) = if x y then F ε (e 1 ) else F ε (e 2 ) F ε (let x = e 1 in e 2 ) = e 1 = F ε (e 1 ) F ε (x) = x let x = e 1 in F ε,x e 1 (e 2 ) F ε (let rec x y 1... y n = e 1 in e 2 ) = let rec x y 1... y n = F ε (e 1 ) in F ε (e 2 ) F ε (x y 1... y n ) = x y 1... y n F ε ((x 1,..., x n )) = (x 1,..., x n ) F ε (let (x 1,..., x n ) = y in e) = let x 1 = y 1 in... let x n = y n in F ε (e) F ε (let (x 1,..., x n ) = y in e) = let (x 1,..., x n ) = y in F ε (e) F ε (x.(y)) = x.(y) F ε (x.(y) z) = x.(y) z ε(y) = (y 1,..., y n ) 10: ε 7

8 E : KNormal.t KNormal.t E(c) = c E(op(x 1,..., x n )) = op(x 1,..., x n ) E(if x = y then e 1 else e 2 ) = if x = y then E(e 1 ) else E(e 2 ) E(if x y then e 1 else e 2 ) = if x y then E(e 1 ) else E(e 2 ) E(let x = e 1 in e 2 ) = E(e 2 ) effect(e(e 1 )) = false x FV (E(e 2 )) E(let x = e 1 in e 2 ) = let x = E(e 1 ) in E(e 2 ) E(x) = x E(let rec x y 1... y n = e 1 in e 2 ) = E(e 2 ) x FV (E(e 2 )) E(let rec x y 1... y n = e 1 in e 2 ) = let rec x y 1... y n = E(e 1 ) in E(e 2 ) E(x y 1... y n ) = x y 1... y n E((x 1,..., x n )) = (x 1,..., x n ) E(let (x 1,..., x n ) = y in e) = E(e) {x 1,..., x n } FV (E(e)) = E(let (x 1,..., x n ) = y in e) = let (x 1,..., x n ) = y in E(e) E(x.(y)) = x.(y) E(x.(y) z) = x.(y) z effect : KNormal.t bool effect(c) = false effect(op(x 1,..., x n )) = false effect(if x = y then e 1 else e 2 ) = effect(e 1 ) effect(e 2 ) effect(if x y then e 1 else e 2 ) = effect(e 1 ) effect(e 2 ) effect(let x = e 1 in e 2 ) = effect(e 1 ) effect(e 2 ) effect(x) = false effect(let rec x y 1... y n = e 1 in e 2 ) = effect(e 2 ) effect(x y 1... y n ) = true effect((x 1,..., x n )) = false effect(let (x 1,..., x n ) = y in e) = effect(e) effect(x.(y)) = false effect(x.(y) z) = true 11: (1/2) 8

9 FV : KNormal.t S.t FV (c) = FV (op(x 1,..., x n )) = {x 1,..., x n } FV (if x = y then e 1 else e 2 ) = {x, y} FV (e 1 ) FV (e 2 ) FV (if x y then e 1 else e 2 ) = {x, y} FV (e 1 ) FV (e 2 ) FV (let x = e 1 in e 2 ) = FV (e 1 ) (FV (e 2 ) \ {x}) FV (x) = {x} FV (let rec x y 1... y n = e 1 in e 2 ) = ((FV (e 1 ) \ {y 1,..., y n }) FV (e 2 )) \ {x} FV (x y 1... y n ) = {x, y 1,..., y n } FV ((x 1,..., x n )) = {x 1,..., x n } FV (let (x 1,..., x n ) = y in e) = {y} (FV (e) \ {x 1,..., x n }) FV (x.(y)) = {x, y} FV (x.(y) z) = {x, y, z} 12: (2/2) P ::= ({D 1,..., D n }, e) D ::= L x (y 1,..., y m )(z 1,..., z n ) = e e ::= c op(x 1,..., x n ) if x = y then e 1 else e 2 if x y then e 1 else e 2 let x = e 1 in e 2 x make closure x = (L x, (y 1,..., y n )) in e apply closure(x, y 1,..., y n ) apply direct(l x, y 1,..., y n ) (x 1,..., x n ) let (x 1,..., x n ) = y in e x.(y) x.(y) z (known function call) 13: 9

10 C : KNormal.t Closure.t C(c) = c C(op(x 1,..., x n )) = op(x 1,..., x n ) C(if x = y then e 1 else e 2 ) = if x = y then C(e 1 ) else C(e 2 ) C(if x y then e 1 else e 2 ) = if x y then C(e 1 ) else C(e 2 ) C(let x = e 1 in e 2 ) = let x = C(e 1 ) in C(e 2 ) C(x) = x C(let rec x y 1... y n = e 1 in e 2 ) = D L x (y 1,..., y n )(z 1,..., z m ) = e 1 make closure x = (L x, (z 1,..., z m )) in e 2 e 1 = C(e 1 ), e 2 = C(e 2 ), FV (e 1) \ {x, y 1,..., y n } = {z 1,..., z m } C(x y 1... y n ) = apply closure(x, y 1,..., y n ) C((x 1,..., x n )) = (x 1,..., x n ) C(let (x 1,..., x n ) = y in e) = let (x 1,..., x n ) = y in C(e) C(x.(y)) = x.(y) C(x.(y) z) = x.(y) z FV : Closure.t S.t FV (c) = FV (op(x 1,..., x n )) = {x 1,..., x n } FV (if x = y then e 1 else e 2 ) = {x, y} FV (e 1 ) FV (e 2 ) FV (if x y then e 1 else e 2 ) = {x, y} FV (e 1 ) FV (e 2 ) FV (let x = e 1 in e 2 ) = FV (e 1 ) (FV (e 2 ) \ {x}) FV (x) = {x} FV (make closure x = (L x, (y 1,..., y n )) in e) = {y 1,..., y n } (FV (e) \ {x}) FV (apply closure(x, y 1,..., y n )) = {x, y 1,..., y n } FV (apply direct(l x, y 1,..., y n )) = {y 1,..., y n } FV ((x 1,..., x n )) = {x 1,..., x n } FV (let (x 1,..., x n ) = y in e) = {y} (FV (e) \ {x 1,..., x n }) FV (x.(y)) = {x, y} FV (x.(y) z) = {x, y, z} 14: Closure C(e) D 10

11 C : S.t KNormal.t Closure.t C s (let rec x y 1... y n = e 1 in e 2 ) = D L x (y 1,..., y n )() = e 1 make closure x = (L x, ()) in e 2 e 1 = C s (e 1 ), e 2 = C s (e 2 ), s = s {x}, FV (e 1) \ {y 1,..., y n } = C s (let rec x y 1... y n = e 1 in e 2 ) = D L x (y 1,..., y n )(z 1,..., z m ) = e 1 make closure x = (L x, (z 1,..., z m )) in e 2 e 1 = C s (e 1 ), e 2 = C s (e 2 ), FV (e 1) \ {y 1,..., y n }, FV (e 1) \ {x, y 1,..., y n } = {z 1,..., z m } C s (x y 1... y n ) = apply closure(x, y 1,..., y n ) x s C s (x y 1... y n ) = apply direct(l x, y 1,..., y n ) x s 15: Closure C s (e) s C : S.t KNormal.t Closure.t C s (let rec x y 1... y n = e 1 in e 2 ) = D L x (y 1,..., y n )() = e 1 make closure x = (L x, ()) in e 2 e 1 = C s (e 1 ), e 2 = C s (e 2 ), s = s {x}, FV (e 1) \ {y 1,..., y n } = x FV (e 2) C s (let rec x y 1... y n = e 1 in e 2 ) = D L x (y 1,..., y n )() = e 1 e 2 e 1 = C s (e 1 ), e 2 = C s (e 2 ), s = s {x}, FV (e 1) \ {y 1,..., y n } = x FV (e 2) C s (let rec x y 1... y n = e 1 in e 2 ) = D L x (y 1,..., y n )(z 1,..., z m ) = e 1 make closure x = (L x, (z 1,..., z m )) in e 2 e 1 = C s (e 1 ), e 2 = C s (e 2 ), FV (e 1) \ {y 1,..., y n } =, FV (e 1) \ {x, y 1,..., y n } = {z 1,..., z m } C s (x y 1... y n ) = apply closure(x, y 1,..., y n ) x s C s (x y 1... y n ) = apply direct(l x, y 1,..., y n ) x s 16: Closure C s (e) 11

12 P ::= ({D 1,..., D n }, E) D ::= L x (y 1,..., y n ) = E E ::= x e; E e e ::= c L x op(x 1,..., x n ) if x = y then E 1 else E 2 if x y then E 1 else E 2 x apply closure(x, y 1,..., y n ) apply direct(l x, y 1,..., y n ) x.(y) x.(y) z save(x, y) restore(y) mov x y y 17: 12

13 V : Closure.prog SparcAsm.prog V(({D 1,..., D n }, e)) = ({V(D 1 ),..., V(D n )}, V(e)) V : Closure.fundef SparcAsm.fundef V(L x (y 1,..., y n )(z 1,..., z n ) = e) = L x (y 1,..., y n ) = z 1 R 0.(4);... ; z n R 0.(4n); V(e) V : Closure.t SparcAsm.t V(c) = c V(op(x 1,..., x n )) = op(x 1,..., x n ) V(if x = y then e 1 else e 2 ) = if x = y then V(e 1 ) else V(e 2 ) V(if x y then e 1 else e 2 ) = if x y then V(e 1 ) else V(e 2 ) V(let x = e 1 in e 2 ) = x V(e 1 ); V(e 2 ) V(x) = x V(make closure x = (L x, (y 1,..., y n )) in e) = x R hp ; R hp R hp + 4(n + 1); z L x ; x.(0) z; x.(4) y 1 ;... ; x.(4n) y n ; V(e) V(apply closure(x, y 1,..., y n )) = apply closure(x, y 1,..., y n ) V(apply direct(l x, y 1,..., y n )) = apply direct(l x, y 1,..., y n ) V((x 1,..., x n )) = y R hp ; R hp R hp + 4n; y.(0) x 1 ;... ; y.(4(n 1)) x n ; y V(let (x 1,..., x n ) = y in e) = {x 1,..., x n } FV (e) = {x i1,..., x im } x i1 y.(4(i 1 1));... ; x im y.(4(i m 1)); V(e) V(x.(y)) = y 4 y; x.(y ) V(x.(y) z) = y 4 y; x.(y ) z 18: V(P ), V(D) V(e) fresh R hp e 1 ; e 2 x x e 1 ; e 2 x E 1 ; E 2 E 1 = (x 1 e 1 ;... ; x n e n ; e) x 1 e 1 ;... ; x n e n ; x e; E 2 13

14 FV : S.t SparcAsm.t S.t FV s (x e; E) = s = FV s (E) \ {x} FV s (e) FV s (e) = FV s (e) FV : S.t SparcAsm.exp S.t FV s (c) = s FV s (L x ) = s FV s (op(x 1,..., x n )) = {x 1,..., x n } s FV s (if x = y then E 1 else E 2 ) = {x, y} FV s (E 1 ) FV s (E 2 ) FV s (if x y then E 1 else E 2 ) = {x, y} FV s (E 1 ) FV s (E 2 ) FV s (x) = {x} s FV s (apply closure(x, y 1,..., y n )) = {x, y 1,..., y n } s FV s (apply direct(l x, y 1,..., y n )) = {y 1,..., y n } s FV s (x.(y)) = {x, y} s FV s (x.(y) z) = {x, y, z} s FV s (save(x, y)) = {x} s FV s (restore(y)) = s 19: E e FV s (E) FV s (e) s E e FV (E) FV (E) 14

15 R : SparcAsm.prog SparcAsm.prog R(({D 1,..., D n }, E)) = ({R(D 1 ),..., R(D n )}, R (E, x, ())) x fresh R : SparcAsm.fundef SparcAsm.fundef R(L x (y 1,..., y n ) = E) = L x (R 1,..., R n ) = R x R0,y 1 R 1,...,y n R n (E, R 0, R 0 ) R : Id.t M.t SparcAsm.t Id.t SparcAsm.t SparcAsm.t Id.t M.t R ε ((x e; E), z dest, E cont ) = E cont = (z dest E; E cont ), R ε (e, x, E cont) = (E, ε ), r {ε (y) y FV (E cont)}, R ε,x r(e, z dest, E cont ) = (E, ε ) ((r E ; E ), ε ) x R ε ((r e; E), z dest, E cont ) = E cont = (z dest E; E cont ), R ε (e, r, E cont) = (E, ε ), R ε (E, z dest, E cont ) = (E, ε ) ((r E ; E ), ε ) R ε (e, x, E cont ) = R ε (e, x, E cont ) 20: R(P ), R(D) R ε (E, z dest, E cont ) ε z dest E E cont E R ε (E, x, E cont ) E E ε [ regalloc.notarget-nospill.ml ] 15

16 R : Id.t M.t SparcAsm.exp Id.t SparcAsm.t SparcAsm.t Id.t M.t R ε (c, z dest, E cont ) = (c, ε) R ε (L x, z dest, E cont ) = (L x, ε) R ε (op(x 1,..., x n ), z dest, E cont ) = (op(ε(x 1 ),..., ε(x n )), ε) R ε (if x = y then E 1 else E 2, z dest, E cont ) = R ε (E 1, z dest, E cont ) = (E 1, ε 1 ), R ε (E 2, z dest, E cont ) = (E 2, ε 2 ), ε = {z r ε 1 (z) = ε 2 (z) = r}, {z 1,..., z n } = (FV (E cont ) \ {z dest } \ dom(ε )) dom(ε) ((save(ε(z 1 ), z 1 );... ; save(ε(z n ), z n ); if ε(x) ε(y) then E 1 else E 2), ε ) R ε (if x y then E 1 else E 2, z dest, E cont ) = R ε (x, z dest, E cont ) = (ε(x), ε) R ε (apply closure(x, y 1,..., y n ), z dest, E cont ) = {z 1,..., z n } = (FV (E cont ) \ {z dest }) dom(ε) ((save(ε(z 1 ), z 1 );... ; save(ε(z n ), z n ); apply closure(ε(x), ε(y 1 ),..., ε(y n ))), ) R ε (apply direct(l x, y 1,..., y n ), z dest, E cont ) = R ε (x.(y), z dest, E cont ) = (ε(x).(ε(y)), ε) R ε (x.(y) z, z dest, E cont ) = (ε(x).(ε(y)) ε(z), ε) R ε (save(x, y), z dest, E cont ) = (save(ε(x), y), ε) R ε (restore(y), z dest, E cont ) = (restore(y), ε) 21: R ε (e, z dest, E cont ) R ε (e) x ε(x) R ε (e) = R ε (x restore(x); e) r ε(r) = r [ regalloc.notarget-nospill.ml ] 16

17 T : Id.t SparcAsm.t Id.t bool S.t T x ((y e; E), z dest ) = T x (e, y) = (c 1, s 1 ) c 1 (true, s 1 ) T x (E, z dest ) = (c 2, s 2 ) (c 2, s 1 s 2 ) T x (e, z dest ) = T x (e, z dest ) T : Id.t SparcAsm.exp Id.t bool S.t T x (x, z dest ) = (false, {z dest }) T x (if y = z then E 1 else E 2, z dest ) = T x (E 1, z dest ) = (c 1, s 1 ), T x (E 2, z dest ) = (c 2, s 2 ) (c 1 c 2, s 1 s 2 ) T x (if y z then E 1 else E 2, z dest ) = T x (apply closure(y 0, y 1,..., y n ), z dest ) = (true, {R i x = y i }) T x (apply direct(l y, y 1,..., y n ), z dest ) = T x (e, z dest ) = (false, ) 22: x r targeting T x (E, z dest ) T x (e, z dest ) E e c x s x T x (E cont, z dest ) = (c, s) r s [ regalloc.target-nospill.ml ] R : Id.t M.t SparcAsm.t Id.t SparcAsm.t SparcAsm.t Id.t M.t R ε ((x e; E), z dest, E cont ) = E cont = (z dest E; E cont ), R ε (e, x, E cont) = (E, ε ), y FV (E cont), R ε \{y ε (y)},x ε (y)(e, z dest, E cont ) = (E, ε ) { ((save(ε(y), y); ε (y) E ; E ), ε ) y dom(ε) ((ε (y) E ; E ), ε ) y dom(ε) x r {ε (y) y FV (E cont)} r 23: spilling R ε (E, z dest, E cont ) [ regalloc.target-latespill.ml ] 17

18 S : SparcAsm.prog string S(({D 1,..., D n }, E)) =.section ".text" S(D 1 )... S(D n ).global min_caml_start min_caml_start: save %sp, -112, %sp S(E, %g0) ret restore S : SparcAsm.fundef string S(L x (y 1,..., y n ) = E) = x: S(E, R 0 ) retl nop S : SparcAsm.t Id.t string S((x e; E), z dest ) = S(e, x) S(E, z dest ) S(e, z dest ) = S(e, z dest ) 24: S(P ), S(D) S(E, z dest ) 18

19 S : SparcAsm.exp Id.t string S(c, z dest ) = set c, z dest S(L x, z dest ) = set L x, z dest S(op(x 1,..., x n ), z dest ) = op x 1,..., x n, z dest S(if x = y then E 1 else E 2, z dest ) = cmp x, y bne b 1 nop S(E 1, z dest ) b b 2 nop b 1 : S(E 2, z dest ) b 2 : S(if x y then E 1 else E 2, z dest ) = S(x, z dest ) = mov x, z dest S(apply closure(x, y 1,..., y n ), z dest ) = shuffle((x, y 1,..., y n ), (R 0, R 1,..., R n )) st R ra, [R st + 4#ε] ld [R 0 ], R n+1 call R n+1 add R st, 4(#ε + 1), R st! delay slot sub R st, 4(#ε + 1), R st ld [R st + 4#ε], R ra mov R 0, z dest S(apply direct(l x, y 1,..., y n ), z dest ) = shuffle((y 1,..., y n ), (R 1,..., R n )) st R ra, [R st + 4#ε] call x add R st, 4(#ε + 1), R st! delay slot sub R st, 4(#ε + 1), R st ld [R st + 4#ε], R ra mov R 0, z dest S(x.(y), z dest ) = ld [x + y], z dest S(x.(y) z, z dest ) = st z, [x + y] S(save(x, y), z dest ) = y dom(ε) ε y 4#ε st x, [R st + ε(y)] S(restore(y), z dest ) = ld [R st + ε(y)], z dest 25: S(e, z dest ) ε #ε ε shuffle((x 1,..., x n ), (r 1,..., r n )) x 1,..., x n r 1,..., r n 19

20 S : S.t SparcAsm.t Id.t S.t string S s ((x e; E), z dest ) = S s (e, x) = (s, S), S s (E, z dest ) = (s, S ) (s, SS ) S s (e, z dest ) = S s (e, z dest ) S : S.t SparcAsm.exp Id.t S.t string S s (if x = y then E 1 else E 2, z dest ) = S s (E 1, z dest ) = (s 1, S 1 ), S s (E 2, z dest ) = (s 2, S 2 ) (s 1 s 2, cmp x, y bne b 1 nop S 1 b b 2 nop b 1 : S 2 b 2 :) S s (if x y then E 1 else E 2, z dest ) = S s (save(x, y), z dest ) = (s, nop) y s S s (save(x, y), z dest ) = y dom(ε) ε y 4#ε (s {y}, st x, [R st + ε(y)]) y s S s (e, z dest ) = (s, ) 26: save S s (E, z dest ) S s (e, z dest ) s save S(E, z dest ) S (E, z dest ) = (s, S) S 20

21 S : SparcAsm.fundef string S(L x (y 1,..., y n ) = E) = S (E, tail) = (s, S) x: S S : S.t SparcAsm.exp Id.t S.t string S s (if x = y then E 1 else E 2, tail) = S s (E 1, tail) = (s 1, S 1 ), S s (E 2, tail) = (s 2, S 2 ) (, cmp x, y bne b nop S 1 b: S 2 ) S s (if x y then E 1 else E 2, tail) = S s (apply closure(x, y 1,..., y n ), tail) = (, S s (apply direct(l x, y 1,..., y n ), tail) = (, shuffle((x, y 1,..., y n ), (R 0, R 1,..., R n )) ld [R 0 ], R n+1 jmp R n+1 nop) shuffle((y 1,..., y n ), (R 1,..., R n )) b x nop) S s (e, tail) = S s (e, R 0 ) = (s, S) (, S retl nop) 27: S s (D) S s (e, z dest ) z dest = tail 21