author | bulwahn |
Fri, 21 Oct 2011 11:17:14 +0200 | |
changeset 45231 | d85a2fdc586c |
parent 44037 | 25011c3a5c3d |
child 45827 | 66c68453455c |
permissions | -rw-r--r-- |
12951 | 1 |
(* Title: HOL/MicroJava/J/JListExample.thy |
12442 | 2 |
Author: Stefan Berghofer |
3 |
*) |
|
4 |
||
12911 | 5 |
header {* \isaheader{Example for generating executable code from Java semantics} *} |
12442 | 6 |
|
28524 | 7 |
theory JListExample |
32356
e11cd88e6ade
temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents:
28524
diff
changeset
|
8 |
imports Eval |
28524 | 9 |
begin |
12442 | 10 |
|
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
35416
diff
changeset
|
11 |
declare [[syntax_ambiguity_level = 100000]] |
12442 | 12 |
|
13 |
consts |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
14 |
list_nam :: cnam |
12442 | 15 |
append_name :: mname |
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
16 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
17 |
axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
18 |
where distinct_fields: "val_name \<noteq> next_name" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
19 |
and distinct_vars: |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
20 |
"l_nam \<noteq> l1_nam" "l_nam \<noteq> l2_nam" "l_nam \<noteq> l3_nam" "l_nam \<noteq> l4_nam" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
21 |
"l1_nam \<noteq> l2_nam" "l1_nam \<noteq> l3_nam" "l1_nam \<noteq> l4_nam" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
22 |
"l2_nam \<noteq> l3_nam" "l2_nam \<noteq> l4_nam" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
23 |
"l3_nam \<noteq> l4_nam" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
24 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
25 |
definition list_name :: cname where |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
26 |
"list_name = Cname list_nam" |
12442 | 27 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
28 |
definition val_name :: vname where |
12442 | 29 |
"val_name == VName val_nam" |
30 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
31 |
definition next_name :: vname where |
12442 | 32 |
"next_name == VName next_nam" |
33 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
34 |
definition l_name :: vname where |
12442 | 35 |
"l_name == VName l_nam" |
36 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
37 |
definition l1_name :: vname where |
12442 | 38 |
"l1_name == VName l1_nam" |
39 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
40 |
definition l2_name :: vname where |
12442 | 41 |
"l2_name == VName l2_nam" |
42 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
43 |
definition l3_name :: vname where |
12442 | 44 |
"l3_name == VName l3_nam" |
45 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
46 |
definition l4_name :: vname where |
12442 | 47 |
"l4_name == VName l4_nam" |
48 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
49 |
definition list_class :: "java_mb class" where |
12442 | 50 |
"list_class == |
51 |
(Object, |
|
52 |
[(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))], |
|
53 |
[((append_name, [RefT (ClassT list_name)]), PrimT Void, |
|
54 |
([l_name], [], |
|
55 |
If(BinOp Eq ({list_name}(LAcc This)..next_name) (Lit Null)) |
|
56 |
Expr ({list_name}(LAcc This)..next_name:=LAcc l_name) |
|
57 |
Else |
|
58 |
Expr ({list_name}({list_name}(LAcc This)..next_name).. |
|
59 |
append_name({[RefT (ClassT list_name)]}[LAcc l_name])), |
|
60 |
Lit Unit))])" |
|
61 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
62 |
definition example_prg :: "java_mb prog" where |
12442 | 63 |
"example_prg == [ObjectC, (list_name, list_class)]" |
64 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
65 |
code_datatype list_nam |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
66 |
lemma equal_cnam_code [code]: |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
67 |
"HOL.equal list_nam list_nam \<longleftrightarrow> True" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
68 |
by(simp add: equal_cnam_def) |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
69 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
70 |
code_datatype append_name |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
71 |
lemma equal_mname_code [code]: |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
72 |
"HOL.equal append_name append_name \<longleftrightarrow> True" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
73 |
by(simp add: equal_mname_def) |
12442 | 74 |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
75 |
code_datatype val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
76 |
lemma equal_vnam_code [code]: |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
77 |
"HOL.equal val_nam val_nam \<longleftrightarrow> True" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
78 |
"HOL.equal next_nam next_nam \<longleftrightarrow> True" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
79 |
"HOL.equal l_nam l_nam \<longleftrightarrow> True" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
80 |
"HOL.equal l1_nam l1_nam \<longleftrightarrow> True" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
81 |
"HOL.equal l2_nam l2_nam \<longleftrightarrow> True" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
82 |
"HOL.equal l3_nam l3_nam \<longleftrightarrow> True" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
83 |
"HOL.equal l4_nam l4_nam \<longleftrightarrow> True" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
84 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
85 |
"HOL.equal val_nam next_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
86 |
"HOL.equal next_nam val_nam \<longleftrightarrow> False" |
12442 | 87 |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
88 |
"HOL.equal l_nam l1_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
89 |
"HOL.equal l_nam l2_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
90 |
"HOL.equal l_nam l3_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
91 |
"HOL.equal l_nam l4_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
92 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
93 |
"HOL.equal l1_nam l_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
94 |
"HOL.equal l1_nam l2_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
95 |
"HOL.equal l1_nam l3_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
96 |
"HOL.equal l1_nam l4_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
97 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
98 |
"HOL.equal l2_nam l_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
99 |
"HOL.equal l2_nam l1_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
100 |
"HOL.equal l2_nam l3_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
101 |
"HOL.equal l2_nam l4_nam \<longleftrightarrow> False" |
12442 | 102 |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
103 |
"HOL.equal l3_nam l_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
104 |
"HOL.equal l3_nam l1_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
105 |
"HOL.equal l3_nam l2_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
106 |
"HOL.equal l3_nam l4_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
107 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
108 |
"HOL.equal l4_nam l_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
109 |
"HOL.equal l4_nam l1_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
110 |
"HOL.equal l4_nam l2_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
111 |
"HOL.equal l4_nam l3_nam \<longleftrightarrow> False" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
112 |
by(simp_all add: distinct_fields distinct_fields[symmetric] distinct_vars distinct_vars[symmetric] equal_vnam_def) |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
113 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
114 |
axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
115 |
lemma equal_loc'_code [code]: |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
116 |
"HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
117 |
by(simp add: equal_loc'_def nat_to_loc'_inject) |
12442 | 118 |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
119 |
definition undefined_cname :: cname |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
120 |
where [code del]: "undefined_cname = undefined" |
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44037
diff
changeset
|
121 |
declare undefined_cname_def[symmetric, code_unfold] |
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
122 |
code_datatype Object Xcpt Cname undefined_cname |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
123 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
124 |
definition undefined_val :: val |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
125 |
where [code del]: "undefined_val = undefined" |
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44037
diff
changeset
|
126 |
declare undefined_val_def[symmetric, code_unfold] |
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
127 |
code_datatype Unit Null Bool Intg Addr undefined_val |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
128 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
129 |
definition E where |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
130 |
"E = Expr (l1_name::=NewC list_name);; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
131 |
Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
132 |
Expr (l2_name::=NewC list_name);; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
133 |
Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
134 |
Expr (l3_name::=NewC list_name);; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
135 |
Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
136 |
Expr (l4_name::=NewC list_name);; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
137 |
Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
138 |
Expr ({list_name}(LAcc l1_name).. |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
139 |
append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
140 |
Expr ({list_name}(LAcc l1_name).. |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
141 |
append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
142 |
Expr ({list_name}(LAcc l1_name).. |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
143 |
append_name({[RefT (ClassT list_name)]}[LAcc l4_name]))" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
144 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
145 |
definition test where |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
146 |
"test = Predicate.Pred (\<lambda>s. example_prg\<turnstile>Norm (empty, empty) -E-> s)" |
12442 | 147 |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
148 |
lemma test_code [code]: |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
149 |
"test = exec_i_i_i_o example_prg (Norm (empty, empty)) E" |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
150 |
by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def) |
12442 | 151 |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
152 |
ML {* |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
153 |
val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test}; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
154 |
locs @{code l1_name}; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
155 |
locs @{code l2_name}; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
156 |
locs @{code l3_name}; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
157 |
locs @{code l4_name}; |
12442 | 158 |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
159 |
fun list_fields n = |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
160 |
@{code snd} (@{code the} (heap (@{code Loc} (@{code "nat_to_loc'"} n)))); |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
161 |
fun val_field n = |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
162 |
list_fields n (@{code val_name}, @{code "list_name"}); |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
163 |
fun next_field n = |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
164 |
list_fields n (@{code next_name}, @{code "list_name"}); |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
165 |
val Suc = @{code Suc}; |
12442 | 166 |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
167 |
val_field @{code "0 :: nat"}; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
168 |
next_field @{code "0 :: nat"}; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
169 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
170 |
val_field @{code "1 :: nat"}; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
171 |
next_field @{code "1 :: nat"}; |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
172 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
173 |
val_field (Suc (Suc @{code "0 :: nat"})); |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
174 |
next_field (Suc (Suc @{code "0 :: nat"})); |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
175 |
|
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
176 |
val_field (Suc (Suc (Suc @{code "0 :: nat"}))); |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
39126
diff
changeset
|
177 |
next_field (Suc (Suc (Suc @{code "0 :: nat"}))); |
12442 | 178 |
*} |
179 |
||
180 |
end |