Quelle  TranslCompTp.thy

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

theory TranslCompTp
imports Index "../BV/JVMType"
begin

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

definition comb :: "['a ==> 'b list × 'c, 'c ==> 'b list × 'd, 'a] ==> 'b list × 'd"
  (infixr ‹◻› 55)
where 
  "comb == (λ f1 f2 x0. let (xs1, x1) = f1 x0;
                            (xs2, x2) = f2 x1
                        in (xs1 @ xs2, x2))"

definition comb_nil :: "'a ==> 'b list × 'a" where
  "comb_nil a == ([], a)"

lemma comb_nil_left [simp]: "comb_nil ◻ f = f"
  by (simp add: comb_def comb_nil_def split_beta)

lemma comb_nil_right [simp]: "f ◻ comb_nil = f"
  by (simp add: comb_def comb_nil_def split_beta)

lemma comb_assoc [simp]: "(fa ◻ fb) ◻ fc = fa ◻ (fb ◻ fc)"
  by (simp add: comb_def split_beta)

lemma comb_inv:
  "(xs', x') = (f1 ◻ f2) x0 ==>
  ∃xs1 x1 xs2 x2. (xs1, x1) = (f1 x0) ∧ (xs2, x2) = f2 x1 ∧ xs'= xs1 @ xs2 ∧ x'=x2"
  by (case_tac "f1 x0") (simp add: comb_def split_beta)

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

abbreviation (input)
  mt_of :: "method_type × state_type ==> method_type"
  where "mt_of == fst"

abbreviation (input)
  sttp_of :: "method_type × state_type ==> state_type"
  where "sttp_of == snd"

definition nochangeST :: "state_type ==> method_type × state_type" where
  "nochangeST sttp == ([Some sttp], sttp)"

definition pushST :: "[ty list, state_type] ==> method_type × state_type" where
  "pushST tps == (λ (ST, LT). ([Some (ST, LT)], (tps @ ST, LT)))"

definition dupST :: "state_type ==> method_type × state_type" where
  "dupST == (λ (ST, LT). ([Some (ST, LT)], (hd ST # ST, LT)))"

definition dup_x1ST :: "state_type ==> method_type × state_type" where
  "dup_x1ST == (λ (ST, LT). ([Some (ST, LT)],
                             (hd ST # hd (tl ST) # hd ST # (tl (tl ST)), LT)))"

definition popST :: "[nat, state_type] ==> method_type × state_type" where
  "popST n == (λ (ST, LT). ([Some (ST, LT)], (drop n ST, LT)))"

definition replST :: "[nat, ty, state_type] ==> method_type × state_type" where
  "replST n tp == (λ (ST, LT). ([Some (ST, LT)], (tp # (drop n ST), LT)))"

definition storeST :: "[nat, ty, state_type] ==> method_type × state_type" where
  "storeST i tp == (λ (ST, LT). ([Some (ST, LT)], (tl ST, LT [i:= OK tp])))"


(* Expressions *)

primrec compTpExpr :: "java_mb ==> java_mb prog ==> expr ==>
    state_type ==> method_type × state_type"
  and compTpExprs :: "java_mb ==> java_mb prog ==> expr list ==>
    state_type ==> method_type × state_type"
where
  "compTpExpr jmb G (NewC c) = pushST [Class c]"
| "compTpExpr jmb G (Cast c e) = (compTpExpr jmb G e) ◻ (replST 1 (Class c))"
| "compTpExpr jmb G (Lit val) = pushST [the (typeof (λv. None) val)]"
| "compTpExpr jmb G (BinOp bo e1 e2) =
     (compTpExpr jmb G e1) ◻ (compTpExpr jmb G e2) ◻
     (case bo of
       Eq => popST 2 ◻ pushST [PrimT Boolean] ◻ popST 1 ◻ pushST [PrimT Boolean]
     | Add => replST 2 (PrimT Integer))"
| "compTpExpr jmb G (LAcc vn) = (λ (ST, LT).
      pushST [ok_val (LT ! (index jmb vn))] (ST, LT))"
| "compTpExpr jmb G (vn::=e) =
      (compTpExpr jmb G e) ◻ dupST ◻ (popST 1)"
| "compTpExpr jmb G ( {cn}e..fn ) =
      (compTpExpr jmb G e) ◻ replST 1 (snd (the (field (G,cn) fn)))"
| "compTpExpr jmb G (FAss cn e1 fn e2 ) =
      (compTpExpr jmb G e1) ◻ (compTpExpr jmb G e2) ◻ dup_x1ST ◻ (popST 2)"
| "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
       (compTpExpr jmb G a) ◻ (compTpExprs jmb G ps) ◻
       (replST ((length ps) + 1) (method_rT (the (method (G,C) (mn,fpTs)))))"
| "compTpExprs jmb G [] = comb_nil"
| "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) ◻ (compTpExprs jmb G es)"


(* Statements *)
primrec compTpStmt :: "java_mb ==> java_mb prog ==> stmt ==>
    state_type ==> method_type × state_type"
where
  "compTpStmt jmb G Skip = comb_nil"
| "compTpStmt jmb G (Expr e) = (compTpExpr jmb G e) ◻ popST 1"
| "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) ◻ (compTpStmt jmb G c2)"
| "compTpStmt jmb G (If(e) c1 Else c2) =
      (pushST [PrimT Boolean]) ◻ (compTpExpr jmb G e) ◻ popST 2 ◻
      (compTpStmt jmb G c1) ◻ nochangeST ◻ (compTpStmt jmb G c2)"
| "compTpStmt jmb G (While(e) c) =
      (pushST [PrimT Boolean]) ◻ (compTpExpr jmb G e) ◻ popST 2 ◻
      (compTpStmt jmb G c) ◻ nochangeST"

definition compTpInit :: "java_mb ==> (vname * ty)
                   ==> state_type ==> method_type × state_type" where
  "compTpInit jmb == (λ (vn,ty). (pushST [ty]) ◻ (storeST (index jmb vn) ty))"

primrec compTpInitLvars :: "[java_mb, (vname × ty) list] ==>
    state_type ==> method_type × state_type"
where
  "compTpInitLvars jmb [] = comb_nil"
| "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) ◻ (compTpInitLvars jmb lvars)"

definition start_ST :: "opstack_type" where
  "start_ST == []"

definition start_LT :: "cname ==> ty list ==> nat ==> locvars_type" where
  "start_LT C pTs n == (OK (Class C))#((map OK pTs))@(replicate n Err)"

definition compTpMethod  :: "[java_mb prog, cname, java_mb mdecl] ==> method_type" where
  "compTpMethod G C == λ ((mn,pTs),rT, jmb).
                         let (pns,lvars,blk,res) = jmb
                         in (mt_of
                            ((compTpInitLvars jmb lvars ◻
                              compTpStmt jmb G blk ◻
                              compTpExpr jmb G res ◻
                              nochangeST)
                                (start_ST, start_LT C pTs (length lvars))))"

definition compTp :: "java_mb prog => prog_type" where
  "compTp G C sig == let (D, rT, jmb) = (the (method (G, C) sig))
                      in compTpMethod G C (sig, rT, jmb)"



(**********************************************************************)
  (* Computing the maximum stack size from the method_type *)

definition ssize_sto :: "(state_type option) ==> nat" where
  "ssize_sto sto == case sto of None ==> 0 | (Some (ST, LT)) ==> length ST"

definition max_of_list :: "nat list ==> nat" where
  "max_of_list xs == foldr max xs 0"

definition max_ssize :: "method_type ==> nat" where
  "max_ssize mt == max_of_list (map ssize_sto mt)"

end