author | berghofe |
Tue, 12 Jul 2005 11:51:31 +0200 | |
changeset 16770 | 1f1b1fae30e4 |
parent 16417 | 9bc16273c2d4 |
child 17145 | e623e57b0f44 |
permissions | -rw-r--r-- |
12951 | 1 |
(* Title: HOL/MicroJava/J/JListExample.thy |
12442 | 2 |
ID: $Id$ |
3 |
Author: Stefan Berghofer |
|
4 |
*) |
|
5 |
||
12911 | 6 |
header {* \isaheader{Example for generating executable code from Java semantics} *} |
12442 | 7 |
|
16417 | 8 |
theory JListExample imports Eval SystemClasses begin |
12442 | 9 |
|
10 |
ML {* Syntax.ambiguity_level := 100000 *} |
|
11 |
||
12 |
consts |
|
13 |
list_name :: cname |
|
14 |
append_name :: mname |
|
15 |
val_nam :: vnam |
|
16 |
next_nam :: vnam |
|
17 |
l_nam :: vnam |
|
18 |
l1_nam :: vnam |
|
19 |
l2_nam :: vnam |
|
20 |
l3_nam :: vnam |
|
21 |
l4_nam :: vnam |
|
22 |
||
23 |
constdefs |
|
24 |
val_name :: vname |
|
25 |
"val_name == VName val_nam" |
|
26 |
||
27 |
next_name :: vname |
|
28 |
"next_name == VName next_nam" |
|
29 |
||
30 |
l_name :: vname |
|
31 |
"l_name == VName l_nam" |
|
32 |
||
33 |
l1_name :: vname |
|
34 |
"l1_name == VName l1_nam" |
|
35 |
||
36 |
l2_name :: vname |
|
37 |
"l2_name == VName l2_nam" |
|
38 |
||
39 |
l3_name :: vname |
|
40 |
"l3_name == VName l3_nam" |
|
41 |
||
42 |
l4_name :: vname |
|
43 |
"l4_name == VName l4_nam" |
|
44 |
||
45 |
list_class :: "java_mb class" |
|
46 |
"list_class == |
|
47 |
(Object, |
|
48 |
[(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))], |
|
49 |
[((append_name, [RefT (ClassT list_name)]), PrimT Void, |
|
50 |
([l_name], [], |
|
51 |
If(BinOp Eq ({list_name}(LAcc This)..next_name) (Lit Null)) |
|
52 |
Expr ({list_name}(LAcc This)..next_name:=LAcc l_name) |
|
53 |
Else |
|
54 |
Expr ({list_name}({list_name}(LAcc This)..next_name).. |
|
55 |
append_name({[RefT (ClassT list_name)]}[LAcc l_name])), |
|
56 |
Lit Unit))])" |
|
57 |
||
58 |
example_prg :: "java_mb prog" |
|
59 |
"example_prg == [ObjectC, (list_name, list_class)]" |
|
60 |
||
61 |
types_code |
|
62 |
cname ("string") |
|
63 |
vnam ("string") |
|
64 |
mname ("string") |
|
13672 | 65 |
loc_ ("int") |
12442 | 66 |
|
67 |
consts_code |
|
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16417
diff
changeset
|
68 |
"new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}") |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16417
diff
changeset
|
69 |
attach {* |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16417
diff
changeset
|
70 |
fun new_addr p none loc hp = |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16417
diff
changeset
|
71 |
let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16417
diff
changeset
|
72 |
in nr 0 end; |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16417
diff
changeset
|
73 |
*} |
12442 | 74 |
|
75 |
"arbitrary" ("(raise ERROR)") |
|
76 |
"arbitrary" :: "val" ("{* Unit *}") |
|
77 |
"arbitrary" :: "cname" ("\"\"") |
|
78 |
||
79 |
"Object" ("\"Object\"") |
|
80 |
"list_name" ("\"list\"") |
|
81 |
"append_name" ("\"append\"") |
|
82 |
"val_nam" ("\"val\"") |
|
83 |
"next_nam" ("\"next\"") |
|
84 |
"l_nam" ("\"l\"") |
|
85 |
"l1_nam" ("\"l1\"") |
|
86 |
"l2_nam" ("\"l2\"") |
|
87 |
"l3_nam" ("\"l3\"") |
|
88 |
"l4_nam" ("\"l4\"") |
|
89 |
||
90 |
generate_code |
|
13890 | 91 |
test = "example_prg\<turnstile>Norm (empty, empty) |
12442 | 92 |
-(Expr (l1_name::=NewC list_name);; |
93 |
Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));; |
|
94 |
Expr (l2_name::=NewC list_name);; |
|
95 |
Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));; |
|
96 |
Expr (l3_name::=NewC list_name);; |
|
97 |
Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));; |
|
98 |
Expr (l4_name::=NewC list_name);; |
|
99 |
Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));; |
|
100 |
Expr ({list_name}(LAcc l1_name).. |
|
101 |
append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));; |
|
102 |
Expr ({list_name}(LAcc l1_name).. |
|
103 |
append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));; |
|
104 |
Expr ({list_name}(LAcc l1_name).. |
|
12565 | 105 |
append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _" |
12442 | 106 |
|
12911 | 107 |
section {* Big step execution *} |
12442 | 108 |
|
109 |
ML {* |
|
110 |
||
15531 | 111 |
val SOME ((_, (heap, locs)), _) = Seq.pull test; |
12442 | 112 |
locs l1_name; |
113 |
locs l2_name; |
|
114 |
locs l3_name; |
|
115 |
locs l4_name; |
|
13672 | 116 |
snd (the (heap (Loc 0))) (val_name, "list"); |
117 |
snd (the (heap (Loc 0))) (next_name, "list"); |
|
118 |
snd (the (heap (Loc 1))) (val_name, "list"); |
|
119 |
snd (the (heap (Loc 1))) (next_name, "list"); |
|
120 |
snd (the (heap (Loc 2))) (val_name, "list"); |
|
121 |
snd (the (heap (Loc 2))) (next_name, "list"); |
|
122 |
snd (the (heap (Loc 3))) (val_name, "list"); |
|
123 |
snd (the (heap (Loc 3))) (next_name, "list"); |
|
12442 | 124 |
|
125 |
*} |
|
126 |
||
127 |
end |