Theory Compiler1

(*  Title:      JinjaDCI/Compiler/Compiler1.thy
    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   TUM 2003, UIUC 2019-20

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

section ‹ Compilation Stage 1 ›

theory Compiler1 imports PCompiler J1 Hidden begin

text‹ Replacing variable names by indices. ›

primrec compE⇩1  :: "vname list ⇒ expr ⇒ expr⇩1"
  and compEs⇩1 :: "vname list ⇒ expr list ⇒ expr⇩1 list" where
  "compE⇩1 Vs (new C) = new C"
| "compE⇩1 Vs (Cast C e) = Cast C (compE⇩1 Vs e)"
| "compE⇩1 Vs (Val v) = Val v"
| "compE⇩1 Vs (e⇩1 «bop» e⇩2) = (compE⇩1 Vs e⇩1) «bop» (compE⇩1 Vs e⇩2)"
| "compE⇩1 Vs (Var V) = Var(last_index Vs V)"
| "compE⇩1 Vs (V:=e) = (last_index Vs V):= (compE⇩1 Vs e)"
| "compE⇩1 Vs (e∙F{D}) = (compE⇩1 Vs e)∙F{D}"
| "compE⇩1 Vs (C∙⇩sF{D}) = C∙⇩sF{D}"
| "compE⇩1 Vs (e⇩1∙F{D}:=e⇩2) = (compE⇩1 Vs e⇩1)∙F{D} := (compE⇩1 Vs e⇩2)"
| "compE⇩1 Vs (C∙⇩sF{D}:=e⇩2) = C∙⇩sF{D} := (compE⇩1 Vs e⇩2)"
| "compE⇩1 Vs (e∙M(es)) = (compE⇩1 Vs e)∙M(compEs⇩1 Vs es)"
| "compE⇩1 Vs (C∙⇩sM(es)) = C∙⇩sM(compEs⇩1 Vs es)"
| "compE⇩1 Vs {V:T; e} = {(size Vs):T; compE⇩1 (Vs@[V]) e}"
| "compE⇩1 Vs (e⇩1;;e⇩2) = (compE⇩1 Vs e⇩1);;(compE⇩1 Vs e⇩2)"
| "compE⇩1 Vs (if (e) e⇩1 else e⇩2) = if (compE⇩1 Vs e) (compE⇩1 Vs e⇩1) else (compE⇩1 Vs e⇩2)"
| "compE⇩1 Vs (while (e) c) = while (compE⇩1 Vs e) (compE⇩1 Vs c)"
| "compE⇩1 Vs (throw e) = throw (compE⇩1 Vs e)"
| "compE⇩1 Vs (try e⇩1 catch(C V) e⇩2) =
    try(compE⇩1 Vs e⇩1) catch(C (size Vs)) (compE⇩1 (Vs@[V]) e⇩2)"
| "compE⇩1 Vs (INIT C (Cs,b) ← e) = INIT C (Cs,b) ← (compE⇩1 Vs e)"
| "compE⇩1 Vs (RI(C,e);Cs ← e') = RI(C,(compE⇩1 Vs e));Cs ← (compE⇩1 Vs e')"

| "compEs⇩1 Vs []     = []"
| "compEs⇩1 Vs (e#es) = compE⇩1 Vs e # compEs⇩1 Vs es"

lemma [simp]: "compEs⇩1 Vs es = map (compE⇩1 Vs) es"
(*<*)by(induct es type:list) simp_all(*>*)

lemma [simp]: "⋀Vs. sub_RI (compE⇩1 Vs e) = sub_RI e"
 and [simp]: "⋀Vs. sub_RIs (compEs⇩1 Vs es) = sub_RIs es"
proof(induct rule: sub_RI_sub_RIs_induct) qed(auto)

primrec fin⇩1:: "expr ⇒ expr⇩1" where
  "fin⇩1(Val v) = Val v"
| "fin⇩1(throw e) = throw(fin⇩1 e)"

lemma comp_final: "final e ⟹ compE⇩1 Vs e = fin⇩1 e"
(*<*)by(erule finalE, simp_all)(*>*)


lemma [simp]:
      "⋀Vs. max_vars (compE⇩1 Vs e) = max_vars e"
and "⋀Vs. max_varss (compEs⇩1 Vs es) = max_varss es"
(*<*)by (induct e and es rule: max_vars.induct max_varss.induct) simp_all(*>*)


text‹ Compiling programs: ›

definition compP⇩1 :: "J_prog ⇒ J⇩1_prog"
where
  "compP⇩1  ≡  compP (λb (pns,body). compE⇩1 (case b of NonStatic ⇒ this#pns | Static ⇒ pns) body)"

(*<*)
declare compP⇩1_def[simp]
(*>*)

end