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