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