src/HOL/MicroJava/Comp/TranslComp.thy

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

(*  Title:      HOL/MicroJava/Comp/TranslComp.thy
    Author:     Martin Strecker
*)

(* Compiling MicroJava into MicroJVM -- Translation functions *)

theory TranslComp imports  TranslCompTp begin


(* parameter java_mb only serves to define function index later *)


(**********************************************************************)
(** code generation for expressions **)

primrec compExpr :: "java_mb => expr => instr list"
  and compExprs :: "java_mb => expr list => instr list"
where

(*class instance creation*)
"compExpr jmb (NewC c) = [New c]" |

(*type cast*)
"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" |


(*literals*)
"compExpr jmb (Lit val) = [LitPush val]" |

      
(* binary operation *)                         
"compExpr jmb (BinOp bo e1 e2) = compExpr jmb e1 @ compExpr jmb e2 @ 
  (case bo of Eq => [Ifcmpeq 3,LitPush(Bool False),Goto 2,LitPush(Bool True)]
            | Add => [IAdd])" |

(*local variable*)
"compExpr jmb (LAcc vn) = [Load (index jmb vn)]" |


(*assignement*)
"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" |


(*field access*)
"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]" |


(*field assignement - expected syntax:  {_}_.._:=_ *)
"compExpr jmb (FAss cn e1 fn e2 ) = 
       compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]" |


(*method call*)
"compExpr jmb (Call cn e1 mn X ps) = 
        compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]" |


(** code generation expression lists **)

"compExprs jmb []     = []" |

"compExprs jmb (e#es) = compExpr jmb e @ compExprs jmb es"


primrec compStmt :: "java_mb => stmt => instr list" where

(** code generation for statements **)

"compStmt jmb Skip = []" |

"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])" |

"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))" |

"compStmt jmb (If(e) c1 Else c2) =
        (let cnstf = LitPush (Bool False);
             cnd   = compExpr jmb e;
             thn   = compStmt jmb c1;
             els   = compStmt jmb c2;
             test  = Ifcmpeq (int(length thn +2)); 
             thnex = Goto (int(length els +1))
         in
         [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)" |

"compStmt jmb (While(e) c) =
        (let cnstf = LitPush (Bool False);
             cnd   = compExpr jmb e;
             bdy   = compStmt jmb c;
             test  = Ifcmpeq (int(length bdy +2)); 
             loop  = Goto (-(int((length bdy) + (length cnd) +2)))
         in
         [cnstf] @ cnd @ [test] @ bdy @ [loop])"

(**********************************************************************)

(*compiling methods, classes and programs*) 

(*initialising a single variable*)
definition load_default_val :: "ty => instr" where
"load_default_val ty == LitPush (default_val ty)"

definition compInit :: "java_mb => (vname * ty) => instr list" where
"compInit jmb == \<lambda> (vn,ty). [load_default_val ty, Store (index jmb vn)]"

definition compInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow> bytecode" where
 "compInitLvars jmb lvars == concat (map (compInit jmb) lvars)"

definition compMethod :: "java_mb prog \<Rightarrow> cname \<Rightarrow> java_mb mdecl \<Rightarrow> jvm_method mdecl" where
  "compMethod G C jmdl == let (sig, rT, jmb) = jmdl;
                        (pns,lvars,blk,res) = jmb;
                        mt = (compTpMethod G C jmdl);
                        bc = compInitLvars jmb lvars @ 
                             compStmt jmb blk @ compExpr jmb res @
                             [Return]
                  in (sig, rT, max_ssize mt, length lvars, bc, [])"

definition compClass :: "java_mb prog => java_mb cdecl=> jvm_method cdecl" where
  "compClass G == \<lambda> (C,cno,fdls,jmdls). (C,cno,fdls, map (compMethod G C) jmdls)"

definition comp :: "java_mb prog => jvm_prog" where
  "comp G == map (compClass G) G"

end