src/HOL/MicroJava/Comp/TranslCompTp.thy
changeset 35416 d8d7d1b785af
parent 35102 cc7a0b9f938c
child 35417 47ee18b6ae32
     1.1 --- a/src/HOL/MicroJava/Comp/TranslCompTp.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -6,17 +6,14 @@
     1.4  imports Index "../BV/JVMType"
     1.5  begin
     1.6  
     1.7 -
     1.8 -
     1.9  (**********************************************************************)
    1.10  
    1.11 -
    1.12 -constdefs
    1.13 -  comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd" 
    1.14 +definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd" where 
    1.15    "comb == (\<lambda> f1 f2 x0. let (xs1, x1) = f1 x0; 
    1.16                              (xs2, x2) = f2 x1 
    1.17                          in  (xs1 @ xs2, x2))"
    1.18 -  comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a"
    1.19 +
    1.20 +definition comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a" where
    1.21    "comb_nil a == ([], a)"
    1.22  
    1.23  syntax (xsymbols)
    1.24 @@ -59,23 +56,26 @@
    1.25    compTpStmt  :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt
    1.26                     \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
    1.27  
    1.28 -
    1.29 -constdefs
    1.30 -  nochangeST :: "state_type \<Rightarrow> method_type \<times> state_type"
    1.31 +definition nochangeST :: "state_type \<Rightarrow> method_type \<times> state_type" where
    1.32    "nochangeST sttp == ([Some sttp], sttp)"
    1.33 -  pushST :: "[ty list, state_type] \<Rightarrow> method_type \<times> state_type"
    1.34 +
    1.35 +definition pushST :: "[ty list, state_type] \<Rightarrow> method_type \<times> state_type" where
    1.36    "pushST tps == (\<lambda> (ST, LT). ([Some (ST, LT)], (tps @ ST, LT)))"
    1.37 -  dupST :: "state_type \<Rightarrow> method_type \<times> state_type"
    1.38 +
    1.39 +definition dupST :: "state_type \<Rightarrow> method_type \<times> state_type" where
    1.40    "dupST == (\<lambda> (ST, LT). ([Some (ST, LT)], (hd ST # ST, LT)))"
    1.41 -  dup_x1ST :: "state_type \<Rightarrow> method_type \<times> state_type"
    1.42 +
    1.43 +definition dup_x1ST :: "state_type \<Rightarrow> method_type \<times> state_type" where
    1.44    "dup_x1ST == (\<lambda> (ST, LT). ([Some (ST, LT)], 
    1.45                               (hd ST # hd (tl ST) # hd ST # (tl (tl ST)), LT)))"
    1.46 -  popST :: "[nat, state_type] \<Rightarrow> method_type \<times> state_type"
    1.47 +
    1.48 +definition popST :: "[nat, state_type] \<Rightarrow> method_type \<times> state_type" where
    1.49    "popST n == (\<lambda> (ST, LT). ([Some (ST, LT)], (drop n ST, LT)))"
    1.50 -  replST :: "[nat, ty, state_type] \<Rightarrow> method_type \<times> state_type"
    1.51 +
    1.52 +definition replST :: "[nat, ty, state_type] \<Rightarrow> method_type \<times> state_type" where
    1.53    "replST n tp == (\<lambda> (ST, LT). ([Some (ST, LT)], (tp # (drop n ST), LT)))"
    1.54  
    1.55 -  storeST :: "[nat, ty, state_type] \<Rightarrow> method_type \<times> state_type"
    1.56 +definition storeST :: "[nat, ty, state_type] \<Rightarrow> method_type \<times> state_type" where
    1.57    "storeST i tp == (\<lambda> (ST, LT). ([Some (ST, LT)], (tl ST, LT [i:= OK tp])))"
    1.58  
    1.59  
    1.60 @@ -138,9 +138,8 @@
    1.61        (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
    1.62        (compTpStmt jmb G c) \<box> nochangeST"
    1.63  
    1.64 -constdefs
    1.65 -  compTpInit  :: "java_mb \<Rightarrow> (vname * ty)
    1.66 -                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
    1.67 +definition compTpInit :: "java_mb \<Rightarrow> (vname * ty)
    1.68 +                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type" where
    1.69    "compTpInit jmb == (\<lambda> (vn,ty). (pushST [ty]) \<box>  (storeST (index jmb vn) ty))"
    1.70  
    1.71  consts
    1.72 @@ -151,14 +150,13 @@
    1.73    "compTpInitLvars jmb [] = comb_nil"
    1.74    "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
    1.75  
    1.76 -constdefs
    1.77 -   start_ST :: "opstack_type"
    1.78 +definition start_ST :: "opstack_type" where
    1.79    "start_ST == []"
    1.80  
    1.81 -   start_LT :: "cname \<Rightarrow> ty list \<Rightarrow> nat \<Rightarrow> locvars_type"
    1.82 +definition start_LT :: "cname \<Rightarrow> ty list \<Rightarrow> nat \<Rightarrow> locvars_type" where
    1.83    "start_LT C pTs n ==  (OK (Class C))#((map OK pTs))@(replicate n Err)"
    1.84  
    1.85 -  compTpMethod  :: "[java_mb prog, cname, java_mb mdecl] \<Rightarrow> method_type"
    1.86 +definition compTpMethod  :: "[java_mb prog, cname, java_mb mdecl] \<Rightarrow> method_type" where
    1.87    "compTpMethod G C == \<lambda> ((mn,pTs),rT, jmb). 
    1.88                           let (pns,lvars,blk,res) = jmb
    1.89                           in (mt_of
    1.90 @@ -168,7 +166,7 @@
    1.91                                nochangeST)
    1.92                                  (start_ST, start_LT C pTs (length lvars))))"
    1.93  
    1.94 -  compTp :: "java_mb prog => prog_type"
    1.95 +definition compTp :: "java_mb prog => prog_type" where
    1.96    "compTp G C sig == let (D, rT, jmb) = (the (method (G, C) sig))
    1.97                        in compTpMethod G C (sig, rT, jmb)"
    1.98  
    1.99 @@ -177,15 +175,13 @@
   1.100  (**********************************************************************)
   1.101    (* Computing the maximum stack size from the method_type *)
   1.102  
   1.103 -constdefs
   1.104 -  ssize_sto :: "(state_type option) \<Rightarrow> nat"
   1.105 +definition ssize_sto :: "(state_type option) \<Rightarrow> nat" where
   1.106    "ssize_sto sto ==  case sto of None \<Rightarrow> 0 | (Some (ST, LT)) \<Rightarrow> length ST"
   1.107  
   1.108 -  max_of_list :: "nat list \<Rightarrow> nat"
   1.109 +definition max_of_list :: "nat list \<Rightarrow> nat" where
   1.110    "max_of_list xs == foldr max xs 0"
   1.111  
   1.112 -  max_ssize :: "method_type \<Rightarrow> nat"
   1.113 +definition max_ssize :: "method_type \<Rightarrow> nat" where
   1.114    "max_ssize mt == max_of_list (map ssize_sto mt)"
   1.115  
   1.116 -
   1.117  end