Theory Compiler1

(*  Title:      Jinja/Compiler/Compiler1.thy
    ID:         $Id: Compiler1.thy,v 1.4 2008-11-06 15:48:09 nipkow Exp $
    Author:     Tobias Nipkow
    Copyright   TUM 2003
*)

header {* \isaheader{Compilation Stage 1} *}

theory Compiler1 imports PCompiler J1 ListIndex begin

text{* Replacing variable names by indices. *}

consts
  compE1  :: "vname list => expr      => expr1"
  compEs1 :: "vname list => expr list => expr1 list"

primrec
"compE1 Vs (new C) = new C"
"compE1 Vs (Cast C e) = Cast C (compE1 Vs e)"
"compE1 Vs (Val v) = Val v"
"compE1 Vs (e1 «bop» e2) = (compE1 Vs e1) «bop» (compE1 Vs e2)"
"compE1 Vs (Var V) = Var(index Vs V)"
"compE1 Vs (V:=e) = (index Vs V):= (compE1 Vs e)"
"compE1 Vs (e•F{D}) = (compE1 Vs e)•F{D}"
"compE1 Vs (e1•F{D}:=e2) = (compE1 Vs e1)•F{D} := (compE1 Vs e2)"
"compE1 Vs (e•M(es)) = (compE1 Vs e)•M(compEs1 Vs es)"
"compE1 Vs {V:T; e} = {(size Vs):T; compE1 (Vs@[V]) e}"
"compE1 Vs (e1;;e2) = (compE1 Vs e1);;(compE1 Vs e2)"
"compE1 Vs (if (e) e1 else e2) = if (compE1 Vs e) (compE1 Vs e1) else (compE1 Vs e2)"
"compE1 Vs (while (e) c) = while (compE1 Vs e) (compE1 Vs c)"
"compE1 Vs (throw e) = throw (compE1 Vs e)"
"compE1 Vs (try e1 catch(C V) e2) =
    try(compE1 Vs e1) catch(C (size Vs)) (compE1 (Vs@[V]) e2)"

"compEs1 Vs []     = []"
"compEs1 Vs (e#es) = compE1 Vs e # compEs1 Vs es"

lemma [simp]: "compEs1 Vs es = map (compE1 Vs) es"
(*<*)by(induct es type:list) simp_all(*>*)


consts
  fin1:: "expr => expr1"
primrec
  "fin1(Val v) = Val v"
  "fin1(throw e) = throw(fin1 e)"

lemma comp_final: "final e ==> compE1 Vs e = fin1 e"
(*<*)by(erule finalE, simp_all)(*>*)


lemma [simp]:
      "!!Vs. max_vars (compE1 Vs e) = max_vars e"
and "!!Vs. max_varss (compEs1 Vs es) = max_varss es"
(*<*)by (induct e and es) simp_all(*>*)


text{* Compiling programs: *}

constdefs
  compP1 :: "J_prog => J1_prog"
  "compP1  ≡  compP (λ(pns,body). compE1 (this#pns) body)"

(*<*)
declare compP1_def[simp]
(*>*)

end