equal
deleted
inserted
replaced
3 Author: Stefan Berghofer |
3 Author: Stefan Berghofer |
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{Example for generating executable code from Java semantics} *} |
6 header {* \isaheader{Example for generating executable code from Java semantics} *} |
7 |
7 |
8 theory JListExample imports Eval SystemClasses begin |
8 theory JListExample |
|
9 imports Eval SystemClasses |
|
10 begin |
9 |
11 |
10 ML {* Syntax.ambiguity_level := 100000 *} |
12 ML {* Syntax.ambiguity_level := 100000 *} |
11 |
13 |
12 consts |
14 consts |
13 list_name :: cname |
15 list_name :: cname |
70 fun new_addr p none loc hp = |
72 fun new_addr p none loc hp = |
71 let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); |
73 let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); |
72 in nr 0 end; |
74 in nr 0 end; |
73 *} |
75 *} |
74 |
76 |
75 "arbitrary" ("(raise Match)") |
77 "undefined" ("(raise Match)") |
76 "arbitrary :: val" ("{* Unit *}") |
78 "undefined :: val" ("{* Unit *}") |
77 "arbitrary :: cname" ("\"\"") |
79 "undefined :: cname" ("\"\"") |
78 |
80 |
79 "Object" ("\"Object\"") |
81 "Object" ("\"Object\"") |
80 "list_name" ("\"list\"") |
82 "list_name" ("\"list\"") |
81 "append_name" ("\"append\"") |
83 "append_name" ("\"append\"") |
82 "val_nam" ("\"val\"") |
84 "val_nam" ("\"val\"") |