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