Theory PCompiler
section ‹ Program Compilation ›
theory PCompiler
imports "../Common/WellForm"
begin
definition compM :: "(staticb ⇒ 'a ⇒ 'b) ⇒ 'a mdecl ⇒ 'b mdecl"
where
"compM f ≡ λ(M, b, Ts, T, m). (M, b, Ts, T, f b m)"
definition compC :: "(staticb ⇒ 'a ⇒ 'b) ⇒ 'a cdecl ⇒ 'b cdecl"
where
"compC f ≡ λ(C,D,Fdecls,Mdecls). (C,D,Fdecls, map (compM f) Mdecls)"
definition compP :: "(staticb ⇒ 'a ⇒ 'b) ⇒ 'a prog ⇒ 'b prog"
where
"compP f ≡ map (compC f)"
text‹ Compilation preserves the program structure. Therefore lookup
functions either commute with compilation (like method lookup) or are
preserved by it (like the subclass relation). ›
lemma map_of_map4:
"map_of (map (λ(x,a,b,c).(x,a,b,f c)) ts) =
map_option (λ(a,b,c).(a,b,f c)) ∘ (map_of ts)"
proof(induct ts)
case Nil then show ?case by simp
qed fastforce
lemma map_of_map245:
"map_of (map (λ(x,a,b,c,d).(x,a,b,c,f a c d)) ts) =
map_option (λ(a,b,c,d).(a,b,c,f a c d)) ∘ (map_of ts)"
proof(induct ts)
case Nil then show ?case by simp
qed fastforce
lemma class_compP:
"class P C = Some (D, fs, ms)
⟹ class (compP f P) C = Some (D, fs, map (compM f) ms)"
by(simp add:class_def compP_def compC_def map_of_map4)
lemma class_compPD:
"class (compP f P) C = Some (D, fs, cms)
⟹ ∃ms. class P C = Some(D,fs,ms) ∧ cms = map (compM f) ms"
by(clarsimp simp add:class_def compP_def compC_def map_of_map4)
lemma [simp]: "is_class (compP f P) C = is_class P C"
by(auto simp:is_class_def dest: class_compP class_compPD)
lemma [simp]: "class (compP f P) C = map_option (λc. snd(compC f (C,c))) (class P C)"
by(simp add:compP_def compC_def class_def map_of_map4)
(simp add:split_def)
lemma sees_methods_compP:
"P ⊢ C sees_methods Mm ⟹
compP f P ⊢ C sees_methods (map_option (λ((b,Ts,T,m),D). ((b,Ts,T,f b m),D)) ∘ Mm)"
(is "?P ⟹ compP f P ⊢ C sees_methods (?map Mm)")
proof(induct rule: Methods.induct)
case Object: (sees_methods_Object D fs ms Mm)
let ?Mm1 = "λx. map_option ((λm. (m, Object)) ∘ (λ(b, Ts, T, m). (b, Ts, T, f b m))) (map_of ms x)"
let ?Mm2 = "λx. map_option (case_prod (λ(b, Ts, T, m).
Pair (b, Ts, T, f b m)) ∘ (λm. (m, Object))) (map_of ms x)"
have Mm_eq: "⋀x. ?Mm1 x = ?Mm2 x"
proof -
fix x show "?Mm1 x = ?Mm2 x"
proof(cases "map_of ms x")
case None then show ?thesis by simp
qed fastforce
qed
have Mm: "Mm = map_option (λm. (m, Object)) ∘ map_of ms" by fact
let ?Mm = "map_option (λm. (m, Object)) ∘ map_of (map (compM f) ms)"
let ?Mm' = "?map Mm"
have "?Mm' = ?Mm"
by(rule ext) (simp add:Mm Mm_eq compM_def map_of_map245 option.map_comp)
then show ?case by(rule sees_methods_Object[OF class_compP[OF Object(1)]])
next
case rec: (sees_methods_rec C D fs ms Mm Mm')
have Mm': "Mm' = Mm ++ (map_option (λm. (m, C)) ∘ map_of ms)" by fact
let ?Mm' = "?map Mm'"
let ?Mm'' = "(?map Mm) ++ (map_option (λm. (m, C)) ∘ map_of (map (compM f) ms))"
have "?Mm' = ?Mm''"
by(rule ext) (simp add:Mm' map_add_def compM_def map_of_map245)
moreover have "compP f P ⊢ C sees_methods ?Mm''"
using sees_methods_rec[OF class_compP[OF rec(1)] rec(2,4)] by fast
ultimately show "compP f P ⊢ C sees_methods ?Mm'" by simp
qed
lemma sees_method_compP:
"P ⊢ C sees M,b: Ts→T = m in D ⟹
compP f P ⊢ C sees M,b: Ts→T = (f b m) in D"
by(fastforce elim:sees_methods_compP simp add:Method_def)
lemma [simp]:
"P ⊢ C sees M,b: Ts→T = m in D ⟹
method (compP f P) C M = (D,b,Ts,T,f b m)"
proof -
let ?P = "λ(D, b, Ts, T, m). compP f P ⊢ C sees M, b : Ts→T = m in D"
let ?a = "(D, b, Ts, T, f b m)"
assume cM: "P ⊢ C sees M,b: Ts→T = m in D"
have compP_cM: "?P ?a" using sees_method_compP[OF cM] by simp
moreover {
fix x assume "?P x" then have "x = ?a"
using compP_cM by(fastforce dest:sees_method_fun)
}
ultimately have "(THE x. ?P x) = ?a" by(rule the_equality)
then show ?thesis by(simp add:method_def)
qed
lemma sees_methods_compPD:
"⟦ cP ⊢ C sees_methods Mm'; cP = compP f P ⟧ ⟹
∃Mm. P ⊢ C sees_methods Mm ∧
Mm' = (map_option (λ((b,Ts,T,m),D). ((b,Ts,T,f b m),D)) ∘ Mm)"
(is "⟦ ?P; ?Q ⟧ ⟹ ∃Mm. P ⊢ C sees_methods Mm ∧ Mm' = (?map Mm)")
proof(induct rule: Methods.induct)
case Object: (sees_methods_Object D fs ms Mm)
then obtain ms' where P_Obj: "class P Object = ⌊(D, fs, ms')⌋"
and ms: "ms = map (compM f) ms'" by(clarsimp simp:compC_def)
let ?Mm1 = "λx. map_option ((λm. (m, Object)) ∘ (λ(b, Ts, T, m). (b, Ts, T, f b m))) (map_of ms' x)"
let ?Mm2 = "λx. map_option (case_prod (λ(b, Ts, T, m). Pair (b, Ts, T, f b m)) ∘ (λm. (m, Object)))
(map_of ms' x)"
have Mm_eq: "⋀x. ?Mm1 x = ?Mm2 x"
proof -
fix x show "?Mm1 x = ?Mm2 x"
proof(cases "map_of ms' x")
case None then show ?thesis by simp
qed fastforce
qed
let ?Mm = "map_option (λm. (m,Object)) ∘ map_of ms'"
let ?Mm' = "?map ?Mm"
have Mm: "Mm = map_option (λm. (m, Object)) ∘ map_of ms" by fact
have "P ⊢ Object sees_methods ?Mm"
using sees_methods_Object[OF P_Obj] by simp
moreover have "Mm = ?Mm'"
by(rule ext) (simp add:Mm_eq Mm ms compM_def map_of_map245 option.map_comp)
ultimately show ?case by fast
next
case rec: (sees_methods_rec C D fs ms Mm Mm')
then obtain ms' Mm⇩D where P_D: "class P C = ⌊(D, fs, ms')⌋"
and ms: "ms = map (compM f) ms'" and C_nObj: "C ≠ Object"
and Mm⇩D: "P ⊢ D sees_methods Mm⇩D"
and Mm: "Mm = (λa. map_option (case_prod (λ(b, Ts, T, m). Pair (b, Ts, T, f b m))) (Mm⇩D a))"
by(clarsimp simp:compC_def)
let ?Mm = "Mm⇩D ++ (map_option (λm. (m, C)) ∘ map_of ms')"
let ?Mm1 = "Mm ++ (map_option (λm. (m, C)) ∘ map_of ms)"
let ?Mm2 = "Mm ++ (map_option (λm. (m, C)) ∘ map_of (map (compM f) ms'))"
let ?Mm3 = "?map ?Mm"
have "Mm' = ?Mm1" by fact
also have "… = ?Mm2" using ms by simp
also have "… = ?Mm3"
by(rule ext)(simp add:Mm map_add_def compM_def map_of_map245)
moreover have "P ⊢ C sees_methods ?Mm"
using sees_methods_rec[OF P_D C_nObj Mm⇩D] by simp
ultimately show ?case by fast
qed
lemma sees_method_compPD:
"compP f P ⊢ C sees M,b: Ts→T = fm in D ⟹
∃m. P ⊢ C sees M,b: Ts→T = m in D ∧ f b m = fm"
proof -
assume "compP f P ⊢ C sees M,b: Ts→T = fm in D"
then obtain Mm where Mm: "compP f P ⊢ C sees_methods Mm"
and MmM: "Mm M = ⌊((b, Ts, T, fm), D)⌋"
by(clarsimp simp:Method_def)
show ?thesis using sees_methods_compPD[OF Mm refl] MmM
by(fastforce simp: Method_def)
qed
lemma [simp]: "subcls1(compP f P) = subcls1 P"
by(fastforce simp add: is_class_def compC_def intro:subcls1I order_antisym dest:subcls1D)
lemma compP_widen[simp]: "(compP f P ⊢ T ≤ T') = (P ⊢ T ≤ T')"
by(cases T')(simp_all add:widen_Class)
lemma [simp]: "(compP f P ⊢ Ts [≤] Ts') = (P ⊢ Ts [≤] Ts')"
proof(induct Ts)
case (Cons a Ts)
then show ?case by(cases Ts')(auto simp:fun_of_def)
qed simp
lemma [simp]: "is_type (compP f P) T = is_type P T"
by(cases T) simp_all
lemma [simp]: "(compP (f::staticb⇒'a⇒'b) P ⊢ C has_fields FDTs) = (P ⊢ C has_fields FDTs)"
(is "?A = ?B")
proof
{ fix cP::"'b prog" assume "cP ⊢ C has_fields FDTs"
hence "cP = compP f P ⟹ P ⊢ C has_fields FDTs"
proof induct
case has_fields_Object
thus ?case by(fast intro:Fields.has_fields_Object dest:class_compPD)
next
case has_fields_rec
thus ?case by(fast intro:Fields.has_fields_rec dest:class_compPD)
qed
} note lem = this
assume ?A
with lem show ?B by blast
next
assume ?B
thus ?A
proof induct
case has_fields_Object
thus ?case by(fast intro:Fields.has_fields_Object class_compP)
next
case has_fields_rec
thus ?case by(fast intro:Fields.has_fields_rec class_compP)
qed
qed
lemma fields_compP [simp]: "fields (compP f P) C = fields P C"
by(simp add:fields_def)
lemma ifields_compP [simp]: "ifields (compP f P) C = ifields P C"
by(simp add:ifields_def)
lemma blank_compP [simp]: "blank (compP f P) C = blank P C"
by(simp add:blank_def)
lemma isfields_compP [simp]: "isfields (compP f P) C = isfields P C"
by(simp add:isfields_def)
lemma sblank_compP [simp]: "sblank (compP f P) C = sblank P C"
by(simp add:sblank_def)
lemma sees_fields_compP [simp]: "(compP f P ⊢ C sees F,b:T in D) = (P ⊢ C sees F,b:T in D)"
by(simp add:sees_field_def)
lemma has_field_compP [simp]: "(compP f P ⊢ C has F,b:T in D) = (P ⊢ C has F,b:T in D)"
by(simp add:has_field_def)
lemma field_compP [simp]: "field (compP f P) F D = field P F D"
by(simp add:field_def)
subsection‹Invariance of @{term wf_prog} under compilation ›
lemma [iff]: "distinct_fst (compP f P) = distinct_fst P"
by (induct P)
(auto simp:distinct_fst_def compP_def compC_def image_iff)
lemma [iff]: "distinct_fst (map (compM f) ms) = distinct_fst ms"
by (induct ms)
(auto simp:distinct_fst_def compM_def image_iff)
lemma [iff]: "wf_syscls (compP f P) = wf_syscls P"
by(simp add:wf_syscls_def compP_def compC_def image_def Bex_def)
lemma [iff]: "wf_fdecl (compP f P) = wf_fdecl P"
by(simp add:wf_fdecl_def)
lemma wf_clinit_compM [iff]: "wf_clinit (map (compM f) ms) = wf_clinit ms"
proof(rule iffI)
assume "wf_clinit (map (compM f) ms)"
then obtain m where "(clinit, Static, [], Void, m) ∈ set ms"
by(clarsimp simp: wf_clinit_def compM_def)
then show "wf_clinit ms" by(fastforce simp: wf_clinit_def)
next
assume "wf_clinit ms"
then obtain m where "(clinit, Static, [], Void, m) ∈ set ms"
by(clarsimp simp: wf_clinit_def compM_def)
then have "∃m. (clinit, Static, [], Void, m)
∈ (λx. case x of (M, b, Ts, T, m) ⇒ (M, b, Ts, T, f b m)) ` set ms"
by(rule_tac x = "f Static m" in exI) (simp add: rev_image_eqI)
then show "wf_clinit (map (compM f) ms)"
by(simp add: wf_clinit_def compM_def)
qed
lemma set_compP:
"((C,D,fs,ms') ∈ set(compP f P)) =
(∃ms. (C,D,fs,ms) ∈ set P ∧ ms' = map (compM f) ms)"
by(fastforce simp add:compP_def compC_def image_iff Bex_def)
lemma wf_cdecl_compPI:
"⟦ ⋀C M b Ts T m.
⟦ wf_mdecl wf⇩1 P C (M,b,Ts,T,m); P ⊢ C sees M,b:Ts→T = m in C ⟧
⟹ wf_mdecl wf⇩2 (compP f P) C (M,b,Ts,T, f b m);
∀x∈set P. wf_cdecl wf⇩1 P x; x ∈ set (compP f P); wf_prog p P ⟧
⟹ wf_cdecl wf⇩2 (compP f P) x"
proof -
assume
wfm: "⋀C M b Ts T m. ⟦ wf_mdecl wf⇩1 P C (M,b,Ts,T,m); P ⊢ C sees M,b:Ts→T = m in C ⟧
⟹ wf_mdecl wf⇩2 (compP f P) C (M,b,Ts,T, f b m)"
and wfc: "∀x∈set P. wf_cdecl wf⇩1 P x"
and compP: "x ∈ set (compP f P)" and wf: "wf_prog p P"
obtain C D fs ms where x: "x = (C, D, fs, map (compM f) ms)"
and x_set: "(C, D, fs, ms) ∈ set P"
using compP by(case_tac x) (clarsimp simp: set_compP)
have wfc': "wf_cdecl wf⇩1 P (C, D, fs, ms)" using wfc x_set by fast
let ?P = "compP f P" and ?ms = "compM f ` set ms"
{ fix M b Ts T m
assume M: "(M,b,Ts,T,m) ∈ set ms"
then have "wf_mdecl wf⇩1 P C (M, b, Ts, T, m)" using wfc'
by(simp add:wf_cdecl_def)
moreover have cM: "P ⊢ C sees M, b : Ts→T = m in C" using M
by(rule mdecl_visible[OF wf x_set])
ultimately have "wf_mdecl wf⇩2 (compP f P) C (M, b, Ts, T, f b m)"
by(rule wfm)
}
then have "∀m ∈ ?ms. wf_mdecl wf⇩2 ?P C m"
by (clarsimp simp:compM_def)
moreover have "C ≠ Object ⟶
(∀(M,b,Ts,T,m)∈?ms.
∀D' b' Ts' T' m'. ?P ⊢ D sees M,b':Ts' → T' = m' in D' ⟶
b = b' ∧ P ⊢ Ts' [≤] Ts ∧ P ⊢ T ≤ T')"
proof -
{ fix M b Ts T m D' b' Ts' T' m'
assume "C ≠ Object" and "(M,b,Ts,T,m)∈?ms"
and dM: "?P ⊢ D sees M,b':Ts' → T' = m' in D'"
then have "b = b' ∧ P ⊢ Ts' [≤] Ts ∧ P ⊢ T ≤ T'"
using wfc' sees_method_compPD[OF dM]
by(fastforce simp:wf_cdecl_def image_iff compM_def)
}
then show ?thesis by fast
qed
moreover have "(∀f∈set fs. wf_fdecl P f) ∧ distinct_fst fs
∧ distinct_fst ms ∧ wf_clinit ms
∧ (C ≠ Object ⟶ is_class P D ∧ ¬ P ⊢ D ≼⇧* C)" using wfc'
by(simp add: wf_cdecl_def)
ultimately show ?thesis using x by(simp add:wf_cdecl_def)
qed
lemma wf_prog_compPI:
assumes lift:
"⋀C M b Ts T m.
⟦ P ⊢ C sees M,b:Ts→T = m in C; wf_mdecl wf⇩1 P C (M,b,Ts,T,m) ⟧
⟹ wf_mdecl wf⇩2 (compP f P) C (M,b,Ts,T, f b m)"
and wf: "wf_prog wf⇩1 P"
shows "wf_prog wf⇩2 (compP f P)"
using wf
by (simp add:wf_prog_def) (blast intro:wf_cdecl_compPI lift wf)
end