Theory PCompiler

(*  Title:      JinjaDCI/Compiler/PCompiler.thy

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

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

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: TsT = m in D 
  compP f P  C sees M,b: TsT = (f b m) in D"
(*<*)by(fastforce elim:sees_methods_compP simp add:Method_def)(*>*)


lemma [simp]:
  "P  C sees M,b: TsT = 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 :  TsT = m in D"
  let ?a = "(D, b, Ts, T, f b m)"
  assume cM: "P  C sees M,b: TsT = 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' MmD where P_D: "class P C = (D, fs, ms')"
     and ms: "ms = map (compM f) ms'" and C_nObj: "C  Object"
     and MmD: "P  D sees_methods MmD"
     and Mm: "Mm = (λa. map_option (case_prod (λ(b, Ts, T, m). Pair (b, Ts, T, f b m))) (MmD a))"
    by(clarsimp simp:compC_def)

  let ?Mm = "MmD ++ (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 MmD] by simp
  ultimately show ?case by fast
qed
(*>*)


lemma sees_method_compPD:
  "compP f P  C sees M,b: TsT = fm in D 
  m. P  C sees M,b: TsT = m in D  f b m = fm"
(*<*)
proof -
  assume "compP f P  C sees M,b: TsT = 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 wf1 P C (M,b,Ts,T,m); P  C sees M,b:TsT = m in C 
      wf_mdecl wf2 (compP f P) C (M,b,Ts,T, f b m);
    xset P. wf_cdecl wf1 P x; x  set (compP f P); wf_prog p P 
   wf_cdecl wf2 (compP f P) x"
(*<*)
proof -
  assume
   wfm: "C M b Ts T m.  wf_mdecl wf1 P C (M,b,Ts,T,m); P  C sees M,b:TsT = m in C 
      wf_mdecl wf2 (compP f P) C (M,b,Ts,T, f b m)"
    and wfc: "xset P. wf_cdecl wf1 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 wf1 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 wf1 P C (M, b, Ts, T, m)" using wfc'
      by(simp add:wf_cdecl_def)
    moreover have cM: "P  C sees M, b :  TsT = m in C" using M
      by(rule mdecl_visible[OF wf x_set])
    ultimately have "wf_mdecl wf2 (compP f P) C (M, b, Ts, T, f b m)"
      by(rule wfm)
  }
  then have "m  ?ms. wf_mdecl wf2 ?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 "(fset 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:TsT = m in C; wf_mdecl wf1 P C (M,b,Ts,T,m) 
     wf_mdecl wf2 (compP f P) C (M,b,Ts,T, f b m)"
and wf: "wf_prog wf1 P"
shows "wf_prog wf2 (compP f P)"
(*<*)
using wf
by (simp add:wf_prog_def) (blast intro:wf_cdecl_compPI lift wf)
(*>*)


end