Theory Compiler1

(*  Title:      Jinja/Compiler/Compiler1.thy
    Author:     Tobias Nipkow
    Copyright   TUM 2003
*)

header {* \isaheader{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 (e⇣1•F{D}:=e⇣2) = (compE⇣1 Vs e⇣1)•F{D} := (compE⇣1 Vs e⇣2)"
| "compE⇣1 Vs (e•M(es)) = (compE⇣1 Vs e)•M(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)"

| "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(*>*)


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) simp_all(*>*)


text{* Compiling programs: *}

definition compP⇣1 :: "J_prog => J⇣1_prog"
where
  "compP⇣1  ≡  compP (λ(pns,body). compE⇣1 (this#pns) body)"

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

end