# Theory PCompiler

```(*  Title:      JinjaThread/Compiler/PCompiler.thy
Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Program Compilation›

theory PCompiler
imports
"../Common/WellForm"
"../Common/BinOp"
"../Common/Conform"
begin

definition compM :: "(mname ⇒ ty list ⇒ ty ⇒ 'a ⇒ 'b) ⇒ 'a mdecl' ⇒ 'b mdecl'"
where "compM f ≡ λ(M, Ts, T, m). (M, Ts, T, map_option (f M Ts T) m)"

definition compC :: "(cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'a ⇒ 'b) ⇒ 'a cdecl ⇒ 'b cdecl"
where "compC f  ≡  λ(C,D,Fdecls,Mdecls). (C,D,Fdecls, map (compM (f C)) Mdecls)"

primrec compP :: "(cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'a ⇒ 'b) ⇒ 'a prog ⇒ 'b prog"
where "compP f (Program P) = Program (map (compC f) P)"

text‹Compilation preserves the program structure.  Therfore 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 x a b c)) ts) =
(λx. map_option (λ(a,b,c).(a,b,f x a b c)) (map_of ts x))"
apply(induct ts)
apply simp
apply(rule ext)
apply fastforce
done

lemma class_compP:
"class P C = Some (D, fs, ms)
⟹ class (compP f P) C = Some (D, fs, map (compM (f C)) ms)"
by(cases P)(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 C)) ms"
by(cases P)(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)"
(*<*)
apply(cases P)
done
(*>*)

lemma sees_methods_compP:
"P ⊢ C sees_methods Mm ⟹
compP f P ⊢ C sees_methods (λM. map_option (λ((Ts,T,m),D). ((Ts,T,map_option (f D M Ts T) m),D)) (Mm M))"
(*<*)
apply(erule Methods.induct)
apply(rule sees_methods_Object)
apply(erule class_compP)
apply(rule ext)
apply(case_tac "map_of ms M")
apply simp
apply fastforce
apply(rule sees_methods_rec)
apply(erule class_compP)
apply assumption
apply assumption
apply(rule ext)
done
(*>*)

lemma sees_method_compP:
"P ⊢ C sees M: Ts→T = m in D ⟹
compP f P ⊢ C sees M: Ts→T = map_option (f D M Ts T) m in D"

lemma [simp]:
"P ⊢ C sees M: Ts→T = m in D ⟹
method (compP f P) C M = (D,Ts,T,map_option (f D M Ts T) m)"
(*<*)
apply(drule sees_method_compP)
apply(rule the_equality)
apply simp
apply(fastforce dest:sees_method_fun)
done
(*>*)

lemma sees_methods_compPD:
"⟦ cP ⊢ C sees_methods Mm'; cP = compP f P ⟧ ⟹
∃Mm. P ⊢ C sees_methods Mm ∧
Mm' = (λM. map_option (λ((Ts,T,m),D). ((Ts,T,map_option (f D M Ts T) m),D)) (Mm M))"
(*<*)
apply(erule Methods.induct)
apply(clarsimp simp:compC_def)
apply(rule exI)
apply(rule conjI, erule sees_methods_Object)
apply(rule refl)
apply(rule ext)
apply(case_tac "map_of b M")
apply simp
apply fastforce
apply(clarsimp simp:compC_def)
apply(rule exI, rule conjI)
apply(erule (2) sees_methods_rec)
apply(rule refl)
apply(rule ext)
done
(*>*)

lemma sees_method_compPD:
"compP f P ⊢ C sees M: Ts→T = fm in D ⟹
∃m. P ⊢ C sees M: Ts→T = m in D ∧ map_option (f D M Ts T) m = fm"
(*<*)
apply clarify
apply(drule sees_methods_compPD[OF _ refl])
apply clarsimp
apply blast
done
(*>*)

lemma sees_method_native_compP [simp]:
"compP f P ⊢ C sees M:Ts → T = Native in D ⟷ P ⊢ C sees M:Ts → T = Native in D"
by(auto dest: sees_method_compPD sees_method_compP)

lemma [simp]: "subcls1(compP f P) = subcls1 P"
by(fastforce simp add: is_class_def compC_def intro:subcls1I order_antisym dest:subcls1D)

lemma [simp]: "is_type (compP f P) T = is_type P T"
by(induct T)(auto cong: ty.case_cong)

lemma is_type_compP [simp]: "is_type (compP f P) = is_type P"
by auto

lemma compP_widen[simp]:
"(compP f P ⊢ T ≤ T') = (P ⊢ T ≤ T')"
by(induct T' arbitrary: T)(simp_all add: widen_Class widen_Array)

lemma [simp]: "(compP f P ⊢ Ts [≤] Ts') = (P ⊢ Ts [≤] Ts')"
(*<*)
apply(induct Ts)
apply simp
apply(cases Ts')
apply(auto simp:fun_of_def)
done
(*>*)

lemma is_lub_compP [simp]:
"is_lub (compP f P) = is_lub P"
by(auto intro!: ext elim!: is_lub.cases intro: is_lub.intros)

lemma [simp]:
fixes f :: "cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'a ⇒ 'b"
shows "(compP f 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 [simp]: "fields (compP f P) C = fields P C"

lemma [simp]: "(compP f P ⊢ C sees F:T (fm) in D) = (P ⊢ C sees F:T (fm) in D)"

lemma [simp]: "field (compP f P) F D = field P F D"

subsection‹Invariance of @{term wf_prog} under compilation›

lemma [iff]: "distinct_fst (classes (compP f P)) = distinct_fst (classes P)"
(*<*)
apply(cases P)
apply(rename_tac list)
apply(induct_tac list)
apply (auto simp:image_iff)
done
(*>*)

lemma [iff]: "distinct_fst (map (compM f) ms) = distinct_fst ms"
(*<*)
apply(induct ms)
apply (auto simp:image_iff)
done
(*>*)

lemma [iff]: "wf_syscls (compP f P) = wf_syscls P"
unfolding wf_syscls_def by auto

lemma [iff]: "wf_fdecl (compP f P) = wf_fdecl P"

lemma set_compP:
"(class (compP f P) C = ⌊(D,fs,ms')⌋) ⟷
(∃ms. class P C = ⌊(D,fs,ms)⌋ ∧ ms' = map (compM (f C)) ms)"
by(cases P)(auto simp add: compC_def image_iff map_of_map4)

lemma compP_has_method: "compP f P ⊢ C has M ⟷ P ⊢ C has M"
unfolding has_method_def
by(fastforce dest: sees_method_compPD intro: sees_method_compP)

lemma is_native_compP [simp]: "is_native (compP f P) = is_native P"

lemma τexternal_compP [simp]:
"τexternal (compP f P) = τexternal P"
by(auto intro!: ext simp add: τexternal_def)

context heap_base begin

lemma heap_clone_compP [simp]:
"heap_clone (compP f P) = heap_clone P"
by(intro ext)(auto elim!: heap_clone.cases intro: heap_clone.intros)

lemma red_external_compP [simp]:
"compP f P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩ ⟷ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩"
by(auto elim!: red_external.cases intro: red_external.intros)

lemma τexternal'_compP [simp]:
"τexternal' (compP f P) = τexternal' P"

end

lemma wf_overriding_compP [simp]: "wf_overriding (compP f P) D (compM (f C) m) = wf_overriding P D m"
by(cases m)(fastforce intro: sees_method_compP[where f=f] dest: sees_method_compPD[where f=f] simp add: compM_def)

lemma wf_cdecl_compPI:
assumes wf1_imp_wf2:
"⋀C M Ts T m. ⟦ wf_mdecl wf⇩1 P C (M,Ts,T,⌊m⌋); P ⊢ C sees M:Ts→T = ⌊m⌋ in C ⟧
⟹ wf_mdecl wf⇩2 (compP f P) C (M,Ts,T, ⌊f C M Ts T m⌋)"
and wfcP1: "∀C rest. class P C = ⌊rest⌋ ⟶ wf_cdecl wf⇩1 P (C, rest)"
and xcomp: "class (compP f P) C = ⌊rest'⌋"
and wf: "wf_prog p P"
shows "wf_cdecl wf⇩2 (compP f P) (C, rest')"
proof -
obtain D fs ms' where x: "rest' = (D, fs, ms')" by(cases rest')
with xcomp obtain ms where xsrc: "class P C = ⌊(D,fs,ms)⌋"
and ms': "ms' = map (compM (f C)) ms"
from xsrc wfcP1 have wf1: "wf_cdecl wf⇩1 P (C,D,fs,ms)" by blast
{ fix field
assume "field ∈ set fs"
with wf1 have "wf_fdecl (compP f P) field" by(simp add: wf_cdecl_def)
}
moreover from wf1 have "distinct_fst fs" by(simp add: wf_cdecl_def)
moreover
{ fix m
assume mset': "m ∈ set ms'"
obtain M Ts' T' body' where m: "m = (M, Ts', T', body')" by(cases m)
with ms' obtain body where mf: "body' = map_option (f C M Ts' T') body"
and mset: "(M, Ts', T', body) ∈ set ms" using mset'
moreover from mset xsrc wfcP1 have "wf_mdecl wf⇩1 P C (M,Ts',T',body)"
moreover from wf xsrc mset x have "P ⊢ C sees M:Ts'→T' = body in C"
by(auto intro: mdecl_visible)
ultimately have "wf_mdecl wf⇩2 (compP f P) C m" using m
by(cases body)(simp add: wf_mdecl_def, auto intro: wf1_imp_wf2) }
moreover from wf1 have "distinct_fst ms" by(simp add: wf_cdecl_def)
with ms' have "distinct_fst ms'" by(auto)
moreover
{ assume CObj: "C ≠ Object"
with xsrc wfcP1
have part1: "is_class (compP f P) D" "¬ compP f P ⊢ D ≼⇧* C"
{ fix m
assume mset': "m ∈ set ms'"
obtain M Ts T body' where m: "m = (M, Ts, T, body')" by(cases m)
with mset' ms' obtain body where mf: "body' = map_option (f C M Ts T) body"
and mset: "(M, Ts, T, body) ∈ set ms"
from wf1 CObj mset
have "wf_overriding P D (M, Ts, T, body)" by(auto simp add: wf_cdecl_def simp del: wf_overriding.simps)
hence "wf_overriding (compP f P) D m" unfolding m mf
by(subst (asm) wf_overriding_compP[symmetric, where f=f and C=C])(simp del: wf_overriding.simps wf_overriding_compP add: compM_def) }
note this part1 }
moreover
with wf1 ms' have "∃m. (run, [], Void, m) ∈ set ms'"
by(fastforce simp add: wf_cdecl_def image_iff compM_def)+ }
ultimately show ?thesis unfolding x wf_cdecl_def by blast
qed

lemma wf_prog_compPI:
assumes lift:
"⋀C M Ts T m.
⟦ P ⊢ C sees M:Ts→T = ⌊m⌋ in C; wf_mdecl wf⇩1 P C (M,Ts,T,⌊m⌋) ⟧
⟹ wf_mdecl wf⇩2 (compP f P) C (M,Ts,T, ⌊f C M Ts T m⌋)"
and wf: "wf_prog wf⇩1 P"
shows "wf_prog wf⇩2 (compP f P)"
using wf
apply(rule wf_cdecl_compPI[OF lift], assumption+)
apply(auto intro: wf)
done

lemma wf_cdecl_compPD:
assumes wf1_imp_wf2:
"⋀C M Ts T m. ⟦ wf_mdecl wf⇩1 (compP f P) C (M,Ts,T,⌊f C M Ts T m⌋); compP f P ⊢ C sees M:Ts→T = ⌊f C M Ts T m⌋ in C ⟧
⟹ wf_mdecl wf⇩2 P C (M,Ts,T, ⌊m⌋)"
and wfcP1: "∀C rest. class (compP f P) C = ⌊rest⌋ ⟶ wf_cdecl wf⇩1 (compP f P) (C, rest)"
and xcomp: "class P C = ⌊rest⌋"
and wf: "wf_prog wf_md (compP f P)"
shows "wf_cdecl wf⇩2 P (C, rest)"
proof -
obtain D fs ms' where x: "rest = (D, fs, ms')" by(cases rest)
with xcomp have xsrc: "class (compP f P) C = ⌊(D,fs,map (compM (f C)) ms')⌋"
from xsrc wfcP1 have wf1: "wf_cdecl wf⇩1 (compP f P) (C,D,fs,map (compM (f C)) ms')" by blast
{ fix field
assume "field ∈ set fs"
with wf1 have "wf_fdecl P field" by(simp add: wf_cdecl_def)
}
moreover from wf1 have "distinct_fst fs" by(simp add: wf_cdecl_def)
moreover
{ fix m
assume mset': "m ∈ set ms'"
obtain M Ts' T' body' where m: "m = (M, Ts', T', body')" by(cases m)
hence mset: "(M, Ts', T', map_option (f C M Ts' T') body') ∈ set (map (compM (f C)) ms')" using mset'
by(auto simp add: image_iff compM_def intro: rev_bexI)
moreover from wf xsrc mset x have "compP f P ⊢ C sees M:Ts'→T' = map_option (f C M Ts' T') body' in C"
by(auto intro: mdecl_visible)
moreover from mset wfcP1[rule_format, OF xsrc]
have "wf_mdecl wf⇩1 (compP f P) C (M,Ts',T',map_option (f C M Ts' T') body')"
ultimately have "wf_mdecl wf⇩2 P C m" using m
by(cases body')(simp add: wf_mdecl_def, auto intro: wf1_imp_wf2) }
moreover from wf1 have "distinct_fst ms'" by(simp add: wf_cdecl_def)
moreover
{ assume CObj: "C ≠ Object"
with xsrc wfcP1
have part1: "is_class P D" "¬ P ⊢ D ≼⇧* C"
{ fix m
assume mset': "m ∈ set ms'"
with wf1 CObj have "wf_overriding (compP f P) D (compM (f C) m)"
hence "wf_overriding P D m" by simp }
note this part1 }
moreover
with wf1 have "∃m. (run, [], Void, m) ∈ set ms'"
by(fastforce simp add: wf_cdecl_def image_iff compM_def)+ }
ultimately show ?thesis unfolding x wf_cdecl_def by blast
qed

lemma wf_prog_compPD:
assumes wf: "wf_prog wf1 (compP f P)"
and lift:
"⋀C M Ts T m.
⟦ compP f P ⊢ C sees M:Ts→T = ⌊f C M Ts T m⌋ in C; wf_mdecl wf1 (compP f P) C (M,Ts,T, ⌊f C M Ts T m⌋) ⟧
⟹ wf_mdecl wf2 P C (M,Ts,T,⌊m⌋)"
shows "wf_prog wf2 P"
using wf
apply(rule wf_cdecl_compPD[OF lift], assumption+)
apply(auto intro: wf)
done

lemma WT_binop_compP [simp]: "compP f P ⊢ T1«bop»T2 :: T ⟷ P ⊢ T1«bop»T2 :: T"
by(cases bop)(fastforce)+

lemma WTrt_binop_compP [simp]: "compP f P ⊢ T1«bop»T2 : T ⟷ P ⊢ T1«bop»T2 : T"
by(cases bop)(fastforce)+

lemma binop_relevant_class_compP [simp]: "binop_relevant_class bop (compP f P) = binop_relevant_class bop P"
by(cases bop) simp_all

lemma is_class_compP [simp]:
"is_class (compP f P) = is_class P"

lemma has_field_compP [simp]:
"compP f P ⊢ C has F:T (fm) in D ⟷ P ⊢ C has F:T (fm) in D"

context heap_base begin

lemma conf_compP [simp]:
"compP f P,h ⊢ v :≤ T ⟷ P,h ⊢ v :≤ T"

lemma compP_conf: "conf (compP f P) = conf P"
by(auto simp add: conf_def intro!: ext)

lemma compP_confs: "compP f P,h ⊢ vs [:≤] Ts ⟷ P,h ⊢ vs [:≤] Ts"

lemma tconf_compP [simp]: "compP f P, h ⊢ t √t ⟷ P,h ⊢ t √t"

lemma wf_start_state_compP [simp]:
"wf_start_state (compP f P) = wf_start_state P"
by(auto 4 6 simp add: fun_eq_iff wf_start_state.simps compP_conf dest: sees_method_compP[where f=f] sees_method_compPD[where f=f])

end

by simp

lemma compP_heap:
by auto

lemma compP_heap_conf:
unfolding heap_conf_def heap_conf_axioms_def compP_heap
by(rule refl)

by(rule refl)

text ‹compiler composition›

lemma compM_compM:
"compM f (compM g md) = compM (λM Ts T. f M Ts T ∘ g M Ts T) md"
by(cases md)(simp add: compM_def option.map_comp o_def)

lemma compC_compC:
"compC f (compC g cd) = compC (λC M Ts T. f C M Ts T ∘ g C M Ts T) cd"