Theory Compiler

(*  Title:      JinjaDCI/Compiler/Compiler.thy

    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   TUM 2003, UIUC 2019-20

    Based on the Jinja theory Compiler/Compiler.thy by Tobias Nipkow
*)

section ‹ Combining Stages 1 and 2 ›

theory Compiler
imports Correctness1 Correctness2
begin

definition J2JVM :: "J_prog ⇒ jvm_prog"
where 
  "J2JVM  ≡  compP⇩2 ∘ compP⇩1"

theorem comp_correct_NonStatic:
assumes wf: "wf_J_prog P"
and "method": "P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in C"
and eval: "P ⊢ ⟨body,(h,[this#pns [↦] vs],sh)⟩ ⇒ ⟨e',(h',l',sh')⟩"
and sizes: "size vs = size pns + 1"    "size rest = max_vars body"
shows "J2JVM P ⊢ (None,h,[([],vs@rest,C,M,0,No_ics)],sh) -jvm→ (exception e',h',[],sh')"
(*<*)
proof -
  let ?P⇩1 = "compP⇩1 P"
  have nclinit: "M ≠ clinit" using wf_sees_clinit1[OF wf] visible_method_exists[OF "method"]
    sees_method_idemp[OF "method"] by fastforce
  have wf⇩1: "wf_J⇩1_prog ?P⇩1" by(rule compP⇩1_pres_wf[OF wf])
  have fv: "fv body ⊆ set (this#pns)"
    using wf_prog_wwf_prog[OF wf] "method" by(auto dest!:sees_wf_mdecl simp:wf_mdecl_def)
  have init: "[this#pns [↦] vs] ⊆⇩m [this#pns [↦] vs@rest]"
    using sizes by simp
  have "?P⇩1 ⊢ C sees M,NonStatic: Ts→T = (compE⇩1 (this#pns) body) in C"
    using sees_method_compP[OF "method", of "λb (pns,e). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) e"]
    by(simp)
  moreover obtain ls' where
    "?P⇩1 ⊢⇩1 ⟨compE⇩1 (this#pns) body, (h, vs@rest, sh)⟩ ⇒ ⟨fin⇩1 e', (h',ls', sh')⟩"
    using eval⇩1_eval[OF wf_prog_wwf_prog[OF wf] eval fv init] sizes by auto
  ultimately show ?thesis using comp⇩2_correct[OF wf⇩1] eval_final[OF eval] nclinit
    by(fastforce simp add:J2JVM_def final_def)
qed
(*>*)

theorem comp_correct_Static:
assumes wf: "wf_J_prog P"
and "method": "P ⊢ C sees M,Static:Ts→T = (pns,body) in C"
and eval: "P ⊢ ⟨body,(h,[pns [↦] vs],sh)⟩ ⇒ ⟨e',(h',l',sh')⟩"
and sizes: "size vs = size pns"    "size rest = max_vars body"
and nclinit: "M ≠ clinit"
shows "J2JVM P ⊢ (None,h,[([],vs@rest,C,M,0,No_ics)],sh) -jvm→ (exception e',h',[],sh')"
(*<*)
proof -
  let ?P⇩1 = "compP⇩1 P"
  have wf⇩1: "wf_J⇩1_prog ?P⇩1" by(rule compP⇩1_pres_wf[OF wf])
  have fv: "fv body ⊆ set pns"
    using wf_prog_wwf_prog[OF wf] "method" by(auto dest!:sees_wf_mdecl simp:wf_mdecl_def)
  have init: "[pns [↦] vs] ⊆⇩m [pns [↦] vs@rest]"
    using sizes by simp
  have "?P⇩1 ⊢ C sees M,Static: Ts→T = (compE⇩1 pns body) in C"
    using sees_method_compP[OF "method", of "λb (pns,e). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) e"]
    by(simp)
  moreover obtain ls' where
    "?P⇩1 ⊢⇩1 ⟨compE⇩1 pns body, (h, vs@rest, sh)⟩ ⇒ ⟨fin⇩1 e', (h',ls', sh')⟩"
    using eval⇩1_eval[OF wf_prog_wwf_prog[OF wf] eval fv init] sizes by auto
  ultimately show ?thesis using comp⇩2_correct[OF wf⇩1] eval_final[OF eval] nclinit
    by(fastforce simp add:J2JVM_def final_def)
qed
(*>*)

end