|
1 (* Title: HOL/MicroJava/Comp/TranslComp.thy |
|
2 ID: $Id$ |
|
3 Author: Martin Strecker |
|
4 Copyright GPL 2002 |
|
5 *) |
|
6 |
|
7 (* Compiling MicroJava into MicroJVM -- Translation functions *) |
|
8 |
|
9 theory TranslComp = TranslCompTp: |
|
10 |
|
11 |
|
12 (* parameter java_mb only serves to define function index later *) |
|
13 consts |
|
14 compExpr :: "java_mb => expr => instr list" |
|
15 compExprs :: "java_mb => expr list => instr list" |
|
16 compStmt :: "java_mb => stmt => instr list" |
|
17 |
|
18 |
|
19 |
|
20 (**********************************************************************) |
|
21 (** code generation for expressions **) |
|
22 |
|
23 primrec |
|
24 (*class instance creation*) |
|
25 "compExpr jmb (NewC c) = [New c]" |
|
26 |
|
27 (*type cast*) |
|
28 "compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" |
|
29 |
|
30 |
|
31 (*literals*) |
|
32 "compExpr jmb (Lit val) = [LitPush val]" |
|
33 |
|
34 |
|
35 (* binary operation *) |
|
36 "compExpr jmb (BinOp bo e1 e2) = compExpr jmb e1 @ compExpr jmb e2 @ |
|
37 (case bo of Eq => [Ifcmpeq 3,LitPush(Bool False),Goto 2,LitPush(Bool True)] |
|
38 | Add => [IAdd])" |
|
39 |
|
40 (*local variable*) |
|
41 "compExpr jmb (LAcc vn) = [Load (index jmb vn)]" |
|
42 |
|
43 |
|
44 (*assignement*) |
|
45 "compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" |
|
46 |
|
47 |
|
48 (*field access*) |
|
49 "compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]" |
|
50 |
|
51 |
|
52 (*field assignement - expected syntax: {_}_.._:=_ *) |
|
53 "compExpr jmb (FAss cn e1 fn e2 ) = |
|
54 compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]" |
|
55 |
|
56 |
|
57 (*method call*) |
|
58 "compExpr jmb (Call cn e1 mn X ps) = |
|
59 compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]" |
|
60 |
|
61 |
|
62 (** code generation expression lists **) |
|
63 |
|
64 "compExprs jmb [] = []" |
|
65 |
|
66 "compExprs jmb (e#es) = compExpr jmb e @ compExprs jmb es" |
|
67 |
|
68 |
|
69 |
|
70 primrec |
|
71 (** code generation for statements **) |
|
72 |
|
73 "compStmt jmb Skip = []" |
|
74 |
|
75 "compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])" |
|
76 |
|
77 "compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))" |
|
78 |
|
79 "compStmt jmb (If(e) c1 Else c2) = |
|
80 (let cnstf = LitPush (Bool False); |
|
81 cnd = compExpr jmb e; |
|
82 thn = compStmt jmb c1; |
|
83 els = compStmt jmb c2; |
|
84 test = Ifcmpeq (int(length thn +2)); |
|
85 thnex = Goto (int(length els +1)) |
|
86 in |
|
87 [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)" |
|
88 |
|
89 "compStmt jmb (While(e) c) = |
|
90 (let cnstf = LitPush (Bool False); |
|
91 cnd = compExpr jmb e; |
|
92 bdy = compStmt jmb c; |
|
93 test = Ifcmpeq (int(length bdy +2)); |
|
94 loop = Goto (-(int((length bdy) + (length cnd) +2))) |
|
95 in |
|
96 [cnstf] @ cnd @ [test] @ bdy @ [loop])" |
|
97 |
|
98 (**********************************************************************) |
|
99 |
|
100 (*compiling methods, classes and programs*) |
|
101 |
|
102 (*initialising a single variable*) |
|
103 constdefs |
|
104 load_default_val :: "ty => instr" |
|
105 "load_default_val ty == LitPush (default_val ty)" |
|
106 |
|
107 compInit :: "java_mb => (vname * ty) => instr list" |
|
108 "compInit jmb == \<lambda> (vn,ty). [load_default_val ty, Store (index jmb vn)]" |
|
109 |
|
110 compInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow> bytecode" |
|
111 "compInitLvars jmb lvars == concat (map (compInit jmb) lvars)" |
|
112 |
|
113 compMethod :: "java_mb prog \<Rightarrow> cname \<Rightarrow> java_mb mdecl \<Rightarrow> jvm_method mdecl" |
|
114 "compMethod G C jmdl == let (sig, rT, jmb) = jmdl; |
|
115 (pns,lvars,blk,res) = jmb; |
|
116 mt = (compTpMethod G C jmdl); |
|
117 bc = compInitLvars jmb lvars @ |
|
118 compStmt jmb blk @ compExpr jmb res @ |
|
119 [Return] |
|
120 in (sig, rT, max_ssize mt, length lvars, bc, [])" |
|
121 |
|
122 compClass :: "java_mb prog => java_mb cdecl=> jvm_method cdecl" |
|
123 "compClass G == \<lambda> (C,cno,fdls,jmdls). (C,cno,fdls, map (compMethod G C) jmdls)" |
|
124 |
|
125 comp :: "java_mb prog => jvm_prog" |
|
126 "comp G == map (compClass G) G" |
|
127 |
|
128 end |
|
129 |
|
130 |