src/HOL/MicroJava/Comp/TranslCompTp.thy
author wenzelm
Thu Jul 23 22:13:42 2015 +0200 (2015-07-23)
changeset 60773 d09c66a0ea10
parent 60304 3f429b7d8eb5
permissions -rw-r--r--
more symbols by default, without xsymbols mode;
     1 (*  Title:      HOL/MicroJava/Comp/TranslCompTp.thy
     2     Author:     Martin Strecker
     3 *)
     4 
     5 theory TranslCompTp
     6 imports Index "../BV/JVMType"
     7 begin
     8 
     9 (**********************************************************************)
    10 
    11 definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"
    12   (infixr "\<box>" 55)
    13 where 
    14   "comb == (\<lambda> f1 f2 x0. let (xs1, x1) = f1 x0; 
    15                             (xs2, x2) = f2 x1 
    16                         in  (xs1 @ xs2, x2))"
    17 
    18 definition comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a" where
    19   "comb_nil a == ([], a)"
    20 
    21 lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
    22   by (simp add: comb_def comb_nil_def split_beta)
    23 
    24 lemma comb_nil_right [simp]: "f \<box> comb_nil = f"
    25   by (simp add: comb_def comb_nil_def split_beta)
    26 
    27 lemma comb_assoc [simp]: "(fa \<box> fb) \<box> fc = fa \<box> (fb \<box> fc)"
    28   by (simp add: comb_def split_beta)
    29 
    30 lemma comb_inv:
    31   "(xs', x') = (f1 \<box> f2) x0 \<Longrightarrow>
    32   \<exists>xs1 x1 xs2 x2. (xs1, x1) = (f1 x0) \<and> (xs2, x2) = f2 x1 \<and> xs'= xs1 @ xs2 \<and> x'=x2"
    33   by (case_tac "f1 x0") (simp add: comb_def split_beta)
    34 
    35 (**********************************************************************)
    36 
    37 abbreviation (input)
    38   mt_of :: "method_type \<times> state_type \<Rightarrow> method_type"
    39   where "mt_of == fst"
    40 
    41 abbreviation (input)
    42   sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
    43   where "sttp_of == snd"
    44 
    45 definition nochangeST :: "state_type \<Rightarrow> method_type \<times> state_type" where
    46   "nochangeST sttp == ([Some sttp], sttp)"
    47 
    48 definition pushST :: "[ty list, state_type] \<Rightarrow> method_type \<times> state_type" where
    49   "pushST tps == (\<lambda> (ST, LT). ([Some (ST, LT)], (tps @ ST, LT)))"
    50 
    51 definition dupST :: "state_type \<Rightarrow> method_type \<times> state_type" where
    52   "dupST == (\<lambda> (ST, LT). ([Some (ST, LT)], (hd ST # ST, LT)))"
    53 
    54 definition dup_x1ST :: "state_type \<Rightarrow> method_type \<times> state_type" where
    55   "dup_x1ST == (\<lambda> (ST, LT). ([Some (ST, LT)], 
    56                              (hd ST # hd (tl ST) # hd ST # (tl (tl ST)), LT)))"
    57 
    58 definition popST :: "[nat, state_type] \<Rightarrow> method_type \<times> state_type" where
    59   "popST n == (\<lambda> (ST, LT). ([Some (ST, LT)], (drop n ST, LT)))"
    60 
    61 definition replST :: "[nat, ty, state_type] \<Rightarrow> method_type \<times> state_type" where
    62   "replST n tp == (\<lambda> (ST, LT). ([Some (ST, LT)], (tp # (drop n ST), LT)))"
    63 
    64 definition storeST :: "[nat, ty, state_type] \<Rightarrow> method_type \<times> state_type" where
    65   "storeST i tp == (\<lambda> (ST, LT). ([Some (ST, LT)], (tl ST, LT [i:= OK tp])))"
    66 
    67 
    68 (* Expressions *)
    69 
    70 primrec compTpExpr :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr \<Rightarrow>
    71     state_type \<Rightarrow> method_type \<times> state_type"
    72   and compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list \<Rightarrow>
    73     state_type \<Rightarrow> method_type \<times> state_type"
    74 where
    75   "compTpExpr jmb G (NewC c) = pushST [Class c]"
    76 | "compTpExpr jmb G (Cast c e) = (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
    77 | "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
    78 | "compTpExpr jmb G (BinOp bo e1 e2) =
    79      (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> 
    80      (case bo of 
    81        Eq => popST 2 \<box> pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]
    82      | Add => replST 2 (PrimT Integer))"
    83 | "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT). 
    84       pushST [ok_val (LT ! (index jmb vn))] (ST, LT))"
    85 | "compTpExpr jmb G (vn::=e) = 
    86       (compTpExpr jmb G e) \<box> dupST \<box> (popST 1)"
    87 | "compTpExpr jmb G ( {cn}e..fn ) = 
    88       (compTpExpr jmb G e) \<box> replST 1 (snd (the (field (G,cn) fn)))"
    89 | "compTpExpr jmb G (FAss cn e1 fn e2 ) = 
    90       (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> dup_x1ST \<box> (popST 2)"
    91 | "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
    92        (compTpExpr jmb G a) \<box> (compTpExprs jmb G ps) \<box> 
    93        (replST ((length ps) + 1) (method_rT (the (method (G,C) (mn,fpTs)))))"
    94 | "compTpExprs jmb G [] = comb_nil"
    95 | "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
    96 
    97 
    98 (* Statements *)
    99 primrec compTpStmt :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt \<Rightarrow> 
   100     state_type \<Rightarrow> method_type \<times> state_type"
   101 where
   102   "compTpStmt jmb G Skip = comb_nil"
   103 | "compTpStmt jmb G (Expr e) =  (compTpExpr jmb G e) \<box> popST 1"
   104 | "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
   105 | "compTpStmt jmb G (If(e) c1 Else c2) = 
   106       (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
   107       (compTpStmt jmb G c1) \<box> nochangeST \<box> (compTpStmt jmb G c2)"
   108 | "compTpStmt jmb G (While(e) c) = 
   109       (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
   110       (compTpStmt jmb G c) \<box> nochangeST"
   111 
   112 definition compTpInit :: "java_mb \<Rightarrow> (vname * ty)
   113                    \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type" where
   114   "compTpInit jmb == (\<lambda> (vn,ty). (pushST [ty]) \<box>  (storeST (index jmb vn) ty))"
   115 
   116 primrec compTpInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow>
   117     state_type \<Rightarrow> method_type \<times> state_type"
   118 where
   119   "compTpInitLvars jmb [] = comb_nil"
   120 | "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
   121 
   122 definition start_ST :: "opstack_type" where
   123   "start_ST == []"
   124 
   125 definition start_LT :: "cname \<Rightarrow> ty list \<Rightarrow> nat \<Rightarrow> locvars_type" where
   126   "start_LT C pTs n ==  (OK (Class C))#((map OK pTs))@(replicate n Err)"
   127 
   128 definition compTpMethod  :: "[java_mb prog, cname, java_mb mdecl] \<Rightarrow> method_type" where
   129   "compTpMethod G C == \<lambda> ((mn,pTs),rT, jmb). 
   130                          let (pns,lvars,blk,res) = jmb
   131                          in (mt_of
   132                             ((compTpInitLvars jmb lvars \<box> 
   133                               compTpStmt jmb G blk \<box> 
   134                               compTpExpr jmb G res \<box>
   135                               nochangeST)
   136                                 (start_ST, start_LT C pTs (length lvars))))"
   137 
   138 definition compTp :: "java_mb prog => prog_type" where
   139   "compTp G C sig == let (D, rT, jmb) = (the (method (G, C) sig))
   140                       in compTpMethod G C (sig, rT, jmb)"
   141 
   142 
   143 
   144 (**********************************************************************)
   145   (* Computing the maximum stack size from the method_type *)
   146 
   147 definition ssize_sto :: "(state_type option) \<Rightarrow> nat" where
   148   "ssize_sto sto ==  case sto of None \<Rightarrow> 0 | (Some (ST, LT)) \<Rightarrow> length ST"
   149 
   150 definition max_of_list :: "nat list \<Rightarrow> nat" where
   151   "max_of_list xs == foldr max xs 0"
   152 
   153 definition max_ssize :: "method_type \<Rightarrow> nat" where
   154   "max_ssize mt == max_of_list (map ssize_sto mt)"
   155 
   156 end