author | haftmann |
Tue, 07 Oct 2008 16:07:50 +0200 | |
changeset 28524 | 644b62cf678f |
parent 24783 | 5a3e336a2e37 |
child 32356 | e11cd88e6ade |
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 |
|
28524 | 8 |
theory JListExample |
9 |
imports Eval SystemClasses |
|
10 |
begin |
|
12442 | 11 |
|
12 |
ML {* Syntax.ambiguity_level := 100000 *} |
|
13 |
||
14 |
consts |
|
15 |
list_name :: cname |
|
16 |
append_name :: mname |
|
17 |
val_nam :: vnam |
|
18 |
next_nam :: vnam |
|
19 |
l_nam :: vnam |
|
20 |
l1_nam :: vnam |
|
21 |
l2_nam :: vnam |
|
22 |
l3_nam :: vnam |
|
23 |
l4_nam :: vnam |
|
24 |
||
25 |
constdefs |
|
26 |
val_name :: vname |
|
27 |
"val_name == VName val_nam" |
|
28 |
||
29 |
next_name :: vname |
|
30 |
"next_name == VName next_nam" |
|
31 |
||
32 |
l_name :: vname |
|
33 |
"l_name == VName l_nam" |
|
34 |
||
35 |
l1_name :: vname |
|
36 |
"l1_name == VName l1_nam" |
|
37 |
||
38 |
l2_name :: vname |
|
39 |
"l2_name == VName l2_nam" |
|
40 |
||
41 |
l3_name :: vname |
|
42 |
"l3_name == VName l3_nam" |
|
43 |
||
44 |
l4_name :: vname |
|
45 |
"l4_name == VName l4_nam" |
|
46 |
||
47 |
list_class :: "java_mb class" |
|
48 |
"list_class == |
|
49 |
(Object, |
|
50 |
[(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))], |
|
51 |
[((append_name, [RefT (ClassT list_name)]), PrimT Void, |
|
52 |
([l_name], [], |
|
53 |
If(BinOp Eq ({list_name}(LAcc This)..next_name) (Lit Null)) |
|
54 |
Expr ({list_name}(LAcc This)..next_name:=LAcc l_name) |
|
55 |
Else |
|
56 |
Expr ({list_name}({list_name}(LAcc This)..next_name).. |
|
57 |
append_name({[RefT (ClassT list_name)]}[LAcc l_name])), |
|
58 |
Lit Unit))])" |
|
59 |
||
60 |
example_prg :: "java_mb prog" |
|
61 |
"example_prg == [ObjectC, (list_name, list_class)]" |
|
62 |
||
63 |
types_code |
|
64 |
cname ("string") |
|
65 |
vnam ("string") |
|
66 |
mname ("string") |
|
24783 | 67 |
loc' ("int") |
12442 | 68 |
|
69 |
consts_code |
|
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16417
diff
changeset
|
70 |
"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
|
71 |
attach {* |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16417
diff
changeset
|
72 |
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
|
73 |
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
|
74 |
in nr 0 end; |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16417
diff
changeset
|
75 |
*} |
12442 | 76 |
|
28524 | 77 |
"undefined" ("(raise Match)") |
78 |
"undefined :: val" ("{* Unit *}") |
|
79 |
"undefined :: cname" ("\"\"") |
|
12442 | 80 |
|
81 |
"Object" ("\"Object\"") |
|
82 |
"list_name" ("\"list\"") |
|
83 |
"append_name" ("\"append\"") |
|
84 |
"val_nam" ("\"val\"") |
|
85 |
"next_nam" ("\"next\"") |
|
86 |
"l_nam" ("\"l\"") |
|
87 |
"l1_nam" ("\"l1\"") |
|
88 |
"l2_nam" ("\"l2\"") |
|
89 |
"l3_nam" ("\"l3\"") |
|
90 |
"l4_nam" ("\"l4\"") |
|
91 |
||
17145 | 92 |
code_module J |
93 |
contains |
|
13890 | 94 |
test = "example_prg\<turnstile>Norm (empty, empty) |
12442 | 95 |
-(Expr (l1_name::=NewC list_name);; |
96 |
Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));; |
|
97 |
Expr (l2_name::=NewC list_name);; |
|
98 |
Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));; |
|
99 |
Expr (l3_name::=NewC list_name);; |
|
100 |
Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));; |
|
101 |
Expr (l4_name::=NewC list_name);; |
|
102 |
Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));; |
|
103 |
Expr ({list_name}(LAcc l1_name).. |
|
104 |
append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));; |
|
105 |
Expr ({list_name}(LAcc l1_name).. |
|
106 |
append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));; |
|
107 |
Expr ({list_name}(LAcc l1_name).. |
|
12565 | 108 |
append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _" |
12442 | 109 |
|
12911 | 110 |
section {* Big step execution *} |
12442 | 111 |
|
112 |
ML {* |
|
113 |
||
24460
62b96cf2bebb
Code generator now uses sequences with depth limit.
berghofe
parents:
22921
diff
changeset
|
114 |
val SOME ((_, (heap, locs)), _) = DSeq.pull J.test; |
17145 | 115 |
locs J.l1_name; |
116 |
locs J.l2_name; |
|
117 |
locs J.l3_name; |
|
118 |
locs J.l4_name; |
|
119 |
snd (J.the (heap (J.Loc 0))) (J.val_name, "list"); |
|
120 |
snd (J.the (heap (J.Loc 0))) (J.next_name, "list"); |
|
121 |
snd (J.the (heap (J.Loc 1))) (J.val_name, "list"); |
|
122 |
snd (J.the (heap (J.Loc 1))) (J.next_name, "list"); |
|
123 |
snd (J.the (heap (J.Loc 2))) (J.val_name, "list"); |
|
124 |
snd (J.the (heap (J.Loc 2))) (J.next_name, "list"); |
|
125 |
snd (J.the (heap (J.Loc 3))) (J.val_name, "list"); |
|
126 |
snd (J.the (heap (J.Loc 3))) (J.next_name, "list"); |
|
12442 | 127 |
|
128 |
*} |
|
129 |
||
130 |
end |