1(*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
2    Author:     Stefan Berghofer
3*)
4
5section \<open>Example for generating executable code from JVM semantics \label{sec:JVMListExample}\<close>
6
7theory JVMListExample
8imports "../J/SystemClasses" JVMExec
9begin
10
11text \<open>
12  Since the types @{typ cnam}, \<open>vnam\<close>, and \<open>mname\<close> are 
13  anonymous, we describe distinctness of names in the example by axioms:
14\<close>
15axiomatization list_nam test_nam :: cnam
16  where distinct_classes: "list_nam \<noteq> test_nam"
17
18axiomatization append_name makelist_name :: mname
19  where distinct_methods: "append_name \<noteq> makelist_name"
20
21axiomatization val_nam next_nam :: vnam
22  where distinct_fields: "val_nam \<noteq> next_nam"
23
24axiomatization
25  where nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
26
27definition list_name :: cname
28  where "list_name = Cname list_nam"
29  
30definition test_name :: cname
31  where "test_name = Cname test_nam"
32
33definition val_name :: vname
34  where "val_name = VName val_nam"
35
36definition next_name :: vname
37  where "next_name = VName next_nam"
38
39definition append_ins :: bytecode where
40  "append_ins =
41       [Load 0,
42        Getfield next_name list_name,
43        Dup,
44        LitPush Null,
45        Ifcmpeq 4,
46        Load 1,       
47        Invoke list_name append_name [Class list_name],
48        Return,
49        Pop,
50        Load 0,
51        Load 1,
52        Putfield next_name list_name,
53        LitPush Unit,
54        Return]"
55
56definition list_class :: "jvm_method class" where
57  "list_class =
58    (Object,
59     [(val_name, PrimT Integer), (next_name, Class list_name)],
60     [((append_name, [Class list_name]), PrimT Void,
61        (3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])"
62
63definition make_list_ins :: bytecode where
64  "make_list_ins =
65       [New list_name,
66        Dup,
67        Store 0,
68        LitPush (Intg 1),
69        Putfield val_name list_name,
70        New list_name,
71        Dup,
72        Store 1,
73        LitPush (Intg 2),
74        Putfield val_name list_name,
75        New list_name,
76        Dup,
77        Store 2,
78        LitPush (Intg 3),
79        Putfield val_name list_name,
80        Load 0,
81        Load 1,
82        Invoke list_name append_name [Class list_name],
83        Pop,
84        Load 0,
85        Load 2,
86        Invoke list_name append_name [Class list_name],
87        Return]"
88
89definition test_class :: "jvm_method class" where
90  "test_class =
91    (Object, [],
92     [((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])"
93
94definition E :: jvm_prog where
95  "E = SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
96
97code_datatype list_nam test_nam
98lemma equal_cnam_code [code]:
99  "HOL.equal list_nam list_nam \<longleftrightarrow> True"
100  "HOL.equal test_nam test_nam \<longleftrightarrow> True"
101  "HOL.equal list_nam test_nam \<longleftrightarrow> False"
102  "HOL.equal test_nam list_nam \<longleftrightarrow> False"
103  by(simp_all add: distinct_classes distinct_classes[symmetric] equal_cnam_def)
104
105code_datatype append_name makelist_name
106lemma equal_mname_code [code]: 
107  "HOL.equal append_name append_name \<longleftrightarrow> True"
108  "HOL.equal makelist_name makelist_name \<longleftrightarrow> True"
109  "HOL.equal append_name makelist_name \<longleftrightarrow> False"
110  "HOL.equal makelist_name append_name \<longleftrightarrow> False"
111  by(simp_all add: distinct_methods distinct_methods[symmetric] equal_mname_def)
112
113code_datatype val_nam next_nam
114lemma equal_vnam_code [code]: 
115  "HOL.equal val_nam val_nam \<longleftrightarrow> True"
116  "HOL.equal next_nam next_nam \<longleftrightarrow> True"
117  "HOL.equal val_nam next_nam \<longleftrightarrow> False"
118  "HOL.equal next_nam val_nam \<longleftrightarrow> False"
119  by(simp_all add: distinct_fields distinct_fields[symmetric] equal_vnam_def)
120
121
122lemma equal_loc'_code [code]:
123  "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'"
124  by(simp add: equal_loc'_def nat_to_loc'_inject)
125
126definition undefined_cname :: cname 
127  where [code del]: "undefined_cname = undefined"
128code_datatype Object Xcpt Cname undefined_cname
129declare undefined_cname_def[symmetric, code_unfold]
130
131definition undefined_val :: val
132  where [code del]: "undefined_val = undefined"
133declare undefined_val_def[symmetric, code_unfold]
134code_datatype Unit Null Bool Intg Addr undefined_val
135
136definition
137  "test = exec (E, start_state E test_name makelist_name)"
138
139ML_val \<open>
140  @{code test}; 
141  @{code exec} (@{code E}, @{code the} it);
142  @{code exec} (@{code E}, @{code the} it);
143  @{code exec} (@{code E}, @{code the} it);
144  @{code exec} (@{code E}, @{code the} it);
145  @{code exec} (@{code E}, @{code the} it);
146  @{code exec} (@{code E}, @{code the} it);
147  @{code exec} (@{code E}, @{code the} it);
148  @{code exec} (@{code E}, @{code the} it);
149  @{code exec} (@{code E}, @{code the} it);
150  @{code exec} (@{code E}, @{code the} it);
151  @{code exec} (@{code E}, @{code the} it);
152  @{code exec} (@{code E}, @{code the} it);
153  @{code exec} (@{code E}, @{code the} it);
154  @{code exec} (@{code E}, @{code the} it);
155  @{code exec} (@{code E}, @{code the} it);
156  @{code exec} (@{code E}, @{code the} it);
157  @{code exec} (@{code E}, @{code the} it);
158  @{code exec} (@{code E}, @{code the} it);
159  @{code exec} (@{code E}, @{code the} it);
160  @{code exec} (@{code E}, @{code the} it);
161  @{code exec} (@{code E}, @{code the} it);
162  @{code exec} (@{code E}, @{code the} it);
163  @{code exec} (@{code E}, @{code the} it);
164  @{code exec} (@{code E}, @{code the} it);
165  @{code exec} (@{code E}, @{code the} it);
166  @{code exec} (@{code E}, @{code the} it);
167  @{code exec} (@{code E}, @{code the} it);
168  @{code exec} (@{code E}, @{code the} it);
169  @{code exec} (@{code E}, @{code the} it);
170  @{code exec} (@{code E}, @{code the} it);
171  @{code exec} (@{code E}, @{code the} it);
172  @{code exec} (@{code E}, @{code the} it);
173  @{code exec} (@{code E}, @{code the} it);
174  @{code exec} (@{code E}, @{code the} it);
175  @{code exec} (@{code E}, @{code the} it);
176  @{code exec} (@{code E}, @{code the} it);
177  @{code exec} (@{code E}, @{code the} it);
178  @{code exec} (@{code E}, @{code the} it);
179  @{code exec} (@{code E}, @{code the} it);
180  @{code exec} (@{code E}, @{code the} it);
181  @{code exec} (@{code E}, @{code the} it);
182  @{code exec} (@{code E}, @{code the} it);
183  @{code exec} (@{code E}, @{code the} it);
184  @{code exec} (@{code E}, @{code the} it);
185  @{code exec} (@{code E}, @{code the} it);
186  @{code exec} (@{code E}, @{code the} it);
187  @{code exec} (@{code E}, @{code the} it);
188  @{code exec} (@{code E}, @{code the} it);
189  @{code exec} (@{code E}, @{code the} it);
190  @{code exec} (@{code E}, @{code the} it);
191  @{code exec} (@{code E}, @{code the} it);
192  @{code exec} (@{code E}, @{code the} it);
193  @{code exec} (@{code E}, @{code the} it);
194\<close>
195
196end
197