Theory Compiler2

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

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

theory Compiler2
imports PCompiler J1 "../JVM/JVMExec"
begin

primrec compE⇣2 :: "expr⇣1 => instr list"
  and compEs⇣2 :: "expr⇣1 list => instr list" where
  "compE⇣2 (new C) = [New C]"
| "compE⇣2 (Cast C e) = compE⇣2 e @ [Checkcast C]"
| "compE⇣2 (Val v) = [Push v]"
| "compE⇣2 (e⇣1 «bop» e⇣2) = compE⇣2 e⇣1 @ compE⇣2 e⇣2 @ 
  (case bop of Eq => [CmpEq]
            | Add => [IAdd])"
| "compE⇣2 (Var i) = [Load i]"
| "compE⇣2 (i:=e) = compE⇣2 e @ [Store i, Push Unit]"
| "compE⇣2 (e•F{D}) = compE⇣2 e @ [Getfield F D]"
| "compE⇣2 (e⇣1•F{D} := e⇣2) =
       compE⇣2 e⇣1 @ compE⇣2 e⇣2 @ [Putfield F D, Push Unit]"
| "compE⇣2 (e•M(es)) = compE⇣2 e @ compEs⇣2 es @ [Invoke M (size es)]"
| "compE⇣2 ({i:T; e}) = compE⇣2 e"
| "compE⇣2 (e⇣1;;e⇣2) = compE⇣2 e⇣1 @ [Pop] @ compE⇣2 e⇣2"
| "compE⇣2 (if (e) e⇣1 else e⇣2) =
        (let cnd   = compE⇣2 e;
             thn   = compE⇣2 e⇣1;
             els   = compE⇣2 e⇣2;
             test  = IfFalse (int(size thn + 2)); 
             thnex = Goto (int(size els + 1))
         in cnd @ [test] @ thn @ [thnex] @ els)"
| "compE⇣2 (while (e) c) =
        (let cnd   = compE⇣2 e;
             bdy   = compE⇣2 c;
             test  = IfFalse (int(size bdy + 3)); 
             loop  = Goto (-int(size bdy + size cnd + 2))
         in cnd @ [test] @ bdy @ [Pop] @ [loop] @ [Push Unit])"
| "compE⇣2 (throw e) = compE⇣2 e @ [instr.Throw]"
| "compE⇣2 (try e⇣1 catch(C i) e⇣2) =
   (let catch = compE⇣2 e⇣2
    in compE⇣2 e⇣1 @ [Goto (int(size catch)+2), Store i] @ catch)"

| "compEs⇣2 []     = []"
| "compEs⇣2 (e#es) = compE⇣2 e @ compEs⇣2 es"

text{* Compilation of exception table. Is given start address of code
to compute absolute addresses necessary in exception table. *}

primrec compxE⇣2  :: "expr⇣1      => pc => nat => ex_table"
  and compxEs⇣2 :: "expr⇣1 list => pc => nat => ex_table" where
  "compxE⇣2 (new C) pc d = []"
| "compxE⇣2 (Cast C e) pc d = compxE⇣2 e pc d"
| "compxE⇣2 (Val v) pc d = []"
| "compxE⇣2 (e⇣1 «bop» e⇣2) pc d =
   compxE⇣2 e⇣1 pc d @ compxE⇣2 e⇣2 (pc + size(compE⇣2 e⇣1)) (d+1)"
| "compxE⇣2 (Var i) pc d = []"
| "compxE⇣2 (i:=e) pc d = compxE⇣2 e pc d"
| "compxE⇣2 (e•F{D}) pc d = compxE⇣2 e pc d"
| "compxE⇣2 (e⇣1•F{D} := e⇣2) pc d =
   compxE⇣2 e⇣1 pc d @ compxE⇣2 e⇣2 (pc + size(compE⇣2 e⇣1)) (d+1)"
| "compxE⇣2 (e•M(es)) pc d =
   compxE⇣2 e pc d @ compxEs⇣2 es (pc + size(compE⇣2 e)) (d+1)"
| "compxE⇣2 ({i:T; e}) pc d = compxE⇣2 e pc d"
| "compxE⇣2 (e⇣1;;e⇣2) pc d =
   compxE⇣2 e⇣1 pc d @ compxE⇣2 e⇣2 (pc+size(compE⇣2 e⇣1)+1) d"
| "compxE⇣2 (if (e) e⇣1 else e⇣2) pc d =
        (let pc⇣1   = pc + size(compE⇣2 e) + 1;
             pc⇣2   = pc⇣1 + size(compE⇣2 e⇣1) + 1
         in compxE⇣2 e pc d @ compxE⇣2 e⇣1 pc⇣1 d @ compxE⇣2 e⇣2 pc⇣2 d)"
| "compxE⇣2 (while (b) e) pc d =
   compxE⇣2 b pc d @ compxE⇣2 e (pc+size(compE⇣2 b)+1) d"
| "compxE⇣2 (throw e) pc d = compxE⇣2 e pc d"
| "compxE⇣2 (try e⇣1 catch(C i) e⇣2) pc d =
   (let pc⇣1 = pc + size(compE⇣2 e⇣1)
    in compxE⇣2 e⇣1 pc d @ compxE⇣2 e⇣2 (pc⇣1+2) d @ [(pc,pc⇣1,C,pc⇣1+1,d)])"

| "compxEs⇣2 [] pc d    = []"
| "compxEs⇣2 (e#es) pc d = compxE⇣2 e pc d @ compxEs⇣2 es (pc+size(compE⇣2 e)) (d+1)"

primrec max_stack :: "expr⇣1 => nat"
  and max_stacks :: "expr⇣1 list => nat" where
  "max_stack (new C) = 1"
| "max_stack (Cast C e) = max_stack e"
| "max_stack (Val v) = 1"
| "max_stack (e⇣1 «bop» e⇣2) = max (max_stack e⇣1) (max_stack e⇣2) + 1"
| "max_stack (Var i) = 1"
| "max_stack (i:=e) = max_stack e"
| "max_stack (e•F{D}) = max_stack e"
| "max_stack (e⇣1•F{D} := e⇣2) = max (max_stack e⇣1) (max_stack e⇣2) + 1"
| "max_stack (e•M(es)) = max (max_stack e) (max_stacks es) + 1"
| "max_stack ({i:T; e}) = max_stack e"
| "max_stack (e⇣1;;e⇣2) = max (max_stack e⇣1) (max_stack e⇣2)"
| "max_stack (if (e) e⇣1 else e⇣2) =
  max (max_stack e) (max (max_stack e⇣1) (max_stack e⇣2))"
| "max_stack (while (e) c) = max (max_stack e) (max_stack c)"
| "max_stack (throw e) = max_stack e"
| "max_stack (try e⇣1 catch(C i) e⇣2) = max (max_stack e⇣1) (max_stack e⇣2)"
 
| "max_stacks [] = 0"
| "max_stacks (e#es) = max (max_stack e) (1 + max_stacks es)"

lemma max_stack1: "1 ≤ max_stack e"
(*<*)by(induct e) (simp_all add:max_def)(*>*)


definition compMb⇣2 :: "expr⇣1 => jvm_method"
where
  "compMb⇣2  ≡  λbody.
  let ins = compE⇣2 body @ [Return];
      xt = compxE⇣2 body 0 0
  in (max_stack body, max_vars body, ins, xt)"

definition compP⇣2 :: "J⇣1_prog => jvm_prog"
where
  "compP⇣2  ≡  compP compMb⇣2"

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

lemma compMb⇣2 [simp]:
  "compMb⇣2 e = (max_stack e, max_vars e, compE⇣2 e @ [Return], compxE⇣2 e 0 0)"
(*<*)by (simp add: compMb⇣2_def)(*>*)


end