author | wenzelm |
Sun, 30 Sep 2007 21:55:15 +0200 | |
changeset 24783 | 5a3e336a2e37 |
parent 24460 | 62b96cf2bebb |
child 28524 | 644b62cf678f |
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") |
|
24783 | 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 |
|
18679 | 75 |
"arbitrary" ("(raise Match)") |
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
18679
diff
changeset
|
76 |
"arbitrary :: val" ("{* Unit *}") |
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
18679
diff
changeset
|
77 |
"arbitrary :: cname" ("\"\"") |
12442 | 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 |
||
17145 | 90 |
code_module J |
91 |
contains |
|
13890 | 92 |
test = "example_prg\<turnstile>Norm (empty, empty) |
12442 | 93 |
-(Expr (l1_name::=NewC list_name);; |
94 |
Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));; |
|
95 |
Expr (l2_name::=NewC list_name);; |
|
96 |
Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));; |
|
97 |
Expr (l3_name::=NewC list_name);; |
|
98 |
Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));; |
|
99 |
Expr (l4_name::=NewC list_name);; |
|
100 |
Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));; |
|
101 |
Expr ({list_name}(LAcc l1_name).. |
|
102 |
append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));; |
|
103 |
Expr ({list_name}(LAcc l1_name).. |
|
104 |
append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));; |
|
105 |
Expr ({list_name}(LAcc l1_name).. |
|
12565 | 106 |
append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _" |
12442 | 107 |
|
12911 | 108 |
section {* Big step execution *} |
12442 | 109 |
|
110 |
ML {* |
|
111 |
||
24460
62b96cf2bebb
Code generator now uses sequences with depth limit.
berghofe
parents:
22921
diff
changeset
|
112 |
val SOME ((_, (heap, locs)), _) = DSeq.pull J.test; |
17145 | 113 |
locs J.l1_name; |
114 |
locs J.l2_name; |
|
115 |
locs J.l3_name; |
|
116 |
locs J.l4_name; |
|
117 |
snd (J.the (heap (J.Loc 0))) (J.val_name, "list"); |
|
118 |
snd (J.the (heap (J.Loc 0))) (J.next_name, "list"); |
|
119 |
snd (J.the (heap (J.Loc 1))) (J.val_name, "list"); |
|
120 |
snd (J.the (heap (J.Loc 1))) (J.next_name, "list"); |
|
121 |
snd (J.the (heap (J.Loc 2))) (J.val_name, "list"); |
|
122 |
snd (J.the (heap (J.Loc 2))) (J.next_name, "list"); |
|
123 |
snd (J.the (heap (J.Loc 3))) (J.val_name, "list"); |
|
124 |
snd (J.the (heap (J.Loc 3))) (J.next_name, "list"); |
|
12442 | 125 |
|
126 |
*} |
|
127 |
||
128 |
end |